Types under unramified base change

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Unramified.FrobeniusDescent7 8/-!9# Types under unramified base change10 11Let `O → Oδ` be an unramified extension of complete DVRs of degree `δ` (in the applications12`Oδ = O[X]/(Φ)` for an unramified lift `Φ`). This file compares invariants and types over `O` and13over `Oδ`: the invariant `(e, f)` of a field over `Oδ` becomes `(e, δ f)` over `O`, so algebra types14descend by `scaleType δ`; the Frobenius of `Oδ` extends to the fraction fields with fixed field15`K = Frac O`, making `Kδ/K` finite separable; polynomial types ascend from `O` to `Oδ`; and a16Frobenius-invariant product of conjugates of a typed polynomial over `Oδ` descends to `O` with the17scaled type.18 19## Main results20 21* `SurfaceBlowup.field_invariant_unramified_tower`, `SurfaceBlowup.algebra_type_unramified_descent`22* `SurfaceBlowup.frobenius_fraction_extension`, `SurfaceBlowup.unramified_fraction_isSeparable`23* `SurfaceBlowup.factor_invariant_unramified_scale`, `SurfaceBlowup.polynomial_type_map_unramified`24* `SurfaceBlowup.descended_polynomial_type`25 26Provenance: Thm_SurfaceBlowupV2_{field_invariant_unramified_tower,27algebra_type_unramified_descent, factor_invariant_unramified_scale, frobenius_fraction_extension,28descended_polynomial_type}; Thm_Gen_UnramifiedAscent.29-/30 31namespace SurfaceBlowup32 33open Polynomial34 35/-! ### Invariants in an unramified tower -/36 37/-- `K`-isomorphic finite extensions of `K = Frac O` (one with finite closure) have the same38invariants, and the other one also has finite closure. -/39private theorem fieldInvariant_congr (O : Type) [CommRing O] [IsDomain O]40    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]41    [Finite (IsLocalRing.ResidueField O)] (L L' : Type) [Field L] [Field L']42    [Algebra (BaseField O) L] [Algebra O L] [IsScalarTower O (BaseField O) L]43    [FiniteDimensional (BaseField O) L] [Algebra (BaseField O) L'] [Algebra O L']44    [IsScalarTower O (BaseField O) L'] [FiniteDimensional (BaseField O) L']45    (e : L ≃ₐ[BaseField O] L') [Module.Finite O (integralClosure O L)] :46    fieldInvariant O L = fieldInvariant O L' ∧ Module.Finite O (integralClosure O L') := by47  obtain ⟨φ, -⟩ := integral_closure_algEquiv O L L' (e.restrictScalars O)48  exact ⟨field_invariant_algEquiv O L L' e inferInstance, .equiv φ.toLinearEquiv⟩49 50/-- In an unramified tower `O → Oδ` of degree `δ`, the invariant `(e, f)` of a finite extension51`L` over `Oδ` becomes `(e, δ f)` over `O`. -/52theorem field_invariant_unramified_tower (O Oδ : Type) [CommRing O] [IsDomain O](6.4)53    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]54    [Algebra O Oδ] [Module.Finite O Oδ] [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ)55    (pi : O) (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi))56    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (L : Type)57    [Field L] [Algebra O L] [Algebra Oδ L] [IsScalarTower O Oδ L] [Algebra (BaseField O) L]58    [IsScalarTower O (BaseField O) L] [FiniteDimensional (BaseField O) L] [Algebra (BaseField Oδ) L]59    [IsScalarTower Oδ (BaseField Oδ) L] [FiniteDimensional (BaseField Oδ) L]60    (hfinδ : Module.Finite Oδ (integralClosure Oδ L)) :61    fieldInvariant O L = ((fieldInvariant Oδ L).1, δ * (fieldInvariant Oδ L).2) := by62  -- `Oδ` is again complete with finite residue field63  have hmap : (IsLocalRing.maximalIdeal O).map (algebraMap O Oδ) = IsLocalRing.maximalIdeal Oδ := by64    rw [(IsDiscreteValuationRing.irreducible_iff_uniformizer pi).1 hpi,65      (IsDiscreteValuationRing.irreducible_iff_uniformizer _).1 hpiδ, Ideal.map_span,66      Set.image_singleton]67  have : IsAdicComplete (IsLocalRing.maximalIdeal Oδ) Oδ := by68    rw [← hmap]69    exact (IsAdicComplete.map_algebraMap_iff _ _).270      (finite_free_adic_complete O Oδ (IsLocalRing.maximalIdeal O))71  have : Finite (IsLocalRing.ResidueField Oδ) := by72    have : Finite (O ⧸ IsLocalRing.maximalIdeal O) :=73      inferInstanceAs (Finite (IsLocalRing.ResidueField O))74    have := finite_free_residue_quotient O Oδ (IsLocalRing.maximalIdeal O)75    have hle : (IsLocalRing.maximalIdeal O • ⊤ : Submodule O Oδ) ≤76        LinearMap.ker (Ideal.Quotient.mkₐ O (IsLocalRing.maximalIdeal Oδ)).toLinearMap := by77      refine Submodule.smul_le.2 fun r hr n _ ↦ ?_78      rw [LinearMap.mem_ker, AlgHom.toLinearMap_apply, Ideal.Quotient.mkₐ_eq_mk,79        Ideal.Quotient.eq_zero_iff_mem, Algebra.smul_def]80      exact Ideal.mul_mem_right _ _ (hmap ▸ Ideal.mem_map_of_mem _ hr)81    refine Finite.of_surjective ((IsLocalRing.maximalIdeal O • ⊤ : Submodule O Oδ).liftQ _ hle)82      fun y ↦ ?_83    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective y84    exact ⟨Submodule.Quotient.mk x, rfl⟩85  -- compare the two (equal) integral closures, both DVRs86  have := closure_finite_descent O Oδ L hfinδ87  have h1 := integral_closure_is_local O (BaseField O) L88  have h2 := integral_closure_is_local Oδ (BaseField Oδ) L89  have := integral_closure_is_dvr O (BaseField O) L90  have := integral_closure_is_dvr Oδ (BaseField Oδ) L91  obtain ⟨-, _, -⟩ := integral_closure_finite_free Oδ (BaseField Oδ) L92  have : Algebra.IsIntegral O Oδ := Algebra.IsIntegral.of_finite O Oδ93  have : Algebra.IsIntegral O (integralClosure Oδ L) := .trans Oδ94  obtain ⟨hr, hi⟩ := dvr_algEquiv_ramification_inertia O _ _95    (algebraMap_injective_of_tower O _ L) (algebraMap_injective_of_tower O _ L)96    (integralClosureTowerEquiv O Oδ L)97  unfold fieldInvariant98  rw [dif_pos h1, dif_pos h2]99  rw [hr, hi, ramificationIdx_unramified_tower O Oδ (integralClosure Oδ L) δ hrank pi hpi hpiδ,100    inertiaDeg_unramified_tower O Oδ (integralClosure Oδ L) δ hrank pi hpi hpiδ]101 102/-- Algebra types descend along an unramified extension `O → Oδ` of degree `δ`, scaled by `δ`. -/103theorem algebra_type_unramified_descent (O Oδ : Type) [CommRing O] [IsDomain O](6.4)104    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]105    [Algebra O Oδ] [Module.Finite O Oδ] [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ)106    (pi : O) (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi))107    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (B : Type)108    [CommRing B] [Algebra O B] [Algebra Oδ B] [IsScalarTower O Oδ B] (σ : FactorType)109    (h : HasAlgebraType Oδ B σ) :110    HasAlgebraType O B (scaleType δ σ) := by111  obtain ⟨ι, hι, L, hF, hK, hO, hT, hFD, e, rfl, hfinL⟩ := h112  obtain ⟨hK', hO', hT', hT'', hFD', E, -⟩ :=113    unramified_generic_fibre_witness O Oδ δ hrank pi hpi hpiδ B ι L e114  refine ⟨ι, hι, L, hF, hK', hO', hT', hFD', E, ?_,115    fun i ↦ closure_finite_descent O Oδ (L i) (hfinL i)⟩116  unfold scaleType117  rw [← Multiset.coe_mapAddMonoidHom, map_sum]118  simp only [Multiset.coe_mapAddMonoidHom, Multiset.map_singleton,119    field_invariant_unramified_tower O Oδ δ hrank pi hpi hpiδ _ (hfinL _)]120 121/-! ### Frobenius on the fraction field -/122 123/-- The Frobenius iterates of `Oδ = O[X]/(Φ)` extend to automorphisms `τ i` of `Kδ = Frac Oδ`124fixing `K`; `τ` is a group action of `ℕ` with `τ δ = id`, and the fixed field of `τ 1` is `K`. -/125theorem frobenius_fraction_extension (O : Type) [CommRing O] [IsDomain O]126    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]127    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)128    [IsDomain (AdjoinRoot Φ)] (ι : BaseField O →+* BaseField (AdjoinRoot Φ))129    (hι : ∀ c : O, ι (algebraMap O (BaseField O) c) =130      algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) (algebraMap O (AdjoinRoot Φ) c)) :131    ∃ τ : ℕ → (BaseField (AdjoinRoot Φ) ≃+* BaseField (AdjoinRoot Φ)),132      (∀ (i : ℕ) (x : AdjoinRoot Φ), τ i (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) x) =133        algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) (frobeniusIter O Φ i x))134      ∧ (∀ (i : ℕ) (y : BaseField O), τ i (ι y) = ι y)135      ∧ τ 0 = RingEquiv.refl (BaseField (AdjoinRoot Φ)) ∧ (∀ i : ℕ, τ (i + 1) = (τ i).trans (τ 1))136      ∧ (∀ z : BaseField (AdjoinRoot Φ), τ Φ.natDegree z = z)137      ∧ (∀ z : BaseField (AdjoinRoot Φ), τ 1 z = z → ∃ y : BaseField O, ι y = z) := by138  obtain ⟨hid, hbij⟩ := frobenius_pow_degree_eq_id O Φ hΦ139  have bij : ∀ i, Function.Bijective (frobeniusIter O Φ i) := fun i ↦ by140    induction i with141    | zero => exact Function.bijective_id142    | succ i ih =>143      change Function.Bijective (⇑(unramifiedFrobenius O Φ) ∘ ⇑(frobeniusIter O Φ i))144      exact hbij.comp ih145  set K := BaseField (AdjoinRoot Φ)146  let τ : ℕ → (K ≃+* K) := fun i ↦ IsFractionRing.ringEquivOfRingEquiv147    (RingEquiv.ofBijective (frobeniusIter O Φ i).toRingHom (bij i))148  have h1 : ∀ (i : ℕ) (x : AdjoinRoot Φ),149      τ i (algebraMap (AdjoinRoot Φ) K x) = algebraMap (AdjoinRoot Φ) K (frobeniusIter O Φ i x) :=150    fun i x ↦ IsFractionRing.ringEquivOfRingEquiv_algebraMap _ x151  have ext : ∀ f g : K ≃+* K,152      (∀ x : AdjoinRoot Φ, f (algebraMap _ _ x) = g (algebraMap _ _ x)) → f = g := fun f g h ↦153    RingEquiv.toRingHom_injective154      (IsLocalization.ringHom_ext (nonZeroDivisors (AdjoinRoot Φ)) (RingHom.ext h))155  refine ⟨τ, h1, fun i y ↦ ?_, ext _ _ fun x ↦ by rw [h1]; rfl,156    fun i ↦ ext _ _ fun x ↦ by rw [RingEquiv.trans_apply, h1, h1, h1]; rfl,157    fun z ↦ by rw [ext (τ Φ.natDegree) (RingEquiv.refl _) fun x ↦ by rw [h1, hid]; rfl]; rfl,158    fun z hz ↦ ?_⟩159  · refine RingHom.congr_fun (?_ : (τ i).toRingHom.comp ι = ι) y160    refine IsLocalization.ringHom_ext (nonZeroDivisors O) (RingHom.ext fun c ↦ ?_)161    simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom]162    rw [hι, h1, AlgHom.commutes]163  · -- write `z = a' / ϖᵏ` with `ϖ ∈ O` a uniformizer; then `a'` is Frobenius-fixed, so in `O`164    obtain ⟨_, _, hdvr, -, hirr, -⟩ := unramified_is_dvr O Φ hΦ165    obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible O166    obtain ⟨a, s, hs, rfl⟩ := IsFractionRing.div_surjective (A := AdjoinRoot Φ) z167    obtain ⟨k, u, hu⟩ :=168      IsDiscreteValuationRing.eq_unit_mul_pow_irreducible (nonZeroDivisors.ne_zero hs) (hirr ϖ hϖ)169    have hdK : algebraMap (AdjoinRoot Φ) K (algebraMap O (AdjoinRoot Φ) (ϖ ^ k)) ≠ 0 :=170      IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero (by171        rw [map_pow]; exact pow_ne_zero _ (hirr ϖ hϖ).ne_zero))172    set a' := a * ↑u⁻¹ with ha'173    have hz' : algebraMap (AdjoinRoot Φ) K a / algebraMap (AdjoinRoot Φ) K s =174        algebraMap (AdjoinRoot Φ) K a' /175          algebraMap (AdjoinRoot Φ) K (algebraMap O (AdjoinRoot Φ) (ϖ ^ k)) := by176      rw [div_eq_div_iff (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hs) hdK, ← map_mul,177        ← map_mul, hu, ha', map_pow]178      rw [mul_assoc, Units.inv_mul_cancel_left]179    rw [hz'] at hz ⊢180    rw [map_div₀, h1, h1, AlgHom.commutes] at hz181    obtain ⟨c, hc⟩ := frobenius_fixed_ring O Φ hΦ a'182      (IsFractionRing.injective (AdjoinRoot Φ) K ((div_left_inj' hdK).mp hz))183    exact ⟨algebraMap O (BaseField O) c / algebraMap O (BaseField O) (ϖ ^ k),184      by rw [map_div₀, hι, hι, hc]⟩185 186/-! ### Ascent and descent of polynomial types -/187 188section Ascent189 190variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]191  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]192  (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) [IsDomain (AdjoinRoot Φ)]193  (ι : BaseField O →+* BaseField (AdjoinRoot Φ))194  (hι : ∀ c : O, ι (algebraMap O (BaseField O) c) =195    algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) (algebraMap O (AdjoinRoot Φ) c))196 197include hΦ hι in198/-- The unramified fraction-field extension `Kδ/K` is finite and separable (it is Galois: the199Frobenius `τ 1` already has fixed field `K`). -/200theorem unramified_fraction_isSeparable :201    letI := ι.toAlgebra202    FiniteDimensional (BaseField O) (BaseField (AdjoinRoot Φ)) ∧203      Algebra.IsSeparable (BaseField O) (BaseField (AdjoinRoot Φ)) := by204  let := ι.toAlgebra205  obtain ⟨ι0, hι0, -, huniq, hfin0, -⟩ := unramified_fraction_field_lift O Φ hΦ206  obtain rfl : ι = ι0 := huniq ι hι207  have hfd : FiniteDimensional (BaseField O) (BaseField (AdjoinRoot Φ)) := hfin0208  obtain ⟨τ, -, hτι, -, -, -, hfix⟩ := frobenius_fraction_extension O Φ hΦ ι hι209  let σ1 : BaseField (AdjoinRoot Φ) ≃ₐ[BaseField O] BaseField (AdjoinRoot Φ) :=210    AlgEquiv.ofRingEquiv (f := τ 1) (hτι 1)211  have : IsGalois (BaseField O) (BaseField (AdjoinRoot Φ)) :=212    IsGalois.of_fixedField_eq_bot _ _ <| eq_bot_iff.2 fun x hx ↦ by213      obtain ⟨y, rfl⟩ := hfix x ((IntermediateField.mem_fixedField_iff _ _).1 hx σ1214        (Subgroup.mem_top σ1))215      exact IntermediateField.algebraMap_mem _ y216  exact ⟨hfd, inferInstance⟩217 218/-- For a monic irreducible `H` over `K` whose root field is `K`-isomorphic to the root field of a219monic irreducible `g` over `Kδ` (with finite `Oδ`-closure), the factor invariant of `H` is that220of `g` with inertia degree scaled by `δ = deg Φ`, and `H` has finite `O`-closure. -/221theorem factor_invariant_unramified_scale (O : Type) [CommRing O] [IsDomain O]222    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]223    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)224    [IsDomain (AdjoinRoot Φ)] (ι : BaseField O →+* BaseField (AdjoinRoot Φ))225    (hι : ∀ c : O, ι (algebraMap O (BaseField O) c) =226      algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) (algebraMap O (AdjoinRoot Φ) c))227    (g : Polynomial (BaseField (AdjoinRoot Φ))) (hg : g.Monic) (hgi : Irreducible g)228    (H : Polynomial (BaseField O)) (hH : H.Monic) (hHi : Irreducible H)229    (hiso : letI := ι.toAlgebra; Nonempty (AdjoinRoot H ≃ₐ[BaseField O] AdjoinRoot g))230    (hfinδ : Module.Finite (AdjoinRoot Φ) (integralClosure (AdjoinRoot Φ) (AdjoinRoot g))) :231    factorInvariant O H = ((factorInvariant (AdjoinRoot Φ) g).1,232      Φ.natDegree * (factorInvariant (AdjoinRoot Φ) g).2) ∧233      Module.Finite O (integralClosure O (AdjoinRoot H)) := by234  let _ := ι.toAlgebra235  set K := BaseField O236  set Oδ := AdjoinRoot Φ237  set Kδ := BaseField Oδ238  set L := AdjoinRoot g239  obtain ⟨_, _, hdvrδ, -, hirrδ, _, _, -⟩ := unramified_is_dvr O Φ hΦ240  obtain ⟨hfree, hfin, hrank⟩ := unramified_free_module O Φ hΦ.1241  obtain ⟨hfd, -⟩ := unramified_fraction_isSeparable O Φ hΦ ι hι242  have : Fact (Irreducible g) := ⟨hgi⟩243  have : Fact (Irreducible H) := ⟨hHi⟩244  have : IsScalarTower O K Kδ := .of_algebraMap_eq fun c ↦ (hι c).symm245  have : IsScalarTower O K L := .of_algebraMap_eq fun c ↦ by246    rw [IsScalarTower.algebraMap_apply O Kδ L, IsScalarTower.algebraMap_apply K Kδ L,247      IsScalarTower.algebraMap_apply O K Kδ]248  have : IsScalarTower O Oδ L := .of_algebraMap_eq fun c ↦ by249    rw [IsScalarTower.algebraMap_apply O Kδ L, IsScalarTower.algebraMap_apply Oδ Kδ L,250      IsScalarTower.algebraMap_apply O Oδ Kδ]251  have : Module.Finite K (AdjoinRoot H) := hH.finite_adjoinRoot252  have : Module.Finite Kδ L := hg.finite_adjoinRoot253  have : Module.Finite K L := .trans Kδ L254  have : Module.Finite O (integralClosure O L) := closure_finite_descent O Oδ L hfinδ255  obtain ⟨e⟩ : Nonempty (AdjoinRoot H ≃ₐ[K] L) := hiso256  obtain ⟨hinv, hfinH⟩ := fieldInvariant_congr O L (AdjoinRoot H) e.symm257  obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O258  refine ⟨?_, hfinH⟩259  change fieldInvariant O (AdjoinRoot H) =260    ((fieldInvariant Oδ L).1, Φ.natDegree * (fieldInvariant Oδ L).2)261  rw [← hinv, field_invariant_unramified_tower O Oδ Φ.natDegree hrank pi hpi (hirrδ pi hpi) L hfinδ]262 263include hΦ hι in264/-- An irreducible factor type over `O` ascends to a type over `Oδ`. -/265private theorem polynomial_type_map_irreducible (g : Polynomial (BaseField O)) (hgm : g.Monic)266    (hgi : Irreducible g) (hfin : Module.Finite O (integralClosure O (AdjoinRoot g))) :267    ∃ τ' : FactorType, HasPolynomialTypeF (AdjoinRoot Φ) (g.map ι) τ' := by268  let := ι.toAlgebra269  obtain ⟨hfd, hsep⟩ := unramified_fraction_isSeparable O Φ hΦ ι hι270  have : Fact (Irreducible g) := ⟨hgi⟩271  obtain ⟨-, hfinδ, -⟩ := unramified_free_module O Φ hΦ.1272  have : IsScalarTower O (BaseField O) (BaseField (AdjoinRoot Φ)) :=273    .of_algebraMap_eq fun c ↦ by274      rw [IsScalarTower.algebraMap_apply O (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))]275      exact (hι c).symm276  refine squarefree_monic_has_polynomial_type (AdjoinRoot Φ) _ (hgm.map _)277    (squarefree_map_of_isSeparable _ _ g) fun h hh ↦ ?_278  exact closure_finite_ascent_root O (AdjoinRoot Φ) (BaseField O) (BaseField (AdjoinRoot Φ)) g hgm279    hgi hfin h (UniqueFactorizationMonoid.irreducible_of_normalized_factor h hh)280    (UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hh)281 282include hΦ hι in283/-- A polynomial with a type over `O` has a type over the unramified extension `Oδ`. -/284theorem polynomial_type_map_unramified (F : Polynomial (BaseField O)) (σ : FactorType)285    (hF : HasPolynomialTypeF O F σ) :286    ∃ τ' : FactorType, HasPolynomialTypeF (AdjoinRoot Φ) (F.map ι) τ' := by287  obtain ⟨gs, hgs, hpw, rfl, -, hfin⟩ := hF288  induction gs with289  | nil => exact ⟨0, [], by simp, by simp, by simp, by simp, by simp⟩290  | cons g t ih =>291    rw [List.pairwise_cons] at hpw292    obtain ⟨τ1, h1⟩ := polynomial_type_map_irreducible O Φ hΦ ι hι g (hgs g (by simp)).1293      (hgs g (by simp)).2 (hfin g (by simp))294    obtain ⟨τ2, h2⟩ := ih (fun x hx ↦ hgs x (by simp [hx])) hpw.2295      (fun x hx ↦ hfin x (by simp [hx]))296    have hc : ∀ l : List (Polynomial (BaseField O)), (∀ x ∈ l, IsCoprime g x) →297        IsCoprime g l.prod := by298      intro l299      induction l with300      | nil => exact fun _ ↦ isCoprime_one_right301      | cons x l ih2 => exact fun h ↦302        (h x (by simp)).mul_right (ih2 fun y hy ↦ h y (by simp [hy]))303    have hct : IsCoprime g t.prod := hc t fun x hx ↦304      distinct_monic_irreducible_coprime _ g x (hgs g (by simp)).1 (hgs x (by simp [hx])).1305        (hgs g (by simp)).2 (hgs x (by simp [hx])).2 (hpw.1 x hx)306    rw [List.prod_cons, Polynomial.map_mul]307    exact ⟨_, polynomial_type_mul_coprime _ _ _ _ _ h1 h2 (hct.map (mapRingHom ι))⟩308 309end Ascent310 311/-- Descent of polynomial types: if `F` over `Oδ` has type `σ` with pairwise coprime Frobenius312conjugates, and `G ∈ O[X]` maps to the conjugate product of `F`, then `G` has type313`scaleType δ σ` over `O`, where `δ = deg Φ`. -/314theorem descended_polynomial_type (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 7.1315    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]316    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) [IsDomain (AdjoinRoot Φ)]317    (F : Polynomial (AdjoinRoot Φ)) (σ : FactorType)318    (hσ : HasPolynomialTypeF (AdjoinRoot Φ)319      (F.map (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) σ)320    (hcop : ∀ i j : Fin Φ.natDegree, i ≠ j → IsCoprime321      ((fun i : Fin Φ.natDegree ↦ (F.map (frobeniusIter O Φ i).toRingHom).map322        (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) i)323      ((fun i : Fin Φ.natDegree ↦ (F.map (frobeniusIter O Φ i).toRingHom).map324        (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) j)) (G : Polynomial O)325    (hG : G.map (algebraMap O (AdjoinRoot Φ)) = conjugateProduct O Φ F) :326    HasPolynomialTypeF O (G.map (algebraMap O (BaseField O))) (scaleType Φ.natDegree σ) := by327  obtain ⟨gs, hgs, hd, hprod, hσeq, hfinδ⟩ := hσ328  obtain ⟨ι, hι, hinj, -, hfin⟩ := unramified_fraction_field_lift O Φ hΦ329  obtain ⟨τ, hτ, hτι, hτ0, hrec, hτδ, hfix⟩ := frobenius_fraction_extension O Φ hΦ ι hι330  obtain ⟨H, hHmi, hHinj, hHorb, hHdeg, hHprod⟩ := invariant_orbit_factors O Φ hΦ ι τ hτ hτι hτ0331    hrec hτδ hfix hinj F gs hgs hd hprod hcop332  have hcomp : ι.comp (algebraMap O (BaseField O)) =333      (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))).comp (algebraMap O (AdjoinRoot Φ)) :=334    RingHom.ext hι335  have hGprod : ∏ a, H a = G.map (algebraMap O (BaseField O)) := by336    apply Polynomial.map_injective ι hinj337    rw [hHprod, ← hG, Polynomial.map_map, Polynomial.map_map, hcomp]338  have hδpos : 0 < Φ.natDegree := Nat.pos_of_ne_zero fun h ↦ by339    have h2 := hΦ.2340    rw [eq_one_of_monic_natDegree_zero hΦ.1 h, residuePoly, Polynomial.map_one] at h2341    exact h2.not_isUnit isUnit_one342  have hinv : ∀ a, factorInvariant O (H a) =343      (fun z : ℕ × ℕ ↦ (z.1, Φ.natDegree * z.2)) (factorInvariant (AdjoinRoot Φ) (gs.get a)) ∧344      Module.Finite O (integralClosure O (AdjoinRoot (H a))) := by345    intro a346    have hga := hgs (gs.get a) (List.get_mem _ _)347    have hdiv : gs.get a ∣ (H a).map ι := by348      rw [hHorb a]349      conv_lhs => rw [← show (gs.get a).map (τ (⟨0, hδpos⟩ : Fin Φ.natDegree)).toRingHom =350        gs.get a by simp [hτ0]]351      exact Finset.dvd_prod_of_mem _ (Finset.mem_univ _)352    exact factor_invariant_unramified_scale O Φ hΦ ι hι (gs.get a) hga.1 hga.2 (H a)353      (hHmi a).1 (hHmi a).2 (root_field_algEquiv_conjugate_orbit O Φ ι hfin (gs.get a)354        hga.1 hga.2 (H a) (hHmi a).1 (hHmi a).2 hdiv (hHdeg a)) (hfinδ _ (List.get_mem _ _))355  refine ⟨List.ofFn H, fun g hg ↦ ?_, List.nodup_ofFn.mpr hHinj, by rw [List.prod_ofFn, hGprod],356    ?_, fun g hg ↦ ?_⟩357  · obtain ⟨a, rfl⟩ := List.mem_ofFn.mp hg358    exact hHmi a359  · rw [hσeq, List.map_ofFn]360    conv_lhs => rw [← List.ofFn_get gs]361    rw [List.map_ofFn, scaleType, Multiset.map_coe, List.map_ofFn]362    exact congrArg _ (congrArg _ (funext fun a ↦ (hinv a).1.symm))363  · obtain ⟨a, rfl⟩ := List.mem_ofFn.mp hg364    exact (hinv a).2365 366end SurfaceBlowup