Members of the recursion universe

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.Surfaces.ConcreteStrictTransforms7import SurfaceBlowup.Unramified.DescentTypes8 9/-!10# Members of the recursion universe11 12This file sets up the objects on which the measure-theoretic recursion of Theorem 8.1 runs.13A `MeasuredSurface` is a regular local surface over a complete DVR with finite residue field,14equipped with a state and an atlas of division charts, hence with a state measure; a15`SurfaceUniverse` is a family of measured surfaces closed under passing to the children of16tangent cells. Concrete members (`ConcreteMember`) are the surfaces `O[[T,X]]/(π − u T^a X^b)`;17for them we prove the chart, measurability and finiteness inputs, and the structure of the18generators of state ideals. We also define the recursion events (type, return and exit events).19 20## Main definitions21 22* `CellAssignment`, `MeasuredSurface`, `SurfaceUniverse`, `ConcreteMember`, `ChildMember`,23  `CellChildData`, `SurfaceUniverse.Terminates`, `SurfaceUniverse.LawStatement`.24 25## Main results26 27* `concrete_member_charts`, `concrete_member_cell_measurable`,28  `concrete_member_stateSet_measurable`, `concrete_member_measure_finite_support`:29  measure-theoretic inputs for concrete members.30* `concrete_member_curve_order_free`, `concrete_member_state_generator_division`,31  `concrete_member_division_chart_measure`: generators of state ideals give division charts.32* `cell_datum_point_equiv`: children of a cell correspond to points of two-chart curve data.33* `concrete_type_add_of_index_map`: additivity of algebra types along a child decomposition.34* `curve_sections_connecting_map_exists`: the connecting map of the Čech sequence.35 36Provenance: `Def_SurfaceBlowupV2_{CellAssignments, MeasuredSurfaces, ConcreteMembers,37CellChildData, RecursionEvents}`; `Thm_SurfaceBlowupV2_{allowed_pattern_of_divisor_unique,38baseChange_bijective_of_finite_cokernel, boundary_contact_length_ne_zero_iff,39cell_child_mem_stateSet, cell_datum_point_equiv, chart_cell_law_generic,40coefficient_measure_pi_one, concrete_member_{charts, cell_measurable, data_exists,41stateSet_measurable, measure_finite_support, state_generator_contact_length,42state_generator_regular, division_chart_measure, state_generator_transverse, curve_order_free,43state_generator_division}, concrete_surface_crossing_curve_free, concrete_type_add_of_index_map,44coordinate_ideal_measurableEmbedding, curve_sections_connecting_map_exists}`.45-/46 47noncomputable section48 49namespace SurfaceBlowup50 51open IsLocalRing MeasureTheory52open scoped BigOperators ENNReal53 54/-! ### Cell assignments -/55 56section CellAssignments57 58variable (k : Type) [Field k]59 60open scoped Classical in61/-- The child state at the point Q of a degree-d tangent divisor Dv of a parent in state s,62equations (7.1)–(7.2): the point at infinity (old t-boundary) gives T(a,a; Dv(∞), c−d) resp.63T(a+b,a; Dv(∞), c−d); at a crossing the point Z = 0 (old x-boundary) gives T(a+b,b; Dv(Z), h−d);64every other point gives S(a; Dv(Q)) resp. S(a+b; Dv(Q)). -/65def pointChildState (s : State) (d : ℕ) (Dv : ExceptionalDivisor k) (Q : ClosedDirection k) :66    State :=67  match s with68  | State.single a c =>69    if Q = infinityDirection k then State.crossing a a (Dv Q) (c - d) else State.single a (Dv Q)70  | State.crossing a b c h =>71    if Q = infinityDirection k then State.crossing (a + b) a (Dv Q) (c - d)72    else if Q = zeroDirection k then State.crossing (a + b) b (Dv Q) (h - d)73    else State.single (a + b) (Dv Q)74/-- A cell assignment for the pattern P and the divisor Dv: a bijection between the entries of the75children list `children s P` and the support of Dv, sending the j-th entry to a point of the76prescribed degree whose child state (`pointChildState`) is the listed state. Existence follows77from `HasPattern` by counting. -/78structure CellAssignment (s : State) (P : TangentPattern s.degree) (Dv : ExceptionalDivisor k) where79  pt : Fin (children s P).length → ClosedDirection k80  inj : Function.Injective pt81  supp : ∀ Q : ClosedDirection k, 0 < Dv Q ↔ ∃ j, pt j = Q82  deg : ∀ j, directionDegree k (pt j) = ((children s P).get j).183  state : ∀ j, ((children s P).get j).2 = pointChildState k s P.d.val Dv (pt j)84 85end CellAssignments86 87/-! ### Measured surfaces and the recursion universe -/88 89/-- A surface realizing a state, over a complete DVR O with finite residue field and its compact90adic Borel structure, together with a finite atlas of division charts of its state set. -/91structure MeasuredSurface where92  O : Type93  [instCommRing : CommRing O]94  [instDomain : IsDomain O]95  [instDVR : IsDiscreteValuationRing O]96  [instComplete : IsAdicComplete (maximalIdeal O) O]97  [instFinite : Finite (ResidueField O)]98  [instTop : TopologicalSpace O]99  [instTopRing : IsTopologicalRing O]100  [instCompact : CompactSpace O]101  [instT2 : T2Space O]102  [instSecond : SecondCountableTopology O]103  [instMeas : MeasurableSpace O]104  [instBorel : BorelSpace O]105  htop : IsAdic (maximalIdeal O)106  R : Type107  [instCommRingR : CommRing R]108  [instDomainR : IsDomain R]109  [instAlgebra : Algebra O R]110  [instRegular : IsRegularLocalRing R]111  S : SurfaceData O R112  s : State113  valid : s.Valid114  atlas : IdealAtlas O R S.pi s.degree (surfaceStateSet O R S s)115attribute [instance] MeasuredSurface.instCommRing MeasuredSurface.instDomain116  MeasuredSurface.instDVR MeasuredSurface.instComplete MeasuredSurface.instFinite117      MeasuredSurface.instTop118  MeasuredSurface.instTopRing MeasuredSurface.instCompact MeasuredSurface.instT2119      MeasuredSurface.instSecond120  MeasuredSurface.instMeas MeasuredSurface.instBorel MeasuredSurface.instCommRingR121      MeasuredSurface.instDomainR122  MeasuredSurface.instAlgebra MeasuredSurface.instRegular123namespace MeasuredSurface124variable (M : MeasuredSurface)125/-- The residue cardinality q of the coefficient ring. -/126abbrev q : ℕ := Nat.card (ResidueField M.O)127/-- The state set `surfaceStateSet` of the surface in its state. -/128abbrev stateSet : Set (Ideal M.R) := surfaceStateSet M.O M.R M.S M.s129/-- The intrinsic σ-algebra `idealChartSigma` on the curve ideals of the surface. -/130instance measurableSpaceIdeal : MeasurableSpace (Ideal M.R) := idealChartSigma M.O M.R M.S.pi131/-- The state measure `stateMeasure` for the chosen atlas, with the intrinsic σ-algebra. -/132noncomputable def μ : Measure (Ideal M.R) := stateMeasure M.O M.R M.S.pi M.s.degree M.q M.atlas133/-- Allowed patterns of the state, as a type. -/134abbrev allowedPattern : Type := {P : TangentPattern M.s.degree // Allowed M.s P}135/-- A tangent cell index: an allowed pattern together with a divisor realizing it. -/136abbrev cellIndex : Type := Σ P : M.allowedPattern, patternDivisors (ResidueField M.R) M.s P.1137/-- The degree `d` of the tangent pattern of a cell. -/138def cellDegree (c : M.cellIndex) : ℕ := c.1.1.d.val139/-- The fixed-tangent cell `fixedTangentCell` attached to a cell index. -/140def cell (c : M.cellIndex) : Set (Ideal M.R) :=141  fixedTangentCell M.O M.R M.S M.s (M.cellDegree c) c.2.1142/-- The list of (residue degree, state) pairs of the children of a cell. -/143def childList (c : M.cellIndex) : List (ℕ × State) := children M.s c.1.1144/-- The index type of the children of a cell. -/145abbrev childIdx (c : M.cellIndex) : Type := Fin (M.childList c).length146/-- The residue degree of the `j`-th child of a cell. -/147def childDelta (c : M.cellIndex) (j : M.childIdx c) : ℕ := ((M.childList c).get j).1148/-- The state of the `j`-th child of a cell. -/149def childState (c : M.cellIndex) (j : M.childIdx c) : State := ((M.childList c).get j).2150/-- A cell is a self cell if its pattern returns to the parent state. -/151def IsSelfCell (c : M.cellIndex) : Prop := SelfPattern M.s c.1.1152end MeasuredSurface153/-- The recursion interface record: a family of measured surfaces closed under passing to the154children of every tangent cell, with the geometric inputs of Theorem 8.1 as explicit fields (facts155about cells, child surfaces, the fixed-tangent bijections and types). No field mentions stateLaw. -/156structure SurfaceUniverse where157  ι : Type 1158  M : ι → MeasuredSurface159  stateSet_measurable : ∀ i, MeasurableSet (M i).stateSet160  volume : ∀ i, (M i).μ (M i).stateSet = densityValue (stateVolume (M i).s) (M i).q161  divisors_finite : ∀ i (P : TangentPattern (M i).s.degree),162    Finite (patternDivisors (ResidueField (M i).R) (M i).s P)163  divisor_count : ∀ i, (M i).s.terminal = false → ∀ P : TangentPattern (M i).s.degree, Allowed164      (M i).s P →165    ((Nat.card (patternDivisors (ResidueField (M i).R) (M i).s P) : ℕ) : ℚ) =166      (tangentCount (M i).s P).eval ((M i).q : ℚ)167  cell_measurable : ∀ i, (M i).s.terminal = false → ∀ c : (M i).cellIndex, MeasurableSet168      ((M i).cell c)169  cells_cover : ∀ i, (M i).s.terminal = false → (M i).stateSet = ⋃ c : (M i).cellIndex, (M i).cell c170  cells_disjoint : ∀ i, (M i).s.terminal = false →171    Pairwise fun c c' : (M i).cellIndex => Disjoint ((M i).cell c) ((M i).cell c')172  child : ∀ i (c : (M i).cellIndex), (M i).childIdx c → ι173  child_state : ∀ i c j, (M (child i c j)).s = (M i).childState c j174  child_residue : ∀ i c j, (M (child i c j)).q = (M i).q ^ (M i).childDelta c j175  Φ : ∀ i (c : (M i).cellIndex), Ideal (M i).R → ∀ j : (M i).childIdx c, Ideal (M (child i c j)).R176  Φ_bij : ∀ i, (M i).s.terminal = false → ∀ c,177    Set.BijOn (Φ i c) ((M i).cell c) (Set.pi Set.univ fun j => (M (child i c j)).stateSet)178  Φ_measurable : ∀ i, (M i).s.terminal = false → ∀ c (G : ∀ j, Set (Ideal (M (child i c j)).R)),179    (∀ j, MeasurableSet (G j)) → MeasurableSet ((M i).cell c ∩ Φ i c ⁻¹' Set.pi Set.univ G)180  Φ_measure : ∀ i, (M i).s.terminal = false → ∀ c (G : ∀ j, Set (Ideal (M (child i c j)).R)),181    (∀ j, MeasurableSet (G j)) →182    (M i).μ ((M i).cell c ∩ Φ i c ⁻¹' Set.pi Set.univ G) =183      ((M i).q : ℝ≥0∞)⁻¹ ^ tri ((M i).cellDegree c) * ∏ j, (M (child i c j)).μ (G j)184  type_add : ∀ i, (M i).s.terminal = false → ∀ c (J : Ideal (M i).R), J ∈ (M i).cell c →185    ∀ τ : (M i).childIdx c → FactorType,186    (∀ j, HasAlgebraType (M (child i c j)).O ((M (child i c j)).R ⧸ Φ i c J j) (τ j)) →187    HasAlgebraType (M i).O ((M i).R ⧸ J) (∑ j, scaleType ((M i).childDelta c j) (τ j))188  terminal_type : ∀ i (a : ℕ), (M i).s = State.single a 1 → ∀ J ∈ (M i).stateSet,189    HasAlgebraType (M i).O ((M i).R ⧸ J) {(a,1)}190 191/-- In a surface universe `U`, every child ideal of a typed cell ideal again has an algebra type. -/192def SurfaceUniverse.ChildTypesExist (U : SurfaceUniverse) : Prop :=193  ∀ i, (U.M i).s.terminal = false → ∀ (c : (U.M i).cellIndex) (J : Ideal (U.M i).R),194    J ∈ (U.M i).cell c → ∀ σ : FactorType, HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ → ∀ j,195      ∃ τ : FactorType, HasAlgebraType (U.M (U.child i c j)).O196          ((U.M (U.child i c j)).R ⧸ U.Φ i c J j) τ197 198/-- An invariant `δ` of the ideals of a surface universe `U` does not increase when passing from a199typed cell ideal to a child, and strictly decreases on self cells. -/200def SurfaceUniverse.InvariantDecreases (U : SurfaceUniverse)201    (δ : ∀ i : U.ι, Ideal (U.M i).R → ℕ) : Prop :=202  ∀ i, (U.M i).s.terminal = false → ∀ (c : (U.M i).cellIndex) (J : Ideal (U.M i).R),203    J ∈ (U.M i).cell c → (∃ σ : FactorType, HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ) → ∀ j,204      δ (U.child i c j) (U.Φ i c J j) ≤ δ i J ∧205        ((U.M i).IsSelfCell c → δ (U.child i c j) (U.Φ i c J j) < δ i J)206 207/-! ### Concrete members -/208 209/-- The states realized by a concrete surface with vertical exponents (a, b): S(a;c) when b = 0 and210T(a,b;c,h) when b > 0, with every displayed entry positive (compare S.a = a, S.b = b in211`surfaceStateSet`). -/212def StateShape (a b : ℕ) : State → Prop213  | State.single a' c => a' = a ∧ b = 0 ∧ 0 < c214  | State.crossing a' b' c h => a' = a ∧ b' = b ∧ 0 < b ∧ 0 < c ∧ 0 < h215/-- A state of the shape of a concrete surface with `0 < a` is valid. -/216theorem StateShape.valid {a b : ℕ} (ha : 0 < a) {s : State} (h : StateShape a b s) : s.Valid := by217  cases s with218  | single => obtain ⟨rfl, -, h3⟩ := h; exact ⟨ha, h3⟩219  | crossing => obtain ⟨rfl, rfl, h3, h4, h5⟩ := h; exact ⟨ha, h3, h4, h5⟩220/-- A concrete member of the recursion universe: a complete DVR O with finite residue field and221its compact adic Borel structure, the concrete surface R = O[[T,X]]/(pi − u T^a X^b) with its222regular local structure and a `SurfaceData` whose parameters are the concrete ones, a state of223matching shape, and an ideal atlas of its state set. All fields are data or elementary224predicates. -/225structure ConcreteMember where226  O : Type227  [instCommRing : CommRing O]228  [instDomain : IsDomain O]229  [instDVR : IsDiscreteValuationRing O]230  [instComplete : IsAdicComplete (maximalIdeal O) O]231  [instFinite : Finite (ResidueField O)]232  [instTop : TopologicalSpace O]233  [instTopRing : IsTopologicalRing O]234  [instCompact : CompactSpace O]235  [instT2 : T2Space O]236  [instSecond : SecondCountableTopology O]237  [instMeas : MeasurableSpace O]238  [instBorel : BorelSpace O]239  htop : IsAdic (maximalIdeal O)240  pi : O241  hpi : Irreducible pi242  u : (TwoSeries O)ˣ243  a : ℕ244  b : ℕ245  ha : 0 < a246  [instDomainR : IsDomain (ConcreteSurface O pi u a b)]247  [instRegular : IsRegularLocalRing (ConcreteSurface O pi u a b)]248  S : SurfaceData O (ConcreteSurface O pi u a b)249  hS_pi : S.pi = pi250  hS_t : S.t = surfaceT O pi u a b251  hS_x : S.x = surfaceX O pi u a b252  hS_a : S.a = a253  hS_b : S.b = b254  s : State255  shape : StateShape a b s256  atlas : IdealAtlas O (ConcreteSurface O pi u a b) S.pi s.degree257    (surfaceStateSet O (ConcreteSurface O pi u a b) S s)258attribute [instance] ConcreteMember.instCommRing ConcreteMember.instDomain259  ConcreteMember.instDVR ConcreteMember.instComplete ConcreteMember.instFinite260      ConcreteMember.instTop261  ConcreteMember.instTopRing ConcreteMember.instCompact ConcreteMember.instT2262      ConcreteMember.instSecond263  ConcreteMember.instMeas ConcreteMember.instBorel ConcreteMember.instDomainR264      ConcreteMember.instRegular265namespace ConcreteMember266variable (m : ConcreteMember)267/-- The concrete surface of a member. -/268abbrev R : Type := ConcreteSurface m.O m.pi m.u m.a m.b269/-- The member as a measured surface: same coefficient ring, surface, SurfaceData, state and270atlas. -/271def toMeasured : MeasuredSurface where272  O := m.O273  htop := m.htop274  R := m.R275  S := m.S276  s := m.s277  valid := m.shape.valid m.ha278  atlas := m.atlas279/-- The cell indices of a member, written on `m.R` (definitionally `m.toMeasured.cellIndex`):280an allowed pattern and a divisor realizing it. -/281abbrev cellIndex : Type :=282  Σ P : {P : TangentPattern m.s.degree // Allowed m.s P}, patternDivisors (ResidueField m.R) m.s P.1283end ConcreteMember284 285/-! ### Child data of a cell -/286 287section FromSurface288variable (R : Type) [CommRing R] (t x : R) [IsLocalRing R]289  (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (ResidueField R))290  (Dv : ExceptionalDivisor (ResidueField R)) (hinf : (infinityPoint R t x).IsPrime)291/-- The canonical map from the surface into the completed local ring at a point of the support:292through the right chart at ∞, through the left chart at an affine point. -/293def divisorFromSurface : ∀ Q, R →+* divisorLocalRing R t x e Dv hinf Q294  | ⟨none, _⟩ => (@completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf).comp295      (chartBase R x t)296  | ⟨some φ, _⟩ => (completedPointMap (BlowupChart R t x) (directionPoint R t x e φ)).comp297      (chartBase R t x)298end FromSurface299/-- The point of the support of Dv assigned to the j-th child by a cell assignment; kept as a300definition so that `divisorLocalRing … (asg.point j)` is not unfolded by instance resolution. -/301def CellAssignment.point {k : Type} [Field k] {s : State} {P : TangentPattern s.degree}302    {Dv : ExceptionalDivisor k}303    (asg : CellAssignment k s P Dv) (j : Fin (children s P).length) : divisorSupport Dv :=304  ⟨asg.pt j, (asg.supp _).mpr ⟨j, rfl⟩⟩305/-- A child member with its tower data over the parent coefficient ring `m.O`: a concrete member306`mc` in the state `s'` whose coefficient ring is a finite free `m.O`-algebra of rank δ with residue307field of cardinality q^δ and the same uniformizer, with coordinates `pc : mc.O ≃ₗ[m.O] m.O^δ` that308are a homeomorphism and a measurable equivalence under which the coefficient Haar measures of309`mc.O^r` are products of the parent's. Instance fields are non-dependent so that they are available310to the later fields. -/311structure ChildMember (m : ConcreteMember) (δ : ℕ) (s' : State) where312  mc : ConcreteMember313  [algO : Algebra m.O mc.O]314  [finO : Module.Finite m.O mc.O]315  [freeO : Module.Free m.O mc.O]316  hrank : Module.finrank m.O mc.O = δ317  hcard : Nat.card (ResidueField mc.O) = Nat.card (ResidueField m.O) ^ δ318  hpi : mc.pi = algebraMap m.O mc.O m.pi319  hstate : mc.s = s'320  pc : mc.O ≃ₗ[m.O] (Fin δ → m.O)321  pc_cont : Continuous pc ∧ Continuous pc.symm ∧ Measurable pc ∧ Measurable pc.symm322  pc_measure : ∀ r : ℕ, coefficientMeasure mc.O r =323    Measure.pi (fun _ : Fin r => Measure.map pc.symm (coefficientMeasure m.O δ))324attribute [instance] ChildMember.algO ChildMember.finO ChildMember.freeO325/-- The child data of a cell `c` (allowed pattern P, divisor Dv) of a concrete member `m`: the326exceptional-line isomorphism e with its formulas, the primality of the point at infinity, a327cell assignment matching the children list with the support of Dv, for each child index j a328child member (ChildMember) in the listed child state with the listed residue degree, and a ring329isomorphism Eq j from the completed local ring at the assigned point onto the child's surface330carrying the exceptional equation to T′, the old boundary to X′ at the boundary points, and the331coefficients through the tower. All fields are data or elementary predicates. -/332structure CellChildData (m : ConcreteMember) (c : m.cellIndex) where333  e : (BlowupChart m.R m.S.t m.S.x ⧸ chartExceptional m.R m.S.t m.S.x) ≃+* Polynomial334      (ResidueField m.R)335  he : ∀ r : m.R, e (Ideal.Quotient.mk (chartExceptional m.R m.S.t m.S.x)336      (chartBase m.R m.S.t m.S.x r)) =337    Polynomial.C (residue m.R r)338  heZ : e (Ideal.Quotient.mk (chartExceptional m.R m.S.t m.S.x) (chartSlope m.R m.S.t m.S.x)) =339      Polynomial.X340  hinf : (infinityPoint m.R m.S.t m.S.x).IsPrime341  asg : CellAssignment (ResidueField m.R) m.s c.1.1 c.2.1342  child : ∀ j : m.toMeasured.childIdx c, ChildMember m (m.toMeasured.childDelta c j)343      (m.toMeasured.childState c j)344  Eq : ∀ j, divisorLocalRing m.R m.S.t m.S.x e c.2.1 hinf (asg.point j) ≃+* (child j).mc.R345  hEq_e : ∀ j, Eq j (divisorException m.R m.S.t m.S.x e c.2.1 hinf (asg.point j)) = (child j).mc.S.t346  hEq_b : ∀ j, (asg.pt j = infinityDirection (ResidueField m.R) ∨ asg.pt j = zeroDirection347      (ResidueField m.R)) →348    Eq j (divisorBoundary m.R m.S.t m.S.x e c.2.1 hinf (asg.point j)) = (child j).mc.S.x349  hEq_c : ∀ (j) (r : m.O), Eq j (divisorFromSurface m.R m.S.t m.S.x e c.2.1 hinf (asg.point j)350    (algebraMap m.O m.R r)) = algebraMap (child j).mc.O (child j).mc.R351        (algebraMap m.O (child j).mc.O r)352namespace CellChildData353variable {m : ConcreteMember} {c : m.toMeasured.cellIndex} (D : CellChildData m c)354/-- The j-th child member. -/355abbrev mc (j : m.toMeasured.childIdx c) : ConcreteMember := (D.child j).mc356/-- The point of the support assigned to the j-th child. -/357abbrev point (j : m.toMeasured.childIdx c) : divisorSupport c.2.1 := D.asg.point j358/-- The pullback into the j-th child surface as an O-algebra homomorphism. -/359def alpha (j : m.toMeasured.childIdx c) : m.R →ₐ[m.O] (D.mc j).R where360  toRingHom := (D.Eq j).toRingHom.comp (divisorFromSurface m.R m.S.t m.S.x D.e c.2.1 D.hinf361      (D.point j))362  commutes' r := (D.hEq_c j r).trans (IsScalarTower.algebraMap_apply m.O (D.mc j).O (D.mc j).R363      r).symm364/-- The strict-transform map of the recursion record on this cell: the colon strict transform365(`strictTransformIdeal`) of a parent ideal along alpha j by the d-th power of the child's366exceptional equation T′, d the degree of the cell. -/367def Φ (J : Ideal m.R) (j : m.toMeasured.childIdx c) : Ideal (D.mc j).R :=368  strictTransformIdeal (D.alpha j) ((D.mc j).S.t) (m.toMeasured.cellDegree c) J369end CellChildData370 371/-! ### Recursion events -/372 373namespace SurfaceUniverse374variable (U : SurfaceUniverse)375/-- The type event: ideals of the state whose curve order has type σ. -/376def typeEvent (i : U.ι) (σ : FactorType) : Set (Ideal (U.M i).R) :=377  {J | J ∈ (U.M i).stateSet ∧ HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ}378/-- The recursion tree of J is finite: J is in a terminal state, or J lies in a cell all of whose379child ideals have finite trees. -/380inductive Terminates : ∀ i : U.ι, Ideal (U.M i).R → Prop381  | leaf (i : U.ι) (J : Ideal (U.M i).R) (hJ : J ∈ (U.M i).stateSet)382      (ht : (U.M i).s.terminal = true) : Terminates i J383  | node (i : U.ι) (c : (U.M i).cellIndex) (J : Ideal (U.M i).R) (hJ : J ∈ (U.M i).cell c)384      (hnt : (U.M i).s.terminal = false)385      (h : ∀ j, Terminates (U.child i c j) (U.Φ i c J j)) : Terminates i J386/-- The ideals of member `i` whose recursion tree is finite. -/387def terminatingSet (i : U.ι) : Set (Ideal (U.M i).R) := {J | U.Terminates i J}388/-- The ideals of the state set of member `i` whose recursion tree is infinite. -/389def nonterminatingSet (i : U.ι) : Set (Ideal (U.M i).R) := (U.M i).stateSet ∩ (U.terminatingSet i)ᶜ390/-- The measurable core of the type event: terminating ideals of type σ. -/391def termTypeEvent (i : U.ι) (σ : FactorType) : Set (Ideal (U.M i).R) :=392  U.typeEvent i σ ∩ U.terminatingSet i393/-- The self cells of member `i`. -/394def selfCells (i : U.ι) : Type := {c : (U.M i).cellIndex // (U.M i).IsSelfCell c}395/-- The non-self (exit) cells of member `i`. -/396def exitCells (i : U.ι) : Type := {c : (U.M i).cellIndex // ¬ (U.M i).IsSelfCell c}397/-- The part of a cell whose child ideals lie in the prescribed sides G_j. -/398def childBox (i : U.ι) (c : (U.M i).cellIndex) (G : ∀ j, Set (Ideal (U.M (U.child i c j)).R)) :399    Set (Ideal (U.M i).R) :=400  (U.M i).cell c ∩ U.Φ i c ⁻¹' Set.pi Set.univ G401/-- The part of a cell whose children terminate with types τ_j adding up (with residue scaling) to402σ. -/403def typeBox (i : U.ι) (c : (U.M i).cellIndex) (σ : FactorType) : Set (Ideal (U.M i).R) :=404  ⋃ (τ : (U.M i).childIdx c → FactorType) (_ : σ = ∑ j, scaleType ((U.M i).childDelta c j) (τ j)),405    U.childBox i c (fun j => U.termTypeEvent (U.child i c j) (τ j))406/-- At least k successive self returns. -/407def returnEvent : ℕ → ∀ i : U.ι, Set (Ideal (U.M i).R)408  | 0, i => (U.M i).stateSet409  | k+1, i => ⋃ c : U.selfCells i, U.childBox i c.1 (fun j => returnEvent k (U.child i c.1 j))410/-- Exactly k self returns, then an exit cell whose children terminate with total type σ. -/411def exitEvent (σ : FactorType) : ℕ → ∀ i : U.ι, Set (Ideal (U.M i).R)412  | 0, i => ⋃ c : U.exitCells i, U.typeBox i c.1 σ413  | k+1, i => ⋃ c : U.selfCells i, U.childBox i c.1 (fun j => exitEvent σ k (U.child i c.1 j))414/-- Exactly k self returns, then an exit cell all of whose children terminate. -/415def termExitEvent : ℕ → ∀ i : U.ι, Set (Ideal (U.M i).R)416  | 0, i => ⋃ c : U.exitCells i, U.childBox i c.1 (fun j => U.terminatingSet (U.child i c.1 j))417  | k+1, i => ⋃ c : U.selfCells i, U.childBox i c.1 (fun j => termExitEvent k (U.child i c.1 j))418/-- Exactly k self returns, then an exit cell with some nonterminating child. -/419def badExitEvent : ℕ → ∀ i : U.ι, Set (Ideal (U.M i).R)420  | 0, i => ⋃ c : U.exitCells i, ⋃ j₀ : (U.M i).childIdx c.1,421      U.childBox i c.1 (Function.update (fun _ => Set.univ) j₀422          (U.nonterminatingSet (U.child i c.1 j₀)))423  | k+1, i => ⋃ c : U.selfCells i, U.childBox i c.1 (fun j => badExitEvent k (U.child i c.1 j))424/-- The inductive statement of Theorem 8.1 for one member: the terminating type events are425measurable, the law coefficients are nonnegative and give the measures, the terminating set is426measurable and the nonterminating set is null. -/427def LawStatement (i : U.ι) : Prop :=Theorem 6.2428  (∀ σ : FactorType, MeasurableSet (U.termTypeEvent i σ) ∧429    0 ≤ (lawCoeff (stateLaw (U.M i).s) σ).eval ((U.M i).q : ℚ) ∧430    (U.M i).μ (U.termTypeEvent i σ) =431      densityValue (lawCoeff (stateLaw (U.M i).s) σ) (U.M i).q * (U.M i).μ (U.M i).stateSet) ∧432  MeasurableSet (U.terminatingSet i) ∧ (U.M i).μ (U.nonterminatingSet i) = 0433end SurfaceUniverse434/-! ### Patterns, base change and boundary contact -/435 436/-- An exceptional divisor has at most one allowed tangent pattern. -/437theorem allowed_pattern_of_divisor_unique (k : Type) [Field k] (s : State)438    (Dv : ExceptionalDivisor k) (P P' : TangentPattern s.degree) (hP : Allowed s P)439    (hP' : Allowed s P') (h : HasPattern k s Dv P) (h' : HasPattern k s Dv P') :440    P = P' := by441  obtain ⟨d1, t1, x1, o1⟩ := h442  obtain ⟨d2, t2, x2, o2⟩ := h'443  have hd : P.d = P'.d := Fin.ext (d1.symm.trans d2)444  have ht : P.rt = P'.rt := Fin.ext (t1.symm.trans t2)445  have hx : P.rx = P'.rx := Fin.ext <| by446    cases s with447    | single => exact hP.2.2.2.1.trans hP'.2.2.2.1.symm448    | crossing => exact x1.symm.trans x2449  have ho : P.other = P'.other := funext fun ij ↦ Fin.ext ((o1 ij).symm.trans (o2 ij))450  cases P; cases P'451  cases hd; cases ht; cases hx; cases ho452  rfl453 454/-- An injective linear map over a DVR whose cokernel has finite length becomes bijective455after base change to the fraction field. -/456theorem baseChange_bijective_of_finite_cokernel (O : Type) [CommRing O] [IsDomain O]457    [IsDiscreteValuationRing O] (M N : Type) [AddCommGroup M] [Module O M] [AddCommGroup N]458    [Module O N] (φ : M →ₗ[O] N) (hinj : Function.Injective φ) (ℓ : ℕ)459    (hℓ : Module.length O (N ⧸ LinearMap.range φ) = ℓ) :460    Function.Bijective (LinearMap.baseChange (BaseField O) φ) := by461  have hflat : Module.Flat O (BaseField O) :=462    IsLocalization.flat (BaseField O) (nonZeroDivisors O)463  constructor464  · rw [LinearMap.baseChange_eq_ltensor]465    exact Module.Flat.lTensor_preserves_injective_linearMap φ hinj466  · obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O467    have hmax := hpi.maximalIdeal_eq468    have key := linear_image_bound_from_cokernel_length O M N pi hmax φ ℓ hℓ469    have hne : algebraMap O (BaseField O) pi ≠ 0 := fun h ↦470      hpi.ne_zero (IsFractionRing.injective O (BaseField O) (by simpa using h))471    have hu : IsUnit ((algebraMap O (BaseField O) pi)^ℓ) := (pow_ne_zero ℓ hne).isUnit472    intro x473    induction x using TensorProduct.induction_on with474    | zero => exact ⟨0, map_zero _⟩475    | tmul k y =>476      obtain ⟨m, hm⟩ := key y477      obtain ⟨u, hu'⟩ := hu478      refine ⟨(k * ↑u⁻¹) ⊗ₜ[O] m, ?_⟩479      rw [LinearMap.baseChange_tmul, hm, ← TensorProduct.smul_tmul, Algebra.smul_def, map_pow,480        ← hu']481      congr 1482      rw [mul_left_comm, Units.mul_inv, mul_one]483    | add a b ha hb =>484      obtain ⟨a', rfl⟩ := ha485      obtain ⟨b', rfl⟩ := hb486      exact ⟨a' + b', map_add _ _ _⟩487 488/-- On the chart at infinity, the curve `∑ cᵢ W^(d-i)` meets the boundary `W = 0` iff its constant489coefficient `c_d` lies in the maximal ideal. -/490theorem boundary_contact_length_ne_zero_iff (R : Type) [CommRing R] [IsLocalRing R] (t x : R)491    (hmax : maximalIdeal R = Ideal.span {t, x}) (d : ℕ) (c : Fin (d + 1) → R) :492    Module.length (BlowupChart R x t) (BlowupChart R x t ⧸ (Ideal.span493      {(∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) * (chartSlope R x t)^(d - i.val))} ⊔494      Ideal.span {chartSlope R x t})) ≠ 0 ↔ c (Fin.last d) ∈ maximalIdeal R := by495  set B := BlowupChart R x t496  set W := chartSlope R x t497  set g : B := ∑ i : Fin (d+1), algebraMap R B (c i) * W^(d - i.val) with hg498  have hdiff : g - algebraMap R B (c (Fin.last d)) ∈ Ideal.span {W} := by499    rw [hg, Fin.sum_univ_castSucc]500    simp only [Fin.val_last, Fin.val_castSucc]501    rw [Nat.sub_self, pow_zero, mul_one, add_sub_cancel_right]502    refine Ideal.sum_mem _ fun i _ => ?_503    rw [show d - (i : ℕ) = (d - i - 1) + 1 by have := i.isLt; omega, pow_succ, ← mul_assoc]504    exact Ideal.mul_mem_left _ _ (Ideal.mem_span_singleton_self W)505  rw [Ne, Module.length_eq_zero_iff, Ideal.Quotient.subsingleton_iff]506  constructor507  · intro h508    by_contra hc509    refine h (Ideal.eq_top_of_isUnit_mem _ ?_ ((notMem_maximalIdeal.mp hc).map (algebraMap R B)))510    simpa using Ideal.sub_mem _ (Ideal.mem_sup_left (Ideal.mem_span_singleton_self g))511      (Ideal.mem_sup_right hdiff)512  · intro hc hI513    obtain ⟨ρ, hρ1, hρ2⟩ := boundary_chart_quotient_equiv R t x514    have htm : Ideal.span {t} ≤ maximalIdeal R := by515      rw [Ideal.span_singleton_le_iff_mem, hmax]; exact Ideal.subset_span (by simp)516    let φ : B →+* R ⧸ maximalIdeal R :=517      (Ideal.Quotient.factor htm).comp518        ((ρ : _ →+* _).comp (Ideal.Quotient.mk (Ideal.span {W})))519    have hφW : φ W = 0 := by520      change Ideal.Quotient.factor htm (ρ (Ideal.Quotient.mk (Ideal.span {W}) W)) = 0521      rw [hρ2]; simp522    have hφa : φ (algebraMap R B (c (Fin.last d))) = 0 := by523      change Ideal.Quotient.factor htm (ρ (Ideal.Quotient.mk (Ideal.span {W})524          (chartBase R x t (c (Fin.last d))))) = 0525      rw [hρ1]526      simpa using (Ideal.Quotient.eq_zero_iff_mem.mpr hc)527    have hφg : φ g = 0 := by528      obtain ⟨y, hy⟩ := Ideal.mem_span_singleton.mp hdiff529      rw [← sub_add_cancel g (algebraMap R B _), hy, map_add, map_mul, hφW, hφa, zero_mul, zero_add]530    have : (1 : B) ∈ Ideal.span {g} ⊔ Ideal.span {W} := hI ▸ Submodule.mem_top531    obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp this532    obtain ⟨u, rfl⟩ := Ideal.mem_span_singleton.mp hp533    obtain ⟨v, rfl⟩ := Ideal.mem_span_singleton.mp hq534    have := congrArg φ hpq535    rw [map_add, map_mul, map_mul, hφg, hφW] at this536    simp at this537 538/-- The strict-transform map sends an ideal of a cell into the state set of each child. -/539theorem cell_child_mem_stateSet (U : SurfaceUniverse) (i : U.ι) (hnt : (U.M i).s.terminal = false)540    (c : (U.M i).cellIndex) (J : Ideal (U.M i).R) (hJ : J ∈ (U.M i).cell c)541    (j : (U.M i).childIdx c) :542    U.Φ i c J j ∈ (U.M (U.child i c j)).stateSet :=543  Set.mem_univ_pi.mp ((U.Φ_bij i hnt c).mapsTo hJ) j544 545/-! ### Points of a cell -/546 547private theorem completedLocalAt_equiv_of_eq {R : Type} [CommRing R] [IsLocalRing R] (t x : R)548    (P P' : Ideal (BlowupChart R t x))549    [hP : P.IsPrime] [hP' : P'.IsPrime] (h : P = P') :550    ∃ ι : CompletedLocalAt (BlowupChart R t x) P ≃+* CompletedLocalAt (BlowupChart R t x) P',551      (∀ a, ι (completedPointMap _ P a) = completedPointMap _ P' a) ∧552      ∀ d J, Ideal.map ι.toRingHom553        (strictTransformAt R t x P d J) = strictTransformAt R t x P' d J := by554  subst h555  exact ⟨RingEquiv.refl _, fun _ ↦ rfl, fun _ _ ↦ Ideal.map_id _⟩556 557private theorem directionPoint_quot_surjective {R : Type} [CommRing R] [IsLocalRing R] (t x : R)558    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (ResidueField R)) :559    Function.Surjective (e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R t x))) :=560  e.surjective.comp Ideal.Quotient.mk_surjective561 562private theorem directionPoint_isMaximal {R : Type} [CommRing R] [IsLocalRing R] (t x : R)563    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (ResidueField R))564    (φ : AffineDirection (ResidueField R)) : (directionPoint R t x e φ).IsMaximal := by565  have : (Ideal.span {φ.val}).IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible φ.property.2566  exact Ideal.comap_isMaximal_of_surjective _ (directionPoint_quot_surjective t x e)567 568private theorem directionPoint_injective {R : Type} [CommRing R] [IsLocalRing R] (t x : R)569    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (ResidueField R)) :570    Function.Injective (directionPoint R t x e) := by571  intro φ ψ h572  have hs := Ideal.map_comap_of_surjective _ (directionPoint_quot_surjective t x e)573  have h3 : Ideal.span {φ.val} = Ideal.span {ψ.val} := by574    rw [← hs (Ideal.span {φ.val}), ← hs (Ideal.span {ψ.val})]575    exact congrArg (Ideal.map _) h576  rw [Ideal.span_singleton_eq_span_singleton] at h3577  exact Subtype.ext (Polynomial.eq_of_monic_of_associated φ.2.1 ψ.2.1 h3)578 579private theorem directionPoint_eq_comap {R : Type} [CommRing R] [IsLocalRing R] (t x : R)580    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (ResidueField R))581    (φ : AffineDirection (ResidueField R)) (Q : Ideal (BlowupOverlap R t x)) [Q.IsMaximal]582    (hQ : Q = (directionPoint R t x e φ).map583      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) :584    directionPoint R t x e φ = Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) := by585  have hmax := directionPoint_isMaximal t x e φ586  refine hmax.eq_of_le (Ideal.IsPrime.comap _).ne_top ?_587  rw [hQ]588  exact Ideal.le_comap_map589 590private theorem map_trans_symm_eq_span {A B C : Type} [CommRing A] [CommRing B] [CommRing C]591    (ι0 : A ≃+* B) (L : C ≃+* B)592    (I : Ideal A) (g : C) (h : Ideal.map ι0.toRingHom I = Ideal.span {L g}) :593    Ideal.map (ι0.trans L.symm : A →+* C) I = Ideal.span {g} := by594  have e2 := congrArg (Ideal.map L.symm.toRingHom) h595  rw [Ideal.map_map, Ideal.map_span, Set.image_singleton] at e2596  rw [RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply] at e2597  exact e2598 599/-- Given two-chart curve data matching the divisor of a cell, the children of the cell are in600bijection with the points of the curve data, compatibly with the completed local rings, the maps601from the surface, and the strict transforms. -/602theorem cell_datum_point_equiv (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)603    (J : Ideal m.R) (beta : BlowupRestriction m.R m.S.t m.S.x)604    (Df : TwoChartCurveData m.R m.S.t m.S.x beta) (hst : (∀ s : Df.ι ⊕ Df.ι0, strictTransformAt m.R605    m.S.t m.S.x (leftPoint Df s) (m.toMeasured.cellDegree c) J = Ideal.span {leftData Df s}) ∧ ∀ s :606    Df.ι ⊕ Df.ιinf, strictTransformAt m.R m.S.x m.S.t (rightPoint Df s) (m.toMeasured.cellDegree c)607    J = Ideal.span {rightData Df s}) (hm : MatchesDivisor D.e Df c.2.1)608    (hpos : (∀ i : Df.ι, 0 < commonMultiplicity Df i) ∧ (∀ k : Df.ι0, 0 < leftMultiplicity Df609    (Sum.inr k)) ∧ ∀ l : Df.ιinf, 0 < rightMultiplicity Df (Sum.inr l)) :610    ∃ ee : m.toMeasured.childIdx c ≃ AllPoints Df, ∀ j : m.toMeasured.childIdx c, ∃ ι :611      divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) ≃+* localRing Df (ee j),612      (∀ r : m.R, ι (divisorFromSurface m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) r) =613      localFromSurface Df (ee j) r) ∧ Ideal.map (ι : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1614      D.hinf (D.point j) →+* localRing Df (ee j)) (divisorStrictTransform m.R m.S.t m.S.x D.e c.2.1615      D.hinf (m.toMeasured.cellDegree c) J (D.point j)) = Ideal.span {localCurve Df (ee j)} := by616  let φc : Df.ι → AffineDirection (ResidueField m.R) := fun i => Classical.choose (hm.common i)617  have hφc : ∀ i, φc i ≠ zeroAffine _ ∧ Df.Q i = (directionPoint m.R m.S.t m.S.x D.e (φc i)).map618      (algebraMap (BlowupChart m.R m.S.t m.S.x) (BlowupOverlap m.R m.S.t m.S.x)) ∧619      c.2.1 (some (φc i)) = commonMultiplicity Df i := fun i => Classical.choose_spec (hm.common i)620  let p : AllPoints Df → divisorSupport c.2.1 := fun a => match a with621    | Sum.inl i => ⟨some (φc i), by rw [(hφc i).2.2]; exact hpos.1 i⟩622    | Sum.inr (Sum.inl k) => ⟨some (zeroAffine _), (hm.zero k).2 ▸ hpos.2.1 k⟩623    | Sum.inr (Sum.inr l) => ⟨none, (hm.inf l).2 ▸ hpos.2.2 l⟩624  have hcφ : ∀ i, directionPoint m.R m.S.t m.S.x D.e (φc i) =625      (Df.Q i).comap (algebraMap (BlowupChart m.R m.S.t m.S.x) (BlowupOverlap m.R m.S.t m.S.x)) :=626    fun i => directionPoint_eq_comap _ _ D.e (φc i) (Df.Q i) (hφc i).2.1627  have hloc : ∀ (a : AllPoints Df) (Q : divisorSupport c.2.1), p a = Q →628      ∃ ι : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf Q ≃+* localRing Df a,629        (∀ r : m.R, ι (divisorFromSurface m.R m.S.t m.S.x D.e c.2.1 D.hinf Q r) =630          localFromSurface Df a r) ∧631        Ideal.map (ι : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf Q →+* localRing Df a)632          (divisorStrictTransform m.R m.S.t m.S.x D.e c.2.1 D.hinf (m.toMeasured.cellDegree c) J633            Q) = Ideal.span {localCurve Df a} := by634    rintro a Q rfl635    rcases a with i | k | l636    · obtain ⟨ι0, h1, h2⟩ := completedLocalAt_equiv_of_eq m.S.t m.S.x _ _ (hcφ i)637      refine ⟨ι0.trans (Df.leftIso i).symm, fun r => ?_, ?_⟩638      · exact (congrArg (Df.leftIso i).symm (h1 _)).trans639          ((Df.leftIso i).symm_apply_eq.mpr (Df.leftIso_compat i _).symm)640      · exact map_trans_symm_eq_span ι0 (Df.leftIso i) _ (Df.g i)641          ((h2 _ J).trans (hst.1 (Sum.inl i)))642    · obtain ⟨ι0, h1, h2⟩ := completedLocalAt_equiv_of_eq m.S.t m.S.x643        (directionPoint m.R m.S.t m.S.x D.e (zeroAffine _))644        (leftPoint Df (Sum.inr k)) (hm.zero k).1.symm645      exact ⟨ι0, fun r => h1 _, (h2 _ J).trans (hst.1 (Sum.inr k))⟩646    · obtain ⟨ι0, h1, h2⟩ := @completedLocalAt_equiv_of_eq _ _ _ m.S.x m.S.t647        (infinityPoint m.R m.S.t m.S.x)648        (rightPoint Df (Sum.inr l)) D.hinf _ (hm.inf l).1.symm649      exact ⟨ι0, fun r => h1 _, (h2 _ J).trans (hst.2 (Sum.inr l))⟩650  have hp : Function.Bijective p := by651    constructor652    · intro a b hab653      have hv := congrArg Subtype.val hab654      rcases a with i | k | l <;> rcases b with i' | k' | l'655      · have h1 : φc i = φc i' := Option.some.inj hv656        exact congrArg Sum.inl (Df.inj (by rw [(hφc i).2.1, (hφc i').2.1, h1]))657      · exact absurd (Option.some.inj hv) (hφc i).1658      · simp [p] at hv659      · exact absurd (Option.some.inj hv).symm (hφc i').1660      · exact congrArg (fun z => Sum.inr (Sum.inl z)) (Df.inj0661          (by rw [(hm.zero k).1, (hm.zero k').1]))662      all_goals first663        | (simp [p] at hv; done)664        | exact congrArg (fun z => Sum.inr (Sum.inr z)) (Df.injinf665            (by rw [(hm.inf l).1, (hm.inf l').1]))666    · rintro ⟨q, hq⟩667      rcases q with _ | φ668      · obtain ⟨l⟩ := hm.inf_surj hq669        exact ⟨Sum.inr (Sum.inr l), rfl⟩670      · by_cases hφ : φ = zeroAffine _671        · subst hφ672          obtain ⟨k⟩ := hm.zero_surj hq673          exact ⟨Sum.inr (Sum.inl k), rfl⟩674        · obtain ⟨i, hi⟩ := hm.common_surj φ hφ hq675          refine ⟨Sum.inl i, Subtype.ext ?_⟩676          change some (φc i) = some φ677          congr 1678          apply directionPoint_injective m.S.t m.S.x D.e679          rw [hcφ i, directionPoint_eq_comap _ _ D.e φ (Df.Q i) hi]680  have hasg : Function.Bijective D.point := by681    refine ⟨fun j j' h => D.asg.inj (congrArg Subtype.val h), fun Q => ?_⟩682    obtain ⟨j, hj⟩ := (D.asg.supp Q.val).mp Q.property683    exact ⟨j, Subtype.ext hj⟩684  let ee : m.toMeasured.childIdx c ≃ AllPoints Df := (Equiv.ofBijective _ hasg).trans685      (Equiv.ofBijective p hp).symm686  exact ⟨ee, fun j ↦ hloc (ee j) (D.point j) (Equiv.ofBijective_apply_symm_apply p hp _)⟩687 688/-! ### Charts and measures of concrete members -/689 690/-- Transfer of a cell law through a single coordinate chart: if a chart covers the set `X` and the691type event in `X` agrees up to a null set with a set of measure given by the law, then the692coefficient measure of the polynomial type event equals the law density, and `μ X = q⁻ʳ`. -/693theorem chart_cell_law_generic (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]694    [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]695    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]696    [MeasurableSpace O] [BorelSpace O] (htop : IsAdic (maximalIdeal O)) (pi : O)697    (R : Type) [CommRing R] [Algebra O R] [MeasurableSpace (Ideal R)] (r : ℕ) (f : R)698    (b : Fin r → R) (hmeas : Measurable (coordinateIdeal pi f b))699    (X : Set (Ideal R)) (hcell : ∀ z : Fin r → O, coordinateIdeal pi f b z ∈ X)700    (μ : Measure (Ideal R)) (hμ : μ = (((Nat.card (ResidueField O)) : ℝ≥0∞)⁻¹ ^ r) •701    (coefficientMeasure O r).map (coordinateIdeal pi f b)) (htype : ∀ (z : Fin r → O)702    (σ : FactorType), HasAlgebraType O (R ⧸ coordinateIdeal pi f b z) σ ↔ HasPolynomialTypeF O703    (monicPolynomial O (pi • z)) σ) (σ : FactorType) (F N : Set (Ideal R)) (hFm : MeasurableSet F)704    (hFE : F ⊆ {J | J ∈ X ∧ HasAlgebraType O (R ⧸ J) σ}) (hEF :705    {J | J ∈ X ∧ HasAlgebraType O (R ⧸ J) σ} ⊆ F ∪ N) (hN : μ N = 0)706    (hF : μ F = densityValue (lawCoeff (stateLaw (State.single 1 r)) σ) (Nat.card (ResidueField O))707    * μ X) :708    coefficientMeasure O r {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} =709      densityValue (lawCoeff (stateLaw (State.single 1 r)) σ) (Nat.card (ResidueField O)) ∧ μ X =710      ((Nat.card (ResidueField O)) : ℝ≥0∞)⁻¹ ^ r := by711  set c := coordinateIdeal pi f b with hc712  set ν := coefficientMeasure O r with hν713  set q : ℝ≥0∞ := ((Nat.card (ResidueField O)) : ℝ≥0∞) with hq714  have := coefficient_measure_probability O htop r715  have hq0 : q ≠ 0 := by716    rw [hq]; exact_mod_cast (Nat.card_pos (α := ResidueField O)).ne'717  have hk0 : q⁻¹ ^ r ≠ 0 := pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))718  have hkt : q⁻¹ ^ r ≠ ⊤ := ENNReal.pow_ne_top (ENNReal.inv_ne_top.2 hq0)719  have hpreX : c ⁻¹' X = Set.univ := Set.eq_univ_of_forall hcell720  have hmapX : (ν.map c) X = 1 := by721    apply le_antisymm722    · calc (ν.map c) X ≤ (ν.map c) Set.univ := measure_mono (Set.subset_univ _)723        _ = 1 := by rw [Measure.map_apply hmeas MeasurableSet.univ]; simp724    · calc (1 : ℝ≥0∞) = ν (c ⁻¹' X) := by rw [hpreX]; simp725        _ ≤ (ν.map c) X := Measure.le_map_apply hmeas.aemeasurable _726  have hX : μ X = q⁻¹ ^ r := by727    rw [hμ, Measure.smul_apply, hmapX, smul_eq_mul, mul_one]728  refine ⟨?_, hX⟩729  have hpreE : c ⁻¹' {J | J ∈ X ∧ HasAlgebraType O (R ⧸ J) σ}730      = {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} := by731    ext z; simp only [Set.mem_preimage, Set.mem_ofPred_eq]732    exact ⟨fun h => (htype z σ).1 h.2, fun h => ⟨hcell z, (htype z σ).2 h⟩⟩733  have hNnull : ν (c ⁻¹' N) = 0 := by734    have h1 : (ν.map c) N = 0 := by735      rw [hμ, Measure.smul_apply, smul_eq_mul] at hN736      exact (mul_eq_zero.1 hN).resolve_left hk0737    exact le_antisymm (h1 ▸ Measure.le_map_apply hmeas.aemeasurable _) (zero_le)738  have hEq : ν (c ⁻¹' {J | J ∈ X ∧ HasAlgebraType O (R ⧸ J) σ}) = ν (c ⁻¹' F) := by739    apply le_antisymm740    · calc _ ≤ ν (c ⁻¹' F ∪ c ⁻¹' N) := by741            rw [← Set.preimage_union]; exact measure_mono (Set.preimage_mono hEF)742        _ ≤ ν (c ⁻¹' F) + ν (c ⁻¹' N) := measure_union_le _ _743        _ = ν (c ⁻¹' F) := by rw [hNnull, add_zero]744    · exact measure_mono (Set.preimage_mono hFE)745  rw [← hpreE, hEq]746  rw [hX, hμ, Measure.smul_apply, smul_eq_mul,747    Measure.map_apply hmeas hFm, mul_comm] at hF748  exact (ENNReal.mul_left_inj hk0 hkt).1 hF749 750/-- The coefficient Haar measure on `O^r` is the product of the coefficient measure on `O`,751transported along `O^1 ≃ O`, which is a homeomorphic measurable equivalence. -/752theorem coefficient_measure_pi_one (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]753    [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]754    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]755    [MeasurableSpace O] [BorelSpace O] (htop : IsAdic (maximalIdeal O)) (pi : O)756    (hpi : Irreducible pi) (r : ℕ) [SigmaFinite ((coefficientMeasure O 1).map757    (LinearEquiv.funUnique (Fin 1) O O))] :758    coefficientMeasure O r = Measure.pi (fun _ : Fin r => (coefficientMeasure O 1).map759      (LinearEquiv.funUnique (Fin 1) O O)) ∧ IsProbabilityMeasure760      ((coefficientMeasure O 1).map (LinearEquiv.funUnique (Fin 1) O O)) ∧ Continuous761      (LinearEquiv.funUnique (Fin 1) O O) ∧ Continuous (LinearEquiv.funUnique (Fin 1) O O).symm ∧762      Measurable (LinearEquiv.funUnique (Fin 1) O O) ∧ Measurable763      (LinearEquiv.funUnique (Fin 1) O O).symm := by764  have hc : Continuous (LinearEquiv.funUnique (Fin 1) O O) := continuous_apply _765  have hc' : Continuous (LinearEquiv.funUnique (Fin 1) O O).symm := continuous_pi766      (fun _ => continuous_id)767  have hm : Measurable (LinearEquiv.funUnique (Fin 1) O O) := hc.measurable768  have hm' : Measurable (LinearEquiv.funUnique (Fin 1) O O).symm := hc'.measurable769  obtain ⟨-, h1, h2, -, -⟩ := coefficient_space_strict_instances O htop pi hpi 1770  obtain ⟨-, h3, h4, -, -⟩ := coefficient_space_strict_instances O htop pi hpi r771  have hν : Measure.IsAddHaarMeasure ((coefficientMeasure O 1).map772      (LinearEquiv.funUnique (Fin 1) O O)) :=773    Measure.isAddHaarMeasure_map_of_isFiniteMeasure (coefficientMeasure O 1)774      (LinearEquiv.funUnique (Fin 1) O O).toAddMonoidHom hc (LinearEquiv.funUnique (Fin 1) O775          O).surjective776  have hp : IsProbabilityMeasure ((coefficientMeasure O 1).map777      (LinearEquiv.funUnique (Fin 1) O O)) :=778    Measure.isProbabilityMeasure_map hm.aemeasurable779  refine ⟨?_, hp, hc, hc', hm, hm'⟩780  exact Measure.isAddHaarMeasure_eq_of_isProbabilityMeasure _ _781 782/-- The division-coordinate module `O^deg × R` of a concrete member is `π`-adically complete. -/783theorem concrete_member_division_module_isAdicComplete (m : ConcreteMember) :784    IsAdicComplete (Ideal.span {m.toMeasured.S.pi})785      ((Fin m.toMeasured.s.degree → m.toMeasured.O) × m.toMeasured.R) := by786  change IsAdicComplete (Ideal.span {m.S.pi}) ((Fin m.s.degree → m.O) × ConcreteSurface m.O m.pi787    m.u m.a m.b)788  rw [m.hS_pi]789  exact division_coordinate_module_isAdicComplete m.O m.pi m.hpi m.u m.a m.b m.ha _790 791/-- Each chart of the atlas of a concrete member is an injective measurable map onto its792residue cell. -/793theorem concrete_member_charts (m : ConcreteMember) (i : m.atlas.ι) :794    Function.Injective (coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b) ∧ Set.range795      (coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b) = residueIdealCell796      (algebraMap m.O m.R m.S.pi) (m.atlas.chart i).f ∧ @Measurable (Fin m.s.degree → m.O)797      (Ideal m.R) inferInstance (idealChartSigma m.O m.R m.S.pi)798      (coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b) := by799  obtain ⟨hp0, hpm⟩ := surface_vertical_parameter m.O m.R m.S800  have : IsAdicComplete (Ideal.span {m.S.pi}) ((Fin m.s.degree → m.O) × m.R) :=801    concrete_member_division_module_isAdicComplete m802  have h1 := coordinate_ideal_cell_bijection m.O m.R m.s.degree m.S.pi803    (m.atlas.chart i).b (m.atlas.chart i).E hp0 hpm (m.atlas.chart i).f804    (m.atlas.chart i).division (m.atlas.chart i).regular805  exact ⟨h1.1, h1.2, coordinate_ideal_measurable_chart_sigma m.O m.htop m.R m.S.pi806    m.toMeasured.S.pi_irreducible hp0 hpm _ _ _ (m.atlas.chart i).isDivisionChart⟩807 808/-- The fixed-tangent cells of a concrete member are measurable. -/809theorem concrete_member_cell_measurable (m : ConcreteMember) (c : m.toMeasured.cellIndex) :810    MeasurableSet (m.toMeasured.cell c) := by811  have hcov := m.atlas.cover812  have hsub : m.toMeasured.cell c ⊆ ⋃ i, Set.range (coordinateIdeal (O := m.O) (R := m.R) m.S.pi813      (m.atlas.chart i).f (m.atlas.chart i).b) := by814    intro J hJ815    obtain ⟨i, hi⟩ := Set.mem_iUnion.1 (hcov.subset hJ.1)816    exact Set.mem_iUnion.2 ⟨i, (Set.ext_iff.1 (concrete_member_charts m i).2.1 J).2 hi⟩817  rw [← Set.inter_eq_left.2 hsub, Set.inter_iUnion]818  refine MeasurableSet.iUnion fun i => ?_819  have hirr : Irreducible m.S.pi := m.toMeasured.S.pi_irreducible820  obtain ⟨reps, hreps⟩ := coordinate_coset_representatives_exist m.O m.S.pi hirr m.s.degree821      (m.toMeasured.cellDegree c)822  have hmax : Ideal.span {m.S.pi} = maximalIdeal m.O := (hirr.maximalIdeal_eq).symm823  have hb := finite_coordinate_borel_cylinders m.O (maximalIdeal m.O) m.htop m.s.degree824  have hcoset : ∀ z₀ : Fin m.s.degree → m.O, MeasurableSet (coordinateCoset m.S.pi825      (m.toMeasured.cellDegree c) z₀) := by826    intro z₀827    have h2 : @MeasurableSet _ (adicCylinderSpace (maximalIdeal m.O) (Fin m.s.degree → m.O))828        (coordinateCoset m.S.pi (m.toMeasured.cellDegree c) z₀) := by829      rw [← hmax]830      exact MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨_, z₀, rfl⟩)831    rw [← hb] at h2832    exact h2833  have hf : Ideal.span {(m.atlas.chart i).f} ∈ surfaceStateSet m.O m.R m.S m.s :=834    hcov.symm.subset (Set.mem_iUnion.2 ⟨i, ⟨_, rfl⟩, by rw [Ideal.map_span]; simp⟩)835  exact fixed_tangent_cell_chart_measurable m.O m.R m.S m.s m.s.degree (m.atlas.chart i).b836    (m.atlas.chart i).f hf (concrete_member_charts m i).1 (m.atlas.chart i).isDivisionChart _837    (m.toMeasured.cellDegree c) le_rfl _ reps hreps hcoset838 839/-- Every admissible shape is realized: the concrete surface carries surface data with the concrete840parameters and an ideal atlas of the state set. -/841theorem concrete_member_data_exists (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]842    [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]843    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]844    [MeasurableSpace O] [BorelSpace O] (pi : O)845    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) (s : State)846    (hs : StateShape a b s) :847    ∃ (_ : IsDomain (ConcreteSurface O pi u a b)) (_ : IsRegularLocalRing848      (ConcreteSurface O pi u a b)) (S : SurfaceData O (ConcreteSurface O pi u a b)), S.pi = pi ∧849      S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b ∧ Nonempty850      (IdealAtlas O (ConcreteSurface O pi u a b) S.pi s.degree851      (surfaceStateSet O (ConcreteSurface O pi u a b) S s)) := by852  obtain ⟨hD, hR, S, hSpi, hSt, hSx, -, hSa, hSb⟩ :=853    concrete_surface_data_exists_unconditional O pi hpi u a b ha854  obtain ⟨e, he⟩ := concrete_surface_special_fiber_equiv O pi hpi u a b855  refine ⟨hD, hR, S, hSpi, hSt, hSx, hSa, hSb, ?_⟩856  cases s with857  | single a' c =>858    obtain ⟨h1, h2, h3⟩ := hs859    subst h1 h2860    obtain ⟨A, -⟩ := concrete_single_state_atlas_exists O pi hpi u a' ha S hSt hSa hSb e he c861        h3862    rw [hSpi]863    exact ⟨A⟩864  | crossing a' b' c h =>865    obtain ⟨h1, h2, h3, h4, h5⟩ := hs866    subst h1 h2867    obtain ⟨A, -⟩ := concrete_crossing_state_atlas_exists O pi hpi u a' b' ha h3 S hSt hSx hSa868        hSb e he c h h4 h5869    rw [hSpi]870    exact ⟨A⟩871 872/-- The state set of a concrete member is measurable. -/873theorem concrete_member_stateSet_measurable (m : ConcreteMember) :874    MeasurableSet m.toMeasured.stateSet := by875  have h : m.toMeasured.stateSet = ⋃ i, Set.range (coordinateIdeal m.S.pi (m.atlas.chart i).f876      (m.atlas.chart i).b) := by877    refine (m.atlas.cover).trans ?_878    exact Set.iUnion_congr fun i => (concrete_member_charts m i).2.1.symm879  rw [h]880  have : Fintype m.atlas.ι := m.atlas.fin881  have : Countable m.atlas.ι := Finite.to_countable882  refine @MeasurableSet.iUnion _ _ (idealChartSigma m.O m.R m.S.pi) _ _ fun i => ?_883  rw [← Set.image_univ]884  exact chart_image_measurable_chart_sigma m.O m.R m.S.pi _ _ _885    (m.atlas.chart i).isDivisionChart _ MeasurableSet.univ886 887/-- The state measure of a concrete member is finite and concentrated on the state set. -/888theorem concrete_member_measure_finite_support (m : ConcreteMember) :889    IsFiniteMeasure m.toMeasured.μ ∧ ∀ X : Set (Ideal m.toMeasured.R), m.toMeasured.μ X =890      m.toMeasured.μ (X ∩ m.toMeasured.stateSet) := by891  have hS := concrete_member_stateSet_measurable m892  have hnull : m.toMeasured.μ m.toMeasured.stateSetᶜ = 0 := by893    change stateMeasure _ _ _ _ _ _ _ = 0894    unfold stateMeasure895    rw [Measure.smul_apply, Measure.finsetSum_apply]896    simp only [smul_eq_mul]897    rw [Finset.sum_eq_zero, mul_zero]898    intro i _899    obtain ⟨-, hr, hm⟩ := concrete_member_charts m i900    unfold chartMeasure901    refine (Measure.map_apply hm hS.compl).trans ?_902    have : (coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b) ⁻¹'903        m.toMeasured.stateSetᶜ = ∅ := by904      refine Set.eq_empty_of_forall_notMem fun x hx ↦905        hx (m.atlas.cover.symm.subset (Set.mem_iUnion.2 ⟨i, ?_⟩))906      rw [← hr]; exact ⟨x, rfl⟩907    exact (congrArg (coefficientMeasure m.O m.s.degree) this).trans measure_empty908  refine ⟨⟨?_⟩, ?_⟩909  · let inst : MeasurableSpace (Ideal m.R) := m.toMeasured.measurableSpaceIdeal910    have h := state_measure_total_mass m.O m.R m.htop m.S.pi m.s.degree _ m.atlas911      (fun i => (concrete_member_charts m i).2.2)912    refine h.trans_lt ?_913    exact ENNReal.mul_lt_top (ENNReal.natCast_lt_top _) (ENNReal.pow_lt_top914      (ENNReal.inv_lt_top.2 (by exact_mod_cast Nat.card_pos (α := ResidueField m.O))))915  · intro X916    rw [← measure_inter_add_sdiff X hS, measure_mono_null (Set.sdiff_subset_compl _ _) hnull,917        add_zero]918 919/-! ### Generators of state ideals -/920 921/-- Multiplication by the parameter `t` of a concrete member is injective. -/922theorem concrete_member_mul_t_injective {m : ConcreteMember} {e : m.toMeasured.R}923    (he : e = m.toMeasured.S.t) : Function.Injective (fun z : m.toMeasured.R => e * z) := by924  have h := (concrete_surface_equiv_regular_pair m.R m.O m.pi m.hpi m.u m.a m.b m.ha925    (RingEquiv.refl _)).2.2926  rw [he]927  change Function.Injective (fun z : m.R => m.S.t * z)928  rwa [m.hS_t]929 930/-- The degree of the state of a concrete member is positive. -/931theorem concrete_member_one_le_degree (m : ConcreteMember) : 1 ≤ m.toMeasured.s.degree := by932  have hv : m.toMeasured.s.Valid := m.toMeasured.valid933  revert hv934  cases m.toMeasured.s with935  | single a c => exact fun hv => Nat.mul_pos hv.1 hv.2936  | crossing a b c h =>937    intro hv; have := Nat.mul_pos hv.1 hv.2.2.1; simp only [State.degree]; omega938 939/-- A generator of an ideal of the state set meets `T = 0` with `O`-length the first contact940of the state. -/941theorem concrete_member_state_generator_contact_length (m : ConcreteMember) (g : m.toMeasured.R)942    (hg : Ideal.span {g} ∈ m.toMeasured.stateSet) :943    Module.length m.toMeasured.O (m.toMeasured.R ⧸ (Ideal.span {g} ⊔ Ideal.span {m.toMeasured.S.t}))944      = (m.toMeasured.s.firstContact : ℕ∞) := by945  have hfin : Finite (ResidueField m.toMeasured.R) :=946    Finite.of_equiv _ m.toMeasured.S.residueEquiv.toEquiv947  have hcard : Nat.card (ResidueField m.toMeasured.R) =948      Nat.card (ResidueField m.toMeasured.O) ^ 1 := by949    rw [pow_one]; exact (Nat.card_congr m.toMeasured.S.residueEquiv.toEquiv).symm950  obtain ⟨_, _, hc⟩ := hg951  have key : Module.length m.toMeasured.R (m.toMeasured.R ⧸ (Ideal.span {g} ⊔ Ideal.span952      {m.toMeasured.S.t})) = (m.toMeasured.s.firstContact : ℕ∞) := by953    generalize m.toMeasured.s = s at hc ⊢954    cases s with955    | single a c => exact hc.2.2956    | crossing a b c h => exact hc.2.2.1957  have := length_scaling_of_residue_card m.toMeasured.O m.toMeasured.R 1 hcard958    (m.toMeasured.R ⧸ (Ideal.span {g} ⊔ Ideal.span {m.toMeasured.S.t})) m.toMeasured.s.firstContact959        key960  simpa using this961 962/-- A generator of an ideal of the state set is a nonzero nonunit that is regular modulo `π`. -/963theorem concrete_member_state_generator_regular (m : ConcreteMember) (g : m.toMeasured.R)964    (hg : Ideal.span {g} ∈ m.toMeasured.stateSet) :965    g ≠ 0 ∧ ¬ IsUnit g ∧ Function.Injective (fun y : m.toMeasured.R ⧸ Ideal.span966      {(algebraMap m.toMeasured.O m.toMeasured.R m.toMeasured.S.pi)} => y * Ideal.Quotient.mk967      (Ideal.span {(algebraMap m.toMeasured.O m.toMeasured.R m.toMeasured.S.pi)}) g) := by968  have hprop := surface_state_ideal_proper _ _ m.toMeasured.S m.toMeasured.s _ hg969  have hnu : ¬ IsUnit g := fun h => hprop (Ideal.span_singleton_eq_top.mpr h)970  have hpi := surface_vertical_parameter m.toMeasured.O m.toMeasured.R m.toMeasured.S971  have hcov := m.toMeasured.atlas.cover972  have hg' : Ideal.span {g} ∈ ⋃ i, residueIdealCell (algebraMap m.toMeasured.O m.toMeasured.R973      m.toMeasured.S.pi) (m.toMeasured.atlas.chart i).f := by974    rw [← hcov]; exact hg975  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hg'976  set mk := Ideal.Quotient.mk (Ideal.span {(algebraMap m.toMeasured.O m.toMeasured.R977      m.toMeasured.S.pi)}) with hmk978  have h1 : Ideal.span {mk (m.toMeasured.atlas.chart i).f} = Ideal.span {mk g} := by979    rw [← principal_ideal_image _ _ mk g]980    exact hi.2.symm981  obtain ⟨u, hu⟩ := regular_principal_generators_associated _ _ _982    (m.toMeasured.atlas.chart i).regular h1983  have hreg : Function.Injective (fun y : m.toMeasured.R ⧸ Ideal.span984      {(algebraMap m.toMeasured.O m.toMeasured.R m.toMeasured.S.pi)} => y * mk g) := by985    intro a b hab986    simp only [hu] at hab987    have : (a * ↑u) * mk (m.toMeasured.atlas.chart i).f = (b * ↑u) * mk988        (m.toMeasured.atlas.chart i).f := by989      simpa [mul_assoc, mul_comm, mul_left_comm] using hab990    have := (m.toMeasured.atlas.chart i).regular this991    exact (IsUnit.mul_left_inj u.isUnit).mp this992  refine ⟨fun h0 ↦ ?_, hnu, hreg⟩993  have h01 : (1 : m.toMeasured.R ⧸ Ideal.span {algebraMap m.toMeasured.O m.toMeasured.R994      m.toMeasured.S.pi})995      = 0 := hreg (by simp [h0])996  exact (mem_maximalIdeal _).mp hpi.2997    (Ideal.span_singleton_eq_top.mp (Ideal.Quotient.zero_eq_one_iff.mp h01.symm))998 999/-- A division chart centred at a generator of an ideal of the state set is injective, lands in1000the state set, and scales the coefficient measure by `q^(-deg s)`. -/1001theorem concrete_member_division_chart_measure (m : ConcreteMember) (g : m.toMeasured.R)1002    (hg : Ideal.span {g} ∈ m.toMeasured.stateSet) (bc : Fin m.toMeasured.s.degree → m.toMeasured.R)1003    (E : m.toMeasured.R ≃ₗ[m.toMeasured.O] ((Fin m.toMeasured.s.degree → m.toMeasured.O) ×1004    m.toMeasured.R)) (hE : ∀ w, E.symm w = divisionMap g bc w) :1005    Function.Injective (coordinateIdeal m.toMeasured.S.pi g bc) ∧ Set.range1006      (coordinateIdeal m.toMeasured.S.pi g bc) ⊆ m.toMeasured.stateSet ∧ ∀ S : Set1007      (Fin m.toMeasured.s.degree → m.toMeasured.O), MeasurableSet S → m.toMeasured.μ1008      (coordinateIdeal m.toMeasured.S.pi g bc '' S) = (m.toMeasured.q : ℝ≥0∞)⁻¹ ^1009      m.toMeasured.s.degree * coefficientMeasure m.toMeasured.O m.toMeasured.s.degree S := by1010  classical1011  have := concrete_member_division_module_isAdicComplete m1012  obtain ⟨hp0, hpm⟩ := surface_vertical_parameter m.toMeasured.O m.toMeasured.R m.toMeasured.S1013  obtain ⟨-, -, hreg⟩ := concrete_member_state_generator_regular m g hg1014  have hch : IsDivisionChart _ _ m.toMeasured.S.pi g bc := ⟨⟨E, hE⟩, hreg⟩1015  have hinj : Function.Injective (coordinateIdeal m.toMeasured.S.pi g bc) :=1016    coordinate_ideal_injective _ _ _ _ bc E hp0 hpm g hE hreg1017  -- the atlas chart containing span {g}1018  obtain ⟨i, hi⟩ : ∃ i, Ideal.span {g} ∈ _ := by1019    change Ideal.span {g} ∈ surfaceStateSet _ _ _ _ at hg1020    rwa [m.toMeasured.atlas.cover, Set.mem_iUnion] at hg1021  have hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap m.toMeasured.O m.toMeasured.R1022      m.toMeasured.S.pi}) (m.toMeasured.atlas.chart i).f}1023      = Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap m.toMeasured.O m.toMeasured.R1024          m.toMeasured.S.pi}) g} := by1025    rw [← hi.2, principal_ideal_image]1026  have hcell : ∀ z, coordinateIdeal m.toMeasured.S.pi g bc z ∈1027      residueIdealCell (algebraMap m.toMeasured.O m.toMeasured.R m.toMeasured.S.pi)1028          (m.toMeasured.atlas.chart i).f := fun z =>1029    have := coordinate_ideal_in_residue_cell _ _ _ m.toMeasured.S.pi bc g z1030    ⟨this.1, this.2.trans hres.symm⟩1031  have hrange : Set.range (coordinateIdeal m.toMeasured.S.pi g bc) ⊆ m.toMeasured.stateSet := by1032    rintro _ ⟨z, rfl⟩1033    change _ ∈ surfaceStateSet _ _ _ _1034    rw [m.toMeasured.atlas.cover, Set.mem_iUnion]1035    exact ⟨i, hcell z⟩1036  refine ⟨hinj, hrange, ?_⟩1037  intro S hS1038  set c := m.toMeasured.atlas.chart i with hc_def1039  obtain ⟨g', c', F, h0, hF, hfg, hreg', hcoord⟩ :=1040    division_chart_same_cell_recenter _ _ m.toMeasured.S.pi hpm _ c.f g c.b bc1041      c.isDivisionChart hch hres1042  have hmeas' := coordinate_ideal_measurable_chart_sigma _ m.toMeasured.htop _ _1043    m.toMeasured.S.pi_irreducible hp0 hpm _ g' c' ⟨⟨F, hF⟩, hreg'⟩1044  have hmeasΨ := coordinate_ideal_measurable_chart_sigma _ m.toMeasured.htop _ _1045    m.toMeasured.S.pi_irreducible hp0 hpm _ g bc hch1046  have hpush : (coefficientMeasure m.toMeasured.O m.toMeasured.s.degree).map1047      (coordinateIdeal m.toMeasured.S.pi c.f c.b)1048      = (coefficientMeasure m.toMeasured.O m.toMeasured.s.degree).map1049          (coordinateIdeal m.toMeasured.S.pi g bc) := by1050    rw [ideal_chart_pushforward_independent _ _ _ _ c.b c.E hp0 hpm c.f c.division c.regular g' c' F1051      hF hreg' h0 hfg m.toMeasured.htop m.toMeasured.S.pi_irreducible hmeas']1052    exact congrArg (Measure.map · _) (funext fun z => (hcoord z).symm)1053  have hSm : MeasurableSet (coordinateIdeal m.toMeasured.S.pi g bc '' S) :=1054    chart_image_measurable_chart_sigma _ _ _ _ g bc hch S hS1055  have hsum : ∀ k, chartMeasure m.toMeasured.O m.toMeasured.R m.toMeasured.S.pi1056      m.toMeasured.s.degree1057      (m.toMeasured.atlas.chart k) (coordinateIdeal m.toMeasured.S.pi g bc '' S)1058      = if k = i then coefficientMeasure m.toMeasured.O m.toMeasured.s.degree S else 0 := by1059    intro k1060    obtain ⟨-, hrk, hmk⟩ := concrete_member_charts m k1061    unfold chartMeasure1062    split_ifs with hk1063    · subst hk1064      rw [hpush, Measure.map_apply hmeasΨ hSm, Set.preimage_image_eq _ hinj]1065    · rw [Measure.map_apply (by exact hmk) hSm]1066      convert measure_empty (μ := coefficientMeasure m.toMeasured.O m.toMeasured.s.degree)1067      rw [Set.eq_empty_iff_forall_notMem]1068      rintro z ⟨w, -, hw⟩1069      exact Set.disjoint_left.mp (m.toMeasured.atlas.disjoint hk) (hrk ▸ Set.mem_range_self z)1070        (hw ▸ hcell w)1071  change stateMeasure m.toMeasured.O m.toMeasured.R m.toMeasured.S.pi m.toMeasured.s.degree1072      m.toMeasured.q1073    m.toMeasured.atlas _ = _1074  unfold stateMeasure1075  rw [Measure.smul_apply, Measure.finsetSum_apply, smul_eq_mul]1076  simp only [hsum, Finset.sum_ite_eq', Finset.mem_univ, if_true]1077 1078/-- A generator `g` of an ideal of the state set and the parameter `T` form a regular sequence1079in both orders. -/1080theorem concrete_member_state_generator_transverse (m : ConcreteMember) (g : m.toMeasured.R)1081    (hg : Ideal.span {g} ∈ m.toMeasured.stateSet) :1082    Function.Injective (fun w : m.toMeasured.R ⧸ Ideal.span {m.toMeasured.S.t} => Ideal.Quotient.mk1083      (Ideal.span {m.toMeasured.S.t}) g * w) ∧ Function.Injective1084      (fun y : m.toMeasured.R ⧸ Ideal.span {g} => Ideal.Quotient.mk (Ideal.span {g})1085      m.toMeasured.S.t * y) := by1086  change m.R at g1087  -- finite contact1088  have hfin : idealContact m.R (Ideal.span {g}) (surfaceT m.O m.pi m.u m.a m.b) ≠ ⊤ := by1089    obtain ⟨_, _, hs⟩ := hg1090    rw [← m.hS_t]1091    revert hs1092    cases m.toMeasured.s with1093    | single a c => rintro ⟨_, _, h⟩; exact fun h' ↦ ENat.natCast_ne_top c (h.symm.trans h')1094    | crossing a b c _ =>1095      rintro ⟨_, _, h, _⟩; exact fun h' ↦ ENat.natCast_ne_top c (h.symm.trans h')1096  obtain ⟨q, -⟩ := concrete_surface_quotient_T_equiv m.O m.pi m.hpi m.u m.a m.b m.ha1097  have h878 := concrete_surface_equiv_curve_length_and_regular m.R m.O m.pi m.u m.a m.b1098    (RingEquiv.refl _) q g1099  have h872 := (concrete_surface_equiv_regular_pair m.R m.O m.pi m.hpi m.u m.a m.b m.ha1100    (RingEquiv.refl _)).2.21101  rw [show (RingEquiv.refl m.R).symm = RingEquiv.refl m.R from rfl] at h878 h8721102  simp only [RingEquiv.refl_apply] at h878 h8721103  set t : m.R := surfaceT m.O m.pi m.u m.a m.b with ht1104  have h1 : Function.Injective (fun w : m.R ⧸ Ideal.span {t} =>1105      Ideal.Quotient.mk (Ideal.span {t}) g * w) := by1106    refine h878.2.mpr ?_1107    intro h01108    apply hfin1109    unfold idealContact1110    rw [ideal_contact_generator, contact]1111    exact h878.1.trans (by rw [h0, PowerSeries.order_zero])1112  have hker : ∀ y : m.R ⧸ Ideal.span {g}, Ideal.Quotient.mk (Ideal.span {g}) t * y = 0 → y = 0 := by1113    intro y hy1114    obtain ⟨h, rfl⟩ := Ideal.Quotient.mk_surjective y1115    rw [← map_mul, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton'] at hy1116    obtain ⟨r, hr⟩ := hy1117    have hr0 : Ideal.Quotient.mk (Ideal.span {t}) g * Ideal.Quotient.mk (Ideal.span {t}) r = 0 := by1118      rw [← map_mul, mul_comm, hr, Ideal.Quotient.eq_zero_iff_mem]1119      exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self t)1120    have hr1 : Ideal.Quotient.mk (Ideal.span {t}) r = 0 := h1 (by simp only; linear_combination hr0)1121    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton'] at hr11122    obtain ⟨r', rfl⟩ := hr11123    have : h = g * r' := by1124      apply h8721125      change t * h = t * (g * r')1126      rw [← hr]; ring1127    rw [Ideal.Quotient.eq_zero_iff_mem, this]1128    exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self g)1129  have h2 : Function.Injective (fun y : m.R ⧸ Ideal.span {g} =>1130      Ideal.Quotient.mk (Ideal.span {g}) t * y) := fun a b hab =>1131    sub_eq_zero.mp (hker (a - b) (by simp only at hab; linear_combination hab))1132  change Function.Injective (fun w : m.R ⧸ Ideal.span {m.S.t} =>1133      Ideal.Quotient.mk (Ideal.span {m.S.t}) g * w) ∧1134    Function.Injective (fun y : m.R ⧸ Ideal.span {g} =>1135      Ideal.Quotient.mk (Ideal.span {g}) m.S.t * y)1136  rw [m.hS_t]1137  exact ⟨h1, h2⟩1138 1139/-- A curve on a concrete surface with crossing contacts `(c, h)` has free curve order of rank1140`a c + b h`. -/1141private theorem concrete_surface_crossing_curve_free (O : Type) [CommRing O] [IsDomain O]1142    [IsDiscreteValuationRing O] [IsAdicComplete (maximalIdeal O) O] (pi : O) (hpi : Irreducible pi)1143    (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) (hb : 0 < b) (f : ConcreteSurface O pi u a b)1144    (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})1145    ≃+* SpecialFiber (ResidueField O) a b) (c h : ℕ) (hc : 0 < c)1146    (hcontact : contact (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b)1147    pi}) f)) (fiberT (ResidueField O) a b) = c) (hxcontact : contact1148    (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f))1149    (fiberX (ResidueField O) a b) = h) :1150    Module.Free O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧ Module.Finite O1151      (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧ Module.finrank O1152      (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) = a*c+b*h := by1153  have hreg := special_fiber_crossing_contact_regular _ a b c h ha hb _ hcontact hxcontact1154  have hinj := concrete_surface_residue_regular_of_special_fiber O pi u a b f e hreg1155  have hlen := crossing_special_fiber_length _ a b c h ha hb _ hcontact hxcontact1156  have hlen2 := concrete_surface_special_fiber_length_transport O pi u a b f e1157  have hfu : ¬ IsUnit f := by1158    intro hu1159    have hu' : IsUnit (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b)1160        pi}) f)) :=1161      (hu.map (Ideal.Quotient.mk _)).map e1162    have h1 : Ideal.span {e (Ideal.Quotient.mk (Ideal.span {algebraMap O1163        (ConcreteSurface O pi u a b) pi}) f)} = ⊤ :=1164      (Ideal.span_singleton_eq_top).2 hu'1165    rw [h1] at hlen1166    simp only [Module.length_eq_zero] at hlen1167    have : a*c+b*h = 0 := by exact_mod_cast hlen.symm1168    have := Nat.mul_pos ha hc1169    omega1170  exact concrete_surface_curve_free_of_length O pi hpi u a b ha f hinj (a*c+b*h)1171      (hlen2.trans hlen)1172 1173private theorem single_curve_free_of_eq_zero (O : Type) [CommRing O] [IsDomain O]1174    [IsDiscreteValuationRing O] [IsAdicComplete (maximalIdeal O) O] (pi : O) (hpi : Irreducible pi)1175    (u : (TwoSeries O)ˣ) (a b : ℕ) (hb : b = 0) (ha : 0 < a) (f : ConcreteSurface O pi u a b)1176    (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})1177      ≃+*1178      SpecialFiber (ResidueField O) a b) (c : ℕ) (hc : 0 < c)1179    (hcontact : contact (e (Ideal.Quotient.mk1180      (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f)) (fiberT (ResidueField O) a b)1181      = c) :1182    Module.Free O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧1183    Module.Finite O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧1184    Module.finrank O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) = a * c := by1185  subst hb1186  exact concrete_surface_single_curve_free O pi hpi u a ha f e c hc hcontact1187 1188/-- The curve order `R/J` of an ideal `J` in the state set of a concrete member is a free `O`-module1189of rank the degree of the state. -/1190theorem concrete_member_curve_order_free (m : ConcreteMember) (J : Ideal m.R)Lemma 2.11191    (hJ : J ∈ m.toMeasured.stateSet) :1192    Module.Free m.O (m.R ⧸ J) ∧ Module.Finite m.O (m.R ⧸ J) ∧ Module.finrank m.O (m.R ⧸ J) =1193      m.s.degree := by1194  obtain ⟨⟨f, rfl⟩, -, hmatch⟩ := hJ1195  obtain ⟨e, he⟩ := concrete_surface_special_fiber_equiv m.O m.pi m.hpi m.u m.a m.b1196  have hc := concrete_surface_contact_eq_special_fiber_contact m.O m.pi m.u m.a m.b m.ha e he1197      f1198  have hT : m.S.t = surfaceT m.O m.pi m.u m.a m.b := m.hS_t1199  have hsh := m.shape1200  have hmatch' : (match m.s with1201    | .single a c => m.S.a = a ∧ m.S.b = 0 ∧ idealContact m.R (Ideal.span {f}) m.S.t = c1202    | .crossing a b c h => m.S.a = a ∧ m.S.b = b ∧1203      idealContact m.R (Ideal.span {f}) m.S.t = c ∧ idealContact m.R (Ideal.span {f}) m.S.x = h) :=1204          hmatch1205  revert hmatch' hsh1206  generalize m.s = s1207  intro hsh hmatch'1208  cases s with1209  | single a' c =>1210    obtain ⟨rfl, hb, hc0⟩ := hsh1211    exact single_curve_free_of_eq_zero m.O m.pi m.hpi m.u _ m.b hb m.ha f e c hc01212      (by rw [← hc.1, ← hT]; exact hmatch'.2.2)1213  | crossing a' b' c h =>1214    obtain ⟨rfl, rfl, hb, hc0, hh0⟩ := hsh1215    exact concrete_surface_crossing_curve_free m.O m.pi m.hpi m.u _ _ m.ha hb f e c h hc01216      (by rw [← hc.1, ← hT]; exact hmatch'.2.2.1)1217      (by rw [← hc.2 hb, ← m.hS_x]; exact hmatch'.2.2.2)1218 1219/-- Every generator of an ideal of the state set admits a division chart. -/1220theorem concrete_member_state_generator_division (m : ConcreteMember) (g : m.toMeasured.R)1221    (hg : Ideal.span {g} ∈ m.toMeasured.stateSet) :1222    ∃ (bc : Fin m.toMeasured.s.degree → m.toMeasured.R) (E : m.toMeasured.R ≃ₗ[m.toMeasured.O]1223      ((Fin m.toMeasured.s.degree → m.toMeasured.O) × m.toMeasured.R)), ∀ w, E.symm w = divisionMap1224      g bc w := by1225  obtain ⟨hF, hFin, hr⟩ := concrete_member_curve_order_free m _ hg1226  have hg0 := (concrete_member_state_generator_regular m g hg).11227  have := m.instDomainR1228  have : Module.Free m.toMeasured.O (m.toMeasured.R ⧸ Ideal.span {g}) := hF1229  have : Module.Finite m.toMeasured.O (m.toMeasured.R ⧸ Ideal.span {g}) := hFin1230  let B := Module.finBasisOfFinrankEq m.toMeasured.O (m.toMeasured.R ⧸ Ideal.span {g}) hr1231  choose bc hbc using fun i => Ideal.Quotient.mk_surjective (B i)1232  obtain ⟨E, hE⟩ := division_linear_equivalence m.toMeasured.O m.toMeasured.R m.toMeasured.s.degree1233      g B bc hbc hg01234  exact ⟨bc, E, hE⟩1235 1236/-! ### Type additivity and the Čech connecting map -/1237 1238/-- Type additivity: if `R/J` embeds with finite-length cokernel into a product of algebras over1239unramified extensions, then the type of `R/J` is the sum of the residue-scaled types. -/1240theorem concrete_type_add_of_index_map (m : ConcreteMember) (n : ℕ) (mc : Fin n → ConcreteMember)1241    [∀ j, Algebra m.O (mc j).O] [∀ j, Module.Finite m.O (mc j).O] [∀ j, Module.Free m.O (mc j).O]1242    (δ : Fin n → ℕ) (hrank : ∀ j, Module.finrank m.O (mc j).O = δ j)1243    (hpi : ∀ j, Irreducible (algebraMap m.O (mc j).O m.pi)) (J : Ideal m.R) (B : Fin n → Type)1244    [∀ j, CommRing (B j)] [∀ j, Algebra m.O (B j)] [∀ j, Algebra (mc j).O (B j)]1245    [∀ j, IsScalarTower m.O (mc j).O (B j)] [∀ j, Module.Finite (mc j).O (B j)]1246    [∀ j, Module.Free (mc j).O (B j)] (ψ : (m.R ⧸ J) →ₐ[m.O] ∀ j, B j) (hψ : Function.Injective ψ)1247    (ℓ : ℕ) (hlen : Module.length m.O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = (ℓ : ℕ∞))1248    (τ : Fin n → FactorType) (hτ : ∀ j, HasAlgebraType (mc j).O (B j) (τ j)) :1249    HasAlgebraType m.O (m.R ⧸ J) (∑ j, scaleType (δ j) (τ j)) := by1250  have hdesc : ∀ j, HasAlgebraType m.O (B j) (scaleType (δ j) (τ j)) := fun j =>1251    algebra_type_unramified_descent m.O (mc j).O (δ j) (hrank j) m.pi m.hpi1252      (hpi j) (B j) (τ j) (hτ j)1253  have hprod := algebra_type_pi m.O n B _ hdesc1254  have hbij := baseChange_bijective_of_finite_cokernel m.O _ _1255    ψ.toLinearMap hψ ℓ hlen1256  let f := Algebra.TensorProduct.map (AlgHom.id (BaseField m.O) (BaseField m.O)) ψ1257  have hf : ⇑f = ⇑(LinearMap.baseChange (BaseField m.O) ψ.toLinearMap) := by1258    funext x1259    induction x using TensorProduct.induction_on with1260    | zero => simp1261    | tmul a b => simp [f, Algebra.TensorProduct.map_tmul]1262    | add x y hx hy => rw [map_add, map_add, hx, hy]1263  have hfb : Function.Bijective f := hf ▸ hbij1264  exact algebra_type_of_generic_fibre_equiv m.O _ _1265    (AlgEquiv.ofBijective f hfb) _ hprod1266 1267/-- A division chart is a measurable embedding for the intrinsic σ-algebra. -/1268theorem coordinate_ideal_measurableEmbedding (O : Type) [CommRing O] [IsDomain O]1269    [IsDiscreteValuationRing O] [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)]1270    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]1271    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] (htop : IsAdic (maximalIdeal O))1272    (R : Type) [CommRing R] [Algebra O R] [IsDomain R] [IsLocalRing R] (pi : O)1273    (hpi : Irreducible pi) (hp0 : algebraMap O R pi ≠ 0) (hpm : algebraMap O R pi ∈ maximalIdeal R)1274    (n : ℕ) (f : R) (b : Fin n → R) (hchart : IsDivisionChart O R pi f b)1275    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] :1276    @MeasurableEmbedding (Fin n → O) (Ideal R) inferInstance (idealChartSigma O R pi)1277      (coordinateIdeal pi f b) := by1278  obtain ⟨E, hE⟩ := hchart.11279  exact @MeasurableEmbedding.mk _ _ _ (idealChartSigma O R pi) _1280    (coordinate_ideal_injective O R n pi b E hp0 hpm f hE hchart.2)1281    (coordinate_ideal_measurable_chart_sigma O htop R pi hpi hp0 hpm n f b hchart)1282    (fun S hS => chart_image_measurable_chart_sigma O R pi n f b hchart S hS)1283 1284/-- Two curve-section representatives of the same class modulo the curve ideal lattice have the1285same connecting class. -/1286private theorem connecting_class_eq_of_mkQ_eq (R : Type) [CommRing R] (t x : R)1287    (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)1288    (hregSwap : RegularParameterPair R x t) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ)1289    (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap1290    (fullCechDifferential R t x beta d)) (hregF : Function.Injective1291    (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j => Ideal.Quotient.mk1292    ((Ideal.span {overlapException R t x})^j) ((algebraMap (BlowupChart R t x)1293    (BlowupOverlap R t x)) (G.left j)) * c))1294    (p p' : BlowupChart R t x × BlowupChart R x t) (c c' : BlowupOverlap R t x)1295    (hc : fullCechDifferential R t x beta 0 p - (algebraMap (BlowupChart R t x)1296      (BlowupOverlap R t x)) (G.left j) * c ∈ (Ideal.span {overlapException R t x})^j)1297    (hc' : fullCechDifferential R t x beta 0 p' - (algebraMap (BlowupChart R t x)1298      (BlowupOverlap R t x)) (G.left j) * c' ∈ (Ideal.span {overlapException R t x})^j)1299    (hpp : (curveIdealLattice R t x beta G j).mkQ p = (curveIdealLattice R t x beta G j).mkQ p') :1300    (LinearMap.range (finiteCechDifferential R t x beta d j h)).mkQ1301        ((cechOutputLattice R t x j).mkQ c) =1302      (LinearMap.range (finiteCechDifferential R t x beta d j h)).mkQ1303        ((cechOutputLattice R t x j).mkQ c') := by1304  have hmem : p - p' ∈ curveIdealLattice R t x beta G j := (Submodule.Quotient.eq _).1 hpp1305  have hs := curve_ideal_lattice_le_sections R t x beta d G j hmem1306  have hc2 : fullCechDifferential R t x beta 0 (p - p') - (algebraMap (BlowupChart R t x)1307      (BlowupOverlap R t x)) (G.left j) * (c - c') ∈ (Ideal.span {overlapException R t x})^j := by1308    convert Ideal.sub_mem _ hc hc' using 11309    simp only [map_sub, mul_sub]1310    abel1311  have := (curve_section_connecting_class_zero_iff R t x beta d G hreg hregSwap j h hregF1312    (p - p') hs (c - c') hc2).2 ⟨0, by simpa using hmem⟩1313  rwa [map_sub, map_sub, sub_eq_zero] at this1314 1315/-- Every curve section has a coefficient `c` with `D p - (left j) * c` in the `j`-th power of the1316exceptional ideal of the overlap. -/1317private theorem exists_connecting_coefficient (R : Type) [CommRing R] (t x : R)1318    (beta : BlowupRestriction R t x) {d : ℕ} (G : GluedGenerators R t x beta d) (j : ℕ)1319    (p : BlowupChart R t x × BlowupChart R x t) (hp : p ∈ curveSections R t x beta G j) :1320    ∃ c, fullCechDifferential R t x beta 0 p - (algebraMap (BlowupChart R t x)1321      (BlowupOverlap R t x)) (G.left j) * c ∈ (Ideal.span {overlapException R t x})^j := by1322  have hp' : fullCechDifferential R t x beta 0 p ∈ overlapCurveIdeal R t x beta G j := hp1323  obtain ⟨y, hy, z, hz, hyz⟩ := Submodule.mem_sup.1 hp'1324  obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.1 hy1325  exact ⟨c, by convert hz using 1; rw [← hyz, mul_comm]; abel⟩1326 1327/-- The connecting map from curve sections to the Čech cokernel, characterized on1328representatives. -/1329private theorem exists_connecting_linear_map (O R : Type) [CommRing O] [CommRing R] [Algebra O R]1330    (t x : R) (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)1331    (hregSwap : RegularParameterPair R x t) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ)1332    (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap1333    (fullCechDifferential R t x beta d)) (hregF : Function.Injective1334    (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j => Ideal.Quotient.mk1335    ((Ideal.span {overlapException R t x})^j) ((algebraMap (BlowupChart R t x)1336    (BlowupOverlap R t x)) (G.left j)) * c)) :1337    ∃ δ : curveSectionsQuot R t x beta G j →ₗ[O] (CechLevelOutput R t x j ⧸ LinearMap.range1338      (finiteCechDifferential R t x beta d j h)), ∀ (p : BlowupChart R t x × BlowupChart R x t)1339      (hp : p ∈ curveSections R t x beta G j) (c : BlowupOverlap R t x), fullCechDifferential R t x1340      beta 0 p - (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c ∈1341      (Ideal.span {overlapException R t x})^j → δ ⟨(curveIdealLattice R t x beta G j).mkQ p,1342      Submodule.mem_map_of_mem hp⟩ = (LinearMap.range (finiteCechDifferential R t x beta d j h)).mkQ1343      ((cechOutputLattice R t x j).mkQ c) := by1344  let L := curveIdealLattice R t x beta G j1345  let S := curveSections R t x beta G j1346  let I := (Ideal.span {overlapException R t x})^j1347  let Q := LinearMap.range (finiteCechDifferential R t x beta d j h)1348  let a := (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)1349  let D := fullCechDifferential R t x beta 01350  let cl : BlowupOverlap R t x → (CechLevelOutput R t x j ⧸ Q) :=1351    fun c => Q.mkQ ((cechOutputLattice R t x j).mkQ c)1352  have cl_add : ∀ c c', cl (c + c') = cl c + cl c' := fun c c' => by simp only [cl, map_add]1353  have cl_smul : ∀ (o : O) c, cl (o • c) = o • cl c := fun o c => by1354    simp only [cl, LinearMap.map_smul_of_tower]1355  have exist : ∀ p ∈ S, ∃ c, D p - a * c ∈ I := exists_connecting_coefficient R t x beta G j1356  have rep : ∀ u : curveSectionsQuot R t x beta G j, ∃ p ∈ S, L.mkQ p = u :=1357    fun u => Submodule.mem_map.1 u.21358  let f : curveSectionsQuot R t x beta G j → (CechLevelOutput R t x j ⧸ Q) := fun u =>1359    cl (Classical.choose (exist _ (Classical.choose_spec (rep u)).1))1360  have spec : ∀ (u : curveSectionsQuot R t x beta G j) p, p ∈ S → ∀ c, D p - a * c ∈ I → L.mkQ p =1361      (u : _) → f u = cl c := by1362    intro u p hp c hc hpu1363    have h1 := Classical.choose_spec (rep u)1364    have h2 := Classical.choose_spec (exist _ h1.1)1365    exact connecting_class_eq_of_mkQ_eq R t x hreg beta hregSwap d G j h hregF _ p _ c h2 hc1366      (h1.2.trans hpu.symm)1367  clear_value f1368  have hadd : ∀ u v, f (u + v) = f u + f v := by1369    intro u v1370    obtain ⟨p, hp, hpu⟩ := rep u1371    obtain ⟨q, hq, hqv⟩ := rep v1372    obtain ⟨c, hc⟩ := exist p hp1373    obtain ⟨c', hc'⟩ := exist q hq1374    rw [spec u p hp c hc hpu, spec v q hq c' hc' hqv, ← cl_add]1375    apply spec _ _ (S.add_mem hp hq)1376    · convert I.add_mem hc hc' using 1; simp [map_add, mul_add]; abel1377    · rw [map_add, hpu, hqv, Submodule.coe_add]1378  have hsmul : ∀ (o : O) u, f (o • u) = RingHom.id O o • f u := by1379    intro o u1380    obtain ⟨p, hp, hpu⟩ := rep u1381    obtain ⟨c, hc⟩ := exist p hp1382    rw [RingHom.id_apply, spec u p hp c hc hpu, ← cl_smul]1383    apply spec _ (o • p) (S.smul_of_tower_mem o hp)1384    · convert I.smul_of_tower_mem o hc using 11385      rw [LinearMap.map_smul_of_tower, smul_sub, mul_smul_comm]1386    · rw [Submodule.coe_smul_of_tower, ← hpu]1387      exact LinearMap.map_smul_of_tower L.mkQ o p1388  exact ⟨{ toFun := f, map_add' := hadd, map_smul' := hsmul },1389    fun p hp c hc => spec _ p hp c hc rfl⟩1390 1391/-- The connecting map from curve sections to the Čech cokernel exists, is surjective, and has1392kernel the image of the surface. -/1393theorem curve_sections_connecting_map_exists (O R : Type) [CommRing O] [CommRing R] [Algebra O R]1394    (t x : R) (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)1395    (hregSwap : RegularParameterPair R x t) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ)1396    (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap1397    (fullCechDifferential R t x beta d)) (hregF : Function.Injective1398    (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j => Ideal.Quotient.mk1399    ((Ideal.span {overlapException R t x})^j) ((algebraMap (BlowupChart R t x)1400    (BlowupOverlap R t x)) (G.left j)) * c)) :1401    ∃ δ : curveSectionsQuot R t x beta G j →ₗ[O] (CechLevelOutput R t x j ⧸ LinearMap.range1402      (finiteCechDifferential R t x beta d j h)), (∀ (p : BlowupChart R t x × BlowupChart R x t)1403      (hp : p ∈ curveSections R t x beta G j) (c : BlowupOverlap R t x), fullCechDifferential R t x1404      beta 0 p - (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c ∈1405      (Ideal.span {overlapException R t x})^j → δ ⟨(curveIdealLattice R t x beta G j).mkQ p,1406      Submodule.mem_map_of_mem hp⟩ = (LinearMap.range (finiteCechDifferential R t x beta d j h)).mkQ1407      ((cechOutputLattice R t x j).mkQ c)) ∧ Function.Surjective δ ∧ ∀ u : curveSectionsQuot R t x1408      beta G j, δ u = 0 ↔ ∃ r : R, (u : (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice1409      R t x beta G j) = (curveIdealLattice R t x beta G j).mkQ (surfaceToChartPair R t x r) := by1410  obtain ⟨δ, hδ⟩ := exists_connecting_linear_map O R t x hreg beta hregSwap d G j h hregF1411  refine ⟨δ, hδ, fun y => ?_, fun u => ?_⟩1412  · obtain ⟨y', rfl⟩ := Submodule.mkQ_surjective _ y1413    obtain ⟨c, rfl⟩ := Submodule.mkQ_surjective _ y'1414    obtain ⟨p, hp, hc⟩ := curve_sections_cover_overlap R t x beta d G hreg j c1415    exact ⟨_, hδ p hp c hc⟩1416  · obtain ⟨u, hu⟩ := u1417    obtain ⟨p, hp, rfl⟩ := Submodule.mem_map.1 hu1418    obtain ⟨c, hc⟩ := exists_connecting_coefficient R t x beta G j p hp1419    have hδu : δ ⟨(curveIdealLattice R t x beta G j).mkQ p, hu⟩ = _ := hδ p hp c hc1420    rw [hδu]1421    refine (curve_section_connecting_class_zero_iff R t x beta d G hreg hregSwap j h hregF1422      p hp c hc).trans (exists_congr fun r => ?_)1423    exact (Submodule.Quotient.eq _).symm1424 1425end SurfaceBlowup1426 1427end