Charts of concrete members and the inseparable locus

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.CechStability7import SurfaceBlowup.Formula.TypeTransport8import SurfaceBlowup.Recursion.Members9 10/-!11# Charts of concrete members and the inseparable locus12 13For a concrete member of the recursion we describe its coordinate charts: translations of the14coordinates, the coset decomposition of a cell in a chart, and the pushforward of Haar measure along15a product of child charts. We show that the inseparable locus of monic polynomials is Haar-null,16and compute the cokernel length `binom(d, 2)` of the child-order map of a blown-up curve.17 18## Main results19 20* `member_chart_translate`: translating chart coordinates recenters the generator and preserves the21  coefficient measure.22* `member_coefficient_measure_map_product_coordinates`: a measurable linear isomorphism onto the23  child coordinate spaces maps Haar measure to the product of Haar measures.24* `monic_inseparable_null`: the inseparable locus of monic polynomials is Haar-null.25* `member_cell_chart_coset_decomposition`: the preimage of a cell in a chart is a finite disjoint26  union of coordinate cosets.27* `member_product_chart_pushforward`: the pushforward of Haar measure along a product of child28  charts.29* `child_order_index_and_kernel`, `concrete_curve_order_index`: the child-order map has kernel30  `(f)` and cokernel of length `binom(d, 2)`.31 32Provenance: `Thm_SurfaceBlowupV2_*`: `member_chart_translate`, `member_children_degree_sum`,33`member_coefficient_measure_map_product_coordinates`, `member_cell_chart_coset_decomposition`,34`member_product_chart_pushforward`, `curve_order_limit_cokernel_length`,35`child_order_index_and_kernel`, `concrete_curve_order_index`; `Thm_Gen_InseparableNull`.36-/37 38open scoped BigOperators ENNReal39 40namespace SurfaceBlowup41 42/-- Translating chart coordinates by `z₀` recenters the generator at `f + π Σ z₀ᵢ bᵢ`, maps cosets43  to translated cosets, and preserves the coefficient measure and measurability. -/44theorem member_chart_translate (m : ConcreteMember) (f : m.toMeasured.R)45    (b : Fin m.toMeasured.s.degree → m.toMeasured.R) (Mlev : ℕ)46    (z₀ : Fin m.toMeasured.s.degree → m.toMeasured.O) :47    (∀ z, coordinateIdeal m.toMeasured.S.pi f b (z₀ + z) =48      coordinateIdeal m.toMeasured.S.pi (f + m.toMeasured.S.pi • coordinateLift b z₀) b z) ∧49      coordinateCoset m.toMeasured.S.pi Mlev z₀ =50      (fun z => z₀ + z) '' Set.range (coordinateScale m.toMeasured.S.pi Mlev) ∧51        ∀ A : Set (Fin m.toMeasured.s.degree → m.toMeasured.O),52        coefficientMeasure m.toMeasured.O m.toMeasured.s.degree ((fun z => z₀ + z) '' A) =53        coefficientMeasure m.toMeasured.O m.toMeasured.s.degree A ∧54        (MeasurableSet A → MeasurableSet ((fun z => z₀ + z) '' A)) := by55  refine ⟨?_, ?_, ?_⟩56  · intro z57    unfold coordinateIdeal normalizedIdeal normalizedGenerator coordinateLift58    congr 259    simp only [Pi.smul_apply, Pi.add_apply, smul_add, add_smul, Finset.sum_add_distrib,60      Finset.smul_sum, smul_eq_mul, mul_smul, ← add_assoc]61  · ext z62    rw [Set.mem_image]63    simp only [coordinateCoset, Set.mem_ofPred_eq, Set.mem_range, coordinateScale]64    rw [finite_coordinate_adic_congruence]65    constructor66    · intro h67      choose y hy using fun i ↦ Ideal.mem_span_singleton'.168        (by simpa only [Ideal.span_singleton_pow] using h i)69      refine ⟨(m.toMeasured.S.pi ^ Mlev) • y, ⟨y, rfl⟩, ?_⟩70      ext i71      simp [mul_comm _ (y i), hy i]72    · rintro ⟨_, ⟨y, rfl⟩, rfl⟩ i73      rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton']74      exact ⟨y i, by simp [mul_comm]⟩75  · intro A76    have := (coefficient_space_strict_instances m.toMeasured.O m.toMeasured.htop77      m.toMeasured.S.pi m.toMeasured.S.pi_irreducible m.toMeasured.s.degree).2.178    rw [Set.image_add_left]79    exact ⟨MeasureTheory.measure_preimage_add _ _ _, fun hA ↦ measurable_const_add _ hA⟩80 81/-- The degrees of the children of a cell, weighted by their multiplicities `δ_j`, sum to the degree82  of the parent state. -/83theorem member_children_degree_sum (m : ConcreteMember) (c : m.toMeasured.cellIndex) :84    ∑ j, m.toMeasured.childDelta c j * (m.toMeasured.childState c j).degree =85      m.toMeasured.s.degree := by86  rw [← children_degree_identity m.toMeasured.s (m.shape.valid m.ha) c.1.1 c.1.2]87  exact Fin.sum_univ_fun_getElem _ fun z : ℕ × State ↦ z.1 * z.2.degree88 89/-- A measurable linear isomorphism onto the product of child coordinate spaces maps the parent90  coefficient measure to the product of child coefficient measures. -/91theorem member_coefficient_measure_map_product_coordinates (m : ConcreteMember)92    (c : m.toMeasured.cellIndex) (mc : m.toMeasured.childIdx c → ConcreteMember)93    [∀ j, Algebra m.toMeasured.O (mc j).toMeasured.O]94    (ρ : (Fin m.toMeasured.s.degree → m.toMeasured.O) ≃ₗ[m.toMeasured.O]95      (∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O))96    (hρ : Measurable ρ) :97    MeasureTheory.Measure.map ρ (coefficientMeasure m.toMeasured.O m.toMeasured.s.degree) =98      MeasureTheory.Measure.pi99      (fun j => coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree) := by100  classical101  have hm := coefficient_space_strict_instances m.toMeasured.O m.toMeasured.htop102    m.pi m.hpi m.toMeasured.s.degree103  have hc := fun j => coefficient_space_strict_instances (mc j).toMeasured.O (mc j).toMeasured.htop104    (mc j).pi (mc j).hpi (mc j).toMeasured.s.degree105  have := hm.2.1106  have := hm.2.2.1107  have : ∀ j, MeasureTheory.Measure.IsAddHaarMeasure108      (coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree) := fun j => (hc j).2.1109  have : ∀ j, MeasureTheory.IsProbabilityMeasure110      (coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree) := fun j => (hc j).2.2.1111  set ν := MeasureTheory.Measure.pi112      (fun j => coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree)113  set μ' := MeasureTheory.Measure.map ρ (coefficientMeasure m.toMeasured.O m.toMeasured.s.degree)114  have : MeasureTheory.IsProbabilityMeasure μ' :=115    MeasureTheory.Measure.isProbabilityMeasure_map hρ.aemeasurable116  have : μ'.IsAddLeftInvariant :=117    MeasureTheory.isAddLeftInvariant_map (ρ.toLinearMap.toAddMonoidHom.toAddHom) hρ ρ.surjective118  have key := MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace μ' ν119  have h1 := congrArg (fun μ => μ Set.univ) key120  simp only [MeasureTheory.Measure.smul_apply, MeasureTheory.measure_univ] at h1121  rw [ENNReal.smul_def, smul_eq_mul, mul_one, eq_comm, ENNReal.coe_eq_one] at h1122  rw [key, h1, one_smul]123 124/-! ### The inseparable locus is Haar-null -/125 126section InseparableNull127 128open MeasureTheory Polynomial129 130section Res131variable {K : Type} [Field K]132 133/-- The resultant of `f` and `f'` computed in formal degrees `(n, n - 1)` is a power of the leading134  coefficient times the usual resultant. -/135private theorem resultant_deriv_eq (f : K[X]) (n : ℕ) (hn : f.natDegree = n) :136    resultant f (derivative f) n (n-1) =137      f.coeff n ^ (n - 1 - (derivative f).natDegree) * resultant f (derivative f) := by138  have hd : (derivative f).natDegree ≤ n - 1 := hn ▸ natDegree_derivative_le f139  have := resultant_add_right_deg (f := f) (g := derivative f) (m := n)140    (n := (derivative f).natDegree) (n - 1 - (derivative f).natDegree) le_rfl141  rw [Nat.add_sub_cancel' hd] at this142  rw [this, ← hn]143 144/-- A nonzero polynomial of degree `n` whose resultant with its derivative in degrees `(n, n - 1)`145  is nonzero is separable. -/146theorem separable_of_resultant (f : K[X]) (n : ℕ) (hn : f.natDegree = n) (hf : f ≠ 0)147    (h : resultant f (derivative f) n (n - 1) ≠ 0) : f.Separable := by148  rw [resultant_deriv_eq f n hn] at h149  have h2 : resultant f (derivative f) ≠ 0 := right_ne_zero_of_mul h150  rw [Ne, resultant_eq_zero_iff] at h2151  push Not at h2152  exact h2 (Or.inl hf)153 154/-- A nonzero separable polynomial of degree `n` has nonzero resultant with its derivative in155  degrees `(n, n - 1)`. -/156theorem resultant_ne_zero_of_separable (f : K[X]) (n : ℕ) (hn : f.natDegree = n) (hf : f ≠ 0)157    (hs : f.Separable) : resultant f (derivative f) n (n-1) ≠ 0 := by158  rw [resultant_deriv_eq f n hn]159  refine mul_ne_zero (pow_ne_zero _ ?_) (resultant_ne_zero f _ hs)160  rw [← hn]; exact leadingCoeff_ne_zero.mpr hf161end Res162 163/-- The generic monic polynomial `X^n + Σ aᵢ Xⁱ` over `ℤ[a₀, …, a_{n-1}]`. -/164private noncomputable def genericMonic (n : ℕ) : Polynomial (MvPolynomial (Fin n) ℤ) :=165  X ^ n + ∑ i : Fin n, C (MvPolynomial.X i) * X ^ i.val166/-- The generic polynomial `Σ_{i ≤ n} aᵢ Xⁱ` over `ℤ[a₀, …, a_n]`. -/167private noncomputable def genericAffine (n : ℕ) : Polynomial (MvPolynomial (Fin (n+1)) ℤ) :=168  ∑ i : Fin (n+1), C (MvPolynomial.X i) * X ^ i.val169/-- The discriminant-type resultant of the generic monic polynomial and its derivative. -/170private noncomputable def discMonic (n : ℕ) : MvPolynomial (Fin n) ℤ :=171  resultant (genericMonic n) (derivative (genericMonic n)) n (n-1)172/-- The discriminant-type resultant of the generic polynomial of degree `n` and its derivative. -/173noncomputable def discAffine (n : ℕ) : MvPolynomial (Fin (n+1)) ℤ :=174  resultant (genericAffine n) (derivative (genericAffine n)) n (n-1)175 176variable (O : Type) [CommRing O] [IsDomain O]177 178/-- Specialization `ℤ[a] → Frac O` sending the generic coefficients to `a`. -/179private noncomputable def specHom {m : ℕ} (a : Fin m → O) :180    MvPolynomial (Fin m) ℤ →+* BaseField O :=181  MvPolynomial.eval₂Hom (Int.castRingHom _) fun i ↦ algebraMap O (BaseField O) (a i)182 183omit [IsDomain O] in184/-- The monic polynomial with coefficients `a` is the specialization of the generic monic185  polynomial. -/186private theorem monicPolynomial_eq_map {n : ℕ} (a : Fin n → O) :187    monicPolynomial O a = (genericMonic n).map (specHom O a) := by188  simp [monicPolynomial, genericMonic, specHom, Polynomial.map_sum]189 190omit [IsDomain O] in191/-- The polynomial with coefficients `a` is the specialization of the generic polynomial. -/192private theorem affinePolynomial_eq_map {n : ℕ} (a : Fin (n + 1) → O) :193    affinePolynomial O a = (genericAffine n).map (specHom O a) := by194  simp [affinePolynomial, genericAffine, specHom, Polynomial.map_sum]195 196omit [IsDomain O] in197/-- Specialization agrees with evaluating the polynomial mapped to `O`, then passing to `Frac O`. -/198private theorem specHom_eq {m : ℕ} (a : Fin m → O) (D : MvPolynomial (Fin m) ℤ) :199    specHom O a D = algebraMap O (BaseField O)200      (MvPolynomial.eval a (MvPolynomial.map (Int.castRingHom O) D)) := by201  induction D using MvPolynomial.induction_on with202  | C z => simp [specHom]203  | add p q hp hq => simp only [map_add, hp, hq]204  | mul_X p i hp =>205    rw [map_mul, map_mul, MvPolynomial.map_X, map_mul, map_mul, MvPolynomial.eval_X, ← hp]206    simp [specHom]207 208omit [IsDomain O] in209/-- The resultant of a monic polynomial with its derivative is the evaluation of `discMonic` at its210  coefficients. -/211private theorem monic_resultant_eq {n : ℕ} (a : Fin n → O) :212    resultant (monicPolynomial O a) (derivative (monicPolynomial O a)) n (n-1) =213      algebraMap O (BaseField O)214        (MvPolynomial.eval a (MvPolynomial.map (Int.castRingHom O) (discMonic n))) := by215  rw [← specHom_eq, monicPolynomial_eq_map, derivative_map, resultant_map_map]; rfl216 217omit [IsDomain O] in218/-- The resultant of a polynomial with its derivative is the evaluation of `discAffine` at its219  coefficients. -/220theorem affine_resultant_eq {n : ℕ} (a : Fin (n + 1) → O) :221    resultant (affinePolynomial O a) (derivative (affinePolynomial O a)) n (n-1) =222      algebraMap O (BaseField O)223        (MvPolynomial.eval a (MvPolynomial.map (Int.castRingHom O) (discAffine n))) := by224  rw [← specHom_eq, affinePolynomial_eq_map, derivative_map, resultant_map_map]; rfl225 226/-- Over a domain there is a separable monic polynomial of every degree over the fraction field. -/227theorem exists_separable_monic (n : ℕ) : ∃ a : Fin n → O, (monicPolynomial O a).Separable := by228  rcases n with _ | k229  · exact ⟨Fin.elim0, by simp [monicPolynomial]⟩230  by_cases h : ((k+1 : ℕ) : BaseField O) = 0231  · rcases k with _ | k232    · simp at h233    refine ⟨Pi.single 1 (-1), ?_⟩234    have he : monicPolynomial O (Pi.single (1 : Fin (k+2)) (-1 : O)) = X ^ (k+2) - X := by235      simp [monicPolynomial, Fin.sum_univ_succ, Pi.single_apply, sub_eq_add_neg,236        Fin.succ_succ_ne_one]237      ring238    rw [he]239    have hd : derivative (X ^ (k+2) - X : Polynomial (BaseField O)) = -1 := by240      simp only [derivative_sub, derivative_X_pow, derivative_X]241      rw [show ((k+2 : ℕ) : BaseField O) = 0 by exact_mod_cast h]242      simp243    rw [Polynomial.Separable, hd]244    exact isCoprime_one_right.neg_right245  · refine ⟨Pi.single 0 (-1), ?_⟩246    have he : monicPolynomial O (Pi.single (0 : Fin (k+1)) (-1 : O)) = X ^ (k+1) - 1 := by247      simp [monicPolynomial, Fin.sum_univ_succ, Pi.single_apply, sub_eq_add_neg]248    rw [he]249    exact (X_pow_sub_one_separable_iff).2 h250 251variable [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]252  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] [IsDiscreteValuationRing O]253  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]254 255/-- The zero locus of a polynomial that does not vanish identically on `O^m` is null for the256  coefficient measure. -/257theorem coefficientMeasure_zero_null (htop : IsAdic (IsLocalRing.maximalIdeal O)) (m : ℕ)258    (P : MvPolynomial (Fin m) O) (a₀ : Fin m → O) (h₀ : MvPolynomial.eval a₀ P ≠ 0) :259    coefficientMeasure O m {a | MvPolynomial.eval a P = 0} = 0 := by260  obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O261  have := coefficient_measure_probability O htop 1262  set ν := (coefficientMeasure O 1).map (LinearEquiv.funUnique (Fin 1) O O) with hν263  have h := coefficient_measure_pi_one O htop pi hpi m264  rw [h.1]265  have : MeasureTheory.Measure.IsAddLeftInvariant (coefficientMeasure O 1) := by266    unfold coefficientMeasure267    infer_instance268  have : NullSingletonClass ν := ⟨fun x => by269    rw [hν, Measure.map_apply h.2.2.2.2.1 (measurableSet_singleton x)]270    have hpre : (LinearEquiv.funUnique (Fin 1) O O) ⁻¹' {x} =271        (fun b : Fin 1 → O => (fun _ => -x) + b) ⁻¹' {b : Fin 1 → O | b 0 = 0} := by272      ext b273      simp only [Set.mem_preimage, Set.mem_singleton_iff, LinearEquiv.funUnique_apply,274        Set.mem_ofPred_eq, Pi.add_apply]275      rw [show (default : Fin 1) = 0 from rfl, neg_add_eq_zero, eq_comm]276    rw [hpre, measure_preimage_add]277    exact (coordinate_hyperplane_null O htop 1 0).2⟩278  exact mvPolynomial_zero_null ν m P (fun hP => h₀ (by rw [hP, map_zero]))279 280/-- The coefficients of inseparable monic polynomials form a null set for the coefficient measure.281-/282theorem monic_inseparable_null (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :Remark 6.3Discriminant locus is null283    coefficientMeasure O n {a | ¬ (monicPolynomial O a).Separable} = 0 := by284  obtain ⟨a₀, h₀⟩ := exists_separable_monic O n285  have hdeg := fun a => monic_polynomial_degree O n a286  refine measure_mono_null (fun a ha => ?_) (coefficientMeasure_zero_null O htop n287    (MvPolynomial.map (Int.castRingHom O) (discMonic n)) a₀ ?_)288  · simp only [Set.mem_ofPred_eq] at ha ⊢289    by_contra hne290    apply ha291    refine separable_of_resultant _ n (hdeg a).2 (hdeg a).1.ne_zero ?_292    rw [monic_resultant_eq]293    exact fun h => hne ((IsFractionRing.injective O (BaseField O)) (by rw [h, map_zero]))294  · have := resultant_ne_zero_of_separable _ n (hdeg a₀).2 (hdeg a₀).1.ne_zero h₀295    rw [monic_resultant_eq] at this296    exact fun h => this (by rw [h, map_zero])297 298end InseparableNull299 300open scoped Classical in301/-- Coordinate cosets of level `M ≥ cellDegree` give a finite measurable partition of the coordinate302  space, and the preimage of a cell in any chart is the union of the cosets whose representatives303  lie in the cell. -/304theorem member_cell_chart_coset_decomposition (m : ConcreteMember) (c : m.toMeasured.cellIndex)305    (Mlev : ℕ) (hM : m.toMeasured.cellDegree c ≤ Mlev) :306    ∃ reps : Finset (Fin m.s.degree → m.O),307      (∀ z : Fin m.s.degree → m.O, ∃! z₀, z₀ ∈ reps ∧ adicCongr (Ideal.span {m.S.pi}) Mlev z z₀) ∧308      (∀ z₀ : Fin m.s.degree → m.O, MeasurableSet (coordinateCoset m.S.pi Mlev z₀)) ∧309      (reps : Set (Fin m.s.degree → m.O)).PairwiseDisjoint310      (fun z₀ => coordinateCoset m.S.pi Mlev z₀) ∧ ∀ i : m.atlas.ι,311        coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b ⁻¹' m.toMeasured.cell c =312        ⋃ z₀ ∈ reps.filter313        (fun z₀ => coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b z₀ ∈314        m.toMeasured.cell c), coordinateCoset m.S.pi Mlev z₀ := by315  obtain ⟨reps, hreps⟩ :=316      coordinate_coset_representatives_exist m.O m.S.pi317      (by rw [m.hS_pi]; exact m.hpi) m.s.degree Mlev318  have hmax : Ideal.span {m.S.pi} = IsLocalRing.maximalIdeal m.O := by319    rw [m.hS_pi]; exact ((m.hpi).maximalIdeal_eq).symm320  have hmeas : ∀ z₀ : Fin m.s.degree → m.O, MeasurableSet (coordinateCoset m.S.pi Mlev z₀) := by321    intro z₀322    have h := finite_coordinate_borel_cylinders m.O (IsLocalRing.maximalIdeal m.O) m.htop m.s.degree323    have : @MeasurableSet _324        (adicCylinderSpace (IsLocalRing.maximalIdeal m.O) (Fin m.s.degree → m.O))325        (coordinateCoset m.S.pi Mlev z₀) := MeasurableSpace.measurableSet_generateFrom326      (.inr ⟨Mlev, z₀, by unfold coordinateCoset; rw [hmax]⟩)327    rwa [← h] at this328  refine ⟨reps, hreps, hmeas, fun z₁ h₁ z₂ h₂ hne ↦ Set.disjoint_left.2 fun z hz1 hz2 ↦ ?_, ?_⟩329  · obtain ⟨w, _, hw⟩ := hreps z330    exact hne ((hw z₁ ⟨h₁, hz1⟩).trans (hw z₂ ⟨h₂, hz2⟩).symm)331  intro i332  obtain ⟨hinj, -, -⟩ := concrete_member_charts m i333  have hf : Ideal.span {(m.atlas.chart i).f} ∈ surfaceStateSet m.O m.R m.S m.s :=334    m.atlas.cover.symm.subset <| Set.mem_iUnion.2335      ⟨i, ⟨_, rfl⟩, by rw [Ideal.map_span, Set.image_singleton]⟩336  obtain ⟨hpart, -⟩ := fixed_tangent_cell_chart_partition m.O m.R m.S m.s m.s.degree337    (m.atlas.chart i).b (m.atlas.chart i).f hf hinj (m.toMeasured.cellDegree c) Mlev hM c.2.1 reps338    hreps339  have hstate : ∀ z₀, coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b z₀ ∈340      surfaceStateSet m.O m.R m.S m.s := fun z₀ ↦ by341    change Ideal.span {_ + coordinateLift _ _} ∈ _342    rw [coordinateLift_smul_eq_mul]343    exact surface_state_vertical_perturbation m.O m.R m.S m.s (m.atlas.chart i).f _ hf344  rw [Finset.filter_congr fun z₀ _ ↦ ⟨fun h ↦ h.2, fun h ↦ ⟨hstate z₀, h⟩⟩]345  have h2 := congrArg346    (fun T ↦ coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b ⁻¹' T) hpart347  simp only [Set.preimage_inter_range] at h2348  refine h2.trans ?_349  simp only [Set.preimage_iUnion₂, Set.preimage_image_eq _ hinj]350  rfl351 352private theorem member_chart_measurableEmbedding (m : ConcreteMember) (g : m.toMeasured.R)353    (hg : Ideal.span {g} ∈ m.toMeasured.stateSet)354    (bc : Fin m.toMeasured.s.degree → m.toMeasured.R)355    (E : m.toMeasured.R ≃ₗ[m.toMeasured.O]356      ((Fin m.toMeasured.s.degree → m.toMeasured.O) × m.toMeasured.R))357    (hE : ∀ w, E.symm w = divisionMap g bc w) :358    @MeasurableEmbedding _ _ inferInstance m.toMeasured.measurableSpaceIdeal359      (coordinateIdeal m.toMeasured.S.pi g bc) := by360  have hreg := (concrete_member_state_generator_regular m g hg).2.2361  have hvp := surface_vertical_parameter m.toMeasured.O m.toMeasured.R m.toMeasured.S362  have hpi' : Irreducible m.toMeasured.S.pi := by363    change Irreducible m.S.pi364    rw [m.hS_pi]; exact m.hpi365  have := concrete_member_division_module_isAdicComplete m366  exact coordinate_ideal_measurableEmbedding m.toMeasured.O m.toMeasured.htop m.toMeasured.R367    m.toMeasured.S.pi hpi' hvp.1 hvp.2 _ g bc ⟨⟨E, hE⟩, hreg⟩368 369/-- The product of child coordinate-ideal maps is a measurable embedding, and pushes the product370  state measure back to `Π_j q_j^(-deg_j)` times the product coefficient measure. -/371theorem member_product_chart_pushforward (ι : Type) [Fintype ι] (mc : ι → ConcreteMember)372    (g : ∀ j, (mc j).toMeasured.R) (hg : ∀ j, Ideal.span {g j} ∈ (mc j).toMeasured.stateSet)373    (bc' : ∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.R)374    (E' : ∀ j, (mc j).toMeasured.R ≃ₗ[(mc j).toMeasured.O]375      ((Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) × (mc j).toMeasured.R))376    (hE' : ∀ j w, (E' j).symm w = divisionMap (g j) (bc' j) w) :377    (letI : ∀ j, MeasurableSpace (Ideal (mc j).toMeasured.R) :=378      fun j => (mc j).toMeasured.measurableSpaceIdeal; MeasurableEmbedding379        (fun (w : ∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) (j : ι)380        => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (w j)) ∧381        ∀ Y : Set (∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O), MeasurableSet Y →382        MeasureTheory.Measure.pi (fun j => (mc j).toMeasured.μ)383        ((fun (w : ∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) (j : ι)384        => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (w j)) '' Y) =385        (∏ j, ((mc j).toMeasured.q : ℝ≥0∞)⁻¹ ^ (mc j).toMeasured.s.degree) *386        MeasureTheory.Measure.pi387        (fun j => coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree) Y) := by388  set Ψ : (∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) → ∀ j,389      Ideal (mc j).toMeasured.R :=390    fun w j ↦ coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (w j)391  have hemb : MeasurableEmbedding Ψ :=392    measurableEmbedding_pi ι _ _ _393      (fun j => member_chart_measurableEmbedding (mc j) (g j) (hg j) (bc' j) (E' j) (hE' j))394  refine ⟨hemb, fun Y hY ↦ ?_⟩395  have : ∀ j, MeasureTheory.IsFiniteMeasure (mc j).toMeasured.μ :=396    fun j => (concrete_member_measure_finite_support (mc j)).1397  have : ∀ j, MeasureTheory.IsProbabilityMeasure398      (coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree) :=399    fun j => coefficient_measure_probability _ (mc j).toMeasured.htop _400  set C : ℝ≥0∞ := ∏ j, ((mc j).toMeasured.q : ℝ≥0∞)⁻¹ ^ (mc j).toMeasured.s.degree401  have hC0 : C ≠ 0 := Finset.prod_ne_zero_iff.2 fun j _ ↦402    pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))403  have hCt : C ≠ ⊤ := ENNReal.prod_ne_top fun j _ ↦ ENNReal.pow_ne_top <| ENNReal.inv_ne_top.2 <|404    Nat.cast_ne_zero.2405      (Finite.one_lt_card (α := IsLocalRing.ResidueField (mc j).toMeasured.O)).ne_bot406  set κ := MeasureTheory.Measure.comap Ψ407      (MeasureTheory.Measure.pi (fun j => (mc j).toMeasured.μ))408  have hκapp : ∀ Z, MeasurableSet Z → κ Z =409      MeasureTheory.Measure.pi (fun j => (mc j).toMeasured.μ) (Ψ '' Z) :=410    fun Z hZ => MeasureTheory.Measure.comap_apply Ψ hemb.injective411      (fun s hs => hemb.measurableSet_image' hs) _ hZ412  have hbox : ∀ s : ∀ j, Set (Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O),413      Ψ '' Set.pi Set.univ s =414        Set.pi Set.univ (fun j => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) '' s j) := by415    intro s416    ext y417    refine ⟨fun ⟨w, hw, hwy⟩ j _ ↦ hwy ▸ ⟨w j, hw j trivial, rfl⟩, fun hy ↦ ?_⟩418    choose w hw using fun j ↦ hy j trivial419    exact ⟨w, fun j _ ↦ (hw j).1, funext fun j ↦ (hw j).2⟩420  have hpi : MeasureTheory.Measure.pi421      (fun j => coefficientMeasure (mc j).toMeasured.O (mc j).toMeasured.s.degree)422      = C⁻¹ • κ := by423    apply MeasureTheory.Measure.pi_eq424    intro s hs425    rw [MeasureTheory.Measure.smul_apply, smul_eq_mul, hκapp _ (MeasurableSet.univ_pi hs), hbox,426      MeasureTheory.Measure.pi_pi, Finset.prod_congr rfl fun j _ ↦427        (concrete_member_division_chart_measure (mc j) (g j) (hg j) (bc' j) (E' j) (hE' j)).2.2 _428          (hs j), Finset.prod_mul_distrib, ← mul_assoc, ENNReal.inv_mul_cancel hC0 hCt, one_mul]429  rw [← hκapp _ hY, hpi, MeasureTheory.Measure.smul_apply, smul_eq_mul, ← mul_assoc,430    ENNReal.mul_inv_cancel hC0 hCt, one_mul]431 432/-! ### The child-order map of a blown-up curve -/433 434section ChildOrder435 436variable (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (t x : R)437  (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)438  (hregSwap : RegularParameterPair R x t) [(Ideal.span ({t,x} : Set R)).IsMaximal]439  (hres : Function.Surjective (algebraMap O (R ⧸ Ideal.span {t,x})))440  [IsAdicComplete (Ideal.span {t,x}) R]441 442include hreg hregSwap hres443 444/-- The cokernel of the map from the surface to the curve-order limit has length `binom(d, 2)`. -/445private theorem curve_order_limit_cokernel_length (d : ℕ) (G : GluedGenerators R t x beta d)446    (hregF : ∀ j : ℕ, Function.Injective447      (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j =>448        Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)449          ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))450    (f : R)451    (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =452      (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))453    (σ : R →ₗ[R] CurveOrderLimit R t x beta G)454    (hσ : ∀ r : R, ∃ p : curveThreads R t x beta G, σ r = curveLimitMk R t x beta G p ∧ ∀ j : ℕ,455      p.val j = surfaceToChartPair R t x r) :456    Module.length O (CurveOrderLimit R t x beta G ⧸ LinearMap.range (σ.restrictScalars O)) =457      (chooseTwo d : ℕ∞) := by458  set J := max (d - 1) 1459  have hJ : d - 1 ≤ J := le_max_left _ _460  have hpres := fun j ↦ actual_cech_preserves_exceptional_lattices R t x beta d j461  obtain ⟨π, hπ⟩ := curve_limit_level_map_exists R t x beta d G J462  obtain ⟨δ, -, hδs, hδk⟩ := curve_sections_connecting_map_exists O R t x hreg beta hregSwap d G J463    (hpres J) (hregF J)464  let Θ := δ ∘ₗ (π.restrictScalars O)465  have hker : LinearMap.ker Θ = LinearMap.range (σ.restrictScalars O) := by466    ext u467    simp only [LinearMap.mem_ker, LinearMap.mem_range, LinearMap.restrictScalars_apply]468    constructor469    · intro hu470      obtain ⟨p, rfl⟩ := Submodule.Quotient.mk_surjective _ u471      obtain ⟨r, hr⟩ := (hδk _).1 (show δ (π (curveLimitMk R t x beta G p)) = 0 from hu)472      rw [hπ p] at hr473      exact curve_limit_range_of_stable_level R t x beta d G hreg hregSwap hregF f hf J hJ σ hσ p474        ⟨r, (Submodule.Quotient.eq _).1 hr⟩475    · rintro ⟨r, rfl⟩476      obtain ⟨p, hp1, hp2⟩ := hσ r477      change δ (π (σ r)) = 0478      exact (hδk _).2 ⟨r, by rw [hp1, hπ p, hp2]⟩479  rw [((Submodule.quotEquivOfEq _ _ hker.symm).trans (LinearMap.quotKerEquivOfSurjective Θ480    (hδs.comp (curve_limit_level_map_surjective R t x beta d G hreg J π hπ)))).length_eq]481  exact actual_finite_cech_coefficient_triangular O R t x hreg beta hregSwap hres d J hJ hpres482 483/-- The child-order map has kernel `(f)` and cokernel of length `binom(d, 2)`. -/484theorem child_order_index_and_kernel [IsNoetherianRing (BlowupChart R t x)]Proposition 4.4485    [IsNoetherianRing (BlowupChart R x t)] (D : TwoChartCurveData R t x beta) (d : ℕ)486    (G : GluedGenerators R t x beta d)487    (hregF : ∀ j : ℕ, Function.Injective488      (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j =>489        Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)490          ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))491    (f : R)492    (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =493      (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))494    (hclosed : (⨅ j : ℕ, (Ideal.span {f} ⊔ (Ideal.span {t,x})^j)) = Ideal.span {f})495    [∀ p : AllPoints D, IsLocalRing (localRing D p)]496    [∀ p : AllPoints D, IsNoetherianRing (localRing D p)]497    [∀ p : AllPoints D, IsAdicComplete (IsLocalRing.maximalIdeal (localRing D p)) (localRing D p)]498    [∀ p : AllPoints D, Algebra O (localRing D p)]499    (E : CurveOrderLimit R t x beta G ≃ₗ[O] childOrder D) (σ : R →ₗ[R] CurveOrderLimit R t x beta G)500    (hσ : ∀ r : R, ∃ p : curveThreads R t x beta G, σ r = curveLimitMk R t x beta G p ∧ ∀ j : ℕ,501      p.val j = surfaceToChartPair R t x r)502    (hE : ∀ (p : curveThreads R t x beta G) (r : R),503      (∀ j : ℕ, p.val j = surfaceToChartPair R t x r) → E (curveLimitMk R t x beta G p) =504      childOrderMap D r)505    (φ : R →ₗ[O] childOrder D) (hφ : ∀ r : R, φ r = childOrderMap D r) :506    RingHom.ker (childOrderMap D) = Ideal.span {f} ∧507      Module.length O ((childOrder D) ⧸ LinearMap.range φ) = (chooseTwo d : ℕ∞) := by508  have key : ∀ r : R, childOrderMap D r = E (σ r) := fun r ↦ by509    obtain ⟨p, hp1, hp2⟩ := hσ r510    rw [hp1, hE p r hp2]511  have hker := surface_to_curve_limit_kernel R t x beta d G hreg hregSwap hregF f hf hclosed σ hσ512  refine ⟨Ideal.ext fun r ↦ ?_, ?_⟩513  · rw [RingHom.mem_ker, key, LinearEquiv.map_eq_zero_iff, ← LinearMap.mem_ker, hker]514  · have hrange : (LinearMap.range (σ.restrictScalars O)).map515        (E : CurveOrderLimit R t x beta G →ₗ[O] childOrder D) = LinearMap.range φ := by516      ext y517      simp only [Submodule.mem_map, LinearMap.mem_range, LinearMap.coe_restrictScalars]518      constructor519      · rintro ⟨_, ⟨r, rfl⟩, rfl⟩520        exact ⟨r, by rw [hφ, key]; rfl⟩521      · rintro ⟨r, rfl⟩522        exact ⟨σ r, ⟨r, rfl⟩, by rw [hφ, key]; rfl⟩523    rw [← curve_order_limit_cokernel_length O R t x hreg beta hregSwap hres d G hregF f hf σ hσ]524    exact (LinearEquiv.length_eq (Submodule.Quotient.equiv _ _ E hrange)).symm525 526end ChildOrder527 528section ConcreteIndex529 530variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]531  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)532  (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)533 534-- Abbreviations for the concrete surface and its two parameters.535local notation "𝒮" => ConcreteSurface O pi u a b536local notation "𝒯" => surfaceT O pi u a b537local notation "𝒳" => surfaceX O pi u a b538 539include hpi ha in540/-- For a concrete surface, the child-order map is `O`-linear with kernel `(f)` and cokernel of541  length `binom(d, 2)`, where `d` is the curve degree. -/542theorem concrete_curve_order_index (beta : BlowupRestriction 𝒮 𝒯 𝒳)Proposition 4.4543    (D : TwoChartCurveData 𝒮 𝒯 𝒳 beta) (f : 𝒮) (G : GluedGenerators 𝒮 𝒯 𝒳 beta (curveDataDegree D))544    (hf : ∀ j : ℕ, surfaceToCechInput 𝒮 𝒯 𝒳 j f =545      (cechInputLattice 𝒮 𝒯 𝒳 j).mkQ (gluedFunctionPair 𝒮 𝒯 𝒳 G j))546    (hG : ∀ j : ℕ,547      Ideal.span {Ideal.Quotient.mk ((chartExceptional 𝒮 𝒯 𝒳)^j) (G.left j)} =548        leftLevelKernel D j ∧549      Ideal.span {Ideal.Quotient.mk ((chartExceptional 𝒮 𝒳 𝒯)^j) (G.right j)} =550        rightLevelKernel D j) :551    (letI : ∀ p : AllPoints D, Algebra O (localRing D p) :=552      fun p => ((localFromSurface D p).comp (algebraMap O 𝒮)).toAlgebra;553        ∃ φ : 𝒮 →ₗ[O] childOrder D, (∀ r : 𝒮, φ r = childOrderMap D r) ∧554        RingHom.ker (childOrderMap D) = Ideal.span {f} ∧555        Module.length O (childOrder D ⧸ LinearMap.range φ) =556        (chooseTwo (curveDataDegree D) : ℕ∞)) := by557  let _ : ∀ p : AllPoints D, Algebra O (localRing D p) := fun p ↦558    ((localFromSurface D p).comp (algebraMap O 𝒮)).toAlgebra559  have hreg := concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha560  have hregSwap := concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha561  have : (Ideal.span ({𝒯, 𝒳} : Set 𝒮)).IsMaximal :=562    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha563  have : IsAdicComplete (Ideal.span ({𝒯, 𝒳} : Set 𝒮)) 𝒮 :=564    concrete_surface_isAdicComplete_parameterIdeal O pi u a b565  have := blowupChart_concrete_isNoetherianRing O pi u a b 𝒯 𝒳566  have := blowupChart_concrete_isNoetherianRing O pi u a b 𝒳 𝒯567  have := concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha568  have := concrete_surface_isNoetherianRing O pi u a b569  have hclosed : (⨅ j : ℕ, (Ideal.span {f} ⊔ (Ideal.span ({𝒯, 𝒳} : Set 𝒮))^j)) =570      Ideal.span {f} := by571    have := ideal_closed_noetherian_local 𝒮 (Ideal.span {f})572    rwa [concrete_surface_maximalIdeal_eq O pi hpi u a b ha] at this573  have h3 := (two_chart_datum_concrete_instances O pi hpi u a b ha beta D).2.2574  have : ∀ p : AllPoints D, IsNoetherianRing (localRing D p) := fun p ↦ (h3 p).1575  have : ∀ p : AllPoints D, IsLocalRing (localRing D p) := fun p ↦ (h3 p).2.choose576  have : ∀ p : AllPoints D,577      IsAdicComplete (IsLocalRing.maximalIdeal (localRing D p)) (localRing D p) :=578    fun p ↦ (h3 p).2.choose_spec.1579  obtain ⟨σ, hσ⟩ := surface_to_curve_limit_exists 𝒮 𝒯 𝒳 beta _ G580  obtain ⟨E, hE⟩ := child_order_equiv_linear 𝒮 𝒯 𝒳 beta D _ G hG581    (fun p ↦ (h3 p).2.choose_spec.2) O fun p o ↦ rfl582  let φ : 𝒮 →ₗ[O] childOrder D :=583    { toFun := fun r ↦ childOrderMap D r584      map_add' := fun r s ↦ map_add _ r s585      map_smul' := fun o r ↦ by586        rw [RingHom.id_apply, Algebra.smul_def o r, map_mul, Algebra.smul_def]587        congr 1 }588  refine ⟨φ, fun r ↦ rfl, child_order_index_and_kernel O 𝒮 𝒯 𝒳 hreg beta hregSwap ?_ D _ G589    (two_chart_left_generators_regular_on_overlap 𝒮 𝒯 𝒳 beta D _ G hG hreg hregSwap) f hf hclosed590    E σ hσ hE φ fun r ↦ rfl⟩591  intro y592  obtain ⟨e, he'⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha593  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y594  obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective r595  refine ⟨MvPowerSeries.constantCoeff s, e.injective ?_⟩596  have h2 := he' (MvPowerSeries.C (MvPowerSeries.constantCoeff s))597  simp only [MvPowerSeries.constantCoeff_C] at h2598  exact h2.trans (he' s).symm599 600end ConcreteIndex601 602end SurfaceBlowup