Single-state residue ideal counts and Haar-measure transport

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.CurveOrders7import SurfaceBlowup.Surfaces.TruncatedSeries8 9/-!10# Single-state residue ideal counts and Haar-measure transport11 12We count the residue ideals of a single state `k⟦T, X⟧ ⧸ (T^a)` with contact `c` with `T`, deduce13the total state measure `q^(-c)`, and collect general facts on transporting Haar probability14measures: congruence-preserving bijections preserve measure, and a continuous injective homomorphism15from a compact group scales Haar measure by the inverse index of its image.16 17## Main results18 19* `single_residue_ideal_count`20* `single_state_volume`21* `congruence_bijection_measure_preserving`22* `compact_injective_image_measure`23 24Provenance: single_residue_ideal_count, single_state_volume,25congruence_bijection_measure_preserving, compact_image_index_mass, compact_injective_comap_measure,26compact_injective_image_measure.27-/28 29open scoped BigOperators ENNReal30 31namespace SurfaceBlowup32 33/-- The number of single residue ideals of `k⟦T, X⟧ ⧸ (T^a)` with contact `c` with `T` is34  `q^(ac - c)`, where `q = #k`. -/35theorem single_residue_ideal_count (k : Type) [Field k] [Finite k] (a c : ℕ) (ha : 0 < a) :Proposition 3.336    Nat.card (singleResidueIdeals k a c) = (Nat.card k)^(a*c-c) := by37  have hcN : c ≤ a * c := Nat.le_mul_of_pos_left c ha38  have hlen : ∀ F : TwoSeries k, axisQuotientLength k 0 F = c →39      Module.length (TwoSeries k) (TwoSeries k ⧸ (monomialIdeal k a 0 ⊔ Ideal.span {F})) =40        ((a*c : ℕ) : ℕ∞) := by41    intro F hF42    have h5 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a 0) (Ideal.span {F})43    rw [Ideal.map_span, Set.image_singleton] at h544    rw [← h5, single_special_fiber_length k a c ha _45      (by rw [contact_fiberT_eq_axisQuotientLength k a 0 ha, hF]), Nat.cast_mul]46  have : Finite (IsLocalRing.ResidueField (TwoSeries k)) :=47    .of_equiv _ (twoSeriesResidueEquiv k).toEquiv.symm48  have hmem : ∀ j < a*c+1, ((0:ℕ), j) ∈ truncIndex a 0 (a*c+1) := by49    intro j hj; simp [truncIndex]; omega50  have hE : ∀ j, truncExponent ((0:ℕ), j) = Finsupp.single 1 j := by simp [truncExponent]51  let A : Finset (truncIndex a 0 (a*c+1)) := Finset.univ.filter (fun s => s.1.1 = 0 ∧ s.1.2 < c)52  let B : Finset (truncIndex a 0 (a*c+1)) := {⟨(0, c), hmem c (by omega)⟩}53  have hA : A.card = c := card_truncIndex_axis_segment a 0 _ c Prod.fst Prod.snd ((0, ·))54    (fun _ => ⟨rfl, rfl⟩) (fun x h => Prod.ext h.symm rfl) fun j hj => hmem j (by omega)55  have key := principal_residue_ideal_count k a 0 (a*c) ha (axisQuotientLength k 0 · = c)56    (contact · (fiberT k a 0) = c) (fun F => by rw [contact_fiberT_eq_axisQuotientLength k a 0 ha])57    (fun U F hU hF => by rwa [axisQuotientLength, Ideal.span_singleton_mul_left_unit hU])58    hlen (fun F hF => by59      rw [finite_length_module_card (TwoSeries k) _ _ (hlen F hF),60        Nat.card_congr (twoSeriesResidueEquiv k).toEquiv])61    A B (by simp [A, B]) (Finset.singleton_nonempty _) (fun F => by62      rw [axisQuotientLength_eq_iff k (s := 0) (t := 1) (by decide)]63      simp only [A, B, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton,64        forall_eq, truncCoeffs_apply, hE]65      refine and_congr_left' ⟨fun h ⟨⟨i, j⟩, _⟩ ⟨hi, hj⟩ => ?_,66        fun h j hj => by simpa [hE] using h ⟨_, hmem j (by omega)⟩ ⟨rfl, hj⟩⟩67      obtain rfl : i = 0 := hi68      rw [hE]; exact h j hj)69  rw [hA, Finset.card_singleton, pow_one, Nat.add_sub_cancel,70    show a * c = c + (a * c - c) by omega, pow_add] at key71  have hpos : 0 < (Nat.card k - 1) * Nat.card k ^ c :=72    Nat.mul_pos (by have := Finite.one_lt_card (α := k); omega) (pow_pos Nat.card_pos _)73  unfold singleResidueIdeals74  exact Nat.eq_of_mul_eq_mul_left hpos (by linarith [key])75 76/-- The total state measure of a single state with contact `c` is `q^(-c)`, where `q` is the residue77  cardinality. -/78theorem single_state_volume (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Proposition 3.379    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]80    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]81    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]82    (htop : IsAdic (IsLocalRing.maximalIdeal O)) [CommRing R] [Algebra O R]83    [MeasurableSpace (Ideal R)] (pi : O) (X : Set (Ideal R))84    (a c : ℕ) (ha : 0 < a) (A : IdealAtlas O R pi (a * c) X)85    (hA : ∀ i, Measurable (coordinateIdeal pi (A.chart i).f (A.chart i).b))86    (hcount : Nonempty (A.ι ≃ singleResidueIdeals (IsLocalRing.ResidueField O) a c)) :87    stateMeasure O R pi (a*c) (Nat.card (IsLocalRing.ResidueField O)) A Set.univ =88      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^c := by89  rw [state_measure_total_mass O R htop pi (a*c) X A hA]90  obtain ⟨e⟩ := hcount91  have hcard : Fintype.card A.ι = Nat.card (IsLocalRing.ResidueField O) ^ (a*c-c) := by92    rw [← Nat.card_eq_fintype_card, Nat.card_congr e,93      single_residue_ideal_count _ a c ha]94  rw [hcard]95  set q := Nat.card (IsLocalRing.ResidueField O)96  have hq : 0 < q := Nat.card_pos97  have hq0 : (q : ℝ≥0∞) ≠ 0 := by exact_mod_cast hq.ne'98  have hqt : (q : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top q99  have hle : c ≤ a * c := Nat.le_mul_of_pos_left c ha100  obtain ⟨m, hm⟩ : ∃ m, a * c = m + c := ⟨a*c - c, (Nat.sub_add_cancel hle).symm⟩101  rw [hm, Nat.add_sub_cancel, pow_add]102  push_cast103  rw [← mul_assoc, ← mul_pow, ENNReal.mul_inv_cancel hq0 hqt, one_pow, one_mul]104 105/-- A surjection preserving every adic congruence preserves any probability measure on adic106  cylinders that gives all balls of the same radius the same mass. -/107theorem congruence_bijection_measure_preserving (O V : Type) [CommRing O] [AddCommGroup V]108    [Module O V] (I : Ideal O) [MeasurableSpace V]109    (hgen : ‹MeasurableSpace V› = adicCylinderSpace I V) (F : V → V) (honto : Function.Surjective F)110    (hcong : ∀ j x y, adicCongr I j (F x) (F y) ↔ adicCongr I j x y) (mu : MeasureTheory.Measure V)111    [MeasureTheory.IsProbabilityMeasure mu]112    (hball : ∀ j (x y : V), mu {z | adicCongr I j z x} = mu {z | adicCongr I j z y}) :113    MeasureTheory.MeasurePreserving F mu mu := by114  have hF : Measurable F := congruence_bijection_measurable O V I hgen F honto hcong115  refine ⟨hF, ?_⟩116  have : MeasureTheory.IsFiniteMeasure (mu.map F) := inferInstance117  refine finite_measures_from_cylinders O V I (mu.map F) mu hgen ?_118  intro j x119  have hmeas : MeasurableSet {y | adicCongr I j y x} := by120    rw [hgen]121    exact MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, x, rfl⟩)122  rw [MeasureTheory.Measure.map_apply hF hmeas]123  obtain ⟨w, rfl⟩ := honto x124  have : F ⁻¹' {y | adicCongr I j y (F w)} = {z | adicCongr I j z w} := by125    ext z; simp [hcong]126  rw [this]127  exact hball j w (F w)128 129/-- The image of a continuous homomorphism from a compact group, of finite index `n`, has Haar130  probability mass `1 / n`. -/131private theorem compact_image_index_mass (G H : Type) [AddCommGroup G] [AddCommGroup H]132    [TopologicalSpace G]133    [IsTopologicalAddGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G]134    [TopologicalSpace H] [IsTopologicalAddGroup H] [T2Space H] [MeasurableSpace H] [BorelSpace H]135    (f : G →+ H) (hf : Continuous f) [Finite (H ⧸ f.range)] (nu : MeasureTheory.Measure H)136    [MeasureTheory.IsProbabilityMeasure nu] [MeasureTheory.Measure.IsAddLeftInvariant nu] :137    nu (Set.range f) = (f.range.index : ℝ≥0∞)⁻¹ := by138  have hcl : IsClosed (Set.range f) := (isCompact_range hf).isClosed139  have hm : ∀ a : H ⧸ f.range, MeasurableSet {x | QuotientAddGroup.mk' f.range x = a} := by140    intro a141    obtain ⟨y, rfl⟩ := QuotientAddGroup.mk'_surjective f.range a142    have : {x | QuotientAddGroup.mk' f.range x = QuotientAddGroup.mk' f.range y}143        = (fun x => -y + x) ⁻¹' Set.range f := by144      ext x145      simp only [Set.mem_ofPred_eq, Set.mem_preimage, QuotientAddGroup.mk'_apply]146      rw [eq_comm, QuotientAddGroup.eq]147      change _ ↔ _ ∈ (f.range : Set H)148      simp149    rw [this]150    exact (hcl.preimage (continuous_const.add continuous_id)).measurableSet151  have h := finite_quotient_fiber_mass H (H ⧸ f.range) nu152    (QuotientAddGroup.mk' f.range) (QuotientAddGroup.mk'_surjective f.range) hm 0153  have e : {x | QuotientAddGroup.mk' f.range x = 0} = Set.range f := by154    ext x155    simp [QuotientAddGroup.eq_zero_iff]156  rw [e] at h157  rw [h, AddSubgroup.index]158 159/-- Pulling back a Haar probability measure along a continuous injective homomorphism from a compact160  group of image index `n` gives `1 / n` times Haar measure. -/161private theorem compact_injective_comap_measure (G H : Type) [AddCommGroup G] [AddCommGroup H]162    [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] [MeasurableSpace G]163    [BorelSpace G] [TopologicalSpace H] [IsTopologicalAddGroup H] [T2Space H] [MeasurableSpace H]164    [BorelSpace H] (f : G →+ H) (hf : Continuous f) [Finite (H ⧸ f.range)]165    (hinj : Function.Injective f) (mu : MeasureTheory.Measure G)166    [MeasureTheory.IsProbabilityMeasure mu] [MeasureTheory.Measure.IsAddHaarMeasure mu]167    (nu : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure nu]168    [MeasureTheory.Measure.IsAddLeftInvariant nu] :169    nu.comap f = (f.range.index : ℝ≥0∞)⁻¹ • mu := by170  have hce : Topology.IsClosedEmbedding f := hf.isClosedEmbedding hinj171  have hme : MeasurableEmbedding f := hce.measurableEmbedding172  have : (nu.comap f).IsAddLeftInvariant :=173    MeasureTheory.Measure.IsAddLeftInvariant.comap nu (f := f) hme174  have huniv : nu.comap f Set.univ = nu (Set.range f) := by175    rw [hme.comap_apply, Set.image_univ]176  have : MeasureTheory.IsFiniteMeasure (nu.comap f) :=177    ⟨by rw [huniv]; exact MeasureTheory.measure_lt_top _ _⟩178  have key := MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace (nu.comap f) mu179  have hc : (MeasureTheory.Measure.addHaarScalarFactor (nu.comap f) mu : ℝ≥0∞)180      = (f.range.index : ℝ≥0∞)⁻¹ := by181    have := congrArg (fun m : MeasureTheory.Measure G => m Set.univ) key182    simp only [MeasureTheory.Measure.smul_apply, MeasureTheory.measure_univ] at this183    rw [← compact_image_index_mass G H f hf nu, ← huniv]184    rw [this, ENNReal.smul_def, smul_eq_mul, mul_one]185  rw [key]186  ext s hs187  simp only [MeasureTheory.Measure.smul_apply, smul_eq_mul]188  rw [← hc, ENNReal.smul_def, smul_eq_mul]189 190/-- A continuous injective homomorphism from a compact group of image index `n` maps a measurable191  set of Haar mass `m` to a set of Haar mass `m / n`. -/192theorem compact_injective_image_measure (G H : Type) [AddCommGroup G] [AddCommGroup H]193    [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] [MeasurableSpace G]194    [BorelSpace G] [TopologicalSpace H] [IsTopologicalAddGroup H] [T2Space H] [MeasurableSpace H]195    [BorelSpace H] (f : G →+ H) (hf : Continuous f) [Finite (H ⧸ f.range)]196    (hinj : Function.Injective f) (mu : MeasureTheory.Measure G)197    [MeasureTheory.IsProbabilityMeasure mu] [MeasureTheory.Measure.IsAddHaarMeasure mu]198    (nu : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure nu]199    [MeasureTheory.Measure.IsAddLeftInvariant nu] (S : Set G) :200    nu (f '' S) = (f.range.index : ℝ≥0∞)⁻¹ * mu S := by201  have hemb : MeasurableEmbedding f :=202    (hf.isClosedEmbedding hinj).measurableEmbedding203  have h := compact_injective_comap_measure G H f hf hinj mu nu204  have h2 := congrArg (fun m => m S) h205  rw [hemb.comap_apply] at h2206  rw [h2]207  simp208 209end SurfaceBlowup