Binary forms, factor cells and 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.Measure.HenselProducts7 8/-!9# Binary forms, factor cells and unramified extensions10 11Basic definitions for the factorization-type analysis: binary forms and their products, the12residue, projective and normalized factor cells, the unramified extension `O_δ = O[X]/(Φ)` with13its Frobenius, and the Frobenius descent maps. Alongside, the algebraic toolkit used throughout:14adic completeness under change of ideal and for finite free modules, lifting idempotents,15locality criteria, coordinates of `m_O O_δ`, coprimality via residues, Hensel uniqueness for16families of factors, partial fractions for coprime binary forms, and descent of Frobenius orbits17of irreducible factors.18 19## Main results20 21* `SurfaceBlowup.base_ideal_coordinates`, `SurfaceBlowup.base_ideal_pure`22* `SurfaceBlowup.finite_free_adic_complete`, `SurfaceBlowup.complete_domain_finite_quotient_local`23* `SurfaceBlowup.coprime_of_coprime_residue_dvr`, `SurfaceBlowup.hensel_family_unique`24* `SurfaceBlowup.form_product_maps_to_and_preserves`, `SurfaceBlowup.forms_linear_bijective`25* `SurfaceBlowup.invariant_orbit_factors`26 27Provenance: `Def_SurfaceBlowupV2_{BinaryForms, FactorCells, ProjectiveCells, HomogeneousCells,28UnramifiedExtension, FrobeniusDescent}`; `Thm_SurfaceBlowupV2_{adic_complete_iff_of_pow_le,29adic_idempotent_lift, base_ideal_coordinates, base_ideal_pure,30conjugate_irreducible_factors_distinct, coprime_family_linear_injective,31coprime_of_coprime_residue_dvr, distinct_monic_irreducible_coprime,32dvr_extension_maximalIdeal_map_eq_pow, dvr_maximalIdeal_pow_injective, eval_at_pow_card,33factor_product_continuous, finite_field_frobenius_fixed_points, finite_free_adic_complete,34finite_free_residue_quotient, finite_monoid_idempotent_power, finite_ring_local_of_idempotents,35complete_domain_finite_quotient_local, form_product_maps_to_and_preserves, forms_linear_injective,36forms_linear_bijective, hensel_factor_unique_of_dvd, hensel_family_unique, invariant_orbit_factors,37local_algEquiv_maximalIdeal}`.38-/39 40noncomputable section41 42namespace SurfaceBlowup43 44open Polynomial IsLocalRing MeasureTheory45 46/-! ### Binary forms -/47 48section49variable {A : Type} [CommRing A]50/-- The dehomogenized polynomial `∑ a_i X^i` of a degree-`n` binary form with coefficient vector51`a` (the form is `∑ a_i X^i Y^(n-i)`; the multiplicity of its zero at infinity is `n − deg`). -/52def formPoly {n : ℕ} (a : Fin (n + 1) → A) : Polynomial A :=53  ∑ i : Fin (n+1), C (a i) * X ^ (i : ℕ)54/-- Product of a finite family of binary forms of degrees `d i`, as a form of degree `∑ d i`. -/55def formProd {ι : Type} [Fintype ι] (d : ι → ℕ) (a : ∀ i, Fin (d i + 1) → A) :56    Fin ((∑ i, d i) + 1) → A :=57  fun j => (∏ i, formPoly (a i)).coeff j58/-- Pairwise coprimality of a family of binary forms over a field: the dehomogenized polynomials59are pairwise coprime (no common affine zero) and at most one form vanishes at infinity (has60dehomogenized degree below its form degree). -/61def FormsCoprime {ι : Type} [Fintype ι] (d : ι → ℕ) (g : ∀ i, Fin (d i + 1) → A) : Prop :=62  (∀ i j, i ≠ j → IsCoprime (formPoly (g i)) (formPoly (g j))) ∧63    ∀ i j, i ≠ j → (formPoly (g i)).natDegree = d i ∨ (formPoly (g j)).natDegree = d j64end65 66/-! ### Factor cells -/67 68section69variable {O : Type} [CommRing O]70/-- The integral monic polynomial `X^n + ∑ a_i X^i` attached to a coefficient vector. -/71def monicPolyO {n : ℕ} (a : Fin n → O) : Polynomial O :=72  X ^ n + ∑ i : Fin n, C (a i) * X ^ (i : ℕ)73/-- The first `n` coefficients of a polynomial, as a coefficient vector. -/74def coeffVec (n : ℕ) (F : Polynomial O) : Fin n → O := fun i => F.coeff i75/-- Coefficient vector of the product of the monic polynomials attached to a family of vectors. -/76def factorProduct {ι : Type} [Fintype ι] (d : ι → ℕ) (a : ∀ i, Fin (d i) → O) :77    Fin (∑ i, d i) → O :=78  coeffVec (∑ i, d i) (∏ i, monicPolyO (a i))79end80/-- The integral monic polynomial maps to the fraction-field monic polynomial `monicPolynomial`. -/81theorem monicPolyO_map_fraction (O : Type) [CommRing O] [IsDomain O] {n : ℕ} (a : Fin n → O) :82    (monicPolyO a).map (algebraMap O (BaseField O)) = monicPolynomial O a := by83  simp [monicPolyO, monicPolynomial, Polynomial.map_sum]84section85variable (O : Type) [CommRing O] [IsLocalRing O]86/-- The residue cell: coefficient vectors whose monic polynomial reduces to `G`. -/87def residueCell (n : ℕ) (G : Polynomial (ResidueField O)) : Set (Fin n → O) :=88  {a | (monicPolyO a).map (residue O) = G}89end90section91variable (O : Type) [CommRing O] [IsDomain O]92  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]93  [SecondCountableTopology O]94  [MeasurableSpace O] [BorelSpace O]95/-- The normalized coefficient measure of a cell: restriction of `coefficientMeasure` to `S`,96divided by the mass of `S` (junk when the mass is `0` or `∞`; probability otherwise). -/97noncomputable def cellMeasure (n : ℕ) (S : Set (Fin n → O)) : Measure (Fin n → O) :=98  (coefficientMeasure O n S)⁻¹ • (coefficientMeasure O n).restrict S99end100 101/-! ### Projective cells -/102 103section104variable {k : Type} [CommRing k]105/-- The nonzero scalar multiples of a coefficient vector. -/106def scalarClass {n : ℕ} (v : Fin (n + 1) → k) : Set (Fin (n+1) → k) :=107  {w | ∃ c : k, c ≠ 0 ∧ w = c • v}108end109section110variable (O : Type) [CommRing O] [IsLocalRing O]111/-- Coordinatewise reduction of a binary coefficient vector to the residue field. -/112def residueVector {n : ℕ} (a : Fin (n + 1) → O) : Fin (n+1) → ResidueField O :=113  fun i => residue O (a i)114/-- The projective residue cell of `v`: primitive vectors whose reduction is a nonzero scalar115multiple of `v`. -/116def projectiveCell (n : ℕ) (v : Fin (n + 1) → ResidueField O) : Set (Fin (n+1) → O) :=117  {a | primitive O a ∧ residueVector O a ∈ scalarClass v}118end119 120/-! ### Normalized (homogeneous) cells -/121 122section123variable {A : Type} [CommRing A]124/-- Insert the value `1` at coordinate `ν`: the form with normalized `ν`-coefficient and free125coefficients `b`. -/126def insertOne {d : ℕ} (ν : Fin (d + 1)) (b : Fin d → A) : Fin (d+1) → A := Fin.insertNth ν 1 b127/-- Forget coordinate `μ`. -/128def dropCoord {d : ℕ} (μ : Fin (d + 1)) (a : Fin (d + 1) → A) : Fin d → A := Fin.removeNth μ a129/-- Scale a form by the inverse of its `μ`-coordinate (`Ring.inverse`: junk `0` if that coordinate130is not a unit). -/131def normalizeAt {d : ℕ} (μ : Fin (d + 1)) (a : Fin (d + 1) → A) : Fin (d+1) → A :=132  Ring.inverse (a μ) • a133end134section135variable (O : Type) [CommRing O] [IsLocalRing O]136/-- Normalized factor cell: forms with `ν`-coordinate `1` reducing to the residue form `g` (so137`g ν = 1` if nonempty). -/138def normalizedFormCell (d : ℕ) (ν : Fin (d + 1)) (g : Fin (d + 1) → ResidueField O) :139    Set (Fin (d+1) → O) :=140  {a | a ν = 1 ∧ residueVector O a = g}141/-- The same cell in the `d` free coordinates. -/142def reducedFormCell (d : ℕ) (ν : Fin (d + 1)) (g : Fin (d + 1) → ResidueField O) :143    Set (Fin d → O) :=144  {b | insertOne ν b ∈ normalizedFormCell O d ν g}145open scoped Classical in146/-- The normalized product map in reduced coordinates: multiply the normalized factors, divide by147the `μ`-coordinate of the product, forget coordinate `μ`. Guarded by membership in the product of148the factor cells (junk `0` outside), so that measurability needs no continuity of inversion. -/149def reducedFormProduct {ι : Type} [Fintype ι] (d : ι → ℕ) (ν : ∀ i, Fin (d i + 1))150    (g : ∀ i, Fin (d i + 1) → ResidueField O) (μ : Fin ((∑ i, d i) + 1))151    (a : ∀ i, Fin (d i) → O) : Fin (∑ i, d i) → O :=152  if ∀ i, a i ∈ reducedFormCell O (d i) (ν i) (g i) then153    dropCoord μ (normalizeAt μ (formProd d (fun i => insertOne (ν i) (a i)))) else 0154open scoped Classical in155/-- Normalization of a primitive form in the projective chart `μ`, in reduced coordinates (junk `0`156off the projective residue cell of `G`). -/157def projectiveNormalize (n : ℕ) (G : Fin (n + 1) → ResidueField O) (μ : Fin (n + 1))158    (a : Fin (n + 1) → O) : Fin n → O :=159  if a ∈ projectiveCell O n G then dropCoord μ (normalizeAt μ a) else 0160end161 162/-! ### The unramified extension and its Frobenius -/163 164section165variable (O : Type) [CommRing O] [IsLocalRing O]166/-- Number of elements of the residue field of `O` (written q throughout). -/167abbrev residueCard : ℕ := Nat.card (ResidueField O)168/-- Reduction of an integral polynomial to the residue field. -/169abbrev residuePoly (Φ : Polynomial O) : Polynomial (ResidueField O) := Φ.map (residue O)170/-- `Φ` is a monic polynomial over `O` whose reduction is irreducible over the residue field. -/171def IsUnramifiedLift (Φ : Polynomial O) : Prop := Φ.Monic ∧ Irreducible (residuePoly O Φ)172/-- The ideal `m_O · O_δ` generated by the maximal ideal of the base, in `O_δ := O[X]/(Φ)`. -/173def baseIdeal (Φ : Polynomial O) : Ideal (AdjoinRoot Φ) := (maximalIdeal O).map (AdjoinRoot.of Φ)174/-- The residue extension `k_δ := O_δ / m_O O_δ`. -/175abbrev residueExtension (Φ : Polynomial O) : Type := AdjoinRoot Φ ⧸ baseIdeal O Φ176/-- Reduction of `O_δ` to its residue extension. -/177abbrev baseReduce (Φ : Polynomial O) : AdjoinRoot Φ →+* residueExtension O Φ :=178  Ideal.Quotient.mk (baseIdeal O Φ)179open scoped Classical in180/-- The Frobenius root: the root of `Φ` in `O_δ` congruent to `θ^q` modulo `m_O O_δ` when such a181root exists, and `θ` itself otherwise. Existence and uniqueness are theorems, not part of the182data. -/183noncomputable def frobeniusRoot (Φ : Polynomial O) : AdjoinRoot Φ :=184  if h : ∃ a : AdjoinRoot Φ, (Φ.map (AdjoinRoot.of Φ)).IsRoot a ∧185      a - (AdjoinRoot.root Φ) ^ residueCard O ∈ baseIdeal O Φ186  then Classical.choose h else AdjoinRoot.root Φ187/-- Both branches of `frobeniusRoot` are roots of `Φ`; this makes the Frobenius a genuine algebra188map. -/189private theorem frobeniusRoot_eval₂ (Φ : Polynomial O) :190    Φ.eval₂ (AdjoinRoot.of Φ) (frobeniusRoot O Φ) = 0 := by191  unfold frobeniusRoot192  split_ifs with h193  · simpa [Polynomial.IsRoot, Polynomial.eval_map] using (Classical.choose_spec h).1194  · exact AdjoinRoot.eval₂_root Φ195/-- The Frobenius `O`-algebra endomorphism of `O_δ`, sending `θ` to the Frobenius root. -/196noncomputable def unramifiedFrobenius (Φ : Polynomial O) : AdjoinRoot Φ →ₐ[O] AdjoinRoot Φ :=197  AdjoinRoot.liftAlgHom Φ (Algebra.ofId O (AdjoinRoot Φ)) (frobeniusRoot O Φ)198    (frobeniusRoot_eval₂ O Φ)199/-- Iterates `σ^i` of the Frobenius, defined by recursion so that no monoid structure on200endomorphisms is needed. -/201noncomputable def frobeniusIter (Φ : Polynomial O) : ℕ → (AdjoinRoot Φ →ₐ[O] AdjoinRoot Φ)202  | 0 => AlgHom.id O (AdjoinRoot Φ)203  | i+1 => (unramifiedFrobenius O Φ).comp (frobeniusIter Φ i)204end205 206/-! ### Frobenius descent -/207 208section209variable (O : Type) [CommRing O] [IsLocalRing O] (Φ : Polynomial O)210/-- The residue embedding `k → k_δ` induced by `O → O_δ`. -/211noncomputable def residueEmbed : ResidueField O →+* residueExtension O Φ :=212  Ideal.quotientMap (I := maximalIdeal O) (baseIdeal O Φ) (AdjoinRoot.of Φ)213    (Ideal.map_le_iff_le_comap.mp le_rfl)214/-- The reduction `θ̄` of the root `θ` to `k_δ`. -/215abbrev rootBar : residueExtension O Φ := baseReduce O Φ (AdjoinRoot.root Φ)216/-- The linear residue factor `X − θ̄^(q^i)` above the `i`-th conjugate root. -/217noncomputable def conjugateFactor (i : ℕ) : Polynomial (residueExtension O Φ) :=218  X - C (rootBar O Φ ^ residueCard O ^ i)219/-- Block cell: coefficient vectors over `O_δ` whose monic polynomial reduces to `(X − θ̄)^r`. -/220def blockCell (r : ℕ) : Set (Fin r → AdjoinRoot Φ) :=221  {b | (monicPolyO b).map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r}222/-- The `X^r` cell over `O_δ`: coefficient vectors whose monic polynomial reduces to `X^r`. -/223def zeroCell (r : ℕ) : Set (Fin r → AdjoinRoot Φ) :=224  {b | (monicPolyO b).map (baseReduce O Φ) = X ^ r}225/-- The product of the `δ` Frobenius conjugates `B^(σ^i)`, `i < δ = deg Φ`. -/226noncomputable def conjugateProduct (B : Polynomial (AdjoinRoot Φ)) : Polynomial (AdjoinRoot Φ) :=227  ∏ i : Fin Φ.natDegree, B.map (frobeniusIter O Φ i).toRingHom228open scoped Classical in229/-- The element of `O` mapping to `x` when one exists, and `0` otherwise. -/230noncomputable def descendCoeff (x : AdjoinRoot Φ) : O :=231  if h : ∃ c : O, algebraMap O (AdjoinRoot Φ) c = x then Classical.choose h else 0232/-- Descent map: a block over `O_δ` goes to the `O`-coefficient vector of its conjugate233product. -/234noncomputable def descendBlock (r : ℕ) (b : Fin r → AdjoinRoot Φ) : Fin (Φ.natDegree * r) → O :=235  fun j => descendCoeff O Φ ((conjugateProduct O Φ (monicPolyO b)).coeff j)236open scoped Classical in237/-- Block selection: the monic degree-`r` divisor over `O_δ` of the lifted polynomial that reduces238to `(X − θ̄)^r`, when one exists (uniqueness is a theorem); `0` otherwise. -/239noncomputable def selectBlock (r : ℕ) (a : Fin (Φ.natDegree * r) → O) : Fin r → AdjoinRoot Φ :=240  if h : ∃ B : Polynomial (AdjoinRoot Φ), B.Monic ∧ B.natDegree = r ∧241      B.map (baseReduce O Φ) = conjugateFactor O Φ 0 ^ r ∧242      B ∣ (monicPolyO a).map (AdjoinRoot.of Φ)243  then coeffVec r (Classical.choose h) else 0244/-- Translation `X ↦ X + θ` on coefficient vectors over `O_δ`. -/245noncomputable def translateBlock (r : ℕ) (b : Fin r → AdjoinRoot Φ) : Fin r → AdjoinRoot Φ :=246  coeffVec r (Polynomial.taylor (AdjoinRoot.root Φ) (monicPolyO b))247end248 249/-! ### Commutative algebra toolkit -/250 251/-- If `J^k ≤ I ≤ J`, then a module is `I`-adically complete iff it is `J`-adically complete. -/252theorem adic_complete_iff_of_pow_le (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]253    (I J : Ideal R) (k : ℕ) (h1 : J ^ k ≤ I) (h2 : I ≤ J) :254    IsAdicComplete I M ↔ IsAdicComplete J M := by255  set φ : ℕ → ℕ := fun n => max 1 k * n256  have hle : ∀ n, n ≤ φ n := fun n => Nat.le_mul_of_pos_left n (by omega)257  have hmono : ∀ {m n : ℕ}, m ≤ n → φ m ≤ φ n := fun h => Nat.mul_le_mul_left _ h258  have hIJ : ∀ n, (I ^ n • ⊤ : Submodule R M) ≤ J ^ n • ⊤ :=259    fun n => Submodule.smul_mono_left (Ideal.pow_right_mono h2 n)260  have hJI : ∀ n, (J ^ φ n • ⊤ : Submodule R M) ≤ I ^ n • ⊤ := by261    intro n262    apply Submodule.smul_mono_left263    calc J ^ φ n ≤ J ^ (k * n) := Ideal.pow_le_pow_right (Nat.mul_le_mul_right _ (le_max_right _ _))264      _ = (J ^ k) ^ n := pow_mul _ _ _265      _ ≤ I ^ n := Ideal.pow_right_mono h1 n266  constructor267  · intro hI268    refine { haus' := ?_, prec' := ?_ }269    · exact fun x hx => hI.haus' x fun n => SModEq.mono (hJI n) (hx (φ n))270    · intro f hf271      obtain ⟨L, hL⟩ := hI.prec' (fun n => f (φ n))272        (fun {m n} h => SModEq.mono (hJI m) (hf (hmono h)))273      exact ⟨L, fun n => (hf (hle n)).trans (SModEq.mono (hIJ n) (hL n))⟩274  · intro hJ275    refine { haus' := ?_, prec' := ?_ }276    · exact fun x hx => hJ.haus' x fun n => SModEq.mono (hIJ n) (hx n)277    · intro f hf278      obtain ⟨L, hL⟩ := hJ.prec' f (fun {m n} h => SModEq.mono (hIJ m) (hf h))279      exact ⟨L, fun n => (hf (hle n)).trans (SModEq.mono (hJI n) (hL (φ n)))⟩280 281/-- Idempotents lift along `A → A/I` when `A` is `I`-adically complete (Hensel applied to282`X² − X`). -/283private theorem adic_idempotent_lift (A : Type) [CommRing A] (I : Ideal A) [IsAdicComplete I A]284    (e : A ⧸ I)285    (he : e * e = e) :286    ∃ x : A, x*x=x ∧ Ideal.Quotient.mk I x = e := by287  obtain ⟨x0, rfl⟩ := Ideal.Quotient.mk_surjective e288  have hmon : (X ^ 2 - X : A[X]).Monic := by289    simpa using monic_X_pow_sub (R := A) (p := X) (n := 2)290      (degree_X_le.trans_lt (by exact_mod_cast (by norm_num : 1 < 2)))291  have h1 : (X ^ 2 - X : A[X]).eval x0 ∈ I := by292    rw [← Ideal.Quotient.eq_zero_iff_mem]293    simp [sq, he]294  have h2 : IsUnit (Ideal.Quotient.mk I ((X ^ 2 - X : A[X]).derivative.eval x0)) := by295    refine IsUnit.of_mul_eq_one (Ideal.Quotient.mk I ((X ^ 2 - X : A[X]).derivative.eval x0)) ?_296    simp only [derivative_X_pow, derivative_X, eval_sub, eval_mul, eval_pow,297      eval_X, eval_one, eval_natCast, map_sub, map_mul, map_pow, map_one, map_natCast]298    norm_num299    linear_combination (4 : A ⧸ I) * he300  obtain ⟨a, ha, hax⟩ := HenselianRing.is_henselian _ hmon x0 h1 h2301  refine ⟨a, ?_, ?_⟩302  · have := ha.eq_zero303    simp only [eval_sub, eval_pow, eval_X] at this304    linear_combination this305  · exact Ideal.Quotient.eq.mpr hax306 307/-- Membership in `J • ⊤` is read off coordinatewise in a finite basis. -/308private theorem mem_smul_top_iff_repr {R M ι : Type} [CommRing R] [AddCommGroup M] [Module R M]309    [Finite ι] (b : Module.Basis ι R M) (J : Ideal R) (x : M) :310    x ∈ (J • ⊤ : Submodule R M) ↔ ∀ i, b.repr x i ∈ J := by311  have := Fintype.ofFinite ι312  refine ⟨fun hx => Submodule.smul_induction_on hx313    (fun r hr m _ i => by simpa using J.mul_mem_right _ hr)314    (fun x y hx hy i => by simpa using J.add_mem (hx i) (hy i)), fun h => ?_⟩315  rw [← b.sum_repr x]316  exact Submodule.sum_mem _ fun i _ => Submodule.smul_mem_smul (h i) trivial317 318/-- An element of `O[X]/(Φ)` lies in `(m_O O_δ)^L` iff all its coordinates in the power basis319lie in `m_O^L`. -/320theorem base_ideal_coordinates (O : Type) [CommRing O] [IsLocalRing O] (Φ : Polynomial O)321    (hΦ : Φ.Monic) (L : ℕ) (x : AdjoinRoot Φ) :322    x ∈ (baseIdeal O Φ)^L ↔ ∀ i, (AdjoinRoot.powerBasis' hΦ).basis.repr x i ∈323      (IsLocalRing.maximalIdeal O)^L := by324  rw [← mem_smul_top_iff_repr, Ideal.smul_top_eq_map, Submodule.restrictScalars_mem, baseIdeal,325    ← Ideal.map_pow, AdjoinRoot.algebraMap_eq]326 327/-- A base element `c ∈ O` lies in `(m_O O_δ)^L` iff `c ∈ m_O^L` (for `Φ` monic of positive328degree). -/329theorem base_ideal_pure (O : Type) [CommRing O] [IsLocalRing O] (Φ : Polynomial O) (hΦ : Φ.Monic)330    (hdeg : 0 < Φ.natDegree) (L : ℕ) (c : O) :331    algebraMap O (AdjoinRoot Φ) c ∈ (baseIdeal O Φ)^L ↔ c ∈ (IsLocalRing.maximalIdeal O)^L := by332  rw [SurfaceBlowup.base_ideal_coordinates O Φ hΦ L]333  set b := AdjoinRoot.powerBasis' hΦ334  have h0 : 0 < b.dim := by simpa [b] using hdeg335  have hb : b.basis ⟨0, h0⟩ = 1 := by336    rw [PowerBasis.coe_basis]; simp337  have hrepr : b.basis.repr (algebraMap O (AdjoinRoot Φ) c) = Finsupp.single ⟨0, h0⟩ c := by338    rw [Algebra.algebraMap_eq_smul_one, ← hb, map_smul, Module.Basis.repr_self,339      Finsupp.smul_single, smul_eq_mul, mul_one]340  rw [hrepr]341  constructor342  · intro h; simpa using h ⟨0, h0⟩343  · intro h i344    by_cases hi : i = ⟨0, h0⟩345    · subst hi; simpa using h346    · rw [Finsupp.single_apply, if_neg (Ne.symm hi)]; exact zero_mem _347 348/-- Frobenius conjugates of the distinct monic irreducible factors of `F` over `Frac O_δ` are349monic irreducible and pairwise distinct, and they factor each conjugate of `F` and the350conjugate product of `F`. -/351private theorem conjugate_irreducible_factors_distinct (O : Type) [CommRing O] [IsDomain O]352    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]353    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) [IsDomain (AdjoinRoot Φ)]354    (τ : ℕ → (BaseField (AdjoinRoot Φ) ≃+* BaseField (AdjoinRoot Φ)))355    (hτ : ∀ (i : ℕ) (x : AdjoinRoot Φ), τ i356      (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) x) = algebraMap (AdjoinRoot Φ)357      (BaseField (AdjoinRoot Φ)) (frobeniusIter O Φ i x)) (F : Polynomial (AdjoinRoot Φ))358    (gs : List (Polynomial (BaseField (AdjoinRoot Φ))))359    (hgs : ∀ g ∈ gs, g.Monic ∧ Irreducible g) (hd : gs.Pairwise (fun g h => g ≠ h))360    (hprod : F.map (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) = gs.prod)361    (hcop : ∀ i j : Fin Φ.natDegree, i ≠ j → IsCoprime362      ((fun i : Fin Φ.natDegree => (F.map (frobeniusIter O Φ i).toRingHom).map363          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) i)364      ((fun i : Fin Φ.natDegree => (F.map (frobeniusIter O Φ i).toRingHom).map365          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) j)) :366    (∀ (i : ℕ) (g : Polynomial (BaseField (AdjoinRoot Φ))), g.Monic → Irreducible g →367        (g.map (τ i).toRingHom).Monic ∧ Irreducible (g.map (τ i).toRingHom)) ∧368      (∀ (i j : Fin Φ.natDegree) (a b : Fin gs.length), (gs.get a).map (τ i).toRingHom =369        (gs.get b).map (τ j).toRingHom → i = j ∧ a = b) ∧370      (∀ i : Fin Φ.natDegree,371        (fun i : Fin Φ.natDegree => (F.map (frobeniusIter O Φ i).toRingHom).map372          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) i =373        (gs.map (Polynomial.map (τ i).toRingHom)).prod) ∧ (conjugateProduct O Φ F).map374      (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) = ∏ i : Fin Φ.natDegree,375      (gs.map (Polynomial.map (τ i).toRingHom)).prod := by376  set L := algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) with hL377  have key : ∀ (i : ℕ) (P : Polynomial (AdjoinRoot Φ)),378      (P.map (frobeniusIter O Φ i).toRingHom).map L = (P.map L).map (τ i).toRingHom := by379    intro i P380    rw [Polynomial.map_map, Polynomial.map_map]381    congr 1382    exact RingHom.ext fun x => (hτ i x).symm383  have c1 : ∀ (i : ℕ) (g : Polynomial (BaseField (AdjoinRoot Φ))), g.Monic → Irreducible g →384      (g.map (τ i).toRingHom).Monic ∧ Irreducible (g.map (τ i).toRingHom) := by385    intro i g hm hi386    exact ⟨hm.map _, by simpa using (MulEquiv.irreducible_iff (mapEquiv (τ i)).toMulEquiv).mpr hi⟩387  have c3 : ∀ i : Fin Φ.natDegree, (F.map (frobeniusIter O Φ i).toRingHom).map L388      = (gs.map (Polynomial.map (τ i).toRingHom)).prod := fun i => by389    rw [key, hprod, Polynomial.map_list_prod]390  refine ⟨c1, ?_, c3, ?_⟩391  · intro i j a b hab392    have hmem : ∀ (k : Fin Φ.natDegree) (c : Fin gs.length),393        (gs.get c).map (τ k).toRingHom ∣ (F.map (frobeniusIter O Φ k).toRingHom).map L := by394      intro k c395      rw [c3]396      exact List.dvd_prod (List.mem_map.mpr ⟨_, List.get_mem _ _, rfl⟩)397    have hirr := (c1 i (gs.get a) (hgs _ (List.get_mem gs a)).1 (hgs _ (List.get_mem gs a)).2).2398    have hij : i = j := by399      by_contra hne400      apply hirr.not_isUnit401      exact (hcop i j hne).isUnit_of_dvd' (hmem i a) (hab ▸ hmem j b)402    subst hij403    exact ⟨rfl, (List.Nodup.get_inj_iff hd).mp (Polynomial.map_injective _ (τ i).injective hab)⟩404  · rw [conjugateProduct, Polynomial.map_prod]405    exact Finset.prod_congr rfl fun i _ => c3 i406 407open scoped Classical in408/-- For pairwise coprime monic `g i` over a field, `∑ h i ∏_{j ≠ i} g j = 0` with409`deg h i < deg g i` forces all `h i = 0`. -/410theorem coprime_family_linear_injective (k ι : Type) [Field k] [Fintype ι] (g : ι → Polynomial k)411    (hg : ∀ i, (g i).Monic) (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) (h : ι → Polynomial k)412    (hdeg : ∀ i, (h i).degree < ((g i).natDegree : WithBot ℕ))413    (hsum : ∑ i, h i * ∏ j ∈ Finset.univ.erase i, g j = 0) :414    ∀ i, h i = 0 := by415  intro i416  have hrest : g i ∣ ∑ l ∈ Finset.univ.erase i, h l * ∏ j ∈ Finset.univ.erase l, g j := by417    apply Finset.dvd_sum418    intro l hl419    have hil : i ∈ Finset.univ.erase l :=420      Finset.mem_erase.mpr ⟨fun e => (Finset.mem_erase.mp hl).1 e.symm, Finset.mem_univ _⟩421    exact Dvd.dvd.mul_left (Finset.dvd_prod_of_mem _ hil) _422  have hsplit := Finset.add_sum_erase Finset.univ423    (fun l => h l * ∏ j ∈ Finset.univ.erase l, g j) (Finset.mem_univ i)424  rw [hsum] at hsplit425  have hmain : g i ∣ h i * ∏ j ∈ Finset.univ.erase i, g j := by426    have : h i * ∏ j ∈ Finset.univ.erase i, g j427        = -∑ l ∈ Finset.univ.erase i, h l * ∏ j ∈ Finset.univ.erase l, g j := by428      rw [eq_neg_iff_add_eq_zero]; exact hsplit429    rw [this]; exact (dvd_neg).mpr hrest430  have hcop : IsCoprime (g i) (∏ j ∈ Finset.univ.erase i, g j) :=431    IsCoprime.prod_right fun j hj => hc i j (Finset.mem_erase.mp hj).1.symm432  have hd : g i ∣ h i := hcop.dvd_of_dvd_mul_right hmain433  apply Polynomial.eq_zero_of_dvd_of_degree_lt hd434  rw [Polynomial.degree_eq_natDegree (hg i).ne_zero]435  exact hdeg i436 437/-- Monic polynomials over a local ring `R` with coprime reductions stay coprime over any438`R`-algebra `K` (classically: the fraction field of a DVR). -/439theorem coprime_of_coprime_residue_dvr (R K : Type) [CommRing R] [IsLocalRing R] [CommRing K]440    [Algebra R K] (A B : Polynomial R) (hA : A.Monic) (hB : B.Monic)441    (hc : IsCoprime (A.map (IsLocalRing.residue R)) (B.map (IsLocalRing.residue R))) :442    IsCoprime (A.map (algebraMap R K)) (B.map (algebraMap R K)) :=443  (isCoprime_of_isCoprime_map_residue hA hB hc).map (Polynomial.mapRingHom (algebraMap R K))444 445/-- Distinct monic irreducible polynomials over a field are coprime. -/446theorem distinct_monic_irreducible_coprime (K : Type) [Field K] (g h : Polynomial K) (hg : g.Monic)447    (hh : h.Monic) (hgi : Irreducible g) (hhi : Irreducible h) (hne : g ≠ h) :448    IsCoprime g h := by449  rw [hgi.coprime_iff_not_dvd]450  intro hd451  exact hne (Polynomial.eq_of_monic_of_associated hg hh (hgi.associated_of_dvd hhi hd))452 453/-- For an integral injective extension of DVRs `O → B`, `m_O B = m_B^e` with `e` the454ramification index. -/455theorem dvr_extension_maximalIdeal_map_eq_pow (O B : Type) [CommRing O] [IsDomain O]456    [IsDiscreteValuationRing O] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra O B]457    [Algebra.IsIntegral O B] (hinj : Function.Injective (algebraMap O B)) :458    (IsLocalRing.maximalIdeal O).map (algebraMap O B) =459      (IsLocalRing.maximalIdeal B)^((IsLocalRing.maximalIdeal B).ramificationIdx O) := by460  set p := IsLocalRing.maximalIdeal O461  set q := IsLocalRing.maximalIdeal B462  have hcomap : q.comap (algebraMap O B) = p :=463    IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal q)464  have : q.LiesOver p := ⟨hcomap.symm⟩465  have hp : p ≠ ⊥ := IsDiscreteValuationRing.not_a_field O466  have hq : q ≠ ⊥ := IsDiscreteValuationRing.not_a_field B467  have hp0 : p.map (algebraMap O B) ≠ ⊥ := by468    rwa [Ne, Ideal.map_eq_bot_iff_of_injective hinj]469  obtain ⟨k, hk⟩ : ∃ k : ℕ, p.map (algebraMap O B) = q ^ k := by470    obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible B471    obtain ⟨k, hk⟩ := IsDiscreteValuationRing.ideal_eq_span_pow_irreducible hp0 hϖ472    refine ⟨k, ?_⟩473    rw [hk, show q = Ideal.span {ϖ} from474      (IsDiscreteValuationRing.irreducible_iff_uniformizer ϖ).mp hϖ, Ideal.span_singleton_pow]475  have hprime : Prime q := Ideal.prime_of_isPrime hq inferInstance476  have he : q.ramificationIdx O = k := by477    rw [Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count p q hp0, hk,478      UniqueFactorizationMonoid.normalizedFactors_pow,479      UniqueFactorizationMonoid.normalizedFactors_irreducible hprime.irreducible, normalize_eq,480      Multiset.count_nsmul, Multiset.count_singleton_self, mul_one]481  rw [he, hk]482 483/-- In a DVR, `n ↦ m^n` is injective. -/484theorem dvr_maximalIdeal_pow_injective (B : Type) [CommRing B] [IsDomain B]485    [IsDiscreteValuationRing B] (a b : ℕ)486    (h : (IsLocalRing.maximalIdeal B) ^ a = (IsLocalRing.maximalIdeal B) ^ b) :487    a = b := by488  have h0 : IsLocalRing.maximalIdeal B ≠ ⊥ := by489    intro h0490    exact IsDiscreteValuationRing.not_isField B ((IsLocalRing.isField_iff_maximalIdeal_eq).2 h0)491  have h1 : IsLocalRing.maximalIdeal B ≠ ⊤ := (IsLocalRing.maximalIdeal.isMaximal B).ne_top492  exact (Ideal.pow_right_strictAnti _ h0 h1).injective h493 494/-- Over a finite field `k` with `q` elements, `P(y^q) = P(y)^q` for `P ∈ k[X]`. -/495theorem eval_at_pow_card (k K : Type) [Field k] [Finite k] [CommRing K] (ρ : k →+* K)496    (P : Polynomial k) (y : K) :497    P.eval₂ ρ (y ^ Nat.card k) = (P.eval₂ ρ y) ^ Nat.card k := by498  cases nonempty_fintype k499  rw [Nat.card_eq_fintype_card, Polynomial.eval₂_eq_eval_map, Polynomial.eval₂_eq_eval_map,500    ← Polynomial.expand_eval, ← Polynomial.map_expand, FiniteField.expand_card,501    Polynomial.map_pow, Polynomial.eval_pow]502 503/-- The factor product map (coefficients of a product of monic polynomials) is continuous and504measurable. -/505theorem factor_product_continuous (O : Type) [CommRing O] [TopologicalSpace O] [IsTopologicalRing O]506    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] (ι : Type) [Fintype ι]507    (d : ι → ℕ) :508    Continuous (fun a : (∀ i, Fin (d i) → O) => factorProduct d a) ∧ Measurable509      (fun a : (∀ i, Fin (d i) → O) => factorProduct d a) := by510  have key := Finset.prod_induction (s := Finset.univ)511    (fun i (a : ∀ i, Fin (d i) → O) => monicPolyO (a i))512    (fun P => ∀ j, Continuous fun a => (P a).coeff j)513    (fun P Q hP hQ j => by514      simpa [coeff_mul] using continuous_finsetSum _ fun p _ => (hP p.1).mul (hQ p.2))515    (fun j => by simpa using continuous_const) fun i _ m => by516      simp only [monicPolyO, coeff_add, finsetSum_coeff, coeff_C_mul_X_pow]517      refine continuous_const.add (continuous_finsetSum _ fun k _ => ?_)518      split_ifs <;> fun_prop519  simp only [Finset.prod_apply] at key520  have hc : Continuous fun a => factorProduct d a := continuous_pi fun j => key j521  exact ⟨hc, hc.measurable⟩522 523/-- For a finite field `k ↪ K`, the solutions of `x^q = x` in the field `K` are exactly the image524of `k`. -/525theorem finite_field_frobenius_fixed_points (k K : Type) [Field k] [Finite k] [Field K]526    (ρ : k →+* K) (x : K) :527    x ^ Nat.card k = x ↔ x ∈ Set.range ρ := by528  classical529  cases nonempty_fintype k530  rw [Nat.card_eq_fintype_card]531  set q := Fintype.card k with hq532  have hq1 : 1 < q := Fintype.one_lt_card533  have himg : ∀ c : k, (ρ c) ^ q = ρ c := by534    intro c; rw [← map_pow, FiniteField.pow_card]535  constructor536  · intro hx537    set P : Polynomial K := Polynomial.X ^ q - Polynomial.X with hP538    have hP0 : P ≠ 0 := FiniteField.X_pow_card_sub_X_ne_zero K hq1539    have hdeg : P.natDegree = q := FiniteField.X_pow_card_sub_X_natDegree_eq K hq1540    have hmem : ∀ y : K, y ^ q = y → y ∈ P.roots.toFinset := by541      intro y hy542      rw [Multiset.mem_toFinset, Polynomial.mem_roots hP0]543      simp [hP, Polynomial.IsRoot, hy]544    have hsub : Finset.univ.image ρ ⊆ P.roots.toFinset := by545      intro y hy546      obtain ⟨c, -, rfl⟩ := Finset.mem_image.mp hy547      exact hmem _ (himg c)548    have hcard : P.roots.toFinset.card ≤ (Finset.univ.image ρ).card := by549      rw [Finset.card_image_of_injective _ ρ.injective, Finset.card_univ]550      calc P.roots.toFinset.card ≤ Multiset.card P.roots := Multiset.toFinset_card_le _551        _ ≤ P.natDegree := Polynomial.card_roots' P552        _ = q := hdeg553    have heq := Finset.eq_of_subset_of_card_le hsub hcard554    have : x ∈ Finset.univ.image ρ := heq ▸ hmem x hx555    obtain ⟨c, -, hc⟩ := Finset.mem_image.mp this556    exact ⟨c, hc⟩557  · rintro ⟨c, rfl⟩558    exact himg c559 560/-- A finite free module over an `I`-adically complete ring is `I`-adically complete. -/561theorem finite_free_adic_complete (O M : Type) [CommRing O] [AddCommGroup M] [Module O M]562    [Module.Finite O M] [Module.Free O M] (I : Ideal O) [IsAdicComplete I O] :563    IsAdicComplete I M := by564  let b := Module.Free.chooseBasis O M565  have key := mem_smul_top_iff_repr b566  have keyO : ∀ (J : Ideal O) (x : O), x ∈ (J • ⊤ : Submodule O O) ↔ x ∈ J := by567    intro J x568    rw [smul_eq_mul, Ideal.mul_top]569  have hM : ∀ (n : ℕ) (x y : M), x ≡ y [SMOD (I ^ n • ⊤ : Submodule O M)] ↔570      ∀ i, b.repr x i ≡ b.repr y i [SMOD (I ^ n • ⊤ : Submodule O O)] := by571    intro n x y572    simp only [SModEq.sub_mem, key, keyO, map_sub, Finsupp.sub_apply]573  refine { haus' := ?_, prec' := ?_ }574  · intro x hx575    apply b.repr.injective576    ext i577    have := IsHausdorff.haus (I := I) (M := O) inferInstance (b.repr x i) fun n =>578      by simpa using (hM n x 0).1 (hx n) i579    simpa using this580  · intro f hf581    have hc : ∀ i, ∃ L : O, ∀ n, b.repr (f n) i ≡ L [SMOD (I ^ n • ⊤ : Submodule O O)] :=582      fun i => IsPrecomplete.prec (I := I) inferInstance fun {m n} hmn => (hM m _ _).1 (hf hmn) i583    choose L hL using hc584    refine ⟨∑ i, L i • b i, fun n => (hM n _ _).2 fun i => ?_⟩585    simpa [Finsupp.single_apply] using hL i n586 587/-- If `O/I` is finite, then so is `M/IM` for a finite free `O`-module `M`. -/588theorem finite_free_residue_quotient (O M : Type) [CommRing O] [AddCommGroup M] [Module O M]589    [Module.Finite O M] [Module.Free O M] (I : Ideal O) [Finite (O ⧸ I)] :590    Finite (M ⧸ (I • ⊤ : Submodule O M)) := by591  have : Module.Finite (O ⧸ I) (M ⧸ (I • ⊤ : Submodule O M)) :=592    Module.Finite.of_restrictScalars_finite O _ _593  exact Module.finite_of_finite (O ⧸ I)594 595/-- Every element of a finite monoid has a positive power that is idempotent. -/596private theorem finite_monoid_idempotent_power (A : Type) [Monoid A] [Finite A] (a : A) :597    ∃ n : ℕ, 0 < n ∧ a^n * a^n = a^n := by598  have key : ∃ i p : ℕ, 0 < p ∧ a^(i+p) = a^i := by599    obtain ⟨x, y, hxy, h⟩ := Finite.exists_ne_map_eq_of_infinite (fun n : ℕ => a^n)600    rcases lt_or_gt_of_ne hxy with hlt | hlt601    · exact ⟨x, y - x, by omega, by rw [Nat.add_sub_cancel' hlt.le]; exact h.symm⟩602    · exact ⟨y, x - y, by omega, by rw [Nat.add_sub_cancel' hlt.le]; exact h⟩603  obtain ⟨i, p, hp, h⟩ := key604  have per : ∀ m k : ℕ, i ≤ k → a^(k + m*p) = a^k := by605    intro m606    induction m with607    | zero => intro k _; simp608    | succ m ih =>609      intro k hk610      have e : k + (m+1)*p = (k - i) + (i + p) + m*p := by611        rw [Nat.add_mul]; omega612      rw [e, pow_add, pow_add, h, ← pow_add, Nat.sub_add_cancel hk, ← pow_add, ih k hk]613  refine ⟨p*(i+1), Nat.mul_pos hp (Nat.succ_pos _), ?_⟩614  rw [← pow_add]615  have := per (i+1) (p*(i+1)) (by nlinarith)616  rwa [Nat.mul_comm (i+1) p] at this617 618/-- A nontrivial finite commutative ring whose only idempotents are `0, 1` is local. -/619private theorem finite_ring_local_of_idempotents (A : Type) [CommRing A] [Nontrivial A] [Finite A]620    (he : ∀ e : A, e*e=e → e=0 ∨ e=1) :621    IsLocalRing A := by622  refine ⟨fun {a b} hab => ?_⟩623  obtain ⟨n, hn, hidem⟩ := finite_monoid_idempotent_power A a624  rcases he _ hidem with h | h625  · exact Or.inr (eq_sub_of_add_eq' hab ▸ IsNilpotent.isUnit_one_sub ⟨n, h⟩)626  · exact Or.inl (IsUnit.of_pow_eq_one h hn.ne')627 628/-- A domain that is `I`-adically complete with `A/I` finite is local. -/629theorem complete_domain_finite_quotient_local (A : Type) [CommRing A] [IsDomain A] (I : Ideal A)630    [IsAdicComplete I A] [Finite (A ⧸ I)] :631    IsLocalRing A := by632  have hjac : I ≤ (⊥ : Ideal A).jacobson := IsAdicComplete.le_jacobson_bot I633  have hI : I ≠ ⊤ := by634    intro h635    have : (⊥ : Ideal A).jacobson = ⊤ := top_le_iff.mp (h ▸ hjac)636    exact bot_ne_top (Ideal.jacobson_eq_top_iff.mp this)637  have : Nontrivial (A ⧸ I) := Ideal.Quotient.nontrivial_iff.mpr hI638  have : IsLocalRing (A ⧸ I) := by639    apply SurfaceBlowup.finite_ring_local_of_idempotents640    intro e he641    obtain ⟨x, hx, rfl⟩ := SurfaceBlowup.adic_idempotent_lift A I e he642    have : x * (x - 1) = 0 := by rw [mul_sub, hx]; ring643    rcases mul_eq_zero.mp this with h | h644    · left; simp [h]645    · right; rw [sub_eq_zero.mp h, map_one]646  have := isLocalHom_of_le_jacobson_bot I hjac647  refine IsLocalRing.of_isUnit_or_isUnit_one_sub_self fun a => ?_648  rcases IsLocalRing.isUnit_or_isUnit_one_sub_self (Ideal.Quotient.mk I a) with h | h649  · left; exact isUnit_of_map_unit _ _ h650  · right; exact isUnit_of_map_unit (Ideal.Quotient.mk I) _ (by simpa using h)651 652/-! ### Coefficients of binary forms -/653 654section FormPolyLemmas655 656variable {A : Type} [CommRing A] {n : ℕ}657 658private theorem coeff_formPoly (a : Fin (n + 1) → A) (j : Fin (n + 1)) :659    (formPoly a).coeff (j : ℕ) = a j := by660  simp [formPoly, finsetSum_coeff, coeff_X_pow, Fin.val_inj]661 662private theorem natDegree_formPoly_le (a : Fin (n + 1) → A) : (formPoly a).natDegree ≤ n :=663  natDegree_sum_le_of_forall_le _ _ fun i _ =>664    (natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.mp i.2)665 666private theorem formPoly_eq_zero (a : Fin (n + 1) → A) (h : formPoly a = 0) : a = 0 :=667  funext fun j => by rw [← coeff_formPoly a j, h, coeff_zero, Pi.zero_apply]668 669/-- `formPoly` is additive. -/670theorem formPoly_add (a b : Fin (n + 1) → A) :671    formPoly (a + b) = formPoly a + formPoly b := by672  simp [formPoly, add_mul, Finset.sum_add_distrib]673 674private theorem formPoly_C_smul (c : A) (a : Fin (n + 1) → A) :675    formPoly (c • a) = C c * formPoly a := by676  simp [formPoly, Finset.mul_sum, mul_assoc]677 678private theorem formProd_map {B : Type} [CommRing B] (f : A →+* B) {ι : Type} [Fintype ι]679    (d : ι → ℕ) (a : ∀ i, Fin (d i + 1) → A) (j : Fin ((∑ i, d i) + 1)) :680    f (formProd d a j) = formProd d (fun i k => f (a i k)) j := by681  have h1 : ∀ i, formPoly (fun k => f (a i k)) = (formPoly (a i)).map f := fun i => by682    simp [formPoly, Polynomial.map_sum]683  simp only [formProd, h1, ← Polynomial.map_prod, Polynomial.coeff_map]684 685end FormPolyLemmas686 687/-- The normalized product of factor cells lands in the product cell, has the expected688reduction and unit `μ`-coordinate, and preserves congruences modulo `m^L`. -/689theorem form_product_maps_to_and_preserves (O : Type) [CommRing O] [IsLocalRing O] (ι : Type)690    [Fintype ι] (d : ι → ℕ) (ν : ∀ i, Fin (d i + 1))691    (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O)692    (μ : Fin ((∑ i, d i) + 1)) (hμ : formProd d g μ = 1)693    (a a' : ∀ i, Fin (d i) → O)694    (ha : a ∈ Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i)))695    (ha' : a' ∈ Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i))) :696    reducedFormProduct O d ν g μ a ∈ reducedFormCell O (∑ i, d i) μ (formProd d g) ∧697      residueVector O (formProd d (fun i => insertOne (ν i) (a i))) = formProd d g ∧ IsUnit698      (formProd d (fun i => insertOne (ν i) (a i)) μ) ∧ ∀ L : ℕ,699      (∀ i j, a i j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L) → ∀ j,700      reducedFormProduct O d ν g μ a j - reducedFormProduct O d ν g μ a' j ∈701      (IsLocalRing.maximalIdeal O) ^ L := by702  set S := Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i))703  have hres : ∀ b ∈ S,704      residueVector O (formProd d (fun i => insertOne (ν i) (b i))) = formProd d g := by705    intro b hb706    funext j707    simp only [residueVector]708    rw [formProd_map]709    exact congrArg (fun G => formProd d G j) (funext fun i => (Set.mem_univ_pi.mp hb i).2)710  have hunit : ∀ b ∈ S, IsUnit (formProd d (fun i => insertOne (ν i) (b i)) μ) := by711    intro b hb712    have h : IsLocalRing.residue O (formProd d (fun i => insertOne (ν i) (b i)) μ) = 1 := by713      rw [← hμ]; exact congrFun (hres b hb) μ714    apply IsLocalRing.notMem_maximalIdeal.mp715    intro hm716    rw [← IsLocalRing.residue_eq_zero_iff, h] at hm717    exact one_ne_zero hm718  have hguard : ∀ b ∈ S, reducedFormProduct O d ν g μ b =719      dropCoord μ (normalizeAt μ (formProd d (fun i => insertOne (ν i) (b i)))) :=720    fun b hb => if_pos fun i => Set.mem_univ_pi.mp hb i721  refine ⟨?_, hres a ha, hunit a ha, ?_⟩722  · rw [hguard a ha]723    have hu := hunit a ha724    set P := formProd d (fun i => insertOne (ν i) (a i)) with hP725    have hPμ : normalizeAt μ P μ = 1 := by726      simp only [normalizeAt, Pi.smul_apply, smul_eq_mul]; exact Ring.inverse_mul_cancel _ hu727    have hins : insertOne μ (dropCoord μ (normalizeAt μ P)) = normalizeAt μ P := by728      simp only [insertOne, dropCoord]729      rw [Fin.insertNth_eq_iff]730      exact ⟨hPμ.symm, rfl⟩731    simp only [reducedFormCell, Set.mem_ofPred_eq]732    rw [hins]733    refine ⟨hPμ, ?_⟩734    funext j735    have h : ∀ m, IsLocalRing.residue O (P m) = formProd d g m := fun m => congrFun (hres a ha) m736    have hμ' : IsLocalRing.residue O (P μ) = 1 := by rw [h, hμ]737    simp only [residueVector, normalizeAt, Pi.smul_apply, smul_eq_mul, map_mul, h]738    have : IsLocalRing.residue O (Ring.inverse (P μ)) = 1 := by739      simpa [hμ'] using congrArg (IsLocalRing.residue O) (Ring.inverse_mul_cancel _ hu)740    rw [this, one_mul]741  · intro L hL j742    set I := (IsLocalRing.maximalIdeal O) ^ L743    rw [hguard a ha, hguard a' ha', ← Ideal.Quotient.eq]744    set P := formProd d (fun i => insertOne (ν i) (a i)) with hP745    set P' := formProd d (fun i => insertOne (ν i) (a' i)) with hP'746    have hA : ∀ i k, Ideal.Quotient.mk I (insertOne (ν i) (a i) k) =747        Ideal.Quotient.mk I (insertOne (ν i) (a' i) k) := by748      intro i k749      simp only [insertOne]750      rcases Fin.eq_self_or_eq_succAbove (ν i) k with rfl | ⟨k, rfl⟩751      · simp752      · simp only [Fin.insertNth_apply_succAbove]753        exact Ideal.Quotient.eq.mpr (hL i k)754    have hPP : ∀ m, Ideal.Quotient.mk I (P m) = Ideal.Quotient.mk I (P' m) := by755      intro m756      rw [hP, hP', formProd_map, formProd_map]757      simp only [hA]758    have hu := hunit a ha759    have hu' := hunit a' ha'760    have hinv : Ideal.Quotient.mk I (Ring.inverse (P μ)) =761        Ideal.Quotient.mk I (Ring.inverse (P' μ)) := by762      have e1 := congrArg (Ideal.Quotient.mk I) (Ring.inverse_mul_cancel _ hu)763      have e2 := congrArg (Ideal.Quotient.mk I) (Ring.mul_inverse_cancel _ hu')764      simp only [map_mul, map_one] at e1 e2765      rw [hPP μ] at e1766      exact left_inv_eq_right_inv e1 e2767    simp only [dropCoord, Fin.removeNth_apply, normalizeAt, Pi.smul_apply, smul_eq_mul, map_mul,768      hinv, hPP]769 770open scoped Classical in771/-- Injectivity of the partial-fraction map for pairwise coprime binary forms: if772`∑ h i ∏_{j ≠ i} g j = c ∏ g i` with `h i` vanishing at `ν i`, then all `h i = 0`. -/773theorem forms_linear_injective (k ι : Type) [Field k] [Fintype ι] (d : ι → ℕ)774    (g : ∀ i, Fin (d i + 1) → k) (hg : ∀ i, g i ≠ 0) (hc : FormsCoprime d g)775    (ν : ∀ i, Fin (d i + 1)) (hν : ∀ i, g i (ν i) ≠ 0) (h : ∀ i, Fin (d i + 1) → k)776    (hh : ∀ i, h i (ν i) = 0) (c : k)777    (hsum : ∑ i, formPoly (h i) * ∏ j ∈ Finset.univ.erase i, formPoly (g j) = Polynomial.C c * ∏ i,778      formPoly (g i)) :779    ∀ i, h i = 0 := by780  set p : ι → Polynomial k := fun i => formPoly (h i) with hp781  set q : ι → Polynomial k := fun i => formPoly (g i) with hq782  have hq0 : ∀ i, q i ≠ 0 := fun i h0 => hg i (formPoly_eq_zero _ h0)783  have hQ0 : (∏ i, q i) ≠ 0 := Finset.prod_ne_zero_iff.mpr (fun i _ => hq0 i)784  -- Step 1: divisibility785  have hdvd : ∀ i, q i ∣ p i := by786    intro i787    have hcop : IsCoprime (q i) (∏ j ∈ Finset.univ.erase i, q j) :=788      IsCoprime.prod_right (fun j hj => hc.1 i j (Finset.ne_of_mem_erase hj).symm)789    apply hcop.dvd_of_dvd_mul_right790    have hs := hsum791    rw [← Finset.add_sum_erase _ _ (Finset.mem_univ i)] at hs792    have : p i * ∏ j ∈ Finset.univ.erase i, q j =793        Polynomial.C c * ∏ i, q i - ∑ l ∈ Finset.univ.erase i,794          p l * ∏ j ∈ Finset.univ.erase l, q j := by795      rw [← hs]; ring796    rw [this]797    apply dvd_sub798    · exact dvd_mul_of_dvd_right (Finset.dvd_prod_of_mem _ (Finset.mem_univ i)) _799    · apply Finset.dvd_sum800      intro l hl801      exact dvd_mul_of_dvd_right (Finset.dvd_prod_of_mem _802        (Finset.mem_erase.mpr ⟨(Finset.ne_of_mem_erase hl).symm, Finset.mem_univ i⟩)) _803  choose u hu using hdvd804  -- Step 2: sum of u equals C c805  have husum : ∑ i, u i = Polynomial.C c := by806    have : (∑ i, u i) * ∏ i, q i = Polynomial.C c * ∏ i, q i := by807      rw [← hsum, Finset.sum_mul]808      apply Finset.sum_congr rfl809      intro i _810      change u i * ∏ i, q i = p i * ∏ j ∈ Finset.univ.erase i, q j811      rw [hu i, ← Finset.mul_prod_erase _ _ (Finset.mem_univ i)]812      ring813    exact mul_right_cancel₀ hQ0 this814  have hconst_full : ∀ i, (q i).natDegree = d i → (u i).natDegree = 0 := by815    intro i hi816    by_cases hu0 : u i = 0817    · simp [hu0]818    have h1 : (p i).natDegree ≤ d i := natDegree_formPoly_le _819    rw [hu i, Polynomial.natDegree_mul (hq0 i) hu0, hi] at h1820    omega821  have hconst : ∀ i, (u i).natDegree = 0 := by822    intro i823    by_cases hi : (q i).natDegree = d i824    · exact hconst_full i hi825    have hoth : ∀ j ∈ Finset.univ.erase i, (u j).natDegree = 0 := fun j hj =>826      hconst_full j ((hc.2 i j (Finset.ne_of_mem_erase hj).symm).resolve_left hi)827    have : u i = Polynomial.C c - ∑ j ∈ Finset.univ.erase i, u j := by828      rw [← husum, ← Finset.add_sum_erase _ _ (Finset.mem_univ i)]; ring829    rw [this, ← Nat.le_zero]830    refine (natDegree_sub_le _ _).trans ?_831    rw [natDegree_C, zero_max]832    exact natDegree_sum_le_of_forall_le _ _ fun j hj => (hoth j hj).le833  -- Step 3: normalization834  intro i835  have hC : u i = Polynomial.C ((u i).coeff 0) := Polynomial.eq_C_of_natDegree_eq_zero (hconst i)836  have hco := coeff_formPoly (h i) (ν i)837  change (p i).coeff _ = _ at hco838  rw [hu i, hC, Polynomial.coeff_mul_C, hh i] at hco839  change (formPoly (g i)).coeff _ * _ = 0 at hco840  rw [coeff_formPoly] at hco841  have ha : (u i).coeff 0 = 0 := (mul_eq_zero.mp hco).resolve_left (hν i)842  apply formPoly_eq_zero843  change p i = 0844  rw [hu i, hC, ha]845  simp846 847/-- Degree bound for the partial-fraction map: `∑ h i ∏_{j ≠ i} g j + c ∏ g i` has degree at most848`∑ d i` when `g i, h i` are forms of degree `d i`. -/849private theorem natDegree_partial_fraction_le {k ι : Type} [Field k] [Fintype ι] [DecidableEq ι]850    (d : ι → ℕ) (g h : ∀ i, Fin (d i + 1) → k) (c : k) :851    (∑ i, formPoly (h i) * ∏ j ∈ Finset.univ.erase i, formPoly (g j) +852      C c * ∏ i, formPoly (g i)).natDegree ≤ ∑ i, d i := by853  have hprod : ∀ s : Finset ι, (∏ j ∈ s, formPoly (g j)).natDegree ≤ ∑ j ∈ s, d j := fun s =>854    (natDegree_prod_le _ _).trans (Finset.sum_le_sum fun j _ => natDegree_formPoly_le _)855  apply natDegree_add_le_of_degree_le856  · refine natDegree_sum_le_of_forall_le _ _ fun i _ => natDegree_mul_le.trans ?_857    have h1 := natDegree_formPoly_le (h i)858    have h2 := hprod (Finset.univ.erase i)859    rw [← Finset.add_sum_erase _ _ (Finset.mem_univ i)]860    omega861  · refine natDegree_mul_le.trans ?_862    rw [natDegree_C, zero_add]863    exact hprod _864 865open scoped Classical in866/-- Every binary form of degree `∑ d i` is `∑ h i ∏_{j ≠ i} g j + c ∏ g i` with `h i (ν i) = 0`867(partial fractions for pairwise coprime binary forms). -/868theorem forms_linear_bijective (k ι : Type) [Field k] [Fintype ι] (d : ι → ℕ)869    (g : ∀ i, Fin (d i + 1) → k) (hg : ∀ i, g i ≠ 0) (hc : FormsCoprime d g)870    (ν : ∀ i, Fin (d i + 1)) (hν : ∀ i, g i (ν i) ≠ 0) (w : Fin ((∑ i, d i) + 1) → k) :871    ∃ (h : ∀ i, Fin (d i + 1) → k) (c : k), (∀ i, h i (ν i) = 0) ∧ formPoly w = ∑ i, formPoly872      (h i) * ∏ j ∈ Finset.univ.erase i, formPoly (g j) + Polynomial.C c * ∏ i, formPoly (g i) := by873  let n := ∑ i, d i874  have hn : n = ∑ i, d i := rfl875  let P : ((∀ i, Fin (d i + 1) → k) × k) → k[X] := fun p =>876    ∑ i, formPoly (p.1 i) * ∏ j ∈ Finset.univ.erase i, formPoly (g j) +877      C p.2 * ∏ i, formPoly (g i)878  have hPdeg : ∀ p : (∀ i, Fin (d i + 1) → k) × k, (P p).natDegree ≤ n :=879    fun p => natDegree_partial_fraction_le d g p.1 p.2880  let Φ : ((∀ i, Fin (d i + 1) → k) × k) →ₗ[k] k[X] :=881    { toFun := P882      map_add' := by883        intro p q884        simp only [P, Prod.fst_add, Prod.snd_add, Pi.add_apply, formPoly_add, add_mul,885          Finset.sum_add_distrib, C_add]886        ring887      map_smul' := by888        intro c p889        simp only [P, Prod.smul_fst, Prod.smul_snd, Pi.smul_apply, formPoly_C_smul,890          RingHom.id_apply, smul_eq_mul, C_mul, Polynomial.smul_eq_C_mul, mul_add,891          Finset.mul_sum, mul_assoc] }892  let T : k[X] →ₗ[k] (Fin (n + 1) → k) := LinearMap.pi fun j => Polynomial.lcoeff k (j : ℕ)893  let ev : ((∀ i, Fin (d i + 1) → k) × k) →ₗ[k] (ι → k) :=894    { toFun := fun p i => p.1 i (ν i)895      map_add' := by intros; rfl896      map_smul' := by intros; rfl }897  let V := LinearMap.ker ev898  let L : V →ₗ[k] (Fin (n + 1) → k) := T.comp (Φ.comp V.subtype)899  have hev : Function.Surjective ev := by900    intro y901    refine ⟨(fun i => Pi.single (ν i) (y i), 0), ?_⟩902    funext i903    simp [ev]904  have hVdim : Module.finrank k V = n + 1 := by905    have h1 := LinearMap.finrank_range_add_finrank_ker ev906    rw [LinearMap.range_eq_top.mpr hev, finrank_top] at h1907    have h2 : Module.finrank k ((∀ i, Fin (d i + 1) → k) × k) = ∑ i, (d i + 1) + 1 := by908      simp [Module.finrank_prod, Module.finrank_pi_fintype]909    have h3 : ∑ i, (d i + 1) = n + Fintype.card ι := by910      rw [Finset.sum_add_distrib]911      simp [hn]912    rw [h2, Module.finrank_fintype_fun_eq_card, h3] at h1913    change Module.finrank k (LinearMap.ker ev) = n + 1914    omega915  have hL : Function.Injective L := by916    rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']917    intro p hp918    obtain ⟨⟨h, c⟩, hpv⟩ := p919    have hnu : ∀ i, h i (ν i) = 0 := fun i => by920      simpa [ev] using congrFun (LinearMap.mem_ker.mp hpv) i921    have hP0 : P (h, c) = 0 := by922      ext m923      rw [coeff_zero]924      by_cases hm : m ≤ n925      · have := congrFun hp ⟨m, Nat.lt_succ_of_le hm⟩926        simpa [L, T, Φ] using this927      · exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (hPdeg _) (by omega))928    have hsum : ∑ i, formPoly (h i) * ∏ j ∈ Finset.univ.erase i, formPoly (g j) =929        C (-c) * ∏ i, formPoly (g i) := by930      rw [C_neg, neg_mul, eq_neg_iff_add_eq_zero]931      exact hP0932    have hh0 := SurfaceBlowup.forms_linear_injective k ι d g hg hc ν hν h hnu (-c) hsum933    have hprod : ∏ i, formPoly (g i) ≠ 0 :=934      Finset.prod_ne_zero_iff.mpr fun i _ h0 => hg i (formPoly_eq_zero _ h0)935    obtain rfl : h = 0 := funext hh0936    have h3 : ∀ m : ℕ, formPoly (0 : Fin (m + 1) → k) = 0 := fun m => by simp [formPoly]937    obtain rfl : c = 0 := by simpa [P, h3, hprod] using hP0938    rfl939  have hsurj : Function.Surjective L :=940    (LinearMap.injective_iff_surjective_of_finrank_eq_finrank941      (by rw [hVdim, Module.finrank_fin_fun])).mp hL942  obtain ⟨⟨⟨h, c⟩, hpv⟩, hp⟩ := hsurj w943  refine ⟨h, c, fun i => by simpa [ev] using congrFun (LinearMap.mem_ker.mp hpv) i, ?_⟩944  · change formPoly w = P (h, c)945    ext m946    by_cases hm : m ≤ n947    · have := congrFun hp ⟨m, Nat.lt_succ_of_le hm⟩948      have h5 := coeff_formPoly w ⟨m, Nat.lt_succ_of_le hm⟩949      simp only at h5950      rw [h5, ← this]951      simp [L, T, Φ]952    · rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (natDegree_formPoly_le w) (by omega)),953        coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (hPdeg _) (by omega))]954 955/-- Over a local ring, a monic factorization `B C = B' C'` with `B ≡ B'` and `B̄, C̄`956coprime is unique. -/957theorem hensel_factor_unique_of_dvd (O : Type) [CommRing O] [IsLocalRing O]958    (B C B' C' : Polynomial O) (hB : B.Monic) (hC : C.Monic) (hB' : B'.Monic) (hC' : C'.Monic)959    (hp : B * C = B' * C')960    (hred : B.map (IsLocalRing.residue O) = B'.map (IsLocalRing.residue O))961    (hc : IsCoprime (B.map (IsLocalRing.residue O)) (C.map (IsLocalRing.residue O))) :962    B = B' ∧ C = C' := by963  have hm := congrArg (Polynomial.map (IsLocalRing.residue O)) hp964  rw [Polynomial.map_mul, Polynomial.map_mul, ← hred] at hm965  have hne : B.map (IsLocalRing.residue O) ≠ 0 := (hB.map _).ne_zero966  have hCC : C.map (IsLocalRing.residue O) = C'.map (IsLocalRing.residue O) :=967    mul_left_cancel₀ hne hm968  exact SurfaceBlowup.hensel_pair_unique O B C B' C' hB hC hB' hC' hred hCC hc hp969 970/-- Over a local ring, a factorization into monic factors with pairwise coprime reductions971is determined by the reductions. -/972theorem hensel_family_unique (O ι : Type) [CommRing O] [IsLocalRing O] [Fintype ι]973    (G G' : ι → Polynomial O) (hG : ∀ i, (G i).Monic) (hG' : ∀ i, (G' i).Monic)974    (hred : ∀ i, (G i).map (IsLocalRing.residue O) = (G' i).map (IsLocalRing.residue O))975    (hc : ∀ i j, i ≠ j → IsCoprime ((G i).map (IsLocalRing.residue O))976      ((G j).map (IsLocalRing.residue O))) (hp : ∏ i, G i = ∏ i, G' i) :977    G = G' := by978  classical979  have key : ∀ s : Finset ι, ∏ i ∈ s, G i = ∏ i ∈ s, G' i → ∀ i ∈ s, G i = G' i := by980    intro s981    induction s using Finset.induction_on with982    | empty => intro _ i hi; simp at hi983    | @insert a s ha ih =>984      intro h i hi985      rw [Finset.prod_insert ha, Finset.prod_insert ha] at h986      have hcop : IsCoprime ((G a).map (IsLocalRing.residue O))987          ((∏ j ∈ s, G j).map (IsLocalRing.residue O)) := by988        rw [Polynomial.map_prod]989        exact IsCoprime.prod_right fun j hj => hc a j (fun e => ha (e ▸ hj))990      have hmap : (∏ j ∈ s, G j).map (IsLocalRing.residue O)991          = (∏ j ∈ s, G' j).map (IsLocalRing.residue O) := by992        rw [Polynomial.map_prod, Polynomial.map_prod]993        exact Finset.prod_congr rfl fun j _ => hred j994      obtain ⟨h1, h2⟩ := SurfaceBlowup.hensel_pair_unique O (G a) (∏ j ∈ s, G j) (G' a)995        (∏ j ∈ s, G' j) (hG a) (Polynomial.monic_prod_of_monic _ _ fun j _ => hG j) (hG' a)996        (Polynomial.monic_prod_of_monic _ _ fun j _ => hG' j) (hred a) hmap hcop h997      rcases Finset.mem_insert.mp hi with rfl | hi998      · exact h1999      · exact ih h2 i hi1000  funext i1001  exact key Finset.univ hp i (Finset.mem_univ i)1002 1003/-- If `τ i` are the iterates of a ring automorphism `τ 1` of `L` of period `δ`, whose fixed points1004come from `ι : K → L`, then the orbit product `∏_{i<δ} p^{τ i}` of every polynomial descends1005along `ι`. -/1006private theorem orbit_product_lifts {K L : Type} [CommRing K] [CommRing L] (ι : K →+* L)1007    (τ : ℕ → (L ≃+* L)) (δ : ℕ) (hτ0 : τ 0 = RingEquiv.refl L)1008    (hrec : ∀ i : ℕ, τ (i+1) = (τ i).trans (τ 1)) (hτδ : ∀ z : L, τ δ z = z)1009    (hfix : ∀ z : L, τ 1 z = z → ∃ y : K, ι y = z) (p : Polynomial L) :1010    ∏ i : Fin δ, p.map (τ i).toRingHom ∈ Polynomial.lifts ι := by1011  have hτδ' : τ δ = τ 0 := by1012    ext z; rw [hτδ, hτ0]; rfl1013  have hshift : ∀ i : Fin δ, (τ 1).toRingHom.comp (τ i).toRingHom = (τ (i.val + 1)).toRingHom :=1014    fun i => by rw [hrec (i : ℕ)]; rfl1015  -- the orbit product is `τ 1`-invariant: applying `τ 1` shifts the orbit cyclically1016  have Pinv : (∏ i : Fin δ, p.map (τ i).toRingHom).map (τ 1).toRingHom =1017      ∏ i : Fin δ, p.map (τ i).toRingHom := by1018    simp only [Polynomial.map_prod, Polynomial.map_map, hshift]1019    cases δ with1020    | zero => simp1021    | succ n =>1022      rw [Fin.prod_univ_castSucc, Fin.prod_univ_succ]1023      simp only [Fin.val_castSucc, Fin.val_last, Fin.val_succ, Fin.val_zero]1024      rw [hτδ', mul_comm]1025  exact (Polynomial.lifts_iff_coeff_lifts _).2 fun n => hfix _ <| by1026    simpa [Polynomial.coeff_map] using congrArg (Polynomial.coeff · n) Pinv1027 1028/-- A monic polynomial `H` over `K` is irreducible if `H.map ι` is the product of pairwise1029distinct monic irreducible conjugates `g^{τ i}` of an irreducible `g ∣ H.map ι`, the `τ i` being1030automorphisms fixing the image of `K`. -/1031private theorem irreducible_of_map_eq_orbit_product {K L : Type} [Field K] [Field L]1032    (ι : K →+* L) (hinj : Function.Injective ι) (τ : ℕ → (L ≃+* L))1033    (hτι : ∀ (i : ℕ) (y : K), τ i (ι y) = ι y) {δ : ℕ} {g : Polynomial L} (hgi : Irreducible g)1034    (hconj : ∀ i : Fin δ, (g.map (τ i).toRingHom).Monic ∧ Irreducible (g.map (τ i).toRingHom))1035    (hdist : ∀ i j : Fin δ, g.map (τ i).toRingHom = g.map (τ j).toRingHom → i = j)1036    {H : Polynomial K} (hHm : H.Monic) (hH : H.map ι = ∏ i : Fin δ, g.map (τ i).toRingHom)1037    (hgdvd : g ∣ H.map ι) : Irreducible H := by1038  have hcomp : ∀ i : ℕ, ((τ i).toRingHom.comp ι) = ι := fun i => RingHom.ext (hτι i)1039  -- a factor `A` of `H` with `g ∣ A^ι` absorbs every conjugate, hence all of `H^ι`1040  have key : ∀ A B, H = A * B → g ∣ A.map ι → IsUnit B := by1041    intro A B hAB hg1042    have hA : A ≠ 0 := by rintro rfl; exact hHm.ne_zero (by simp [hAB])1043    have hB : B ≠ 0 := by rintro rfl; exact hHm.ne_zero (by simp [hAB])1044    have hdvd : H.map ι ∣ A.map ι := by1045      rw [hH]1046      apply Fintype.prod_dvd_of_coprime1047      · exact fun i j hij => distinct_monic_irreducible_coprime _ _ _ (hconj i).1 (hconj j).11048          (hconj i).2 (hconj j).2 fun he => hij (hdist i j he)1049      · intro i1050        have := Polynomial.map_dvd (τ i).toRingHom hg1051        rwa [Polynomial.map_map, hcomp] at this1052    have hle := Polynomial.natDegree_le_of_dvd hdvd (Polynomial.map_ne_zero hA)1053    rw [Polynomial.natDegree_map_eq_of_injective hinj,1054      Polynomial.natDegree_map_eq_of_injective hinj, hAB, Polynomial.natDegree_mul hA hB] at hle1055    rw [Polynomial.isUnit_iff_degree_eq_zero, Polynomial.degree_eq_natDegree hB]1056    exact_mod_cast (by omega : B.natDegree = 0)1057  refine ⟨fun hu => hgi.not_isUnit (isUnit_of_dvd_unit hgdvd ((Polynomial.isUnit_map ι).2 hu)),1058    fun A B hAB => ?_⟩1059  have : g ∣ A.map ι * B.map ι := by rw [← Polynomial.map_mul, ← hAB]; exact hgdvd1060  rcases hgi.prime.dvd_or_dvd this with h | h1061  · exact Or.inr (key A B hAB h)1062  · exact Or.inl (key B A (by rw [hAB, mul_comm]) h)1063 1064/-- The Frobenius orbit products of the irreducible factors of `F` descend to distinct monic1065irreducible polynomials over `Frac O` whose product is the conjugate product of `F`. -/1066theorem invariant_orbit_factors (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1067    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]1068    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) [IsDomain (AdjoinRoot Φ)]1069    (ι : BaseField O →+* BaseField (AdjoinRoot Φ))1070    (τ : ℕ → (BaseField (AdjoinRoot Φ) ≃+* BaseField (AdjoinRoot Φ)))1071    (hτ : ∀ (i : ℕ) (x : AdjoinRoot Φ), τ i1072      (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)) x) = algebraMap (AdjoinRoot Φ)1073      (BaseField (AdjoinRoot Φ)) (frobeniusIter O Φ i x))1074    (hτι : ∀ (i : ℕ) (y : BaseField O), τ i (ι y) = ι y)1075    (hτ0 : τ 0 = RingEquiv.refl (BaseField (AdjoinRoot Φ)))1076    (hrec : ∀ i : ℕ, τ (i+1) = (τ i).trans (τ 1))1077    (hτδ : ∀ z : BaseField (AdjoinRoot Φ), τ Φ.natDegree z = z)1078    (hfix : ∀ z : BaseField (AdjoinRoot Φ), τ 1 z = z → ∃ y : BaseField O, ι y = z)1079    (hinj : Function.Injective ι) (F : Polynomial (AdjoinRoot Φ))1080    (gs : List (Polynomial (BaseField (AdjoinRoot Φ)))) (hgs : ∀ g ∈ gs, g.Monic ∧ Irreducible g)1081    (hd : gs.Pairwise (fun g h => g ≠ h))1082    (hprod : F.map (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) = gs.prod)1083    (hcop : ∀ i j : Fin Φ.natDegree, i ≠ j → IsCoprime1084      ((fun i : Fin Φ.natDegree => (F.map (frobeniusIter O Φ i).toRingHom).map1085          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) i)1086      ((fun i : Fin Φ.natDegree => (F.map (frobeniusIter O Φ i).toRingHom).map1087          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ)))) j)) :1088    ∃ H : Fin gs.length → Polynomial (BaseField O), (∀ a, (H a).Monic ∧ Irreducible (H a)) ∧1089      Function.Injective H ∧1090      (∀ a, (H a).map ι = ∏ i : Fin Φ.natDegree, (gs.get a).map (τ i).toRingHom) ∧1091      (∀ a, (H a).natDegree = Φ.natDegree * (gs.get a).natDegree) ∧ (∏ a, H a).map ι =1092      (conjugateProduct O Φ F).map (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) := by1093  obtain ⟨h1, h2, _h3, h4⟩ := SurfaceBlowup.conjugate_irreducible_factors_distinct O Φ τ hτ1094    F gs hgs hd hprod hcop1095  -- positivity of δ1096  have hδ : 0 < Φ.natDegree := Nat.pos_of_ne_zero fun h0 => hΦ.2.not_isUnit <| by1097    rw [residuePoly, eq_one_of_monic_natDegree_zero (hΦ.1.map _) (by rw [hΦ.1.natDegree_map, h0])]1098    exact isUnit_one1099  set δ := Φ.natDegree with hδdef1100  -- orbit product1101  let P : Polynomial (BaseField (AdjoinRoot Φ)) → Polynomial (BaseField (AdjoinRoot Φ)) :=1102    fun p => ∏ i : Fin δ, p.map (τ i).toRingHom1103  have Plifts : ∀ p, P p ∈ Polynomial.lifts ι := orbit_product_lifts ι τ δ hτ0 hrec hτδ hfix1104  choose H hH using fun a : Fin gs.length => Polynomial.mem_lifts _ |>.mp (Plifts (gs.get a))1105  have gmem : ∀ a : Fin gs.length, gs.get a ∈ gs := fun a => List.get_mem gs a1106  have gmon : ∀ a, (gs.get a).Monic := fun a => (hgs _ (gmem a)).11107  have girr : ∀ a, Irreducible (gs.get a) := fun a => (hgs _ (gmem a)).21108  have Pmon : ∀ a, (P (gs.get a)).Monic := fun a =>1109    Polynomial.monic_prod_of_monic _ _ fun (i : Fin δ) _ => (h1 i _ (gmon a) (girr a)).11110  have Pdeg : ∀ a, (P (gs.get a)).natDegree = δ * (gs.get a).natDegree := by1111    intro a1112    simp only [P]1113    rw [Polynomial.natDegree_prod_of_monic (h := fun (i : Fin δ) _ => (h1 i _ (gmon a) (girr a)).1)]1114    simp [Polynomial.natDegree_map]1115  have Hmon : ∀ a, (H a).Monic := fun a =>1116    Polynomial.monic_of_injective hinj (by rw [hH a]; exact Pmon a)1117  have Hdeg : ∀ a, (H a).natDegree = δ * (gs.get a).natDegree := by1118    intro a1119    rw [← Pdeg a, ← hH a, Polynomial.natDegree_map_eq_of_injective hinj]1120  have hτ0' : ∀ p : Polynomial (BaseField (AdjoinRoot Φ)), p.map (τ 0).toRingHom = p :=1121    fun p => by simp [hτ0]1122  have gdvdP : ∀ a, gs.get a ∣ P (gs.get a) := fun a => by1123    have h := Finset.dvd_prod_of_mem (fun i : Fin δ => (gs.get a).map (τ i).toRingHom)1124      (Finset.mem_univ (⟨0, hδ⟩ : Fin δ))1125    rwa [Fin.val_mk, hτ0'] at h1126  refine ⟨H, fun a => ⟨Hmon a, ?_⟩, ?_, hH, Hdeg, ?_⟩1127  · -- irreducibility1128    exact irreducible_of_map_eq_orbit_product ι hinj τ hτι (girr a)1129      (fun i => h1 i _ (gmon a) (girr a)) (fun i j he => (h2 i j a a he).1) (Hmon a) (hH a)1130      (by rw [hH a]; exact gdvdP a)1131  · -- injectivity1132    intro a b hab1133    have : gs.get a ∣ P (gs.get b) := by1134      rw [← hH b, ← hab, hH a]; exact gdvdP a1135    obtain ⟨i, -, hi⟩ := ((girr a).prime).exists_mem_finset_dvd this1136    have hm := h1 i _ (gmon b) (girr b)1137    have heq := Polynomial.eq_of_monic_of_associated (gmon a) hm.11138      ((girr a).associated_of_dvd hm.2 hi)1139    exact (h2 ⟨0, hδ⟩ i a b (by rw [Fin.val_mk, hτ0']; exact heq)).21140  · -- product1141    rw [h4, Polynomial.map_prod]1142    simp only [hH, P]1143    rw [Finset.prod_comm]1144    refine Finset.prod_congr rfl (fun i _ => ?_)1145    rw [← Fin.prod_univ_fun_getElem]1146    rfl1147 1148/-- An algebra isomorphism of local rings identifies the maximal ideals (via `comap` and `map`). -/1149theorem local_algEquiv_maximalIdeal (O B B' : Type) [CommRing O] [CommRing B] [CommRing B']1150    [IsLocalRing B] [IsLocalRing B'] [Algebra O B] [Algebra O B'] (φ : B ≃ₐ[O] B') :1151    (IsLocalRing.maximalIdeal B').comap (φ : B →+* B') = IsLocalRing.maximalIdeal B ∧1152      (IsLocalRing.maximalIdeal B).map (φ : B →+* B') = IsLocalRing.maximalIdeal B' := by1153  have h1 : (IsLocalRing.maximalIdeal B').comap (φ : B →+* B') = IsLocalRing.maximalIdeal B := by1154    have : IsLocalHom (φ : B →+* B') := ⟨fun a ha => by simpa using ha.map φ.symm⟩1155    exact IsLocalRing.maximalIdeal_comap _1156  refine ⟨h1, ?_⟩1157  rw [← h1]1158  exact Ideal.map_comap_of_surjective _ φ.surjective _1159 1160end SurfaceBlowup