Frobenius descent for unramified extensions

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.PolynomialTypes7 8/-!9# Frobenius descent for unramified extensions10 11Let `O` be a complete discrete valuation ring with finite residue field and let `Φ` be an12unramified lift (a monic polynomial over `O` with irreducible residue polynomial). This file13first computes the Haar mass of projective cells, then develops the ring `O_δ = O[X]/(Φ)`: it is a14complete discrete valuation ring, unramified over `O`, carrying a Frobenius automorphism of order15`δ = deg Φ` with fixed ring `O`. Finally it proves Frobenius descent for blocks: monic residue16cells of `residuePoly Φ ^ r` over `O` correspond bijectively, and congruence-preservingly, to block17cells over `O_δ`.18 19## Main results20 21* `SurfaceBlowup.projective_cell_mass`, `SurfaceBlowup.projective_cell_conditional_density`:22  the mass of a projective cell and its density inside the primitive locus.23* `SurfaceBlowup.unramified_is_dvr`: `O_δ` is a complete DVR with uniformizer any uniformizer of24  `O` and residue field of cardinality `q ^ δ`.25* `SurfaceBlowup.frobenius_pow_degree_eq_id`, `SurfaceBlowup.frobenius_fixed_ring`: the Frobenius26  has order dividing `δ` and its fixed points are exactly `O`.27* `SurfaceBlowup.block_descent_bijection`, `SurfaceBlowup.block_descent_congruence_iff`: the28  descent bijection between residue cells and block cells, and its compatibility with congruences.29 30Provenance: `Thm_SurfaceBlowupV2_{projective_cell_mass, projective_cell_mass_mul_normalizer,31projective_cell_conditional_density, unramified_base_invariants, inertiaDeg_unramified_tower,32ramificationIdx_unramified_tower, unramified_fraction_field_lift, unramified_free_module,33unramified_adic_complete, base_ideal_maximal_local, simple_root_derivative_unit,34frobenius_root_exists, frobenius_root_spec, frobenius_residue_action, frobenius_fixed_mod_pow,35frobenius_fixed_ring, root_unique_of_congruent, frobenius_pow_degree_eq_id, unramified_is_domain,36conjugate_product_invariant, descend_block_mem_cell, unramified_is_dvr, block_conjugates,37block_conjugates_coprime, block_splitting, block_descent_bijection, block_descent_congruence_iff}`.38-/39 40namespace SurfaceBlowup41 42open scoped BigOperators ENNReal43 44/-! ### Projective cells -/45 46/-- The projective cell of a nonzero residue vector `v` is measurable, of Haar mass47`(q - 1) * q⁻¹ ^ (n + 1)`. -/48theorem projective_cell_mass (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]49    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]50    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]51    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]52    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)53    (v : Fin (n + 1) → IsLocalRing.ResidueField O) (hv : v ≠ 0) :54    MeasurableSet (projectiveCell O n v) ∧55      coefficientMeasure O (n+1) (projectiveCell O n v) =56        ((Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) - 1) *57          (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (n+1) := by58  obtain ⟨hcard, hne, hfin⟩ := scalar_class_card (IsLocalRing.ResidueField O) n v hv59  set S := hfin.toFinset with hS60  have heq : projectiveCell O n v = ⋃ w ∈ S, {a : Fin (n+1) → O | residueVector O a = w} := by61    ext a62    simp only [projectiveCell, Set.mem_ofPred_eq, Set.mem_iUnion, hS, Set.Finite.mem_toFinset,63      exists_prop, exists_eq_right']64    exact ⟨fun h => h.2, fun h => ⟨(primitive_iff_residue_ne_zero O n a).2 (hne _ h), h⟩⟩65  have hmeas : ∀ w ∈ S, MeasurableSet {a : Fin (n+1) → O | residueVector O a = w} :=66    fun w _ => (residue_vector_fiber_mass O htop n w).167  refine ⟨heq ▸ Finset.measurableSet_biUnion S hmeas, ?_⟩68  rw [heq, MeasureTheory.measure_biUnion_finset _ hmeas]69  · simp only [fun w => (residue_vector_fiber_mass O htop n w).2]70    rw [Finset.sum_const, nsmul_eq_mul]71    congr 172    have : S.card = Nat.card (IsLocalRing.ResidueField O) - 1 := by73      rw [← hcard, hS, Nat.card_eq_card_finite_toFinset hfin]74    rw [this, ENNReal.natCast_sub]75    simp76  · exact fun w _ w' _ hww' => Set.disjoint_left.2 fun a h h' => hww' (h.symm.trans h')77 78/-- The mass of a projective cell times `∑_{i ≤ n} q ^ i` is the mass of the primitive locus. -/79private theorem projective_cell_mass_mul_normalizer (O : Type) [CommRing O] [IsDomain O]80    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]81    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]82    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]83    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)84    (v : Fin (n + 1) → IsLocalRing.ResidueField O) (hv : v ≠ 0) :85    coefficientMeasure O (n+1) (projectiveCell O n v) *86        (∑ i ∈ Finset.range (n+1), (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) ^ i) =87      coefficientMeasure O (n+1) {a : Fin (n+1) → O | primitive O a} := by88  rw [(projective_cell_mass O htop n v hv).2, primitive_locus_mass O htop n]89  set q := Nat.card (IsLocalRing.ResidueField O)90  have hq : 1 < q := Finite.one_lt_card91  have hN : (q - 1) * ∑ i ∈ Finset.range (n+1), q ^ i = q ^ (n+1) - 1 := by92    have h1 : 1 ≤ q ^ (n+1) := Nat.one_le_pow _ _ (by omega)93    zify [hq.le, h1]94    rw [mul_comm]; exact_mod_cast geom_sum_mul (q : ℤ) (n+1)95  have hE : ((q : ℝ≥0∞) - 1) * ∑ i ∈ Finset.range (n+1), (q : ℝ≥0∞) ^ i96      = (q : ℝ≥0∞) ^ (n+1) - 1 := by97    have := congrArg (fun m : ℕ => (m : ℝ≥0∞)) hN98    simp only [Nat.cast_mul, Nat.cast_sum, Nat.cast_pow] at this99    rw [ENNReal.natCast_sub, ENNReal.natCast_sub] at this100    simpa [Nat.cast_pow] using this101  have hq0 : (q : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : q ≠ 0)102  have hqt : (q : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top q103  calc ((q : ℝ≥0∞) - 1) * (q : ℝ≥0∞)⁻¹ ^ (n+1) * ∑ i ∈ Finset.range (n+1), (q : ℝ≥0∞) ^ i104      = (((q : ℝ≥0∞) - 1) * ∑ i ∈ Finset.range (n+1), (q : ℝ≥0∞) ^ i) *105          (q : ℝ≥0∞)⁻¹ ^ (n+1) := by ring106    _ = ((q : ℝ≥0∞) ^ (n+1) - 1) * (q : ℝ≥0∞)⁻¹ ^ (n+1) := by rw [hE]107    _ = 1 - (q : ℝ≥0∞)⁻¹ ^ (n+1) := by108      rw [ENNReal.sub_mul (fun _ _ => ENNReal.pow_ne_top (ENNReal.inv_ne_top.2 hq0)),109        ← mul_pow, ENNReal.mul_inv_cancel hq0 hqt, one_pow, one_mul]110 111/-- The conditional density of a projective cell inside the primitive locus is the value of112`1 / projectiveNormalizer n` at `q`. -/113theorem projective_cell_conditional_density (O : Type) [CommRing O] [IsDomain O]Lemma 7.1114    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]115    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]116    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]117    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)118    (v : Fin (n + 1) → IsLocalRing.ResidueField O) (hv : v ≠ 0) :119    coefficientMeasure O (n+1) (projectiveCell O n v) /120        coefficientMeasure O (n+1) {a : Fin (n+1) → O | primitive O a} =121      densityValue (Expr.inv (projectiveNormalizer n)) (Nat.card (IsLocalRing.ResidueField O)) := by122  have hmul := projective_cell_mass_mul_normalizer O htop n v hv123  have hP := primitive_locus_mass O htop n124  have hev := (projective_normalizer_eval (Nat.card (IsLocalRing.ResidueField O) : ℚ) n).1125  set q := Nat.card (IsLocalRing.ResidueField O)126  have hq1 : 1 < q := Finite.one_lt_card127  set C := coefficientMeasure O (n+1) (projectiveCell O n v)128  set P := coefficientMeasure O (n+1) {a : Fin (n+1) → O | primitive O a}129  set D : ℝ≥0∞ := ∑ i ∈ Finset.range (n+1), (q : ℝ≥0∞) ^ i with hD130  have hD0 : D ≠ 0 := by131    intro h132    rw [hD, Finset.sum_eq_zero_iff] at h133    simpa using h 0 (by simp)134  have hDtop : D ≠ ⊤ :=135    ENNReal.sum_ne_top.2 (fun i _ => ENNReal.pow_ne_top (ENNReal.natCast_ne_top _))136  have hPtop : P ≠ ⊤ := by rw [hP]; exact ne_top_of_le_ne_top ENNReal.one_ne_top tsub_le_self137  have hP0 : P ≠ 0 := by138    rw [hP]139    apply ne_of_gt140    rw [tsub_pos_iff_lt]141    apply pow_lt_one₀ (zero_le) _ (Nat.succ_ne_zero _)142    rw [ENNReal.inv_lt_one]143    exact_mod_cast hq1144  have hC0 : C ≠ 0 := by rintro h; rw [h, zero_mul] at hmul; exact hP0 hmul.symm145  have hCtop : C ≠ ⊤ := by146    rintro h; rw [h, ENNReal.top_mul hD0] at hmul; exact hPtop hmul.symm147  have lhs : C / P = D⁻¹ := by148    rw [← hmul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv (Or.inl hC0) (Or.inl hCtop), mul_comm C⁻¹,149      mul_assoc, ENNReal.inv_mul_cancel hC0 hCtop, mul_one]150  rw [lhs, densityValue]151  change D⁻¹ = ENNReal.ofReal (((projectiveNormalizer n).eval (q : ℚ))⁻¹ : ℚ)152  rw [hev]153  have hpos : (0 : ℝ) < ((∑ i ∈ Finset.range (n+1), (q : ℚ) ^ i : ℚ) : ℝ) := by154    push_cast155    exact Finset.sum_pos (fun i _ => by positivity) ⟨0, by simp⟩156  rw [Rat.cast_inv, ENNReal.ofReal_inv_of_pos hpos]157  congr 1158  rw [hD]; push_cast159  rw [ENNReal.ofReal_sum_of_nonneg (fun i _ => by positivity)]160  exact Finset.sum_congr rfl fun i _ => by rw [ENNReal.ofReal_pow (by positivity),161    ENNReal.ofReal_natCast]162 163/-! ### Unramified extensions of discrete valuation rings -/164 165/-- A finite free extension of DVRs of rank `δ` in which a uniformizer stays irreducible has166ramification index `1` and inertia degree `δ`. -/167private theorem unramified_base_invariants (O Oδ : Type) [CommRing O] [IsDomain O]168    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]169    [Algebra O Oδ] [Module.Finite O Oδ] [Module.Free O Oδ] (δ : ℕ)170    (hrank : Module.finrank O Oδ = δ) (pi : O) (hpi : Irreducible pi)171    (hpiδ : Irreducible (algebraMap O Oδ pi)) :172    (IsLocalRing.maximalIdeal Oδ).ramificationIdx O = 1 ∧173      (IsLocalRing.maximalIdeal Oδ).inertiaDeg O = δ := by174  have hinj : Function.Injective (algebraMap O Oδ) := by175    rw [injective_iff_map_eq_zero]176    intro x hx177    by_contra hx0178    obtain ⟨k, u, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx0 hpi179    rw [map_mul, map_pow] at hx180    rcases mul_eq_zero.mp hx with h | h181    · exact (Units.map (algebraMap O Oδ : O →* Oδ) u).ne_zero h182    · exact hpiδ.ne_zero (pow_eq_zero_iff'.mp h).1183  have : Algebra.IsIntegral O Oδ := Algebra.IsIntegral.of_finite O Oδ184  have h512 := dvr_extension_maximalIdeal_map_eq_pow O Oδ hinj185  have h1 : (IsLocalRing.maximalIdeal O).map (algebraMap O Oδ) =186      (IsLocalRing.maximalIdeal Oδ) ^ 1 := by187    rw [pow_one, hpi.maximalIdeal_eq, Ideal.map_span, Set.image_singleton,188      ← hpiδ.maximalIdeal_eq]189  have he : (IsLocalRing.maximalIdeal Oδ).ramificationIdx O = 1 :=190    dvr_maximalIdeal_pow_injective Oδ _ _ (h512.symm.trans h1)191  have : Module.Flat O Oδ := Module.Flat.of_free192  have h251 := finite_flat_local_ramification_degree O Oδ193  rw [he, hrank, one_mul] at h251194  exact ⟨he, h251⟩195 196/-- In a tower `O → O_δ → B` with `O_δ` unramified of rank `δ` over `O`, inertia degrees over `O`197are `δ` times inertia degrees over `O_δ`. -/198theorem inertiaDeg_unramified_tower (O Oδ B : Type) [CommRing O] [IsDomain O]199    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]200    [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra O Oδ] [Algebra O B]201    [Algebra Oδ B] [IsScalarTower O Oδ B] [Module.Finite O Oδ] [Module.Free O Oδ]202    [Module.Finite Oδ B] (δ : ℕ) (hrank : Module.finrank O Oδ = δ) (pi : O)203    (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi)) :204    (IsLocalRing.maximalIdeal B).inertiaDeg O =205      δ * (IsLocalRing.maximalIdeal B).inertiaDeg Oδ := by206  have : Algebra.IsIntegral Oδ B := Algebra.IsIntegral.of_finite Oδ B207  have : (IsLocalRing.maximalIdeal B).LiesOver (IsLocalRing.maximalIdeal Oδ) :=208    ⟨(integral_local_extension_unique_prime Oδ B).1.symm⟩209  rw [Ideal.inertiaDeg_tower (R := O) (S := Oδ) (IsLocalRing.maximalIdeal Oδ)210    (IsLocalRing.maximalIdeal B), (unramified_base_invariants O Oδ δ hrank pi hpi hpiδ).2]211 212/-- In a tower `O → O_δ → B` with `O_δ` unramified over `O`, ramification indices over `O` and213over `O_δ` agree. -/214theorem ramificationIdx_unramified_tower (O Oδ B : Type) [CommRing O] [IsDomain O]215    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]216    [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra O Oδ] [Algebra O B]217    [Algebra Oδ B] [IsScalarTower O Oδ B] [Module.Finite O Oδ] [Module.Free O Oδ]218    [Module.Finite Oδ B] (δ : ℕ) (hrank : Module.finrank O Oδ = δ) (pi : O)219    (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi)) [Module.Free Oδ B] :220    (IsLocalRing.maximalIdeal B).ramificationIdx O =221      (IsLocalRing.maximalIdeal B).ramificationIdx Oδ := by222  have : Algebra.IsIntegral Oδ B := Algebra.IsIntegral.of_finite Oδ B223  have : (IsLocalRing.maximalIdeal B).LiesOver (IsLocalRing.maximalIdeal Oδ) :=224    ⟨(integral_local_extension_unique_prime Oδ B).1.symm⟩225  rw [Ideal.ramificationIdx_tower (R := O) (S := Oδ) (T := B) (IsLocalRing.maximalIdeal Oδ)226    (IsLocalRing.maximalIdeal B), (unramified_base_invariants O Oδ δ hrank pi hpi hpiδ).1,227    one_mul]228 229/-- For an unramified lift `Φ` with `O[X]/(Φ)` a domain, there is a unique ring map of fraction230fields extending `O → O[X]/(Φ)`; it is injective and makes the target a field extension of degree231`deg Φ`. -/232theorem unramified_fraction_field_lift (O : Type) [CommRing O] [IsDomain O]233    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]234    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)235    [IsDomain (AdjoinRoot Φ)] :236    ∃ ι : BaseField O →+* BaseField (AdjoinRoot Φ),237      (∀ c : O, ι (algebraMap O (BaseField O) c) =238        algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) (algebraMap O (AdjoinRoot Φ) c)) ∧239      Function.Injective ι ∧240      (∀ ι' : BaseField O →+* BaseField (AdjoinRoot Φ),241        (∀ c : O, ι' (algebraMap O (BaseField O) c) =242          algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) (algebraMap O (AdjoinRoot Φ) c)) →243        ι' = ι) ∧244      (letI := ι.toAlgebra; Module.Finite (BaseField O) (BaseField (AdjoinRoot Φ)) ∧245        Module.finrank (BaseField O) (BaseField (AdjoinRoot Φ)) = Φ.natDegree) := by246  have hmon : Φ.Monic := hΦ.1247  let pb := AdjoinRoot.powerBasis' hmon248  have : Module.Free O (AdjoinRoot Φ) := Module.Free.of_basis pb.basis249  have : Module.Finite O (AdjoinRoot Φ) := pb.finite250  let j : O →+* BaseField (AdjoinRoot Φ) :=251    (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))).comp (algebraMap O (AdjoinRoot Φ))252  have hj : Function.Injective j :=253    (IsFractionRing.injective (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))).comp254      (FaithfulSMul.algebraMap_injective O (AdjoinRoot Φ))255  refine ⟨IsFractionRing.lift hj, fun c => IsFractionRing.lift_algebraMap hj c,256    RingHom.injective (IsFractionRing.lift hj : BaseField O →+* BaseField (AdjoinRoot Φ)),257    fun ι' h => ?_, ?_⟩258  · exact IsFractionRing.ringHom_ext (A := O) (K := BaseField O) fun c => by259      rw [h, IsFractionRing.lift_algebraMap hj c]; rfl260  · let _ : Algebra (BaseField O) (BaseField (AdjoinRoot Φ)) := (IsFractionRing.lift hj).toAlgebra261    have : IsScalarTower O (BaseField O) (BaseField (AdjoinRoot Φ)) :=262      IsScalarTower.of_algebraMap_eq fun c => by263        change _ = IsFractionRing.lift hj _264        rw [IsFractionRing.lift_algebraMap hj c]265        exact IsScalarTower.algebraMap_apply O (AdjoinRoot Φ) _ c266    have hrank : Module.finrank (BaseField O) (BaseField (AdjoinRoot Φ)) = Φ.natDegree := by267      rw [IsFractionRing.finrank_eq O (BaseField O) (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)),268        pb.finrank]269      exact AdjoinRoot.powerBasis'_dim hmon270    refine ⟨?_, hrank⟩271    apply Module.finite_of_finrank_pos272    rw [hrank, ← hmon.natDegree_map (IsLocalRing.residue O)]273    exact Irreducible.natDegree_pos hΦ.2274 275/-- For monic `Φ`, `O[X]/(Φ)` is a free `O`-module of finite rank `deg Φ`. -/276theorem unramified_free_module (O : Type) [CommRing O] [Nontrivial O] (Φ : Polynomial O)277    (hΦ : Φ.Monic) :278    Module.Free O (AdjoinRoot Φ) ∧ Module.Finite O (AdjoinRoot Φ) ∧279      Module.finrank O (AdjoinRoot Φ) = Φ.natDegree :=280  ⟨hΦ.free_adjoinRoot, hΦ.finite_adjoinRoot, by simp [(AdjoinRoot.powerBasis' hΦ).finrank]⟩281 282/-- For monic `Φ` over a complete local ring, `O[X]/(Φ)` is complete and separated for the283extended ideal `𝔪 O[X]/(Φ)`, and regular elements of `O` stay regular in it. -/284private theorem unramified_adic_complete (O : Type) [CommRing O] [IsLocalRing O]285    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (Φ : Polynomial O) (hΦ : Φ.Monic) :286    IsAdicComplete (baseIdeal O Φ) (AdjoinRoot Φ) ∧287      (∀ x : AdjoinRoot Φ, (∀ L, x ∈ (baseIdeal O Φ)^L) → x = 0) ∧288      (∀ c : O, (∀ y : O, c * y = 0 → y = 0) →289        ∀ x : AdjoinRoot Φ, algebraMap O (AdjoinRoot Φ) c * x = 0 → x = 0) := by290  obtain ⟨hfree, hfin, -⟩ := unramified_free_module O Φ hΦ291  refine ⟨?_, ?_, ?_⟩292  · exact (IsAdicComplete.map_algebraMap_iff (S := AdjoinRoot Φ) (M := AdjoinRoot Φ)293      (I := IsLocalRing.maximalIdeal O)).2 (finite_free_adic_complete O (AdjoinRoot Φ) _)294  · intro x hx295    apply (AdjoinRoot.powerBasis' hΦ).basis.repr.injective296    ext i297    simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]298    have hi : ∀ L, (AdjoinRoot.powerBasis' hΦ).basis.repr x i ∈ (IsLocalRing.maximalIdeal O)^L :=299      fun L => (base_ideal_coordinates O Φ hΦ L x).1 (hx L) i300    apply IsHausdorff.haus (IsAdicComplete.toIsHausdorff (I := IsLocalRing.maximalIdeal O))301    intro n302    simpa [SModEq.zero, smul_eq_mul, Ideal.mul_top] using hi n303  · intro c hc x hx304    rw [← Algebra.smul_def] at hx305    apply (AdjoinRoot.powerBasis' hΦ).basis.repr.injective306    ext i307    have := congrArg (fun y => (AdjoinRoot.powerBasis' hΦ).basis.repr y i) hx308    simp only [map_smul, Finsupp.smul_apply, smul_eq_mul, map_zero, Finsupp.coe_zero,309      Pi.zero_apply] at this ⊢310    exact hc _ this311 312/-- For an unramified lift `Φ`, the extended ideal `𝔪 O[X]/(Φ)` is maximal, units can be detected313modulo it, and `O[X]/(Φ)` is local with that maximal ideal. -/314theorem base_ideal_maximal_local (O : Type) [CommRing O] [IsLocalRing O]315    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]316    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :317    (baseIdeal O Φ).IsMaximal ∧ (∀ x : AdjoinRoot Φ, IsUnit (baseReduce O Φ x) → IsUnit x) ∧318      ∃ _ : IsLocalRing (AdjoinRoot Φ),319        IsLocalRing.maximalIdeal (AdjoinRoot Φ) = baseIdeal O Φ := by320  have hF := (residue_extension_field O Φ hΦ).1321  have hmax : (baseIdeal O Φ).IsMaximal := Ideal.Quotient.maximal_of_isField _ hF322  have hC := (unramified_adic_complete O Φ hΦ.1).1323  have hloc : IsLocalHom (baseReduce O Φ) :=324    isLocalHom_of_le_jacobson_bot _ (IsAdicComplete.le_jacobson_bot _)325  have hunit : ∀ x : AdjoinRoot Φ, IsUnit (baseReduce O Φ x) → IsUnit x :=326    fun x hx => IsUnit.of_map (baseReduce O Φ) x hx327  let _ : Field (residueExtension O Φ) := hF.toField328  have : Nontrivial (AdjoinRoot Φ) := by329    by_contra h330    rw [not_nontrivial_iff_subsingleton] at h331    exact hmax.ne_top (Subsingleton.elim _ _)332  have : IsLocalRing (AdjoinRoot Φ) := by333    refine IsLocalRing.of_isUnit_or_isUnit_one_sub_self fun a => ?_334    by_cases ha : baseReduce O Φ a = 0335    · right; apply hunit; simp [map_sub, ha]336    · left; exact hunit a (Ne.isUnit ha)337  exact ⟨hmax, hunit, inferInstance, (IsLocalRing.eq_maximalIdeal hmax).symm⟩338 339/-- An approximate root of `Φ` in `O[X]/(Φ)` (a root modulo `𝔪`) is a simple root: the derivative340of `Φ` there is a unit, already modulo `𝔪`. -/341theorem simple_root_derivative_unit (O : Type) [CommRing O] [IsLocalRing O]342    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]343    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (a : AdjoinRoot Φ)344    (ha : baseReduce O Φ ((Φ.map (AdjoinRoot.of Φ)).eval a) = 0) :345    IsUnit (baseReduce O Φ ((Φ.map (AdjoinRoot.of Φ)).derivative.eval a)) ∧346      IsUnit ((Φ.map (AdjoinRoot.of Φ)).derivative.eval a) := by347  have hle : IsLocalRing.maximalIdeal O ≤ (baseIdeal O Φ).comap (AdjoinRoot.of Φ) :=348    Ideal.map_le_iff_le_comap.1 le_rfl349  let ρ : IsLocalRing.ResidueField O →+* residueExtension O Φ :=350    Ideal.quotientMap (baseIdeal O Φ) (AdjoinRoot.of Φ) hle351  have hcomp : (baseReduce O Φ).comp (AdjoinRoot.of Φ) = ρ.comp (IsLocalRing.residue O) :=352    (Ideal.quotientMap_comp_mk hle).symm353  have key : ∀ p : Polynomial O, baseReduce O Φ ((p.map (AdjoinRoot.of Φ)).eval a)354      = (p.map (IsLocalRing.residue O)).eval₂ ρ (baseReduce O Φ a) := fun p => by355    rw [Polynomial.eval_map, Polynomial.hom_eval₂, Polynomial.eval₂_map, hcomp]356  let _ : Field (residueExtension O Φ) := (residue_extension_field O Φ hΦ).1.toField357  have hsep : (residuePoly O Φ).Separable := PerfectField.separable_of_irreducible hΦ.2358  have h1 : IsUnit (baseReduce O Φ ((Φ.map (AdjoinRoot.of Φ)).derivative.eval a)) := by359    rw [Polynomial.derivative_map, key, ← Polynomial.derivative_map]360    rw [key] at ha361    exact isUnit_iff_ne_zero.mpr (hsep.eval₂_derivative_ne_zero ρ ha)362  exact ⟨h1, (base_ideal_maximal_local O Φ hΦ).2.1 _ h1⟩363 364/-! ### The Frobenius automorphism -/365 366/-- Hensel's lemma produces a root of `Φ` in `O[X]/(Φ)` congruent to `X ^ q` modulo `𝔪`. -/367private theorem frobenius_root_exists (O : Type) [CommRing O] [IsLocalRing O]368    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]369    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :370    ∃ a : AdjoinRoot Φ, (Φ.map (AdjoinRoot.of Φ)).IsRoot a ∧371      a - (AdjoinRoot.root Φ) ^ residueCard O ∈ baseIdeal O Φ := by372  have : IsAdicComplete (baseIdeal O Φ) (AdjoinRoot Φ) := (unramified_adic_complete O Φ hΦ.1).1373  have : HenselianRing (AdjoinRoot Φ) (baseIdeal O Φ) := IsAdicComplete.henselianRing _ _374  have hker : ∀ c ∈ IsLocalRing.maximalIdeal O,375      ((baseReduce O Φ).comp (AdjoinRoot.of Φ)) c = 0 := fun c hc => by376    simp only [RingHom.comp_apply, baseReduce, Ideal.Quotient.eq_zero_iff_mem]377    exact Ideal.mem_map_of_mem _ hc378  let ρ : IsLocalRing.ResidueField O →+* residueExtension O Φ :=379    Ideal.Quotient.lift _ ((baseReduce O Φ).comp (AdjoinRoot.of Φ)) hker380  have key : ∀ x : AdjoinRoot Φ, baseReduce O Φ ((Φ.map (AdjoinRoot.of Φ)).eval x)381      = (residuePoly O Φ).eval₂ ρ (baseReduce O Φ x) := fun x => by382    rw [Polynomial.eval_map, Polynomial.hom_eval₂, residuePoly, Polynomial.eval₂_map]383    congr 1384  have h0 : baseReduce O Φ385      ((Φ.map (AdjoinRoot.of Φ)).eval (AdjoinRoot.root Φ ^ residueCard O)) = 0 := by386    rw [key, map_pow, residueCard, eval_at_pow_card (IsLocalRing.ResidueField O) _ ρ387      (residuePoly O Φ) (baseReduce O Φ (AdjoinRoot.root Φ)), ← key,388      show (Φ.map (AdjoinRoot.of Φ)).eval (AdjoinRoot.root Φ) = 0 from AdjoinRoot.isRoot_root Φ,389      map_zero, zero_pow Nat.card_pos.ne']390  exact HenselianRing.is_henselian (Φ.map (AdjoinRoot.of Φ)) (hΦ.1.map _)391    (AdjoinRoot.root Φ ^ residueCard O) (Ideal.Quotient.eq_zero_iff_mem.mp h0)392    (simple_root_derivative_unit O Φ hΦ _ h0).1393 394/-- The Frobenius root is a root of `Φ` congruent to `X ^ q`, and the Frobenius is the395`O`-algebra endomorphism sending `X` to it. -/396private theorem frobenius_root_spec (O : Type) [CommRing O] [IsLocalRing O]397    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]398    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :399    (Φ.map (AdjoinRoot.of Φ)).IsRoot (frobeniusRoot O Φ) ∧400      frobeniusRoot O Φ - (AdjoinRoot.root Φ) ^ residueCard O ∈ baseIdeal O Φ ∧401      unramifiedFrobenius O Φ (AdjoinRoot.root Φ) = frobeniusRoot O Φ ∧402      ∀ c : O, unramifiedFrobenius O Φ (algebraMap O (AdjoinRoot Φ) c) =403        algebraMap O (AdjoinRoot Φ) c := by404  have h := frobenius_root_exists O Φ hΦ405  have hr : frobeniusRoot O Φ = Classical.choose h := dif_pos h406  exact ⟨hr ▸ (Classical.choose_spec h).1, hr ▸ (Classical.choose_spec h).2,407    AdjoinRoot.liftAlgHom_root _ _ _ _, (unramifiedFrobenius O Φ).commutes⟩408 409/-- Modulo `𝔪`, the Frobenius acts as `x ↦ x ^ q`, and its `i`-th iterate as `x ↦ x ^ (q ^ i)`. -/410private theorem frobenius_residue_action (O : Type) [CommRing O] [IsLocalRing O]411    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]412    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :413    (∀ x : AdjoinRoot Φ,414      baseReduce O Φ (unramifiedFrobenius O Φ x) = (baseReduce O Φ x) ^ residueCard O) ∧415    (∀ (i : ℕ) (x : AdjoinRoot Φ),416      baseReduce O Φ (frobeniusIter O Φ i x) = (baseReduce O Φ x) ^ (residueCard O ^ i)) := by417  obtain ⟨-, hcong, hroot, -⟩ := frobenius_root_spec O Φ hΦ418  have hle : IsLocalRing.maximalIdeal O ≤419      RingHom.ker ((baseReduce O Φ).comp (AdjoinRoot.of Φ)) := fun c hc => by420    rw [RingHom.mem_ker, RingHom.comp_apply, baseReduce, Ideal.Quotient.eq_zero_iff_mem]421    exact Ideal.mem_map_of_mem _ hc422  let ρ : IsLocalRing.ResidueField O →+* residueExtension O Φ :=423    Ideal.Quotient.lift _ ((baseReduce O Φ).comp (AdjoinRoot.of Φ)) hle424  have hρ : ρ.comp (IsLocalRing.residue O) = (baseReduce O Φ).comp (AdjoinRoot.of Φ) := by425    ext c; rfl426  have key : ∀ (p : Polynomial O) (a : AdjoinRoot Φ),427      baseReduce O Φ (Polynomial.aeval a p) =428        (p.map (IsLocalRing.residue O)).eval₂ ρ (baseReduce O Φ a) := fun p a => by429    rw [Polynomial.eval₂_map, hρ, Polynomial.aeval_def, Polynomial.hom_eval₂]430    rfl431  have h1 : ∀ x : AdjoinRoot Φ, baseReduce O Φ (unramifiedFrobenius O Φ x) =432      (baseReduce O Φ x) ^ residueCard O := by433    intro x434    obtain ⟨p, rfl⟩ := AdjoinRoot.mk_surjective x435    rw [← AdjoinRoot.aeval_eq, ← Polynomial.aeval_algHom_apply, hroot, key, key]436    have : baseReduce O Φ (frobeniusRoot O Φ) =437        (baseReduce O Φ (AdjoinRoot.root Φ)) ^ residueCard O := by438      rw [← map_pow, baseReduce, Ideal.Quotient.eq]; exact hcong439    rw [this]440    exact eval_at_pow_card _ _ ρ _ _441  refine ⟨h1, fun i => ?_⟩442  induction i with443  | zero => intro x; simp [frobeniusIter]444  | succ i ih =>445    intro x446    change baseReduce O Φ (unramifiedFrobenius O Φ (frobeniusIter O Φ i x)) = _447    rw [h1, ih, ← pow_mul, pow_succ]448 449private theorem natDegree_pos_of_isUnramifiedLift {O : Type} [CommRing O] [IsLocalRing O]450    {Φ : Polynomial O} (hΦ : IsUnramifiedLift O Φ) : 0 < Φ.natDegree := by451  have := hΦ.2.natDegree_pos452  rwa [residuePoly, hΦ.1.natDegree_map] at this453 454/-- An element of `O[X]/(Φ)` fixed by the Frobenius modulo `𝔪 ^ L` is congruent to an element of455`O` modulo `𝔪 ^ L`. -/456private theorem frobenius_fixed_mod_pow (O : Type) [CommRing O] [IsDomain O]457    [IsDiscreteValuationRing O]458    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]459    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (L : ℕ) (a : AdjoinRoot Φ)460    (ha : unramifiedFrobenius O Φ a - a ∈ (baseIdeal O Φ) ^ L) :461    ∃ c : O, a - algebraMap O (AdjoinRoot Φ) c ∈ (baseIdeal O Φ)^L := by462  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible O463  set σ := unramifiedFrobenius O Φ464  have hpow : ∀ j : ℕ, (baseIdeal O Φ) ^ j = Ideal.span {algebraMap O (AdjoinRoot Φ) ϖ ^ j} :=465    fun j => by466      rw [baseIdeal, hϖ.maximalIdeal_eq, Ideal.map_span, Set.image_singleton,467        Ideal.span_singleton_pow]468      rfl469  have hmem1 : ∀ x, x ∈ baseIdeal O Φ ↔ ∃ e, x = e * algebraMap O (AdjoinRoot Φ) ϖ := fun x => by470    rw [← pow_one (baseIdeal O Φ), hpow, pow_one, Ideal.mem_span_singleton']471    exact ⟨fun ⟨e, he⟩ => ⟨e, he.symm⟩, fun ⟨e, he⟩ => ⟨e, he.symm⟩⟩472  have htf := (unramified_adic_complete O Φ hΦ.1).2.2473  obtain ⟨hfield, -, -⟩ := residue_extension_field O Φ hΦ474  let _ : Field (residueExtension O Φ) := hfield.toField475  have hres := (frobenius_residue_action O Φ hΦ).1476  let ρ : IsLocalRing.ResidueField O →+* residueExtension O Φ :=477    Ideal.quotientMap (baseIdeal O Φ) (AdjoinRoot.of Φ) Ideal.le_comap_map478  induction L generalizing a with479  | zero => exact ⟨0, by simp⟩480  | succ L ih =>481    obtain ⟨c, hc⟩ := ih a (Ideal.pow_le_pow_right (Nat.le_succ L) ha)482    rw [hpow, Ideal.mem_span_singleton'] at hc ha483    obtain ⟨b, hb⟩ := hc484    obtain ⟨d, hd⟩ := ha485    have ha' : a = algebraMap O (AdjoinRoot Φ) c + b * algebraMap O (AdjoinRoot Φ) ϖ ^ L := by486      rw [hb]; ring487    have hσa : σ a - a = algebraMap O (AdjoinRoot Φ) (ϖ ^ L) * (σ b - b) := by488      rw [ha', map_add, map_mul, map_pow, AlgHom.commutes, AlgHom.commutes, map_pow]; ring489    have hkey : σ b - b = algebraMap O (AdjoinRoot Φ) ϖ * d := by490      have h0 : algebraMap O (AdjoinRoot Φ) (ϖ ^ L) *491          (σ b - b - algebraMap O (AdjoinRoot Φ) ϖ * d) = 0 := by492        rw [mul_sub, ← hσa, ← hd, map_pow]; ring493      exact sub_eq_zero.1 (htf _ (fun y hy => (mul_eq_zero.1 hy).resolve_left494        (pow_ne_zero _ hϖ.ne_zero)) _ h0)495    have hfix : (baseReduce O Φ b) ^ Nat.card (IsLocalRing.ResidueField O) = baseReduce O Φ b := by496      rw [← hres b]497      exact Ideal.Quotient.eq.2 ((hmem1 _).2 ⟨d, by rw [hkey, mul_comm]⟩)498    obtain ⟨r, hr⟩ := (finite_field_frobenius_fixed_points _ _ ρ _).1 hfix499    obtain ⟨c', rfl⟩ := IsLocalRing.residue_surjective r500    have hbc : b - algebraMap O (AdjoinRoot Φ) c' ∈ baseIdeal O Φ := by501      apply Ideal.Quotient.eq.1502      rw [← hr]; rfl503    obtain ⟨e, he⟩ := (hmem1 _).1 hbc504    refine ⟨c + ϖ ^ L * c', ?_⟩505    rw [hpow, Ideal.mem_span_singleton']506    refine ⟨e, ?_⟩507    rw [ha', show b = algebraMap O (AdjoinRoot Φ) c' + e * algebraMap O (AdjoinRoot Φ) ϖ by508      rw [← he]; ring, map_add, map_mul, map_pow]509    ring510 511/-- The elements of `O[X]/(Φ)` fixed by the Frobenius are exactly the elements of `O`. -/512theorem frobenius_fixed_ring (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Standard facts513    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]514    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (a : AdjoinRoot Φ)515    (ha : unramifiedFrobenius O Φ a = a) :516    ∃ c : O, algebraMap O (AdjoinRoot Φ) c = a := by517  have hc : ∀ L : ℕ, ∃ c : O, a - algebraMap O (AdjoinRoot Φ) c ∈ (baseIdeal O Φ)^L :=518    fun L => frobenius_fixed_mod_pow O Φ hΦ L a (by rw [ha, sub_self]; exact Submodule.zero_mem _)519  choose c hc using hc520  set m := IsLocalRing.maximalIdeal O521  have hpure := base_ideal_pure O Φ hΦ.1 (natDegree_pos_of_isUnramifiedLift hΦ)522  have hcompat : ∀ {L L' : ℕ}, L ≤ L' → c L ≡ c L' [SMOD (m ^ L • ⊤ : Submodule O O)] := by523    intro L L' hLL'524    rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← hpure]525    have : algebraMap O (AdjoinRoot Φ) (c L - c L') =526        (a - algebraMap O (AdjoinRoot Φ) (c L')) - (a - algebraMap O (AdjoinRoot Φ) (c L)) := by527      rw [map_sub]; ring528    rw [this]; exact Ideal.sub_mem _ (Ideal.pow_le_pow_right hLL' (hc L')) (hc L)529  obtain ⟨c0, hc0⟩ := IsPrecomplete.prec (I := m) inferInstance hcompat530  refine ⟨c0, ?_⟩531  rw [← sub_eq_zero, ← neg_sub, neg_eq_zero]532  refine (unramified_adic_complete O Φ hΦ.1).2.1 _ fun L => ?_533  have h3 : c L - c0 ∈ m ^ L := by534    simpa only [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top] using hc0 L535  rw [← hpure] at h3536  have : a - algebraMap O (AdjoinRoot Φ) c0 =537      (a - algebraMap O (AdjoinRoot Φ) (c L)) + algebraMap O (AdjoinRoot Φ) (c L - c0) := by538    rw [map_sub]; ring539  rw [this]; exact Ideal.add_mem _ (hc L) h3540 541/-- Two roots of `Φ` in `O[X]/(Φ)` that are congruent modulo `𝔪` are equal. -/542private theorem root_unique_of_congruent (O : Type) [CommRing O] [IsLocalRing O]543    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]544    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (a b : AdjoinRoot Φ)545    (ha : (Φ.map (AdjoinRoot.of Φ)).IsRoot a) (hb : (Φ.map (AdjoinRoot.of Φ)).IsRoot b)546    (hab : a - b ∈ baseIdeal O Φ) :547    a = b := by548  set Φ' := Φ.map (AdjoinRoot.of Φ)549  set d := b - a with hd550  have hdI : d ∈ baseIdeal O Φ := by simpa [hd] using (baseIdeal O Φ).neg_mem hab551  obtain ⟨k, hk⟩ := Polynomial.binomExpansion Φ' a d552  rw [show a + d = b by simp [hd]] at hk553  have h0 : d * (Φ'.derivative.eval a + k * d) = 0 := by554    rw [show Φ'.eval b = 0 from hb, show Φ'.eval a = 0 from ha] at hk555    linear_combination -hk556  obtain ⟨v, hv⟩ := (simple_root_derivative_unit O Φ hΦ a (by557    change baseReduce O Φ (Φ'.eval a) = 0558    rw [show Φ'.eval a = 0 from ha, map_zero])).2559  have hC := (unramified_adic_complete O Φ hΦ.1).1560  have hJ : baseIdeal O Φ ≤ Ideal.jacobson ⊥ := IsAdicComplete.le_jacobson_bot _561  have hkd : (↑v⁻¹ : AdjoinRoot Φ) * (k * d) ∈ baseIdeal O Φ :=562    (baseIdeal O Φ).mul_mem_left _ ((baseIdeal O Φ).mul_mem_left _ hdI)563  have h1 : IsUnit ((↑v⁻¹ : AdjoinRoot Φ) * (k * d) + 1) := by564    simpa using Ideal.mem_jacobson_bot.mp (hJ hkd) 1565  have h2 : IsUnit (Φ'.derivative.eval a + k * d) := by566    have : Φ'.derivative.eval a + k * d = v * ((↑v⁻¹ : AdjoinRoot Φ) * (k * d) + 1) := by567      rw [← hv, mul_add, ← mul_assoc, Units.mul_inv, one_mul, mul_one, add_comm]568    rw [this]; exact v.isUnit.mul h1569  have : d = 0 := h2.mul_right_cancel (by rw [h0, zero_mul])570  exact (sub_eq_zero.mp this).symm571 572/-- The `deg Φ`-th iterate of the Frobenius is the identity; in particular the Frobenius is573bijective. -/574theorem frobenius_pow_degree_eq_id (O : Type) [CommRing O] [IsLocalRing O]575    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]576    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :577    frobeniusIter O Φ Φ.natDegree = AlgHom.id O (AdjoinRoot Φ) ∧578      Function.Bijective (unramifiedFrobenius O Φ) := by579  -- roots are preserved by algebra maps580  have hroot : ∀ f : AdjoinRoot Φ →ₐ[O] AdjoinRoot Φ,581      (Φ.map (AdjoinRoot.of Φ)).IsRoot (f (AdjoinRoot.root Φ)) := by582    intro f583    have h0 : Polynomial.aeval (AdjoinRoot.root Φ) Φ = 0 := AdjoinRoot.aeval_eq Φ ▸ by simp584    rw [Polynomial.IsRoot, Polynomial.eval_map, ← AdjoinRoot.algebraMap_eq,585      ← Polynomial.aeval_def, Polynomial.aeval_algHom_apply, h0, map_zero]586  have hid : frobeniusIter O Φ Φ.natDegree = AlgHom.id O (AdjoinRoot Φ) := by587    apply AdjoinRoot.algHom_ext588    obtain ⟨hF, hFin, hcard⟩ := residue_extension_field O Φ hΦ589    let _ := hF.toField590    let _ := Fintype.ofFinite (residueExtension O Φ)591    have hc : Fintype.card (residueExtension O Φ) = residueCard O ^ Φ.natDegree := by592      rw [← Nat.card_eq_fintype_card, hcard]593    have h2 := (frobenius_residue_action O Φ hΦ).2 Φ.natDegree (AdjoinRoot.root Φ)594    rw [← hc, FiniteField.pow_card] at h2595    exact root_unique_of_congruent O Φ hΦ _ _ (hroot _) (hroot (AlgHom.id O _))596      (Ideal.Quotient.eq.mp h2)597  refine ⟨hid, ?_⟩598  have hcomm : ∀ i, frobeniusIter O Φ (i+1) =599      (frobeniusIter O Φ i).comp (unramifiedFrobenius O Φ) := by600    intro i601    induction i with602    | zero => rfl603    | succ n ih =>604      change (unramifiedFrobenius O Φ).comp (frobeniusIter O Φ (n+1)) = _605      conv_lhs => rw [ih]606      rw [← AlgHom.comp_assoc]; rfl607  obtain ⟨d, hd⟩ : ∃ d, Φ.natDegree = d + 1 :=608    ⟨Φ.natDegree - 1, by have := natDegree_pos_of_isUnramifiedLift hΦ; omega⟩609  rw [Function.bijective_iff_has_inverse]610  refine ⟨frobeniusIter O Φ d, fun x => ?_, fun x => ?_⟩611  · have := congrArg (fun f : AdjoinRoot Φ →ₐ[O] AdjoinRoot Φ => f x) hid612    simp only [hd, hcomm] at this613    exact this614  · have := congrArg (fun f : AdjoinRoot Φ →ₐ[O] AdjoinRoot Φ => f x) hid615    simp only [hd] at this616    exact this617 618/-- For an unramified lift `Φ`, the ring `O[X]/(Φ)` is an integral domain. -/619private theorem unramified_is_domain (O : Type) [CommRing O] [IsDomain O]620    [IsDiscreteValuationRing O]621    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]622    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :623    IsDomain (AdjoinRoot Φ) := by624  classical625  obtain ⟨hcomp, hsep, htors⟩ := unramified_adic_complete O Φ hΦ.1626  obtain ⟨hfield, -, -⟩ := residue_extension_field O Φ hΦ627  let _ : Field (residueExtension O Φ) := hfield.toField628  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible O629  set c : AdjoinRoot Φ := algebraMap O (AdjoinRoot Φ) ϖ with hc630  have hI : baseIdeal O Φ = Ideal.span {c} := by631    rw [baseIdeal, hϖ.maximalIdeal_eq, Ideal.map_span, Set.image_singleton, hc,632      AdjoinRoot.algebraMap_eq]633  have hIpow : ∀ L : ℕ, (baseIdeal O Φ) ^ L = Ideal.span {c ^ L} := fun L => by634    rw [hI, Ideal.span_singleton_pow]635  have key : ∀ x : AdjoinRoot Φ, x ≠ 0 → ∃ (i : ℕ) (x' : AdjoinRoot Φ),636      x = c ^ i * x' ∧ x' ∉ baseIdeal O Φ := by637    intro x hx638    have hex : ∃ L, x ∉ (baseIdeal O Φ) ^ L := by639      by_contra h640      push Not at h641      exact hx (hsep x h)642    have hspec := Nat.find_spec hex643    have hn0 : Nat.find hex ≠ 0 := fun h0 => hspec (by simp [h0])644    obtain ⟨i, hi⟩ := Nat.exists_eq_succ_of_ne_zero hn0645    have hmem : x ∈ (baseIdeal O Φ) ^ i := by646      simpa using Nat.find_min hex (show i < Nat.find hex by omega)647    rw [hIpow, Ideal.mem_span_singleton'] at hmem648    obtain ⟨x', hx'⟩ := hmem649    refine ⟨i, x', by rw [← hx', mul_comm], fun hx'I => ?_⟩650    rw [hI, Ideal.mem_span_singleton'] at hx'I651    obtain ⟨d, hd⟩ := hx'I652    apply hspec653    rw [hi, hIpow, Ideal.mem_span_singleton']654    exact ⟨d, by rw [← hx', ← hd, pow_succ]; ring⟩655  have hnt : Nontrivial (AdjoinRoot Φ) := (baseReduce O Φ).domain_nontrivial656  have hnzd : NoZeroDivisors (AdjoinRoot Φ) := by657    constructor658    intro a b hab659    by_contra hne660    push Not at hne661    obtain ⟨i, a', rfl, ha'⟩ := key a hne.1662    obtain ⟨j, b', rfl, hb'⟩ := key b hne.2663    have h1 : algebraMap O (AdjoinRoot Φ) (ϖ ^ (i + j)) * (a' * b') = 0 := by664      rw [map_pow, ← hc, ← hab]; ring665    have h2 := htors _ (fun y hy => (mul_eq_zero.1 hy).resolve_left666      (pow_ne_zero _ hϖ.ne_zero)) _ h1667    have h3 : baseReduce O Φ a' * baseReduce O Φ b' = 0 := by668      rw [← map_mul, h2, map_zero]669    rcases mul_eq_zero.1 h3 with h | h670    · exact ha' (Ideal.Quotient.eq_zero_iff_mem.1 h)671    · exact hb' (Ideal.Quotient.eq_zero_iff_mem.1 h)672  exact NoZeroDivisors.to_isDomain _673 674/-! ### Conjugate products and descent of blocks -/675 676/-- For a block `b`, the product of the Frobenius conjugates of its monic polynomial is677Frobenius-invariant with coefficients in `O`, monic of degree `δ * r`, and reduces to678`∏ i, (X - θ̄ ^ (q ^ i)) ^ r`. -/679private theorem conjugate_product_invariant (O : Type) [CommRing O] [IsDomain O]680    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]681    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r : ℕ)682    (b : Fin r → AdjoinRoot Φ) (hb : b ∈ blockCell O Φ r) :683    (conjugateProduct O Φ (monicPolyO b)).map (unramifiedFrobenius O Φ).toRingHom =684        conjugateProduct O Φ (monicPolyO b) ∧685      (∀ j, ∃ c : O,686        algebraMap O (AdjoinRoot Φ) c = (conjugateProduct O Φ (monicPolyO b)).coeff j) ∧687      (conjugateProduct O Φ (monicPolyO b)).Monic ∧688      (conjugateProduct O Φ (monicPolyO b)).natDegree = Φ.natDegree * r ∧689      (conjugateProduct O Φ (monicPolyO b)).map (baseReduce O Φ) =690        ∏ i : Fin Φ.natDegree, conjugateFactor O Φ i ^ r := by691  have := unramified_is_domain O Φ hΦ692  obtain ⟨hBm, hBd, -, -⟩ := monic_poly_reconstruct (AdjoinRoot Φ) r b693  set B := monicPolyO b694  set δ := Φ.natDegree695  have hid := (frobenius_pow_degree_eq_id O Φ hΦ).1696  have hcomp : ∀ a c : ℕ,697      frobeniusIter O Φ (a + c) = (frobeniusIter O Φ a).comp (frobeniusIter O Φ c) := by698    intro a c699    induction a with700    | zero => simp [frobeniusIter]701    | succ a ih =>702      rw [show a + 1 + c = (a + c) + 1 by omega]703      simp only [frobeniusIter, ih]704      rfl705  have hmul : ∀ m : ℕ, frobeniusIter O Φ (δ * m) = AlgHom.id O (AdjoinRoot Φ) := by706    intro m707    induction m with708    | zero => simp [frobeniusIter]709    | succ m ih => rw [Nat.mul_succ, hcomp, ih, hid]; rfl710  have hmod : ∀ n : ℕ, frobeniusIter O Φ n = frobeniusIter O Φ (n % δ) := by711    intro n712    conv_lhs => rw [← Nat.mod_add_div n δ]713    rw [hcomp, hmul]; rfl714  have hP : ∀ i : Fin δ, (B.map (frobeniusIter O Φ i).toRingHom).Monic ∧715      (B.map (frobeniusIter O Φ i).toRingHom).natDegree = r := fun i =>716    ⟨hBm.map _, by rw [hBm.natDegree_map, hBd]⟩717  have hinv : (conjugateProduct O Φ B).map (unramifiedFrobenius O Φ).toRingHom =718      conjugateProduct O Φ B := by719    unfold conjugateProduct720    rw [Polynomial.map_prod]721    simp_rw [Polynomial.map_map]722    refine Fintype.prod_equiv (finRotate δ) _ _ (fun i => ?_)723    congr 1724    have hi := i.neZero725    rw [finRotate_apply, hmod ((i + 1 : Fin δ) : ℕ), Fin.val_add]726    have : (unramifiedFrobenius O Φ).toRingHom.comp (frobeniusIter O Φ i).toRingHom727        = (frobeniusIter O Φ ((i : ℕ) + 1)).toRingHom := rfl728    rw [this, hmod]729    congr 2730    simp [Nat.add_mod]731  refine ⟨hinv, fun j => ?_, Polynomial.monic_prod_of_monic _ _ (fun i _ => (hP i).1), ?_, ?_⟩732  · apply frobenius_fixed_ring O Φ hΦ733    simpa [Polynomial.coeff_map] using congrArg (fun p => Polynomial.coeff p j) hinv734  · unfold conjugateProduct735    rw [Polynomial.natDegree_prod_of_monic _ _ (fun i _ => (hP i).1),736      Finset.sum_congr rfl (fun i _ => (hP i).2)]737    simp [mul_comm]738  · have hres := (frobenius_residue_action O Φ hΦ).2739    unfold conjugateProduct740    rw [Polynomial.map_prod]741    refine Finset.prod_congr rfl (fun i _ => ?_)742    have hle : baseIdeal O Φ ≤ (baseIdeal O Φ).comap (frobeniusIter O Φ i).toRingHom := by743      rw [← Ideal.map_le_iff_le_comap, baseIdeal, Ideal.map_map]744      apply le_of_eq745      congr 1746      exact RingHom.ext fun c => (frobeniusIter O Φ i).commutes c747    let g := Ideal.quotientMap (baseIdeal O Φ) (frobeniusIter O Φ i).toRingHom hle748    have hg : (baseReduce O Φ).comp (frobeniusIter O Φ i).toRingHom =749        g.comp (baseReduce O Φ) := by750      ext x <;> simp [g, Ideal.quotientMap_mk]751    rw [Polynomial.map_map, hg, ← Polynomial.map_map, hb, conjugateFactor, conjugateFactor,752      Polynomial.map_pow, Polynomial.map_sub, Polynomial.map_X, Polynomial.map_C]753    congr 3754    change g (baseReduce O Φ (AdjoinRoot.root Φ) ^ residueCard O ^ 0) = _755    rw [pow_zero, pow_one]756    simp only [g, Ideal.quotientMap_mk]757    exact hres i _758 759/-- The descent of a block lies in the residue cell of `residuePoly Φ ^ r`, and its monic760polynomial lifts to the conjugate product of the block. -/761theorem descend_block_mem_cell (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]762    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]763    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r : ℕ) (b : Fin r → AdjoinRoot Φ)764    (hb : b ∈ blockCell O Φ r) :765    descendBlock O Φ r b ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r) ∧766      (monicPolyO (descendBlock O Φ r b)).map (AdjoinRoot.of Φ) =767        conjugateProduct O Φ (monicPolyO b) := by768  obtain ⟨_, hdesc, hPm, hPdeg, hPred⟩ := conjugate_product_invariant O Φ hΦ r b hb769  obtain ⟨hcompat, hinj, _, _, hfac, _⟩ := conjugate_roots_distinct O Φ hΦ770  obtain ⟨hFm, hFdeg, hFcoeff, _⟩ :=771    monic_poly_reconstruct O (Φ.natDegree * r) (descendBlock O Φ r b)772  set P := conjugateProduct O Φ (monicPolyO b)773  set F := monicPolyO (descendBlock O Φ r b)774  have hlift : F.map (AdjoinRoot.of Φ) = P := by775    ext j776    rw [Polynomial.coeff_map]777    by_cases hj : j < Φ.natDegree * r778    · rw [show F.coeff j = _ from hFcoeff ⟨j, hj⟩]779      change (AdjoinRoot.of Φ) (descendCoeff O Φ (P.coeff j)) = P.coeff j780      unfold descendCoeff781      rw [dif_pos (hdesc j)]782      exact Classical.choose_spec (hdesc j)783    · rcases (not_lt.mp hj).eq_or_lt with h | h784      · subst h785        have h1 : F.coeff (Φ.natDegree * r) = 1 := by786          have := hFm.coeff_natDegree; rwa [hFdeg] at this787        have h2 : P.coeff (Φ.natDegree * r) = 1 := by788          have := hPm.coeff_natDegree; rwa [hPdeg] at this789        rw [h1, h2, map_one]790      · rw [Polynomial.coeff_eq_zero_of_natDegree_lt (by rw [hFdeg]; exact h),791          Polynomial.coeff_eq_zero_of_natDegree_lt (by rw [hPdeg]; exact h), map_zero]792  refine ⟨?_, hlift⟩793  change F.map (IsLocalRing.residue O) = residuePoly O Φ ^ r794  apply Polynomial.map_injective _ hinj795  have hcomp : (residueEmbed O Φ).comp (IsLocalRing.residue O)796      = (baseReduce O Φ).comp (AdjoinRoot.of Φ) := by797    ext c; exact hcompat c798  rw [Polynomial.map_map, hcomp, ← Polynomial.map_map, hlift, hPred, Polynomial.map_pow, hfac,799    Finset.prod_pow]800 801/-- For an unramified lift `Φ`, `O[X]/(Φ)` is a complete DVR with maximal ideal `𝔪 O[X]/(Φ)`, in802which every uniformizer of `O` stays a uniformizer, with finite residue field of cardinality803`q ^ deg Φ`. -/804theorem unramified_is_dvr (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Standard facts805    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]806    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :807    ∃ (_ : IsDomain (AdjoinRoot Φ)) (_ : IsLocalRing (AdjoinRoot Φ)),808      IsDiscreteValuationRing (AdjoinRoot Φ) ∧809      IsLocalRing.maximalIdeal (AdjoinRoot Φ) = baseIdeal O Φ ∧810      (∀ ϖ : O, Irreducible ϖ → Irreducible (algebraMap O (AdjoinRoot Φ) ϖ)) ∧811      IsAdicComplete (IsLocalRing.maximalIdeal (AdjoinRoot Φ)) (AdjoinRoot Φ) ∧812      Finite (IsLocalRing.ResidueField (AdjoinRoot Φ)) ∧813      Nat.card (IsLocalRing.ResidueField (AdjoinRoot Φ)) = residueCard O ^ Φ.natDegree := by814  have hdom : IsDomain (AdjoinRoot Φ) := unramified_is_domain O Φ hΦ815  obtain ⟨-, -, hloc, hmax⟩ := base_ideal_maximal_local O Φ hΦ816  obtain ⟨hcomp, -, htors⟩ := unramified_adic_complete O Φ hΦ.1817  obtain ⟨-, hfin, hcard⟩ := residue_extension_field O Φ hΦ818  obtain ⟨ϖ₀, hϖ₀⟩ := IsDiscreteValuationRing.exists_irreducible O819  -- the maximal ideal is generated by the image of any uniformizer820  have hspan : ∀ ϖ : O, Irreducible ϖ →821      IsLocalRing.maximalIdeal (AdjoinRoot Φ) = Ideal.span {algebraMap O (AdjoinRoot Φ) ϖ} := by822    intro ϖ hϖ823    rw [hmax, baseIdeal, hϖ.maximalIdeal_eq, Ideal.map_span, Set.image_singleton]824    rfl825  have hnf : ¬ IsField (AdjoinRoot Φ) := by826    rw [IsLocalRing.isField_iff_maximalIdeal_eq, hspan ϖ₀ hϖ₀, Ideal.span_singleton_eq_bot]827    intro h828    exact one_ne_zero (htors ϖ₀ (fun y hy => (mul_eq_zero.1 hy).resolve_left hϖ₀.ne_zero) 1829      (by rw [h, zero_mul]))830  have hdvr : IsDiscreteValuationRing (AdjoinRoot Φ) := by831    have := (IsDiscreteValuationRing.TFAE (AdjoinRoot Φ) hnf).out 0 4832    exact this.2 ⟨⟨_, hspan ϖ₀ hϖ₀⟩⟩833  have e : IsLocalRing.ResidueField (AdjoinRoot Φ) ≃ residueExtension O Φ :=834    (Ideal.quotEquivOfEq hmax).toEquiv835  refine ⟨hdom, hloc, hdvr, hmax, fun ϖ hϖ =>836    (IsDiscreteValuationRing.irreducible_iff_uniformizer _).2 (hspan ϖ hϖ), hmax ▸ hcomp,837    Finite.of_equiv _ e.symm, by rw [Nat.card_congr e, hcard]⟩838 839/-- Reducing modulo the maximal ideal of `O[X]/(Φ)` agrees with reducing modulo `𝔪 O[X]/(Φ)`. -/840private theorem map_residue_eq_map_baseReduce {O : Type} [CommRing O] [IsLocalRing O]841    {Φ : Polynomial O} [IsLocalRing (AdjoinRoot Φ)]842    (hmax : IsLocalRing.maximalIdeal (AdjoinRoot Φ) = baseIdeal O Φ)843    (P : Polynomial (AdjoinRoot Φ)) :844    P.map (IsLocalRing.residue (AdjoinRoot Φ)) =845      (P.map (baseReduce O Φ)).map (Ideal.quotEquivOfEq hmax.symm).toRingHom := by846  rw [Polynomial.map_map]847  rfl848 849private theorem map_residue_eq_of_map_baseReduce_eq {O : Type} [CommRing O] [IsLocalRing O]850    {Φ : Polynomial O} [IsLocalRing (AdjoinRoot Φ)]851    (hmax : IsLocalRing.maximalIdeal (AdjoinRoot Φ) = baseIdeal O Φ)852    {P Q : Polynomial (AdjoinRoot Φ)} (h : P.map (baseReduce O Φ) = Q.map (baseReduce O Φ)) :853    P.map (IsLocalRing.residue (AdjoinRoot Φ)) = Q.map (IsLocalRing.residue (AdjoinRoot Φ)) := by854  rw [map_residue_eq_map_baseReduce hmax, map_residue_eq_map_baseReduce hmax, h]855 856private theorem isCoprime_map_residue {O : Type} [CommRing O] [IsLocalRing O]857    {Φ : Polynomial O} [IsLocalRing (AdjoinRoot Φ)]858    (hmax : IsLocalRing.maximalIdeal (AdjoinRoot Φ) = baseIdeal O Φ)859    {P Q : Polynomial (AdjoinRoot Φ)}860    (h : IsCoprime (P.map (baseReduce O Φ)) (Q.map (baseReduce O Φ))) :861    IsCoprime (P.map (IsLocalRing.residue (AdjoinRoot Φ)))862      (Q.map (IsLocalRing.residue (AdjoinRoot Φ))) := by863  rw [map_residue_eq_map_baseReduce hmax, map_residue_eq_map_baseReduce hmax]864  exact h.map (Polynomial.mapRingHom (Ideal.quotEquivOfEq hmax.symm).toRingHom)865 866/-- Applying the `i`-th Frobenius iterate to a polynomial reducing to `(X - θ̄) ^ r` gives a867polynomial reducing to `(X - θ̄ ^ (q ^ i)) ^ r`. -/868private theorem map_frobeniusIter_baseReduce (O : Type) [CommRing O] [IsLocalRing O]869    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]870    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r i : ℕ) (B : Polynomial (AdjoinRoot Φ))871    (hB : B.map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r) :872    (B.map (frobeniusIter O Φ i).toRingHom).map (baseReduce O Φ) = conjugateFactor O Φ i ^ r := by873  obtain ⟨-, hinj, -, -, -, -⟩ := conjugate_roots_distinct O Φ hΦ874  have hfrob := (frobenius_residue_action O Φ hΦ).2875  let K := residueExtension O Φ876  let : Fintype (IsLocalRing.ResidueField O) := Fintype.ofFinite _877  obtain ⟨p, hpc⟩ := CharP.exists (IsLocalRing.ResidueField O)878  obtain ⟨n, hp, hq⟩ := FiniteField.card (IsLocalRing.ResidueField O) p879  have : Fact p.Prime := ⟨hp⟩880  have : CharP K p := charP_of_injective_ringHom hinj p881  let fr : K →+* K := iterateFrobenius K p ((n : ℕ) * i)882  have hfr : ∀ x : K, fr x = x ^ (residueCard O ^ i) := fun x => by883    rw [residueCard, Nat.card_eq_fintype_card, hq, ← pow_mul]; rfl884  have hcomp' : (baseReduce O Φ).comp (frobeniusIter O Φ i).toRingHom =885      fr.comp (baseReduce O Φ) := RingHom.ext fun x => by886    simp only [RingHom.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, hfr, hfrob]887  rw [Polynomial.map_map, hcomp', ← Polynomial.map_map, hB, Polynomial.map_pow]888  simp [conjugateFactor, hfr]889 890/-- If monic polynomials `B i` over `O[X]/(Φ)` of degree `r`, with `B i` reducing to891`(X - θ̄ ^ (q ^ i)) ^ r`, multiply to the lift of `monicPolyO a`, then each `B i` is the `i`-th892Frobenius conjugate of `B 0`. -/893private theorem block_conjugates (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]894    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]895    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r : ℕ) (a : Fin (Φ.natDegree * r) → O)896    (hδ : 0 < Φ.natDegree)897    (B : Fin Φ.natDegree → Polynomial (AdjoinRoot Φ)) (hB : ∀ i, (B i).Monic)898    (hBr : ∀ i, (B i).map (baseReduce O Φ) = conjugateFactor O Φ i ^ r)899    (hBp : ∏ i, B i = (monicPolyO a).map (AdjoinRoot.of Φ)) :900    ∀ i : Fin Φ.natDegree, B i = (B ⟨0, hδ⟩).map (frobeniusIter O Φ i).toRingHom := by901  intro i902  obtain ⟨_, _, -, hmax, -, hcomp, -, -⟩ := unramified_is_dvr O Φ hΦ903  have hcop := (conjugate_roots_distinct O Φ hΦ).2.2.2.2.2904  set τ := frobeniusIter O Φ (i : ℕ)905  set F' := (monicPolyO a).map (AdjoinRoot.of Φ) with hF'906  set D := (B ⟨0, hδ⟩).map τ.toRingHom with hD907  have hτF : F'.map τ.toRingHom = F' := by908    rw [hF', Polynomial.map_map]909    congr 1910    ext x911    simp [← AdjoinRoot.algebraMap_eq]912  have hDred : D.map (baseReduce O Φ) = conjugateFactor O Φ i ^ r :=913    map_frobeniusIter_baseReduce O Φ hΦ r i _ (hBr _)914  have hprod1 : B i * ∏ j ∈ Finset.univ.erase i, B j = F' := by915    rw [Finset.mul_prod_erase _ _ (Finset.mem_univ i), hBp]916  have hprod2 : D * ∏ j ∈ Finset.univ.erase ⟨0, hδ⟩, (B j).map τ.toRingHom = F' := by917    rw [hD, Finset.mul_prod_erase (f := fun j => (B j).map τ.toRingHom) _ (Finset.mem_univ _),918      ← Polynomial.map_prod, hBp, hτF]919  have hc0 : IsCoprime ((B i).map (baseReduce O Φ))920      ((∏ j ∈ Finset.univ.erase i, B j).map (baseReduce O Φ)) := by921    rw [Polynomial.map_prod, hBr]922    exact IsCoprime.prod_right fun j hj => by923      rw [hBr]; exact (hcop i j (Finset.ne_of_mem_erase hj).symm).pow924  exact (hensel_factor_unique_of_dvd (AdjoinRoot Φ) _ _ _ _ (hB i)925    (Polynomial.monic_prod_of_monic _ _ fun j _ => hB j) ((hB _).map _)926    (Polynomial.monic_prod_of_monic _ _ fun j _ => (hB j).map _) (hprod1.trans hprod2.symm)927    (map_residue_eq_of_map_baseReduce_eq hmax (by rw [hBr, hDred]))928    (isCoprime_map_residue hmax hc0)).1929 930/-- Distinct Frobenius conjugates of the monic polynomial of a block are coprime over the931fraction field of `O[X]/(Φ)`. -/932theorem block_conjugates_coprime (O : Type) [CommRing O] [IsDomain O]933    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]934    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)935    [IsDomain (AdjoinRoot Φ)] (r : ℕ) (b : Fin r → AdjoinRoot Φ) (hb : b ∈ blockCell O Φ r) :936    ∀ i j : Fin Φ.natDegree, i ≠ j →937      IsCoprime (((monicPolyO b).map (frobeniusIter O Φ i).toRingHom).map938          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))))939        (((monicPolyO b).map (frobeniusIter O Φ j).toRingHom).map940          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) := by941  intro i j hij942  obtain ⟨_, _, hdvr, hmax, -, -, -, -⟩ := unramified_is_dvr O Φ hΦ943  have hBm : (monicPolyO b).Monic := (monic_poly_reconstruct (AdjoinRoot Φ) r b).1944  refine coprime_of_coprime_residue_dvr (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) _ _945    (hBm.map _) (hBm.map _) (isCoprime_map_residue hmax ?_)946  rw [map_frobeniusIter_baseReduce O Φ hΦ r i _ hb, map_frobeniusIter_baseReduce O Φ hΦ r j _ hb]947  exact ((conjugate_roots_distinct O Φ hΦ).2.2.2.2.2 i j hij).pow948 949/-- Hensel splitting: for `a` in the residue cell of `residuePoly Φ ^ r`, the lift of950`monicPolyO a` to `O[X]/(Φ)` factors uniquely as a product of monic polynomials `B i` of degree951`r` with `B i` reducing to `(X - θ̄ ^ (q ^ i)) ^ r`. -/952private theorem block_splitting (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]953    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]954    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r : ℕ) (a : Fin (Φ.natDegree * r) → O)955    (ha : a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r)) :956    ∃! B : Fin Φ.natDegree → Polynomial (AdjoinRoot Φ), (∀ i, (B i).Monic) ∧957      (∀ i, (B i).natDegree = r) ∧958      (∀ i, (B i).map (baseReduce O Φ) = conjugateFactor O Φ i ^ r) ∧959      ∏ i, B i = (monicPolyO a).map (AdjoinRoot.of Φ) := by960  obtain ⟨_, _, _, hm, -, hcomp, -, -⟩ := unramified_is_dvr O Φ hΦ961  obtain ⟨hcompat, -, -, -, hfact, hcop⟩ := conjugate_roots_distinct O Φ hΦ962  obtain ⟨hFm, -, -, -⟩ := monic_poly_reconstruct O _ a963  set F := monicPolyO a964  let e : IsLocalRing.ResidueField (AdjoinRoot Φ) ≃+* residueExtension O Φ :=965    Ideal.quotEquivOfEq hm966  have hmapE : ∀ P : Polynomial (AdjoinRoot Φ),967      (P.map (IsLocalRing.residue _)).map (e : _ →+* _) = P.map (baseReduce O Φ) := fun P => by968    rw [Polynomial.map_map]; rfl969  have hinj : Function.Injective (Polynomial.map970      (e : IsLocalRing.ResidueField (AdjoinRoot Φ) →+* residueExtension O Φ)) :=971    Polynomial.map_injective _ e.injective972  have hNt : Nontrivial (residueExtension O Φ) := e.symm.toEquiv.nontrivial973  let g : Fin Φ.natDegree → Polynomial (residueExtension O Φ) := fun i => conjugateFactor O Φ i ^ r974  have hgm : ∀ i, (g i).Monic := fun i => (Polynomial.monic_X_sub_C _).pow r975  have hgc : ∀ i j, i ≠ j → IsCoprime (g i) (g j) := fun i j h => (hcop i j h).pow976  have hgd : ∀ i, (g i).natDegree = r := fun i => by977    simp only [g, conjugateFactor]978    rw [(Polynomial.monic_X_sub_C _).natDegree_pow, Polynomial.natDegree_X_sub_C, mul_one]979  have hred : (F.map (AdjoinRoot.of Φ)).map (baseReduce O Φ) = ∏ i, g i := by980    have h1 : (baseReduce O Φ).comp (AdjoinRoot.of Φ) =981        (residueEmbed O Φ).comp (IsLocalRing.residue O) := by982      ext c; exact (hcompat c).symm983    rw [Polynomial.map_map, h1, ← Polynomial.map_map,984      show F.map (IsLocalRing.residue O) = residuePoly O Φ ^ r from ha, Polynomial.map_pow, hfact,985      ← Finset.prod_pow]986  have hsymm : ∀ P : Polynomial (residueExtension O Φ),987      (P.map (e.symm : residueExtension O Φ →+* IsLocalRing.ResidueField (AdjoinRoot Φ))).map988        (e : IsLocalRing.ResidueField (AdjoinRoot Φ) →+* residueExtension O Φ) = P := fun P => by989    simp [Polynomial.map_map]990  let g' : Fin Φ.natDegree → Polynomial (IsLocalRing.ResidueField (AdjoinRoot Φ)) :=991    fun i => (g i).map (e.symm : residueExtension O Φ →+* IsLocalRing.ResidueField (AdjoinRoot Φ))992  have hg'c : ∀ i j, i ≠ j → IsCoprime (g' i) (g' j) := fun i j h =>993    (hgc i j h).map (Polynomial.mapRingHom994      (e.symm : residueExtension O Φ →+* IsLocalRing.ResidueField (AdjoinRoot Φ)))995  have hred' : (F.map (AdjoinRoot.of Φ)).map (IsLocalRing.residue _) = ∏ i, g' i := by996    apply hinj997    simp only [hmapE, g', Polynomial.map_prod, hsymm, hred]998  obtain ⟨G, hGm, hGp, hGr, hGd⟩ := hensel_family_exists (AdjoinRoot Φ) (Fin Φ.natDegree)999    (F.map (AdjoinRoot.of Φ)) (hFm.map _) g' (fun i => (hgm i).map _) hg'c hred'1000  refine ⟨G, ⟨hGm, fun i => ?_, fun i => ?_, hGp.symm⟩, ?_⟩1001  · rw [hGd i, (hgm i).natDegree_map, hgd i]1002  · rw [← hmapE, hGr i, hsymm]1003  · rintro B ⟨hBm, -, hBr, hBp⟩1004    have hBr' : ∀ i, (B i).map (IsLocalRing.residue _) = g' i := fun i => by1005      apply hinj; rw [hmapE, hBr i, hsymm]1006    exact hensel_family_unique (AdjoinRoot Φ) (Fin Φ.natDegree) B G hBm hGm1007      (fun i => by rw [hBr' i, hGr i]) (fun i j h => by rw [hBr' i, hBr' j]; exact hg'c i j h)1008      (by rw [hBp, hGp])1009 1010/-- `selectBlock` picks block `0` of the Hensel splitting of the lift of `monicPolyO a`, which is1011the unique monic divisor of degree `r` reducing to `(X - θ̄) ^ r`. -/1012private theorem selectBlock_spec (O : Type) [CommRing O] [IsDomain O]1013    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1014    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)1015    (r : ℕ) (hδ : 0 < Φ.natDegree) (a : Fin (Φ.natDegree * r) → O)1016    (ha : a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r)) :1017    ∃ B : Fin Φ.natDegree → Polynomial (AdjoinRoot Φ), (∀ i, (B i).Monic) ∧1018      (∀ i, (B i).natDegree = r) ∧1019      (∀ i, (B i).map (baseReduce O Φ) = conjugateFactor O Φ i ^ r) ∧1020      ∏ i, B i = (monicPolyO a).map (AdjoinRoot.of Φ) ∧1021      (∀ B₀ : Polynomial (AdjoinRoot Φ), B₀.Monic → B₀.natDegree = r →1022        B₀.map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r →1023        B₀ ∣ (monicPolyO a).map (AdjoinRoot.of Φ) → B₀ = B ⟨0, hδ⟩) ∧1024      selectBlock O Φ r a = coeffVec r (B ⟨0, hδ⟩) ∧1025      monicPolyO (selectBlock O Φ r a) = B ⟨0, hδ⟩ := by1026  obtain ⟨B, ⟨hBm, hBd, hBr, hBp⟩, -⟩ := block_splitting O Φ hΦ r a ha1027  obtain ⟨_, _, _, hmax, -, hcomp, -, -⟩ := unramified_is_dvr O Φ hΦ1028  set i0 : Fin Φ.natDegree := ⟨0, hδ⟩1029  have huniq : ∀ B₀ : Polynomial (AdjoinRoot Φ), B₀.Monic → B₀.natDegree = r →1030      B₀.map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r →1031      B₀ ∣ (monicPolyO a).map (AdjoinRoot.of Φ) → B₀ = B i0 := by1032    intro B₀ hB₀m hB₀d hB₀r hdvd1033    obtain ⟨C₀, hC₀⟩ := hdvd1034    have hC₀m : C₀.Monic := Polynomial.Monic.of_mul_monic_left hB₀m1035      (hC₀ ▸ (monic_poly_reconstruct O _ a).1.map _)1036    set C := ∏ j ∈ Finset.univ.erase i0, B j1037    have hprod : B i0 * C = B₀ * C₀ := by1038      rw [Finset.mul_prod_erase _ _ (Finset.mem_univ _), hBp, hC₀]1039    have hcop := (conjugate_roots_distinct O Φ hΦ).2.2.2.2.21040    refine (hensel_factor_unique_of_dvd (AdjoinRoot Φ) (B i0) C B₀ C₀ (hBm i0)1041      (Polynomial.monic_prod_of_monic _ _ (fun j _ => hBm j)) hB₀m hC₀m hprod1042      (map_residue_eq_of_map_baseReduce_eq hmax (by rw [hBr, hB₀r]))1043      (isCoprime_map_residue hmax ?_)).1.symm1044    rw [Polynomial.map_prod]1045    refine IsCoprime.prod_right (fun j hj => ?_)1046    rw [hBr, hBr]1047    exact (hcop i0 j (Finset.ne_of_mem_erase hj).symm).pow1048  have hw : ∃ B₀ : Polynomial (AdjoinRoot Φ), B₀.Monic ∧ B₀.natDegree = r ∧1049      B₀.map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r ∧1050      B₀ ∣ (monicPolyO a).map (AdjoinRoot.of Φ) :=1051    ⟨B i0, hBm i0, hBd i0, hBr i0, hBp ▸ Finset.dvd_prod_of_mem _ (Finset.mem_univ _)⟩1052  have hs : selectBlock O Φ r a = coeffVec r (B i0) := by1053    unfold selectBlock1054    rw [dif_pos hw]1055    obtain ⟨h1, h2, h3, h4⟩ := Classical.choose_spec hw1056    rw [huniq _ h1 h2 h3 h4]1057  refine ⟨B, hBm, hBd, hBr, hBp, huniq, hs, ?_⟩1058  rw [hs]1059  exact (monic_poly_reconstruct _ r (coeffVec r (B i0))).2.2.2 _ (hBm i0) (hBd i0)1060 1061/-- Frobenius descent: `selectBlock` is a bijection from the residue cell of `residuePoly Φ ^ r`1062over `O` onto the block cell over `O[X]/(Φ)`, with inverse `descendBlock`; the selected monic1063polynomial divides the lift of `monicPolyO a`. -/1064theorem block_descent_bijection (O : Type) [CommRing O] [IsDomain O]Lemma 7.11065    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1066    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)1067    (r : ℕ) :1068    Set.BijOn (selectBlock O Φ r) (residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r))1069      (blockCell O Φ r) ∧1070    (∀ a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r),1071      descendBlock O Φ r (selectBlock O Φ r a) = a) ∧1072    (∀ b ∈ blockCell O Φ r, selectBlock O Φ r (descendBlock O Φ r b) = b) ∧1073    (∀ a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r),1074      (monicPolyO (selectBlock O Φ r a)).Monic ∧1075        monicPolyO (selectBlock O Φ r a) ∣ (monicPolyO a).map (AdjoinRoot.of Φ)) := by1076  obtain ⟨hdom, -, -, -, -, -, -, -⟩ := unramified_is_dvr O Φ hΦ1077  have hδ := natDegree_pos_of_isUnramifiedLift hΦ1078  have hinj : Function.Injective (algebraMap O (AdjoinRoot Φ)) := by1079    rw [AdjoinRoot.algebraMap_eq]1080    apply AdjoinRoot.of.injective_of_degree_ne_zero1081    rw [Polynomial.degree_eq_natDegree hΦ.1.ne_zero]1082    exact_mod_cast hδ.ne'1083  have hdesc : ∀ c : O, descendCoeff O Φ (algebraMap O (AdjoinRoot Φ) c) = c := by1084    intro c1085    have h : ∃ c' : O, algebraMap O (AdjoinRoot Φ) c' = algebraMap O (AdjoinRoot Φ) c := ⟨c, rfl⟩1086    unfold descendCoeff1087    rw [dif_pos h]1088    exact hinj (Classical.choose_spec h)1089  have hleft : ∀ a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r),1090      descendBlock O Φ r (selectBlock O Φ r a) = a := by1091    intro a ha1092    obtain ⟨B, hBm, hBd, hBr, hBp, -, -, hmp⟩ := selectBlock_spec O Φ hΦ r hδ a ha1093    have hconj := block_conjugates O Φ hΦ r a hδ B hBm hBr hBp1094    have hcp : conjugateProduct O Φ (monicPolyO (selectBlock O Φ r a)) =1095        (monicPolyO a).map (AdjoinRoot.of Φ) := by1096      rw [hmp, conjugateProduct, ← hBp]1097      exact Finset.prod_congr rfl (fun i _ => (hconj i).symm)1098    funext j1099    unfold descendBlock1100    rw [hcp, Polynomial.coeff_map, (monic_poly_reconstruct O _ a).2.2.1 j,1101      ← AdjoinRoot.algebraMap_eq, hdesc]1102  have hright : ∀ b ∈ blockCell O Φ r, selectBlock O Φ r (descendBlock O Φ r b) = b := by1103    intro b hb1104    obtain ⟨hcell, hF⟩ := descend_block_mem_cell O Φ hΦ r b hb1105    obtain ⟨B, hBm, hBd, hBr, hBp, huniq, hs, -⟩ := selectBlock_spec O Φ hΦ r hδ _ hcell1106    have hb' := monic_poly_reconstruct (AdjoinRoot Φ) r b1107    have heq : monicPolyO b = B ⟨0, hδ⟩ := by1108      refine huniq _ hb'.1 hb'.2.1 hb ?_1109      rw [hF, conjugateProduct]1110      have : monicPolyO b =1111          (monicPolyO b).map (frobeniusIter O Φ ((⟨0, hδ⟩ : Fin _) : ℕ)).toRingHom :=1112        Polynomial.map_id.symm1113      conv_lhs => rw [this]1114      exact Finset.dvd_prod_of_mem _ (Finset.mem_univ _)1115    rw [hs, ← heq]1116    exact funext hb'.2.2.11117  refine ⟨⟨fun a ha => ?_, fun a ha a' ha' h => ?_, fun b hb => ?_⟩, hleft, hright, fun a ha => ?_⟩1118  · obtain ⟨B, -, -, hBr, -, -, -, hmp⟩ := selectBlock_spec O Φ hΦ r hδ a ha1119    change (monicPolyO (selectBlock O Φ r a)).map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r1120    rw [hmp, hBr]1121  · rw [← hleft a ha, ← hleft a' ha', h]1122  · exact ⟨_, (descend_block_mem_cell O Φ hΦ r b hb).1, hright b hb⟩1123  · obtain ⟨B, hBm, -, -, hBp, -, -, hmp⟩ := selectBlock_spec O Φ hΦ r hδ a ha1124    rw [hmp]1125    exact ⟨hBm _, hBp ▸ Finset.dvd_prod_of_mem _ (Finset.mem_univ _)⟩1126 1127/-- Frobenius descent preserves congruences: `a ≡ a' (mod 𝔪 ^ L)` coordinatewise if and only if1128the selected blocks are congruent modulo `(𝔪 O[X]/(Φ)) ^ L`. -/1129theorem block_descent_congruence_iff (O : Type) [CommRing O] [IsDomain O]1130    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1131    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)1132    (r : ℕ) (L : ℕ) (a a' : Fin (Φ.natDegree * r) → O)1133    (ha : a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r))1134    (ha' : a' ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r)) :1135    (∀ j, a j - a' j ∈ (IsLocalRing.maximalIdeal O) ^ L) ↔1136      ∀ j, selectBlock O Φ r a j - selectBlock O Φ r a' j ∈ (baseIdeal O Φ) ^ L := by1137  obtain ⟨hdom, hloc, -, hmax, hirr, -, -, -⟩ := unramified_is_dvr O Φ hΦ1138  have hδ := natDegree_pos_of_isUnramifiedLift hΦ1139  obtain ⟨B, hBm, hBd, hBr, hBp, -, hs, -⟩ := selectBlock_spec O Φ hΦ r hδ a ha1140  obtain ⟨B', hBm', hBd', hBr', hBp', -, hs', -⟩ := selectBlock_spec O Φ hΦ r hδ a' ha'1141  rw [hs, hs']1142  have hpure := base_ideal_pure O Φ hΦ.1 hδ L1143  have hA := monic_poly_reconstruct O _ a1144  have hA' := monic_poly_reconstruct O _ a'1145  -- coefficientwise congruence of the lifted polynomials1146  have hlift : (∀ j, a j - a' j ∈ (IsLocalRing.maximalIdeal O) ^ L) ↔1147      ∀ j, ((monicPolyO a).map (AdjoinRoot.of Φ)).coeff j -1148        ((monicPolyO a').map (AdjoinRoot.of Φ)).coeff j ∈ (baseIdeal O Φ) ^ L := by1149    simp only [Polynomial.coeff_map, ← map_sub, ← AdjoinRoot.algebraMap_eq, hpure]1150    refine ⟨fun h => (monic_coeff_sub_mem_iff _ _ _ _ hA.1 hA'.1 hA.2.1 hA'.2.1).11151      (fun j => by rw [hA.2.2.1, hA'.2.2.1]; exact h j), fun h j => ?_⟩1152    simpa only [hA.2.2.1, hA'.2.2.1] using h j1153  rw [hlift]1154  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible O1155  have hspan : IsLocalRing.maximalIdeal (AdjoinRoot Φ) =1156      Ideal.span {algebraMap O (AdjoinRoot Φ) ϖ} := by1157    rw [hmax, baseIdeal, hϖ.maximalIdeal_eq, Ideal.map_span, Set.image_singleton,1158      AdjoinRoot.algebraMap_eq]1159  have hreg : ∀ x : AdjoinRoot Φ, algebraMap O (AdjoinRoot Φ) ϖ * x = 0 → x = 0 :=1160    fun x hx => (mul_eq_zero.mp hx).resolve_left (hirr ϖ hϖ).ne_zero1161  have hcop := (conjugate_roots_distinct O Φ hΦ).2.2.2.2.21162  constructor1163  · intro h j1164    have := hensel_family_unique_mod_pow (AdjoinRoot Φ) (Fin Φ.natDegree) _ hspan hreg B B' hBm1165      hBm' (fun i => map_residue_eq_of_map_baseReduce_eq hmax (by rw [hBr, hBr']))1166      (fun i j hij => isCoprime_map_residue hmax (by rw [hBr, hBr]; exact (hcop i j hij).pow)) L1167      (by rw [hBp, hBp', hmax]; exact h) ⟨0, hδ⟩ j1168    rwa [hmax] at this1169  · intro h1170    have h0 : ∀ j, (B ⟨0, hδ⟩).coeff j - (B' ⟨0, hδ⟩).coeff j ∈ (baseIdeal O Φ) ^ L :=1171      (monic_coeff_sub_mem_iff _ _ _ _ (hBm _) (hBm' _) (hBd _) (hBd' _)).1 h1172    have hconj := block_conjugates O Φ hΦ r a hδ B hBm hBr hBp1173    have hconj' := block_conjugates O Φ hΦ r a' hδ B' hBm' hBr' hBp'1174    have hJ : (baseIdeal O Φ) ^ L =1175        ((IsLocalRing.maximalIdeal O) ^ L).map (algebraMap O (AdjoinRoot Φ)) := by1176      rw [baseIdeal, Ideal.map_pow, AdjoinRoot.algebraMap_eq]1177    have hall : ∀ i j, (B i).coeff j - (B' i).coeff j ∈ (baseIdeal O Φ) ^ L := by1178      intro i j1179      rw [hconj i, hconj' i, Polynomial.coeff_map, Polynomial.coeff_map, ← map_sub]1180      have hm := Ideal.mem_map_of_mem (frobeniusIter O Φ i).toRingHom (h0 j)1181      rw [hJ, Ideal.map_map] at hm1182      rw [hJ]1183      convert hm using 21184      exact ((frobeniusIter O Φ i).comp_algebraMap).symm1185    have := (polynomial_congruence_and_product (AdjoinRoot Φ) ((baseIdeal O Φ) ^ L)).21186      (Fin Φ.natDegree) B B' hall1187    rwa [hBp, hBp'] at this1188 1189end SurfaceBlowup