Lean sources / SurfaceBlowup / Recursion / ChildMembers.lean
Child members and terminal states of the blowup recursion
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.Measure.Haar7 8/-!9# Child members and terminal states of the blowup recursion10 11This file constructs the concrete child members attached to closed points of the exceptional12divisor of a blowup (via the `t`-chart and the point at infinity), assembles them into cell13child data, and shows that the tangent divisor of an ideal is unique, so tangent cells are14disjoint. It then treats terminal states `single a 1`: the curve order is a DVR whose generic15fibre is a field with field invariant `(a, 1)`. Finally it develops the terminating sets of a16surface universe: their cell decomposition, uniqueness of the factorization type, the law in17the terminal case, and the return-chain decomposition for single states.18 19## Main results20 21* `t_chart_point_child_member`, `direction_child_member_exists`, `cell_child_data_exists`.22* `tangent_divisor_unique`, `concrete_member_cells_disjoint`.23* `terminal_curve_order_dvr`, `terminal_field_invariant`, `concrete_member_terminal_type`.24* `terminates_cell_decomposition`, `terminates_type_unique`, `recursion_terminal_law`,25 `term_type_event_cell_decomposition`, `single_state_return_chain`, `universe_basic_facts`.26 27Provenance: `Thm_SurfaceBlowupV2_` nodes `t_chart_point_child_member`,28`direction_child_member_exists`, `cell_child_data_exists`, `tangent_divisor_unique`,29`concrete_member_cells_disjoint`, `terminal_curve_order_{local_principal,dvr}`,30`terminal_generic_fibre_field`, `terminal_field_invariant`, `concrete_member_terminal_type`,31`terminates_{cell_decomposition,type_unique}`, `recursion_terminal_step`,32`term_type_event_cell_decomposition`, `single_state_return_chain`, `universe_basic_facts`.33-/34 35open scoped BigOperators ENNReal TensorProduct36 37namespace SurfaceBlowup38 39/-! ### Child members at points of the exceptional divisor -/40 41/-- If `P = (T, Z - α)` is a maximal ideal with `α` zero or a unit, then `Z ∈ P` exactly when42`α = 0`. -/43private theorem mem_span_sub_iff_eq_zero {O A : Type} [CommRing O] [CommRing A] (f : O →+* A)44 (P : Ideal A) [P.IsMaximal] (T Z : A) (α : O) (hα : α = 0 ∨ IsUnit α)45 (hP : P = Ideal.span {T, Z - f α}) : Z ∈ P ↔ α = 0 := by46 refine ⟨fun hZP ↦ hα.resolve_right fun hunit ↦ ?_, fun h0 ↦ ?_⟩47 · have hsub : Z - f α ∈ P := by rw [hP]; exact Ideal.subset_span (by simp)48 exact Ideal.IsMaximal.ne_top ‹_› (Ideal.eq_top_of_isUnit_mem P49 (by simpa using P.sub_mem hZP hsub) (hunit.map _))50 · rw [hP, h0]51 exact Ideal.subset_span (by simp)52 53/-- If `Φ` is an unramified lift of degree `≥ 2` and `Φ(Z)` lies in a maximal ideal `P`, then54`Z ∉ P`: the constant coefficient of `Φ` is a unit. -/55private theorem not_mem_of_eval₂_mem {O A : Type} [CommRing O] [IsLocalRing O] [CommRing A]56 (f : O →+* A) (P : Ideal A) [P.IsMaximal] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)57 (h2 : 2 ≤ Φ.natDegree) (Z : A) (hmem : Φ.eval₂ f Z ∈ P) : Z ∉ P := by58 intro hZP59 have hc0 : IsUnit (Φ.coeff 0) := by60 rw [← IsLocalRing.residue_ne_zero_iff_isUnit]61 intro h062 have hX : Polynomial.X ∣ residuePoly O Φ := by63 rw [Polynomial.X_dvd_iff, residuePoly, Polynomial.coeff_map]; exact h064 have hd := Polynomial.natDegree_eq_of_degree_eq65 (Polynomial.degree_eq_degree_of_associated66 (Polynomial.irreducible_X.associated_of_dvd hΦ.2 hX))67 rw [Polynomial.natDegree_X, residuePoly, hΦ.1.natDegree_map] at hd68 omega69 obtain ⟨q, hq⟩ := Polynomial.X_dvd_sub_C (p := Φ)70 rw [show Φ = Polynomial.C (Φ.coeff 0) + Polynomial.X * q by rw [← hq]; ring,71 Polynomial.eval₂_add, Polynomial.eval₂_mul, Polynomial.eval₂_C, Polynomial.eval₂_X,72 Ideal.add_mem_iff_left _ (P.mul_mem_right _ hZP)] at hmem73 exact Ideal.IsMaximal.ne_top ‹_› (Ideal.eq_top_of_isUnit_mem P hmem (hc0.map _))74 75open scoped Classical in76/-- A closed point of degree `δ` on the exceptional line of the `t`-chart carries a concrete child77member: a concrete surface over a finite free `O`-algebra of rank `δ` (residue field of size78`q^δ`) in any prescribed compatible state, with measure-compatible coordinates and an79identification of its ring with the completed local ring at the point. -/80theorem t_chart_point_child_member (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]81 [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]82 [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]83 [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]84 (htop : IsAdic (IsLocalRing.maximalIdeal O)) (pi : O) (hpi : Irreducible pi)85 (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)86 (P : Ideal (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)87 (surfaceX O pi u a b)))88 [P.IsMaximal] [P.IsPrime]89 (hP : (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))90 (surfaceT O pi u a b) ∈ P)91 (δ : ℕ) (hδ : 0 < δ)92 (hdeg : Module.length (ConcreteSurface O pi u a b) ((BlowupChart (ConcreteSurface O pi u a b)93 (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸ P) = (δ : ℕ∞))94 (s' : State)95 (hs' : StateShape (a + b) (if (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)96 (surfaceX O pi u a b)) ∈ P then b else 0) s') :97 ∃ mc : ConcreteMember,98 ∃ (_ : Algebra O mc.O) (_ : Module.Finite O mc.O) (_ : Module.Free O mc.O),99 Module.finrank O mc.O = δ ∧100 Nat.card (IsLocalRing.ResidueField mc.O) = Nat.card (IsLocalRing.ResidueField O) ^ δ ∧101 mc.pi = algebraMap O mc.O pi ∧ mc.a = a + b ∧102 mc.b = (if (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)103 (surfaceX O pi u a b)) ∈ P then b else 0) ∧104 mc.s = s' ∧105 (∃ pc : mc.O ≃ₗ[O] (Fin δ → O), Continuous pc ∧ Continuous pc.symm ∧ Measurable pc ∧106 Measurable pc.symm ∧107 MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map pc.symm108 (coefficientMeasure O δ))109 ∧ ∀ r : ℕ, coefficientMeasure mc.O r = MeasureTheory.Measure.pi110 (fun _ : Fin r => MeasureTheory.Measure.map pc.symm (coefficientMeasure O δ))) ∧111 ∃ Eq : CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)112 (surfaceX O pi u a b)) P ≃+* mc.R,113 Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)114 (surfaceX O pi u a b)) P) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)115 (surfaceX O pi u a b)) (surfaceT O pi u a b))) = mc.S.t ∧116 ((chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ∈ P →117 Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)118 (surfaceX O pi u a b)) P) (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)119 (surfaceX O pi u a b))) = mc.S.x) ∧120 ∀ c : O,121 Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)122 (surfaceX O pi u a b)) P) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)123 (surfaceX O pi u a b)) (algebraMap O (ConcreteSurface O pi u a b) c))) =124 algebraMap O mc.R c := by125 rcases Nat.lt_or_ge δ 2 with hlt | h2126 · obtain rfl : δ = 1 := by omega127 obtain ⟨α, hα, hPspan, u', Eq, h1, h2, h3⟩ :=128 t_chart_rational_point_child_data O pi hpi u a b ha P hP (by exact_mod_cast hdeg)129 have hZiff : chartSlope _ (surfaceT O pi u a b) (surfaceX O pi u a b) ∈ P ↔ α = 0 :=130 mem_span_sub_iff_eq_zero ((chartBase _ (surfaceT O pi u a b) (surfaceX O pi u a b)).comp131 (algebraMap O _)) P _ _ α hα hPspan132 simp only [hZiff] at hs' ⊢133 obtain ⟨i1, i2, S, hSpi, hSt, hSx, hSa, hSb, ⟨atlas⟩⟩ :=134 concrete_member_data_exists O pi hpi u' (a + b) (if α = 0 then b else 0) (by omega) s' hs'135 have := coefficient_measure_probability O htop 1136 obtain ⟨-, hm2, hm3, hm4, hm5, hm6⟩ := coefficient_measure_pi_one O htop pi hpi 0137 refine ⟨⟨O, htop, pi, hpi, u', a + b, if α = 0 then b else 0, by omega, S, hSpi, hSt, hSx,138 hSa, hSb, s', hs', atlas⟩, Algebra.id O, Module.Finite.self O, Module.Free.self O,139 Module.finrank_self O, by simp, by simp, rfl, rfl, rfl,140 ⟨(LinearEquiv.funUnique (Fin 1) O O).symm, hm4, hm3, hm6, hm5, by simpa using hm2,141 fun r ↦ by simpa using (coefficient_measure_pi_one O htop pi hpi r).1⟩,142 Eq, by simpa [hSt] using h1, fun hZP ↦ ?_, fun c ↦ by simpa using h3 c⟩143 simpa [hSx, hZP] using h2144 · obtain ⟨Φ, hΦ, rfl, hPspan, hθ, Eq, h1, h3⟩ :=145 t_chart_nonrational_point_child_data O pi hpi u a b ha P hP δ hdeg h2146 have hZ : chartSlope _ (surfaceT O pi u a b) (surfaceX O pi u a b) ∉ P :=147 not_mem_of_eval₂_mem ((chartBase _ (surfaceT O pi u a b) (surfaceX O pi u a b)).comp148 (algebraMap O _)) P Φ hΦ h2 _ (by rw [hPspan]; exact Ideal.subset_span (by simp))149 simp only [hZ, if_false] at hs' ⊢150 let τ : TopologicalSpace (AdjoinRoot Φ) := unramifiedTopology O Φ hΦ.1151 let μ : MeasurableSpace (AdjoinRoot Φ) := unramifiedMeasurableSpace O Φ hΦ.1152 obtain ⟨i1, i2, hchar, hdvr, hcomp, hfin, hcard, htr, hcpt, ht2, hsc, hbor, htop'⟩ :=153 unramified_extension_measure_package O htop Φ hΦ rfl rfl154 have hpi' : Irreducible (algebraMap O (AdjoinRoot Φ) pi) :=155 (unramified_is_dvr O Φ hΦ).2.2.2.2.1 pi hpi156 obtain ⟨hfree, hfinite, hrank⟩ := unramified_free_module O Φ hΦ.1157 obtain ⟨-, -, -, -, -, hc1, hc2, hc3, hc4⟩ := power_coordinates_transport O Φ hΦ.1 rfl rfl158 obtain ⟨-, hprob, -⟩ := unramified_coefficient_measure_haar O Φ hΦ.1 rfl rfl htop159 obtain ⟨j1, j2, S, hSpi, hSt, hSx, hSa, hSb, ⟨atlas⟩⟩ :=160 concrete_member_data_exists (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) hpi'161 (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)162 (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) *163 shiftUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0 (by omega) s' hs'164 refine ⟨⟨AdjoinRoot Φ, htop', _, hpi', _, a + b, 0, by omega, S, hSpi, hSt, hSx, hSa, hSb, s',165 hs', atlas⟩, inferInstance, hfinite, hfree, hrank, hcard, rfl, rfl, rfl, rfl,166 ⟨powerCoordinates O Φ hΦ.1, hc1, hc2, hc3, hc4, hprob, fun r ↦167 (unramified_coefficient_measure_pi O htop Φ hΦ rfl rfl r).1⟩, Eq,168 by simpa [hSt] using h1, fun hZP ↦ hZP.elim, fun c ↦ ?_⟩169 rw [h3 c]170 exact (IsScalarTower.algebraMap_apply O (AdjoinRoot Φ) _ c).symm171 172/-- The child state at the point at infinity has the shape of the infinity chart. -/173private theorem infinity_child_state_shape (m : ConcreteMember)174 (Dv : ExceptionalDivisor (IsLocalRing.ResidueField m.R)) (d : ℕ) (hQ : 0 < Dv none)175 (hb : d < stateContactT m.s) :176 StateShape (m.a + m.b) m.a (pointChildState (IsLocalRing.ResidueField m.R) m.s d Dv none) := by177 have hsh := m.shape178 generalize m.s = s at hsh hb ⊢179 cases s with180 | single a c =>181 obtain ⟨h1, h2, h3⟩ := hsh182 simp only [pointChildState, infinityDirection, if_true, StateShape, stateContactT] at hb ⊢183 subst h1184 exact ⟨by omega, rfl, m.ha, hQ, by omega⟩185 | crossing a b c h =>186 obtain ⟨h1, h2, h3, h4, h5⟩ := hsh187 simp only [pointChildState, infinityDirection, if_true, StateShape, stateContactT] at hb ⊢188 subst h1 h2189 exact ⟨rfl, rfl, m.ha, hQ, by omega⟩190 191/-- `direction_child_member_exists` with the chart coordinates `t`, `x` given up to equality. -/192private theorem direction_child_member_of_eq (m : ConcreteMember) (t x : m.R)193 (ht : t = surfaceT m.O m.pi m.u m.a m.b) (hx : x = surfaceX m.O m.pi m.u m.a m.b)194 (e : (BlowupChart m.R t x ⧸ chartExceptional m.R t x) ≃+* Polynomial195 (IsLocalRing.ResidueField m.R))196 (hdp : ∀ φ : AffineDirection (IsLocalRing.ResidueField m.R),197 (directionPoint m.R t x e φ).IsMaximal ∧ chartBase m.R t x t ∈ directionPoint m.R t x e φ ∧198 (chartSlope m.R t x ∈ directionPoint m.R t x e φ ↔ φ = zeroAffine199 (IsLocalRing.ResidueField m.R)) ∧200 Module.length m.R (BlowupChart m.R t x ⧸ directionPoint m.R t x e φ) = (φ.val.natDegree : ℕ∞))201 (hinf : (infinityPoint m.R t x).IsPrime)202 (Dv : ExceptionalDivisor (IsLocalRing.ResidueField m.R)) (d : ℕ) (Q : divisorSupport Dv)203 (hb : Q.val = infinityDirection (IsLocalRing.ResidueField m.R) → d < stateContactT m.s)204 (hz : Q.val = zeroDirection (IsLocalRing.ResidueField m.R) →205 ∀ h : ℕ, stateContactX m.s = some h → d < h) :206 ∃ cm : ChildMember m (directionDegree (IsLocalRing.ResidueField m.R) Q.val)207 (pointChildState (IsLocalRing.ResidueField m.R) m.s d Dv Q.val),208 ∃ Eq : divisorLocalRing m.R t x e Dv hinf Q ≃+* cm.mc.R,209 Eq (divisorException m.R t x e Dv hinf Q) = cm.mc.S.t ∧210 ((Q.val = infinityDirection (IsLocalRing.ResidueField m.R) ∨ Q.val = zeroDirection211 (IsLocalRing.ResidueField m.R)) → Eq (divisorBoundary m.R t x e Dv hinf Q) = cm.mc.S.x) ∧212 ∀ r : m.O,213 Eq (divisorFromSurface m.R t x e Dv hinf Q (algebraMap m.O m.R r)) = algebraMap cm.mc.O cm.mc.R214 (algebraMap m.O cm.mc.O r) := by215 classical216 subst ht hx217 obtain ⟨Q, hQ⟩ := Q218 cases Q with219 | none =>220 have key := infinity_child_state_shape m Dv d hQ (hb rfl)221 obtain ⟨mc, alg, fin, free, hrank, hcard, hpi, -, -, hs, ⟨pc, c1, c2, c3, c4, -, hmeas⟩,222 Eq, h1, h2, h3⟩ := infinity_point_child_member m.O m.htop m.pi m.hpi m.u m.a m.b m.ha223 (hinf := hinf) _ key224 refine ⟨@ChildMember.mk m _ _ mc alg fin free hrank hcard hpi hs pc ⟨c1, c2, c3, c4⟩ hmeas,225 Eq, h1, fun _ => h2, fun r => ?_⟩226 exact (h3 r).trans (IsScalarTower.algebraMap_apply m.O mc.O mc.R r)227 | some φ =>228 obtain ⟨hmax, htP, hZ, hlen⟩ := hdp φ229 have hδ : 0 < φ.val.natDegree := Irreducible.natDegree_pos φ.property.2230 have key : StateShape (m.a + m.b)231 (if chartSlope m.R (surfaceT m.O m.pi m.u m.a m.b) (surfaceX m.O m.pi m.u m.a m.b) ∈232 directionPoint m.R (surfaceT m.O m.pi m.u m.a m.b) (surfaceX m.O m.pi m.u m.a m.b) e φ233 then m.b else 0)234 (pointChildState (IsLocalRing.ResidueField m.R) m.s d Dv (some φ)) := by235 have hsh := m.shape236 have hz' := hz237 simp only at hz'238 have hinfne : (some φ : ClosedDirection (IsLocalRing.ResidueField m.R)) ≠239 infinityDirection (IsLocalRing.ResidueField m.R) := by simp [infinityDirection]240 have hzero : (some φ : ClosedDirection (IsLocalRing.ResidueField m.R)) =241 zeroDirection (IsLocalRing.ResidueField m.R) ↔ φ = zeroAffine242 (IsLocalRing.ResidueField m.R) := by243 simp [zeroDirection, zeroAffine]244 rw [← hzero] at hZ245 simp only [hZ]246 generalize m.s = s at hsh hz' ⊢247 cases s with248 | single a c =>249 obtain ⟨h1, h2, h3⟩ := hsh250 subst h1251 simp only [pointChildState, hinfne, if_false, StateShape, h2]252 split_ifs <;> exact ⟨by omega, rfl, hQ⟩253 | crossing a b c h =>254 obtain ⟨h1, h2, h3, h4, h5⟩ := hsh255 subst h1 h2256 simp only [pointChildState, hinfne, if_false]257 by_cases hq : (some φ : ClosedDirection (IsLocalRing.ResidueField m.R)) =258 zeroDirection (IsLocalRing.ResidueField m.R)259 · have := hz' hq h rfl260 simp only [hq, if_true, StateShape]261 rw [← hq]262 refine ⟨?_, ?_, h3, hQ, by omega⟩ <;> simp263 · simp only [hq, if_false, StateShape]264 refine ⟨?_, ?_, hQ⟩ <;> simp265 obtain ⟨mc, alg, fin, free, hrank, hcard, hpi, -, -, hs, ⟨pc, c1, c2, c3, c4, -, hmeas⟩,266 Eq, h1, h2, h3⟩ := t_chart_point_child_member m.O m.htop m.pi m.hpi m.u m.a m.b m.ha267 _ htP _ hδ hlen _ key268 refine ⟨@ChildMember.mk m _ _ mc alg fin free hrank hcard hpi hs pc ⟨c1, c2, c3, c4⟩ hmeas,269 Eq, h1, fun hq => h2 ?_, fun r => ?_⟩270 · rw [hZ]271 rcases hq with hq | hq272 · simp [infinityDirection] at hq273 · simpa [zeroDirection, zeroAffine] using hq274 · exact (h3 r).trans (IsScalarTower.algebraMap_apply m.O mc.O mc.R r)275 276/-- Every support point `Q` of an exceptional divisor (with the boundary contact conditions)277carries a child member of degree `deg Q` in the state `pointChildState`, whose ring is278identified with the local ring at `Q` compatibly with the exceptional and boundary parameters. -/279theorem direction_child_member_exists (m : ConcreteMember)280 (e : (BlowupChart m.R m.S.t m.S.x ⧸ chartExceptional m.R m.S.t m.S.x) ≃+* Polynomial281 (IsLocalRing.ResidueField m.R))282 (he : ∀ r : m.R, e (Ideal.Quotient.mk (chartExceptional m.R m.S.t m.S.x)283 (chartBase m.R m.S.t m.S.x r)) = Polynomial.C (IsLocalRing.residue m.R r))284 (heZ : e (Ideal.Quotient.mk (chartExceptional m.R m.S.t m.S.x) (chartSlope m.R m.S.t m.S.x)) =285 Polynomial.X)286 (hinf : (infinityPoint m.R m.S.t m.S.x).IsPrime)287 (Dv : ExceptionalDivisor (IsLocalRing.ResidueField m.R)) (d : ℕ) (Q : divisorSupport Dv)288 (hb : Q.val = infinityDirection (IsLocalRing.ResidueField m.R) → d < stateContactT m.s)289 (hz : Q.val = zeroDirection (IsLocalRing.ResidueField m.R) →290 ∀ h : ℕ, stateContactX m.s = some h → d < h) :291 ∃ cm : ChildMember m (directionDegree (IsLocalRing.ResidueField m.R) Q.val)292 (pointChildState (IsLocalRing.ResidueField m.R) m.s d Dv Q.val),293 ∃ Eq : divisorLocalRing m.R m.S.t m.S.x e Dv hinf Q ≃+* cm.mc.R,294 Eq (divisorException m.R m.S.t m.S.x e Dv hinf Q) = cm.mc.S.t ∧295 ((Q.val = infinityDirection (IsLocalRing.ResidueField m.R) ∨ Q.val = zeroDirection296 (IsLocalRing.ResidueField m.R)) → Eq (divisorBoundary m.R m.S.t m.S.x e Dv hinf Q) =297 cm.mc.S.x) ∧298 ∀ r : m.O,299 Eq (divisorFromSurface m.R m.S.t m.S.x e Dv hinf Q (algebraMap m.O m.R r)) = algebraMap cm.mc.O300 cm.mc.R (algebraMap m.O cm.mc.O r) := by301 refine direction_child_member_of_eq m m.S.t m.S.x m.hS_t m.hS_x e (fun φ => ?_) hinf Dv d Q hb hz302 obtain ⟨h1, h2, h3, -, h5, -⟩ :=303 direction_point_maximal m.O m.R m.S e he heZ φ304 exact ⟨h1, h2, h3, h5⟩305 306private theorem pattern_d_lt_contactT (s : State) (P : TangentPattern s.degree) (hP : Allowed s P)307 (hrt : 0 < P.rt.val) : P.d.val < stateContactT s := by308 cases s <;> simp only [Allowed, stateContactT] at * <;> tauto309 310private theorem pattern_d_lt_contactX (k : Type) [Field k] (s : State) (P : TangentPattern s.degree)311 (hP : Allowed s P)312 (Dv : ExceptionalDivisor k) (hDv : HasPattern k s Dv P) (hpos : 0 < Dv (zeroDirection k))313 (h : ℕ) (hh : stateContactX s = some h) : P.d.val < h := by314 cases s with315 | single a c => simp [stateContactX] at hh316 | crossing a b c h' =>317 simp only [stateContactX, Option.some.injEq] at hh318 subst hh319 simp only [Allowed, HasPattern] at hP hDv320 rw [hDv.2.2.1] at hpos321 exact hP.2.2.2.2.2.1 hpos322 323/-- Every tangent cell of a concrete member admits cell child data: an assignment of children to324divisor points together with the corresponding child members and identifications. -/325theorem cell_child_data_exists (m : ConcreteMember) (c : m.cellIndex) :326 Nonempty (CellChildData m c) := by327 obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_residue_field m.O m.R m.S328 have hinf : (infinityPoint m.R m.S.t m.S.x).IsPrime :=329 (infinity_point_maximal m.O m.R m.S).1.isPrime330 have : Finite (IsLocalRing.ResidueField m.R) := Finite.of_equiv _ m.S.residueEquiv.toEquiv331 let asg : CellAssignment (IsLocalRing.ResidueField m.R) m.s c.1.1 c.2.1 :=332 Classical.choice (cell_assignment_exists _ m.s (m.shape.valid m.ha) c.1.1 c.1.2 c.2.1 c.2.2)333 have key : ∀ j : m.toMeasured.childIdx c,334 ∃ cm : ChildMember m (m.toMeasured.childDelta c j) (m.toMeasured.childState c j),335 ∃ Eq : divisorLocalRing m.R m.S.t m.S.x e c.2.1 hinf (asg.point j) ≃+* cm.mc.R,336 Eq (divisorException m.R m.S.t m.S.x e c.2.1 hinf (asg.point j)) = cm.mc.S.t ∧337 ((asg.pt j = infinityDirection (IsLocalRing.ResidueField m.R) ∨338 asg.pt j = zeroDirection (IsLocalRing.ResidueField m.R)) →339 Eq (divisorBoundary m.R m.S.t m.S.x e c.2.1 hinf (asg.point j)) = cm.mc.S.x) ∧340 ∀ r : m.O, Eq (divisorFromSurface m.R m.S.t m.S.x e c.2.1 hinf (asg.point j)341 (algebraMap m.O m.R r)) = algebraMap cm.mc.O cm.mc.R (algebraMap m.O cm.mc.O r) := by342 intro j343 have hP := c.1.2344 have hDv := c.2.2345 have hpos : 0 < c.2.1 (asg.pt j) := (asg.supp _).mpr ⟨j, rfl⟩346 have hb : (asg.point j).val = infinityDirection (IsLocalRing.ResidueField m.R) →347 c.1.1.d.val < stateContactT m.s := by348 intro hQ349 have hQ' : asg.pt j = infinityDirection _ := hQ350 rw [hQ'] at hpos351 exact pattern_d_lt_contactT m.s c.1.1 hP (hDv.2.1 ▸ hpos)352 have hz : (asg.point j).val = zeroDirection (IsLocalRing.ResidueField m.R) →353 ∀ h : ℕ, stateContactX m.s = some h → c.1.1.d.val < h := by354 intro hQ h hh355 have hQ' : asg.pt j = zeroDirection _ := hQ356 rw [hQ'] at hpos357 exact pattern_d_lt_contactX _ m.s c.1.1 hP c.2.1 hDv hpos h hh358 have := direction_child_member_exists m e he heZ hinf c.2.1 c.1.1.d.val (asg.point j) hb hz359 have h1 : m.toMeasured.childDelta c j = directionDegree _ (asg.point j).val := (asg.deg j).symm360 have h2 : m.toMeasured.childState c j = pointChildState _ m.s c.1.1.d.val c.2.1361 (asg.point j).val :=362 asg.state j363 rwa [h1, h2]364 choose child Eq hEq_e hEq_b hEq_c using key365 exact ⟨⟨e, he, heZ, hinf, asg, child, Eq, hEq_e, hEq_b, hEq_c⟩⟩366 367/-! ### Uniqueness of the tangent divisor -/368 369/-- The tangent order `d` and the tangent divisor `Dv` of an ideal on a regular surface are370uniquely determined. -/371theorem tangent_divisor_unique (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Proposition 6.1372 [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R] (S : SurfaceData O R)373 (hreg : RegularParameterPair R S.t S.x) (J : Ideal R) (d d' : ℕ)374 (Dv Dv' : ExceptionalDivisor (IsLocalRing.ResidueField R)) (h : HasTangentDivisor O R S J d Dv)375 (h' : HasTangentDivisor O R S J d' Dv') :376 d = d' ∧ Dv = Dv' := by377 set m := IsLocalRing.maximalIdeal R with hm378 have hM := has_tangent_divisor_multiplicity O R S hreg J d Dv h379 have hM' := has_tangent_divisor_multiplicity O R S hreg J d' Dv' h'380 have hdd : d = d' := by381 rcases lt_trichotomy d d' with hlt | heq | hgt382 · exact absurd (hM'.1.trans (Ideal.pow_le_pow_right hlt)) hM.2383 · exact heq384 · exact absurd (hM.1.trans (Ideal.pow_le_pow_right hgt)) hM'.2385 subst hdd386 refine ⟨rfl, ?_⟩387 obtain ⟨f, H, hJ, ⟨hH0, hHd, hHnone, hHfac⟩, hf⟩ := h388 obtain ⟨f', H', hJ', ⟨hH0', hHd', hHnone', hHfac'⟩, hf'⟩ := h'389 have hass : Associated f f' := by390 rw [← Ideal.span_singleton_eq_span_singleton, ← hJ, ← hJ']391 obtain ⟨u, hu⟩ := hass392 have hfm : f ∈ m ^ d := hM.1 (hJ ▸ Ideal.subset_span rfl)393 have hsurj : Function.Surjective (IsLocalRing.residue R) := Ideal.Quotient.mk_surjective394 have hrr : ∀ c, IsLocalRing.residue R (residueRepresentative R c) = c := fun c =>395 Function.invFun_eq (hsurj c)396 set ub := IsLocalRing.residue R (u : R) with hub397 set w := residueRepresentative R ub with hw398 have huw : (u : R) - w ∈ m := by399 rw [hm, ← IsLocalRing.ker_residue, RingHom.mem_ker, map_sub, hw, hrr, sub_self]400 have hdiff : tangentLift O R S d H' - w * tangentLift O R S d H ∈ m ^ (d+1) := by401 have e : tangentLift O R S d H' - w * tangentLift O R S d H =402 -(f' - tangentLift O R S d H') + f * ((u : R) - w) + w * (f - tangentLift O R S d H) := by403 rw [← hu]; ring404 rw [e]405 refine Ideal.add_mem _ (Ideal.add_mem _ (neg_mem hf') ?_) (Ideal.mul_mem_left _ _ hf)406 rw [pow_succ]407 exact Ideal.mul_mem_mul hfm huw408 have : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by409 rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R410 have hcoef : ∀ i : Fin (d+1),411 residueRepresentative R (H'.coeff i.val) - w * residueRepresentative R (H.coeff i.val) ∈412 m := by413 by_contra! hcon414 obtain ⟨i₀, hi₀⟩ := hcon415 rw [hm, ← S.parameters] at hi₀416 refine homogeneous_form_not_mem_pow_succ R S.t S.x hreg d (fun i ↦ residueRepresentative R417 (H'.coeff i.val) - w * residueRepresentative R (H.coeff i.val)) i₀ hi₀ ?_418 rw [S.parameters]419 convert hdiff using 1420 unfold tangentLift421 rw [Finset.mul_sum, ← Finset.sum_sub_distrib]422 exact Finset.sum_congr rfl fun i _ ↦ by ring423 have hub0 : ub ≠ 0 := by424 rw [hub]; exact (u.isUnit.map (IsLocalRing.residue R)).ne_zero425 have hHH : H' = Polynomial.C ub * H := by426 ext n427 rw [Polynomial.coeff_C_mul]428 by_cases hn : n ≤ d429 · have := hcoef ⟨n, Nat.lt_succ_of_le hn⟩430 rwa [hm, ← IsLocalRing.ker_residue, RingHom.mem_ker, map_sub, map_mul, hrr, hrr, hrr,431 sub_eq_zero] at this432 · push Not at hn433 rw [Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt hHd hn),434 Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt hHd' hn), mul_zero]435 have hdeg : H'.natDegree = H.natDegree := by436 rw [hHH, Polynomial.natDegree_C_mul hub0]437 obtain ⟨hA, hcnt⟩ := divisor_affine_polynomial_normalized_factors _ Dv438 obtain ⟨hA', hcnt'⟩ := divisor_affine_polynomial_normalized_factors _ Dv'439 have hAA : divisorAffinePolynomial _ Dv' = divisorAffinePolynomial _ Dv := by440 have e : Polynomial.C H'.leadingCoeff * divisorAffinePolynomial _ Dv' =441 Polynomial.C (ub * H.leadingCoeff) * divisorAffinePolynomial _ Dv := by442 rw [← hHfac', hHH, map_mul, mul_assoc, ← hHfac]443 have hl := congrArg Polynomial.leadingCoeff e444 rw [Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_C,445 Polynomial.leadingCoeff_C, hA.leadingCoeff, hA'.leadingCoeff, mul_one, mul_one] at hl446 rw [hl] at e447 refine mul_left_cancel₀ ?_ e448 rw [Ne, Polynomial.C_eq_zero, ← hl]449 exact Polynomial.leadingCoeff_ne_zero.mpr hH0'450 ext P451 cases P with452 | none => rw [hHnone, hHnone', hdeg]453 | some φ => rw [← hcnt, ← hcnt', hAA]454 455/-- The tangent cells of a concrete member are pairwise disjoint. -/456theorem concrete_member_cells_disjoint (m : ConcreteMember) :457 Pairwise fun c c' : m.toMeasured.cellIndex => Disjoint (m.toMeasured.cell c)458 (m.toMeasured.cell c') := by459 intro c c' hne460 rw [Set.disjoint_left]461 intro J h1 h2462 have hreg : RegularParameterPair m.R m.S.t m.S.x := by463 rw [m.hS_t, m.hS_x]464 exact concrete_surface_regular_pair_tx m.O m.pi m.hpi.ne_zero m.u m.a m.b m.ha465 obtain ⟨hd, hD⟩ := tangent_divisor_unique m.O m.R m.S hreg J _ _ _ _ h1.2 h2.2466 have hP : c.1.1 = c'.1.1 := by467 refine allowed_pattern_of_divisor_unique _ m.s c.2.1 c.1.1 c'.1.1 c.1.2 c'.1.2 c.2.2 ?_468 rw [hD]; exact c'.2.2469 apply hne470 obtain ⟨⟨P, hPa⟩, ⟨D, hDp⟩⟩ := c471 obtain ⟨⟨P', hPa'⟩, ⟨D', hDp'⟩⟩ := c'472 simp only at hP hD473 subst hP474 subst hD475 rfl476 477/-! ### Terminal states -/478 479/-- For `J = (f)` in the terminal state `single a 1`: `(f, t)` is the maximal ideal, and `R/J` is a480Noetherian local ring with principal maximal ideal `(t)`, finite free of rank `a` over `O`. -/481private theorem terminal_curve_order_local_principal (O : Type) [CommRing O] [IsDomain O]482 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]483 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)484 (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]485 [IsRegularLocalRing (ConcreteSurface O pi u a b)]486 (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSpi : S.pi = pi)487 (hSt : S.t = (surfaceT O pi u a b)) (hSx : S.x = (surfaceX O pi u a b)) (hSa : S.a = a)488 (hSb : S.b = b) (J : Ideal (ConcreteSurface O pi u a b))489 (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S (State.single a 1))490 (f : (ConcreteSurface O pi u a b)) (hf : J = Ideal.span {f}) :491 Ideal.span {f} ⊔ Ideal.span {(surfaceT O pi u a b)} = IsLocalRing.maximalIdeal492 (ConcreteSurface O pi u a b) ∧493 (∃ _ : IsLocalRing ((ConcreteSurface O pi u a b) ⧸ J), IsLocalRing.maximalIdeal494 ((ConcreteSurface O pi u a b) ⧸ J) = Ideal.span {(Ideal.Quotient.mk J495 (surfaceT O pi u a b))}) ∧496 IsNoetherianRing ((ConcreteSurface O pi u a b) ⧸ J) ∧497 Module.Free O ((ConcreteSurface O pi u a b) ⧸ J) ∧498 Module.Finite O ((ConcreteSurface O pi u a b) ⧸ J) ∧499 Module.finrank O ((ConcreteSurface O pi u a b) ⧸ J) = a := by500 have hJne := surface_state_ideal_proper O _ S _ J hJ501 obtain ⟨-, -, -, hb0, hc⟩ := hJ502 have hb : b = 0 := hSb ▸ hb0503 subst hb504 unfold idealContact at hc505 rw [hSt, hf] at hc506 have hmax : Ideal.span {f} ⊔ Ideal.span {surfaceT O pi u a 0} =507 IsLocalRing.maximalIdeal (ConcreteSurface O pi u a 0) := by508 have h1 : Module.length (ConcreteSurface O pi u a 0)509 (ConcreteSurface O pi u a 0 ⧸ (Ideal.span {f} ⊔ Ideal.span {surfaceT O pi u a 0})) = 1 := by510 exact_mod_cast hc511 rw [Module.length_eq_one_iff, isSimpleModule_iff_isCoatom] at h1512 exact IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_def.mpr h1)513 subst hf514 have : Nontrivial (ConcreteSurface O pi u a 0 ⧸ Ideal.span {f}) :=515 Ideal.Quotient.nontrivial_iff.mpr hJne516 have : IsLocalRing (ConcreteSurface O pi u a 0 ⧸ Ideal.span {f}) :=517 IsLocalRing.of_surjective' _ Ideal.Quotient.mk_surjective518 have := concrete_surface_isNoetherianRing O pi u a 0519 obtain ⟨e, he⟩ := concrete_surface_special_fiber_equiv O pi hpi u a 0520 have hcon := (concrete_surface_contact_eq_special_fiber_contact O pi u a 0 ha e he f).1521 have hcontact : contact (e (Ideal.Quotient.mk (Ideal.span522 {algebraMap O (ConcreteSurface O pi u a 0) pi}) f)) (fiberT (IsLocalRing.ResidueField O) a 0)523 = (1 : ℕ) := by524 rw [← hcon]; exact_mod_cast hc525 obtain ⟨h1, h2, h3⟩ := concrete_surface_single_curve_free O pi hpi u a ha f e 1 one_pos hcontact526 refine ⟨hmax, ⟨inferInstance, ?_⟩, inferInstance, h1, h2, by simpa using h3⟩527 have hle : Ideal.span {f} ≤ IsLocalRing.maximalIdeal (ConcreteSurface O pi u a 0) :=528 hmax ▸ le_sup_left529 have hm : (IsLocalRing.maximalIdeal (ConcreteSurface O pi u a 0)).map530 (Ideal.Quotient.mk (Ideal.span {f})) =531 Ideal.span {Ideal.Quotient.mk (Ideal.span {f}) (surfaceT O pi u a 0)} := by532 rw [← hmax, Ideal.map_sup, Ideal.map_span, Ideal.map_span]533 simp534 rw [← hm]535 have hM := Ideal.IsMaximal.map_of_surjective_of_ker_le (f := Ideal.Quotient.mk (Ideal.span {f}))536 (m := IsLocalRing.maximalIdeal _) Ideal.Quotient.mk_surjective (by rw [Ideal.mk_ker]; exact hle)537 exact (@IsLocalRing.eq_maximalIdeal (ConcreteSurface O pi u a 0 ⧸ Ideal.span {f}) _ _ _ hM).symm538 539private theorem isDVR_of_maximalIdeal_eq_span (O : Type) [CommRing O] [IsDomain O]540 [IsDiscreteValuationRing O]541 (B : Type) [CommRing B] [Algebra O B] [IsLocalRing B] [IsNoetherianRing B] [Module.Free O B]542 (pi : O) (hpi : Irreducible pi) (a : ℕ) (ha : 0 < a) (tb w : B) (hunit : IsUnit w)543 (hvert : algebraMap O B pi = w * tb ^ a)544 (hm : IsLocalRing.maximalIdeal B = Ideal.span {tb}) :545 ∃ _ : IsDomain B, IsDiscreteValuationRing B ∧ Irreducible tb ∧546 Ideal.map (algebraMap O B) (IsLocalRing.maximalIdeal O) =547 (IsLocalRing.maximalIdeal B) ^ a := by548 classical549 have hinj : Function.Injective (algebraMap O B) := FaithfulSMul.algebraMap_injective O B550 have hnil : ∀ N : ℕ, tb ^ N ≠ 0 := by551 intro N hN552 have h1 : algebraMap O B (pi ^ N) = 0 := by553 obtain ⟨k, hk⟩ : ∃ k, a = k + 1 := ⟨a - 1, by omega⟩554 rw [map_pow, hvert, mul_pow, ← pow_mul, hk, add_mul, one_mul, pow_add, hN, mul_zero, mul_zero]555 have h2 : pi ^ N ≠ 0 := pow_ne_zero _ hpi.ne_zero556 exact h2 (hinj (h1.trans (map_zero _).symm))557 have hmpow : ∀ n : ℕ, IsLocalRing.maximalIdeal B ^ n = Ideal.span {tb ^ n} := by558 intro n; rw [hm, Ideal.span_singleton_pow]559 have hmne : IsLocalRing.maximalIdeal B ≠ ⊤ := Ideal.IsMaximal.ne_top inferInstance560 have hfac : ∀ x : B, x ≠ 0 → ∃ (n : ℕ) (v : B), IsUnit v ∧ x = v * tb ^ n := by561 intro x hx562 have hK := iInf_sup_pow_eq_of_isLocalRing B (IsLocalRing.maximalIdeal B) ⊥ hmne563 have hex : ∃ N, x ∉ Ideal.span {tb ^ N} := by564 by_contra hcon565 push Not at hcon566 apply hx567 have : x ∈ (⨅ n : ℕ, (⊥ : Ideal B) ⊔ IsLocalRing.maximalIdeal B ^ n) := by568 rw [Ideal.mem_iInf]; intro n; rw [bot_sup_eq, hmpow]; exact hcon n569 rw [hK] at this; exact (Submodule.mem_bot _).mp this570 set N := Nat.find hex with hN571 have hNs : x ∉ Ideal.span {tb ^ N} := Nat.find_spec hex572 have hNpos : N ≠ 0 := by573 intro h0; apply hNs; rw [h0, pow_zero, Ideal.span_singleton_one]; trivial574 obtain ⟨n, hn⟩ : ∃ n, N = n + 1 := ⟨N - 1, by omega⟩575 have hmem : x ∈ Ideal.span {tb ^ n} := by simpa using Nat.find_min hex (by omega : n < N)576 obtain ⟨v, hv⟩ := Ideal.mem_span_singleton'.mp hmem577 refine ⟨n, v, ?_, hv.symm⟩578 by_contra hvu579 have hvm : v ∈ IsLocalRing.maximalIdeal B := hvu580 rw [hm] at hvm581 obtain ⟨w, hw⟩ := Ideal.mem_span_singleton'.mp hvm582 apply hNs583 rw [hn, Ideal.mem_span_singleton']584 exact ⟨w, by rw [← hv, ← hw, pow_succ]; ring⟩585 have hdom : IsDomain B := by586 have : NoZeroDivisors B := by587 constructor588 intro x y hxy589 by_contra hne590 push Not at hne591 obtain ⟨n, v, hv, rfl⟩ := hfac x hne.1592 obtain ⟨n', v', hv', rfl⟩ := hfac y hne.2593 have : (v * v') * tb ^ (n + n') = 0 := by rw [← hxy, pow_add]; ring594 exact hnil (n + n') ((hv.mul hv').mul_right_eq_zero.mp this)595 exact NoZeroDivisors.to_isDomain B596 have hnf : ¬ IsField B := by597 rw [IsLocalRing.isField_iff_maximalIdeal_eq, hm]598 intro h599 exact hnil 1 (by rw [pow_one]; exact Ideal.span_singleton_eq_bot.mp h)600 have hp : (IsLocalRing.maximalIdeal B).IsPrincipal := ⟨⟨tb, hm⟩⟩601 have hdvr : IsDiscreteValuationRing B :=602 ((IsDiscreteValuationRing.TFAE B hnf).out 0 4).mpr hp603 refine ⟨hdom, hdvr, ?_, ?_⟩604 · exact (IsDiscreteValuationRing.irreducible_iff_uniformizer tb).mpr hm605 · rw [hpi.maximalIdeal_eq, Ideal.map_span, Set.image_singleton, hvert,606 Ideal.span_singleton_mul_left_unit hunit, hmpow]607 608/-- In the terminal state `single a 1`, the curve order `R/J` is a DVR with uniformizer `t`, and609the maximal ideal of `O` extends to the `a`-th power of its maximal ideal. -/610theorem terminal_curve_order_dvr (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 2.2611 [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)612 (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)613 [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)]614 (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSpi : S.pi = pi)615 (hSt : S.t = (surfaceT O pi u a b)) (hSx : S.x = (surfaceX O pi u a b)) (hSa : S.a = a)616 (hSb : S.b = b) (J : Ideal (ConcreteSurface O pi u a b))617 (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S (State.single a 1))618 (f : (ConcreteSurface O pi u a b)) (hf : J = Ideal.span {f}) :619 ∃ (_ : IsDomain ((ConcreteSurface O pi u a b) ⧸ J)) (_ : IsLocalRing620 ((ConcreteSurface O pi u a b) ⧸ J)),621 IsDiscreteValuationRing ((ConcreteSurface O pi u a b) ⧸ J) ∧622 Irreducible (Ideal.Quotient.mk J (surfaceT O pi u a b)) ∧623 Ideal.map (algebraMap O ((ConcreteSurface O pi u a b) ⧸ J) : O →+*624 ((ConcreteSurface O pi u a b) ⧸ J)) (IsLocalRing.maximalIdeal O) =625 (IsLocalRing.maximalIdeal ((ConcreteSurface O pi u a b) ⧸ J))^a := by626 obtain ⟨-, ⟨hloc, hm⟩, hnoeth, hfree, hfin, hrank⟩ :=627 terminal_curve_order_local_principal O pi hpi u a b ha S hSpi hSt hSx hSa hSb J hJ f hf628 obtain rfl : b = 0 := hSb ▸ hJ.2.2.2.1629 have hvert : (algebraMap O ((ConcreteSurface O pi u a 0) ⧸ J) : O →+*630 ((ConcreteSurface O pi u a 0) ⧸ J)) pi =631 Ideal.Quotient.mk J (surfaceUnit O pi u a 0 : ConcreteSurface O pi u a 0) *632 (Ideal.Quotient.mk J (surfaceT O pi u a 0)) ^ a := by633 rw [← Ideal.Quotient.mk_algebraMap, concrete_surface_vertical]634 simp [map_mul, map_pow]635 obtain ⟨hdom, hdvr, hirr, hmap⟩ := isDVR_of_maximalIdeal_eq_span O636 ((ConcreteSurface O pi u a 0) ⧸ J) pi hpi a ha637 _ _ ((Units.isUnit _).map _) hvert hm638 exact ⟨hdom, hloc, hdvr, hirr, hmap⟩639 640/-- In the terminal state, the generic fibre `K ⊗[O] B` of (an algebra `B` isomorphic to) the641curve order is a finite field extension of `K` in which `B` embeds as the integral closure. -/642private theorem terminal_generic_fibre_field (O : Type) [CommRing O] [IsDomain O]643 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]644 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)645 (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]646 [IsRegularLocalRing (ConcreteSurface O pi u a b)]647 (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSpi : S.pi = pi)648 (hSt : S.t = (surfaceT O pi u a b)) (hSx : S.x = (surfaceX O pi u a b)) (hSa : S.a = a)649 (hSb : S.b = b) (J : Ideal (ConcreteSurface O pi u a b))650 (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S (State.single a 1))651 (f : (ConcreteSurface O pi u a b)) (hf : J = Ideal.span {f}) (B : Type) [CommRing B]652 [Algebra O B] (eB : B ≃ₐ[O] ((ConcreteSurface O pi u a b) ⧸ J)) :653 IsField (TensorProduct O (BaseField O) B) ∧654 Module.Finite (BaseField O) (TensorProduct O (BaseField O) B) ∧655 Function.Injective (Algebra.TensorProduct.includeRight : B →ₐ[O]656 (TensorProduct O (BaseField O) B)) ∧657 integralClosure O (TensorProduct O (BaseField O) B) =658 (Algebra.TensorProduct.includeRight : B →ₐ[O] (TensorProduct O (BaseField O) B)).range := by659 obtain ⟨-, -, -, hfree, hfin, -⟩ := terminal_curve_order_local_principal O pi hpi u a b ha S660 hSpi hSt hSx hSa hSb J hJ f hf661 obtain ⟨hdomA, -, hdvr, -, -⟩ := terminal_curve_order_dvr O pi hpi u a b ha S662 hSpi hSt hSx hSa hSb J hJ f hf663 set A := (ConcreteSurface O pi u a b) ⧸ J664 have : IsDomain B := Function.Injective.isDomain eB.toRingHom eB.injective665 have : IsIntegrallyClosed A := inferInstance666 have : IsIntegrallyClosed B := @IsIntegrallyClosed.of_equiv A B _ _667 (eB.symm.toRingEquiv : A ≃+* B) _668 have : Module.Free O B := Module.Free.of_equiv eB.symm.toLinearEquiv669 have : Module.Finite O B := Module.Finite.equiv eB.symm.toLinearEquiv670 set K := BaseField O671 set L := TensorProduct O K B672 let _ : Algebra B L := Algebra.TensorProduct.rightAlgebra673 have hinjO : Function.Injective (algebraMap O B) := FaithfulSMul.algebraMap_injective O B674 set Mo := Algebra.algebraMapSubmonoid B (nonZeroDivisors O)675 have hloc : IsLocalization Mo L := IsLocalization.tensorRight (A := K) (S := B)676 (nonZeroDivisors O)677 have hM : Mo ≤ nonZeroDivisors B := by678 rintro _ ⟨o, ho, rfl⟩679 exact mem_nonZeroDivisors_of_ne_zero ((map_ne_zero_iff _ hinjO).2 (nonZeroDivisors.ne_zero ho))680 have hinj : Function.Injective (algebraMap B L) := IsLocalization.injective L hM681 have : IsDomain L := IsLocalization.isDomain_of_le_nonZeroDivisors L hM682 have : Module.Finite K L := inferInstance683 have : Algebra.IsIntegral K L := Algebra.IsIntegral.of_finite K L684 have hfield : IsField L :=685 (Algebra.IsIntegral.isField_iff_isField (R := K) (S := L) (algebraMap K L).injective).1686 (Field.toIsField K)687 have hfr : IsFractionRing B L := by688 refine IsLocalization.of_le Mo _ hM (fun r hr => ?_)689 have hx : algebraMap B L r ≠ 0 :=690 (map_ne_zero_iff _ hinj).2 (nonZeroDivisors.ne_zero hr)691 obtain ⟨y, hy⟩ := hfield.mul_inv_cancel hx692 exact IsUnit.of_mul_eq_one _ hy693 refine ⟨hfield, inferInstance, hinj, ?_⟩694 ext x695 constructor696 · intro hx697 have hxB : IsIntegral B x := IsIntegral.tower_top (A := B) hx698 obtain ⟨y, rfl⟩ := (IsIntegrallyClosed.isIntegral_iff (K := L)).1 hxB699 exact ⟨y, rfl⟩700 · rintro ⟨y, rfl⟩701 exact (Algebra.IsIntegral.isIntegral (R := O) y).map702 (Algebra.TensorProduct.includeRight : B →ₐ[O] L)703 704private theorem fieldInvariant_eq_of_dvr (O : Type) [CommRing O] [IsDomain O]705 [IsDiscreteValuationRing O]706 (Q : Type) [CommRing Q] [IsDomain Q] [IsDiscreteValuationRing Q] [Algebra O Q]707 [Module.Free O Q] [Module.Finite O Q] (a : ℕ) (ha : 0 < a) (hrank : Module.finrank O Q = a)708 (hmap : (IsLocalRing.maximalIdeal O).map (algebraMap O Q) = (IsLocalRing.maximalIdeal Q) ^ a)709 (B : Type) [CommRing B] [Algebra O B] (eB : B ≃ₐ[O] Q)710 (hinj : Function.Injective (Algebra.TensorProduct.includeRight : B →ₐ[O]711 (TensorProduct O (BaseField O) B)))712 (hrange : integralClosure O (TensorProduct O (BaseField O) B) =713 (Algebra.TensorProduct.includeRight : B →ₐ[O] (TensorProduct O (BaseField O) B)).range) :714 fieldInvariant O (TensorProduct O (BaseField O) B) = (a, 1) := by715 set L := TensorProduct O (BaseField O) B716 let ψ : Q ≃ₐ[O] integralClosure O L := eB.symm.trans717 ((AlgEquiv.ofInjective _ hinj).trans (Subalgebra.equivOfEq _ _ hrange.symm))718 have : IsDomain (integralClosure O L) := MulEquiv.isDomain Q ψ.symm.toMulEquiv719 have hD : IsDiscreteValuationRing (integralClosure O L) :=720 IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing ψ721 have : Algebra.IsIntegral O Q := Algebra.IsIntegral.of_finite O Q722 have hinjQ : Function.Injective (algebraMap O Q) := FaithfulSMul.algebraMap_injective O Q723 have hinjB : Function.Injective (algebraMap O (integralClosure O L)) := by724 have : algebraMap O (integralClosure O L) = (ψ : Q →+* integralClosure O L).comp725 (algebraMap O Q) := by726 ext x; simp727 rw [this]; exact ψ.injective.comp hinjQ728 obtain ⟨he, hfd⟩ := dvr_algEquiv_ramification_inertia O Q (integralClosure O L) hinjQ hinjB ψ729 have h512 := dvr_extension_maximalIdeal_map_eq_pow O Q hinjQ730 have h251 := finite_flat_local_ramification_degree O Q731 have hea : (IsLocalRing.maximalIdeal Q).ramificationIdx O = a := by732 rw [hmap] at h512733 have hne : IsLocalRing.maximalIdeal Q ≠ ⊥ := IsDiscreteValuationRing.not_a_field Q734 exact ((Ideal.pow_right_strictAnti _ hne (Ideal.IsMaximal.ne_top inferInstance)).injective735 h512).symm736 have hf1 : (IsLocalRing.maximalIdeal Q).inertiaDeg O = 1 := by737 rw [hea, hrank] at h251738 exact Nat.eq_of_mul_eq_mul_left ha (by simpa using h251)739 have hl : IsLocalRing (integralClosure O L) := hD.toIsLocalRing740 unfold fieldInvariant741 dsimp only742 rw [dif_pos hl, ← he, ← hfd, hea, hf1]743 744/-- In the terminal state `single a 1`, the generic fibre of the curve order has field invariant745`(a, 1)`: ramification index `a` and residue degree `1`. -/746theorem terminal_field_invariant (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 2.2747 [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)748 (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)749 [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)]750 (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSpi : S.pi = pi)751 (hSt : S.t = (surfaceT O pi u a b)) (hSx : S.x = (surfaceX O pi u a b)) (hSa : S.a = a)752 (hSb : S.b = b) (J : Ideal (ConcreteSurface O pi u a b))753 (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S (State.single a 1))754 (f : (ConcreteSurface O pi u a b)) (hf : J = Ideal.span {f}) (B : Type) [CommRing B]755 [Algebra O B] (eB : B ≃ₐ[O] ((ConcreteSurface O pi u a b) ⧸ J)) :756 fieldInvariant O (TensorProduct O (BaseField O) B) = (a, 1) := by757 obtain ⟨-, -, -, hfree, hfin, hrank⟩ := terminal_curve_order_local_principal O pi hpi u a b ha S758 hSpi hSt hSx hSa hSb J hJ f hf759 obtain ⟨hdom, hloc, hdvr, -, hmap⟩ := terminal_curve_order_dvr O pi hpi u a b ha S760 hSpi hSt hSx hSa hSb J hJ f hf761 obtain ⟨-, -, hinj, hrange⟩ := terminal_generic_fibre_field O pi hpi u a b ha S762 hSpi hSt hSx hSa hSb J hJ f hf B eB763 exact @fieldInvariant_eq_of_dvr O _ _ _ (ConcreteSurface O pi u a b ⧸ J) _ hdom hdvr _ hfree hfin764 a ha hrank hmap B _ _ eB hinj hrange765 766/-- In the terminal state `single a 1`, every ideal of the state set has algebra type `{(a, 1)}`. -/767theorem concrete_member_terminal_type (m : ConcreteMember) (a : ℕ) (hs : m.s = State.single a 1)Lemma 2.2768 (J : Ideal m.R) (hJ : J ∈ m.toMeasured.stateSet) :769 HasAlgebraType m.O (m.R ⧸ J) {(a, 1)} := by770 have hsh := m.shape771 rw [hs] at hsh772 obtain ⟨rfl, -, -⟩ := hsh773 have hJ' : J ∈ surfaceStateSet m.O m.R m.S (State.single m.a 1) := by774 have : J ∈ surfaceStateSet m.O m.R m.S m.s := hJ775 rwa [hs] at this776 obtain ⟨f, hf⟩ := hJ'.1777 have h1 := terminal_generic_fibre_field m.O m.pi m.hpi m.u m.a m.b m.ha m.S778 m.hS_pi m.hS_t m.hS_x m.hS_a m.hS_b J hJ' f hf (m.R ⧸ J) (AlgEquiv.refl)779 have h2 := terminal_field_invariant m.O m.pi m.hpi m.u m.a m.b m.ha m.S780 m.hS_pi m.hS_t m.hS_x m.hS_a m.hS_b J hJ' f hf (m.R ⧸ J) (AlgEquiv.refl)781 let _ : Field (TensorProduct m.O (BaseField m.O) (m.R ⧸ J)) := h1.1.toField782 obtain ⟨-, -, -, -, _, -⟩ := terminal_curve_order_local_principal m.O m.pi m.hpi m.u783 m.a m.b m.ha m.S m.hS_pi m.hS_t m.hS_x m.hS_a m.hS_b J hJ' f hf784 have hcl := Module.Finite.equiv785 ((AlgEquiv.ofInjective _ h1.2.2.1).trans (Subalgebra.equivOfEq _ _ h1.2.2.2.symm)).toLinearEquiv786 let _ : Algebra (BaseField m.O) (TensorProduct m.O (BaseField m.O) (m.R ⧸ J)) :=787 Algebra.TensorProduct.leftAlgebra (R := m.O) (S := BaseField m.O) (A := BaseField m.O)788 (B := m.R ⧸ J)789 have hfd : FiniteDimensional (BaseField m.O) (TensorProduct m.O (BaseField m.O) (m.R ⧸ J)) :=790 h1.2.1791 refine ⟨Unit, inferInstance, fun _ => TensorProduct m.O (BaseField m.O) (m.R ⧸ J), fun _ =>792 inferInstance,793 fun _ => inferInstance,794 fun _ => Algebra.TensorProduct.instAlgebra (R := m.O) (A := BaseField m.O) (B := m.R ⧸ J),795 fun _ => inferInstance, fun _ => hfd,796 (AlgEquiv.funUnique (BaseField m.O) Unit (TensorProduct m.O (BaseField m.O) (m.R ⧸ J))).symm,797 by rw [Fintype.sum_unique]; exact congrArg _ h2.symm, fun _ => hcl⟩798 799/-! ### Terminating sets of a surface universe -/800 801/-- The terminating set lies in the state set, equals it in terminal states, and in nonterminal802states its intersection with each cell is the child box of the children's terminating sets. -/803theorem terminates_cell_decomposition (U : SurfaceUniverse) (i : U.ι) :804 U.terminatingSet i ⊆ (U.M i).stateSet ∧805 ((U.M i).s.terminal = true → U.terminatingSet i = (U.M i).stateSet) ∧806 ((U.M i).s.terminal = false → ∀ c : (U.M i).cellIndex, U.terminatingSet i ∩ (U.M i).cell c =807 U.childBox i c (fun j => U.terminatingSet (U.child i c j))) := by808 have h1 : U.terminatingSet i ⊆ (U.M i).stateSet := by809 intro J hJ810 cases hJ with811 | leaf _ _ hJ _ => exact hJ812 | node _ c _ hJ hnt _ =>813 rw [U.cells_cover i hnt]814 exact Set.mem_iUnion.2 ⟨c, hJ⟩815 refine ⟨h1, fun ht => Set.Subset.antisymm h1 fun J hJ => SurfaceUniverse.Terminates.leaf i J hJ816 ht, ?_⟩817 intro hnt c818 ext J819 constructor820 · rintro ⟨hJ, hc⟩821 refine ⟨hc, ?_⟩822 change U.Terminates i J at hJ823 cases hJ with824 | leaf _ _ _ ht => rw [ht] at hnt; cases hnt825 | node _ c' _ hJ' _ h =>826 have : c' = c := by827 by_contra hne828 exact Set.disjoint_left.1 (U.cells_disjoint i hnt hne) hJ' hc829 subst this830 exact Set.mem_univ_pi.2 h831 · rintro ⟨hc, hp⟩832 exact ⟨SurfaceUniverse.Terminates.node i c J hc hnt (Set.mem_univ_pi.1 hp), hc⟩833 834/-- Every terminating ideal has a factorization type, and this type is unique. -/835theorem terminates_type_unique (U : SurfaceUniverse) (i : U.ι) (J : Ideal (U.M i).R)836 (hJ : U.Terminates i J) :837 ∃ σ : FactorType, HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ ∧ ∀ τ : FactorType,838 HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) τ → τ = σ := by839 have ex : ∃ σ : FactorType, HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ := by840 induction hJ with841 | leaf i J hJ ht =>842 have : ∃ a, (U.M i).s = State.single a 1 := by843 cases hs : (U.M i).s with844 | single a c =>845 rw [hs] at ht846 cases c with847 | zero => simp [State.terminal] at ht848 | succ n =>849 cases n with850 | zero => exact ⟨a, rfl⟩851 | succ m => simp [State.terminal] at ht852 | crossing a b c h => rw [hs] at ht; simp [State.terminal] at ht853 obtain ⟨a, ha⟩ := this854 exact ⟨_, U.terminal_type i a ha J hJ⟩855 | node i c J hJ hnt h ih =>856 choose τ hτ using ih857 exact ⟨_, U.type_add i hnt c J hJ τ hτ⟩858 obtain ⟨σ, hσ⟩ := ex859 refine ⟨σ, hσ, fun τ hτ => ?_⟩860 have := (U.M i).instDomain861 exact algebra_type_unique (U.M i).O _ τ σ hτ hσ862 863/-- The law statement holds at terminal states of a surface universe. -/864theorem recursion_terminal_law (U : SurfaceUniverse) (i : U.ι) (ht : (U.M i).s.terminal = true) :865 U.LawStatement i := by866 obtain ⟨a, ha⟩ : ∃ a, (U.M i).s = State.single a 1 := by867 generalize (U.M i).s = s at ht868 cases s with869 | single a c =>870 cases c with871 | zero => simp [State.terminal] at ht872 | succ c =>873 cases c with874 | zero => exact ⟨a, rfl⟩875 | succ c => simp [State.terminal] at ht876 | crossing a b c h => simp [State.terminal] at ht877 have hT : U.terminatingSet i = (U.M i).stateSet :=878 (terminates_cell_decomposition U i).2.1 ht879 have hm := U.stateSet_measurable i880 refine ⟨fun σ => ?_, by rw [hT]; exact hm, ?_⟩881 · have hev : U.termTypeEvent i σ = if σ = {(a,1)} then (U.M i).stateSet else ∅ := by882 ext J883 simp only [SurfaceUniverse.termTypeEvent, SurfaceUniverse.typeEvent, Set.mem_inter_iff,884 Set.mem_ofPred_eq, hT]885 split_ifs with hσ886 · subst hσ887 exact ⟨fun h => h.1.1, fun h => ⟨⟨h, U.terminal_type i a ha J h⟩, h⟩⟩888 · simp only [Set.mem_empty_iff_false, iff_false]889 rintro ⟨⟨hJ, hty⟩, -⟩890 have h1 := U.terminal_type i a ha J hJ891 obtain ⟨s, -, hs⟩ := terminates_type_unique U i J892 (SurfaceUniverse.Terminates.leaf i J hJ ht)893 exact hσ ((hs σ hty).trans (hs _ h1).symm)894 have hc : lawCoeff (stateLaw (U.M i).s) σ =895 Expr.add (if ({(a,1)} : FactorType) = σ then Expr.const 1 else Expr.const 0)896 (Expr.const 0) := by897 rw [ha, terminal_law]898 simp [lawCoeff, lawAtom, Expr.sum]899 rw [hev]900 by_cases hσ : σ = {(a,1)}901 · subst hσ902 simp only [if_true]903 have : densityValue (lawCoeff (stateLaw (U.M i).s) {(a,1)}) (U.M i).q = 1 := by904 rw [hc]; simp [densityValue, Expr.eval]905 refine ⟨hm, ?_, ?_⟩906 · rw [hc]; simp [Expr.eval]907 · rw [this, one_mul]908 · have hσ' : ¬ ({(a,1)} : FactorType) = σ := fun h => hσ h.symm909 simp only [hσ, if_false]910 have : densityValue (lawCoeff (stateLaw (U.M i).s) σ) (U.M i).q = 0 := by911 rw [hc]; simp [densityValue, Expr.eval, hσ']912 refine ⟨MeasurableSet.empty, ?_, ?_⟩913 · rw [hc]; simp [Expr.eval, hσ']914 · rw [this, zero_mul, MeasureTheory.measure_empty]915 · unfold SurfaceUniverse.nonterminatingSet916 rw [hT, Set.inter_compl_self, MeasureTheory.measure_empty]917 918/-- At a nonterminal state, the terminating type-`σ` event intersected with a cell is the type box919of that cell. -/920theorem term_type_event_cell_decomposition (U : SurfaceUniverse) (i : U.ι)921 (hnt : (U.M i).s.terminal = false) (c : (U.M i).cellIndex) (σ : FactorType) :922 U.termTypeEvent i σ ∩ (U.M i).cell c = U.typeBox i c σ := by923 ext J924 constructor925 · rintro ⟨⟨⟨hJs, hJσ⟩, hJt⟩, hJc⟩926 have hdec := (terminates_cell_decomposition U i).2.2 hnt c927 have hmem : J ∈ U.childBox i c (fun j => U.terminatingSet (U.child i c j)) := by928 rw [← hdec]; exact ⟨hJt, hJc⟩929 have hchild : ∀ j, U.Terminates (U.child i c j) (U.Φ i c J j) := fun j =>930 (Set.mem_univ_pi.mp hmem.2) j931 choose τ hτ _ using fun j => terminates_type_unique U (U.child i c j) _ (hchild j)932 have hadd := U.type_add i hnt c J hJc τ hτ933 obtain ⟨σ0, _, hu⟩ := terminates_type_unique U i J hJt934 have h1 : σ = ∑ j, scaleType ((U.M i).childDelta c j) (τ j) := by935 rw [hu σ hJσ, hu _ hadd]936 refine Set.mem_iUnion.mpr ⟨τ, Set.mem_iUnion.mpr ⟨h1, hJc, ?_⟩⟩937 refine Set.mem_univ_pi.mpr fun j => ⟨⟨?_, hτ j⟩, hchild j⟩938 exact ((U.Φ_bij i hnt c).mapsTo hJc) j (Set.mem_univ _)939 · intro h940 obtain ⟨τ, h⟩ := Set.mem_iUnion.mp h941 obtain ⟨h1, h⟩ := Set.mem_iUnion.mp h942 obtain ⟨hJc, hΦ⟩ := h943 have hp := Set.mem_univ_pi.mp hΦ944 have hterm : U.Terminates i J :=945 SurfaceUniverse.Terminates.node i c J hJc hnt fun j => (hp j).2946 refine ⟨⟨⟨?_, ?_⟩, hterm⟩, hJc⟩947 · rw [U.cells_cover i hnt]; exact Set.mem_iUnion.mpr ⟨c, hJc⟩948 · rw [h1]; exact U.type_add i hnt c J hJc τ fun j => (hp j).1.2949 950section951 952variable (U : SurfaceUniverse)953 954private theorem self_list {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c) :955 (U.M i).childList c = [(1, (U.M i).s)] :=956 h.choose_spec.choose_spec.2957 958private theorem self_len {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c) :959 ((U.M i).childList c).length = 1 := by960 rw [self_list U h]; rfl961 962private theorem self_get {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c)963 (j : (U.M i).childIdx c) : ((U.M i).childList c).get j = (1, (U.M i).s) := by964 simp [self_list U h]965 966private theorem self_delta {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c)967 (j : (U.M i).childIdx c) : (U.M i).childDelta c j = 1 := by968 unfold MeasuredSurface.childDelta; rw [self_get U h]969 970private theorem self_state {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c)971 (j : (U.M i).childIdx c) : (U.M (U.child i c j)).s = (U.M i).s := by972 rw [U.child_state]; unfold MeasuredSurface.childState; rw [self_get U h]973 974private def selfChildIdx {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c) :975 (U.M i).childIdx c := ⟨0, by rw [self_len U h]; omega⟩976 977private theorem self_sub {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c)978 (j j' : (U.M i).childIdx c) : j = j' := by979 have := self_len U h980 apply Fin.ext; have := j.2; have := j'.2; omega981 982private theorem scale_one (σ : FactorType) : scaleType 1 σ = σ := by983 simp [scaleType]984 985private theorem self_sum {i : U.ι} {c : (U.M i).cellIndex} (h : (U.M i).IsSelfCell c)986 (σ : FactorType) :987 σ = ∑ j : (U.M i).childIdx c, scaleType ((U.M i).childDelta c j) σ := by988 simp only [self_delta U h, scale_one, Finset.sum_const, Finset.card_univ, Fintype.card_fin,989 self_len U h, one_smul]990 991/-- Exit events are contained in terminating type events. -/992private theorem exit_sub (σ : FactorType) : ∀ k (i : U.ι), (U.M i).s.terminal = false →993 U.exitEvent σ k i ⊆ U.termTypeEvent i σ := by994 intro k995 induction k with996 | zero =>997 intro i hnt J hJ998 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion] at hJ999 obtain ⟨c, hc⟩ := hJ1000 rw [← term_type_event_cell_decomposition U i hnt c.1 σ] at hc1001 exact hc.11002 | succ k ih =>1003 intro i hnt J hJ1004 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion] at hJ1005 obtain ⟨c, hc⟩ := hJ1006 have hJ' : J ∈ U.typeBox i c.1 σ := by1007 simp only [SurfaceUniverse.typeBox, Set.mem_iUnion]1008 refine ⟨fun _ => σ, self_sum U c.2 σ, hc.1, ?_⟩1009 intro j _1010 have hnt' : (U.M (U.child i c.1 j)).s.terminal = false := by1011 rw [self_state U c.2 j]; exact hnt1012 exact ih _ hnt' (hc.2 j (Set.mem_univ _))1013 rw [← term_type_event_cell_decomposition U i hnt c.1 σ] at hJ'1014 exact hJ'.11015 1016private theorem term_exit_sub : ∀ k (i : U.ι), (U.M i).s.terminal = false →1017 U.termExitEvent k i ⊆ U.terminatingSet i := by1018 intro k1019 induction k with1020 | zero =>1021 intro i hnt J hJ1022 simp only [SurfaceUniverse.termExitEvent, Set.mem_iUnion] at hJ1023 obtain ⟨c, hc⟩ := hJ1024 exact SurfaceUniverse.Terminates.node i c.1 J hc.1 hnt (fun j => hc.2 j (Set.mem_univ _))1025 | succ k ih =>1026 intro i hnt J hJ1027 simp only [SurfaceUniverse.termExitEvent, Set.mem_iUnion] at hJ1028 obtain ⟨c, hc⟩ := hJ1029 refine SurfaceUniverse.Terminates.node i c.1 J hc.1 hnt (fun j => ?_)1030 have hnt' : (U.M (U.child i c.1 j)).s.terminal = false := by1031 rw [self_state U c.2 j]; exact hnt1032 exact ih _ hnt' (hc.2 j (Set.mem_univ _))1033 1034private theorem term_sub_exit (σ : FactorType) (i : U.ι) (J : Ideal (U.M i).R)1035 (hT : U.Terminates i J) :1036 (U.M i).s.terminal = false → J ∈ U.typeEvent i σ → ∃ k, J ∈ U.exitEvent σ k i := by1037 induction hT with1038 | leaf i J _ ht => intro hnt; rw [ht] at hnt; cases hnt1039 | node i c J hJ hnt h ih =>1040 intro _ hty1041 have hmem : J ∈ U.termTypeEvent i σ ∩ (U.M i).cell c :=1042 ⟨⟨hty, SurfaceUniverse.Terminates.node i c J hJ hnt h⟩, hJ⟩1043 rw [term_type_event_cell_decomposition U i hnt c σ] at hmem1044 by_cases hs : (U.M i).IsSelfCell c1045 · simp only [SurfaceUniverse.typeBox, Set.mem_iUnion] at hmem1046 obtain ⟨τ, hτ, hb⟩ := hmem1047 let j0 := selfChildIdx U hs1048 have hτ0 : σ = τ j0 := by1049 rw [hτ]1050 simp only [self_delta U hs, scale_one]1051 rw [Fintype.sum_eq_single j0 (fun j hj => absurd (self_sub U hs j j0) hj)]1052 have hc0 : U.Φ i c J j0 ∈ U.termTypeEvent (U.child i c j0) (τ j0) := hb.2 j0 (Set.mem_univ _)1053 rw [← hτ0] at hc01054 have hnt' : (U.M (U.child i c j0)).s.terminal = false := by1055 rw [self_state U hs j0]; exact hnt1056 obtain ⟨k, hk⟩ := ih j0 hnt' hc0.11057 refine ⟨k+1, ?_⟩1058 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion]1059 refine ⟨⟨c, hs⟩, hJ, ?_⟩1060 intro j _1061 rw [self_sub U hs j j0]; exact hk1062 · refine ⟨0, ?_⟩1063 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion]1064 exact ⟨⟨c, hs⟩, hmem⟩1065 1066private theorem term_sub_texit (i : U.ι) (J : Ideal (U.M i).R) (hT : U.Terminates i J) :1067 (U.M i).s.terminal = false → ∃ k, J ∈ U.termExitEvent k i := by1068 induction hT with1069 | leaf i J _ ht => intro hnt; rw [ht] at hnt; cases hnt1070 | node i c J hJ hnt h ih =>1071 intro _1072 by_cases hs : (U.M i).IsSelfCell c1073 · let j0 := selfChildIdx U hs1074 have hnt' : (U.M (U.child i c j0)).s.terminal = false := by1075 rw [self_state U hs j0]; exact hnt1076 obtain ⟨k, hk⟩ := ih j0 hnt'1077 refine ⟨k+1, ?_⟩1078 simp only [SurfaceUniverse.termExitEvent, Set.mem_iUnion]1079 refine ⟨⟨c, hs⟩, hJ, ?_⟩1080 intro j _1081 rw [self_sub U hs j j0]; exact hk1082 · refine ⟨0, ?_⟩1083 simp only [SurfaceUniverse.termExitEvent, Set.mem_iUnion]1084 exact ⟨⟨c, hs⟩, hJ, fun j _ => h j⟩1085 1086private theorem exit_disj (σ : FactorType) : ∀ k k' (i : U.ι), (U.M i).s.terminal = false → k ≠ k' →1087 Disjoint (U.exitEvent σ k i) (U.exitEvent σ k' i) := by1088 intro k1089 induction k with1090 | zero =>1091 intro k' i hnt hk1092 obtain ⟨k', rfl⟩ : ∃ m, k' = m + 1 := ⟨k' - 1, by omega⟩1093 rw [Set.disjoint_left]1094 intro J h1 h21095 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion] at h1 h21096 obtain ⟨c1, hc1⟩ := h11097 obtain ⟨c2, hc2⟩ := h21098 have hne : c1.1 ≠ c2.1 := fun e => c1.2 (e ▸ c2.2)1099 have hJ1 : J ∈ (U.M i).cell c1.1 := by1100 simp only [SurfaceUniverse.typeBox, Set.mem_iUnion] at hc11101 obtain ⟨_, _, hb⟩ := hc1; exact hb.11102 exact Set.disjoint_left.mp (U.cells_disjoint i hnt hne) hJ1 hc2.11103 | succ k ih =>1104 intro k' i hnt hk1105 rw [Set.disjoint_left]1106 intro J h1 h21107 cases k' with1108 | zero =>1109 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion] at h1 h21110 obtain ⟨c1, hc1⟩ := h11111 obtain ⟨c2, hc2⟩ := h21112 have hne : c1.1 ≠ c2.1 := fun e => c2.2 (e ▸ c1.2)1113 have hJ2 : J ∈ (U.M i).cell c2.1 := by1114 simp only [SurfaceUniverse.typeBox, Set.mem_iUnion] at hc21115 obtain ⟨_, _, hb⟩ := hc2; exact hb.11116 exact Set.disjoint_left.mp (U.cells_disjoint i hnt hne) hc1.1 hJ21117 | succ k' =>1118 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion] at h1 h21119 obtain ⟨c1, hc1⟩ := h11120 obtain ⟨c2, hc2⟩ := h21121 by_cases hne : c1.1 = c2.11122 · have : c1 = c2 := Subtype.ext hne1123 subst this1124 let j0 := selfChildIdx U c1.21125 have hnt' : (U.M (U.child i c1.1 j0)).s.terminal = false := by1126 rw [self_state U c1.2 j0]; exact hnt1127 exact Set.disjoint_left.mp (ih k' _ hnt' (by omega)) (hc1.2 j0 (Set.mem_univ _))1128 (hc2.2 j0 (Set.mem_univ _))1129 · exact Set.disjoint_left.mp (U.cells_disjoint i hnt hne) hc1.1 hc2.11130 1131end1132 1133/-- For a single state, the terminating type-`σ` event (resp. the terminating set) is the disjoint1134union over `k` of the exit events (resp. terminating exit events) after `k` returns; for a1135crossing state only `k = 0` occurs. -/1136theorem single_state_return_chain (U : SurfaceUniverse) (i : U.ι) (hnt : (U.M i).s.terminal = false)1137 (σ : FactorType) :1138 (∀ a c : ℕ, (U.M i).s = State.single a c → U.termTypeEvent i σ = ⋃ k, U.exitEvent σ k i ∧1139 Pairwise (fun k k' : ℕ => Disjoint (U.exitEvent σ k i) (U.exitEvent σ k' i)) ∧1140 U.terminatingSet i = ⋃ k, U.termExitEvent k i) ∧1141 (∀ a b c h : ℕ, (U.M i).s = State.crossing a b c h → U.termTypeEvent i σ = U.exitEvent σ 0 i ∧1142 U.terminatingSet i = U.termExitEvent 0 i) := by1143 have hA : U.termTypeEvent i σ = ⋃ k, U.exitEvent σ k i := by1144 apply Set.Subset.antisymm1145 · intro J hJ1146 obtain ⟨k, hk⟩ := term_sub_exit U σ i J hJ.2 hnt hJ.11147 exact Set.mem_iUnion.mpr ⟨k, hk⟩1148 · exact Set.iUnion_subset fun k => exit_sub U σ k i hnt1149 have hB : U.terminatingSet i = ⋃ k, U.termExitEvent k i := by1150 apply Set.Subset.antisymm1151 · intro J hJ1152 obtain ⟨k, hk⟩ := term_sub_texit U i J hJ hnt1153 exact Set.mem_iUnion.mpr ⟨k, hk⟩1154 · exact Set.iUnion_subset fun k => term_exit_sub U k i hnt1155 refine ⟨fun _ _ _ => ⟨hA, fun k k' hk => exit_disj U σ k k' i hnt hk, hB⟩, ?_⟩1156 intro a b c h hs1157 have noself : ∀ c' : (U.M i).cellIndex, ¬ (U.M i).IsSelfCell c' := by1158 intro c' hc'1159 obtain ⟨a', c'', hs', _⟩ := hc'1160 rw [hs] at hs'; cases hs'1161 constructor1162 · rw [hA]1163 apply Set.Subset.antisymm1164 · intro J hJ1165 obtain ⟨k, hk⟩ := Set.mem_iUnion.mp hJ1166 cases k with1167 | zero => exact hk1168 | succ k =>1169 simp only [SurfaceUniverse.exitEvent, Set.mem_iUnion] at hk1170 obtain ⟨c', _⟩ := hk1171 exact absurd c'.2 (noself c'.1)1172 · exact Set.subset_iUnion (fun k => U.exitEvent σ k i) 01173 · rw [hB]1174 apply Set.Subset.antisymm1175 · intro J hJ1176 obtain ⟨k, hk⟩ := Set.mem_iUnion.mp hJ1177 cases k with1178 | zero => exact hk1179 | succ k =>1180 simp only [SurfaceUniverse.termExitEvent, Set.mem_iUnion] at hk1181 obtain ⟨c', _⟩ := hk1182 exact absurd c'.2 (noself c'.1)1183 · exact Set.subset_iUnion (fun k => U.termExitEvent k i) 01184 1185/-- Basic facts on a surface universe: `q ≥ 2` for every member and child, the state set has1186positive finite measure, and there are finitely many cells. -/1187theorem universe_basic_facts (U : SurfaceUniverse) (i : U.ι) :1188 2 ≤ (U.M i).q ∧ 0 < (U.M i).μ (U.M i).stateSet ∧ (U.M i).μ (U.M i).stateSet ≠ ⊤ ∧1189 (∀ (c : (U.M i).cellIndex) (j : (U.M i).childIdx c), 2 ≤ (U.M (U.child i c j)).q) ∧1190 Finite (U.M i).cellIndex := by1191 have hq : ∀ k : U.ι, 2 ≤ (U.M k).q := fun k => by1192 exact Finite.one_lt_card1193 have hA0 := fun k => density_value_arith (U.M k).q (hq k) (.const 1) (.const 1)1194 (by simp [Expr.eval]) (by simp [Expr.eval]) 0 (U.M k).s (U.M k).valid1195 have hA := fun k => density_value_arith (U.M k).q (hq k) (stateVolume (U.M k).s) (.const 1)1196 (hA0 k).2.2.2.2.2.2.1.le (by simp [Expr.eval]) 0 (U.M k).s (U.M k).valid1197 refine ⟨hq i, ?_, ?_, ?_, ?_⟩1198 · rw [U.volume]1199 exact pos_iff_ne_zero.2 ((hA i).2.2.2.2.2.1 (hA0 i).2.2.2.2.2.2.1)1200 · rw [U.volume]; exact (hA i).2.2.2.2.11201 · intro c j1202 rw [U.child_residue]1203 have hd : 0 < (U.M i).childDelta c j :=1204 children_residue_degree_pos (U.M i).s c.1.1 _ (List.get_mem _ _)1205 calc 2 ≤ (U.M i).q := hq i1206 _ ≤ _ := Nat.le_self_pow hd.ne' _1207 · have : ∀ P : (U.M i).allowedPattern, Finite (patternDivisors1208 (IsLocalRing.ResidueField (U.M i).R) (U.M i).s P.1) :=1209 fun P => U.divisors_finite i P.11210 have : Finite (U.M i).allowedPattern := inferInstance1211 change Finite (Σ P : (U.M i).allowedPattern,1212 patternDivisors (IsLocalRing.ResidueField (U.M i).R) (U.M i).s P.1)1213 infer_instance1214 1215end SurfaceBlowup