Polynomial types, form products and residue cells

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.Algebra.FactorInvariant7 8/-!9# Polynomial types, form products and residue cells10 11Polynomial types of polynomials over `Frac O` (invariance under isomorphism of quotient algebras,12additivity on coprime products, uniqueness); the Hensel-type analysis of the normalized product13map on binary-form factor cells (congruence reflection, digit lifting, bijectivity); congruence14criteria for products of monic factors; residue cells as cylinders and their masses; and the15residue extension of an unramified lift `Φ` (a finite field in which `Φ̄` splits into distinct16conjugate linear factors), with the block translation `X ↦ X + θ`.17 18## Main results19 20* `SurfaceBlowup.polynomial_type_algEquiv_iff`, `SurfaceBlowup.polynomial_type_unique`21* `SurfaceBlowup.form_product_bijection`, `SurfaceBlowup.factor_product_congruence_iff`22* `SurfaceBlowup.residue_cell_mass`, `SurfaceBlowup.factor_cell_product_measure`23* `SurfaceBlowup.residue_extension_field`, `SurfaceBlowup.conjugate_roots_distinct`,24  `SurfaceBlowup.block_translation`25 26Provenance: `Thm_SurfaceBlowupV2_{polynomial_type_eq_of_algEquiv, polynomial_type_algEquiv_iff,27polynomial_type_mul_coprime, polynomial_type_unique, primitive_iff_residue_ne_zero,28product_first_order_expansion, form_product_congruence_reflects, form_product_digit_lift,29form_product_bijection, hensel_family_unique_mod_pow, factor_product_congruence_iff,30projective_normalizer_eval, residue_cell_cylinder, residue_cell_mass, factor_cell_product_measure,31residue_extension_equiv, residue_extension_field, block_translation, conjugate_roots_distinct,32residue_vector_fiber_mass, scalar_class_card}`.33-/34 35namespace SurfaceBlowup36 37open scoped ENNReal38 39/-- Polynomials over `Frac O` with isomorphic quotient algebras have the same polynomial type. -/40private theorem polynomial_type_eq_of_algEquiv (O : Type) [CommRing O] [IsDomain O]41    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]42    [Finite (IsLocalRing.ResidueField O)] (F F' : Polynomial (BaseField O)) (σ τ : FactorType)43    (hF : HasPolynomialTypeF O F σ) (hF' : HasPolynomialTypeF O F' τ)44    (e : AdjoinRoot F ≃ₐ[BaseField O] AdjoinRoot F') :45    σ = τ := by46  obtain ⟨gs, hgs, hgd, rfl, rfl, hfin⟩ := hF47  obtain ⟨hs, hhs, hhd, rfl, rfl, -⟩ := hF'48  obtain ⟨e₁, -⟩ := polynomial_quotient_product_equiv (BaseField O) gs hgs hgd49  obtain ⟨e₂, -⟩ := polynomial_quotient_product_equiv (BaseField O) hs hhs hhd50  have : ∀ i : Fin gs.length, Fact (Irreducible (gs.get i)) :=51    fun i => ⟨(hgs _ (List.get_mem _ _)).2⟩52  have : ∀ j : Fin hs.length, Fact (Irreducible (hs.get j)) :=53    fun j => ⟨(hhs _ (List.get_mem _ _)).2⟩54  obtain ⟨π, hπ⟩ := pi_fields_algEquiv_index_bijection (BaseField O) (Fin gs.length)55    (Fin hs.length) (fun i => AdjoinRoot (gs.get i)) (fun j => AdjoinRoot (hs.get j))56    (e₁.symm.trans (e.trans e₂))57  have key : ∀ i, factorInvariant O (gs.get i) = factorInvariant O (hs.get (π i)) := by58    intro i59    obtain ⟨φ, -⟩ := (hπ i).260    exact factor_invariant_algEquiv O _ _ (hgs _ (List.get_mem _ _)).161      (hgs _ (List.get_mem _ _)).2 (hhs _ (List.get_mem _ _)).1 (hhs _ (List.get_mem _ _)).2 φ62      (hfin _ (List.get_mem _ _))63  have hL : ∀ l : List (Polynomial (BaseField O)),64      ((l.map (factorInvariant O) : List (ℕ × ℕ)) : Multiset (ℕ × ℕ)) =65        Multiset.map (factorInvariant O ∘ l.get) (Finset.univ : Finset (Fin l.length)).val := by66    intro l67    conv_lhs => rw [← List.ofFn_get l]68    rw [← Multiset.map_coe, ← Multiset.map_map, Fin.univ_val_map]69  rw [hL gs, hL hs, ← Multiset.map_univ_val_equiv π, Multiset.map_map]70  exact Multiset.map_congr rfl (fun i _ => key i)71 72/-- One direction of `polynomial_type_algEquiv_iff`. -/73private theorem hasPolynomialTypeF_of_algEquiv (O : Type) [CommRing O] [IsDomain O]74    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]75    [Finite (IsLocalRing.ResidueField O)] (F F' : Polynomial (BaseField O)) (hF' : F'.Monic)76    (e : AdjoinRoot F ≃ₐ[BaseField O] AdjoinRoot F') (σ : FactorType) :77    HasPolynomialTypeF O F σ → HasPolynomialTypeF O F' σ := by78  intro h79  obtain ⟨gs, h1, h2, h3, h4, h5⟩ := h80  have hred : IsReduced (AdjoinRoot F) := by81    subst h382    obtain ⟨p, _⟩ := SurfaceBlowup.polynomial_quotient_product_equiv (BaseField O) gs h1 h283    have : ∀ i : Fin gs.length, Fact (Irreducible (gs.get i)) :=84        fun i => ⟨(h1 _ (List.get_mem _ _)).2⟩85    exact isReduced_of_injective (p.toRingEquiv.toRingHom) p.injective86  have hred' : IsReduced (AdjoinRoot F') :=87    isReduced_of_injective (e.symm.toRingEquiv.toRingHom) e.symm.injective88  obtain ⟨hs, k1, k2, k3⟩ := SurfaceBlowup.monic_squarefree_factors_of_reduced89      (BaseField O) F' hF' hred'90  -- closure finiteness of the factors of `F'`, by matching root fields with those of `F`91  have k4 : ∀ g ∈ hs, Module.Finite O (integralClosure O (AdjoinRoot g)) := by92    obtain ⟨e₁, -⟩ := SurfaceBlowup.polynomial_quotient_product_equiv (BaseField O) gs h1 h293    obtain ⟨e₂, -⟩ := SurfaceBlowup.polynomial_quotient_product_equiv (BaseField O) hs k1 k294    have : ∀ i : Fin gs.length, Fact (Irreducible (gs.get i)) :=95      fun i => ⟨(h1 _ (List.get_mem _ _)).2⟩96    have : ∀ j : Fin hs.length, Fact (Irreducible (hs.get j)) :=97      fun j => ⟨(k1 _ (List.get_mem _ _)).2⟩98    have e' : AdjoinRoot gs.prod ≃ₐ[BaseField O] AdjoinRoot hs.prod := by99      rw [← h3, ← k3]; exact e100    obtain ⟨π, hπ⟩ := SurfaceBlowup.pi_fields_algEquiv_index_bijection (BaseField O) (Fin gs.length)101      (Fin hs.length) (fun i => AdjoinRoot (gs.get i)) (fun j => AdjoinRoot (hs.get j))102      (e₁.symm.trans (e'.trans e₂))103    intro g hg104    obtain ⟨j, rfl⟩ := List.mem_iff_get.1 hg105    obtain ⟨i, rfl⟩ := π.surjective j106    obtain ⟨φ, -⟩ := (hπ i).2107    obtain ⟨χ, -⟩ := SurfaceBlowup.integral_closure_algEquiv O _ _ (φ.restrictScalars O)108    have := h5 _ (List.get_mem gs i)109    exact Module.Finite.equiv χ.toLinearEquiv110  have hty : HasPolynomialTypeF O F' (hs.map (factorInvariant O) : Multiset (ℕ × ℕ)) :=111    ⟨hs, k1, k2, k3, rfl, k4⟩112  have := SurfaceBlowup.polynomial_type_eq_of_algEquiv O F F' σ _ ⟨gs, h1, h2, h3, h4, h5⟩ hty e113  rw [this]; exact hty114 115 116/-- For monic `F, F'` with `Frac O[X]/(F) ≅ Frac O[X]/(F')`, `F` has type `σ` iff `F'` does. -/117theorem polynomial_type_algEquiv_iff (O : Type) [CommRing O] [IsDomain O]118    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]119    [Finite (IsLocalRing.ResidueField O)] (F F' : Polynomial (BaseField O)) (hF : F.Monic)120    (hF' : F'.Monic) (e : AdjoinRoot F ≃ₐ[BaseField O] AdjoinRoot F') (σ : FactorType) :121    HasPolynomialTypeF O F σ ↔ HasPolynomialTypeF O F' σ :=122  ⟨hasPolynomialTypeF_of_algEquiv O F F' hF' e σ, hasPolynomialTypeF_of_algEquiv O F' F hF e.symm σ⟩123 124/-- The polynomial type of a product of coprime polynomials is the sum of their types. -/125theorem polynomial_type_mul_coprime (O : Type) [CommRing O] [IsDomain O]126    (G H : Polynomial (BaseField O)) (σ τ : FactorType) (hG : HasPolynomialTypeF O G σ)127    (hH : HasPolynomialTypeF O H τ) (hc : IsCoprime G H) :128    HasPolynomialTypeF O (G * H) (σ + τ) := by129  obtain ⟨gs, hg1, hg2, hg3, hg4, hg5⟩ := hG130  obtain ⟨hs, hh1, hh2, hh3, hh4, hh5⟩ := hH131  refine ⟨gs ++ hs, ?_, ?_, ?_, ?_, ?_⟩132  · exact fun g hg => (List.mem_append.1 hg).elim (hg1 g) (hh1 g)133  · rw [List.pairwise_append]134    refine ⟨hg2, hh2, ?_⟩135    intro g hg h hh e136    subst e137    have h1 : g ∣ G := hg3 ▸ List.dvd_prod hg138    have h2 : g ∣ H := hh3 ▸ List.dvd_prod hh139    exact (hg1 g hg).2.not_isUnit (hc.isUnit_of_dvd' h1 h2)140  · rw [List.prod_append, hg3, hh3]141  · rw [List.map_append, hg4, hh4]; rfl142  · exact fun g hg => (List.mem_append.1 hg).elim (hg5 g) (hh5 g)143 144/-- A polynomial has at most one polynomial type. -/145theorem polynomial_type_unique (O : Type) [CommRing O] [IsDomain O] (F : Polynomial (BaseField O))146    (σ τ : FactorType) (hσ : HasPolynomialTypeF O F σ) (hτ : HasPolynomialTypeF O F τ) :147    σ = τ := by148  obtain ⟨gs, hg, -, hF, rfl, -⟩ := hσ149  obtain ⟨hs, hh, -, hF', rfl, -⟩ := hτ150  have hrel : Multiset.Rel Associated (gs : Multiset (Polynomial (BaseField O)))151      (hs : Multiset _) := by152    apply UniqueFactorizationMonoid.factors_unique153    · intro x hx; exact (hg x (by simpa using hx)).2154    · intro x hx; exact (hh x (by simpa using hx)).2155    · rw [Multiset.prod_coe, Multiset.prod_coe, ← hF, ← hF']; exact Associated.refl _156  have : Multiset.Rel Eq (gs : Multiset (Polynomial (BaseField O))) (hs : Multiset _) := by157    refine hrel.mono fun a ha b hb hab => ?_158    exact Polynomial.eq_of_monic_of_associated (hg a (by simpa using ha)).1159      (hh b (by simpa using hb)).1 hab160  have h2 := Multiset.rel_eq.mp this161  rw [Multiset.coe_eq_coe] at h2 ⊢162  exact (List.Perm.map _ h2)163 164/-- A coefficient vector is primitive iff its reduction is nonzero. -/165theorem primitive_iff_residue_ne_zero (O : Type) [CommRing O] [IsLocalRing O] (n : ℕ)166    (a : Fin (n + 1) → O) :167    primitive O a ↔ residueVector O a ≠ 0 := by168  rw [Function.ne_iff]169  unfold primitive residueVector170  refine exists_congr fun i => ?_171  simp only [Pi.zero_apply, ne_eq, IsLocalRing.residue_eq_zero_iff,172    IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not]173 174open scoped Classical in175/-- First-order expansion of a product: `∏ (G i + E i) ≡ ∏ G i + ∑ E i ∏_{j ≠ i} G j`176modulo `J²` when all `E i ∈ J`. -/177private theorem product_first_order_expansion (A ι : Type) [CommRing A] (J : Ideal A) (G E : ι → A)178    (hE : ∀ i, E i ∈ J) (s : Finset ι) :179    ∏ i ∈ s, (G i + E i) - ∏ i ∈ s, G i - ∑ i ∈ s, E i * ∏ j ∈ s.erase i, G j ∈ J ^ 2 := by180  induction s using Finset.induction_on with181  | empty => simp182  | insert a s ha ih =>183    set Q := ∏ i ∈ s, (G i + E i)184    set P := ∏ i ∈ s, G i185    set F := ∑ i ∈ s, E i * ∏ j ∈ s.erase i, G j186    have hF : F ∈ J := Ideal.sum_mem _ (fun i _ => Ideal.mul_mem_right _ _ (hE i))187    have hsum : ∑ i ∈ s, E i * ∏ j ∈ (insert a s).erase i, G j = G a * F := by188      rw [Finset.mul_sum]189      refine Finset.sum_congr rfl (fun i hi => ?_)190      have hne : i ≠ a := fun h => ha (h ▸ hi)191      rw [Finset.erase_insert_of_ne (Ne.symm hne), Finset.prod_insert192          (fun h => ha (Finset.mem_of_mem_erase h))]193      ring194    rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.sum_insert ha, Finset.erase_insert ha,195      hsum]196    have hR : Q - P - F ∈ J ^ 2 := ih197    have hQP : Q - P ∈ J := by198      have : Q - P = (Q - P - F) + F := by ring199      rw [this]200      exact J.add_mem (Ideal.pow_le_self two_ne_zero hR) hF201    have key : (G a + E a) * Q - G a * P - (E a * P + G a * F)202        = G a * (Q - P - F) + E a * (Q - P) := by ring203    rw [key]204    refine (J ^ 2).add_mem (Ideal.mul_mem_left _ _ hR) ?_205    rw [pow_two]206    exact Ideal.mul_mem_mul (hE a) hQP207 208/-! ### Coefficient lemmas for binary forms -/209 210section FormPoly211 212variable {A : Type} [CommRing A] {n : ℕ}213 214private theorem formPoly_coeff_eq (x : Fin (n + 1) → A) (k : Fin (n + 1)) :215    (formPoly x).coeff (k : ℕ) = x k := by216  simp [formPoly, Polynomial.finsetSum_coeff, Polynomial.coeff_X_pow, Fin.val_inj]217 218private theorem formPoly_smul_eq (c : A) (a : Fin (n + 1) → A) :219    formPoly (c • a) = Polynomial.C c * formPoly a := by220  simp [formPoly, Finset.mul_sum, mul_assoc]221 222private theorem formPoly_natDeg_le (a : Fin (n + 1) → A) : (formPoly a).natDegree ≤ n :=223  Polynomial.natDegree_sum_le_of_forall_le _ _ fun i _ =>224    (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.mp i.2)225 226private theorem formPoly_map_eq {B : Type} [CommRing B] (f : A →+* B) (a : Fin (n + 1) → A) :227    formPoly (fun k => f (a k)) = (formPoly a).map f := by228  simp [formPoly, Polynomial.map_sum]229 230private theorem formPoly_map_residue (O : Type) [CommRing O] [IsLocalRing O]231    (x : Fin (n + 1) → O) :232    (formPoly x).map (IsLocalRing.residue O) = formPoly (residueVector O x) :=233  (formPoly_map_eq _ x).symm234 235private theorem formPoly_prod_natDeg_le {ι : Type} (d : ι → ℕ) (v : ∀ i, Fin (d i + 1) → A)236    (s : Finset ι) : (∏ i ∈ s, formPoly (v i)).natDegree ≤ ∑ i ∈ s, d i :=237  (Polynomial.natDegree_prod_le _ _).trans (Finset.sum_le_sum fun _ _ => formPoly_natDeg_le _)238 239variable {ι : Type} [Fintype ι] {d : ι → ℕ}240 241open scoped Classical in242/-- The first-order term `∑ i, H i ∏_{j ≠ i} A j` has degree at most `∑ d i`. -/243private theorem natDegree_sum_formPoly_mul_le (A' H : ∀ i, Fin (d i + 1) → A) :244    (∑ i, formPoly (H i) * ∏ j ∈ Finset.univ.erase i, formPoly (A' j)).natDegree ≤ ∑ i, d i :=245  Polynomial.natDegree_sum_le_of_forall_le _ _ fun i _ => Polynomial.natDegree_mul_le.trans <| by246    have := formPoly_prod_natDeg_le d A' (Finset.univ.erase i)247    have := formPoly_natDeg_le (H i)248    rw [← Finset.add_sum_erase _ _ (Finset.mem_univ i)]249    omega250 251open scoped Classical in252/-- First-order expansion of a perturbed form product, coefficientwise:253`∏ (A i + c H i) ≡ ∏ A i + c ∑ H i ∏_{j ≠ i} A j` modulo `c²`. -/254private theorem formProd_add_smul_dvd (c : A) (A' H : ∀ i, Fin (d i + 1) → A)255    (k : Fin ((∑ i, d i) + 1)) :256    c ^ 2 ∣ formProd d (fun i => A' i + c • H i) k - formProd d A' k -257      c * (∑ i, formPoly (H i) * ∏ j ∈ Finset.univ.erase i, formPoly (A' j)).coeff k := by258  have h := product_first_order_expansion (Polynomial A) ι (Ideal.span {Polynomial.C c})259    (fun i => formPoly (A' i)) (fun i => Polynomial.C c * formPoly (H i))260    (fun i => Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)) Finset.univ261  rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton, ← map_pow,262    Polynomial.C_dvd_iff_dvd_coeff] at h263  simpa only [formProd, formPoly_add, formPoly_smul_eq, mul_assoc, ← Finset.mul_sum,264    Polynomial.coeff_sub, Polynomial.coeff_C_mul] using h k265 266end FormPoly267 268section DVR269 270variable {O : Type} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] {ϖ : O}271 272private theorem mem_maximalIdeal_pow_iff (hϖ : Irreducible ϖ) (n : ℕ) (x : O) :273    x ∈ IsLocalRing.maximalIdeal O ^ n ↔ ϖ ^ n ∣ x := by274  rw [hϖ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton]275 276private theorem residue_eq_zero_iff_dvd (hϖ : Irreducible ϖ) (x : O) :277    IsLocalRing.residue O x = 0 ↔ ϖ ∣ x := by278  rw [IsLocalRing.residue_eq_zero_iff, hϖ.maximalIdeal_eq, Ideal.mem_span_singleton]279 280end DVR281 282/-- On the product of the factor cells, the normalized product map is `P_{μ}⁻¹ P` with the283`μ`-coordinate dropped. -/284private theorem reducedFormProduct_of_mem (O : Type) [CommRing O] [IsLocalRing O] {ι : Type}285    [Fintype ι] (d : ι → ℕ) (ν : ∀ i, Fin (d i + 1))286    (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O) (μ : Fin ((∑ i, d i) + 1))287    {a : ∀ i, Fin (d i) → O} (ha : ∀ i, a i ∈ reducedFormCell O (d i) (ν i) (g i))288    (j : Fin (∑ i, d i)) :289    reducedFormProduct O d ν g μ a j =290      Ring.inverse (formProd d (fun i => insertOne (ν i) (a i)) μ) *291        formProd d (fun i => insertOne (ν i) (a i)) (μ.succAbove j) := by292  simp only [reducedFormProduct, if_pos ha, dropCoord, normalizeAt, Fin.removeNth_apply,293    Pi.smul_apply, smul_eq_mul]294 295/-- One step of congruence reflection: if two families `A, A'` of forms normalized at `ν`, with296residues `g`, agree modulo `ϖ ^ t` (`t ≥ 1`) and their products are proportional modulo297`ϖ ^ (t + 1)`, then the families agree modulo `ϖ ^ (t + 1)`. -/298private theorem form_congruence_step {O : Type} [CommRing O] [IsDomain O]299    [IsDiscreteValuationRing O] {ϖ : O} (hϖ : Irreducible ϖ) {ι : Type} [Fintype ι] (d : ι → ℕ)300    (ν : ∀ i, Fin (d i + 1)) (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O)301    (hgν : ∀ i, g i (ν i) = 1) (hc : FormsCoprime d g) (μ : Fin ((∑ i, d i) + 1))302    (hμ : formProd d g μ = 1) (A A' : ∀ i, Fin (d i + 1) → O) (hA1 : ∀ i, A i (ν i) = 1)303    (hA'1 : ∀ i, A' i (ν i) = 1) (hAres : ∀ i, residueVector O (A i) = g i)304    (hPres : ∀ k, IsLocalRing.residue O (formProd d A k) = formProd d g k) {t : ℕ} (ht : 1 ≤ t)305    (hM : ∀ k, ϖ ^ (t + 1) ∣306      formProd d A' μ * formProd d A k - formProd d A μ * formProd d A' k)307    (H : ∀ i, Fin (d i + 1) → O) (hH : ∀ i k, A' i k - A i k = ϖ ^ t * H i k) :308    ∀ i k, ϖ ^ (t + 1) ∣ A' i k - A i k := by309  classical310  have hres := residue_eq_zero_iff_dvd hϖ311  set P := formProd d A312  set P' := formProd d A'313  have hHν : ∀ i, H i (ν i) = 0 := fun i => by314    have h := hH i (ν i)315    rw [hA'1 i, hA1 i, sub_self, eq_comm, mul_eq_zero] at h316    exact h.resolve_left (pow_ne_zero _ hϖ.ne_zero)317  set S := ∑ i, formPoly (H i) * ∏ j ∈ Finset.univ.erase i, formPoly (A j)318  have hexp : ∀ k, (ϖ ^ t) ^ 2 ∣ P' k - P k - ϖ ^ t * S.coeff k := by319    have hA'H : A' = fun i => A i + ϖ ^ t • H i := funext fun i => funext fun k => by320      simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, ← hH i k]; ring321    intro k322    have h := formProd_add_smul_dvd (ϖ ^ t) A H k323    rwa [← hA'H] at h324  have hX : ∀ k, ϖ ∣ S.coeff μ * P k - P μ * S.coeff k := by325    intro k326    obtain ⟨s, rfl⟩ : ∃ s, t = s + 1 := ⟨t - 1, by omega⟩327    obtain ⟨e, he⟩ := hexp k328    obtain ⟨e', he'⟩ := hexp μ329    obtain ⟨f, hf⟩ := hM k330    refine (mul_dvd_mul_iff_left (pow_ne_zero (s + 1) hϖ.ne_zero)).mp331      ⟨f - ϖ ^ s * (e' * P k - P μ * e), ?_⟩332    linear_combination hf + P μ * he - P k * he'333  have hSmap : S.map (IsLocalRing.residue O) =334      Polynomial.C (IsLocalRing.residue O (S.coeff μ)) * ∏ i, formPoly (g i) := by335    ext n336    rw [Polynomial.coeff_map, Polynomial.coeff_C_mul]337    by_cases hn : n ≤ ∑ i, d i338    · have h := (hres _).2 (hX ⟨n, by omega⟩)339      rw [map_sub, map_mul, map_mul, hPres, hPres, hμ, one_mul, sub_eq_zero] at h340      exact h.symm341    · rw [Polynomial.coeff_eq_zero_of_natDegree_lt342        ((natDegree_sum_formPoly_mul_le A H).trans_lt (by omega)),343        Polynomial.coeff_eq_zero_of_natDegree_lt344        ((formPoly_prod_natDeg_le d g Finset.univ).trans_lt (by omega)), mul_zero, map_zero]345  have hinj := forms_linear_injective (IsLocalRing.ResidueField O) ι d g346    (fun i h0 => by simpa [h0] using hgν i) hc ν (fun i => by simp [hgν])347    (fun i m => IsLocalRing.residue O (H i m)) (fun i => by simp [hHν])348    (IsLocalRing.residue O (S.coeff μ)) (by349      rw [← hSmap, Polynomial.map_sum]350      refine Finset.sum_congr rfl fun i _ => ?_351      simp only [Polynomial.map_mul, Polynomial.map_prod, formPoly_map_residue, hAres]352      rfl)353  intro i k354  obtain ⟨y, hy⟩ := (hres _).1 (congrFun (hinj i) k)355  exact ⟨y, by rw [hH i k, hy]; ring⟩356 357/-- The normalized form-product map reflects congruences: if the products of two families in358the factor cells agree modulo `m^L`, so do the families. -/359theorem form_product_congruence_reflects (O : Type) [CommRing O] [IsDomain O]360    [IsDiscreteValuationRing O] (ι : Type) [Fintype ι] (d : ι → ℕ) (ν : ∀ i, Fin (d i + 1))361    (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O) (hgν : ∀ i, g i (ν i) = 1)362    (hc : FormsCoprime d g) (μ : Fin ((∑ i, d i) + 1)) (hμ : formProd d g μ = 1)363    (a a' : ∀ i, Fin (d i) → O)364    (ha : a ∈ Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i)))365    (ha' : a' ∈ Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i))) (L : ℕ)366    (hL : ∀ j, reducedFormProduct O d ν g μ a j - reducedFormProduct O d ν g μ a' j ∈367      (IsLocalRing.maximalIdeal O) ^ L) :368    ∀ i j, a i j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L := by369  classical370  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible O371  have hres := residue_eq_zero_iff_dvd hϖ372  have ha₁ : ∀ i, a i ∈ reducedFormCell O (d i) (ν i) (g i) := fun i => ha i (Set.mem_univ _)373  have ha₁' : ∀ i, a' i ∈ reducedFormCell O (d i) (ν i) (g i) := fun i => ha' i (Set.mem_univ _)374  obtain ⟨-, hPres, hu, -⟩ := form_product_maps_to_and_preserves O ι d ν g μ hμ a a ha ha375  obtain ⟨-, -, hu', -⟩ := form_product_maps_to_and_preserves O ι d ν g μ hμ a' a' ha' ha'376  set A : ∀ i, Fin (d i + 1) → O := fun i => insertOne (ν i) (a i) with hA377  set A' : ∀ i, Fin (d i + 1) → O := fun i => insertOne (ν i) (a' i) with hA'378  set P := formProd d A379  set P' := formProd d A'380  have hAres : ∀ i k, IsLocalRing.residue O (A i k) = g i k := fun i k => congrFun (ha₁ i).2 k381  have hA'res : ∀ i k, IsLocalRing.residue O (A' i k) = g i k := fun i k => congrFun (ha₁' i).2 k382  have hPres : ∀ k, IsLocalRing.residue O (P k) = formProd d g k := fun k => congrFun hPres k383  have e1 : Ring.inverse (P μ) * P μ = 1 := Ring.inverse_mul_cancel _ hu384  have e2 : Ring.inverse (P' μ) * P' μ = 1 := Ring.inverse_mul_cancel _ hu'385  -- `hL`, cross-multiplied, in all coordinates386  have hM : ∀ k, ϖ ^ L ∣ P' μ * P k - P μ * P' k := by387    intro k388    have hN : ϖ ^ L ∣ Ring.inverse (P μ) * P k - Ring.inverse (P' μ) * P' k := by389      rcases Fin.eq_self_or_eq_succAbove μ k with rfl | ⟨j, rfl⟩390      · rw [e1, e2, sub_self]; exact dvd_zero _391      · have h := (mem_maximalIdeal_pow_iff hϖ _ _).1 (hL j)392        rwa [reducedFormProduct_of_mem O d ν g μ ha₁, reducedFormProduct_of_mem O d ν g μ ha₁'] at h393    convert dvd_mul_of_dvd_right hN (P μ * P' μ) using 1394    linear_combination (-(P' μ * P k)) * e1 + (P μ * P' k) * e2395  -- induction on the precision396  have claim : ∀ t, 1 ≤ t → t ≤ L → ∀ i k, ϖ ^ t ∣ A' i k - A i k := by397    intro t ht398    induction t, ht using Nat.le_induction with399    | base => intro _ i k; rw [pow_one, ← hres, map_sub, hAres, hA'res, sub_self]400    | succ t ht IH =>401      intro htL402      choose H hH using IH (by omega)403      exact form_congruence_step hϖ d ν g hgν hc μ hμ A A' (fun i => (ha₁ i).1)404        (fun i => (ha₁' i).1) (fun i => (ha₁ i).2) hPres ht405        (fun k => (pow_dvd_pow ϖ htL).trans (hM k)) H hH406  intro i j407  rcases Nat.eq_zero_or_pos L with rfl | hL0408  · simp409  · rw [mem_maximalIdeal_pow_iff hϖ, ← dvd_neg, neg_sub]410    simpa [hA, hA', insertOne] using claim L hL0 le_rfl i ((ν i).succAbove j)411 412/-- Digit lifting for the normalized form-product map: an approximate preimage modulo `m^t` can413be corrected by `m^t` to an approximate preimage modulo `m^(t+1)`. -/414private theorem form_product_digit_lift (O : Type) [CommRing O] [IsDomain O]415    [IsDiscreteValuationRing O]416    (ι : Type) [Fintype ι] (d : ι → ℕ) (ν : ∀ i, Fin (d i + 1))417    (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O) (hgν : ∀ i, g i (ν i) = 1)418    (hc : FormsCoprime d g) (μ : Fin ((∑ i, d i) + 1)) (hμ : formProd d g μ = 1)419    (a : ∀ i, Fin (d i) → O)420    (ha : a ∈ Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i)))421    (c : Fin (∑ i, d i) → O) (hcD : c ∈ reducedFormCell O (∑ i, d i) μ (formProd d g)) (t : ℕ)422    (ht : 1 ≤ t)423    (hct : ∀ j, reducedFormProduct O d ν g μ a j - c j ∈ (IsLocalRing.maximalIdeal O) ^ t) :424    ∃ a' ∈ Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i)),425      (∀ i j, a' i j - a i j ∈ (IsLocalRing.maximalIdeal O) ^ t) ∧ ∀ j,426      reducedFormProduct O d ν g μ a' j - c j ∈ (IsLocalRing.maximalIdeal O) ^ (t+1) := by427  classical428  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible O429  have hM := mem_maximalIdeal_pow_iff hπ430  have hres := residue_eq_zero_iff_dvd hπ431  obtain ⟨s, rfl⟩ : ∃ s, t = s + 1 := ⟨t - 1, by omega⟩432  have ha₁ : ∀ i, a i ∈ reducedFormCell O (d i) (ν i) (g i) := fun i => ha i (Set.mem_univ _)433  obtain ⟨-, hPres, hu, -⟩ := form_product_maps_to_and_preserves O ι d ν g μ hμ a a ha ha434  set A : ∀ i, Fin (d i + 1) → O := fun i => insertOne (ν i) (a i) with hAdef435  have hA1 : ∀ i, A i (ν i) = 1 := fun i => (ha₁ i).1436  have hAres : ∀ i, residueVector O (A i) = g i := fun i => (ha₁ i).2437  set P := formProd d A438  set v := Ring.inverse (P μ)439  have hvu : v * P μ = 1 := Ring.inverse_mul_cancel _ hu440  have hu1 : π ∣ P μ - 1 := by441    rw [← hres, map_sub, map_one, sub_eq_zero, ← hμ]442    exact congrFun hPres μ443  set ct := insertOne μ c444  have hct1 : ct μ = 1 := hcD.1445  -- the defect `ct - v P`, in units of `π^t`446  have hdiff : ∀ k, π ^ (s+1) ∣ ct k - v * P k := by447    intro k448    rcases Fin.eq_self_or_eq_succAbove μ k with rfl | ⟨j, rfl⟩449    · rw [hct1, hvu, sub_self]; exact dvd_zero _450    · have h := (hM _ _).1 (hct j)451      rw [reducedFormProduct_of_mem O d ν g μ ha₁, ← dvd_neg, neg_sub] at h452      rwa [show ct (μ.succAbove j) = c j by simp [ct, insertOne]]453  choose w hw using hdiff454  -- solve the linearized equation over the residue field and lift the solution455  obtain ⟨hb, c₀, hbν, hbeq⟩ := forms_linear_bijective (IsLocalRing.ResidueField O) ι d g456    (fun i h => by simpa [h] using hgν i) hc ν (fun i => by simp [hgν]) (residueVector O w)457  choose H₀ hH₀ using fun i k => IsLocalRing.residue_surjective (hb i k)458  set H : ∀ i, Fin (d i + 1) → O := fun i k => H₀ i k - H₀ i (ν i)459  have hHres : ∀ i, residueVector O (H i) = hb i := fun i => funext fun k => by460    simp [residueVector, H, hH₀, hbν]461  obtain ⟨c₀', hc₀'⟩ := IsLocalRing.residue_surjective c₀462  set A' : ∀ i, Fin (d i + 1) → O := fun i => A i + π ^ (s+1) • H i463  set a' : ∀ i, Fin (d i) → O := fun i => dropCoord (ν i) (A' i)464  have hA'1 : ∀ i, A' i (ν i) = 1 := fun i => by simp [A', H, hA1]465  have hins : ∀ i, insertOne (ν i) (a' i) = A' i := fun i => by466    simp only [a', insertOne, dropCoord]467    rw [← hA'1 i, Fin.insertNth_self_removeNth]468  have ha'cell : ∀ i, a' i ∈ reducedFormCell O (d i) (ν i) (g i) := fun i => by469    change insertOne (ν i) (a' i) ∈ normalizedFormCell O (d i) (ν i) (g i)470    rw [hins, ← hAres i]471    refine ⟨hA'1 i, funext fun k => ?_⟩472    simp [residueVector, A', (hres π).2 dvd_rfl]473  refine ⟨a', fun i _ => ha'cell i, fun i j => ?_, fun j => ?_⟩474  · rw [hM]475    simp [a', A', A, dropCoord, insertOne, Fin.removeNth_apply]476  -- main congruence: `P' ≡ λ ct` modulo `π^(t+1)`477  obtain ⟨-, -, hu', -⟩ := form_product_maps_to_and_preserves O ι d ν g μ hμ a' a'478    (fun i _ => ha'cell i) (fun i _ => ha'cell i)479  set S := ∑ i, formPoly (H i) * ∏ j ∈ Finset.univ.erase i, formPoly (A j)480  have hR : Polynomial.C π ∣ S + Polynomial.C c₀' * ∏ i, formPoly (A i) - formPoly w := by481    rw [Polynomial.C_dvd_iff_dvd_coeff]482    intro m483    rw [← hres, ← Polynomial.coeff_map]484    convert Polynomial.coeff_zero m485    simp only [S, Polynomial.map_sub, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul,486      Polynomial.map_prod, formPoly_map_residue, hAres, hHres, Polynomial.map_C, hc₀']487    rw [sub_eq_zero, hbeq]488  set lam := P μ - π ^ (s+1) * c₀'489  have hkey : ∀ k, π ^ (s+2) ∣ formProd d A' k - lam * ct k := by490    intro k491    obtain ⟨f, hf⟩ := formProd_add_smul_dvd (π ^ (s+1)) A H k492    obtain ⟨r, hr⟩ := (Polynomial.C_dvd_iff_dvd_coeff _ _).1 hR k493    simp only [Polynomial.coeff_sub, Polynomial.coeff_add, Polynomial.coeff_C_mul,494      formPoly_coeff_eq, show (∏ i, formPoly (A i)).coeff k = P k from rfl] at hr495    obtain ⟨e, he⟩ := hu1496    refine ⟨π ^ s * f + r - e * w k - c₀' * P k * v * e + π ^ s * c₀' * w k, ?_⟩497    linear_combination hf + π ^ (s+1) * hr - lam * hw k -498      (π ^ (s+1) * w k + π ^ (s+1) * c₀' * P k * v) * he + (π ^ (s+1) * c₀' * P k - P k) * hvu499  have hv' := Ring.inverse_mul_cancel _ hu'500  rw [hM, reducedFormProduct_of_mem O d ν g μ ha'cell]501  have hf : (fun i => insertOne (ν i) (a' i)) = A' := funext hins502  rw [hf] at hv' ⊢503  obtain ⟨x, hx⟩ := hkey (μ.succAbove j)504  obtain ⟨y, hy⟩ : π ^ (s+2) ∣ formProd d A' μ - lam := by simpa [hct1] using hkey μ505  rw [show c j = ct (μ.succAbove j) by simp [ct, insertOne]]506  refine ⟨Ring.inverse (formProd d A' μ) * (x - y * ct (μ.succAbove j)), ?_⟩507  linear_combination ct (μ.succAbove j) * hv' + Ring.inverse (formProd d A' μ) * hx -508    Ring.inverse (formProd d A' μ) * ct (μ.succAbove j) * hy509 510/-- Membership in a reduced factor cell, coordinatewise. -/511private theorem reducedFormCell_iff (O : Type) [CommRing O] [IsLocalRing O] (d : ℕ)512    (ν : Fin (d + 1))513    (g : Fin (d + 1) → IsLocalRing.ResidueField O) (hgν : g ν = 1) (b : Fin d → O) :514    b ∈ reducedFormCell O d ν g ↔ ∀ j, IsLocalRing.residue O (b j) = g (ν.succAbove j) := by515  simp only [reducedFormCell, normalizedFormCell, Set.mem_ofPred_eq, insertOne,516    Fin.insertNth_apply_same, true_and, residueVector, funext_iff]517  rw [Fin.forall_iff_succAbove ν]518  simp [hgν]519 520private theorem sub_mem_maximalIdeal_iff (O : Type) [CommRing O] [IsLocalRing O] (x y : O) :521    x - y ∈ IsLocalRing.maximalIdeal O ↔ IsLocalRing.residue O x = IsLocalRing.residue O y :=522  (Ideal.Quotient.eq (I := IsLocalRing.maximalIdeal O)).symm523 524private theorem eq_zero_of_forall_mem_pow (O : Type) [CommRing O] [IsLocalRing O]525    [IsAdicComplete (IsLocalRing.maximalIdeal O) O]526    (x : O) (h : ∀ n : ℕ, x ∈ (IsLocalRing.maximalIdeal O) ^ n) : x = 0 :=527  IsHausdorff.haus (I := IsLocalRing.maximalIdeal O) IsAdicComplete.toIsHausdorff _ fun n => by528    simpa [SModEq.zero, smul_eq_mul, Ideal.mul_top] using h n529 530/-- Over a complete DVR, the normalized form-product map is a bijection from the product of the531factor cells onto the product cell. -/532theorem form_product_bijection (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]533    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (ι : Type) [Fintype ι] (d : ι → ℕ)534    (ν : ∀ i, Fin (d i + 1)) (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O)535    (hgν : ∀ i, g i (ν i) = 1) (hc : FormsCoprime d g) (μ : Fin ((∑ i, d i) + 1))536    (hμ : formProd d g μ = 1) :537    Set.BijOn (reducedFormProduct O d ν g μ)538      (Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i)))539      (reducedFormCell O (∑ i, d i) μ (formProd d g)) := by540  set m := IsLocalRing.maximalIdeal O541  set S := Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i))542  refine ⟨?_, ?_, ?_⟩543  · exact fun a ha => (form_product_maps_to_and_preserves O ι d ν g μ hμ a a ha ha).1544  · intro a ha a' ha' h545    funext i j546    rw [← sub_eq_zero]547    apply eq_zero_of_forall_mem_pow O548    intro L549    refine form_product_congruence_reflects O ι d ν g hgν hc μ hμ a a' ha ha' L ?_ i j550    intro j; simp [h]551  · intro c hc'552    have hcell := fun i => reducedFormCell_iff O (d i) (ν i) (g i) (hgν i)553    have hGcell := reducedFormCell_iff O (∑ i, d i) μ (formProd d g) hμ554    -- base point555    have a₁ : ∃ a, a ∈ S := by556      refine ⟨fun i j => (IsLocalRing.residue_surjective (g i ((ν i).succAbove j))).choose, ?_⟩557      intro i _558      rw [hcell]559      intro j560      exact (IsLocalRing.residue_surjective _).choose_spec561    obtain ⟨a₁, ha₁⟩ := a₁562    let P : ℕ → (∀ i, Fin (d i) → O) → Prop := fun t a =>563      a ∈ S ∧ ∀ j, reducedFormProduct O d ν g μ a j - c j ∈ m ^ (t + 1)564    have hP0 : P 0 a₁ := by565      refine ⟨ha₁, fun j => ?_⟩566      rw [zero_add, pow_one, sub_mem_maximalIdeal_iff]567      have h1 := (hGcell _).1568        (form_product_maps_to_and_preserves O ι d ν g μ hμ a₁ a₁ ha₁ ha₁).1 j569      rw [h1, (hGcell c).1 hc' j]570    have step : ∀ t a, P t a → ∃ a', P (t+1) a' ∧ ∀ i j, a' i j - a i j ∈ m ^ (t + 1) := by571      intro t a ha572      obtain ⟨a', ha', h1, h2⟩ := form_product_digit_lift O ι d ν g hgν hc μ hμ a ha.1 c hc'573        (t+1) (by omega) ha.2574      exact ⟨a', ⟨ha', h2⟩, h1⟩575    let f : (t : ℕ) → {a // P t a} := fun t => Nat.rec (motive := fun t => {a // P t a})576      ⟨a₁, hP0⟩ (fun t x => ⟨(step t x.1 x.2).choose, (step t x.1 x.2).choose_spec.1⟩) t577    have hf : ∀ t i j, (f (t+1)).1 i j - (f t).1 i j ∈ m ^ (t + 1) := fun t =>578      (step t (f t).1 (f t).2).choose_spec.2579    have hcompat : ∀ s t, s ≤ t → ∀ i j, (f s).1 i j - (f t).1 i j ∈ m ^ (s + 1) := by580      intro s t hst i j581      induction t, hst using Nat.le_induction with582      | base => simp583      | succ t hst ih =>584        simpa only [sub_sub_sub_cancel_right] using585          sub_mem ih (Ideal.pow_le_pow_right (I := m) (by omega : s + 1 ≤ t + 1) (hf t i j))586    have hlim : ∀ i j, ∃ ℓ : O, ∀ n, (f n).1 i j - ℓ ∈ m ^ n := by587      intro i j588      obtain ⟨ℓ, hℓ⟩ := IsPrecomplete.prec (I := m) (IsAdicComplete.toIsPrecomplete)589        (f := fun n => (f n).1 i j) (by590          intro s t hst591          rw [SModEq.sub_mem]592          simpa [smul_eq_mul, Ideal.mul_top] using593            Ideal.pow_le_pow_right (I := m) (by omega : s ≤ s + 1) (hcompat s t hst i j))594      refine ⟨ℓ, fun n => ?_⟩595      have := hℓ n596      rw [SModEq.sub_mem] at this597      simpa [smul_eq_mul, Ideal.mul_top] using this598    choose ℓ hℓ using hlim599    have haS : ℓ ∈ S := by600      intro i _601      rw [hcell]602      intro j603      have h0' : (f 0).1 i j - ℓ i j ∈ m := by604        rw [← sub_add_sub_cancel _ ((f 1).1 i j)]605        exact add_mem (by simpa using hcompat 0 1 (by omega) i j) (by simpa using hℓ i j 1)606      rw [sub_mem_maximalIdeal_iff] at h0'607      rw [← h0']608      exact (hcell i _).1 ((f 0).2.1 i (Set.mem_univ _)) j609    refine ⟨ℓ, haS, ?_⟩610    funext j611    rw [← sub_eq_zero]612    apply eq_zero_of_forall_mem_pow O613    intro t614    have h1 := (form_product_maps_to_and_preserves O ι d ν g μ hμ ℓ (f t).1 haS615      (f t).2.1).2.2.2 t (fun i j => by616        have := hℓ i j t617        rw [← neg_sub]; exact neg_mem this) j618    have h2 := Ideal.pow_le_pow_right (I := m) (by omega : t ≤ t + 1) ((f t).2.2 j)619    simpa only [sub_add_sub_cancel] using add_mem h1 h2620 621/-- Hensel uniqueness modulo `m^L`: monic factors with pairwise coprime reductions whose products622agree modulo `m^L` agree factorwise modulo `m^L`. -/623theorem hensel_family_unique_mod_pow (O ι : Type) [CommRing O] [IsLocalRing O] [Fintype ι] (pi : O)624    (hpi : IsLocalRing.maximalIdeal O = Ideal.span {pi}) (hreg : ∀ x : O, pi * x = 0 → x = 0)625    (G G' : ι → Polynomial O) (hG : ∀ i, (G i).Monic) (hG' : ∀ i, (G' i).Monic)626    (hred : ∀ i, (G i).map (IsLocalRing.residue O) = (G' i).map (IsLocalRing.residue O))627    (hc : ∀ i j, i ≠ j → IsCoprime ((G i).map (IsLocalRing.residue O))628      ((G j).map (IsLocalRing.residue O))) (L : ℕ)629    (hp : ∀ j, (∏ i, G i).coeff j - (∏ i, G' i).coeff j ∈ (IsLocalRing.maximalIdeal O) ^ L) :630    ∀ i j, (G i).coeff j - (G' i).coeff j ∈ (IsLocalRing.maximalIdeal O) ^ L := by631  classical632  have hmpow : ∀ t x, x ∈ (IsLocalRing.maximalIdeal O) ^ t ↔ pi ^ t ∣ x := by633    intro t x; rw [hpi, Ideal.span_singleton_pow, Ideal.mem_span_singleton]634  have hmem : ∀ x : O, x ∈ IsLocalRing.maximalIdeal O ↔ pi ∣ x := by635    intro x; rw [hpi, Ideal.mem_span_singleton]636  have hdeg : ∀ i, (G' i).natDegree = (G i).natDegree := by637    intro i638    rw [← (hG i).natDegree_map (IsLocalRing.residue O),639      ← (hG' i).natDegree_map (IsLocalRing.residue O), hred i]640  -- induction on the precision641  have key : ∀ t, t ≤ L → ∀ i j, pi ^ t ∣ (G' i).coeff j - (G i).coeff j := by642    intro t643    induction t with644    | zero => intro _ i j; simp645    | succ t ih =>646      intro htL647      have ih := ih (by omega)648      rcases t with _ | s649      · intro i j650        rw [zero_add, pow_one, ← hmem, ← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero]651        simpa [Polynomial.coeff_map] using congrArg (Polynomial.coeff · j) (hred i).symm652      choose H hHeq hHdeg using fun i =>653        (monic_congruent_difference_factor O pi hreg (s + 1) _ (G i) (G' i) (hG i) (hG' i) rfl654          (hdeg i) (fun j => Ideal.mem_span_singleton.2 (ih i j))).1655      have hcancel := (monic_congruent_difference_factor O pi hreg (s + 1) 0 1 1656        Polynomial.monic_one Polynomial.monic_one Polynomial.natDegree_one657        Polynomial.natDegree_one (fun j => by simp)).2658      set S : Polynomial O := ∑ i, H i * ∏ j ∈ Finset.univ.erase i, G j with hS659      have hexp := product_first_order_expansion (Polynomial O) ι660        (Ideal.span {Polynomial.C (pi ^ (s + 1))}) G (fun i => Polynomial.C (pi ^ (s + 1)) * H i)661        (fun i => Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)) Finset.univ662      rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hexp663      obtain ⟨R, hR⟩ := hexp664      have hprod : ∏ i, (G i + Polynomial.C (pi ^ (s + 1)) * H i) = ∏ i, G' i :=665        Finset.prod_congr rfl fun i _ => (sub_eq_iff_eq_add'.mp (hHeq i)).symm666      -- the first-order term vanishes modulo `pi`667      have hScoeff : ∀ j, pi ∣ S.coeff j := by668        intro j669        refine Ideal.mem_span_singleton.1 (hcancel _ (Ideal.mem_span_singleton.2 ?_))670        obtain ⟨r, hr⟩ := (pow_dvd_pow pi htL).trans ((hmpow _ _).1 (hp j))671        have hc := congrArg (Polynomial.coeff · j) hR672        simp only [hprod, mul_assoc, ← Finset.mul_sum, ← hS, Polynomial.coeff_sub,673          Polynomial.coeff_C_mul, ← map_pow] at hc674        exact ⟨-r - pi ^ s * R.coeff j, by linear_combination -hc - hr⟩675      have hzero := coprime_family_linear_injective (IsLocalRing.ResidueField O) ι676        (fun i => (G i).map (IsLocalRing.residue O)) (fun i => (hG i).map _) hc677        (fun i => (H i).map (IsLocalRing.residue O))678        (fun i => by rw [(hG i).natDegree_map]; exact Polynomial.degree_map_le.trans_lt (hHdeg i))679        (by680          have hSmap : S.map (IsLocalRing.residue O) = 0 := by681            ext j682            rw [Polynomial.coeff_map, Polynomial.coeff_zero, IsLocalRing.residue_eq_zero_iff, hmem]683            exact hScoeff j684          simpa only [hS, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_prod] using hSmap)685      intro i j686      obtain ⟨y, hy⟩ := (hmem ((H i).coeff j)).1 <| (IsLocalRing.residue_eq_zero_iff _).1 <| by687        rw [← Polynomial.coeff_map, hzero i, Polynomial.coeff_zero]688      exact ⟨y, by rw [← Polynomial.coeff_sub, hHeq i, Polynomial.coeff_C_mul, hy]; ring⟩689  intro i j690  rw [hmpow, ← neg_sub, dvd_neg]691  exact key L le_rfl i j692 693/-- Two monic polynomials of the same degree `n` agree in all coefficients of degree `≥ n`. -/694private theorem coeff_eq_of_monic_of_le {R : Type} [CommRing R] {n : ℕ} {P Q : Polynomial R}695    (hP : P.Monic) (hQ : Q.Monic) (hPn : P.natDegree = n) (hQn : Q.natDegree = n)696    {j : ℕ} (hj : n ≤ j) : P.coeff j = Q.coeff j := by697  rcases hj.eq_or_lt with rfl | hlt698  · have h1 := hP.coeff_natDegree699    have h2 := hQ.coeff_natDegree700    rw [hPn] at h1; rw [hQn] at h2; rw [h1, h2]701  · rw [Polynomial.coeff_eq_zero_of_natDegree_lt (by omega),702      Polynomial.coeff_eq_zero_of_natDegree_lt (by omega)]703 704/-- For monic polynomials of the same degree `N`, coefficientwise congruence modulo `I` below705degree `N` is equivalent to congruence of all coefficients. -/706theorem monic_coeff_sub_mem_iff {O : Type} [CommRing O] (I : Ideal O) (N : ℕ)707    (P Q : Polynomial O) (hP : P.Monic) (hQ : Q.Monic) (hPd : P.natDegree = N)708    (hQd : Q.natDegree = N) :709    (∀ j : Fin N, P.coeff j - Q.coeff j ∈ I) ↔ ∀ j, P.coeff j - Q.coeff j ∈ I := by710  refine ⟨fun h j => if hj : j < N then h ⟨j, hj⟩ else ?_, fun h j => h j⟩711  rw [coeff_eq_of_monic_of_le hP hQ hPd hQd (not_lt.mp hj), sub_self]712  exact I.zero_mem713 714/-- For factor families in the residue cells of pairwise coprime monic `g i`, the factor products715are congruent modulo `m^L` iff the families are. -/716theorem factor_product_congruence_iff (O : Type) [CommRing O] [IsDomain O]717    [IsDiscreteValuationRing O] (ι : Type) [Fintype ι]718    (g : ι → Polynomial (IsLocalRing.ResidueField O))719    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) (L : ℕ) (a a' : ∀ i, Fin (g i).natDegree → O)720    (ha : a ∈ Set.pi Set.univ (fun i => residueCell O (g i).natDegree (g i)))721    (ha' : a' ∈ Set.pi Set.univ (fun i => residueCell O (g i).natDegree (g i))) :722    (∀ j, factorProduct (fun i => (g i).natDegree) a j - factorProduct723        (fun i => (g i).natDegree) a' j ∈ (IsLocalRing.maximalIdeal O) ^ L) ↔ ∀ i j,724      a i j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L := by725  set I := (IsLocalRing.maximalIdeal O) ^ L726  set G : ι → Polynomial O := fun i => monicPolyO (a i)727  set G' : ι → Polynomial O := fun i => monicPolyO (a' i)728  have R := fun i => monic_poly_reconstruct O (g i).natDegree (a i)729  have R' := fun i => monic_poly_reconstruct O (g i).natDegree (a' i)730  have hGm : ∀ i, (G i).Monic := fun i => (R i).1731  have hG'm : ∀ i, (G' i).Monic := fun i => (R' i).1732  have hPm : (∏ i, G i).Monic := Polynomial.monic_prod_of_monic _ _ (fun i _ => hGm i)733  have hP'm : (∏ i, G' i).Monic := Polynomial.monic_prod_of_monic _ _ (fun i _ => hG'm i)734  have hPd : (∏ i, G i).natDegree = ∑ i, (g i).natDegree := by735    rw [Polynomial.natDegree_prod_of_monic _ _ (fun i _ => hGm i)]736    exact Finset.sum_congr rfl (fun i _ => (R i).2.1)737  have hP'd : (∏ i, G' i).natDegree = ∑ i, (g i).natDegree := by738    rw [Polynomial.natDegree_prod_of_monic _ _ (fun i _ => hG'm i)]739    exact Finset.sum_congr rfl (fun i _ => (R' i).2.1)740  have hfac : (∀ j, factorProduct (fun i => (g i).natDegree) a j741      - factorProduct (fun i => (g i).natDegree) a' j ∈ I) ↔742      ∀ j, (∏ i, G i).coeff j - (∏ i, G' i).coeff j ∈ I :=743    monic_coeff_sub_mem_iff I _ _ _ hPm hP'm hPd hP'd744  have hcomp : ∀ i, (∀ j, a i j - a' i j ∈ I) ↔ ∀ j, (G i).coeff j - (G' i).coeff j ∈ I := by745    intro i746    rw [← monic_coeff_sub_mem_iff I _ _ _ (hGm i) (hG'm i) (R i).2.1 (R' i).2.1]747    refine forall_congr' fun j => ?_748    rw [(R i).2.2.1 j, (R' i).2.2.1 j]749  rw [hfac]750  constructor751  · intro hp i752    rw [hcomp i]753    obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O754    have hm : IsLocalRing.maximalIdeal O = Ideal.span {pi} :=755      (IsDiscreteValuationRing.irreducible_iff_uniformizer pi).1 hpi756    have hred : ∀ i, (G i).map (IsLocalRing.residue O) = (G' i).map (IsLocalRing.residue O) :=757      fun i => (ha i (Set.mem_univ _)).trans (ha' i (Set.mem_univ _)).symm758    have hcG : ∀ i j, i ≠ j → IsCoprime ((G i).map (IsLocalRing.residue O))759        ((G j).map (IsLocalRing.residue O)) := by760      intro i j hij761      have e1 : (G i).map (IsLocalRing.residue O) = g i := ha i (Set.mem_univ _)762      have e2 : (G j).map (IsLocalRing.residue O) = g j := ha j (Set.mem_univ _)763      rw [e1, e2]; exact hc i j hij764    exact hensel_family_unique_mod_pow O ι pi hm765      (fun x hx => (mul_eq_zero.1 hx).resolve_left hpi.ne_zero) G G' hGm hG'm hred hcG L hp i766  · intro h767    exact (polynomial_congruence_and_product O I).2 ι G G' (fun i => (hcomp i).1 (h i))768 769/-- The projective normalizer evaluates to `1 + q + ⋯ + q^n`, and770`(1 + ⋯ + q^n)(q − 1) = q^(n+1) − 1`. -/771theorem projective_normalizer_eval (q : ℚ) (n : ℕ) :772    (projectiveNormalizer n).eval q = ∑ i ∈ Finset.range (n+1), q ^ i ∧773      (∑ i ∈ Finset.range (n+1), q ^ i) * (q - 1) = q ^ (n+1) - 1 := by774  have hpow : ∀ (x : Expr) (m : ℕ), (x.pow m).eval q = (x.eval q) ^ m := by775    intro x m776    induction m with777    | zero => simp [Expr.pow, Expr.eval]778    | succ m ih => simp [Expr.pow, Expr.eval, ih, pow_succ]779  have hsum : ∀ xs : List Expr, (Expr.sum xs).eval q = (xs.map (Expr.eval q)).sum := by780    intro xs781    induction xs with782    | nil => simp [Expr.sum, Expr.eval]783    | cons x xs ih =>784      simp only [Expr.sum, List.foldr_cons, Expr.eval, List.map_cons, List.sum_cons] at ih ⊢785      rw [ih]786  refine ⟨?_, geom_sum_mul q (n+1)⟩787  unfold projectiveNormalizer788  rw [hsum, List.map_map]789  have : (Expr.eval q ∘ fun i => Expr.pow Expr.var i) = fun i => q ^ i := by790    funext i; simp [hpow, Expr.eval]791  rw [this]792  simp [Finset.sum, Finset.range_val, Multiset.range]793 794/-- A residue cell is a congruence class modulo `m` around any of its points; it is nonempty iff795`G` is monic of degree `n`. -/796theorem residue_cell_cylinder (O : Type) [CommRing O] [IsLocalRing O] (n : ℕ)797    (G : Polynomial (IsLocalRing.ResidueField O)) :798    (∀ a ∈ residueCell O n G, residueCell O n G =799        {b | ∀ i, b i - a i ∈ IsLocalRing.maximalIdeal O}) ∧800      (G.Monic → G.natDegree = n → (residueCell O n G).Nonempty) ∧801      ((residueCell O n G).Nonempty → G.Monic ∧ G.natDegree = n) := by802  refine ⟨?_, ?_, ?_⟩803  · intro a ha804    ext b805    have hcong := (polynomial_congruence_and_product O (IsLocalRing.maximalIdeal O)).1806      (monicPolyO b) (monicPolyO a)807    obtain ⟨hma, hna, hca, -⟩ := monic_poly_reconstruct O n a808    obtain ⟨hmb, hnb, hcb, -⟩ := monic_poly_reconstruct O n b809    simp only [residueCell, Set.mem_ofPred_eq] at ha ⊢810    rw [← ha]811    change _ ↔ _ at hcong812    refine hcong.trans ⟨fun h i => ?_, fun h j => ?_⟩813    · have := h i; rwa [hca, hcb] at this814    · by_cases hj : j < n815      · have := h ⟨j, hj⟩; rw [← hca ⟨j, hj⟩, ← hcb ⟨j, hj⟩] at this; exact this816      · rw [coeff_eq_of_monic_of_le hmb hma hnb hna (by omega), sub_self]817        exact Ideal.zero_mem _818  · intro hG hGn819    choose a ha using fun i : Fin n => IsLocalRing.residue_surjective (G.coeff i)820    refine ⟨a, ?_⟩821    obtain ⟨hma, hna, hca, -⟩ := monic_poly_reconstruct O n a822    change (monicPolyO a).map (IsLocalRing.residue O) = G823    ext j824    by_cases hj : j < n825    · rw [Polynomial.coeff_map]826      have := hca ⟨j, hj⟩827      simp only at this828      rw [this, ha]829    · exact coeff_eq_of_monic_of_le (hma.map _) hG ((hma.natDegree_map _).trans hna) hGn830        (by omega)831  · rintro ⟨a, ha⟩832    obtain ⟨hma, hna, -, -⟩ := monic_poly_reconstruct O n a833    simp only [residueCell, Set.mem_ofPred_eq] at ha834    subst ha835    exact ⟨hma.map _, (hma.natDegree_map _).trans hna⟩836 837/-- A nonempty residue cell is measurable of mass `q^(-n)`, and its normalized cell measure is a838probability measure. -/839theorem residue_cell_mass (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 7.1840    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]841    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]842    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]843    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)844    (G : Polynomial (IsLocalRing.ResidueField O)) (hG : G.Monic) (hGn : G.natDegree = n) :845    MeasurableSet (residueCell O n G) ∧ coefficientMeasure O n (residueCell O n G) =846      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ n ∧ MeasureTheory.IsProbabilityMeasure847      (cellMeasure O n (residueCell O n G)) := by848  obtain ⟨hcyl, hne, -⟩ := SurfaceBlowup.residue_cell_cylinder O n G849  obtain ⟨a, ha⟩ := hne hG hGn850  have hS := hcyl a ha851  have hmeas : MeasurableSet (residueCell O n G) := by852    have e := SurfaceBlowup.finite_coordinate_borel_cylinders O (IsLocalRing.maximalIdeal O) htop n853    have h2 : @MeasurableSet _ (adicCylinderSpace (IsLocalRing.maximalIdeal O) (Fin n → O))854        (residueCell O n G) := by855      apply MeasurableSpace.measurableSet_generateFrom856      refine Or.inr ⟨1, a, ?_⟩857      rw [hS]858      ext b859      simp only [Set.mem_ofPred_eq]860      rw [SurfaceBlowup.finite_coordinate_adic_congruence]861      simp862    rwa [← e] at h2863  have hmass : coefficientMeasure O n (residueCell O n G)864      = (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ n := by865    rw [hS]866    have := SurfaceBlowup.coefficient_cylinder_mass O htop n 1 a867    simpa using this868  refine ⟨hmeas, hmass, ⟨?_⟩⟩869  have hq : (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) ≠ 0 := by870    have : 0 < Nat.card (IsLocalRing.ResidueField O) := Nat.card_pos871    exact_mod_cast this.ne'872  have h0 : coefficientMeasure O n (residueCell O n G) ≠ 0 := by873    rw [hmass]; exact pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))874  have htop' : coefficientMeasure O n (residueCell O n G) ≠ ⊤ := by875    rw [hmass]; exact ENNReal.pow_ne_top (ENNReal.inv_ne_top.2 hq)876  unfold cellMeasure877  rw [MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.restrict_apply MeasurableSet.univ,878    Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel h0 htop']879 880/-- The product of the normalized factor-cell measures is a probability measure concentrated on the881product of the cells, giving mass `q^(-(∑ deg g i)(L-1))` to each congruence box modulo `m^L`. -/882theorem factor_cell_product_measure (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]883    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]884    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]885    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]886    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (ι : Type) [Fintype ι]887    (g : ι → Polynomial (IsLocalRing.ResidueField O)) (hg : ∀ i, (g i).Monic)888    [hσ : ∀ i, MeasureTheory.SigmaFinite889      (cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i)))] :890    MeasureTheory.IsProbabilityMeasure891      (MeasureTheory.Measure.pi892        (fun i => cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i)))) ∧893      (MeasureTheory.Measure.pi894        (fun i => cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i))))895      (Set.pi Set.univ (fun i => residueCell O (g i).natDegree (g i)))ᶜ = 0 ∧ ∀ (L : ℕ), 1 ≤ L →896      ∀ a' ∈ Set.pi Set.univ (fun i => residueCell O (g i).natDegree (g i)),897      (MeasureTheory.Measure.pi898        (fun i => cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i))))899      (Set.pi Set.univ900        (fun i =>901          {b : Fin (g i).natDegree → O | ∀ j, b j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L})) =902      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ ((∑ i, (g i).natDegree) * (L - 1)) := by903  have hM := fun i => residue_cell_mass O htop (g i).natDegree (g i) (hg i) rfl904  have : ∀ i, MeasureTheory.IsProbabilityMeasure905      (cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i))) := fun i => (hM i).2.2906  set q : ℝ≥0∞ := (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) with hq907  have hq0 : q ≠ 0 := by908    rw [hq]; exact_mod_cast (Nat.card_pos (α := IsLocalRing.ResidueField O)).ne'909  have hqt : q ≠ ⊤ := by rw [hq]; exact ENNReal.natCast_ne_top _910  refine ⟨inferInstance, ?_, ?_⟩911  · have hmeas : MeasurableSet (Set.pi Set.univ (fun i => residueCell O (g i).natDegree (g i))) :=912      MeasurableSet.univ_pi (fun i => (hM i).1)913    rw [MeasureTheory.prob_compl_eq_zero_iff hmeas, MeasureTheory.Measure.pi_pi]914    refine Finset.prod_eq_one (fun i _ => ?_)915    have h1 := (hM i).1916    rw [← MeasureTheory.measure_univ917        (μ := cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i)))]918    unfold cellMeasure919    simp only [MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.restrict_apply' h1,920      Set.inter_self, Set.univ_inter]921  · intro L hL a' ha'922    rw [MeasureTheory.Measure.pi_pi]923    have key : ∀ i, cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i))924        {b : Fin (g i).natDegree → O | ∀ j, b j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L}925        = q⁻¹ ^ ((g i).natDegree * (L - 1)) := by926      intro i927      have h1 := (hM i).1928      have hsub :929          {b : Fin (g i).natDegree → O | ∀ j, b j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L}930          ⊆ residueCell O (g i).natDegree (g i) := by931        rw [(residue_cell_cylinder O (g i).natDegree (g i)).1 (a' i) (ha' i (Set.mem_univ _))]932        intro b hb j933        exact Ideal.pow_le_self (by omega) (hb j)934      unfold cellMeasure935      rw [MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.restrict_apply' h1,936        Set.inter_eq_left.mpr hsub, (hM i).2.1, coefficient_cylinder_mass O htop, smul_eq_mul]937      have : (g i).natDegree * L = (g i).natDegree + (g i).natDegree * (L - 1) := by938        obtain ⟨k, rfl⟩ : ∃ k, L = k + 1 := ⟨L - 1, by omega⟩939        simp [Nat.mul_succ, Nat.add_comm]940      rw [this, pow_add, ← mul_assoc, ENNReal.inv_mul_cancel, one_mul]941      · exact pow_ne_zero _ (ENNReal.inv_ne_zero.mpr hqt)942      · exact ENNReal.pow_ne_top (ENNReal.inv_ne_top.mpr hq0)943    simp only [key]944    rw [Finset.prod_pow_eq_pow_sum, Finset.sum_mul]945 946/-- The residue extension `O_δ / m_O O_δ` is isomorphic to `k[X]/(Φ̄)`, compatibly with947reduction. -/948theorem residue_extension_equiv (O : Type) [CommRing O] [IsLocalRing O] (Φ : Polynomial O) :949    ∃ e : residueExtension O Φ ≃+* AdjoinRoot (residuePoly O Φ),950      (∀ p : Polynomial O, e (baseReduce O Φ (AdjoinRoot.mk Φ p)) = AdjoinRoot.mk (residuePoly O Φ)951        (p.map (IsLocalRing.residue O))) ∧952      (∀ c : O, e (baseReduce O Φ (algebraMap O (AdjoinRoot Φ) c)) = algebraMap953        (IsLocalRing.ResidueField O) (AdjoinRoot (residuePoly O Φ)) (IsLocalRing.residue O c)) := by954  have h1 : ∀ p : Polynomial O,955      (AdjoinRoot.quotEquivQuotMap Φ (IsLocalRing.maximalIdeal O)).toRingEquiv956      (baseReduce O Φ (AdjoinRoot.mk Φ p)) = AdjoinRoot.mk (residuePoly O Φ)957          (p.map (IsLocalRing.residue O)) :=958    fun p => AdjoinRoot.quotEquivQuotMap_apply_mk Φ p (IsLocalRing.maximalIdeal O)959  refine ⟨(AdjoinRoot.quotEquivQuotMap Φ (IsLocalRing.maximalIdeal O)).toRingEquiv, h1, fun c => ?_⟩960  have := h1 (Polynomial.C c)961  rwa [AdjoinRoot.mk_C, Polynomial.map_C, AdjoinRoot.mk_C] at this962 963/-- For an unramified lift `Φ`, the residue extension is a finite field with `q^(deg Φ)`964elements. -/965theorem residue_extension_field (O : Type) [CommRing O] [IsLocalRing O]966    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :967    IsField (residueExtension O Φ) ∧ Finite (residueExtension O Φ) ∧ Nat.card968      (residueExtension O Φ) = residueCard O ^ Φ.natDegree := by969  obtain ⟨e, -, -⟩ := SurfaceBlowup.residue_extension_equiv O Φ970  have : Fact (Irreducible (residuePoly O Φ)) := ⟨hΦ.2⟩971  have hm : (residuePoly O Φ).Monic := hΦ.1.map _972  have hdeg : (residuePoly O Φ).natDegree = Φ.natDegree := hΦ.1.natDegree_map _973  let pb := AdjoinRoot.powerBasis' hm974  let f : residueExtension O Φ ≃ (Fin (residuePoly O Φ).natDegree → IsLocalRing.ResidueField O) :=975    e.toEquiv.trans pb.basis.equivFun.toEquiv976  refine ⟨?_, Finite.of_equiv _ f.symm, ?_⟩977  · exact MulEquiv.isField (Field.toIsField _) e.toMulEquiv978  · rw [Nat.card_congr f, Nat.card_fun, Nat.card_eq_fintype_card (α := Fin _), Fintype.card_fin,979      hdeg]980 981open Polynomial in982/-- Translation `X ↦ X + θ` maps the block cell bijectively onto the `X^r` cell and preserves983congruences modulo powers of `m_O O_δ`. -/984theorem block_translation (O : Type) [CommRing O] [IsLocalRing O]985    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]986    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r : ℕ) :987    Set.BijOn (translateBlock O Φ r) (blockCell O Φ r) (zeroCell O Φ r) ∧988      (∀ (L : ℕ) (b b' : Fin r → AdjoinRoot Φ), (∀ j, b j - b' j ∈ (baseIdeal O Φ) ^ L) ↔ ∀ j,989        translateBlock O Φ r b j - translateBlock O Φ r b' j ∈ (baseIdeal O Φ) ^ L) := by990  set A := AdjoinRoot Φ991  have : Nontrivial (residueExtension O Φ) := ⟨(residue_extension_field O Φ hΦ).1.exists_pair_ne⟩992  have : Nontrivial A := (baseReduce O Φ).domain_nontrivial993  set θ := AdjoinRoot.root Φ994  have R := fun (a : Fin r → A) => monic_poly_reconstruct A r a995  -- translated polynomial996  have hT : ∀ b : Fin r → A, monicPolyO (translateBlock O Φ r b) = taylor θ (monicPolyO b) := by997    intro b998    obtain ⟨h1, h2, -, -⟩ := R b999    exact (R b).2.2.2 _ (by rw [Monic, leadingCoeff_taylor]; exact h1)1000        (by rw [natDegree_taylor, h2])1001  -- coefficient congruence criterion1002  have key : ∀ (J : Ideal A) (c c' : Fin r → A),1003      (∀ j, c j - c' j ∈ J) ↔ monicPolyO c - monicPolyO c' ∈ J.map (C : A →+* A[X]) := by1004    intro J c c'1005    obtain ⟨m1, d1, e1, -⟩ := R c1006    obtain ⟨m2, d2, e2, -⟩ := R c'1007    rw [Ideal.mem_map_C_iff]1008    constructor1009    · intro h n1010      rw [coeff_sub]1011      by_cases hn : n < r1012      · have := h ⟨n, hn⟩1013        rwa [← e1 ⟨n, hn⟩, ← e2 ⟨n, hn⟩] at this1014      · rw [coeff_eq_of_monic_of_le m1 m2 d1 d2 (not_lt.mp hn), sub_self]; exact J.zero_mem1015    · intro h j1016      have := h j1017      rwa [coeff_sub, e1, e2] at this1018  have tmem : ∀ (J : Ideal A) (s : A) (f : A[X]), f ∈ J.map (C : A →+* A[X]) →1019      taylor s f ∈ J.map (C : A →+* A[X]) := by1020    intro J s f hf1021    have : ((taylorAlgHom s : A[X] →ₐ[A] A[X]) : A[X] →+* A[X]).comp C = C := by1022      ext x1023      · simp [taylor_C]1024      · simp1025    have h2 := Ideal.mem_map_of_mem ((taylorAlgHom s : A[X] →ₐ[A] A[X]) : A[X] →+* A[X]) hf1026    rw [Ideal.map_map, this] at h21027    simpa using h21028  have hinv : ∀ f : A[X], taylor (-θ) (taylor θ f) = f := by1029    intro f; rw [taylor_taylor, neg_add_cancel, taylor_zero]1030  have hinv' : ∀ f : A[X], taylor θ (taylor (-θ) f) = f := by1031    intro f; rw [taylor_taylor, add_neg_cancel, taylor_zero]1032  have hcf : conjugateFactor O Φ 0 = X - C (baseReduce O Φ θ) := by1033    simp [conjugateFactor, rootBar, θ]1034  refine ⟨⟨?_, ?_, ?_⟩, ?_⟩1035  · intro b hb1036    change (monicPolyO _).map _ = _1037    change (monicPolyO b).map _ = _ at hb1038    rw [hT, map_taylor, hb, hcf, taylor_pow, sub_eq_add_neg, ← C_neg]1039    simp [taylor_X, taylor_C]1040  · intro b _ b' _ h1041    have h1 : monicPolyO b = monicPolyO b' := by1042      apply taylor_injective θ1043      rw [← hT, ← hT, h]1044    funext j1045    rw [← (R b).2.2.1 j, ← (R b').2.2.1 j, h1]1046  · intro c hc1047    change (monicPolyO c).map _ = _ at hc1048    set F := taylor (-θ) (monicPolyO c)1049    obtain ⟨m1, d1, -, -⟩ := R c1050    have hF := (R c).2.2.2 F (by rw [Monic, leadingCoeff_taylor]; exact m1)1051      (by rw [natDegree_taylor, d1])1052    have hF' : monicPolyO (coeffVec r F) = F := (R (coeffVec r F)).2.2.2 F1053      (by rw [Monic, leadingCoeff_taylor]; exact m1) (by rw [natDegree_taylor, d1])1054    refine ⟨coeffVec r F, ?_, ?_⟩1055    · change (monicPolyO _).map _ = _1056      rw [hF', map_taylor, hc, hcf, taylor_pow, sub_eq_add_neg, ← C_neg]1057      simp [taylor_X]1058    · have := hT (coeffVec r F)1059      rw [hF', hinv'] at this1060      funext j1061      rw [← (R (translateBlock O Φ r (coeffVec r F))).2.2.1 j, this, (R c).2.2.1 j]1062  · intro L b b'1063    rw [key, key, hT, hT, ← map_sub]1064    constructor1065    · exact tmem _ θ _1066    · intro h1067      have := tmem _ (-θ) _ h1068      rwa [hinv] at this1069 1070private theorem pow_natCard_eq_self (K : Type) [CommRing K] (hK : IsField K) [Finite K] (x : K) :1071    x ^ Nat.card K = x := by1072  let := hK.toField1073  cases nonempty_fintype K1074  rw [Nat.card_eq_fintype_card]1075  exact FiniteField.pow_card x1076 1077private theorem natCard_le_of_pow_eq_self (K : Type) [CommRing K] (hK : IsField K) [Finite K]1078    (n : ℕ) (hn : 1 < n)1079    (hall : ∀ x : K, x ^ n = x) : Nat.card K ≤ n := by1080  let := hK.toField1081  cases nonempty_fintype K1082  have hsub : (Finset.univ : Finset K).val ⊆1083      (Polynomial.X ^ n - Polynomial.X : Polynomial K).roots := by1084    intro x _1085    rw [Polynomial.mem_roots (FiniteField.X_pow_card_sub_X_ne_zero K hn)]1086    simp [hall x]1087  have := Polynomial.card_le_degree_of_subset_roots hsub1088  rw [FiniteField.X_pow_card_sub_X_natDegree_eq K hn, Finset.card_univ] at this1089  rwa [Nat.card_eq_fintype_card]1090 1091private theorem monic_eq_prod_X_sub_C (K : Type) [CommRing K] (hK : IsField K) (p : Polynomial K)1092    (hp : p.Monic) (d : ℕ)1093    (hd : p.natDegree = d) (r : Fin d → K) (hr : Function.Injective r)1094    (hroot : ∀ i, p.IsRoot (r i)) :1095    p = ∏ i, (Polynomial.X - Polynomial.C (r i)) ∧ ∀ i j, i ≠ j → IsCoprime1096      (Polynomial.X - Polynomial.C (r i)) (Polynomial.X - Polynomial.C (r j)) := by1097  classical1098  let := hK.toField1099  refine ⟨?_, fun i j hij => Polynomial.pairwise_coprime_X_sub_C hr hij⟩1100  set s := Finset.univ.image r1101  have hs : s.card = d := by1102    rw [Finset.card_image_of_injective _ hr, Finset.card_univ, Fintype.card_fin]1103  have hle : s.val ≤ p.roots := by1104    rw [Multiset.le_iff_subset s.nodup]1105    intro x hx1106    obtain ⟨i, _, rfl⟩ := Finset.mem_image.1 (Finset.mem_val.mp hx)1107    exact (Polynomial.mem_roots hp.ne_zero).2 (hroot i)1108  have heq : s.val = p.roots :=1109    Multiset.eq_of_le_of_card_le hle1110        (by rw [Finset.card_val, hs, ← hd]; exact Polynomial.card_roots' p)1111  have hcard : Multiset.card p.roots = p.natDegree := by1112    rw [← heq, Finset.card_val, hs, hd]1113  rw [← Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq hp hcard, ← heq]1114  rw [← Finset.prod_eq_multiset_prod, Finset.prod_image (fun a _ b _ h => hr h)]1115 1116 1117/-- The residue roots `θ̄^(q^i)`, `i < deg Φ`, are pairwise distinct roots of `Φ̄` in `k_δ`, so `Φ̄`1118splits there as the product of the pairwise coprime conjugate factors. -/1119theorem conjugate_roots_distinct (O : Type) [CommRing O] [IsLocalRing O]1120    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]1121    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :1122    (∀ c : O, residueEmbed O Φ (IsLocalRing.residue O c) = baseReduce O Φ1123        (algebraMap O (AdjoinRoot Φ) c)) ∧ Function.Injective (residueEmbed O Φ) ∧1124      (∀ i : ℕ, ((residuePoly O Φ).map (residueEmbed O Φ)).IsRoot (rootBar O Φ ^ residueCard O ^ i))1125      ∧ (∀ i j : ℕ, i < Φ.natDegree → j < Φ.natDegree → rootBar O Φ ^ residueCard O ^ i =1126        rootBar O Φ ^ residueCard O ^ j → i = j) ∧ (residuePoly O Φ).map (residueEmbed O Φ) = ∏ i :1127      Fin Φ.natDegree, conjugateFactor O Φ i ∧1128      (∀ i j : Fin Φ.natDegree, i ≠ j → IsCoprime (conjugateFactor O Φ i) (conjugateFactor O Φ j))1129      := by1130  obtain ⟨hKf, hKfin, hKcard⟩ := residue_extension_field O Φ hΦ1131  set K := residueExtension O Φ1132  set q := residueCard O1133  set δ := Φ.natDegree1134  set ρ := residueEmbed O Φ1135  set θ := rootBar O Φ1136  -- compatibility1137  have hcomp : ∀ c : O, ρ (IsLocalRing.residue O c) = baseReduce O Φ1138      (algebraMap O (AdjoinRoot Φ) c) :=1139    fun c => rfl1140  have hcompR : ρ.comp (IsLocalRing.residue O) = (baseReduce O Φ).comp (AdjoinRoot.of Φ) :=1141    RingHom.ext hcomp1142  -- iterated Frobenius1143  have hiter : ∀ (P : Polynomial (IsLocalRing.ResidueField O)) (y : K) (n : ℕ),1144      P.eval₂ ρ (y ^ q ^ n) = (P.eval₂ ρ y) ^ q ^ n := by1145    intro P y n1146    induction n with1147    | zero => simp1148    | succ n ih =>1149      rw [pow_succ, pow_mul, pow_mul, eval_at_pow_card, ih]1150  -- every element is a polynomial expression in θ1151  have hsurj : ∀ x : K, ∃ P : Polynomial (IsLocalRing.ResidueField O), x = P.eval₂ ρ θ := by1152    intro x1153    obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x1154    induction a using AdjoinRoot.induction_on with1155    | ih p =>1156      refine ⟨p.map (IsLocalRing.residue O), ?_⟩1157      rw [Polynomial.eval₂_map, hcompR, ← AdjoinRoot.aeval_eq, Polynomial.aeval_def,1158        Polynomial.hom_eval₂]1159      rfl1160  have hq : 1 < q := Finite.one_lt_card1161  have hroot : ∀ i : ℕ, ((residuePoly O Φ).map ρ).IsRoot (θ ^ q ^ i) := by1162    intro i1163    rw [Polynomial.IsRoot.def, Polynomial.eval_map, hiter]1164    have : (residuePoly O Φ).eval₂ ρ θ = 0 := by1165      rw [Polynomial.eval₂_map, hcompR, ← Polynomial.hom_eval₂, AdjoinRoot.eval₂_root, map_zero]1166    rw [this, zero_pow (pow_ne_zero _ (by omega))]1167  have hθδ : θ ^ q ^ δ = θ := by rw [← hKcard]; exact pow_natCard_eq_self K hKf θ1168  have hdist : ∀ i j : ℕ, i < δ → j < δ → θ ^ q ^ i = θ ^ q ^ j → i = j := by1169    have key : ∀ i j : ℕ, i < j → j < δ → θ ^ q ^ i = θ ^ q ^ j → False := by1170      intro i j hij hj h1171      set m := i + (δ - j) with hm1172      have h1 : θ ^ q ^ m = θ := by1173        have := congrArg (· ^ q ^ (δ - j)) h1174        simp only [← pow_mul, ← pow_add] at this1175        rw [hm, this, show j + (δ - j) = δ by omega, hθδ]1176      have hall : ∀ x : K, x ^ q ^ m = x := by1177        intro x1178        obtain ⟨P, rfl⟩ := hsurj x1179        rw [← hiter, h1]1180      have hm1 : 1 < q ^ m := Nat.one_lt_pow (by omega) hq1181      have := natCard_le_of_pow_eq_self K hKf _ hm1 hall1182      rw [hKcard] at this1183      have := (Nat.pow_le_pow_iff_right hq).1 this1184      omega1185    intro i j hi hj h1186    by_contra hne1187    rcases Nat.lt_or_gt_of_ne hne with hij | hij1188    exacts [key i j hij hj h, key j i hij hi h.symm]1189  have hnt : Nontrivial K := ⟨hKf.exists_pair_ne⟩1190  have hmon : ((residuePoly O Φ).map ρ).Monic := (hΦ.1.map _).map _1191  have hdeg : ((residuePoly O Φ).map ρ).natDegree = δ := by1192    rw [(hΦ.1.map _).natDegree_map, hΦ.1.natDegree_map]1193  have hinj : Function.Injective (fun i : Fin δ => θ ^ q ^ (i : ℕ)) :=1194    fun i j h => Fin.ext (hdist i j i.2 j.2 h)1195  obtain ⟨hfac, hcop⟩ := monic_eq_prod_X_sub_C K hKf _ hmon δ hdeg _ hinj (fun i => hroot i)1196  exact ⟨hcomp, ρ.injective, hroot, hdist, hfac, hcop⟩1197 1198/-- Each fiber of the residue map on `O^(n+1)` is measurable of mass `q^(-(n+1))`. -/1199theorem residue_vector_fiber_mass (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1200    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]1201    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]1202    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1203    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)1204    (w : Fin (n + 1) → IsLocalRing.ResidueField O) :1205    MeasurableSet {a : Fin (n+1) → O | residueVector O a = w} ∧ coefficientMeasure O (n+1)1206      {a : Fin (n+1) → O | residueVector O a = w} =1207      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (n+1) := by1208  choose a₀ ha₀ using fun i => IsLocalRing.residue_surjective (w i)1209  have hset : {a : Fin (n+1) → O | residueVector O a = w}1210      = {b | ∀ i, b i - a₀ i ∈ (IsLocalRing.maximalIdeal O) ^ 1} := by1211    ext a1212    simp only [Set.mem_ofPred_eq, pow_one, residueVector, funext_iff, ← ha₀]1213    refine forall_congr' fun i => ?_1214    exact Ideal.Quotient.eq1215  refine ⟨?_, ?_⟩1216  · have hm := finite_coordinate_borel_cylinders O (IsLocalRing.maximalIdeal O) htop (n+1)1217    change @MeasurableSet _ (inferInstance : MeasurableSpace (Fin (n+1) → O)) _1218    rw [hm, hset]1219    apply MeasurableSpace.measurableSet_generateFrom1220    right1221    refine ⟨1, a₀, ?_⟩1222    ext b1223    exact (finite_coordinate_adic_congruence O (n+1) _ 1 b a₀).symm1224  · rw [hset, coefficient_cylinder_mass O htop (n+1) 1 a₀, mul_one]1225 1226/-- The nonzero scalar multiples of a nonzero vector over a finite field `k` form a finite set of1227`|k| − 1` nonzero vectors. -/1228theorem scalar_class_card (k : Type) [Field k] [Finite k] (n : ℕ) (v : Fin (n + 1) → k)1229    (hv : v ≠ 0) :1230    Nat.card (scalarClass v) = Nat.card k - 1 ∧ (∀ w ∈ scalarClass v, w ≠ 0) ∧1231      (scalarClass v).Finite := by1232  classical1233  obtain ⟨i, hi⟩ := Function.ne_iff.mp hv1234  refine ⟨?_, ?_, Set.toFinite _⟩1235  · let f : {c : k // c ≠ 0} → scalarClass v := fun c => ⟨c.1 • v, c.1, c.2, rfl⟩1236    have hf : Function.Bijective f := by1237      constructor1238      · intro a b h1239        have h2 := congrFun (congrArg Subtype.val h) i1240        simp only [f, Pi.smul_apply, smul_eq_mul] at h21241        exact Subtype.ext (mul_right_cancel₀ hi h2)1242      · rintro ⟨w, c, hc, rfl⟩1243        exact ⟨⟨c, hc⟩, rfl⟩1244    rw [← Nat.card_congr (Equiv.ofBijective f hf)]1245    have := Fintype.ofFinite k1246    rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, Fintype.card_subtype_compl,1247      Fintype.card_subtype_eq]1248  · rintro w ⟨c, hc, rfl⟩ h1249    exact hv ((smul_eq_zero.mp h).resolve_left hc)1250 1251end SurfaceBlowup