Haar measures on unramified extensions and strict-transform normalizations

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.Recursion.OrderDefect7 8/-!9# Haar measures on unramified extensions and strict-transform normalizations10 11For an unramified lift `Φ` over a complete DVR `O` with finite residue field, `O[x] ⧸ (Φ)` is again12such a DVR whose Haar measure is the product of coordinate Haar measures in the power basis. We also13compute strict transforms of principal ideals, show that the scaled strict normalizer pushes Haar14measure forward like its linear part, construct the linear part of a member center with its cokernel15length, and show that algebra types descend to factors of a product.16 17## Main results18 19* `strict_transform_ideal_of_generator`: if `α f = e^d g` with `e` regular, the strict transform20  of `(f)` is `(g)`.21* `unramified_extension_measure_package`, `unramified_coefficient_measure_pi`: `O[x] ⧸ (Φ)` is a22  complete DVR whose coefficient Haar measure is the product of power-coordinate measures.23* `strict_normalizer_pushforward_linear`: the scaled strict normalizer pushes Haar measure forward24  like its scaled linear part.25* `member_center_linear_part`: the linear part at a member center is injective, has a scaled26  inverse, and has cokernel length `s · deg - tri(cellDegree)`.27* `algebra_type_children_exists`: algebra types descend to the factors of a product.28 29Provenance: strict_transform_ideal_of_generator, power_coordinates_isAdic,30unramified_extension_measure_package, unramified_coefficient_measure_pi,31strict_normalizer_pushforward_linear, member_center_linear_part,32algebra_type_pi_factor, algebra_type_children_exists.33-/34 35open scoped BigOperators ENNReal36 37namespace SurfaceBlowup38 39/-- If `α f = e^d g` with `e` a nonzerodivisor, then the strict transform of `(f)` is `(g)`. -/40theorem strict_transform_ideal_of_generator (O R C : Type) [CommRing O] [CommRing R] [CommRing C]41    [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (e g : C) (d : ℕ) (f : R)42    (hf : alpha f = e ^ d * g) (he : Function.Injective (fun z : C => e * z)) :43    strictTransformIdeal alpha e d (Ideal.span {f}) = Ideal.span {g} := by44  have hinj : ∀ n : ℕ, ∀ a b : C, e ^ n * a = e ^ n * b → a = b := by45    intro n46    induction n with47    | zero => intro a b h; simpa using h48    | succ n ih =>49      intro a b h50      apply ih51      apply he52      simp only [pow_succ] at h53      simpa [mul_assoc, mul_comm, mul_left_comm] using h54  have hmap : (Ideal.span {f}).map alpha.toRingHom = Ideal.span {e ^ d * g} := by55    rw [Ideal.map_span, Set.image_singleton]56    simp [hf]57  ext u58  unfold strictTransformIdeal59  rw [hmap, Submodule.mem_colon_singleton, Ideal.mem_span_singleton', Ideal.mem_span_singleton']60  constructor61  · rintro ⟨v, hv⟩62    refine ⟨v, hinj d _ _ ?_⟩63    calc e ^ d * (v * g) = v * (e ^ d * g) := by ring64      _ = u • e ^ d := hv65      _ = e ^ d * u := by simp [mul_comm]66  · rintro ⟨v, hv⟩67    refine ⟨v, ?_⟩68    calc v * (e ^ d * g) = e ^ d * (v * g) := by ring69      _ = u • e ^ d := by rw [hv]; simp [mul_comm]70 71/-- On `O[x] ⧸ (Φ)` with the power-coordinate topology, the topology is adic for the base ideal72  `𝔪 O[x] ⧸ (Φ)`. -/73private theorem power_coordinates_isAdic (O : Type) [CommRing O] [IsDomain O] [TopologicalSpace O]74    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]75    [MeasurableSpace O] [BorelSpace O] (Φ : Polynomial O) (hm : Φ.Monic)76    [TopologicalSpace (AdjoinRoot Φ)]77    (hτ : ‹TopologicalSpace (AdjoinRoot Φ)› = unramifiedTopology O Φ hm) [IsDiscreteValuationRing O]78    (htop : IsAdic (IsLocalRing.maximalIdeal O)) :79    IsAdic (baseIdeal O Φ) := by80  let _ : MeasurableSpace (AdjoinRoot Φ) := unramifiedMeasurableSpace O Φ hm81  obtain ⟨hTR, -, -, -, -, hcont, -⟩ :=82    power_coordinates_transport O Φ hm hτ rfl83  set e := powerCoordinates O Φ hm with he84  set m := IsLocalRing.maximalIdeal O85  have hB := finite_coordinate_cylinder_basis O m htop Φ.natDegree86  -- coordinates of I^L87  have hpre : ∀ L : ℕ, ((baseIdeal O Φ ^ L : Ideal _) : Set (AdjoinRoot Φ)) =88      e ⁻¹' {v | adicCongr m L v 0} := by89    intro L90    ext x91    simp only [SetLike.mem_coe, Set.mem_preimage, Set.mem_ofPred_eq,92      finite_coordinate_adic_congruence, Pi.zero_apply, sub_zero]93    rw [base_ideal_coordinates O Φ hm L x]94    exact Iff.rfl95  have hopenB : ∀ L : ℕ, IsOpen {v : Fin Φ.natDegree → O | adicCongr m L v 0} := fun L =>96    hB.isOpen (Or.inr ⟨L, 0, rfl⟩)97  rw [isAdic_iff]98  refine ⟨fun L => ?_, fun s hs => ?_⟩99  · rw [hpre L]; exact (hopenB L).preimage hcont100  · have hs' : s ∈ Filter.comap e (nhds (e 0)) := by101      subst hτ102      rw [← nhds_induced]; exact hs103    rw [map_zero] at hs'104    obtain ⟨V, hV, hVs⟩ := Filter.mem_comap.1 hs'105    obtain ⟨W, hW, h0W, hWV⟩ := hB.mem_nhds_iff.1 hV106    rcases hW with rfl | ⟨L, x, rfl⟩107    · exact absurd h0W (Set.notMem_empty _)108    refine ⟨L, ?_⟩109    rw [hpre L]110    intro y hy111    apply hVs112    apply hWV113    have R := adic_congruence_rules O (Fin Φ.natDegree → O) m114    exact R.2.2.1 L _ _ _ hy h0W115 116/-- For an unramified lift `Φ`, the ring `O[x] ⧸ (Φ)` is a complete DVR with residue field of117  cardinality `q^(deg Φ)`, carrying a compact second-countable Borel topology that is adic for its118  maximal ideal. -/119theorem unramified_extension_measure_package (O : Type) [CommRing O] [IsDomain O]120    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]121    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]122    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]123    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)124    [TopologicalSpace (AdjoinRoot Φ)] [MeasurableSpace (AdjoinRoot Φ)]125    (hτ : ‹TopologicalSpace (AdjoinRoot Φ)› = unramifiedTopology O Φ hΦ.1)126    (hmeas : ‹MeasurableSpace (AdjoinRoot Φ)› = unramifiedMeasurableSpace O Φ hΦ.1) :127    ∃ (_ : IsDomain (AdjoinRoot Φ)) (_ : IsLocalRing (AdjoinRoot Φ)), True ∧128      IsDiscreteValuationRing (AdjoinRoot Φ) ∧129      IsAdicComplete (IsLocalRing.maximalIdeal (AdjoinRoot Φ)) (AdjoinRoot Φ) ∧130      Finite (IsLocalRing.ResidueField (AdjoinRoot Φ)) ∧131      Nat.card (IsLocalRing.ResidueField (AdjoinRoot Φ)) = residueCard O ^ Φ.natDegree ∧132      IsTopologicalRing (AdjoinRoot Φ) ∧ CompactSpace (AdjoinRoot Φ) ∧ T2Space (AdjoinRoot Φ) ∧133      SecondCountableTopology (AdjoinRoot Φ) ∧ BorelSpace (AdjoinRoot Φ) ∧134      IsAdic (IsLocalRing.maximalIdeal (AdjoinRoot Φ)) := by135  obtain ⟨d, l, hdvr, hmax, -, hcomp, hfin, hcard⟩ := unramified_is_dvr O Φ hΦ136  obtain ⟨h1, h2, h3, h4, h5, -⟩ := power_coordinates_transport O Φ hΦ.1 hτ hmeas137  have hadic := power_coordinates_isAdic O Φ hΦ.1 hτ htop138  have hdeg : 0 < Φ.natDegree := by139    have := (unramified_free_module O Φ hΦ.1).2.2140    have hf : Module.finrank O (AdjoinRoot Φ) ≠ 0 := by141      have : Nontrivial (AdjoinRoot Φ) := d.toNontrivial142      have := (unramified_free_module O Φ hΦ.1).1143      have := (unramified_free_module O Φ hΦ.1).2.1144      exact Module.finrank_pos.ne'145    omega146  have hinj : Function.Injective (algebraMap O (AdjoinRoot Φ)) := by147    rw [injective_iff_map_eq_zero]148    intro c hc149    have hm : ∀ L : ℕ, c ∈ (IsLocalRing.maximalIdeal O)^L := fun L =>150      (base_ideal_pure O Φ hΦ.1 hdeg L c).1 (by rw [hc]; exact Ideal.zero_mem _)151    have := Ideal.iInf_pow_eq_bot_of_isDomain (IsLocalRing.maximalIdeal O)152      ((IsLocalRing.maximalIdeal.isMaximal O).ne_top)153    rw [← Ideal.mem_bot, ← this]154    exact Ideal.mem_iInf.2 hm155  exact ⟨d, l, trivial, hdvr, hcomp, hfin, hcard, h1, h2, h3, h4, h5, by rw [hmax]; exact hadic⟩156 157/-- On `O[x] ⧸ (Φ)` the coefficient Haar measure is the product of the power-coordinate measures,158  and a ball of radius `L` in `r` coordinates has mass `q^(-deg Φ · r · L)`. -/159theorem unramified_coefficient_measure_pi (O : Type) [CommRing O] [IsDomain O]Theorem 5.1160    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]161    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]162    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]163    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)164    [TopologicalSpace (AdjoinRoot Φ)] [MeasurableSpace (AdjoinRoot Φ)]165    (hτ : ‹TopologicalSpace (AdjoinRoot Φ)› = unramifiedTopology O Φ hΦ.1)166    (hmeas : ‹MeasurableSpace (AdjoinRoot Φ)› = unramifiedMeasurableSpace O Φ hΦ.1)167    [IsDomain (AdjoinRoot Φ)] [IsTopologicalRing (AdjoinRoot Φ)] [CompactSpace (AdjoinRoot Φ)]168    [T2Space (AdjoinRoot Φ)] [SecondCountableTopology (AdjoinRoot Φ)] [BorelSpace (AdjoinRoot Φ)]169    [MeasureTheory.SigmaFinite (unramifiedCoefficientMeasure O Φ hΦ.1)] (r : ℕ) :170    coefficientMeasure (AdjoinRoot Φ) r =171      MeasureTheory.Measure.pi (fun _ : Fin r => unramifiedCoefficientMeasure O Φ hΦ.1) ∧172      ∀ (L : ℕ) (a : Fin r → AdjoinRoot Φ),173      coefficientMeasure (AdjoinRoot Φ) r {b | ∀ j, b j - a j ∈ (baseIdeal O Φ) ^ L} =174      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (Φ.natDegree * r * L) := by175  obtain ⟨_, _, _, _, _, _, hcard, _, _, _, _, _, hadic⟩ :=176    unramified_extension_measure_package O htop Φ hΦ hτ hmeas177  obtain ⟨_, _, _, hmax, -⟩ := unramified_is_dvr O Φ hΦ178  obtain ⟨hH, hP, -⟩ :=179    unramified_coefficient_measure_haar O Φ hΦ.1 hτ hmeas htop180  have hprob := coefficient_measure_probability (AdjoinRoot Φ) hadic r181  have hμ : MeasureTheory.Measure.IsAddHaarMeasure (coefficientMeasure (AdjoinRoot Φ) r) := by182    unfold coefficientMeasure183    apply MeasureTheory.Measure.IsAddHaarMeasure.smul184    · exact ENNReal.inv_ne_zero.mpr (MeasureTheory.measure_ne_top _ _)185    · exact ENNReal.inv_ne_top.mpr186        (MeasureTheory.Measure.IsOpenPosMeasure.open_pos _ isOpen_univ Set.univ_nonempty)187  refine ⟨MeasureTheory.Measure.isAddHaarMeasure_eq_of_isProbabilityMeasure _ _, ?_⟩188  intro L a189  have h := coefficient_cylinder_mass (AdjoinRoot Φ) hadic r L a190  rw [hmax, hcard] at h191  rw [h, Nat.cast_pow, ← ENNReal.inv_pow, ← pow_mul, mul_assoc, ENNReal.inv_pow]192 193/-- The scaled strict normalizer pushes an invariant probability measure forward to the same measure194  as its scaled linear part. -/195theorem strict_normalizer_pushforward_linear (O R : Type) [CommRing O] [CommRing R] [Algebra O R]196    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))197    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (k : ℕ)198    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))199    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w)200    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] [MeasurableSpace (Fin n → O)]201    [MeasurableAdd (Fin n → O)]202    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))203    (mu : MeasureTheory.Measure (Fin n → O)) [MeasureTheory.IsProbabilityMeasure mu]204    [MeasureTheory.Measure.IsAddLeftInvariant mu]205    (hfinite : ∀ j, Finite (AdicQuotient (Ideal.span {pi}) (Fin n → O) j))206    (hL : Measurable (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z)) :207    mu.map (scaledStrictMap pi a b E H) =208      mu.map (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z) := by209  have hr := strict_correction_raises_order O R n pi a b E H k ha Q210  have hP := adic_perturb_measure_preserving O (Fin n → O) (Ideal.span {pi})211    _ hr mu hgen hfinite212  have hfun : scaledStrictMap pi a b E H =213      (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z) ∘214        adicPerturb (normalizationCorrection pi a k b E H Q) := by215    funext z216    exact strict_normalizer_factors_through_linear O R n pi a b E H k ha Q hQ z217  rw [hfun, ← MeasureTheory.Measure.map_map hL hP.measurable, hP.map_eq]218 219/-- If each `g j` generates a state ideal of the child `mc j`, then the parameters `e j = t_j`220  act injectively on `Π R_j ⧸ (g)`. -/221private theorem child_quotient_mul_parameter_injective (m : ConcreteMember)222    (c : m.toMeasured.cellIndex) (mc : m.toMeasured.childIdx c → ConcreteMember)223    (e g : ∀ j, (mc j).toMeasured.R) (he : ∀ j, e j = (mc j).toMeasured.S.t)224    (hgj : ∀ j, Ideal.span {g j} ∈ (mc j).toMeasured.stateSet) :225    Function.Injective (fun y : (∀ j, (mc j).toMeasured.R) ⧸ Ideal.span {g} =>226      Ideal.Quotient.mk (Ideal.span {g}) e * y) := by227  have hmem : ∀ x : ∀ j, (mc j).toMeasured.R, x ∈ Ideal.span {g} ↔ ∀ j, x j ∈ Ideal.span {g j} :=228    fun x ↦ by rw [← Ideal.pi_span, Ideal.mem_pi]229  intro x y hxy230  induction x using Quotient.inductionOn' with | h x => ?_231  induction y using Quotient.inductionOn' with | h y => ?_232  change Ideal.Quotient.mk _ e * Ideal.Quotient.mk _ x = Ideal.Quotient.mk _ e *233    Ideal.Quotient.mk _ y at hxy234  change Ideal.Quotient.mk _ x = Ideal.Quotient.mk _ y235  rw [← map_mul, ← map_mul, Ideal.Quotient.eq, ← mul_sub] at hxy236  rw [Ideal.Quotient.eq, hmem]237  intro j238  have h0 : Ideal.Quotient.mk (Ideal.span {g j}) (mc j).toMeasured.S.t *239      Ideal.Quotient.mk _ ((x - y) j) = Ideal.Quotient.mk _ (mc j).toMeasured.S.t * 0 := by240    rw [mul_zero, ← map_mul, ← he j, Ideal.Quotient.eq_zero_iff_mem]241    simpa using (hmem _).1 hxy j242  rw [← Ideal.Quotient.eq_zero_iff_mem]243  exact (concrete_member_state_generator_transverse (mc j) (g j) (hgj j)).2 h0244 245/-- The linear part of the normalization at a member center is injective, admits a scaled inverse,246  and has cokernel of length `s · deg - tri(cellDegree)`. -/247theorem member_center_linear_part (m : ConcreteMember) (c : m.toMeasured.cellIndex)Theorem 5.1248    (mc : m.toMeasured.childIdx c → ConcreteMember)249    [∀ j, Algebra m.toMeasured.O (mc j).toMeasured.O]250    [∀ j, Algebra m.toMeasured.O (mc j).toMeasured.R]251    [∀ j, IsScalarTower m.toMeasured.O (mc j).toMeasured.O (mc j).toMeasured.R]252    (hcard : ∀ j, (mc j).toMeasured.q = m.toMeasured.q ^ m.toMeasured.childDelta c j)253    (alpha : ∀ j, m.toMeasured.R →ₐ[m.toMeasured.O] (mc j).toMeasured.R)254    (e : ∀ j, (mc j).toMeasured.R) (he : ∀ j, e j = (mc j).toMeasured.S.t)255    (hbij : Set.BijOn256      (fun (J : Ideal m.toMeasured.R) (j : m.toMeasured.childIdx c) => strictTransformIdeal257      (alpha j) (e j) (m.toMeasured.cellDegree c) J) (m.toMeasured.cell c)258      (Set.pi Set.univ fun j => (mc j).toMeasured.stateSet))259    (hindex : ∀ f : m.toMeasured.R, Ideal.span {f} ∈ m.toMeasured.cell c →260      ∀ g : (∀ j, (mc j).toMeasured.R), (∀ j, alpha j f = e j ^ m.toMeasured.cellDegree c * g j) →261      ∀ iota : (m.toMeasured.R ⧸ Ideal.span {f}) →ₗ[m.toMeasured.O]262      ((∀ j, (mc j).toMeasured.R) ⧸ Ideal.span {g}),263      (∀ h : m.toMeasured.R, iota (Ideal.Quotient.mk (Ideal.span {f}) h) =264      Ideal.Quotient.mk (Ideal.span {g}) (fun j => alpha j h)) → Function.Injective iota ∧265      Module.length m.toMeasured.O266      (((∀ j, (mc j).toMeasured.R) ⧸ Ideal.span {g}) ⧸ LinearMap.range iota) =267      (chooseTwo (m.toMeasured.cellDegree c) : ℕ∞))268    (hsum : ∑ j, m.toMeasured.childDelta c j * (mc j).toMeasured.s.firstContact =269      m.toMeasured.cellDegree c)270    (s : ℕ) (hs : tri (m.toMeasured.cellDegree c) ≤ s) (cc : (∀ j, (mc j).toMeasured.R))271    (hcc : (algebraMap m.toMeasured.O (∀ j, (mc j).toMeasured.R) m.toMeasured.S.pi) ^ s =272      e ^ m.toMeasured.cellDegree c * cc)273    (f : m.toMeasured.R) (b : Fin m.toMeasured.s.degree → m.toMeasured.R)274    (E₀ : m.toMeasured.R ≃ₗ[m.toMeasured.O]275      ((Fin m.toMeasured.s.degree → m.toMeasured.O) × m.toMeasured.R))276    (hE₀ : ∀ w, E₀.symm w = divisionMap f b w) (hf : Ideal.span {f} ∈ m.toMeasured.cell c)277    (g : (∀ j, (mc j).toMeasured.R)) (hg : ∀ j, alpha j f = e j ^ m.toMeasured.cellDegree c * g j)278    (bc : Fin m.toMeasured.s.degree → (∀ j, (mc j).toMeasured.R)) :279    (letI : Module m.toMeasured.O (∀ j, (mc j).toMeasured.R) := Algebra.toModule;280      ∀ (E : (∀ j, (mc j).toMeasured.R) ≃ₗ[m.toMeasured.O]281      ((Fin m.toMeasured.s.degree → m.toMeasured.O) × (∀ j, (mc j).toMeasured.R))),282      (∀ w, E.symm w = divisionMap g bc w) →283      ∃ Q : (Fin m.toMeasured.s.degree → m.toMeasured.O) →ₗ[m.toMeasured.O]284      (Fin m.toMeasured.s.degree → m.toMeasured.O),285      (∀ w, normalizationLinearPart E (pulledVariation (AlgHom.pi alpha) cc b) (Q w) =286      (m.toMeasured.S.pi ^ (s * m.toMeasured.s.degree - tri (m.toMeasured.cellDegree c))) • w) ∧287      Function.Injective (normalizationLinearPart E (pulledVariation (AlgHom.pi alpha) cc b)) ∧288      Module.length m.toMeasured.O289      ((Fin m.toMeasured.s.degree → m.toMeasured.O) ⧸ LinearMap.range290      (normalizationLinearPart E (pulledVariation (AlgHom.pi alpha) cc b))) =291      ((s * m.toMeasured.s.degree - tri (m.toMeasured.cellDegree c) : ℕ) : ℕ∞)) := by292  intro E hE293  -- compute the cokernel length through the strict quotient maps `R ⧸ (f) → Π R_j ⧸ (g)`, then294  -- invert the linear part up to `π^(s · deg - tri)` from the length bound295  have hpiO : Irreducible m.toMeasured.S.pi := m.toMeasured.S.pi_irreducible296  have hf' : AlgHom.pi alpha f = e ^ (m.toMeasured.cellDegree c) * g := by297    funext j; simp [AlgHom.pi_apply, hg j]298  have hgj : ∀ j, Ideal.span {g j} ∈ (mc j).toMeasured.stateSet := fun j => by299    simpa [strict_transform_ideal_of_generator _ _ _ (alpha j) (e j) (g j) _ f (hg j)300      (concrete_member_mul_t_injective (he j))] using hbij.mapsTo hf j (Set.mem_univ _)301  obtain ⟨phi, hphi⟩ := strict_quotient_map_exists m.toMeasured.O m.toMeasured.R _ _ f g e cc _ hf'302  obtain ⟨iota, hiota⟩ :=303    strict_quotient_inclusion_exists m.toMeasured.O m.toMeasured.R _ _ f g e _ hf'304  obtain ⟨hiota_inj, hindex'⟩ := hindex f hf g hg iota hiota305  have hereg := child_quotient_mul_parameter_injective m c mc e g he hgj306  have hechild : Module.length m.toMeasured.O307      (((∀ j, (mc j).toMeasured.R) ⧸ Ideal.span {g}) ⧸ LinearMap.range308      (LinearMap.mulLeft m.toMeasured.O (Ideal.Quotient.mk (Ideal.span {g}) e))) =309      ((m.toMeasured.cellDegree c) : ℕ∞) := by310    rw [pi_mul_cokernel_length m.toMeasured.O _ _ g e311      (fun j => m.toMeasured.childDelta c j * (mc j).toMeasured.s.firstContact) fun j => by312      apply length_scaling_of_residue_card m.toMeasured.O (mc j).toMeasured.O _ (hcard j)313      rw [he j]314      exact concrete_member_state_generator_contact_length (mc j) (g j) (hgj j), hsum]315  obtain ⟨EC, -⟩ := division_equiv_child_coordinates m.toMeasured.O _ _ g bc E hE316  obtain ⟨hpireg, hpiquot⟩ := coordinate_module_pi_quotient_length m.toMeasured.O _ hpiO _ _ EC317  have hlen := strict_quotient_cokernel_length m.toMeasured.O m.toMeasured.R _ _ f g e cc _ _ s hcc318    _ phi iota hphi hiota hindex' hereg hechild hpireg hpiquot319    (le_trans hs (Nat.le_mul_of_pos_right s (concrete_member_one_le_degree m)))320  have hphi_inj := strict_quotient_map_injective m.toMeasured.O m.toMeasured.R _ _ f g e cc _ _ s321    hcc phi iota hphi hiota hiota_inj hpireg322  obtain ⟨EB, hEB⟩ := division_quotient_basis_equiv m.toMeasured.O m.toMeasured.R _ f b E₀ hE₀323  obtain ⟨hL, hI⟩ := normalization_linear_part_cokernel_length_eq m.toMeasured.O m.toMeasured.R _ _324    f g e cc _ hf' _ _ s hcc b bc E hE phi hphi EB hEB325  have hDinj := hI hphi_inj326  have hkl := hL.trans hlen327  obtain ⟨Q, hQ, -⟩ := scaled_inverse_from_image_containment m.toMeasured.O _ _ _ _ _ hDinj328    (linear_image_bound_from_cokernel_length m.toMeasured.O _ _ _ hpiO.maximalIdeal_eq _ _ hkl)329  exact ⟨Q, hQ, hDinj, hkl⟩330 331/-- If `A` has an algebra type and `K ⊗ A ≃ K ⊗ Π B_j`, then every factor `B_j` has an algebra332  type. -/333private theorem algebra_type_pi_factor (O : Type) [CommRing O] [IsDomain O] (A : Type) [CommRing A]334    [Algebra O A] (n : ℕ) (B : Fin n → Type) [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)]335    (e : TensorProduct O (BaseField O) A ≃ₐ[BaseField O] TensorProduct O (BaseField O) (∀ j, B j))336    (σ : FactorType) (hσ : HasAlgebraType O A σ) :337    ∀ j, ∃ τ : FactorType, HasAlgebraType O (B j) τ := by338  intro j339  obtain ⟨ι, hι, L, hF, hK, hO, hT, hD, e₀, -, hsepL⟩ := hσ340  let p := Algebra.TensorProduct.piRight O (BaseField O) (BaseField O) B341  let π := Pi.evalAlgHom (BaseField O) (fun j => TensorProduct O (BaseField O) (B j)) j342  have hπ : Function.Surjective π := fun y => ⟨Pi.single j y, by simp [π]⟩343  let q := Ideal.quotientKerAlgEquivOfSurjective hπ344  let g := p.symm.trans (e.symm.trans e₀)345  let I := (RingHom.ker π).map346      (g : ((i : Fin n) → TensorProduct O (BaseField O) (B i)) →+* ((i : ι) → L i))347  obtain ⟨S, e₁, -⟩ := pi_field_quotient_equiv (BaseField O) ι L I348  let E := q.symm.trans ((Ideal.quotientEquivAlg (RingHom.ker π) I g rfl).trans e₁)349  exact ⟨_, S, inferInstance, fun i => L i.1, fun i => hF i.1, fun i => hK i.1, fun i => hO i.1,350    fun i => hT i.1, fun i => hD i.1, E, rfl, fun i => hsepL i.1⟩351 352/-- If `A → Π B_j` is injective with finite-length cokernel and `A` has an algebra type, then every353  factor `B_j` has an algebra type. -/354theorem algebra_type_children_exists (O : Type) [CommRing O] [IsDomain O]355    [IsDiscreteValuationRing O] (A : Type) [CommRing A] [Algebra O A] (n : ℕ) (B : Fin n → Type)356    [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)] (ψ : A →ₐ[O] ∀ j, B j)357    (hinj : Function.Injective ψ) (ℓ : ℕ)358    (hℓ : Module.length O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = ℓ) (σ : FactorType)359    (hσ : HasAlgebraType O A σ) :360    ∀ j, ∃ τ : FactorType, HasAlgebraType O (B j) τ := by361  have hb := baseChange_bijective_of_finite_cokernel O A (∀ j, B j) ψ.toLinearMap hinj ℓ hℓ362  have hfun : ∀ x, (Algebra.TensorProduct.map (AlgHom.id (BaseField O) (BaseField O)) ψ) x363      = LinearMap.baseChange (BaseField O) ψ.toLinearMap x := by364    intro x365    induction x using TensorProduct.induction_on with366    | zero => simp367    | tmul k a => simp368    | add x y hx hy => rw [map_add, map_add, hx, hy]369  have hΨ : Function.Bijective370      (Algebra.TensorProduct.map (AlgHom.id (BaseField O) (BaseField O)) ψ) := by371    have : ⇑(Algebra.TensorProduct.map (AlgHom.id (BaseField O) (BaseField O)) ψ)372        = ⇑(LinearMap.baseChange (BaseField O) ψ.toLinearMap) := funext hfun373    rw [this]; exact hb374  exact algebra_type_pi_factor O A n B (AlgEquiv.ofBijective _ hΨ) σ hσ375 376end SurfaceBlowup