Lean sources / SurfaceBlowup / Recursion / Termination.lean
Termination of the 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.MemberCharts7import Mathlib.Algebra.Order.Ring.Star8import Mathlib.Data.Int.Star9import Mathlib.LinearAlgebra.Dimension.Torsion.Finite10 11/-!12# Termination of the recursion13 14Inputs for the termination step of Theorem 8.1. We construct the index map of a curve on a15concrete surface, control division charts under perturbation, attach homogeneous tangent divisors16and allowed patterns to initial forms, compute the volume of the state set of a concrete member,17build the child member at the point at infinity, and prove that the recursion terminates outside18the return and bad-exit events. We also show that order defects decrease along unramified towers19and add over products.20 21## Main results22 23* `concrete_index_map_reindexed`: the reindexed index map with cokernel length `d(d-1)/2`.24* `allowed_pattern_of_divisor`: a tangent divisor has an allowed pattern.25* `concrete_member_volume`: the volume of the state set of a concrete member.26* `child_ideal_set_map_iff_stateSet`, `infinity_point_child_member`: child members.27* `etale_type_event_eq_term`, `nonterminating_subset_return_or_bad`: termination.28* `order_defect_le_of_tower`, `order_defect_pi`: order defects.29 30Provenance: `Thm_SurfaceBlowupV2_{concrete_index_map_reindexed,31division_data_vertical_perturbation, division_quotient_basis_equiv,32divisor_affine_polynomial_normalized_factors, divisor_degree_pattern_weight,33allowed_pattern_of_divisor, equiv_of_fiber_card_eq, full_rank_free_submodule_finite_length,34global_function_of_two_chart_curve_data, has_multiplicity_initial_form,35homogeneous_divisor_of_polynomial, homogeneous_divisor_boundary_multiplicities,36ideal_atlas_reindex, concrete_member_volume, ideal_data_along_ringEquiv,37child_ideal_set_map_iff_stateSet, infinity_point_child_member, initial_form_has_tangent_divisor,38length_le_length_restrict, list_get_fiber_card_count, mem_integralClosure_pi_iff,39integralClosure_pi_equiv, generic_closure_free_of_type, nonself_cell_child_rank_lt,40etale_terminates_of_invariant, etale_type_event_eq_term, nonterminating_subset_return_or_bad,41order_defect_le_of_tower, order_defect_pi}`.42-/43 44namespace SurfaceBlowup45 46open IsLocalRing MeasureTheory47open scoped BigOperators ENNReal48 49/-! ### Index maps and division charts -/50 51/-- The index map of a curve on a concrete surface, reindexed along an enumeration `e` of the52points of its two-chart curve data: an injective `O`-algebra map from `R/(f)` into the product of53the local curve orders, with cokernel of length `d(d-1)/2`. -/54theorem concrete_index_map_reindexed (O : Type) [CommRing O] [IsDomain O]55 [IsDiscreteValuationRing O] [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)]56 (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)57 (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)58 (surfaceX O pi u a b)) (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)59 (surfaceX O pi u a b) beta) (f : ConcreteSurface O pi u a b)60 (G : GluedGenerators (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)61 beta (curveDataDegree D)) (hf : ∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b)62 (surfaceT O pi u a b) (surfaceX O pi u a b) j f = (cechInputLattice (ConcreteSurface O pi u a b)63 (surfaceT O pi u a b) (surfaceX O pi u a b) j).mkQ (gluedFunctionPair64 (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) G j))65 (hG : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional (ConcreteSurface O pi u a b)66 (surfaceT O pi u a b) (surfaceX O pi u a b))^j) (G.left j)} = leftLevelKernel D j ∧ Ideal.span67 {Ideal.Quotient.mk ((chartExceptional (ConcreteSurface O pi u a b) (surfaceX O pi u a b)68 (surfaceT O pi u a b))^j) (G.right j)} = rightLevelKernel D j) (n : ℕ) (e : Fin n ≃ AllPoints D)69 (B : Fin n → Type) [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)]70 (eB : ∀ j, B j ≃+* (localRing D (e j) ⧸ Ideal.span {localCurve D (e j)}))71 (hB : ∀ (j : Fin n) (c : O), (eB j) (algebraMap O (B j) c) = Ideal.Quotient.mk72 (Ideal.span {localCurve D (e j)}) (localFromSurface D (e j)73 (algebraMap O (ConcreteSurface O pi u a b) c))) :74 ∃ ψ : ((ConcreteSurface O pi u a b) ⧸ Ideal.span {f}) →ₐ[O] ∀ j, B j, Function.Injective ψ ∧75 Module.length O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) =76 (chooseTwo (curveDataDegree D) : ℕ∞) ∧ ∀ (r : (ConcreteSurface O pi u a b)) (j : Fin n),77 (eB j) (ψ (Ideal.Quotient.mk (Ideal.span {f}) r) j) = Ideal.Quotient.mk78 (Ideal.span {localCurve D (e j)}) (localFromSurface D (e j) r) := by79 obtain ⟨φ, hφ, hker, hlen⟩ := concrete_curve_order_index O pi hpi u a b ha beta D f G hf hG80 let _ : ∀ p : AllPoints D, Algebra O (localRing D p) := fun p =>81 ((localFromSurface D p).comp (algebraMap O (ConcreteSurface O pi u a b))).toAlgebra82 set χ := childOrderMap D with hχ83 let E : childOrder D ≃+* ∀ j, B j :=84 (RingEquiv.piCongrLeft (fun p => localRing D p ⧸ Ideal.span {localCurve D p}) e).symm.trans85 (RingEquiv.piCongrRight fun j => (eB j).symm)86 have hE : ∀ x j, E x j = (eB j).symm (x (e j)) := fun x j => rfl87 have hχapp : ∀ r p, χ r p = Ideal.Quotient.mk (Ideal.span {localCurve D p})88 (localFromSurface D p r) :=89 fun r p => rfl90 have hEalg : ∀ (c : O) (j : Fin n), E (algebraMap O (childOrder D) c) j = algebraMap O (B j)91 c := by92 intro c j93 rw [hE]94 apply (eB j).injective95 rw [RingEquiv.apply_symm_apply, hB]96 rfl97 have hsub : Ideal.span {f} ≤ RingHom.ker (E.toRingHom.comp χ) := by98 intro r hr99 rw [← hker] at hr100 simp only [RingHom.mem_ker, RingHom.comp_apply] at hr ⊢101 rw [hr, map_zero]102 let ψ₀ : ConcreteSurface O pi u a b ⧸ Ideal.span {f} →+* ∀ j, B j :=103 Ideal.Quotient.lift (Ideal.span {f}) (E.toRingHom.comp χ) (fun r hr => hsub hr)104 have hψ₀ : ∀ r, ψ₀ (Ideal.Quotient.mk _ r) = E (χ r) := fun r => rfl105 let ψ : (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) →ₐ[O] ∀ j, B j :=106 { ψ₀ with107 commutes' := by108 intro c109 change ψ₀ (Ideal.Quotient.mk _ (algebraMap O _ c)) = _110 rw [hψ₀]111 funext j112 rw [Pi.algebraMap_apply, ← hEalg]113 congr 2 }114 have hψ : ∀ r, ψ (Ideal.Quotient.mk _ r) = E (χ r) := fun r => rfl115 let L : childOrder D ≃ₗ[O] ∀ j, B j :=116 { E.toAddEquiv with117 map_smul' := by118 intro c x119 funext j120 change E (c • x) j = c • E x j121 rw [Algebra.smul_def, Algebra.smul_def, map_mul, Pi.mul_apply, hEalg] }122 have hL : ∀ x, L x = E x := fun x => rfl123 refine ⟨ψ, ?_, ?_, ?_⟩124 · intro x y hxy125 obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x126 obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y127 rw [hψ, hψ] at hxy128 rw [Ideal.Quotient.eq, ← hker, RingHom.mem_ker, map_sub, E.injective hxy, sub_self]129 · have hrange : LinearMap.range ψ.toLinearMap = (LinearMap.range φ).map L.toLinearMap := by130 ext y131 simp only [LinearMap.mem_range, Submodule.mem_map]132 constructor133 · rintro ⟨q, rfl⟩134 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective q135 exact ⟨φ r, ⟨r, rfl⟩, by rw [hφ]; rfl⟩136 · rintro ⟨_, ⟨r, rfl⟩, rfl⟩137 exact ⟨Ideal.Quotient.mk _ r, by rw [hφ]; rfl⟩138 rw [← hlen]139 exact (Submodule.Quotient.equiv _ _ L hrange.symm).symm.length_eq140 · intro r j141 rw [hψ, hE, RingEquiv.apply_symm_apply]142 rfl143 144/-- Division data survive a vertical perturbation `f ↦ f + π h` of the divisor. -/145theorem division_data_vertical_perturbation (O R : Type) [CommRing O] [CommRing R] [Algebra O R]146 (n : ℕ) (pi : O) (f : R) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))147 (hE : ∀ w, E.symm w = divisionMap f b w) [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)]148 (h : R) :149 ∃ E' : R ≃ₗ[O] ((Fin n → O) × R), ∀ w, E'.symm w = divisionMap (f + pi • h) b w := by150 set M := (Fin n → O) × R151 let r0 : M →ₗ[O] M := E.toLinearMap ∘ₗ (LinearMap.mulRight O h) ∘ₗ LinearMap.snd O (Fin n → O) R152 let rL : M →ₗ[O] M := pi • r0153 have hr : RaisesAdicOrder (Ideal.span {pi}) (rL : M → M) := by154 intro j x y hxy155 have h1 := linear_map_preserves_adic_congruence O M M (Ideal.span {pi}) r0 j x y hxy156 unfold adicCongr at h1 ⊢157 have : rL x - rL y = pi • (r0 x - r0 y) := by158 simp [rL, smul_sub]159 rw [this, pow_succ', Submodule.mul_smul]160 exact Submodule.smul_mem_smul (Ideal.mem_span_singleton_self pi) h1161 have hbij := adic_perturb_bijective O M (Ideal.span {pi}) (rL : M → M) hr162 let L : M →ₗ[O] R := E.symm.toLinearMap ∘ₗ (LinearMap.id + rL)163 have hL : ∀ w, L w = divisionMap (f + pi • h) b w := by164 intro w165 simp only [L, rL, r0, LinearMap.comp_apply, LinearMap.add_apply, LinearMap.id_apply,166 LinearMap.smul_apply, LinearEquiv.coe_coe, map_add, map_smul, LinearEquiv.symm_apply_apply,167 LinearMap.mulRight_apply]168 rw [hE]169 unfold divisionMap170 rw [add_mul, smul_mul_assoc, mul_comm h]171 abel172 have hLb : Function.Bijective L := by173 have : (L : M → R) = E.symm ∘ adicPerturb (rL : M → M) := by174 funext w; simp [L, adicPerturb]175 rw [this]176 exact E.symm.bijective.comp hbij177 refine ⟨(LinearEquiv.ofBijective L hLb).symm, fun w => ?_⟩178 rw [LinearEquiv.symm_symm, LinearEquiv.ofBijective_apply, hL]179 180/-- Division data for `f` give coordinates on `R/(f)`, inverse to the coordinate lift. -/181theorem division_quotient_basis_equiv (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)182 (f : R) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))183 (hE : ∀ w, E.symm w = divisionMap f b w) :184 ∃ EB : (R ⧸ Ideal.span {f}) ≃ₗ[O] (Fin n → O), ∀ z : Fin n → O, EB.symm z = Ideal.Quotient.mk185 (Ideal.span {f}) (coordinateLift b z) := by186 obtain ⟨EC, hEC⟩ := division_equiv_child_coordinates O R n f b E hE187 refine ⟨EC, fun z => ?_⟩188 have h : E.symm (z, 0) = coordinateLift b z := by189 rw [hE]; simp [divisionMap]190 have h2 : E (coordinateLift b z) = (z, 0) := by rw [← h]; exact E.apply_symm_apply _191 rw [LinearEquiv.symm_apply_eq, hEC, h2]192 193/-! ### Tangent divisors and allowed patterns -/194 195open scoped Classical in196/-- The affine polynomial of an exceptional divisor is monic, and the multiplicity of each affine197direction among its normalized factors is the divisor's multiplicity. -/198theorem divisor_affine_polynomial_normalized_factors (k : Type) [Field k]199 (D : ExceptionalDivisor k) :200 (divisorAffinePolynomial k D).Monic ∧ ∀ φ : AffineDirection k, Multiset.count φ.val201 (UniqueFactorizationMonoid.normalizedFactors (divisorAffinePolynomial k D)) = D (some φ) := by202 let g : ClosedDirection k → ℕ → Polynomial k := fun P r =>203 match P with | none => 1 | some phi => phi.val ^ r204 have hg : ∀ P r, (g P r).Monic := by205 intro P r206 cases P with207 | none => exact Polynomial.monic_one208 | some phi => exact phi.property.1.pow r209 have hg0 : ∀ P r, g P r ≠ 0 := fun P r => (hg P r).ne_zero210 have hprod : divisorAffinePolynomial k D = ∏ P ∈ D.support, g P (D P) := rfl211 have key : ∀ s : Finset (ClosedDirection k),212 UniqueFactorizationMonoid.normalizedFactors (∏ P ∈ s, g P (D P)) =213 ∑ P ∈ s, UniqueFactorizationMonoid.normalizedFactors (g P (D P)) := by214 intro s215 induction s using Finset.induction_on with216 | empty => simp217 | insert a s ha ih =>218 rw [Finset.prod_insert ha, Finset.sum_insert ha,219 UniqueFactorizationMonoid.normalizedFactors_mul (hg0 _ _)220 (Finset.prod_ne_zero_iff.mpr fun i _ => hg0 _ _), ih]221 have hnf : ∀ ψ : AffineDirection k, ∀ r,222 UniqueFactorizationMonoid.normalizedFactors (g (some ψ) r) = r • {ψ.val} := by223 intro ψ r224 change UniqueFactorizationMonoid.normalizedFactors (ψ.val ^ r) = _225 rw [UniqueFactorizationMonoid.normalizedFactors_pow,226 UniqueFactorizationMonoid.normalizedFactors_irreducible ψ.property.2,227 (Polynomial.Monic.normalize_eq_self ψ.property.1)]228 refine ⟨?_, ?_⟩229 · rw [hprod]230 exact Polynomial.monic_prod_of_monic _ _ fun P _ => hg _ _231 · intro φ232 rw [hprod, key, Multiset.count_sum']233 rw [Finset.sum_eq_single (some φ)]234 · rw [hnf]; simp235 · intro P _ hP236 cases P with237 | none => simp [g]238 | some ψ =>239 rw [hnf]240 have : ψ.val ≠ φ.val := fun h => hP (by rw [Subtype.val_injective h])241 simp [Ne.symm this]242 · intro h243 rw [Finsupp.notMem_support_iff.mp h]244 simp [g]245 246/-- The contact conditions of a state `s` on an exceptional divisor `Dv` of degree `d`: `d` is at247most the contact `c` (and, for a crossing state, at most the second contact `h`), and `Dv` meets the248direction at infinity (resp. the zero direction) exactly when `d < c` (resp. `d < h`). -/249abbrev DivisorContactCondition (k : Type) [Field k] (s : State) (Dv : ExceptionalDivisor k)250 (d : ℕ) : Prop :=251 match s with252 | State.single _ c => d ≤ c ∧ (0 < Dv (infinityDirection k) ↔ d < c)253 | State.crossing _ _ c h => d ≤ c ∧ (0 < Dv (infinityDirection k) ↔ d < c) ∧ d ≤ h ∧254 (0 < Dv (zeroDirection k) ↔ d < h)255 256/-- The degree of an exceptional divisor splits as its boundary multiplicities plus the weighted257count of interior points by (degree, multiplicity). -/258private theorem divisor_degree_pattern_weight (k : Type) [Field k] [Finite k] (s : State)259 (Dv : ExceptionalDivisor k) (n : ℕ) (hdeg : ∀ Q, 0 < Dv Q → directionDegree k Q ≤ n)260 (hmult : ∀ Q, Dv Q ≤ n) :261 exceptionalDegree k Dv = Dv (infinityDirection k) +262 (match s with263 | State.single _ _ => (0 : ℕ)264 | State.crossing _ _ _ _ => Dv (zeroDirection k)) +265 ∑ ij : Fin n × Fin n, (ij.1.val + 1) * (ij.2.val + 1) *266 Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧267 directionDegree k Q = ij.1.val + 1 ∧ Dv Q = ij.2.val + 1} := by268 classical269 have hpos : ∀ Q, 1 ≤ directionDegree k Q := by270 intro Q271 rcases Q with _ | φ272 · simp [directionDegree]273 · exact φ.2.2.natDegree_pos274 obtain ⟨B, hB, hBsum⟩ : ∃ B : Finset (ClosedDirection k),275 (∀ Q, Q ∈ boundaryDirections k s ↔ Q ∈ B) ∧276 ∑ Q ∈ B, directionDegree k Q * Dv Q = Dv (infinityDirection k) +277 (match s with278 | State.single _ _ => (0 : ℕ)279 | State.crossing _ _ _ _ => Dv (zeroDirection k)) := by280 cases s with281 | single _ _ =>282 exact ⟨{infinityDirection k}, fun Q => by simp [boundaryDirections],283 by simp [infinityDirection, directionDegree]⟩284 | crossing _ _ _ _ =>285 refine ⟨{infinityDirection k, zeroDirection k}, fun Q => by simp [boundaryDirections], ?_⟩286 rw [Finset.sum_pair (by simp [infinityDirection, zeroDirection])]287 simp [infinityDirection, zeroDirection, directionDegree]288 set f : ClosedDirection k → ℕ := fun Q => directionDegree k Q * Dv Q with hf289 have hdegsum : exceptionalDegree k Dv = ∑ Q ∈ Dv.support, f Q := rfl290 rw [hdegsum, ← Finset.sum_filter_add_sum_filter_not Dv.support (fun Q => Q ∈ B)]291 congr 1292 · rw [← hBsum]293 apply Finset.sum_subset294 · intro Q hQ; exact (Finset.mem_filter.1 hQ).2295 · intro Q _ hQ296 have : Dv Q = 0 := by297 by_contra h298 exact hQ (Finset.mem_filter.2 ⟨Finsupp.mem_support_iff.2 h, by assumption⟩)299 simp [f, this]300 · rcases n with _ | m301 · have : ∀ Q, Dv Q = 0 := fun Q => Nat.le_zero.1 (hmult Q)302 simp [this]303 · set g : ClosedDirection k → Fin (m+1) × Fin (m+1) :=304 fun Q => (⟨(directionDegree k Q - 1) % (m+1), Nat.mod_lt _ (Nat.succ_pos _)⟩,305 ⟨(Dv Q - 1) % (m+1), Nat.mod_lt _ (Nat.succ_pos _)⟩)306 rw [← Finset.sum_fiberwise_of_maps_to (s := Dv.support.filter (fun Q => Q ∉ B))307 (t := Finset.univ) (g := g) (fun _ _ => Finset.mem_univ _)]308 apply Finset.sum_congr rfl309 intro ij _310 have hmem : ∀ Q, Q ∈ (Dv.support.filter (fun Q => Q ∉ B)).filter (fun Q => g Q = ij) ↔311 (Q ∉ boundaryDirections k s ∧ directionDegree k Q = ij.1.val + 1 ∧ Dv Q = ij.2.val +312 1) := by313 intro Q314 simp only [Finset.mem_filter, Finsupp.mem_support_iff, hB, g, Prod.ext_iff, Fin.ext_iff]315 have h1 := hpos Q316 constructor317 · rintro ⟨⟨hne, hnb⟩, ha, hb⟩318 have hd := hdeg Q (Nat.pos_of_ne_zero hne)319 have hm := hmult Q320 rw [Nat.mod_eq_of_lt (by omega)] at ha hb321 exact ⟨hnb, by omega, by omega⟩322 · rintro ⟨hnb, ha, hb⟩323 refine ⟨⟨by omega, hnb⟩, ?_, ?_⟩324 · rw [ha, Nat.add_sub_cancel, Nat.mod_eq_of_lt ij.1.2]325 · rw [hb, Nat.add_sub_cancel, Nat.mod_eq_of_lt ij.2.2]326 rw [Nat.card_congr (Equiv.subtypeEquivRight (fun Q => (hmem Q).symm)),327 Nat.card_eq_finsetCard, Finset.sum_congr rfl (g := fun _ => (ij.1.val + 1) *328 (ij.2.val + 1)),329 Finset.sum_const, smul_eq_mul, mul_comm]330 intro Q hQ331 obtain ⟨_, ha, hb⟩ := (hmem Q).1 hQ332 simp [f, ha, hb]333 334private theorem card_le_of_weighted_sum_eq {ι : Type} [Fintype ι] (w c : ι → ℕ)335 (hw : ∀ i, 0 < w i) (e x y : ℕ) (hid : e = x + y + ∑ i, w i * c i) (i : ι) : c i ≤ e := by336 have := Finset.single_le_sum (f := fun i ↦ w i * c i) (fun _ _ ↦ Nat.zero_le _)337 (Finset.mem_univ i)338 have := Nat.le_mul_of_pos_left (c i) (hw i)339 omega340 341/-- An exceptional divisor of degree `d` satisfying the contact conditions of the state has an342allowed tangent pattern of degree `d`. -/343theorem allowed_pattern_of_divisor (k : Type) [Field k] [Finite k] (s : State) (hs : s.Valid)344 (Dv : ExceptionalDivisor k) (d : ℕ) (hd : 0 < d) (hdeg : exceptionalDegree k Dv = d)345 (hQ : ∀ Q, 0 < Dv Q → directionDegree k Q ≤ d) (hmult : ∀ Q, Dv Q ≤ d)346 (hcontact : DivisorContactCondition k s Dv d) :347 ∃ P : TangentPattern s.degree, P.d.val = d ∧ Allowed s P ∧ HasPattern k s Dv P := by348 have hdn : d ≤ s.degree := by349 revert hs hcontact350 cases s with351 | single a c =>352 rintro ⟨ha, -⟩ ⟨h1, -⟩353 change d ≤ a * c354 nlinarith355 | crossing a b c h =>356 rintro ⟨ha, -⟩ ⟨h1, -⟩357 change d ≤ a * c + b * h358 nlinarith359 have hid := divisor_degree_pattern_weight k s Dv s.degree360 (fun Q hQ' => (hQ Q hQ').trans hdn) (fun Q => (hmult Q).trans hdn)361 have hcb := card_le_of_weighted_sum_eq _ _ (fun _ ↦ by positivity) _ _ _ hid362 rw [hdeg] at hid hcb363 have hcb' : ∀ ij : Fin s.degree × Fin s.degree, Nat.card {Q : ClosedDirection k //364 Q ∉ boundaryDirections k s ∧ directionDegree k Q = ij.1.val + 1 ∧ Dv Q = ij.2.val + 1}365 ≤ s.degree := fun ij => (hcb ij).trans hdn366 clear hcb367 revert hcontact hid hcb' hdn368 cases s with369 | single a c =>370 intro hcontact hdn hid hcb371 obtain ⟨h1, h2⟩ := hcontact372 refine ⟨⟨⟨d, by omega⟩,373 ⟨Dv (infinityDirection k), by have := hmult (infinityDirection k); omega⟩,374 ⟨0, by omega⟩, fun ij => ⟨_, hcb ij |> Nat.lt_succ_of_le⟩⟩, rfl, ?_, ?_⟩375 · refine ⟨hd, ?_, h1, rfl, h2⟩376 simp only [patternWeight]377 simp only at hid378 omega379 · exact ⟨hdeg, rfl, trivial, fun ij => rfl⟩380 | crossing a b c h =>381 intro hcontact hdn hid hcb382 obtain ⟨h1, h2, h3, h4⟩ := hcontact383 refine ⟨⟨⟨d, by omega⟩,384 ⟨Dv (infinityDirection k), by have := hmult (infinityDirection k); omega⟩,385 ⟨Dv (zeroDirection k), by have := hmult (zeroDirection k); omega⟩,386 fun ij => ⟨_, hcb ij |> Nat.lt_succ_of_le⟩⟩, rfl, ?_, ?_⟩387 · refine ⟨hd, ?_, h1, h3, h2, h4⟩388 simp only [patternWeight]389 simp only at hid390 omega391 · exact ⟨hdeg, rfl, rfl, fun ij => rfl⟩392 393/-! ### Auxiliary algebra -/394 395/-- Two finite types over `γ` with fibres of equal cardinality are equivalent over `γ`. -/396theorem equiv_of_fiber_card_eq (α β γ : Type) [Finite α] [Finite β] (f : α → γ) (g : β → γ)397 (h : ∀ c : γ, Nat.card {x : α // f x = c} = Nat.card {y : β // g y = c}) :398 ∃ e : α ≃ β, ∀ x, g (e x) = f x := by399 have e : ∀ c, {x : α // f x = c} ≃ {y : β // g y = c} := fun c => by400 haveI : Fintype {x : α // f x = c} := Fintype.ofFinite _401 haveI : Fintype {y : β // g y = c} := Fintype.ofFinite _402 exact Fintype.equivOfCardEq (by simpa [Nat.card_eq_fintype_card] using h c)403 exact ⟨Equiv.ofFiberEquiv e, fun x => Equiv.ofFiberEquiv_map e x⟩404 405/-- Over a DVR with finite residue field, a free submodule of full rank in a finite free module has406quotient of finite length. -/407theorem full_rank_free_submodule_finite_length (O : Type) [CommRing O] [IsDomain O]408 [IsDiscreteValuationRing O] [Finite (ResidueField O)] (N : Type) [AddCommGroup N] [Module O N]409 [Module.Finite O N] [Module.Free O N] (M : Submodule O N) [Module.Finite O M] [Module.Free O M]410 (hrank : Module.finrank O M = Module.finrank O N) :411 Module.length O (N ⧸ M) ≠ ⊤ := by412 have hr := rank_quotient_add_rank_of_isDomain M413 rw [← Module.finrank_eq_rank, ← Module.finrank_eq_rank, ← Module.finrank_eq_rank, hrank] at hr414 norm_cast at hr415 have h0 : Module.finrank O (N ⧸ M) = 0 := by omega416 have htor : Module.IsTorsion O (N ⧸ M) := (Module.finrank_eq_zero_iff_isTorsion).mp h0417 obtain ⟨a, haI, ha0⟩ := Submodule.annihilator_top_inter_nonZeroDivisors htor418 have ha : a ≠ 0 := nonZeroDivisors.ne_zero ha0419 set I := (⊤ : Submodule O (N ⧸ M)).annihilator420 obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible O421 obtain ⟨k, u, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible ha hπ422 have hle : (maximalIdeal O) ^ k ≤ I := by423 rw [hπ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.span_singleton_le_iff_mem]424 have := I.mul_mem_left (↑u⁻¹ : O) haI425 simpa [← mul_assoc] using this426 have hQ : Finite (O ⧸ (maximalIdeal O) ^ k) := by427 apply Nat.finite_of_card_ne_zero428 rw [residue_quotient_card]429 have : Nat.card (ResidueField O) ≠ 0 := Nat.card_ne_zero.mpr ⟨inferInstance, inferInstance⟩430 exact pow_ne_zero _ this431 have hI : Finite (O ⧸ I) := Finite.of_surjective _ (Ideal.Quotient.factor_surjective hle)432 let _ := (Module.isTorsionBySet_annihilator_top O (N ⧸ M)).module433 have : Module.Finite (O ⧸ I) (N ⧸ M) := Module.Finite.of_restrictScalars_finite O _ _434 have : Finite (N ⧸ M) := Module.finite_of_finite (O ⧸ I)435 exact Module.length_ne_top436 437/-! ### Initial forms and homogeneous divisors -/438 439/-- Two-chart curve data with normalized level generators come from a global function `f` and440glued generators. -/441theorem global_function_of_two_chart_curve_data (R : Type) [CommRing R] (t x : R)442 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)443 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsLocalRing R] [IsNoetherianRing (BlowupChart R t x)]444 [IsNoetherianRing (BlowupChart R x t)] [IsAdicComplete (Ideal.span {t,x}) R]445 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t) (d : ℕ)446 (FA : ℕ → BlowupChart R t x) (hFA : ∀ j : ℕ, leftLevelKernel D j = Ideal.span447 {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j) (FA j)}) (FB : ℕ → BlowupChart R x t)448 (hFB : ∀ j : ℕ, rightLevelKernel D j = Ideal.span {Ideal.Quotient.mk449 ((Ideal.span {chartBase R x t x})^j) (FB j)}) (hnorm : ∃ u : Rˣ,450 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA 1) - algebraMap R451 (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x)^d * beta.right (FB 1)) ∈452 (Ideal.span {overlapException R t x})) :453 ∃ f : R, ∃ G : GluedGenerators R t x beta d, (∀ j : ℕ, surfaceToCechInput R t x j f =454 (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j)) ∧ ∀ j : ℕ, Ideal.span455 {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧ Ideal.span456 {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j := by457 obtain ⟨G, hG⟩ := glued_generators_of_two_chart_curve_data R t x beta D hreg hregSwap d FA hFA FB458 hFB hnorm459 obtain ⟨f, hf, _⟩ := glued_function_exists_unique R t x beta d G hreg hregSwap460 exact ⟨f, G, hf, hG⟩461 462/-- An element of exact order `d` is a degree-`d` form in `t, x` with some coefficient a unit. -/463theorem has_multiplicity_initial_form (R : Type) [CommRing R] [IsLocalRing R] (t x : R)464 (hmax : maximalIdeal R = Ideal.span {t, x}) (d : ℕ) (f : R) (hf : f ∈ (maximalIdeal R) ^ d)465 (hf' : f ∉ (maximalIdeal R) ^ (d + 1)) :466 ∃ c : Fin (d+1) → R, f = (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) ∧ ∃ i₀ : Fin (d+1), c467 i₀ ∉ maximalIdeal R := by468 rw [hmax] at hf469 obtain ⟨c, hc⟩ := monomial_span_pow R t x d f hf470 refine ⟨c, hc, ?_⟩471 by_contra hcon472 push Not at hcon473 apply hf'474 rw [hc]475 refine Ideal.sum_mem _ fun i _ => ?_476 have ht : t ∈ maximalIdeal R := hmax ▸ Ideal.subset_span (by simp)477 have hx : x ∈ maximalIdeal R := hmax ▸ Ideal.subset_span (by simp)478 have h1 : t^(d - i.val) * x^i.val ∈ (maximalIdeal R)^d := by479 have := Ideal.mul_mem_mul (Ideal.pow_mem_pow ht (d - i.val)) (Ideal.pow_mem_pow hx i.val)480 rwa [← pow_add, Nat.sub_add_cancel (by omega)] at this481 rw [mul_assoc, pow_succ']482 exact Ideal.mul_mem_mul (hcon i) h1483 484open scoped Classical in485/-- A nonzero polynomial `H` of degree at most `d` has a homogeneous divisor of degree `d`: the486point at infinity with multiplicity `d - deg H` plus the normalized factors of `H`. -/487theorem homogeneous_divisor_of_polynomial (k : Type) [Field k] (d : ℕ) (H : Polynomial k)488 (hH : H ≠ 0) (hdeg : H.natDegree ≤ d) :489 ∃ Dv : ExceptionalDivisor k, HasHomogeneousDivisor k d H Dv ∧ Dv (infinityDirection k) = d -490 H.natDegree ∧ (∀ φ : AffineDirection k, Dv (some φ) = Multiset.count φ.val491 (UniqueFactorizationMonoid.normalizedFactors H)) ∧ exceptionalDegree k Dv = d := by492 set F := UniqueFactorizationMonoid.normalizedFactors H with hF493 have hmon : ∀ ψ ∈ F, ψ.Monic := fun ψ hψ =>494 Polynomial.normalize_eq_self_iff_monic495 (UniqueFactorizationMonoid.irreducible_of_normalized_factor ψ hψ).ne_zero |>.mp496 (UniqueFactorizationMonoid.normalize_normalized_factor ψ hψ)497 have hirr : ∀ ψ ∈ F, Irreducible ψ := fun ψ hψ =>498 UniqueFactorizationMonoid.irreducible_of_normalized_factor ψ hψ499 let g : {ψ // ψ ∈ F} → ClosedDirection k := fun ψ => some ⟨ψ.1, hmon ψ.1 ψ.2, hirr ψ.1 ψ.2⟩500 let M : Multiset (ClosedDirection k) := F.attach.map g501 have hMmap : M.map (Option.map Subtype.val) = F.map some := by502 simp only [M, Multiset.map_map]503 conv_rhs => rw [← Multiset.attach_map_val F, Multiset.map_map]504 rfl505 have hMsum : Multiset.toFinsupp M = (M.map fun Q => Finsupp.single Q 1).sum := by506 induction M using Multiset.induction_on with507 | empty => simp508 | cons a s ih => rw [← Multiset.singleton_add, Multiset.toFinsupp_add, ih]; simp509 have hprod : F.prod = Polynomial.C H.leadingCoeff⁻¹ * H := by510 rw [UniqueFactorizationMonoid.prod_normalizedFactors_eq hH, normalize_apply,511 Polynomial.coe_normUnit, mul_comm]512 simp [hH]513 have hdegF : F.prod.natDegree = H.natDegree := by514 rw [hprod, Polynomial.natDegree_C_mul (inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr hH))]515 refine ⟨Finsupp.single none (d - H.natDegree) + Multiset.toFinsupp M, ⟨hH, hdeg, ?_, ?_⟩, ?_, ?_,516 ?_⟩517 · simp [M, g]518 · have key : ∀ (f : ClosedDirection k → ℕ → Polynomial k), (∀ P, f P 0 = 1) →519 (∀ P a b, f P (a + b) = f P a * f P b) → ∀ L : Multiset (Finsupp (ClosedDirection k) ℕ),520 L.sum.prod f = (L.map fun G => G.prod f).prod := by521 intro f hf0 hfa L522 induction L using Multiset.induction_on with523 | empty => simp524 | cons a s ih =>525 rw [Multiset.sum_cons, Multiset.map_cons, Multiset.prod_cons, Finsupp.prod_add_index' hf0526 hfa, ih]527 have hP : divisorAffinePolynomial k (Finsupp.single none (d - H.natDegree) + Multiset.toFinsupp528 M) = F.prod := by529 unfold divisorAffinePolynomial530 rw [Finsupp.prod_add_index' (fun P => by cases P <;> simp)531 (fun P a b => by cases P <;> simp [pow_add]),532 Finsupp.prod_single_index (by simp), hMsum,533 key _ (fun P => by cases P <;> simp) (fun P a b => by cases P <;> simp [pow_add])]534 simp only [M, Multiset.map_map, Function.comp_def]535 rw [one_mul]536 conv_rhs => rw [← Multiset.attach_map_val F]537 congr 1538 apply Multiset.map_congr rfl539 intro ψ _540 rw [Finsupp.prod_single_index (by simp [g])]541 simp [g]542 rw [hP, hprod, ← mul_assoc, ← Polynomial.C_mul,543 mul_inv_cancel₀ (Polynomial.leadingCoeff_ne_zero.mpr hH), Polynomial.C_1, one_mul]544 · simp [infinityDirection, M, g]545 · intro φ546 simp only [Finsupp.add_apply, Finsupp.single_apply, reduceCtorEq, if_false, zero_add,547 Multiset.toFinsupp_apply]548 rw [← Multiset.count_map_eq_count' (Option.map Subtype.val) M549 (Option.map_injective Subtype.val_injective), hMmap]550 exact Multiset.count_map_eq_count' _ _ (Option.some_injective _) _551 · unfold exceptionalDegree552 have h0 : ∀ P : ClosedDirection k, directionDegree k P * 0 = 0 := fun _ => mul_zero _553 have ha : ∀ (P : ClosedDirection k) (a b : ℕ),554 directionDegree k P * (a + b) = directionDegree k P * a + directionDegree k P * b :=555 fun _ _ _ => mul_add _ _ _556 rw [Finsupp.sum_add_index' h0 ha, Finsupp.sum_single_index (by simp), hMsum,557 Finsupp.multiset_sum_sum_index _ _ h0 ha]558 simp only [directionDegree, one_mul, Multiset.map_map, Function.comp_apply, mul_zero,559 Finsupp.sum_single_index, mul_one, Multiset.attach_map_val', M, g]560 rw [← Polynomial.natDegree_multiset_prod_of_monic F hmon, hdegF]561 omega562 563open scoped Classical in564/-- Boundary multiplicities of the homogeneous divisor of `H`: positive at infinity iff `H_d = 0`,565positive at zero iff `H_0 = 0`, and all multiplicities and degrees of support points at most `d`. -/566theorem homogeneous_divisor_boundary_multiplicities (k : Type) [Field k] (d : ℕ) (H : Polynomial k)(4.6)567 (hH : H ≠ 0) (hdeg : H.natDegree ≤ d) (Dv : ExceptionalDivisor k)568 (hinf : Dv (infinityDirection k) = d - H.natDegree) (haff : ∀ φ : AffineDirection k, Dv (some φ)569 = Multiset.count φ.val (UniqueFactorizationMonoid.normalizedFactors H)) :570 (0 < Dv (infinityDirection k) ↔ H.coeff d = 0) ∧ (0 < Dv (zeroDirection k) ↔ H.coeff 0 = 0) ∧571 (∀ Q : ClosedDirection k, Dv Q ≤ d) ∧ ∀ Q : ClosedDirection k, 0 < Dv Q → directionDegree k Q572 ≤ d := by573 obtain ⟨D', -, hi', ha', hd'⟩ := homogeneous_divisor_of_polynomial k d H hH hdeg574 have heq : Dv = D' := by575 ext Q576 cases Q with577 | none => exact hinf.trans hi'.symm578 | some φ => exact (haff φ).trans (ha' φ).symm579 subst heq580 have hdpos : ∀ Q : ClosedDirection k, 1 ≤ directionDegree k Q := by581 intro Q582 cases Q with583 | none => simp [directionDegree]584 | some φ => exact φ.property.2.natDegree_pos585 have hle : ∀ Q : ClosedDirection k, directionDegree k Q * Dv Q ≤ d := by586 intro Q587 by_cases h : Dv Q = 0588 · simp [h]589 · rw [← hd']590 exact Finset.single_le_sum (f := fun P => directionDegree k P * Dv P)591 (fun _ _ => Nat.zero_le _) (Finsupp.mem_support_iff.mpr h)592 refine ⟨?_, ?_, ?_, ?_⟩593 · rw [hinf]594 constructor595 · intro h596 exact Polynomial.coeff_eq_zero_of_natDegree_lt (by omega)597 · intro h598 by_contra hc599 have : H.natDegree = d := by omega600 have := Polynomial.leadingCoeff_ne_zero.mpr hH601 apply this602 rw [Polynomial.leadingCoeff]603 simpa [‹H.natDegree = d›] using h604 · have h1 : Dv (zeroDirection k) = Multiset.count Polynomial.X605 (UniqueFactorizationMonoid.normalizedFactors H) :=606 haff ⟨Polynomial.X, Polynomial.monic_X, Polynomial.irreducible_X⟩607 rw [h1, Multiset.count_pos, ← Polynomial.X_dvd_iff]608 constructor609 · exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors610 · intro h611 obtain ⟨q, hq, hass⟩ := UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd hH612 (Polynomial.irreducible_X : Irreducible (Polynomial.X : Polynomial k)) h613 have hn := UniqueFactorizationMonoid.normalize_normalized_factor q hq614 have : normalize q = normalize (Polynomial.X : Polynomial k) := normalize_eq_normalize_iff.mpr615 ⟨hass.symm.dvd, hass.dvd⟩616 rw [hn, (Polynomial.normalize_eq_self_iff_monic Polynomial.X_ne_zero).mpr Polynomial.monic_X]617 at this618 rw [← this]; exact hq619 · intro Q620 exact le_trans (Nat.le_mul_of_pos_left _ (hdpos Q)) (hle Q)621 · intro Q _622 have := hle Q623 have hp : 0 < Dv Q := ‹_›624 exact le_trans (Nat.le_mul_of_pos_right _ hp) this625 626/-! ### Atlases and volumes of concrete members -/627 628/-- Any two ideal atlases of the same set have the same residue cells, up to reindexing. -/629private theorem ideal_atlas_reindex (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (pi : O)630 (n : ℕ)631 (X : Set (Ideal R)) (A B : IdealAtlas O R pi n X) :632 ∃ e : A.ι ≃ B.ι, ∀ i, residueIdealCell (algebraMap O R pi) (A.chart i).f = residueIdealCell633 (algebraMap O R pi) (B.chart (e i)).f := by634 have self_mem : ∀ p f : R, Ideal.span {f} ∈ residueIdealCell p f := by635 intro p f636 refine ⟨⟨f, rfl⟩, ?_⟩637 rw [Ideal.map_span]; simp638 have eq_of_mem : ∀ p f g : R, ∀ J, J ∈ residueIdealCell p f → J ∈ residueIdealCell p g →639 residueIdealCell p f = residueIdealCell p g := by640 intro p f g J hf hg641 have h : Ideal.span {Ideal.Quotient.mk (Ideal.span {p}) f} = Ideal.span642 {Ideal.Quotient.mk (Ideal.span {p}) g} := hf.2.symm.trans hg.2643 ext K644 simp only [residueIdealCell, Set.mem_ofPred_eq, h]645 have ex : ∀ i, ∃ j, Ideal.span {(A.chart i).f} ∈ residueIdealCell (algebraMap O R pi)646 (B.chart j).f := by647 intro i648 have : Ideal.span {(A.chart i).f} ∈ X :=649 (Set.ext_iff.1 A.cover _).2 (Set.mem_iUnion.2 ⟨i, self_mem _ _⟩)650 exact Set.mem_iUnion.1 ((Set.ext_iff.1 B.cover _).1 this)651 choose e he using ex652 have hcell : ∀ i, residueIdealCell (algebraMap O R pi) (A.chart i).f = residueIdealCell653 (algebraMap O R pi) (B.chart (e i)).f :=654 fun i => eq_of_mem _ _ _ _ (self_mem _ _) (he i)655 have inj : Function.Injective e := by656 intro i i' h657 by_contra hne658 have h1 : Disjoint (residueIdealCell (algebraMap O R pi) (A.chart i).f)659 (residueIdealCell (algebraMap O R pi) (A.chart i').f) := A.disjoint hne660 have h2 : residueIdealCell (algebraMap O R pi) (A.chart i).f = residueIdealCell661 (algebraMap O R pi) (A.chart i').f := by662 rw [hcell i, hcell i', h]663 rw [h2] at h1664 exact Set.disjoint_left.1 h1 (self_mem _ _) (self_mem _ _)665 have surj : Function.Surjective e := by666 intro j667 have : Ideal.span {(B.chart j).f} ∈ X :=668 (Set.ext_iff.1 B.cover _).2 (Set.mem_iUnion.2 ⟨j, self_mem _ _⟩)669 obtain ⟨i, hi⟩ := Set.mem_iUnion.1 ((Set.ext_iff.1 A.cover _).1 this)670 refine ⟨i, ?_⟩671 by_contra hne672 have h1 : Disjoint (residueIdealCell (algebraMap O R pi) (B.chart (e i)).f)673 (residueIdealCell (algebraMap O R pi) (B.chart j).f) := B.disjoint fun h ↦ hne h674 have h2 := eq_of_mem _ _ _ _ hi (self_mem _ _)675 have h3 : residueIdealCell (algebraMap O R pi) (B.chart (e i)).f = residueIdealCell676 (algebraMap O R pi) (B.chart j).f := by677 rw [← hcell i, h2]678 rw [h3] at h1679 exact Set.disjoint_left.1 h1 (self_mem _ _) (self_mem _ _)680 exact ⟨Equiv.ofBijective e ⟨inj, surj⟩, hcell⟩681 682/-- Transport of a state-measure computation between two atlases of the same set, the first one683built on a parameter `p` propositionally equal to `pi`. -/684private theorem stateMeasure_univ_of_atlas (O R : Type) [CommRing O] [IsDomain O]685 [IsDiscreteValuationRing O] [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)]686 [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]687 [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]688 (htop : IsAdic (maximalIdeal O)) [CommRing R] [Algebra O R] [IsDomain R] [IsLocalRing R]689 (p pi : O) (hp : p = pi) (hpi : Irreducible pi) (hp0 : algebraMap O R pi ≠ 0)690 (hpm : algebraMap O R pi ∈ maximalIdeal R) (n : ℕ) (X : Set (Ideal R))691 [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (A : IdealAtlas O R p n X)692 (A' : IdealAtlas O R pi n X) (V : ℝ≥0∞)693 (hA' : (letI := idealChartSigma O R pi694 stateMeasure O R pi n (Nat.card (ResidueField O)) A' Set.univ = V)) :695 letI := idealChartSigma O R p696 stateMeasure O R p n (Nat.card (ResidueField O)) A Set.univ = V := by697 subst hp698 let _ := idealChartSigma O R p699 obtain ⟨e, he⟩ := ideal_atlas_reindex O R p n X A A'700 rwa [state_measure_atlas_independent O R htop p hpi n X A A' (fun j ↦701 coordinate_ideal_measurable_chart_sigma O htop R p hpi hp0 hpm n _ _702 (A'.chart j).isDivisionChart) e he hp0 hpm]703 704/-- The state measure of the state set of a concrete member is the state volume density. -/705theorem concrete_member_volume (m : ConcreteMember) :706 m.toMeasured.μ m.toMeasured.stateSet = densityValue (stateVolume m.s) m.toMeasured.q := by707 rw [← Set.univ_inter m.toMeasured.stateSet, ← (concrete_member_measure_finite_support m).2]708 obtain ⟨O, htop, pi, hpi, u, a0, b0, ha, S, hS_pi, hS_t, hS_x, hS_a, hS_b, s, shape, atlas⟩ := m709 have hq : 2 ≤ Nat.card (ResidueField O) := Finite.one_lt_card_iff_nontrivial.2 inferInstance710 cases s with711 | single a c =>712 obtain ⟨rfl, rfl, hc⟩ := shape713 obtain ⟨e, he⟩ := concrete_surface_special_fiber_equiv O pi hpi u a 0714 obtain ⟨A', hA'⟩ := concrete_single_state_volume O pi hpi u a ha S hS_pi hS_t hS_a hS_b e he c715 hc htop716 obtain ⟨hp0, hpm⟩ := surface_vertical_parameter O (ConcreteSurface O pi u a 0) S717 rw [hS_pi] at hp0 hpm718 have := division_coordinate_module_isAdicComplete O pi hpi u a 0 ha (a*c)719 refine (stateMeasure_univ_of_atlas O _ htop S.pi pi hS_pi hpi hp0 hpm (a*c) _ atlas A'720 _ hA').trans ?_721 exact (density_value_arith _ hq (.const 1) (.const 1) (by simp [Expr.eval])722 (by simp [Expr.eval]) c (State.single 1 1) ⟨Nat.one_pos, Nat.one_pos⟩).2.2.1.symm723 | crossing a b c h =>724 obtain ⟨rfl, rfl, hb, hc, hh⟩ := shape725 obtain ⟨e, he⟩ := concrete_surface_special_fiber_equiv O pi hpi u a b726 obtain ⟨A', hA'⟩ := concrete_crossing_state_volume O pi hpi u a b ha hb S hS_pi hS_t hS_x hS_a727 hS_b e he c h hc hh htop728 obtain ⟨hp0, hpm⟩ := surface_vertical_parameter O (ConcreteSurface O pi u a b) S729 rw [hS_pi] at hp0 hpm730 have := division_coordinate_module_isAdicComplete O pi hpi u a b ha (a*c+b*h)731 refine (stateMeasure_univ_of_atlas O _ htop S.pi pi hS_pi hpi hp0 hpm (a*c+b*h) _732 atlas A' _ hA').trans ?_733 have hq1 : (1 : ℚ) ≤ (Nat.card (ResidueField O) : ℚ) := by exact_mod_cast (by omega)734 have hdv := density_value_arith _ hq eminusOne (.inv (.pow .var (c+h)))735 (by simp [eminusOne, Expr.sub, Expr.neg, Expr.eval]; linarith)736 (by simp only [Expr.eval, expression_pow_eval]; positivity) (c+h) (State.single 1 1)737 ⟨Nat.one_pos, Nat.one_pos⟩738 have hem : densityValue eminusOne (Nat.card (ResidueField O)) =739 (Nat.card (ResidueField O) : ℝ≥0∞) - 1 := by740 simp only [densityValue, eminusOne, Expr.sub, Expr.neg, Expr.eval]741 push_cast742 rw [show ((Nat.card (ResidueField O) : ℝ) + -1 * 1) =743 (Nat.card (ResidueField O) : ℝ) - 1 by ring,744 ENNReal.ofReal_sub _ zero_le_one, ENNReal.ofReal_natCast, ENNReal.ofReal_one]745 change _ = densityValue (stateVolume (.crossing a b c h)) (Nat.card (ResidueField O))746 rw [stateVolume, hdv.1, hdv.2.2.1, hem]747 748/-! ### Child members -/749 750/-- Principality and contact lengths of ideals are transported by ring isomorphisms. -/751private theorem ideal_data_along_ringEquiv (S S' : Type) [CommRing S] [CommRing S'] (Eq : S ≃+* S')752 (I : Ideal S) (e : S) :753 ((∃ g : S, I = Ideal.span {g}) ↔ ∃ g' : S', Ideal.map (Eq : S →+* S') I = Ideal.span {g'}) ∧754 Module.length S (S ⧸ (I ⊔ Ideal.span {e})) = Module.length S'755 (S' ⧸ (Ideal.map (Eq : S →+* S') I ⊔ Ideal.span {Eq e})) := by756 refine ⟨⟨?_, ?_⟩, ?_⟩757 · rintro ⟨g, rfl⟩758 exact ⟨Eq g, by rw [Ideal.map_span]; simp⟩759 · rintro ⟨g', h⟩760 refine ⟨Eq.symm g', ?_⟩761 have := congrArg (Ideal.map (Eq.symm : S' →+* S)) h762 rw [Ideal.map_span] at this763 simp only [Set.image_singleton] at this764 change I = Ideal.span {(Eq.symm : S' →+* S) g'}765 rw [← this, Ideal.map_map]766 have : (Eq.symm : S' →+* S).comp (Eq : S →+* S') = RingHom.id S := by ext; simp767 rw [this, Ideal.map_id]768 · rw [module_length_quotient_ringEquiv S S' Eq (I ⊔ Ideal.span {e}), Ideal.map_sup,769 Ideal.map_span]770 rw [Set.image_singleton]771 rfl772 773/-- An ideal of the completed local ring at the point of a child lies in the child ideal set iff774its image in the child member lies in the child's state set. -/775theorem child_ideal_set_map_iff_stateSet (m : ConcreteMember) (c : m.cellIndex)776 (D : CellChildData m c) (j : m.toMeasured.childIdx c) (I : Ideal777 (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j))) :778 I ∈ childIdealSet m.R m.S.t m.S.x D.e c.2.1 D.hinf m.s (m.toMeasured.cellDegree c) (D.point j) ↔779 Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) →+*780 (D.mc j).R) I ∈ (D.mc j).toMeasured.stateSet := by781 have hE := ideal_data_along_ringEquiv _ _ (D.Eq j) I782 (divisorException m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j))783 have hB := (ideal_data_along_ringEquiv _ _ (D.Eq j) I784 (divisorBoundary m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j))).2785 rw [D.hEq_e j] at hE786 have hB' : (D.asg.pt j = infinityDirection (ResidueField m.R) ∨ D.asg.pt j = zeroDirection787 (ResidueField m.R)) →788 Module.length (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j))789 (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) ⧸790 (I ⊔ Ideal.span {divisorBoundary m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j)})) =791 idealContact (D.mc j).R (Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1792 D.hinf (D.point j) →+* (D.mc j).R) I) (D.mc j).S.x := by793 intro h; rw [hB, D.hEq_b j h]; rfl794 obtain ⟨hP, hE⟩ := hE795 have hs : (D.mc j).s = pointChildState (ResidueField m.R) m.s (m.toMeasured.cellDegree c) c.2.1796 (D.asg.pt j) :=797 (D.child j).hstate.trans (D.asg.state j)798 have hshape := (D.mc j).shape799 have hvalid := (D.mc j).shape.valid (D.mc j).ha800 have hSa := (D.mc j).hS_a801 have hSb := (D.mc j).hS_b802 change _ ↔ _ ∈ surfaceStateSet (D.mc j).O (D.mc j).R (D.mc j).S (D.mc j).s803 unfold childIdealSet surfaceStateSet804 simp only [Set.mem_ofPred_eq]805 change _ = idealContact (D.mc j).R _ (D.mc j).S.t at hE806 rw [hP, hE]807 have hQ : (D.point j).val = D.asg.pt j := rfl808 rw [hQ, hs]809 rw [hs] at hshape hvalid810 generalize idealContact (D.mc j).R (Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1811 D.hinf (D.point j) →+* (D.mc j).R) I) (D.mc j).S.t = CT at *812 generalize idealContact (D.mc j).R (Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1813 D.hinf (D.point j) →+* (D.mc j).R) I) (D.mc j).S.x = CX at *814 generalize Module.length (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j))815 (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) ⧸816 (I ⊔ Ideal.span {divisorBoundary m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j)})) = LB at *817 generalize (∃ g', Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf818 (D.point j) →+* (D.mc j).R) I = Ideal.span {g'}) = PP at *819 rw [hSa, hSb]820 clear hB hE hP hs821 generalize D.asg.pt j = Q at *822 generalize m.toMeasured.cellDegree c = d at *823 simp only [hvalid, true_and]824 clear hvalid hSa hSb hQ I825 generalize c.2.1 = Dv at *826 generalize m.s = s0 at *827 generalize (D.mc j).a = A at *828 generalize (D.mc j).b = B at *829 rcases Q with _ | φ830 · obtain rfl := hB' (Or.inl rfl)831 cases s0 <;>832 · simp only [pointChildState, infinityDirection, if_true, StateShape, stateContactT,833 stateContactX] at hshape ⊢834 obtain ⟨rfl, rfl, -⟩ := hshape835 simp [zeroDirection]836 have hne : (some φ : ClosedDirection (ResidueField m.R)) ≠ infinityDirection _ := by837 simp [infinityDirection]838 cases s0 with839 | single a0 c0 =>840 simp only [pointChildState, if_neg hne, StateShape, stateContactT, stateContactX] at hshape ⊢841 obtain ⟨rfl, rfl, -⟩ := hshape842 simp843 | crossing a0 b0 c0 h0 =>844 by_cases hz : (some φ : ClosedDirection (ResidueField m.R)) = zeroDirection _845 · obtain rfl := hB' (Or.inr hz)846 simp only [pointChildState, if_neg hne, if_pos hz, StateShape, stateContactT,847 stateContactX] at hshape ⊢848 obtain ⟨rfl, rfl, -⟩ := hshape849 simp [hz, zeroDirection]850 · simp only [pointChildState, if_neg hne, if_neg hz, StateShape, stateContactT,851 stateContactX] at hshape ⊢852 obtain ⟨rfl, rfl, -⟩ := hshape853 simp [hz]854 855/-- The completed local ring at the point at infinity of a concrete surface is a concrete member856of shape `(a + b, a)` over the same coefficient ring, with the expected boundary parameters. -/857theorem infinity_point_child_member (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]858 [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]859 [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]860 [MeasurableSpace O] [BorelSpace O] (htop : IsAdic (maximalIdeal O)) (pi : O)861 (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)862 [hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)863 (surfaceX O pi u a b)).IsPrime] (s' : State) (hs' : StateShape (a + b) a s') :864 ∃ mc : ConcreteMember, ∃ (_ : Algebra O mc.O) (_ : Module.Finite O mc.O)865 (_ : Module.Free O mc.O), Module.finrank O mc.O = 1 ∧ Nat.card (ResidueField mc.O) = Nat.card866 (ResidueField O) ^ 1 ∧ mc.pi = algebraMap O mc.O pi ∧ mc.a = a + b ∧ mc.b = a ∧ mc.s = s' ∧867 (∃ pc : mc.O ≃ₗ[O] (Fin 1 → O), Continuous pc ∧ Continuous pc.symm ∧ Measurable pc ∧868 Measurable pc.symm ∧ IsProbabilityMeasure (Measure.map pc.symm (coefficientMeasure O 1)) ∧ ∀ r869 : ℕ, coefficientMeasure mc.O r = Measure.pi (fun _ : Fin r => Measure.map pc.symm870 (coefficientMeasure O 1))) ∧ ∃ Eq : CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b)871 (surfaceX O pi u a b) (surfaceT O pi u a b)) (infinityPoint (ConcreteSurface O pi u a b)872 (surfaceT O pi u a b) (surfaceX O pi u a b)) ≃+* mc.R, Eq873 ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b)874 (surfaceT O pi u a b)) (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)875 (surfaceX O pi u a b))) ((chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b)876 (surfaceT O pi u a b)) (surfaceX O pi u a b))) = mc.S.t ∧ Eq877 ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b)878 (surfaceT O pi u a b)) (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)879 (surfaceX O pi u a b))) (chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b)880 (surfaceT O pi u a b))) = mc.S.x ∧ ∀ c : O, Eq ((completedPointMap881 (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))882 (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)))883 ((chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))884 (algebraMap O (ConcreteSurface O pi u a b) c))) = algebraMap O mc.R c := by885 obtain ⟨Eq, h1, h2, h3⟩ := x_chart_infinity_completion_equiv O pi hpi u a b ha886 (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) rfl887 obtain ⟨i1, i2, S, hSpi, hSt, hSx, hSa, hSb, ⟨atlas⟩⟩ :=888 concrete_member_data_exists O pi hpi (xSubstUnit O u) (a + b) a (by omega) s' hs'889 have := coefficient_measure_probability O htop 1890 obtain ⟨-, hm2, hm3, hm4, hm5, hm6⟩ := coefficient_measure_pi_one O htop pi hpi 0891 refine ⟨⟨O, htop, pi, hpi, xSubstUnit O u, a + b, a, by omega, S, hSpi, hSt, hSx, hSa, hSb, s',892 hs', atlas⟩, Algebra.id O, Module.Finite.self O, Module.Free.self O, Module.finrank_self O,893 by simp, by simp, rfl, rfl, rfl,894 ⟨(LinearEquiv.funUnique (Fin 1) O O).symm, hm4, hm3, hm6, hm5, by simpa using hm2,895 fun r ↦ by simpa using (coefficient_measure_pi_one O htop pi hpi r).1⟩,896 Eq, ?_, by simpa [hSx] using h2, fun c ↦ by simpa using h3 c⟩897 have := h1 (axisX O)898 rw [(chartSubst_apply_generators O 0).2.2.2.2.2.1] at this899 simpa [hSt, surfaceT, surfaceX] using this900 901/-- A homogeneous divisor of the initial form of `f` is a tangent divisor of `(f)`. -/902theorem initial_form_has_tangent_divisor (O R : Type) [CommRing O] [IsDomain O](4.6)903 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]904 (S : SurfaceData O R) (d : ℕ) (f : R) (c : Fin (d + 1) → R)905 (hc : f = (∑ i : Fin (d + 1), c i * S.t ^ (d - i.val) * S.x ^ i.val))906 (H : Polynomial (ResidueField R)) (hH : H = ∑ i : Fin (d + 1), Polynomial.C (residue R (c i)) *907 Polynomial.X ^ i.val) (Dv : ExceptionalDivisor (ResidueField R))908 (hDv : HasHomogeneousDivisor (ResidueField R) d H Dv) :909 HasTangentDivisor O R S (Ideal.span {f}) d Dv := by910 refine ⟨f, H, rfl, hDv, ?_⟩911 have hco : ∀ i : Fin (d+1), H.coeff i.val = residue R (c i) := by912 intro i913 rw [hH, Polynomial.finsetSum_coeff]914 simp only [Polynomial.coeff_C_mul_X_pow]915 rw [Finset.sum_eq_single i]916 · simp917 · intro j _ hj918 have : i.val ≠ j.val := fun h => hj (Fin.ext h.symm)919 simp [this]920 · simp921 unfold tangentLift922 rw [hc]923 refine initial_form_lift_independent O R S d c924 (fun i => residueRepresentative R (H.coeff i.val)) fun i ↦ ?_925 rw [← IsLocalRing.residue_eq_zero_iff, map_sub, hco i]926 have : residue R (residueRepresentative R (residue R (c i))) = residue R (c i) :=927 Function.rightInverse_invFun IsLocalRing.residue_surjective _928 rw [this, sub_self]929 930/-! ### Lengths, fibres and integral closures -/931 932/-- Restricting scalars along `O → Oδ` does not decrease length. -/933private theorem length_le_length_restrict (O Oδ M : Type) [CommRing O] [CommRing Oδ] [Algebra O Oδ]934 [AddCommGroup M] [Module O M] [Module Oδ M] [IsScalarTower O Oδ M] :935 Module.length Oδ M ≤ Module.length O M := by936 have h := Submodule.length_le_length_restrictScalars O (⊤ : Submodule Oδ M)937 rw [Submodule.restrictScalars_top] at h938 rwa [(Submodule.topEquiv (R := Oδ) (M := M)).length_eq,939 (Submodule.topEquiv (R := O) (M := M)).length_eq] at h940 941/-- The number of positions of a list holding `v` is the count of `v`. -/942theorem list_get_fiber_card_count (β : Type) [DecidableEq β] (l : List β) (v : β) :943 Nat.card {j : Fin l.length // l.get j = v} = l.count v := by944 have key : ∀ l : List β, l.count v = ∑ j : Fin l.length, if l.get j = v then 1 else 0 := by945 intro l946 induction l with947 | nil => simp948 | cons a l ih =>949 rw [List.count_cons, ih]950 erw [Fin.sum_univ_succ]951 by_cases h : a = v <;> simp [h, Nat.add_comm]952 rw [Nat.card_eq_fintype_card, Fintype.card_subtype, Finset.card_filter, key]953 954/-- An element of a finite product is integral iff each coordinate is integral. -/955private theorem mem_integralClosure_pi_iff (O : Type) [CommRing O] (ι : Type) [Finite ι]956 (C : ι → Type)957 [∀ i, CommRing (C i)] [∀ i, Algebra O (C i)] (x : ∀ i, C i) :958 x ∈ integralClosure O (∀ i, C i) ↔ ∀ i, x i ∈ integralClosure O (C i) := by959 have := Fintype.ofFinite ι960 simp only [mem_integralClosure_iff]961 constructor962 · intro h i963 exact h.map (Pi.evalAlgHom O C i)964 · intro h965 choose p hp hx using h966 refine ⟨∏ i, p i, Polynomial.monic_prod_of_monic _ _ (fun i _ => hp i), ?_⟩967 have h1 : Polynomial.aeval x (∏ j, p j) = 0 := by968 funext i969 have : Polynomial.aeval x (∏ j, p j) = ∏ j, Polynomial.aeval x (p j) := map_prod _ _ _970 rw [this, Finset.prod_apply]971 apply Finset.prod_eq_zero (Finset.mem_univ i)972 have := Polynomial.aeval_algHom_apply (Pi.evalAlgHom O C i) x (p i)973 simp only [Pi.evalAlgHom_apply] at this974 rw [← this, Polynomial.aeval_def]975 exact hx i976 rwa [Polynomial.aeval_def] at h1977 978/-- The integral closure in a finite product is the product of the integral closures. -/979private theorem integralClosure_pi_equiv (O : Type) [CommRing O] (ι : Type) [Finite ι]980 (C : ι → Type)981 [∀ i, CommRing (C i)] [∀ i, Algebra O (C i)] :982 ∃ e : integralClosure O (∀ i, C i) ≃ₗ[O] (∀ i, integralClosure O (C i)), ∀983 (x : integralClosure O (∀ i, C i)) (i : ι), ((e x i : integralClosure O (C i)) : C i) =984 (x : ∀ i, C i) i := by985 refine ⟨{ toFun := fun x i => ⟨(x : ∀ i, C i) i, (mem_integralClosure_pi_iff O ι C x.1).1 x.2 i⟩986 map_add' := fun x y => rfl987 map_smul' := fun r x => rfl988 invFun := fun y => ⟨fun i => (y i : C i), (mem_integralClosure_pi_iff O ι C _).2989 (fun i => (y i).2)⟩990 left_inv := fun x => rfl991 right_inv := fun y => rfl }, fun x i => rfl⟩992 993/-- If `B` has an algebra type, its generic closure is finite free of rank the generic rank. -/994theorem generic_closure_free_of_type (O : Type) [CommRing O] [IsDomain O]995 [IsDiscreteValuationRing O] (B : Type) [CommRing B] [Algebra O B] (σ : FactorType)996 (h : HasAlgebraType O B σ) :997 Module.Finite O (GenericClosure O B) ∧ Module.Free O (GenericClosure O B) ∧ Module.finrank O998 (GenericClosure O B) = Module.finrank (BaseField O) (TensorProduct O (BaseField O) B) := by999 obtain ⟨ι, _, L, _, _, _, _, _, e, -, hsepL⟩ := h1000 have : ∀ i, Module.Finite O (integralClosure O (L i)) := hsepL1001 have hL := fun i => integral_closure_finite_free O (BaseField O) (L i)1002 have : ∀ i, Module.Finite O (integralClosure O (L i)) := fun i => (hL i).11003 have : ∀ i, Module.Free O (integralClosure O (L i)) := fun i => (hL i).2.11004 obtain ⟨e₁, -⟩ := integralClosure_pi_equiv O ι L1005 obtain ⟨φ, -⟩ := integral_closure_algEquiv O _ _ (e.restrictScalars O)1006 let E : GenericClosure O B ≃ₗ[O] (∀ i, integralClosure O (L i)) :=1007 φ.toLinearEquiv.trans e₁1008 refine ⟨Module.Finite.equiv E.symm, Module.Free.of_equiv E.symm, ?_⟩1009 rw [E.finrank_eq, Module.finrank_pi_fintype, e.toLinearEquiv.finrank_eq,1010 Module.finrank_pi_fintype]1011 exact Finset.sum_congr rfl fun i _ => (hL i).2.21012 1013/-! ### Termination of the recursion -/1014 1015/-- Children of a non-self cell have strictly smaller state rank. -/1016private theorem nonself_cell_child_rank_lt (U : SurfaceUniverse) (i : U.ι) (c : (U.M i).cellIndex)1017 (hc : ¬ (U.M i).IsSelfCell c) (j : (U.M i).childIdx c) :1018 (U.M (U.child i c j)).s.rank < (U.M i).s.rank := by1019 rw [U.child_state]1020 exact nonself_child_rank_lt _ (U.M i).valid _ c.1.2 hc _1021 (List.get_mem _ _)1022 1023/-- If types propagate to children and an invariant `δ` is non-increasing along the recursion and1024strictly decreasing on self cells, every ideal with a type terminates. -/1025private theorem etale_terminates_of_invariant (U : SurfaceUniverse) (hE1 : U.ChildTypesExist)1026 (δ : ∀ i : U.ι, Ideal (U.M i).R → ℕ) (hE2 : U.InvariantDecreases δ) (i : U.ι)1027 (J : Ideal (U.M i).R) (hJ : J ∈ (U.M i).stateSet) (σ : FactorType)1028 (hσ : HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ) :1029 U.Terminates i J := by1030 have key : ∀ n r : ℕ, ∀ (i : U.ι) (J : Ideal (U.M i).R), δ i J = n → (U.M i).s.rank = r →1031 J ∈ (U.M i).stateSet → (∃ σ, HasAlgebraType (U.M i).O ((U.M i).R ⧸ J) σ) →1032 U.Terminates i J := by1033 intro n1034 induction n using Nat.strong_induction_on with1035 | _ n IHδ =>1036 intro r1037 induction r using Nat.strong_induction_on with1038 | _ r IHr =>1039 intro i J hn hr hJ ⟨σ, hσ⟩1040 cases ht : (U.M i).s.terminal with1041 | true => exact SurfaceUniverse.Terminates.leaf i J hJ ht1042 | false =>1043 rw [U.cells_cover i ht, Set.mem_iUnion] at hJ1044 obtain ⟨c, hc⟩ := hJ1045 refine SurfaceUniverse.Terminates.node i c J hc ht (fun j => ?_)1046 have hτ := hE1 i ht c J hc σ hσ j1047 have hmem := cell_child_mem_stateSet U i ht c J hc j1048 have hδ := hE2 i ht c J hc ⟨σ, hσ⟩ j1049 by_cases hself : (U.M i).IsSelfCell c1050 · exact IHδ _ (hn ▸ hδ.2 hself) _ _ _ rfl rfl hmem hτ1051 · have hrank := nonself_cell_child_rank_lt U i c hself j1052 rcases lt_or_eq_of_le hδ.1 with h | h1053 · exact IHδ _ (hn ▸ h) _ _ _ rfl rfl hmem hτ1054 · exact IHr _ (hr ▸ hrank) _ _ (h.trans hn) rfl hmem hτ1055 exact key _ _ i J rfl rfl hJ ⟨σ, hσ⟩1056 1057/-- Under the hypotheses of `etale_terminates_of_invariant`, the type events consist of1058terminating ideals. -/1059theorem etale_type_event_eq_term (U : SurfaceUniverse) (hE1 : U.ChildTypesExist)1060 (δ : ∀ i : U.ι, Ideal (U.M i).R → ℕ) (hE2 : U.InvariantDecreases δ) (i : U.ι) (σ : FactorType) :1061 U.typeEvent i σ = U.termTypeEvent i σ :=1062 Set.Subset.antisymm (fun J hJ ↦ ⟨hJ, etale_terminates_of_invariant U hE1 δ hE2 i J hJ.1 σ hJ.2⟩)1063 Set.inter_subset_left1064 1065private theorem childList_of_isSelfCell (U : SurfaceUniverse) (i : U.ι) (c : (U.M i).cellIndex)1066 (hc : (U.M i).IsSelfCell c) : (U.M i).childList c = [(1, (U.M i).s)] := by1067 obtain ⟨_, _, _, h⟩ := hc1068 exact h1069 1070private theorem child_state_of_isSelfCell (U : SurfaceUniverse) (i : U.ι) (c : (U.M i).cellIndex)1071 (hc : (U.M i).IsSelfCell c) (j : (U.M i).childIdx c) :1072 (U.M (U.child i c j)).s = (U.M i).s := by1073 rw [U.child_state]1074 have h := childList_of_isSelfCell U i c hc1075 unfold MeasuredSurface.childState1076 have : ∀ (L : List (ℕ × State)) (hL : L = [(1, (U.M i).s)]) (j : Fin L.length), (L.get j).2 =1077 (U.M i).s := by1078 intro L hL j1079 subst hL1080 have hj := j.21081 simp only [List.length_cons, List.length_nil] at hj1082 have : j = ⟨0, by simp⟩ := Fin.ext (by simp only; omega)1083 subst this; rfl1084 exact this _ h j1085 1086private theorem childIdx_subsingleton_of_isSelfCell (U : SurfaceUniverse) (i : U.ι)1087 (c : (U.M i).cellIndex)1088 (hc : (U.M i).IsSelfCell c) (j j' : (U.M i).childIdx c) : j = j' := by1089 have hl : ((U.M i).childList c).length = 1 := by rw [childList_of_isSelfCell U i c hc]; rfl1090 exact Fin.ext (by have := j.2; have := j'.2; omega)1091 1092private theorem exists_child_mem_nonterminatingSet (U : SurfaceUniverse) (i : U.ι)1093 (hnt : (U.M i).s.terminal = false)1094 (c : (U.M i).cellIndex) (J : Ideal (U.M i).R) (hJc : J ∈ (U.M i).cell c)1095 (hJ : J ∉ U.terminatingSet i) : ∃ j, U.Φ i c J j ∈ U.nonterminatingSet (U.child i c j) := by1096 by_contra hcon1097 push Not at hcon1098 refine hJ (SurfaceUniverse.Terminates.node i c J hJc hnt fun j ↦ ?_)1099 by_contra h1100 exact hcon j ⟨cell_child_mem_stateSet U i hnt c J hJc j, h⟩1101 1102private theorem mem_returnEvent_succ_or_badExitEvent (U : SurfaceUniverse) (k : ℕ) : ∀ (i : U.ι),1103 (U.M i).s.terminal = false →1104 ∀ J, J ∈ U.nonterminatingSet i → J ∈ U.returnEvent k i →1105 J ∈ U.returnEvent (k+1) i ∪ U.badExitEvent k i := by1106 induction k with1107 | zero =>1108 intro i hnt J hJ _1109 have hJs := hJ.11110 rw [U.cells_cover i hnt, Set.mem_iUnion] at hJs1111 obtain ⟨c, hJc⟩ := hJs1112 have hmem := (U.Φ_bij i hnt c).mapsTo hJc1113 rw [Set.mem_univ_pi] at hmem1114 by_cases hc : (U.M i).IsSelfCell c1115 · left1116 simp only [SurfaceUniverse.returnEvent, Set.mem_iUnion]1117 exact ⟨⟨c, hc⟩, hJc, Set.mem_univ_pi.2 hmem⟩1118 · right1119 obtain ⟨j₀, hj₀⟩ := exists_child_mem_nonterminatingSet U i hnt c J hJc hJ.21120 simp only [SurfaceUniverse.badExitEvent, Set.mem_iUnion]1121 refine ⟨⟨c, hc⟩, j₀, hJc, Set.mem_univ_pi.2 (fun j => ?_)⟩1122 by_cases hj : j = j₀1123 · subst hj; simp [hj₀]1124 · simp [Function.update_of_ne hj]1125 | succ k ih =>1126 intro i hnt J hJ hJr1127 simp only [SurfaceUniverse.returnEvent, Set.mem_iUnion] at hJr1128 obtain ⟨⟨c, hc⟩, hJc, hJpi⟩ := hJr1129 rw [Set.mem_preimage, Set.mem_univ_pi] at hJpi1130 obtain ⟨j₀, hj₀⟩ := exists_child_mem_nonterminatingSet U i hnt c J hJc hJ.21131 have hnt' : (U.M (U.child i c j₀)).s.terminal = false := by1132 rw [child_state_of_isSelfCell U i c hc]; exact hnt1133 rcases ih _ hnt' _ hj₀ (hJpi j₀) with h | h1134 · left1135 simp only [SurfaceUniverse.returnEvent, Set.mem_iUnion]1136 refine ⟨⟨c, hc⟩, hJc, Set.mem_univ_pi.2 (fun j => ?_)⟩1137 obtain rfl := childIdx_subsingleton_of_isSelfCell U i c hc j j₀1138 simpa [SurfaceUniverse.returnEvent] using h1139 · right1140 simp only [SurfaceUniverse.badExitEvent, Set.mem_iUnion]1141 refine ⟨⟨c, hc⟩, hJc, Set.mem_univ_pi.2 (fun j => ?_)⟩1142 obtain rfl := childIdx_subsingleton_of_isSelfCell U i c hc j j₀1143 exact h1144 1145/-- A nonterminating ideal either returns infinitely often or eventually exits through a bad1146cell; in a crossing state it exits through a bad cell at once. -/1147theorem nonterminating_subset_return_or_bad (U : SurfaceUniverse) (i : U.ι)Proof of Theorem 6.21148 (hnt : (U.M i).s.terminal = false) :1149 (∀ a c : ℕ, (U.M i).s = State.single a c → U.nonterminatingSet i ⊆ (⋂ k, U.returnEvent k i) ∪ ⋃1150 k, U.badExitEvent k i) ∧ (∀ a b c h : ℕ, (U.M i).s = State.crossing a b c h →1151 U.nonterminatingSet i ⊆ U.badExitEvent 0 i) := by1152 classical1153 constructor1154 · intro a c _ J hJ1155 by_cases hall : J ∈ ⋂ k, U.returnEvent k i1156 · exact Or.inl hall1157 · right1158 rw [Set.mem_iInter] at hall1159 push Not at hall1160 have hex : ∃ n, J ∉ U.returnEvent n i := hall1161 have hn0 : Nat.find hex ≠ 0 := fun h0 ↦ (h0 ▸ Nat.find_spec hex) hJ.11162 obtain ⟨m, hm⟩ := Nat.exists_eq_succ_of_ne_zero hn01163 have hin : J ∈ U.returnEvent m i := by1164 by_contra hc1165 have := Nat.find_min' hex hc1166 omega1167 have hnot : J ∉ U.returnEvent (m+1) i := by1168 rw [← Nat.succ_eq_add_one, ← hm]; exact Nat.find_spec hex1169 rcases mem_returnEvent_succ_or_badExitEvent U m i hnt J hJ hin with h | h1170 · exact absurd h hnot1171 · exact Set.mem_iUnion.2 ⟨m, h⟩1172 · intro a b c h hs J hJ1173 rcases mem_returnEvent_succ_or_badExitEvent U 0 i hnt J hJ hJ.1 with h' | h'1174 · exfalso1175 simp only [SurfaceUniverse.returnEvent, Set.mem_iUnion] at h'1176 obtain ⟨⟨c', ⟨a', c'', hs', _⟩⟩, _⟩ := h'1177 rw [hs] at hs'1178 cases hs'1179 · exact h'1180 1181/-! ### Order defects -/1182 1183open scoped TensorProduct in1184/-- The order defect does not increase under an unramified extension of the coefficient DVR. -/1185theorem order_defect_le_of_tower (O Oδ : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1186 [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ] [Algebra O Oδ] [Module.Finite O Oδ]1187 [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ) (pi : O) (hpi : Irreducible pi)1188 (hpiδ : Irreducible (algebraMap O Oδ pi)) (B : Type) [CommRing B] [Algebra O B] [Algebra Oδ B]1189 [IsScalarTower O Oδ B] :1190 orderDefect Oδ B ≤ orderDefect O B := by1191 obtain ⟨-, -, hfr⟩ := unramified_fraction_base_change O Oδ δ hrank pi hpi hpiδ1192 -- fraction field of Oδ as Oδ ⊗[O] K1193 have hfr' : IsFractionRing Oδ (Oδ ⊗[O] BaseField O) := by1194 let _i : Algebra Oδ (BaseField O ⊗[O] Oδ) := Algebra.TensorProduct.rightAlgebra1195 refine IsLocalization.isLocalization_of_algEquiv (nonZeroDivisors Oδ)1196 (AlgEquiv.ofRingEquiv (f := (Algebra.TensorProduct.comm O (BaseField O) Oδ).toRingEquiv) ?_)1197 intro x1198 change (Algebra.TensorProduct.comm O (BaseField O) Oδ) (1 ⊗ₜ x) = _1199 simp1200 let ψ : BaseField Oδ ≃ₐ[Oδ] Oδ ⊗[O] BaseField O :=1201 IsLocalization.algEquiv (nonZeroDivisors Oδ) (BaseField Oδ) (Oδ ⊗[O] BaseField O)1202 let Θ : BaseField Oδ ⊗[Oδ] B ≃+* BaseField O ⊗[O] B :=1203 ((((Algebra.TensorProduct.congr ψ (AlgEquiv.refl (R := Oδ) (A₁ := B))).trans1204 (Algebra.TensorProduct.comm Oδ _ B)).trans1205 (Algebra.TensorProduct.cancelBaseChange O Oδ Oδ B (BaseField O))).toRingEquiv.trans1206 (Algebra.TensorProduct.comm O B (BaseField O)).toRingEquiv)1207 have hΘ : ∀ b : B, Θ (1 ⊗ₜ b) = 1 ⊗ₜ b := by1208 intro b1209 simp [Θ, Algebra.TensorProduct.one_def]1210 let f : Oδ →+* BaseField O ⊗[O] B :=1211 (Algebra.TensorProduct.includeRight : B →ₐ[O] BaseField O ⊗[O] B).toRingHom.comp1212 (algebraMap Oδ B)1213 let alg : Algebra Oδ (BaseField O ⊗[O] B) := f.toAlgebra1214 have hf : ∀ o, Θ (algebraMap Oδ (BaseField Oδ ⊗[Oδ] B) o) = algebraMap Oδ (BaseField O ⊗[O] B)1215 o := by1216 intro o1217 rw [Algebra.TensorProduct.algebraMap_apply', hΘ]1218 rfl1219 have : IsScalarTower O Oδ (BaseField O ⊗[O] B) := IsScalarTower.of_algebraMap_eq (fun a => by1220 change _ = (1 : BaseField O) ⊗ₜ algebraMap Oδ B (algebraMap O Oδ a)1221 rw [Algebra.TensorProduct.algebraMap_apply', ← IsScalarTower.algebraMap_apply])1222 let Θa : BaseField Oδ ⊗[Oδ] B ≃ₐ[Oδ] BaseField O ⊗[O] B := AlgEquiv.ofRingEquiv (f := Θ) hf1223 have : Algebra.IsIntegral O Oδ := Algebra.IsIntegral.of_finite O Oδ1224 have hint : ∀ z, IsIntegral Oδ z ↔ IsIntegral O (Θ z) := by1225 intro z1226 rw [← isIntegral_algEquiv Θa]1227 exact ⟨fun h => isIntegral_trans _ h, fun h => h.tower_top⟩1228 let : Module O (GenericClosure Oδ B) := Module.compHom _ (algebraMap O Oδ)1229 have : IsScalarTower O Oδ (GenericClosure Oδ B) := ⟨fun a b x => by1230 change (a • b) • x = (algebraMap O Oδ a) • (b • x)1231 rw [Algebra.smul_def a b, mul_smul]⟩1232 let θ : GenericClosure Oδ B ≃ₗ[O] GenericClosure O B :=1233 { toFun := fun z => (⟨Θ (z : ↥(integralClosure Oδ (BaseField Oδ ⊗[Oδ] B))).1,1234 (hint _).1 (z : ↥(integralClosure Oδ (BaseField Oδ ⊗[Oδ] B))).2⟩ :1235 ↥(integralClosure O (BaseField O ⊗[O] B)))1236 invFun := fun w => (⟨Θ.symm (w : ↥(integralClosure O (BaseField O ⊗[O] B))).1,1237 (hint _).2 (by simpa [mem_integralClosure_iff] using1238 (w : ↥(integralClosure O (BaseField O ⊗[O] B))).2)⟩ :1239 ↥(integralClosure Oδ (BaseField Oδ ⊗[Oδ] B)))1240 map_add' := fun z w => Subtype.ext (map_add Θ _ _)1241 map_smul' := fun a z => by1242 apply Subtype.ext1243 change Θ (algebraMap O Oδ a • (z : ↥(integralClosure Oδ (BaseField Oδ ⊗[Oδ] B))).1) = a • _1244 rw [← algebraMap_smul Oδ a (Θ _)]1245 exact map_smul Θa _ _1246 left_inv := fun z => Subtype.ext (Θ.symm_apply_apply _)1247 right_inv := fun w => Subtype.ext (Θ.apply_symm_apply _) }1248 have hmap : ((orderImage Oδ B).restrictScalars O).map (θ : GenericClosure Oδ B →ₗ[O]1249 GenericClosure O B)1250 = orderImage O B := by1251 rw [Submodule.map_equiv_eq_comap_symm]1252 ext w1253 change Θ.symm (w : ↥(integralClosure O (BaseField O ⊗[O] B))).1 ∈ LinearMap.range _ ↔1254 (w : ↥(integralClosure O (BaseField O ⊗[O] B))).1 ∈ LinearMap.range _1255 constructor1256 · rintro ⟨b, hb⟩1257 refine ⟨b, ?_⟩1258 have := congrArg Θ hb1259 simp only [RingEquiv.apply_symm_apply] at this1260 rw [← this]1261 exact (hΘ b).symm1262 · rintro ⟨b, hb⟩1263 refine ⟨b, ?_⟩1264 change (1 : BaseField Oδ) ⊗ₜ b = _1265 rw [← Θ.symm_apply_apply ((1 : BaseField Oδ) ⊗ₜ b), hΘ]1266 exact congrArg Θ.symm hb1267 calc orderDefect Oδ B = Module.length Oδ (GenericClosure Oδ B ⧸ orderImage Oδ B) := rfl1268 _ ≤ Module.length O (GenericClosure Oδ B ⧸ orderImage Oδ B) :=1269 length_le_length_restrict O Oδ _1270 _ = Module.length O (GenericClosure Oδ B ⧸ (orderImage Oδ B).restrictScalars O) :=1271 (Submodule.Quotient.restrictScalarsEquiv O (orderImage Oδ B)).length_eq.symm1272 _ = orderDefect O B := (Submodule.Quotient.equiv _ _ θ hmap).length_eq1273 1274/-- The order defect of a finite product is the sum of the order defects. -/1275theorem order_defect_pi (O : Type) [CommRing O] [IsDomain O] (n : ℕ) (B : Fin n → Type)1276 [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)] :1277 orderDefect O (∀ j, B j) = ∑ j, orderDefect O (B j) := by1278 let K := BaseField O1279 let p : TensorProduct O K (∀ j, B j) ≃ₐ[O] ∀ j, TensorProduct O K (B j) :=1280 (Algebra.TensorProduct.piRight O K K B).restrictScalars O1281 obtain ⟨φ, hφ⟩ := integral_closure_algEquiv O _ _ p1282 obtain ⟨e₁, he₁⟩ := integralClosure_pi_equiv O (Fin n) (fun j => TensorProduct O K (B j))1283 let E : GenericClosure O (∀ j, B j) ≃ₗ[O] ∀ j, GenericClosure O (B j) :=1284 φ.toLinearEquiv.trans e₁1285 have hE : ∀ (x : GenericClosure O (∀ j, B j)) (j : Fin n),1286 genericClosureVal O (B j) (E x j) = p (genericClosureVal O (∀ j, B j) x) j := by1287 intro x j1288 have := he₁ (φ x) j1289 rwa [hφ x] at this1290 have hmap : (orderImage O (∀ j, B j)).map E.toLinearMap1291 = Submodule.pi Set.univ (fun j => orderImage O (B j)) := by1292 have hmem : ∀ (C : Type) [CommRing C] [Algebra O C] (z : GenericClosure O C),1293 z ∈ orderImage O C ↔ ∃ c : C, (1 : K) ⊗ₜ[O] c = genericClosureVal O C z := by1294 intro C _ _ z1295 simp [orderImage, Submodule.mem_comap, LinearMap.mem_range,1296 K]1297 ext y1298 simp only [Submodule.mem_map, Submodule.mem_pi, Set.mem_univ, true_implies]1299 constructor1300 · rintro ⟨x, hx, rfl⟩ j1301 obtain ⟨b, hb⟩ := (hmem _ x).1 hx1302 refine (hmem _ _).2 ⟨b j, ?_⟩1303 rw [show (E.toLinearMap x) j = E x j from rfl, hE, ← hb]1304 rfl1305 · intro hy1306 choose b hb using fun j => (hmem _ (y j)).1 (hy j)1307 refine ⟨E.symm y, (hmem _ _).2 ⟨b, ?_⟩, by simp⟩1308 apply p.injective1309 funext j1310 rw [← hE, LinearEquiv.apply_symm_apply, ← hb j]1311 rfl1312 unfold orderDefect1313 rw [(Submodule.Quotient.equiv _ _ E hmap).length_eq, (Submodule.quotientPi _).length_eq,1314 Module.length_pi_of_fintype]1315 1316end SurfaceBlowup