Transport of factorization types and cell measures

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.Blowup.StrictNormalizer7 8/-!9# Transport of factorization types and cell measures10 11This file collects transport statements: the factorization type of a monic polynomial is12invariant under Taylor shift and additive over coprime products, monic irreducible residue13polynomials lift to unramified lifts, a congruence-preserving mass-preserving bijection of14cells transports normalized cell measures, coordinate hyperplanes are null, and scaling by a15uniformizer multiplies coefficient measure by `q⁻ʳ`.16 17## Main results18 19* `SurfaceBlowup.block_translation_type_iff`: Taylor shift preserves the factorization type.20* `SurfaceBlowup.coprime_family_type_iff`: types of pairwise coprime products are sums.21* `SurfaceBlowup.exists_unramified_lift`: existence of unramified lifts of the same degree.22* `SurfaceBlowup.cell_transport_preimage`: transport of normalized cell measures.23* `SurfaceBlowup.coordinate_hyperplane_null`: coordinate hyperplanes have measure zero.24* `SurfaceBlowup.scaling_image_borel_mass`: the scaling image has mass `q⁻ʳ` times the original.25 26Provenance: `Thm_SurfaceBlowupV2_{block_translation_type_iff, coprime_family_type_iff,27exists_unramified_lift, cell_transport_preimage, coordinate_hyperplane_null,28scaling_image_borel_mass}`.29-/30 31open scoped BigOperators ENNReal32 33namespace SurfaceBlowup34 35/-- The factorization type of a monic polynomial over `O` (viewed over the fraction field) is36invariant under the Taylor shift `X ↦ X + θ`. -/37theorem block_translation_type_iff (O : Type) [CommRing O] [IsDomain O]38    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]39    [Finite (IsLocalRing.ResidueField O)] (F : Polynomial O) (hF : F.Monic) (θ : O)40    (σ : FactorType) :41    HasPolynomialTypeF O (F.map (algebraMap O (BaseField O))) σ ↔42      HasPolynomialTypeF O ((Polynomial.taylor θ F).map (algebraMap O (BaseField O))) σ := by43  set K := BaseField O44  have h1 : (Polynomial.taylor θ F).map (algebraMap O K)45      = (Polynomial.algEquivAevalXAddC (algebraMap O K θ)) (F.map (algebraMap O K)) := by46    rw [Polynomial.taylor_apply, Polynomial.algEquivAevalXAddC_apply, ← Polynomial.comp_eq_aeval,47      Polynomial.map_comp]48    simp49  have hm : (Polynomial.taylor θ F).Monic := by50    rw [Polynomial.Monic, Polynomial.leadingCoeff_taylor]; exact hF51  have hI : (Ideal.span {F.map (algebraMap O K)}).map52      (Polynomial.algEquivAevalXAddC (algebraMap O K θ)).toRingEquiv.toRingHom53      = Ideal.span {(Polynomial.taylor θ F).map (algebraMap O K)} := by54    rw [Ideal.map_span, Set.image_singleton, h1]; rfl55  exact polynomial_type_algEquiv_iff O _ _ (hF.map _) (hm.map _)56    (Ideal.quotientEquivAlg _ _ (Polynomial.algEquivAevalXAddC (algebraMap O K θ)) hI.symm) σ57 58/-- For a finite family of monic, pairwise coprime polynomials, the product has type `σ`59exactly when `σ` is the sum of types of the factors. -/60theorem coprime_family_type_iff (O : Type) [CommRing O] [IsDomain O] (ι : Type) [Fintype ι]61    (F : ι → Polynomial (BaseField O)) (hF : ∀ i, (F i).Monic)62    (hc : ∀ i j, i ≠ j → IsCoprime (F i) (F j)) (σ : FactorType) :63    HasPolynomialTypeF O (∏ i, F i) σ ↔64      ∃ τ : ι → FactorType, (∀ i, HasPolynomialTypeF O (F i) (τ i)) ∧ σ = ∑ i, τ i := by65  classical66  have key : ∀ τ : ι → FactorType, (∀ i, HasPolynomialTypeF O (F i) (τ i)) →67      ∀ s : Finset ι, HasPolynomialTypeF O (∏ i ∈ s, F i) (∑ i ∈ s, τ i) := by68    intro τ hτ s69    induction s using Finset.induction_on with70    | empty => exact ⟨[], by simp⟩71    | insert a s ha ih =>72      rw [Finset.prod_insert ha, Finset.sum_insert ha]73      exact polynomial_type_mul_coprime O _ _ _ _ (hτ a) ih74        (IsCoprime.prod_right fun i hi ↦ hc a i fun h ↦ ha (h ▸ hi))75  refine ⟨fun h ↦ ?_, fun ⟨τ, hτ, hσ⟩ ↦ hσ ▸ key τ hτ Finset.univ⟩76  choose τ hτ using fun i ↦77    polynomial_type_dvd O _ (F i) σ h (hF i) (Finset.dvd_prod_of_mem _ (Finset.mem_univ i))78  exact ⟨τ, hτ, polynomial_type_unique O _ _ _ h (key τ hτ Finset.univ)⟩79 80/-- Every monic irreducible residue polynomial `φ` has an unramified lift `Φ` over `O` of the81same degree. -/82theorem exists_unramified_lift (O : Type) [CommRing O] [IsLocalRing O]83    (φ : Polynomial (IsLocalRing.ResidueField O)) (hφ : φ.Monic) (hirr : Irreducible φ) :84    ∃ Φ : Polynomial O,85      IsUnramifiedLift O Φ ∧ residuePoly O Φ = φ ∧ Φ.natDegree = φ.natDegree := by86  obtain ⟨a, ha⟩ := (residue_cell_cylinder O φ.natDegree φ).2.1 hφ rfl87  obtain ⟨h1, h2, -, -⟩ := monic_poly_reconstruct O φ.natDegree a88  have ha' : residuePoly O (monicPolyO a) = φ := ha89  exact ⟨monicPolyO a, ⟨h1, ha'.symm ▸ hirr⟩, ha', h2⟩90 91/-- The normalized measure of a measurable cell, as a quotient of coefficient measures. -/92theorem cellMeasure_apply_of_measurableSet (O : Type) [CommRing O] [IsDomain O]93    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]94    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] (n : ℕ) (S : Set (Fin n → O))95    (hS : MeasurableSet S) (s : Set (Fin n → O)) :96    cellMeasure O n S s = (coefficientMeasure O n S)⁻¹ * coefficientMeasure O n (s ∩ S) := by97  simp [cellMeasure, MeasureTheory.Measure.restrict_apply' hS]98 99/-- The normalized measure of a measurable cell `S` only sees the trace on `S`. -/100theorem cellMeasure_cell_inter {O : Type} [CommRing O] [IsDomain O] [TopologicalSpace O]101    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]102    [MeasurableSpace O] [BorelSpace O] {n : ℕ} {S : Set (Fin n → O)} (hS : MeasurableSet S)103    (T : Set (Fin n → O)) : cellMeasure O n S (S ∩ T) = cellMeasure O n S T := by104  simp [cellMeasure, MeasureTheory.Measure.restrict_apply' hS, Set.inter_comm S T,105    Set.inter_assoc]106 107/-- The normalized measure of a measurable cell of positive mass is a probability measure. -/108private theorem cellMeasure_univ (O : Type) [CommRing O] [IsDomain O]109    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]110    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]111    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]112    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (S : Set (Fin n → O))113    (hS : MeasurableSet S) (h : coefficientMeasure O n S ≠ 0) :114    cellMeasure O n S Set.univ = 1 := by115  have := coefficient_measure_probability O htop n116  rw [cellMeasure_apply_of_measurableSet O n S hS, Set.univ_inter]117  exact ENNReal.inv_mul_cancel h (MeasureTheory.measure_ne_top _ _)118 119/-- A bijection `f : S₁ → S₂` between coefficient cells that preserves `𝔪ᴸ`-congruence and120the normalized masses of all congruence balls of level `L ≥ 1` transports the normalized cell121measure: `f⁻¹' T` has the same measure in `S₁` as `T` in `S₂`. -/122theorem cell_transport_preimage (O₁ : Type) [CommRing O₁] [IsDomain O₁]123    [IsDiscreteValuationRing O₁] [IsAdicComplete (IsLocalRing.maximalIdeal O₁) O₁]124    [Finite (IsLocalRing.ResidueField O₁)] [TopologicalSpace O₁] [IsTopologicalRing O₁]125    [CompactSpace O₁] [T2Space O₁] [SecondCountableTopology O₁] [MeasurableSpace O₁]126    [BorelSpace O₁] (htop₁ : IsAdic (IsLocalRing.maximalIdeal O₁)) (O₂ : Type) [CommRing O₂]127    [IsDomain O₂] [IsDiscreteValuationRing O₂] [IsAdicComplete (IsLocalRing.maximalIdeal O₂) O₂]128    [Finite (IsLocalRing.ResidueField O₂)] [TopologicalSpace O₂] [IsTopologicalRing O₂]129    [CompactSpace O₂] [T2Space O₂] [SecondCountableTopology O₂] [MeasurableSpace O₂]130    [BorelSpace O₂] (htop₂ : IsAdic (IsLocalRing.maximalIdeal O₂)) (n₁ n₂ : ℕ)131    (S₁ : Set (Fin n₁ → O₁)) (S₂ : Set (Fin n₂ → O₂)) (hS₁ : MeasurableSet S₁)132    (hS₂ : MeasurableSet S₂) (h₁ : coefficientMeasure O₁ n₁ S₁ ≠ 0)133    (h₂ : coefficientMeasure O₂ n₂ S₂ ≠ 0) (f : (Fin n₁ → O₁) → (Fin n₂ → O₂))134    (hf : Set.BijOn f S₁ S₂)135    (hcong : ∀ (L : ℕ), ∀ a ∈ S₁, ∀ a' ∈ S₁, (∀ j, a j - a' j ∈ (IsLocalRing.maximalIdeal O₁) ^ L)136      ↔ ∀ j, f a j - f a' j ∈ (IsLocalRing.maximalIdeal O₂) ^ L)137    (hmass : ∀ (L : ℕ), 1 ≤ L → ∀ a ∈ S₁,138      cellMeasure O₁ n₁ S₁ {a' | ∀ j, a' j - a j ∈ (IsLocalRing.maximalIdeal O₁) ^ L} =139        cellMeasure O₂ n₂ S₂ {b | ∀ j, b j - f a j ∈ (IsLocalRing.maximalIdeal O₂) ^ L}) :140    ∀ T : Set (Fin n₂ → O₂), MeasurableSet T →141      MeasurableSet (S₁ ∩ f ⁻¹' T) ∧ cellMeasure O₁ n₁ S₁ (f ⁻¹' T) = cellMeasure O₂ n₂ S₂ T := by142  classical143  set m₁ := IsLocalRing.maximalIdeal O₁144  set m₂ := IsLocalRing.maximalIdeal O₂145  have hgen₂ := finite_coordinate_borel_cylinders O₂ m₂ htop₂ n₂146  have ht : ∀ (L : ℕ) (x : Fin n₂ → O₂),147      {y | adicCongr m₂ L y x} = {y : Fin n₂ → O₂ | ∀ j, y j - x j ∈ m₂ ^ L} := fun L x ↦ by148    ext y; simp only [Set.mem_ofPred_eq, finite_coordinate_adic_congruence]149  -- the trace on `S₁` of the `f`-preimage of a ball is a ball around a point of `S₁`, or empty150  have htrace : ∀ (L : ℕ) (x : Fin n₂ → O₂),151      (∃ a₀ ∈ S₁, S₁ ∩ f ⁻¹' {y | ∀ j, y j - x j ∈ m₂ ^ L} = S₁ ∩ {y | ∀ j, y j - a₀ j ∈ m₁ ^ L}152        ∧ {y : Fin n₂ → O₂ | ∀ j, y j - x j ∈ m₂ ^ L} = {y | ∀ j, y j - f a₀ j ∈ m₂ ^ L}) ∨153      (S₁ ∩ f ⁻¹' {y | ∀ j, y j - x j ∈ m₂ ^ L} = ∅ ∧154        {y : Fin n₂ → O₂ | ∀ j, y j - x j ∈ m₂ ^ L} ∩ S₂ = ∅) := by155    intro L x156    rcases Set.eq_empty_or_nonempty ({y : Fin n₂ → O₂ | ∀ j, y j - x j ∈ m₂ ^ L} ∩ S₂) with157      hne | ⟨b, hbB, hbS⟩158    · exact Or.inr ⟨Set.eq_empty_of_forall_notMem fun a ⟨ha, hB⟩ ↦159        hne.subset ⟨hB, hf.mapsTo ha⟩, hne⟩160    obtain ⟨a₀, ha₀, rfl⟩ := hf.surjOn hbS161    have hB : {y : Fin n₂ → O₂ | ∀ j, y j - x j ∈ m₂ ^ L} = {y | ∀ j, y j - f a₀ j ∈ m₂ ^ L} :=162      Set.ext fun y ↦ ⟨fun hy j ↦ by simpa using (m₂ ^ L).sub_mem (hy j) (hbB j),163        fun hy j ↦ by simpa using (m₂ ^ L).add_mem (hy j) (hbB j)⟩164    refine Or.inl ⟨a₀, ha₀, Set.ext fun a ↦ ?_, hB⟩165    simp only [Set.mem_inter_iff, Set.mem_preimage, hB]166    exact and_congr_right fun ha ↦ (hcong L a ha a₀ ha₀).symm167  -- extend `f` outside `S₁` by a constant to get a measurable map168  obtain ⟨b₀, -⟩ : S₂.Nonempty := Set.nonempty_iff_ne_empty.2 fun h ↦ h₂ (h ▸ by simp)169  let g : (Fin n₁ → O₁) → (Fin n₂ → O₂) := fun a ↦ if a ∈ S₁ then f a else b₀170  have hgS : ∀ T : Set (Fin n₂ → O₂), S₁ ∩ g ⁻¹' T = S₁ ∩ f ⁻¹' T := fun T ↦171    Set.ext fun a ↦ by by_cases ha : a ∈ S₁ <;> simp [g, ha]172  have hgmeas : Measurable g := by173    have : @Measurable _ _ _ (adicCylinderSpace m₂ (Fin n₂ → O₂)) g := by174      refine measurable_generateFrom ?_175      rintro t (rfl | ⟨L, x, rfl⟩)176      · simp177      have hg : g ⁻¹' {y | adicCongr m₂ L y x} =178          (S₁ ∩ g ⁻¹' {y | adicCongr m₂ L y x}) ∪ (S₁ᶜ ∩ {_a | b₀ ∈ {y | adicCongr m₂ L y x}}) :=179        Set.ext fun a ↦ by by_cases ha : a ∈ S₁ <;> simp [g, ha]180      rw [hg, hgS, ht]181      refine MeasurableSet.union ?_ (hS₁.compl.inter (MeasurableSet.const _))182      rcases htrace L x with ⟨a₀, -, h, -⟩ | ⟨h, -⟩ <;> rw [h]183      exacts [hS₁.inter ((coordinate_cylinder_clopen O₁ m₁ htop₁ L).1 n₁ a₀).2.measurableSet,184        .empty]185    rwa [← hgen₂] at this186  have hρ₁ := cellMeasure_apply_of_measurableSet O₁ n₁ S₁ hS₁187  have hρ₂ := cellMeasure_apply_of_measurableSet O₂ n₂ S₂ hS₂188  have hone₁ := cellMeasure_univ O₁ htop₁ n₁ S₁ hS₁ h₁189  have hone₂ := cellMeasure_univ O₂ htop₂ n₂ S₂ hS₂ h₂190  have : MeasureTheory.IsFiniteMeasure (cellMeasure O₂ n₂ S₂) := ⟨by simp [hone₂]⟩191  have hpush : ∀ T : Set (Fin n₂ → O₂), MeasurableSet T →192      (cellMeasure O₁ n₁ S₁).map g T = cellMeasure O₁ n₁ S₁ (f ⁻¹' T) := fun T hT ↦ by193    rw [MeasureTheory.Measure.map_apply hgmeas hT, hρ₁, hρ₁, Set.inter_comm, hgS, Set.inter_comm]194  have hEq : cellMeasure O₂ n₂ S₂ = (cellMeasure O₁ n₁ S₁).map g := by195    refine finite_measures_from_cylinders O₂ (Fin n₂ → O₂) m₂ _ _ hgen₂ fun L x ↦ ?_196    rw [ht, hpush _ ((coordinate_cylinder_clopen O₂ m₂ htop₂ L).1 n₂ x).2.measurableSet]197    rcases Nat.eq_zero_or_pos L with rfl | hL198    · simp only [pow_zero, Ideal.one_eq_top, Submodule.mem_top, implies_true, Set.ofPred_true,199        Set.preimage_univ, hone₁, hone₂]200    rcases htrace L x with ⟨a₀, ha₀, h, hB⟩ | ⟨h, hB⟩201    · rw [hρ₁, Set.inter_comm, h, Set.inter_comm, ← hρ₁, hmass L hL a₀ ha₀, hB]202    · rw [hρ₁, hρ₂, hB, Set.inter_comm (f ⁻¹' _), h]; simp203  exact fun T hT ↦ ⟨hgS T ▸ hS₁.inter (hgmeas hT), by rw [← hpush T hT, ← hEq]⟩204 205/-- A coordinate hyperplane `{b | b j = 0}` is measurable and null for the coefficient206measure. -/207theorem coordinate_hyperplane_null (O : Type) [CommRing O] [IsDomain O]Discriminant locus is null208    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]209    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]210    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]211    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (j : Fin n) :212    MeasurableSet {b : Fin n → O | b j = 0} ∧213      coefficientMeasure O n {b : Fin n → O | b j = 0} = 0 := by214  have hcl : IsClosed {b : Fin n → O | b j = 0} :=215    isClosed_eq (continuous_apply j) continuous_const216  refine ⟨hcl.measurableSet, ?_⟩217  have := coefficient_measure_probability O htop n218  have : MeasureTheory.Measure.IsAddLeftInvariant (coefficientMeasure O n) := by219    unfold coefficientMeasure; infer_instance220  set m := IsLocalRing.maximalIdeal O221  set q := Nat.card (IsLocalRing.ResidueField O)222  have hq1 : 1 < q := Finite.one_lt_card_iff_nontrivial.2 inferInstance223  have key : ∀ L : ℕ, coefficientMeasure O n {b : Fin n → O | b j = 0} ≤ ((q : ℝ≥0∞)⁻¹) ^ L := by224    intro L225    have hcard : Nat.card (O ⧸ m ^ L) = q ^ L := residue_quotient_card O L226    have : Finite (O ⧸ m ^ L) := Nat.finite_of_card_ne_zero (by rw [hcard]; positivity)227    let π : (Fin n → O) →+ (O ⧸ m ^ L) :=228      (Ideal.Quotient.mk (m ^ L)).toAddMonoidHom.comp (Pi.evalAddMonoidHom (fun _ ↦ O) j)229    have hπ : ∀ b, π b = Ideal.Quotient.mk (m ^ L) (b j) := fun b ↦ rfl230    have hsurj : Function.Surjective π := fun c ↦ by231      obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective c232      exact ⟨fun _ ↦ y, rfl⟩233    have hm : ∀ a, MeasurableSet {x | π x = a} := by234      intro a235      obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective a236      have h1 := (coordinate_cylinder_clopen O m htop L).1 1 (fun _ ↦ y)237      have : {x : Fin n → O | π x = Ideal.Quotient.mk (m ^ L) y}238          = (fun b : Fin n → O ↦ fun _ : Fin 1 ↦ b j) ⁻¹'239            {b : Fin 1 → O | ∀ i, b i - (fun _ ↦ y) i ∈ m ^ L} := by240        ext x241        simp only [Set.mem_ofPred_eq, Set.mem_preimage, hπ, Ideal.Quotient.eq]242        exact ⟨fun h _ ↦ h, fun h ↦ h 0⟩243      rw [this]244      exact (h1.1.preimage (continuous_pi fun _ ↦ continuous_apply j)).measurableSet245    have hmass := finite_quotient_event_mass (Fin n → O) (O ⧸ m ^ L)246      (coefficientMeasure O n) π hsurj hm {0}247    have hpre : π ⁻¹' {0} = {b : Fin n → O | b j ∈ m ^ L} := by248      ext b249      simp only [Set.mem_preimage, Set.mem_singleton_iff, hπ, Ideal.Quotient.eq_zero_iff_mem,250        Set.mem_ofPred_eq]251    rw [hpre] at hmass252    have hsub : {b : Fin n → O | b j = 0} ⊆ {b : Fin n → O | b j ∈ m ^ L} := fun b hb ↦ by253      simp_all254    calc _ ≤ _ := MeasureTheory.measure_mono hsub255      _ = _ := hmass256      _ = ((q : ℝ≥0∞)⁻¹) ^ L := by simp [hcard, ENNReal.inv_pow, div_eq_mul_inv]257  have hlt : (q : ℝ≥0∞)⁻¹ < 1 := by rw [ENNReal.inv_lt_one]; exact_mod_cast hq1258  exact le_antisymm (le_of_tendsto_of_tendsto' tendsto_const_nhds259    (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hlt) key) zero_le260 261/-- Scaling by a uniformizer `π` maps a measurable set `T ⊆ Oʳ` to a measurable set of262coefficient measure `q⁻ʳ · μ(T)`, where `q` is the residue field cardinality. -/263theorem scaling_image_borel_mass (O : Type) [CommRing O] [IsDomain O]264    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]265    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]266    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]267    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (pi : O) (hpi : Irreducible pi) (r : ℕ)268    (T : Set (Fin r → O)) (hT : MeasurableSet T) :269    MeasurableSet ((fun z : Fin r → O ↦ pi • z) '' T) ∧270      coefficientMeasure O r ((fun z : Fin r → O ↦ pi • z) '' T) =271        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ r * coefficientMeasure O r T := by272  have e : (fun z : Fin r → O ↦ pi • z) = coordinateScale pi 1 := by273    funext z; simp [coordinateScale]274  refine ⟨?_, by simpa [e] using coordinate_scale_measure O htop pi hpi r 1 T⟩275  have hc : Continuous (fun z : Fin r → O ↦ pi • z) :=276    continuous_pi fun j ↦ continuous_const.mul (continuous_apply j)277  have hi : Function.Injective (fun z : Fin r → O ↦ pi • z) := fun z z' h ↦278    funext fun j ↦ mul_left_cancel₀ hpi.ne_zero (congrFun h j)279  exact (hc.isClosedEmbedding hi).measurableEmbedding.measurableSet_image.2 hT280 281end SurfaceBlowup