Factor cells: residue cells of factor products and root-field isomorphisms

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.Formula.LawAlgebra7import SurfaceBlowup.Unramified.Extension8 9/-!10# Factor cells: residue cells of factor products and root-field isomorphisms11 12Building blocks for the measure of polynomial types: invariance of `(e, f)` under isomorphism of13DVR extensions; monic polynomials as coefficient vectors and the Hensel bijection between products14of residue cells and the residue cell of the product; squarefree factorizations from reducedness;15masses of normalized form cells; idempotents of products of fields and the induced matching of16factors under an isomorphism; the Chinese remainder decomposition of `K[X]/(∏ gᵢ)`; and root-field17isomorphisms along a conjugate orbit.18 19## Main results20 21* `SurfaceBlowup.dvr_algEquiv_ramification_inertia`, `SurfaceBlowup.monic_poly_reconstruct`22* `SurfaceBlowup.factor_product_bijection`, `SurfaceBlowup.monic_squarefree_factors_of_reduced`23* `SurfaceBlowup.normalized_form_cell_cylinder_mass`, `SurfaceBlowup.form_cell_product_measure`24* `SurfaceBlowup.pi_fields_algEquiv_index_bijection`,25  `SurfaceBlowup.polynomial_quotient_product_equiv`,26  `SurfaceBlowup.root_field_algEquiv_conjugate_orbit`27 28Provenance: Thm_SurfaceBlowupV2_{dvr_algEquiv_ramification_inertia,29monic_congruent_difference_factor, monic_poly_reconstruct, factor_product_bijection,30monic_squarefree_factors_of_reduced, normalized_form_cell_cylinder_mass,31form_cell_product_measure, pi_fields_primitive_idempotents, pi_fields_algEquiv_index_bijection,32polynomial_congruence_and_product, polynomial_quotient_product_equiv,33root_field_algEquiv_conjugate_orbit}.34-/35 36namespace SurfaceBlowup37 38open scoped ENNReal39 40/-! ### Invariants of DVR extensions -/41 42/-- `O`-isomorphic integral DVR extensions of a DVR `O` have the same ramification index and43inertia degree. -/44theorem dvr_algEquiv_ramification_inertia (O B B' : Type) [CommRing O] [IsDomain O]45    [IsDiscreteValuationRing O] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [CommRing B']46    [IsDomain B'] [IsDiscreteValuationRing B'] [Algebra O B] [Algebra O B'] [Algebra.IsIntegral O B]47    [Algebra.IsIntegral O B'] (hinj : Function.Injective (algebraMap O B))48    (hinj' : Function.Injective (algebraMap O B')) (φ : B ≃ₐ[O] B') :49    (IsLocalRing.maximalIdeal B).ramificationIdx O = (IsLocalRing.maximalIdeal B').ramificationIdx O50      ∧ (IsLocalRing.maximalIdeal B).inertiaDeg O = (IsLocalRing.maximalIdeal B').inertiaDeg O := by51  obtain ⟨hc, hm⟩ := local_algEquiv_maximalIdeal O B B' φ52  refine ⟨?_, ?_⟩53  · have h1 := dvr_extension_maximalIdeal_map_eq_pow O B hinj54    have h2 := dvr_extension_maximalIdeal_map_eq_pow O B' hinj'55    have h3 := congrArg (Ideal.map (φ : B →+* B')) h156    rw [Ideal.map_map, Ideal.map_pow, hm] at h357    have hcomp : ((φ : B →+* B').comp (algebraMap O B)) = algebraMap O B' := by58      ext x; simp59    rw [hcomp, h2] at h360    exact dvr_maximalIdeal_pow_injective B' _ _ h3.symm61  · have l1 := (integral_local_extension_unique_prime O B).162    have l2 := (integral_local_extension_unique_prime O B').163    have : (IsLocalRing.maximalIdeal B).LiesOver (IsLocalRing.maximalIdeal O) := ⟨l1.symm⟩64    have : (IsLocalRing.maximalIdeal B').LiesOver (IsLocalRing.maximalIdeal O) := ⟨l2.symm⟩65    rw [Ideal.inertiaDeg_eq_of_isMaximal (IsLocalRing.maximalIdeal O) (IsLocalRing.maximalIdeal B),66      Ideal.inertiaDeg_eq_of_isMaximal (IsLocalRing.maximalIdeal O) (IsLocalRing.maximalIdeal B')]67    exact (Ideal.Quotient.algEquivOfEqComap (IsLocalRing.maximalIdeal O) φ68      (by rw [← hc]; rfl)).toLinearEquiv.finrank_eq69 70/-! ### Monic polynomials and coefficient vectors -/71 72/-- If monic `G, G'` of degree `n` are congruent modulo `πⁱ` (with `π` a nonzerodivisor), then73`G' - G = πⁱ H` with `deg H < n`; moreover `πⁱ x ∈ (πⁱ⁺¹)` implies `x ∈ (π)`. -/74theorem monic_congruent_difference_factor (O : Type) [CommRing O] (pi : O)75    (hreg : ∀ x : O, pi * x = 0 → x = 0) (i n : ℕ) (G G' : Polynomial O) (hG : G.Monic)76    (hG' : G'.Monic) (hn : G.natDegree = n) (hn' : G'.natDegree = n)77    (hcong : ∀ j, G'.coeff j - G.coeff j ∈ Ideal.span {pi ^ i}) :78    (∃ H : Polynomial O, G' - G = Polynomial.C (pi ^ i) * H ∧ H.degree < (n : WithBot ℕ)) ∧79      (∀ x : O, pi ^ i * x ∈ Ideal.span {pi ^ (i + 1)} → x ∈ Ideal.span {pi}) := by80  have hpow : ∀ k : ℕ, ∀ x : O, pi ^ k * x = 0 → x = 0 := by81    intro k82    induction k with83    | zero => intro x hx; simpa using hx84    | succ k ih => exact fun x hx ↦ hreg _ (ih _ (by rw [← mul_assoc, ← pow_succ]; exact hx))85  refine ⟨?_, fun x hx ↦ ?_⟩86  · obtain ⟨H, hH⟩ : Polynomial.C (pi ^ i) ∣ G' - G := by87      rw [Polynomial.C_dvd_iff_dvd_coeff]88      exact fun j ↦ by rw [Polynomial.coeff_sub]; exact Ideal.mem_span_singleton.mp (hcong j)89    refine ⟨H, hH, Polynomial.degree_lt_iff_coeff_zero _ _ |>.2 fun m hm ↦ hpow i _ ?_⟩90    rw [← Polynomial.coeff_C_mul, ← hH, Polynomial.coeff_sub]91    rcases Nat.eq_or_lt_of_le hm with rfl | h92    · rw [show G'.coeff n = 1 from hn' ▸ hG'.coeff_natDegree,93        show G.coeff n = 1 from hn ▸ hG.coeff_natDegree, sub_self]94    · rw [Polynomial.coeff_eq_zero_of_natDegree_lt (by omega),95        Polynomial.coeff_eq_zero_of_natDegree_lt (by omega), sub_self]96  · obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp hx97    exact Ideal.mem_span_singleton'.2 ⟨y, (sub_eq_zero.mp (hpow i _ (by98      rw [mul_sub, ← hy, pow_succ]; ring))).symm⟩99 100/-- `monicPolyO a = Xⁿ + Σ aᵢ Xⁱ` is monic of degree `n` with lower coefficients `a`, and every101monic polynomial of degree `n` arises from its coefficient vector. -/102theorem monic_poly_reconstruct (O : Type) [CommRing O] [Nontrivial O] (n : ℕ) (a : Fin n → O) :103    (monicPolyO a).Monic ∧ (monicPolyO a).natDegree = n104      ∧ (∀ i : Fin n, (monicPolyO a).coeff i = a i)105      ∧ (∀ F : Polynomial O, F.Monic → F.natDegree = n → monicPolyO (coeffVec n F) = F) := by106  have hdeg := Polynomial.degree_sum_fin_lt a107  refine ⟨Polynomial.monic_X_pow_add hdeg, ?_, ?_, ?_⟩108  · unfold monicPolyO109    rw [Polynomial.natDegree_add_eq_left_of_degree_lt, Polynomial.natDegree_X_pow]110    rwa [Polynomial.degree_X_pow]111  · intro i112    unfold monicPolyO113    rw [Polynomial.coeff_add, Polynomial.coeff_X_pow, if_neg (by omega), zero_add,114      Polynomial.finsetSum_coeff]115    simp only [Polynomial.coeff_C_mul, Polynomial.coeff_X_pow]116    rw [Finset.sum_eq_single i]117    · simp118    · intro j _ hj119      rw [if_neg (fun h ↦ hj (Fin.ext h.symm)), mul_zero]120    · simp121  · intro F hF hn122    conv_rhs => rw [hF.as_sum, hn]123    unfold monicPolyO coeffVec124    rw [Fin.sum_univ_eq_sum_range (fun i ↦ Polynomial.C (F.coeff i) * Polynomial.X ^ i)]125 126/-- Over a complete local ring, multiplying monic lifts gives a bijection from the product of the127residue cells of pairwise coprime monic `gᵢ` onto the residue cell of `∏ gᵢ` (Hensel). -/128theorem factor_product_bijection (O : Type) [CommRing O] [IsLocalRing O]129    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (ι : Type) [Fintype ι]130    (g : ι → Polynomial (IsLocalRing.ResidueField O)) (hg : ∀ i, (g i).Monic)131    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) :132    Set.BijOn (factorProduct (fun i ↦ (g i).natDegree))133      (Set.pi Set.univ (fun i ↦ residueCell O (g i).natDegree (g i)))134      (residueCell O (∑ i, (g i).natDegree) (∏ i, g i)) := by135  have R := fun (n : ℕ) (a : Fin n → O) ↦ monic_poly_reconstruct O n a136  have hprod : ∀ a : ∀ i, Fin (g i).natDegree → O,137      monicPolyO (factorProduct (fun i ↦ (g i).natDegree) a) = ∏ i, monicPolyO (a i) := by138    intro a139    unfold factorProduct140    apply (R _ (fun _ ↦ (0 : O))).2.2.2141    · exact Polynomial.monic_prod_of_monic _ _ (fun i _ ↦ (R _ (a i)).1)142    · rw [Polynomial.natDegree_prod_of_monic _ _ (fun i _ ↦ (R _ (a i)).1)]143      exact Finset.sum_congr rfl (fun i _ ↦ (R _ (a i)).2.1)144  refine ⟨?_, ?_, ?_⟩145  · intro a ha146    simp only [Set.mem_pi, Set.mem_univ, true_implies, residueCell, Set.mem_ofPred_eq] at ha ⊢147    rw [hprod, Polynomial.map_prod]148    exact Finset.prod_congr rfl (fun i _ ↦ ha i)149  · intro a ha a' ha' h150    simp only [Set.mem_pi, Set.mem_univ, true_implies, residueCell, Set.mem_ofPred_eq] at ha ha'151    have hp : ∏ i, monicPolyO (a i) = ∏ i, monicPolyO (a' i) := by152      rw [← hprod, ← hprod, h]153    have hG := hensel_family_unique O ι (fun i ↦ monicPolyO (a i))154      (fun i ↦ monicPolyO (a' i)) (fun i ↦ (R _ (a i)).1) (fun i ↦ (R _ (a' i)).1)155      (fun i ↦ by simp only [ha i, ha' i])156      (fun i j hij ↦ by simpa only [ha i, ha j] using hc i j hij) hp157    funext i j158    have := congrFun hG i159    rw [← (R _ (a i)).2.2.1 j, ← (R _ (a' i)).2.2.1 j, this]160  · intro c hc'161    simp only [residueCell, Set.mem_ofPred_eq] at hc'162    obtain ⟨G, hGm, hF, hGr, hGd⟩ := hensel_family_exists O ι (monicPolyO c)163      (R _ c).1 g hg hc hc'164    have hrec : ∀ i, monicPolyO (coeffVec (g i).natDegree (G i)) = G i :=165      fun i ↦ (R _ (fun _ ↦ (0 : O))).2.2.2 _ (hGm i) (hGd i)166    refine ⟨fun i ↦ coeffVec (g i).natDegree (G i), ?_, ?_⟩167    · simp only [Set.mem_pi, Set.mem_univ, true_implies, residueCell, Set.mem_ofPred_eq]168      intro i169      rw [hrec i, hGr i]170    · unfold factorProduct171      simp only [hrec]172      rw [← hF]173      funext j174      simp only [coeffVec]175      exact (R _ c).2.2.1 j176 177/-- A monic `F` over a field with `K[X]/(F)` reduced is a product of distinct monic irreducibles. -/178theorem monic_squarefree_factors_of_reduced (K : Type) [Field K] (F : Polynomial K)179    (hF : F.Monic) (hred : IsReduced (AdjoinRoot F)) :180    ∃ gs : List (Polynomial K), (∀ g ∈ gs, g.Monic ∧ Irreducible g) ∧181      gs.Pairwise (fun g h ↦ g ≠ h) ∧ F = gs.prod := by182  classical183  open UniqueFactorizationMonoid in184  have hF0 : F ≠ 0 := hF.ne_zero185  have hsq : Squarefree F := by186    rintro g ⟨h, rfl⟩187    have hgh : g * h ≠ 0 := by rintro h0; apply hF0; rw [mul_assoc, h0, mul_zero]188    have h0 := (show IsNilpotent (AdjoinRoot.mk (g * g * h) (g * h)) from189      ⟨2, by rw [← map_pow, AdjoinRoot.mk_eq_zero]; exact ⟨h, by ring⟩⟩).eq_zero190    rw [AdjoinRoot.mk_eq_zero, mul_assoc] at h0191    exact isUnit_of_dvd_one ((mul_dvd_mul_iff_right hgh).1 (by simpa using h0))192  set M := normalizedFactors F193  have hmon : ∀ g ∈ M, g.Monic := fun g hg ↦ by194    rw [← normalize_normalized_factor g hg]195    exact Polynomial.monic_normalize (irreducible_of_normalized_factor g hg).ne_zero196  refine ⟨M.toList, fun g hg ↦ ?_, ?_, ?_⟩197  · rw [Multiset.mem_toList] at hg198    exact ⟨hmon g hg, irreducible_of_normalized_factor g hg⟩199  · change List.Nodup _200    rw [← Multiset.coe_nodup, Multiset.coe_toList]201    exact (squarefree_iff_nodup_normalizedFactors hF0).1 hsq202  · rw [Multiset.prod_toList]203    exact (Polynomial.eq_of_monic_of_associated204      (by simpa using Polynomial.monic_multiset_prod_of_monic M id hmon) hF205      (prod_normalizedFactors hF0)).symm206 207/-! ### Normalized form cells -/208 209/-- The normalized form cell of `g` (residues prescribed, coordinate `ν` normalized to `1`) is a210nonempty measurable residue class of mass `q^{-d}`; its normalized cell measure is a probability211measure giving each congruence ball mod `m^L` mass `q^{-d(L-1)}`. -/212theorem normalized_form_cell_cylinder_mass (O : Type) [CommRing O] [IsDomain O]213    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]214    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]215    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]216    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (d : ℕ) (ν : Fin (d + 1))217    (g : Fin (d + 1) → IsLocalRing.ResidueField O) (hgν : g ν = 1) :218    (∀ b : Fin d → O, b ∈ reducedFormCell O d ν g ↔219        ∀ j, IsLocalRing.residue O (b j) = g (ν.succAbove j)) ∧220      (∀ b ∈ reducedFormCell O d ν g,221        reducedFormCell O d ν g = {b' | ∀ j, b' j - b j ∈ (IsLocalRing.maximalIdeal O)}) ∧222      (reducedFormCell O d ν g).Nonempty ∧ MeasurableSet (reducedFormCell O d ν g) ∧223      coefficientMeasure O d (reducedFormCell O d ν g) =224        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ d ∧225      MeasureTheory.IsProbabilityMeasure (cellMeasure O d (reducedFormCell O d ν g)) ∧226      ∀ (L : ℕ) (b : Fin d → O), 1 ≤ L → b ∈ reducedFormCell O d ν g →227        cellMeasure O d (reducedFormCell O d ν g)228            {b' | ∀ j, b' j - b j ∈ (IsLocalRing.maximalIdeal O) ^ L} =229          (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (d * (L - 1)) := by230  set C := reducedFormCell O d ν g with hCdef231  set q : ℝ≥0∞ := (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)232  have h1 : ∀ b : Fin d → O, b ∈ C ↔ ∀ j, IsLocalRing.residue O (b j) = g (ν.succAbove j) := by233    intro b234    simp only [hCdef, reducedFormCell, normalizedFormCell, insertOne, Set.mem_ofPred_eq,235      Fin.insertNth_apply_same, true_and]236    refine ⟨fun h j ↦ by237      simpa [residueVector, Fin.insertNth_apply_succAbove] using congrFun h (ν.succAbove j),238      fun h ↦ funext fun i ↦ ?_⟩239    rcases Fin.eq_self_or_eq_succAbove ν i with rfl | ⟨j, rfl⟩240    · simp [residueVector, hgν]241    · simp [residueVector, Fin.insertNth_apply_succAbove, h j]242  have h2 : ∀ b ∈ C, C = {b' | ∀ j, b' j - b j ∈ (IsLocalRing.maximalIdeal O)} := by243    intro b hb244    ext b'245    rw [h1] at hb246    rw [h1, Set.mem_ofPred_eq]247    exact forall_congr' fun j ↦ by rw [← hb j]; exact Ideal.Quotient.eq248  obtain ⟨b0, hb0⟩ : C.Nonempty :=249    ⟨fun j ↦ (IsLocalRing.residue_surjective (g (ν.succAbove j))).choose,250      (h1 _).2 fun j ↦ (IsLocalRing.residue_surjective (g (ν.succAbove j))).choose_spec⟩251  have hball : ∀ L (b : Fin d → O),252      MeasurableSet {b' : Fin d → O | ∀ j, b' j - b j ∈ (IsLocalRing.maximalIdeal O) ^ L} := by253    intro L b254    have hm := finite_coordinate_borel_cylinders O (IsLocalRing.maximalIdeal O) htop d255    have : @MeasurableSet _ (adicCylinderSpace (IsLocalRing.maximalIdeal O) (Fin d → O))256        {b' : Fin d → O | ∀ j, b' j - b j ∈ (IsLocalRing.maximalIdeal O) ^ L} :=257      MeasurableSpace.measurableSet_generateFrom <| Or.inr ⟨L, b, by258        ext y259        simp only [Set.mem_ofPred_eq]260        rw [finite_coordinate_adic_congruence]⟩261    rwa [← hm] at this262  have hC1 : C = {b' | ∀ j, b' j - b0 j ∈ (IsLocalRing.maximalIdeal O) ^ 1} := by263    rw [h2 b0 hb0]; simp264  have h4 : MeasurableSet C := by rw [hC1]; exact hball 1 b0265  have h5 : coefficientMeasure O d C = q⁻¹ ^ d := by266    rw [hC1, coefficient_cylinder_mass O htop, mul_one]267  have hμ0 : q⁻¹ ^ d ≠ 0 := pow_ne_zero _ (ENNReal.inv_ne_zero.mpr (ENNReal.natCast_ne_top _))268  have hμt : q⁻¹ ^ d ≠ ⊤ := ENNReal.pow_ne_top <| ENNReal.inv_ne_top.mpr <| by269    simp only [q]; exact_mod_cast (Nat.card_pos (α := IsLocalRing.ResidueField O)).ne'270  refine ⟨h1, h2, ⟨b0, hb0⟩, h4, h5, ?_, ?_⟩271  · constructor272    rw [cellMeasure, MeasureTheory.Measure.smul_apply,273      MeasureTheory.Measure.restrict_apply MeasurableSet.univ,274      Set.univ_inter, h5, smul_eq_mul, ENNReal.inv_mul_cancel hμ0 hμt]275  · intro L b hL hb276    have hsub : {b' : Fin d → O | ∀ j, b' j - b j ∈ (IsLocalRing.maximalIdeal O) ^ L} ⊆ C := by277      rw [h2 b hb]278      exact fun y hy j ↦ Ideal.pow_le_self (by omega) (hy j)279    rw [cellMeasure, MeasureTheory.Measure.smul_apply,280      MeasureTheory.Measure.restrict_apply (hball L b),281      Set.inter_eq_left.mpr hsub, h5, coefficient_cylinder_mass O htop, smul_eq_mul]282    obtain ⟨k, rfl⟩ : ∃ k, L = k + 1 := ⟨L - 1, by omega⟩283    rw [Nat.add_sub_cancel, mul_add, mul_one, pow_add, ← mul_assoc, mul_comm, ← mul_assoc,284      ENNReal.mul_inv_cancel hμ0 hμt, one_mul]285 286/-- The product of the normalized cell measures of a family of form cells is a probability287measure concentrated on the product cell, giving each congruence box mod `m^L` mass288`q^{-(Σ dᵢ)(L-1)}`. -/289theorem form_cell_product_measure (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]290    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]291    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]292    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]293    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (ι : Type) [Fintype ι] (d : ι → ℕ)294    (ν : ∀ i, Fin (d i + 1)) (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O)295    (hgν : ∀ i, g i (ν i) = 1)296    [hσ : ∀ i,297      MeasureTheory.SigmaFinite (cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i)))] :298    MeasureTheory.IsProbabilityMeasure299        (MeasureTheory.Measure.pi300          (fun i ↦ cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i)))) ∧301      (MeasureTheory.Measure.pi (fun i ↦ cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))))302        (Set.pi Set.univ (fun i ↦ reducedFormCell O (d i) (ν i) (g i)))ᶜ = 0 ∧303      ∀ (L : ℕ), 1 ≤ L → ∀ a' ∈ Set.pi Set.univ (fun i ↦ reducedFormCell O (d i) (ν i) (g i)),304        (MeasureTheory.Measure.pi305            (fun i ↦ cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))))306          (Set.pi Set.univ (fun i ↦307            {b : Fin (d i) → O | ∀ j, b j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L})) =308          (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ ((∑ i, d i) * (L - 1)) := by309  have H := fun i ↦ normalized_form_cell_cylinder_mass O htop (d i) (ν i) (g i) (hgν i)310  have : ∀ i, MeasureTheory.IsProbabilityMeasure311      (cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))) := fun i ↦ (H i).2.2.2.2.2.1312  refine ⟨inferInstance, ?_, ?_⟩313  · have hcompl : ∀ i, cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))314        (reducedFormCell O (d i) (ν i) (g i))ᶜ = 0 := by315      intro i316      unfold cellMeasure317      rw [MeasureTheory.Measure.smul_apply,318        MeasureTheory.Measure.restrict_apply (H i).2.2.2.1.compl, Set.compl_inter_self]319      simp320    have hone : ∀ i, cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))321        (reducedFormCell O (d i) (ν i) (g i)) = 1 := fun i ↦322      (MeasureTheory.prob_compl_eq_zero_iff (H i).2.2.2.1).1 (hcompl i)323    rw [MeasureTheory.prob_compl_eq_zero_iff (MeasurableSet.univ_pi fun i ↦ (H i).2.2.2.1),324      MeasureTheory.Measure.pi_pi]325    simp [hone]326  · intro L hL a' ha'327    rw [MeasureTheory.Measure.pi_pi]328    have : ∀ i, cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))329        {b : Fin (d i) → O | ∀ j, b j - a' i j ∈ (IsLocalRing.maximalIdeal O) ^ L} =330        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (d i * (L - 1)) :=331      fun i ↦ (H i).2.2.2.2.2.2 L (a' i) hL (ha' i (Set.mem_univ i))332    simp only [this]333    rw [Finset.prod_pow_eq_pow_sum, Finset.sum_mul]334 335/-! ### Products of fields -/336 337/-- The primitive idempotents of a finite product of fields `∏ Lᵢ` are the unit vectors338`Pi.single i 1`, which are pairwise orthogonal. -/339private theorem pi_fields_primitive_idempotents (ι : Type) [DecidableEq ι] (L : ι → Type)340    [∀ i, Field (L i)] (x : ∀ i, L i) :341    ((IsIdempotentElem x ∧ x ≠ 0 ∧ ∀ y : (∀ i, L i), IsIdempotentElem y → y * x = y →342      y = 0 ∨ y = x) ↔ ∃ i, x = Pi.single i (1 : L i)) ∧343    ∀ i j : ι, i ≠ j → (Pi.single i (1 : L i) : ∀ i, L i) * Pi.single j (1 : L j) = 0 := by344  have idem : ∀ i, IsIdempotentElem (Pi.single i (1 : L i) : ∀ i, L i) := fun i ↦ by345    rw [IsIdempotentElem, ← Pi.single_mul, mul_one]346  refine ⟨⟨?_, ?_⟩, fun i j hij ↦ ?_⟩347  · rintro ⟨hx, hne, hp⟩348    obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := by349      by_contra! h350      exact hne (funext h)351    have hi1 : x i = 1 :=352      (IsIdempotentElem.iff_eq_zero_or_one.mp (congrFun hx i)).resolve_left hi353    refine ⟨i, ?_⟩354    have hy : Pi.single i (1 : L i) * x = Pi.single i 1 := by355      funext l356      by_cases h : l = i357      · subst h; simp [hi1]358      · simp [Pi.single_eq_of_ne h]359    rcases hp _ (idem i) hy with h | h360    · simpa using congrFun h i361    · exact h.symm362  · rintro ⟨i, rfl⟩363    refine ⟨idem i, fun h ↦ by simpa using congrFun h i, fun y hy hyx ↦ ?_⟩364    have hj : ∀ j, j ≠ i → y j = 0 := fun j hj ↦ by365      simpa [Pi.single_eq_of_ne hj] using (congrFun hyx j).symm366    rcases IsIdempotentElem.iff_eq_zero_or_one.mp (congrFun hy i) with h | h367    · left368      funext l369      by_cases hl : l = i370      · subst hl; simpa using h371      · simpa using hj l hl372    · right373      funext l374      by_cases hl : l = i375      · subst hl; simpa using h376      · simp [Pi.single_eq_of_ne hl, hj l hl]377  · funext l378    by_cases h : l = i379    · subst h; simp [Pi.single_eq_of_ne hij]380    · simp [Pi.single_eq_of_ne h]381 382/-- Ring isomorphisms transport primitive idempotents. -/383private lemma isPrimitiveIdempotent_map {A B : Type} [CommRing A] [CommRing B] (f : A ≃+* B) (x : A)384    (h : IsIdempotentElem x ∧ x ≠ 0 ∧ ∀ y, IsIdempotentElem y → y * x = y → y = 0 ∨ y = x) :385    IsIdempotentElem (f x) ∧ f x ≠ 0 ∧386      ∀ y, IsIdempotentElem y → y * f x = y → y = 0 ∨ y = f x := by387  obtain ⟨h1, h2, h3⟩ := h388  refine ⟨h1.map f, by simpa using h2, fun y hy hyx ↦ ?_⟩389  rcases h3 (f.symm y) (hy.map f.symm) (by rw [← f.symm_apply_apply x, ← map_mul, hyx]) with h | h390  · exact .inl (by simpa using congrArg f h)391  · exact .inr (by simpa using congrArg f h)392 393/-- The unit vectors `Pi.single j 1` of a product of fields are pairwise distinct. -/394private lemma pi_single_one_injective {ι : Type} [DecidableEq ι] (L : ι → Type) [∀ i, Field (L i)]395    (j j' : ι) (h : (Pi.single j (1 : L j) : ∀ i, L i) = Pi.single j' (1 : L j')) : j = j' := by396  by_contra hne397  have := congrFun h j398  rw [Pi.single_eq_same, Pi.single_eq_of_ne hne] at this399  exact one_ne_zero this400 401/-- If `e` sends the `i`-th unit vector to the `j`-th one, it sends the `i`-th factor into402the `j`-th factor. -/403private lemma algEquiv_single_eq_single {K ι ι' : Type} [Field K] [DecidableEq ι] [DecidableEq ι']404    (L : ι → Type) (L' : ι' → Type) [∀ i, Field (L i)] [∀ i, Field (L' i)]405    [∀ i, Algebra K (L i)] [∀ i, Algebra K (L' i)] (e : (∀ i, L i) ≃ₐ[K] (∀ i, L' i))406    (i : ι) (j : ι') (hij : e (Pi.single i (1 : L i)) = Pi.single j (1 : L' j)) (x : L i) :407    e (Pi.single i x) = Pi.single j (e (Pi.single i x) j) := by408  have h2 : e (Pi.single i x) = e (Pi.single i x) * Pi.single j 1 := by409    conv_lhs => rw [← mul_one x, Pi.single_mul]410    rw [map_mul, hij]411  funext k412  by_cases hk : k = j413  · subst hk; simp414  · rw [h2, Pi.mul_apply, Pi.single_eq_of_ne hk, Pi.single_eq_of_ne hk, mul_zero]415 416open scoped Classical in417/-- A `K`-algebra isomorphism of finite products of fields `∏ Lᵢ ≃ ∏ L'ⱼ` is induced by a418bijection `π` of the index sets and isomorphisms `Lᵢ ≃ L'_{π i}`. -/419theorem pi_fields_algEquiv_index_bijection (K ι ι' : Type) [Field K]420    (L : ι → Type) (L' : ι' → Type) [∀ i, Field (L i)] [∀ i, Field (L' i)]421    [∀ i, Algebra K (L i)] [∀ i, Algebra K (L' i)] (e : (∀ i, L i) ≃ₐ[K] (∀ i, L' i)) :422    ∃ π : ι ≃ ι', ∀ i, e (Pi.single i (1 : L i)) = Pi.single (π i) (1 : L' (π i)) ∧423      ∃ φ : L i ≃ₐ[K] L' (π i), ∀ x : L i, e (Pi.single i x) = Pi.single (π i) (φ x) := by424  have hj : ∀ i, ∃ j, e (Pi.single i (1 : L i)) = Pi.single j (1 : L' j) := fun i ↦425    (pi_fields_primitive_idempotents ι' L' _).1.1426      (isPrimitiveIdempotent_map e.toRingEquiv _427        ((pi_fields_primitive_idempotents ι L _).1.2 ⟨i, rfl⟩))428  have hj' : ∀ j, ∃ i, e.symm (Pi.single j (1 : L' j)) = Pi.single i (1 : L i) := fun j ↦429    (pi_fields_primitive_idempotents ι L _).1.1430      (isPrimitiveIdempotent_map e.symm.toRingEquiv _431        ((pi_fields_primitive_idempotents ι' L' _).1.2 ⟨j, rfl⟩))432  choose f hf using hj433  choose g hg using hj'434  let π : ι ≃ ι' :=435    { toFun := f436      invFun := g437      left_inv := fun i ↦ pi_single_one_injective L _ _ <| by438        rw [← hg, ← hf, AlgEquiv.symm_apply_apply]439      right_inv := fun j ↦ pi_single_one_injective L' _ _ <| by440        rw [← hf, ← hg, AlgEquiv.apply_symm_apply] }441  refine ⟨π, fun i ↦ ⟨hf i, ?_⟩⟩442  have hs := algEquiv_single_eq_single L L' e i (f i) (hf i)443  let φ₀ : L i →ₐ[K] L' (f i) :=444    { toFun := fun x ↦ e (Pi.single i x) (f i)445      map_one' := by simp only [hf i, Pi.single_eq_same]446      map_mul' := fun x y ↦ by simp only [Pi.single_mul, map_mul, Pi.mul_apply]447      map_zero' := by simp448      map_add' := fun x y ↦ by simp only [Pi.single_add, map_add, Pi.add_apply]449      commutes' := fun c ↦ by450        simp only [Algebra.algebraMap_eq_smul_one, Pi.single_smul, map_smul, hf i,451          Pi.smul_apply, Pi.single_eq_same] }452  have hbij : Function.Bijective φ₀ := by453    refine ⟨φ₀.toRingHom.injective, fun y ↦ ⟨e.symm (Pi.single (f i) y) i, ?_⟩⟩454    have := congrArg e (algEquiv_single_eq_single L' L e.symm (f i) i455      (by rw [← hf i, AlgEquiv.symm_apply_apply]) y)456    rw [AlgEquiv.apply_symm_apply, hs] at this457    exact (Pi.single_injective (f i) this).symm458  exact ⟨AlgEquiv.ofBijective φ₀ hbij, hs⟩459 460/-! ### Polynomial congruences and the Chinese remainder theorem -/461 462/-- Two polynomials agree modulo `I` iff their coefficients do, and coefficientwise congruence463mod `I` is preserved by finite products. -/464theorem polynomial_congruence_and_product (O : Type) [CommRing O] (I : Ideal O) :465    (∀ P Q : Polynomial O, P.map (Ideal.Quotient.mk I) = Q.map (Ideal.Quotient.mk I) ↔466        ∀ j, P.coeff j - Q.coeff j ∈ I) ∧467      (∀ (ι : Type) [Fintype ι] (F F' : ι → Polynomial O),468        (∀ i j, (F i).coeff j - (F' i).coeff j ∈ I) →469          ∀ j, (∏ i, F i).coeff j - (∏ i, F' i).coeff j ∈ I) := by470  have h1 : ∀ P Q : Polynomial O, P.map (Ideal.Quotient.mk I) = Q.map (Ideal.Quotient.mk I) ↔471      ∀ j, P.coeff j - Q.coeff j ∈ I := fun P Q ↦ by472    simp only [Polynomial.ext_iff, Polynomial.coeff_map, Ideal.Quotient.eq]473  refine ⟨h1, fun ι _ F F' h ↦ ?_⟩474  rw [← h1, Polynomial.map_prod, Polynomial.map_prod]475  exact Finset.prod_congr rfl fun i _ ↦ (h1 _ _).2 (h i)476 477/-- For distinct monic irreducibles `gᵢ` over a field, `K[X]/(∏ gᵢ) ≃ ∏ K[X]/(gᵢ)` (Chinese478remainder), compatibly with `mk`. -/479theorem polynomial_quotient_product_equiv (K : Type) [Field K] (gs : List (Polynomial K))480    (hgs : ∀ g ∈ gs, g.Monic ∧ Irreducible g) (hd : gs.Pairwise (fun g h ↦ g ≠ h)) :481    ∃ e : AdjoinRoot gs.prod ≃ₐ[K] (∀ i : Fin gs.length, AdjoinRoot (gs.get i)),482      ∀ (P : Polynomial K) (i : Fin gs.length),483        e (AdjoinRoot.mk gs.prod P) i = AdjoinRoot.mk (gs.get i) P := by484  have hcop : ∀ i j : Fin gs.length, i ≠ j → IsCoprime (gs.get i) (gs.get j) := fun i j hij ↦485    distinct_monic_irreducible_coprime K _ _ (hgs _ (List.get_mem gs i)).1486      (hgs _ (List.get_mem gs j)).1 (hgs _ (List.get_mem gs i)).2 (hgs _ (List.get_mem gs j)).2487      fun h ↦ hij (List.Nodup.injective_get hd h)488  let f : Fin gs.length → Ideal (Polynomial K) := fun i ↦ Ideal.span {gs.get i}489  have heq : Ideal.span {gs.prod} = ⨅ i, f i := by490    rw [Ideal.iInf_span_singleton hcop, ← List.prod_ofFn, List.ofFn_get]491  let e1 : AdjoinRoot gs.prod ≃+* (∀ i : Fin gs.length, AdjoinRoot (gs.get i)) :=492    (Ideal.quotEquivOfEq heq).trans (Ideal.quotientInfRingEquivPiQuotient f fun i j hij ↦493      (Ideal.isCoprime_span_singleton_iff _ _).mpr (hcop i j hij))494  have hmk : ∀ P : Polynomial K, ∀ i, e1 (AdjoinRoot.mk gs.prod P) i = AdjoinRoot.mk (gs.get i) P :=495    fun P i ↦ rfl496  refine ⟨AlgEquiv.ofRingEquiv (f := e1) fun c ↦ funext fun i ↦ ?_, hmk⟩497  rw [AdjoinRoot.algebraMap_eq, AdjoinRoot.of, RingHom.comp_apply, hmk]498  rfl499 500/-! ### Root fields along a conjugate orbit -/501 502/-- If `L/K` is finite of degree `d`, `g` is monic irreducible over `L` dividing the monic503irreducible `H` over `K`, and `deg H = d · deg g`, then `K[X]/(H) ≃ L[X]/(g)` over `K`. -/504private theorem adjoinRoot_algEquiv_of_dvd_map (K L : Type) [Field K] [Field L] [Algebra K L]505    [Module.Finite K L] (d : ℕ) (hd : Module.finrank K L = d)506    (g : Polynomial L) (hg : g.Monic) (hgi : Irreducible g)507    (H : Polynomial K) (hH : H.Monic) (hHi : Irreducible H)508    (hdiv : g ∣ H.map (algebraMap K L)) (hdeg : H.natDegree = d * g.natDegree) :509    Nonempty (AdjoinRoot H ≃ₐ[K] AdjoinRoot g) := by510  have : Fact (Irreducible H) := ⟨hHi⟩511  have : Fact (Irreducible g) := ⟨hgi⟩512  have h₀ : H.eval₂ (algebraMap K (AdjoinRoot g)) (AdjoinRoot.root g) = 0 := by513    obtain ⟨Q, hQ⟩ := hdiv514    rw [IsScalarTower.algebraMap_eq K L (AdjoinRoot g), ← Polynomial.eval₂_map, hQ,515      Polynomial.eval₂_mul, show g.eval₂ (algebraMap L (AdjoinRoot g)) (AdjoinRoot.root g) = 0 from516        AdjoinRoot.eval₂_root g, zero_mul]517  let φ := AdjoinRoot.liftAlgHom H (Algebra.ofId K (AdjoinRoot g)) (AdjoinRoot.root g) h₀518  have hinj : Function.Injective φ := φ.toRingHom.injective519  have : Module.Finite L (AdjoinRoot g) := (AdjoinRoot.powerBasis hg.ne_zero).finite520  have : Module.Finite K (AdjoinRoot g) := .trans L (AdjoinRoot g)521  have : Module.Finite K (AdjoinRoot H) := (AdjoinRoot.powerBasis hH.ne_zero).finite522  have hsurj : Function.Surjective φ.toLinearMap :=523    (LinearMap.injective_iff_surjective_of_finrank_eq_finrank (by524      rw [(AdjoinRoot.powerBasis hH.ne_zero).finrank, AdjoinRoot.powerBasis_dim,525        ← Module.finrank_mul_finrank K L (AdjoinRoot g), (AdjoinRoot.powerBasis hg.ne_zero).finrank,526        AdjoinRoot.powerBasis_dim, hd, hdeg])).mp hinj527  exact ⟨AlgEquiv.ofBijective φ ⟨hinj, hsurj⟩⟩528 529/-- For the unramified extension `Kδ/K` of degree `δ = deg Φ`, a monic irreducible `g` over `Kδ`530dividing a monic irreducible `H` over `K` of degree `δ · deg g` has `K[X]/(H) ≃ Kδ[X]/(g)`. -/531theorem root_field_algEquiv_conjugate_orbit (O : Type) [CommRing O] [IsDomain O]532    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]533    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O)534    [IsDomain (AdjoinRoot Φ)] (ι : BaseField O →+* BaseField (AdjoinRoot Φ))535    (hfin : letI := ι.toAlgebra; Module.Finite (BaseField O) (BaseField (AdjoinRoot Φ))536    ∧ Module.finrank (BaseField O) (BaseField (AdjoinRoot Φ)) = Φ.natDegree)537    (g : Polynomial (BaseField (AdjoinRoot Φ))) (hg : g.Monic) (hgi : Irreducible g)538    (H : Polynomial (BaseField O)) (hH : H.Monic) (hHi : Irreducible H) (hdiv : g ∣ H.map ι)539    (hdeg : H.natDegree = Φ.natDegree * g.natDegree) :540    letI := ι.toAlgebra; Nonempty (AdjoinRoot H ≃ₐ[BaseField O] AdjoinRoot g) := by541  let := ι.toAlgebra542  have := hfin.1543  exact adjoinRoot_algEquiv_of_dvd_map (BaseField O) (BaseField (AdjoinRoot Φ)) Φ.natDegree hfin.2544      g hg hgi H hH545    hHi hdiv hdeg546 547end SurfaceBlowup