Lean sources / SurfaceBlowup / Blowup / CurveOrders.lean
Curve orders, the exceptional line, and finitely supported local data
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.Formula.FiniteFieldCounts7import SurfaceBlowup.Formula.RationalEval8import SurfaceBlowup.Measure.AdicTransport9import SurfaceBlowup.Unramified.LocalDescent10import SurfaceBlowup.Unramified.PolynomialTypes11 12/-!13# Curve orders, the exceptional line, and finitely supported local data14 15Results about the blow-up charts of `Charts.lean`: curve ideals and curve sections on the two16charts and their inverse limit; glued function pairs; the exceptional line as `k[Z]` and the17overlap level as `k[Z, Z⁻¹]`; and the Chinese-remainder description of finitely supported local18data at finitely many maximal ideals.19 20The adic-perturbation and cylinder-measure API now lives in `Measure/AdicTransport.lean`, the21finite-field counts in `Formula/FiniteFieldCounts.lean`, and the rational evaluation of the22universal expressions in `Formula/RationalEval.lean`; this file imports them so that its23downstream modules see them unchanged.24 25## Main results26 27* `curve_ideal_lattice_eq_kernels`: curve ideals are the kernels of the finitely supported data.28* `curve_quotient_complete_equiv_threads`: `S/(g) ≅ lim S/(g, e^j)` for complete local `S`.29* `exceptional_line_equiv_residue_field`, `exceptional_overlap_is_laurent_line`: the exceptional30 line and its overlap.31* `homogeneous_form_not_mem_pow_succ`: forms with a unit coefficient have exact order `d`.32* `finite_support_quotient_equiv`, `finite_curve_support_kernel_saturated`: finitely supported33 local data.34* `division_equiv_child_coordinates`, `ideal_contact_generator`: miscellaneous.35 36Provenance: `Thm_SurfaceBlowupV2_{curve_ideal_lattice_eq_kernels, curve_ideal_lattice_le_sections,37curve_lattices_antitone, curve_limit_level_map_exists, curve_quotient_complete_equiv_threads,38curve_sections_quot_reduction_exists, directionPoint_properties, distinct_maximal_powers_coprime,39division_equiv_child_coordinates, exceptional_chart_is_affine_line,40exceptional_line_equiv_chart_exceptional, exceptional_line_equiv_residue_field,41exceptional_overlap_is_laurent_line, finite_curve_exceptional_annihilator,42finite_support_localization_recovers, finite_support_completion_recovers,43finite_support_quotient_surjective, finite_support_kernels_compatible,44finite_support_level_kernels_compatible, finite_support_generators_compatible,45finite_support_quotient_equiv, glued_function_left_chart, glued_function_pair_closed,46glued_function_pair_compatible, glued_function_right_chart, glued_generators_level_one,47homogeneous_form_not_mem_pow_succ, ideal_contact_generator,48kernel_saturation_from_top_layer_annihilators, finite_curve_support_kernel_saturated,49laurent_isUnit_iff_monomial}`.50-/51 52namespace SurfaceBlowup53 54/-! ### Curve orders on the two charts -/55 56/-- If `(g) + I` and `K ⊇ I` have the same image modulo `I`, then `(g) + I = K`. -/57private theorem span_sup_eq_of_map_eq {A : Type} [CommRing A] (I K : Ideal A) (g : A)58 (h : Ideal.span {Ideal.Quotient.mk I g} = K.map (Ideal.Quotient.mk I)) (hIK : I ≤ K) :59 Ideal.span {g} ⊔ I = K := by60 have h1 : Ideal.span {Ideal.Quotient.mk I g} = (Ideal.span {g}).map (Ideal.Quotient.mk I) := by61 rw [Ideal.map_span, Set.image_singleton]62 have h2 := congrArg (Ideal.comap (Ideal.Quotient.mk I)) h63 rw [h1, Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,64 Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective] at h265 have hk : Ideal.comap (Ideal.Quotient.mk I) ⊥ = I := Ideal.mk_ker66 rwa [hk, sup_eq_left.mpr hIK] at h267 68/-- If the glued generators generate the level kernels of the curve data, then the curve ideals69on the two charts are the kernels of the finitely supported local data. -/70theorem curve_ideal_lattice_eq_kernels (R : Type) [CommRing R] (t x : R)71 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]72 [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x)73 (D : TwoChartCurveData R t x beta) (d : ℕ) (G : GluedGenerators R t x beta d)74 (hG : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} =75 leftLevelKernel D j ∧ Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} =76 rightLevelKernel D j) (j : ℕ) :77 leftCurveIdeal R t x beta G j = leftKernel D j ∧ rightCurveIdeal R t x beta G j = rightKernel D78 j := by79 have key : ∀ (A : Type) [CommRing A] (ι : Type) (P : ι → Ideal A) [∀ i, (P i).IsPrime]80 (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (e : A) (g : ∀ i, CompletedLocalAt A (P i)),81 (∀ i, J i = finiteLocalCurveIdeal A (P i) e (g i) j) →82 e ^ j ∈ finiteSupportKernel A ι P J := by83 intro A _ ι P _ J e g hJ84 unfold finiteSupportKernel85 rw [Submodule.mem_iInf]86 intro i87 rw [Ideal.mem_comap, hJ i, map_pow]88 exact Ideal.subset_span (by simp)89 have hl : (chartExceptional R t x) ^ j ≤ leftKernel D j := by90 rw [chartExceptional, Ideal.span_singleton_pow, Ideal.span_singleton_le_iff_mem]91 exact key _ _ _ _ _ (fun s => leftData D s) (fun _ => rfl)92 have hr : (chartExceptional R x t) ^ j ≤ rightKernel D j := by93 rw [chartExceptional, Ideal.span_singleton_pow, Ideal.span_singleton_le_iff_mem]94 exact key _ _ _ _ _ (fun s => rightData D s) (fun _ => rfl)95 exact ⟨span_sup_eq_of_map_eq _ _ _ (by rw [(hG j).1]; rfl) hl,96 span_sup_eq_of_map_eq _ _ _ (by rw [(hG j).2]; rfl) hr⟩97 98/-- Every pair in the curve ideal lattice is a curve section. -/99theorem curve_ideal_lattice_le_sections (R : Type) [CommRing R] (t x : R)100 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ) :101 curveIdealLattice R t x beta G j ≤ curveSections R t x beta G j := by102 have hrel := blowup_chart_relation R t x103 set I := overlapCurveIdeal R t x beta G j104 set alg := algebraMap (BlowupChart R t x) (BlowupOverlap R t x)105 have hE : (Ideal.span {overlapException R t x})^j ≤ I := le_sup_right106 have hL : Ideal.map alg (leftCurveIdeal R t x beta G j) ≤ I := by107 rw [leftCurveIdeal, Ideal.map_sup, Ideal.map_span, Set.image_singleton, chartExceptional,108 Ideal.map_pow, Ideal.map_span, Set.image_singleton]109 exact sup_le le_sup_left hE110 have hbx : beta.right (chartBase R x t x) = overlapException R t x * overlapSlope R t x := by111 have h1 : beta.right (chartBase R x t x) = algebraMap R (BlowupOverlap R t x) x :=112 beta.right.commutes x113 rw [h1, overlapException, overlapSlope, ← map_mul, hrel, IsScalarTower.algebraMap_apply R114 (BlowupChart R t x) (BlowupOverlap R t x)]115 rfl116 have hR : Ideal.map beta.right.toRingHom (rightCurveIdeal R t x beta G j) ≤ I := by117 rw [rightCurveIdeal, Ideal.map_sup, Ideal.map_span, Set.image_singleton, chartExceptional,118 Ideal.map_pow, Ideal.map_span, Set.image_singleton]119 refine sup_le ?_ ?_120 · rw [Ideal.span_le, Set.singleton_subset_iff]121 have hu : IsUnit ((overlapSlope R t x)^d) :=122 (IsLocalization.Away.algebraMap_isUnit (chartSlope R t x)).pow d123 have h2 : (overlapSlope R t x)^d * beta.right (G.right j) ∈ I := by124 have h3 := hE (G.overlap j)125 have h4 : alg (G.left j) ∈ I :=126 (le_sup_left : Ideal.span _ ≤ I) (Ideal.subset_span rfl)127 simpa [alg] using I.sub_mem h4 h3128 obtain ⟨u, hu⟩ := hu129 have := I.mul_mem_left (↑u⁻¹) h2130 rwa [← hu, ← mul_assoc, Units.inv_mul, one_mul] at this131 · refine le_trans (Ideal.pow_right_mono ?_ j) hE132 rw [Ideal.span_le, Set.singleton_subset_iff]133 change beta.right (chartBase R x t x) ∈ _134 rw [hbx]135 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)136 rintro ⟨a, b⟩ ⟨ha, hb⟩137 change alg a - (IsLocalization.Away.invSelf (chartSlope R t x))^0 * beta.right b ∈ I138 rw [pow_zero, one_mul]139 exact I.sub_mem (hL (Ideal.mem_map_of_mem _ ha)) (hR (Ideal.mem_map_of_mem _ hb))140 141/-- The curve ideal lattices and the curve sections decrease with the level. -/142theorem curve_lattices_antitone (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x)143 (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ) :144 curveIdealLattice R t x beta G (j+1) ≤ curveIdealLattice R t x beta G j ∧ curveSections R t x145 beta G (j+1) ≤ curveSections R t x beta G j := by146 have key : ∀ (S : Type) [CommRing S] (s : S) (a b : S) (k : ℕ),147 a - b ∈ (Ideal.span {s})^k →148 Ideal.span {a} ⊔ (Ideal.span {s})^(k+1) ≤ Ideal.span {b} ⊔ (Ideal.span {s})^k := by149 intro S _ s a b k h150 refine sup_le ?_ (le_sup_of_le_right (Ideal.pow_le_pow_right (Nat.le_succ k)))151 rw [Ideal.span_singleton_le_iff_mem]152 rw [← add_sub_cancel b a]153 exact Ideal.add_mem _ (Ideal.mem_sup_left (Ideal.subset_span rfl)) (Ideal.mem_sup_right h)154 have hL : leftCurveIdeal R t x beta G (j+1) ≤ leftCurveIdeal R t x beta G j :=155 key _ _ _ _ _ (G.left_compat j)156 have hR : rightCurveIdeal R t x beta G (j+1) ≤ rightCurveIdeal R t x beta G j :=157 key _ _ _ _ _ (G.right_compat j)158 refine ⟨Submodule.prod_mono hL hR, ?_⟩159 have hO : overlapCurveIdeal R t x beta G (j+1) ≤ overlapCurveIdeal R t x beta G j := by160 apply key161 have h := G.left_compat j162 unfold chartExceptional at h163 rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton'] at h164 obtain ⟨c, hc⟩ := h165 rw [← map_sub, ← hc, map_mul, map_pow]166 have hm : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t) ∈167 Ideal.span {overlapException R t x} := Ideal.subset_span rfl168 exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_pow hm j)169 exact Submodule.comap_mono hO170 171/-- The curve order limit maps to each level of the curve sections, compatibly with threads. -/172theorem curve_limit_level_map_exists (R : Type) [CommRing R] (t x : R)173 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ) :174 ∃ π : CurveOrderLimit R t x beta G →ₗ[R] curveSectionsQuot R t x beta G j, ∀ p : curveThreads R175 t x beta G, ((π (curveLimitMk R t x beta G p) : curveSectionsQuot R t x beta G j) :176 (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G j) =177 (curveIdealLattice R t x beta G j).mkQ (p.val j) := by178 let g : curveThreads R t x beta G →ₗ[R] (BlowupChart R t x × BlowupChart R x t) ⧸179 curveIdealLattice R t x beta G j :=180 (curveIdealLattice R t x beta G j).mkQ ∘ₗ (LinearMap.proj j) ∘ₗ181 (curveThreads R t x beta G).subtype182 have hg : ∀ p, g p ∈ curveSectionsQuot R t x beta G j := by183 intro p184 have h := (Submodule.mem_inf.mp p.2).1185 exact ⟨p.val j, (Submodule.mem_pi.mp h) j (Set.mem_univ _), rfl⟩186 let g' := LinearMap.codRestrict (curveSectionsQuot R t x beta G j) g hg187 have hk : curveNullThreads R t x beta G ≤ LinearMap.ker g' := by188 intro p hp189 have : p.val j ∈ curveIdealLattice R t x beta G j := (Submodule.mem_pi.mp hp) j (Set.mem_univ _)190 rw [LinearMap.mem_ker]191 exact Subtype.ext ((Submodule.Quotient.mk_eq_zero _).mpr this)192 exact ⟨(curveNullThreads R t x beta G).liftQ g' hk, fun _ => rfl⟩193 194/-- Reduction maps between consecutive levels of the curve sections modulo the curve lattices. -/195theorem curve_sections_quot_reduction_exists (R : Type) [CommRing R] (t x : R)196 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ) :197 ∃ ρ : curveSectionsQuot R t x beta G (j+1) →ₗ[R] curveSectionsQuot R t x beta G j, ∀ q :198 curveSectionsQuot R t x beta G (j+1), ∀ p : BlowupChart R t x × BlowupChart R x t,199 (q : (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G (j+1)) =200 (curveIdealLattice R t x beta G (j+1)).mkQ p → ((ρ q : curveSectionsQuot R t x beta G j) :201 (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G j) =202 (curveIdealLattice R t x beta G j).mkQ p := by203 obtain ⟨h1, h2⟩ := curve_lattices_antitone R t x beta d G j204 let m := Submodule.mapQ (curveIdealLattice R t x beta G (j+1)) (curveIdealLattice R t x beta G j)205 LinearMap.id206 (by simpa using h1)207 have hm : ∀ p, m ((curveIdealLattice R t x beta G (j+1)).mkQ p) =208 (curveIdealLattice R t x beta G j).mkQ p :=209 fun p => by simp [m]210 have hmap : ∀ q ∈ curveSectionsQuot R t x beta G (j+1), m q ∈ curveSectionsQuot R t x beta G j :=211 by212 intro q hq213 obtain ⟨p, hp, rfl⟩ := hq214 rw [show (curveIdealLattice R t x beta G (j+1)).mkQ p = _ from rfl, hm]215 exact ⟨p, h2 hp, rfl⟩216 refine ⟨m.restrict hmap, fun q p hp => ?_⟩217 change m (q : _) = _218 rw [hp, hm]219 220/-- For a complete Noetherian local ring `S` and `e` in its maximal ideal, `S/(g)` is the221inverse limit of the quotients `S/(g, e^j)`. -/222theorem curve_quotient_complete_equiv_threads (S : Type) [CommRing S] [IsLocalRing S]223 [IsNoetherianRing S] [IsAdicComplete (IsLocalRing.maximalIdeal S) S] (e g : S)224 (he : e ∈ IsLocalRing.maximalIdeal S) :225 ∃ E : (S ⧸ Ideal.span {g}) ≃ {u : ∀ j : ℕ, S ⧸ Ideal.span {g, e^j} // ∀ j, levelReduction e g j226 (u (j+1)) = u j}, ∀ s : S, ∀ j : ℕ, (E (Ideal.Quotient.mk (Ideal.span {g}) s)).val j =227 Ideal.Quotient.mk (Ideal.span {g, e^j}) s := by228 have hle : ∀ j : ℕ, Ideal.span {g} ≤ Ideal.span {g, e^j} := fun j =>229 Ideal.span_mono (by simp)230 have hIne : Ideal.span {e} ≠ ⊤ := by231 rw [Ne, Ideal.span_singleton_eq_top]232 exact (IsLocalRing.mem_maximalIdeal e).mp he233 have hpow : ∀ j : ℕ, ((Ideal.span {e}) ^ j • (⊤ : Submodule S S)) = Ideal.span {e ^ j} :=234 fun j ↦ by rw [smul_eq_mul, Ideal.mul_top, Ideal.span_singleton_pow]235 have hpair : ∀ j : ℕ, Ideal.span {g, e^j} = Ideal.span {g} ⊔ Ideal.span {e} ^ j :=236 fun j ↦ by rw [Ideal.span_singleton_pow, Ideal.span_insert]237 let F : S ⧸ Ideal.span {g} → {u : ∀ j : ℕ, S ⧸ Ideal.span {g, e^j} // ∀ j, levelReduction e g j238 (u (j+1)) = u j} :=239 fun q => ⟨fun j => Ideal.Quotient.factor (hle j) q, by240 intro j241 induction q using Quotient.inductionOn' with242 | h s => rfl⟩243 have hF : ∀ s j, (F (Ideal.Quotient.mk _ s)).val j = Ideal.Quotient.mk (Ideal.span {g, e^j}) s :=244 fun s j => rfl245 have hbij : Function.Bijective F := by246 constructor247 · intro q₁ q₂ h248 obtain ⟨s₁, rfl⟩ := Ideal.Quotient.mk_surjective q₁249 obtain ⟨s₂, rfl⟩ := Ideal.Quotient.mk_surjective q₂250 rw [Ideal.Quotient.eq, ← iInf_sup_pow_eq_of_isLocalRing S (Ideal.span {e}) (Ideal.span {g})251 hIne, Ideal.mem_iInf]252 exact fun j ↦ hpair j ▸ Ideal.Quotient.eq.mp (congrArg (fun u ↦ u.val j) h)253 · intro u254 choose s hs using fun j => Ideal.Quotient.mk_surjective (u.val j)255 have hdiff : ∀ j, s (j+1) - s j ∈ Ideal.span {g, e^j} := by256 intro j257 rw [← Ideal.Quotient.eq]258 have := u.property j259 rwa [← hs (j+1), ← hs j] at this260 choose a b hab using fun j => Ideal.mem_span_pair.mp (hdiff j)261 let t : ℕ → S := fun j => s j - ∑ i ∈ Finset.range j, a i * g262 have ht : ∀ j, t j ≡ t (j+1) [SMOD ((Ideal.span {e}) ^ j • (⊤ : Submodule S S))] := by263 intro j264 rw [SModEq.sub_mem, hpow]265 have : t j - t (j+1) = -(b j) * e ^ j := by266 simp only [t, Finset.sum_range_succ]267 linear_combination hab j268 rw [this]269 exact Ideal.mul_mem_left _ _ (Ideal.mem_span_singleton_self _)270 obtain ⟨L, hL⟩ := IsPrecomplete.prec271 (isAdicComplete_of_isAdicComplete_maximalIdeal S _ hIne).toIsPrecomplete272 ((AdicCompletion.isAdicCauchy_iff (Ideal.span {e}) S t).mpr ht)273 refine ⟨Ideal.Quotient.mk _ L, Subtype.ext <| funext fun j ↦ ?_⟩274 rw [hF, ← hs j, Ideal.Quotient.eq]275 have h1 : L - t j ∈ Ideal.span {e ^ j} := by276 rw [← hpow]; exact (SModEq.sub_mem.mp (hL j).symm)277 have h2 : L - s j = (L - t j) + (-(∑ i ∈ Finset.range j, a i) * g) := by278 simp only [t]; rw [neg_mul, Finset.sum_mul]; ring279 rw [h2]280 exact Ideal.add_mem _ (Ideal.span_mono (by simp) h1)281 (Ideal.mul_mem_left _ _ (Ideal.subset_span (by simp)))282 exact ⟨Equiv.ofBijective F hbij, fun s j => rfl⟩283 284/-! ### Glued functions -/285 286/-- A surface function lifting the glued pair agrees with it on the `t`-chart modulo `(t)^j`. -/287theorem glued_function_left_chart (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x)288 (d : ℕ) (G : GluedGenerators R t x beta d) (f : R) (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =289 (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j)) (j : ℕ) :290 algebraMap R (BlowupChart R t x) f - (chartBase R t x t)^d * G.left j ∈291 (chartExceptional R t x)^j := by292 have h := hf j293 simp only [surfaceToCechInput, LinearMap.comp_apply, Submodule.mkQ_apply] at h294 exact (Submodule.Quotient.eq _).mp h |>.1295 296/-- A surface function lifting the glued pair agrees with it on the `x`-chart modulo `(x)^j`. -/297theorem glued_function_right_chart (R : Type) [CommRing R] (t x : R)298 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) (f : R)299 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ300 (gluedFunctionPair R t x G j)) (j : ℕ) :301 algebraMap R (BlowupChart R x t) f - (chartBase R x t x)^d * G.right j ∈302 (chartExceptional R x t)^j := by303 have h := hf j304 simp only [surfaceToCechInput, LinearMap.comp_apply, Submodule.mkQ_apply] at h305 exact (Submodule.Quotient.eq _).mp h |>.2306 307/-- The glued function pair is closed under the untwisted level Čech differential. -/308theorem glued_function_pair_closed (R : Type) [CommRing R] (t x : R)309 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ)310 (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap311 (fullCechDifferential R t x beta 0)) :312 finiteCechDifferential R t x beta 0 j h ((cechInputLattice R t x j).mkQ313 (gluedFunctionPair R t x G j)) = 0 := by314 unfold finiteCechDifferential315 rw [Submodule.mkQ_apply, Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero]316 have hx : beta.right (chartBase R x t x) = overlapException R t x * overlapSlope R t x := by317 have h1 : chartBase R x t x = algebraMap R (BlowupChart R x t) x := rfl318 rw [h1, AlgHom.commutes, IsScalarTower.algebraMap_apply R (BlowupChart R t x),319 overlapException, overlapSlope, ← map_mul, blowup_chart_relation]320 rfl321 have key : fullCechDifferential R t x beta 0 (gluedFunctionPair R t x G j) =322 overlapException R t x ^ d *323 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (G.left j) -324 (overlapSlope R t x)^d * beta.right (G.right j)) := by325 simp only [fullCechDifferential, ringCechDifferential, gluedFunctionPair, LinearMap.coe_mk,326 AddHom.coe_mk, pow_zero, one_mul, map_mul, map_pow, hx, IsScalarTower.coe_toAlgHom']327 simp only [overlapException]328 ring329 rw [key]330 change _ ∈ (Ideal.span {overlapException R t x})^j331 exact Ideal.mul_mem_left _ _ (G.overlap j)332 333/-- The glued function pairs form a compatible thread. -/334theorem glued_function_pair_compatible (R : Type) [CommRing R] (t x : R)335 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) (j : ℕ) :336 cechInputReduction R t x j ((cechInputLattice R t x (j+1)).mkQ337 (gluedFunctionPair R t x G (j+1))) = (cechInputLattice R t x j).mkQ338 (gluedFunctionPair R t x G j) := by339 change Submodule.Quotient.mk (gluedFunctionPair R t x G (j+1)) =340 Submodule.Quotient.mk (p := cechInputLattice R t x j) (gluedFunctionPair R t x G j)341 rw [Submodule.Quotient.eq]342 constructor343 · change (chartBase R t x t)^d * G.left (j+1) - (chartBase R t x t)^d * G.left j ∈344 (chartExceptional R t x)^j345 rw [← mul_sub]346 exact Ideal.mul_mem_left _ _ (G.left_compat j)347 · change (chartBase R x t x)^d * G.right (j+1) - (chartBase R x t x)^d * G.right j ∈348 (chartExceptional R x t)^j349 rw [← mul_sub]350 exact Ideal.mul_mem_left _ _ (G.right_compat j)351 352/-- Level-one generators glued up to a unit can be renormalized to glue exactly. -/353theorem glued_generators_level_one (R : Type) [CommRing R] (t x : R)354 (beta : BlowupRestriction R t x) (d : ℕ) (gA1 : BlowupChart R t x) (gB1 : BlowupChart R x t)355 (hnorm : ∃ u : Rˣ, (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) gA1 - algebraMap R356 (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x) ^ d * beta.right gB1) ∈357 (Ideal.span {overlapException R t x})) :358 ∃ (FA1 : BlowupChart R t x) (FB1 : BlowupChart R x t), Ideal.span359 {Ideal.Quotient.mk ((chartExceptional R t x)^1) FA1} = Ideal.span360 {Ideal.Quotient.mk ((chartExceptional R t x)^1) gA1} ∧ Ideal.span361 {Ideal.Quotient.mk ((chartExceptional R x t)^1) FB1} = Ideal.span362 {Ideal.Quotient.mk ((chartExceptional R x t)^1) gB1} ∧363 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) FA1 - (overlapSlope R t x)^d *364 beta.right FB1 ∈ (Ideal.span {overlapException R t x})^1 := by365 obtain ⟨u, hu⟩ := hnorm366 refine ⟨gA1, algebraMap R (BlowupChart R x t) (u : R) * gB1, rfl, ?_, ?_⟩367 · have hU : IsUnit (Ideal.Quotient.mk ((chartExceptional R x t)^1)368 (algebraMap R (BlowupChart R x t) (u : R))) :=369 (u.isUnit.map (algebraMap R (BlowupChart R x t))).map _370 obtain ⟨v, hv⟩ := hU371 rw [map_mul, ← hv]372 exact Ideal.span_singleton_mul_left_unit v.isUnit _373 · rw [pow_one]374 have : beta.right (algebraMap R (BlowupChart R x t) (u : R) * gB1) = algebraMap R375 (BlowupOverlap R t x) (u : R) * beta.right gB1 := by376 rw [map_mul]; congr 1; exact AlgHom.commutes _ _377 rwa [this, mul_left_comm]378 379/-! ### The exceptional line -/380 381/-- The first level `A/(t)` of the `t`-chart is the polynomial ring `(R/(t, x))[Z]`. -/382theorem exceptional_chart_is_affine_line (R : Type) [CommRing R] (t x : R) :383 ∃ e : ExceptionalChartLevel R t x 1 ≃+* Polynomial (R ⧸ Ideal.span {t,x}),384 (∀ r : R, e (levelBase R t x 1 r) = Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r)) ∧385 e (levelSlope R t x 1) = Polynomial.X := by386 set I : Ideal R := Ideal.span {t, x}387 have ht : Ideal.Quotient.mk I t = 0 := Ideal.Quotient.eq_zero_iff_mem.2388 (Ideal.subset_span (by simp))389 have hx : Ideal.Quotient.mk I x = 0 := Ideal.Quotient.eq_zero_iff_mem.2390 (Ideal.subset_span (by simp))391 let f0 : Polynomial R →+* Polynomial (R ⧸ I) := Polynomial.mapRingHom (Ideal.Quotient.mk I)392 have hf0 : ∀ a ∈ Ideal.span {blowupRelation R t x}, f0 a = 0 := by393 intro a ha394 obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.1 ha395 simp [f0, blowupRelation, ht, hx]396 let f1 : BlowupChart R t x →+* Polynomial (R ⧸ I) := Ideal.Quotient.lift _ f0 hf0397 have hf1 : ∀ a ∈ exceptionalLevelIdeal R t x 1, f1 a = 0 := by398 intro a ha399 obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.1 ha400 simp [f1, f0, chartBase, ht]401 let F : ExceptionalChartLevel R t x 1 →+* Polynomial (R ⧸ I) := Ideal.Quotient.lift _ f1 hf1402 have hbt : levelBase R t x 1 t = 0 := by403 simp only [levelBase, RingHom.comp_apply]404 exact Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span (by simp))405 have hbx : levelBase R t x 1 x = 0 := by406 simp only [levelBase, RingHom.comp_apply, ← blowup_chart_relation R t x, map_mul]407 have h := hbt408 simp only [levelBase, RingHom.comp_apply] at h409 rw [h]; exact zero_mul (M₀ := ExceptionalChartLevel R t x 1) _410 have hb : ∀ a ∈ I, levelBase R t x 1 a = 0 := fun a ha ↦411 (show I ≤ RingHom.ker (levelBase R t x 1) from412 Ideal.span_le.2 (by rintro y (rfl | rfl); exacts [hbt, hbx])) ha413 let g0 : R ⧸ I →+* ExceptionalChartLevel R t x 1 := Ideal.Quotient.lift I (levelBase R t x 1) hb414 let G : Polynomial (R ⧸ I) →+* ExceptionalChartLevel R t x 1 := Polynomial.eval₂RingHom g0415 (levelSlope R t x 1)416 have hFb : ∀ r : R, F (levelBase R t x 1 r) = Polynomial.C (Ideal.Quotient.mk I r) := by417 intro r; simp [F, f1, f0, levelBase, chartBase]418 have hFs : F (levelSlope R t x 1) = Polynomial.X := by419 simp [F, f1, f0, levelSlope, chartSlope]420 have hGF : G.comp F = RingHom.id _ := by421 refine Ideal.Quotient.ringHom_ext <| Ideal.Quotient.ringHom_ext <| Polynomial.ringHom_ext ?_ ?_422 · intro r423 change G (F (levelBase R t x 1 r)) = levelBase R t x 1 r424 rw [hFb]; simp [G, g0]425 · change G (F (levelSlope R t x 1)) = levelSlope R t x 1426 rw [hFs]; simp [G]427 have hFG : F.comp G = RingHom.id _ := by428 apply Polynomial.ringHom_ext429 · intro r430 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r431 simp [G, g0, hFb]432 · simp [G, hFs]433 exact ⟨RingEquiv.ofRingHom F G hFG hGF, hFb, hFs⟩434 435/-- The `t`-chart modulo its exceptional ideal is `(R/(t, x))[Z]`. -/436theorem exceptional_line_equiv_chart_exceptional (R : Type) [CommRing R] (t x : R) :437 ∃ e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial438 (R ⧸ Ideal.span ({t,x} : Set R)), (∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x)439 (chartBase R t x r)) = Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r)) ∧ e440 (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X := by441 obtain ⟨e₀, h1, h2⟩ := exceptional_chart_is_affine_line R t x442 have hI : chartExceptional R t x = exceptionalLevelIdeal R t x 1 := by443 simp [chartExceptional, exceptionalLevelIdeal]444 exact ⟨(Ideal.quotEquivOfEq hI).trans e₀, fun r => h1 r, h2⟩445 446/-- For a surface, the `t`-chart modulo its exceptional ideal is `k[Z]`, `k` the residue447field. -/448theorem exceptional_line_equiv_residue_field (O R : Type) [CommRing O] [IsDomain O]449 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]450 (S : SurfaceData O R) :451 ∃ e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+* Polynomial452 (IsLocalRing.ResidueField R), (∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x)453 (chartBase R S.t S.x r)) = Polynomial.C (IsLocalRing.residue R r)) ∧ e454 (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X := by455 obtain ⟨e₀, h1, h2⟩ := exceptional_line_equiv_chart_exceptional R S.t S.x456 let κ : (R ⧸ Ideal.span ({S.t, S.x} : Set R)) ≃+* IsLocalRing.ResidueField R :=457 Ideal.quotEquivOfEq S.parameters458 refine ⟨e₀.trans (Polynomial.mapEquiv κ), ?_, ?_⟩459 · intro r460 simp only [RingEquiv.trans_apply, h1]461 change Polynomial.map (κ.toRingHom) (Polynomial.C _) = _462 rw [Polynomial.map_C]463 rfl464 · simp [h2]465 466/-- The first level of the overlap is the Laurent polynomial ring `(R/(t, x))[Z, Z⁻¹]`. -/467theorem exceptional_overlap_is_laurent_line (R : Type) [CommRing R] (t x : R) :468 ∃ e : ExceptionalOverlapLevel R t x 1 ≃+* LaurentPolynomial (R ⧸ Ideal.span {t,x}),469 (∀ r : R, e (levelOverlapMap R t x 1 (levelBase R t x 1 r)) = LaurentPolynomial.C470 (Ideal.Quotient.mk (Ideal.span {t,x}) r)) ∧ e (levelOverlapMap R t x 1 (levelSlope R t x 1))471 = LaurentPolynomial.T 1 := by472 obtain ⟨e0, hC, hX⟩ := exceptional_chart_is_affine_line R t x473 have hL : IsLocalization (Submonoid.powers (Polynomial.X : Polynomial (R ⧸ Ideal.span {t,x})))474 (LaurentPolynomial (R ⧸ Ideal.span {t,x})) := LaurentPolynomial.isLocalization475 let E := IsLocalization.ringEquivOfRingEquiv (ExceptionalOverlapLevel R t x 1)476 (LaurentPolynomial (R ⧸ Ideal.span {t,x})) (M := Submonoid.powers (levelSlope R t x 1))477 (T := Submonoid.powers (Polynomial.X : Polynomial (R ⧸ Ideal.span {t,x}))) e0478 (by rw [Submonoid.map_powers]; exact congrArg Submonoid.powers hX)479 have hE (a) : E (algebraMap _ _ a) = algebraMap _ _ (e0 a) :=480 IsLocalization.ringEquivOfRingEquiv_eq _ a481 refine ⟨E, fun r => ?_, ?_⟩482 · simp only [levelOverlapMap]483 rw [hE, hC, LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_C]484 · simp only [levelOverlapMap]485 rw [hE, hX, LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_X]486 487/-- The units of a Laurent polynomial ring over a field are the nonzero monomials. -/488theorem laurent_isUnit_iff_monomial (k : Type) [Field k] (f : LaurentPolynomial k) :489 IsUnit f ↔ ∃ c : k, c ≠ 0 ∧ ∃ m : ℤ, f = LaurentPolynomial.C c * LaurentPolynomial.T m := by490 constructor491 · rintro ⟨u, rfl⟩492 set f : LaurentPolynomial k := u.val493 set g : LaurentPolynomial k := u.inv494 have hfg : f * g = 1 := u.val_inv495 have hf : f ≠ 0 := fun h => by simp [h] at hfg496 have hg : g ≠ 0 := fun h => by simp [h] at hfg497 have hfn : f.coeff.support.Nonempty := Finsupp.support_nonempty_iff.2 fun h ↦498 hf (AddMonoidAlgebra.coeff_injective (by simpa using h))499 have hgn : g.coeff.support.Nonempty := Finsupp.support_nonempty_iff.2 fun h ↦500 hg (AddMonoidAlgebra.coeff_injective (by simpa using h))501 set a := f.coeff.support.max' hfn502 set a' := g.coeff.support.max' hgn503 set b := f.coeff.support.min' hfn504 set b' := g.coeff.support.min' hgn505 have hsupp1 : ∀ n : ℤ, (1 : LaurentPolynomial k).coeff n ≠ 0 → n = 0 := fun n hn ↦ by506 rw [AddMonoidAlgebra.one_def, AddMonoidAlgebra.coeff_single] at hn507 exact not_imp_comm.1 Finsupp.single_eq_of_ne hn508 have e1 : a + a' = 0 := by509 apply hsupp1510 rw [← hfg, AddMonoidAlgebra.coeff_mul_add_of_uniqueAdd]511 · exact mul_ne_zero (Finsupp.mem_support_iff.1 (Finset.max'_mem _ _))512 (Finsupp.mem_support_iff.1 (Finset.max'_mem _ _))513 · intro x y hx hy hxy514 have := Finset.le_max' _ x hx; have := Finset.le_max' _ y hy515 constructor <;> omega516 have e2 : b + b' = 0 := by517 apply hsupp1518 rw [← hfg, AddMonoidAlgebra.coeff_mul_add_of_uniqueAdd]519 · exact mul_ne_zero (Finsupp.mem_support_iff.1 (Finset.min'_mem _ _))520 (Finsupp.mem_support_iff.1 (Finset.min'_mem _ _))521 · intro x y hx hy hxy522 have := Finset.min'_le _ x hx; have := Finset.min'_le _ y hy523 constructor <;> omega524 have hb' : b' ≤ a' := Finset.min'_le_max' _ hgn525 have hsub : f.coeff.support ⊆ {a} := fun c hc => by526 have := Finset.le_max' _ c hc; have := Finset.min'_le _ c hc527 rw [Finset.mem_singleton]; omega528 refine ⟨f.coeff a, Finsupp.mem_support_iff.1 (Finset.max'_mem _ _), a, ?_⟩529 rw [← LaurentPolynomial.single_eq_C_mul_T]530 apply AddMonoidAlgebra.coeff_injective531 rw [AddMonoidAlgebra.coeff_single]532 exact Finsupp.support_subset_singleton.1 hsub533 · rintro ⟨c, hc, m, rfl⟩534 exact ((isUnit_iff_ne_zero.2 hc).map LaurentPolynomial.C).mul (LaurentPolynomial.isUnit_T m)535 536/-- The points above affine directions of the exceptional line are maximal, contain `t`,537contain the slope exactly for the direction `Z`, map to `(φ)` on the exceptional line, depend538injectively on `φ`, and the point above `Z` is `(t, Z)`. -/539theorem directionPoint_properties (R : Type) [CommRing R] [IsLocalRing R] (t x : R)540 [(Ideal.span ({t,x} : Set R)).IsMaximal] (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+*541 Polynomial (IsLocalRing.ResidueField R)) (he : ∀ r : R, e542 (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) = Polynomial.C543 (IsLocalRing.residue R r)) (heZ : e (Ideal.Quotient.mk (chartExceptional R t x)544 (chartSlope R t x)) = Polynomial.X) :545 (∀ φ : AffineDirection (IsLocalRing.ResidueField R), (directionPoint R t x e φ).IsMaximal ∧546 chartBase R t x t ∈ directionPoint R t x e φ ∧ (chartSlope R t x ∈ directionPoint R t x e φ547 ↔ φ = zeroAffine (IsLocalRing.ResidueField R)) ∧548 ((directionPoint R t x e φ).map (Ideal.Quotient.mk (chartExceptional R t x))).map e =549 Ideal.span {φ.val}) ∧ Function.Injective (directionPoint R t x e) ∧ directionPoint R t x e550 (zeroAffine (IsLocalRing.ResidueField R)) = Ideal.span {chartBase R t x t, chartSlope R t x}551 := by552 set ψ : BlowupChart R t x →+* Polynomial (IsLocalRing.ResidueField R) :=553 e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R t x)) with hψ554 have hsurj : Function.Surjective ψ := e.surjective.comp Ideal.Quotient.mk_surjective555 have hker : RingHom.ker ψ = chartExceptional R t x := by556 ext a557 simp [hψ, RingHom.mem_ker, Ideal.Quotient.eq_zero_iff_mem]558 have hDP : ∀ φ : AffineDirection (IsLocalRing.ResidueField R),559 directionPoint R t x e φ = (Ideal.span {φ.val}).comap ψ := fun _ => rfl560 have ht0 : ψ (chartBase R t x t) = 0 := by561 have hm : Ideal.span ({t,x} : Set R) = IsLocalRing.maximalIdeal R :=562 IsLocalRing.eq_maximalIdeal inferInstance563 have : t ∈ IsLocalRing.maximalIdeal R := hm ▸ Ideal.subset_span (by simp)564 change e _ = 0565 rw [he, (IsLocalRing.residue_eq_zero_iff t).2 this, map_zero]566 have hZ : ψ (chartSlope R t x) = Polynomial.X := heZ567 have himg : ∀ φ : AffineDirection (IsLocalRing.ResidueField R),568 ((directionPoint R t x e φ).map (Ideal.Quotient.mk (chartExceptional R t x))).map e569 = Ideal.span {φ.val} := by570 intro φ571 rw [show Ideal.map e (Ideal.map (Ideal.Quotient.mk (chartExceptional R t x))572 (directionPoint R t x e φ)) = Ideal.map e.toRingHom (Ideal.map573 (Ideal.Quotient.mk (chartExceptional R t x)) (directionPoint R t x e φ)) from rfl,574 Ideal.map_map, hDP]575 exact Ideal.map_comap_of_surjective ψ hsurj _576 refine ⟨fun φ => ⟨?_, ?_, ?_, himg φ⟩, ?_, ?_⟩577 · have := PrincipalIdealRing.isMaximal_of_irreducible φ.2.2578 exact Ideal.comap_isMaximal_of_surjective ψ hsurj579 · rw [hDP, Ideal.mem_comap, ht0]; exact zero_mem _580 · rw [hDP, Ideal.mem_comap, hZ, Ideal.mem_span_singleton]581 exact ⟨fun h ↦ Subtype.ext <| Polynomial.eq_of_monic_of_associated φ.2.1 Polynomial.monic_X582 (φ.2.2.associated_of_dvd Polynomial.irreducible_X h), by rintro rfl; exact dvd_rfl⟩583 · intro φ φ' h584 have h2 := himg φ585 rw [h, himg φ', Ideal.span_singleton_eq_span_singleton] at h2586 exact Subtype.ext (Polynomial.eq_of_monic_of_associated φ.2.1 φ'.2.1 h2.symm)587 · have key : ∀ I J : Ideal (BlowupChart R t x), RingHom.ker ψ ≤ I → RingHom.ker ψ ≤ J →588 I.map ψ = J.map ψ → I = J := by589 intro I J hI hJ hIJ590 rw [RingHom.ker_eq_comap_bot] at hI hJ591 rw [← sup_eq_left.2 hI, ← sup_eq_left.2 hJ, ← Ideal.comap_map_of_surjective ψ hsurj,592 ← Ideal.comap_map_of_surjective ψ hsurj, hIJ]593 apply key594 · rw [hker, chartExceptional, Ideal.span_le, Set.singleton_subset_iff, hDP, SetLike.mem_coe,595 Ideal.mem_comap, ht0]; exact zero_mem _596 · rw [hker, chartExceptional, Ideal.span_le, Set.singleton_subset_iff]597 exact Ideal.subset_span (by simp)598 · rw [hDP, Ideal.map_comap_of_surjective ψ hsurj, Ideal.map_span, Set.image_pair, ht0, hZ,599 Ideal.span_insert_zero]600 rfl601 602/-- A degree-`d` form in a regular pair `(t, x)` with a coefficient outside `(t, x)` does not603lie in `(t, x)^(d+1)`. -/604theorem homogeneous_form_not_mem_pow_succ (R : Type) [CommRing R] (t x : R)605 [(Ideal.span ({t,x} : Set R)).IsMaximal] (hreg : RegularParameterPair R t x) (d : ℕ)606 (c : Fin (d + 1) → R) (i₀ : Fin (d + 1)) (hi₀ : c i₀ ∉ Ideal.span {t,x}) :607 (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) ∉ (Ideal.span {t,x})^(d+1) := by608 intro hF609 set φ := chartBase R t x with hφ610 set Z := chartSlope R t x with hZ611 have hrel : φ t * Z = φ x := blowup_chart_relation R t x612 have hinjd : IsLeftRegular (φ t ^ d) :=613 IsLeftRegular.pow d (blowup_exceptional_parameter_regular R t x hreg)614 set P : BlowupChart R t x := ∑ i : Fin (d+1), φ (c i) * Z ^ i.val with hP615 have hFP : φ (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) = φ t ^ d * P := by616 rw [map_sum, hP, Finset.mul_sum]617 apply Finset.sum_congr rfl618 intro i _619 have hi : i.val ≤ d := Nat.lt_succ_iff.mp i.2620 simp only [map_mul, map_pow]621 rw [← hrel, mul_pow]622 have : φ t ^ d = φ t ^ (d - i.val) * φ t ^ i.val := by623 rw [← pow_add, Nat.sub_add_cancel hi]624 rw [this]; ring625 have hmem : φ (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) ∈ (Ideal.span {φ t})^(d+1) := by626 have h1 : φ (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) ∈ Ideal.map φ627 ((Ideal.span {t,x})^(d+1)) :=628 Ideal.mem_map_of_mem _ hF629 rw [Ideal.map_pow] at h1630 refine Ideal.pow_right_mono ?_ _ h1631 rw [Ideal.map_span, Ideal.span_le]632 rintro _ ⟨y, hy, rfl⟩633 rcases hy with rfl | hy634 · exact Ideal.subset_span rfl635 · have : y = x := by simpa using hy636 subst this637 rw [SetLike.mem_coe, ← hrel]638 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)639 rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton'] at hmem640 obtain ⟨w, hw⟩ := hmem641 rw [hFP] at hw642 have hPw : P = φ t * w := hinjd <| show φ t ^ d * P = φ t ^ d * (φ t * w) by643 rw [← mul_assoc, ← pow_succ, ← hw]; ring644 obtain ⟨e, he1, he2⟩ := exceptional_chart_is_affine_line R t x645 have hQ : (∑ i : Fin (d+1), levelBase R t x 1 (c i) * levelSlope R t x 1 ^ i.val)646 = Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1) P := by647 rw [hP, map_sum]648 apply Finset.sum_congr rfl649 intro i _650 simp [levelBase, levelSlope, hφ, hZ]651 have hzero : Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1) P = 0 := by652 rw [Ideal.Quotient.eq_zero_iff_mem, hPw, exceptionalLevelIdeal, pow_one]653 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)654 have h0 := congrArg e (hQ.trans hzero)655 rw [map_sum, map_zero] at h0656 have h1 := congrArg (fun p => Polynomial.coeff p i₀.val) h0657 simp only [map_mul, map_pow, he1, he2, Polynomial.finsetSum_coeff, Polynomial.coeff_zero] at h1658 rw [Finset.sum_eq_single i₀] at h1659 · exact hi₀ (Ideal.Quotient.eq_zero_iff_mem.mp (by simpa using h1))660 · intro b _ hb661 rw [Polynomial.coeff_C_mul, Polynomial.coeff_X_pow]662 have : i₀.val ≠ b.val := fun h => hb (Fin.ext h).symm663 simp [this]664 · simp665 666/-! ### Finitely supported local data -/667 668/-- Powers of distinct maximal ideals are coprime. -/669private theorem distinct_maximal_powers_coprime (A : Type) [CommRing A] (P Q : Ideal A)670 [P.IsMaximal]671 [Q.IsMaximal] (hPQ : P ≠ Q) (L M : ℕ) :672 IsCoprime (P^L) (Q^M) :=673 (Ideal.isCoprime_of_isMaximal hPQ).pow674 675/-- Localizing the finitely supported kernel at `P i` recovers the contraction of `J i`. -/676private theorem finite_support_localization_recovers (A : Type) [CommRing A] [IsNoetherianRing A]677 (ι : Type)678 [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P) (L : ι → ℕ)679 (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (hJ : ∀ i,680 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map681 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ J i) (i : ι) :682 (finiteSupportKernel A ι P J).map (algebraMap A (Localization.AtPrime (P i))) = (J i).comap683 (localCompletionMap (Localization.AtPrime (P i))) := by684 classical685 have := Fintype.ofFinite ι686 set R := Localization.AtPrime (P i)687 set K : Ideal R := (J i).comap (localCompletionMap R) with hKdef688 have hIi : (J i).comap (completedPointMap A (P i)) = K.comap (algebraMap A R) := rfl689 apply le_antisymm690 · have h1 : finiteSupportKernel A ι P J ≤ (J i).comap (completedPointMap A (P i)) :=691 iInf_le _ i692 calc _ ≤ ((J i).comap (completedPointMap A (P i))).map (algebraMap A R) := Ideal.map_mono h1693 _ = K := by rw [hIi]; exact IsLocalization.map_under (P i).primeCompl R K694 · have hs : ∀ j, j ≠ i → ∃ s ∈ P j, s ∉ P i := fun j hj ↦ SetLike.not_le_iff_exists.1 fun h ↦695 hj (hP (Ideal.IsMaximal.eq_of_le inferInstance (Ideal.IsMaximal.ne_top inferInstance) h))696 choose! s hs using hs697 set t := ∏ j ∈ Finset.univ.erase i, s j ^ L j698 have ht : t ∈ (P i).primeCompl := Submonoid.prod_mem _ fun j hj ↦699 Submonoid.pow_mem _ (hs j (Finset.ne_of_mem_erase hj)).2 _700 have htj : ∀ j, j ≠ i → t ∈ (J j).comap (completedPointMap A (P j)) := fun j hj ↦ by701 apply completed_point_power_contraction A (P j) (L j) (J j) (hJ j)702 obtain ⟨c, hc⟩ : s j ^ L j ∣ t :=703 Finset.dvd_prod_of_mem _ (Finset.mem_erase.2 ⟨hj, Finset.mem_univ _⟩)704 rw [hc]705 exact Ideal.mul_mem_right _ _ (Ideal.pow_mem_pow (hs j hj).1 _)706 intro x hx707 obtain ⟨⟨a, u⟩, rfl⟩ := IsLocalization.mk'_surjective (P i).primeCompl x708 have ha : a ∈ (J i).comap (completedPointMap A (P i)) := by709 rw [hIi, Ideal.mem_comap]710 have : algebraMap A R a = IsLocalization.mk' R a u * algebraMap A R u := by711 rw [IsLocalization.mk'_spec]712 rw [this]713 exact Ideal.mul_mem_right _ _ hx714 have hta : t * a ∈ finiteSupportKernel A ι P J := by715 refine Ideal.mem_iInf.2 fun j => ?_716 by_cases hj : j = i717 · subst hj; exact Ideal.mul_mem_left _ _ ha718 · exact Ideal.mul_mem_right _ _ (htj j hj)719 have : IsLocalization.mk' R a u = algebraMap A R (t * a) * IsLocalization.mk' R (1 : A)720 (u * ⟨t, ht⟩) := by721 rw [← IsLocalization.mk'_eq_mul_mk'_one, ← IsLocalization.mk'_cancel a u ⟨t, ht⟩, mul_comm a722 t]723 change IsLocalization.mk' R a u ∈ _724 rw [this]725 exact Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ hta)726 727/-- Extending the finitely supported kernel to the completion at `P i` recovers `J i`. -/728theorem finite_support_completion_recovers (A : Type) [CommRing A] [IsNoetherianRing A] (ι : Type)729 [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P) (L : ι → ℕ)730 (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (hJ : ∀ i,731 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map732 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ J i) (i : ι) :733 (finiteSupportKernel A ι P J).map (completedPointMap A (P i)) = J i := by734 have h1 := finite_support_localization_recovers A ι P hP L J hJ i735 have h2 := finite_colength_completion_ideal_descent736 (Localization.AtPrime (P i)) (L i) (J i) (hJ i)737 rw [completedPointMap, ← Ideal.map_map, h1, h2]738 739/-! The finitely supported results below are proved first for an arbitrary family of prime ideals740carrying a separate maximality hypothesis `hmax`, and then specialised to the741`[∀ i, (P i).IsMaximal]` statements. This keeps the instance arguments of the families742`finiteSupportQuotientMap`, `finiteSupportKernel` syntactically uniform (a local variable rather743than `fun i ↦ Ideal.IsMaximal.isPrime' (P i)`), which makes the kernel check far cheaper. -/744 745/-- `finite_support_quotient_surjective` for a family of primes that are maximal (the746maximality is a separate hypothesis, keeping the instance arguments uniform). -/747theorem finite_support_quotient_surjective_of_isPrime (A : Type) [CommRing A]748 [IsNoetherianRing A] (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsPrime]749 (hmax : ∀ i, (P i).IsMaximal) (hP : Function.Injective P) (L : ι → ℕ)750 (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (hJ : ∀ i,751 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map752 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ J i) :753 Function.Surjective (finiteSupportQuotientMap A ι P J) := by754 intro b755 have hrep : ∀ i, ∃ a : A, (Ideal.Quotient.mk (J i)) (completedPointMap A (P i) a) = b i :=756 fun i => @finite_completed_point_quotient_surjective A _ _ (P i) (hmax i) (L i) (J i) (hJ i)757 (b i)758 choose a ha using hrep759 have hcop : Pairwise fun i j => IsCoprime (P i ^ L i) (P j ^ L j) := fun i j hij =>760 @distinct_maximal_powers_coprime A _ (P i) (P j) (hmax i) (hmax j) (hP.ne hij) (L i) (L j)761 obtain ⟨r, hr⟩ := Ideal.exists_forall_sub_mem_ideal hcop a762 refine ⟨r, funext fun i => ?_⟩763 have hmem := @completed_point_power_contraction A _ (P i) (hmax i) (L i) (J i) (hJ i) _ (hr i)764 rw [Ideal.mem_comap, map_sub] at hmem765 change (Ideal.Quotient.mk (J i)) (completedPointMap A (P i) r) = b i766 rw [← ha i]767 exact Ideal.Quotient.eq.mpr hmem768 769/-- The map from `A` to the product of finite-colength completed local quotients is surjective. -/770theorem finite_support_quotient_surjective (A : Type) [CommRing A] [IsNoetherianRing A] (ι : Type)771 [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P) (L : ι → ℕ)772 (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (hJ : ∀ i,773 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map774 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ J i) :775 Function.Surjective (finiteSupportQuotientMap A ι P J) :=776 finite_support_quotient_surjective_of_isPrime A ι P (fun _ ↦ inferInstance) hP L J hJ777 778/-- Kernel at level `j` = kernel at level `j + 1` plus `(e)^j`. -/779private theorem finite_support_kernels_compatible (A : Type) [CommRing A] [IsNoetherianRing A]780 (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsPrime] (hmax : ∀ i, (P i).IsMaximal)781 (hP : Function.Injective P) (e : A)782 (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ) (hfin : ∀ i,783 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map784 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤785 finiteLocalCurveIdeal A (P i) e (g i) 1) (j : ℕ) :786 finiteSupportKernel A ι P (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) =787 finiteSupportKernel A ι P (fun i => finiteLocalCurveIdeal A (P i) e (g i) (j+1)) ⊔788 (Ideal.span {e})^j := by789 apply le_antisymm790 · intro a ha791 simp only [finiteSupportKernel, Ideal.mem_iInf, Ideal.mem_comap, finiteLocalCurveIdeal,792 Ideal.mem_span_pair] at ha793 choose u v huv using ha794 obtain ⟨c, hc⟩ := finite_support_quotient_surjective_of_isPrime A ι P hmax hP L795 (fun i => finiteLocalCurveIdeal A (P i) e (g i) 1) hfin796 (fun i => Ideal.Quotient.mk _ (v i))797 have hc' : ∀ i, v i - completedPointMap A (P i) c ∈798 finiteLocalCurveIdeal A (P i) e (g i) 1 := fun i ↦799 Ideal.Quotient.eq.mp (congrFun hc i).symm800 have hmem : a - e ^ j * c ∈ finiteSupportKernel A ι P801 (fun i => finiteLocalCurveIdeal A (P i) e (g i) (j+1)) := by802 simp only [finiteSupportKernel, Ideal.mem_iInf, Ideal.mem_comap]803 intro i804 obtain ⟨x, y, hxy⟩ := Ideal.mem_span_pair.mp (hc' i)805 simp only [finiteLocalCurveIdeal, Ideal.mem_span_pair]806 refine ⟨u i + (completedPointMap A (P i) e) ^ j * x, y, ?_⟩807 rw [map_sub, map_mul, map_pow, ← huv i]808 have : v i =809 x * g i + y * (completedPointMap A (P i) e) ^ 1 + completedPointMap A (P i) c := by810 rw [hxy]; ring811 rw [this]; ring812 rw [← sub_add_cancel a (e ^ j * c)]813 refine Submodule.add_mem_sup hmem ?_814 rw [Ideal.span_singleton_pow]815 exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)816 · refine sup_le ?_ ?_817 · refine iInf_mono fun i => Ideal.comap_mono ?_818 refine Ideal.span_le.mpr ?_819 rintro x (rfl | rfl)820 · exact Ideal.subset_span (by simp)821 · rw [pow_succ]822 exact Ideal.mul_mem_right _ _ (Ideal.subset_span (by simp))823 · rw [Ideal.span_singleton_pow, Ideal.span_le]824 rintro x rfl825 simp only [finiteSupportKernel, SetLike.mem_coe, Ideal.mem_iInf, Ideal.mem_comap]826 intro i827 rw [map_pow]828 exact Ideal.subset_span (by simp)829 830/-- The level kernels are compatible with the reduction maps `A/(e)^{j+1} → A/(e)^j`. -/831private theorem finite_support_level_kernels_compatible (A : Type) [CommRing A] [IsNoetherianRing A]832 (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsPrime] (hmax : ∀ i, (P i).IsMaximal)833 (hP : Function.Injective P)834 (e : A) (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ)835 (hfin : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map836 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤837 finiteLocalCurveIdeal A (P i) e (g i) 1) (j : ℕ) :838 (finiteSupportLevelKernel A ι P (fun i => finiteLocalCurveIdeal A (P i) e (g i) (j+1)) e839 (j+1)).map (principalPowerReduction A e j).toRingHom = finiteSupportLevelKernel A ι P840 (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) e j := by841 unfold finiteSupportLevelKernel842 rw [Ideal.map_map,843 finite_support_kernels_compatible A ι P hmax hP e g L hfin j, Ideal.map_sup,844 Ideal.map_quotient_self, sup_bot_eq]845 congr 1846 847/-- Generators of consecutive level kernels generate the same ideal modulo `(e)^j`. -/848theorem finite_support_generators_compatible (A : Type) [CommRing A] [IsNoetherianRing A] (ι : Type)849 [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P) (e : A)850 (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ) (hfin : ∀ i,851 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map852 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤853 finiteLocalCurveIdeal A (P i) e (g i) 1) (F : ℕ → A)854 (hF : ∀ j : ℕ, finiteSupportLevelKernel A ι P855 (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) e j = Ideal.span856 {Ideal.Quotient.mk ((Ideal.span {e})^j) (F j)}) (j : ℕ) :857 Ideal.span {Ideal.Quotient.mk ((Ideal.span {e})^j) (F (j+1))} = Ideal.span858 {Ideal.Quotient.mk ((Ideal.span {e})^j) (F j)} := by859 have h := finite_support_level_kernels_compatible A ι P (fun _ ↦ inferInstance) hP e g L hfin j860 rwa [hF (j+1), hF j, Ideal.map_span, Set.image_singleton] at h861 862private theorem finite_support_quotient_equiv_aux (A : Type) [CommRing A] (ι : Type)863 (P : ι → Ideal A) [∀ i, (P i).IsPrime] (J : ∀ i, Ideal (CompletedLocalAt A (P i)))864 (hs : Function.Surjective (finiteSupportQuotientMap A ι P J)) :865 ∃ E : (A ⧸ finiteSupportKernel A ι P J) ≃+* (∀ i, CompletedLocalAt A (P i) ⧸ J i), ∀ a : A, E866 (Ideal.Quotient.mk (finiteSupportKernel A ι P J) a) = finiteSupportQuotientMap A ι P J a :=867 by868 have hker : RingHom.ker (finiteSupportQuotientMap A ι P J) = finiteSupportKernel A ι P J := by869 ext a870 simp only [RingHom.mem_ker, finiteSupportKernel, finiteSupportQuotientMap, Ideal.mem_iInf,871 Ideal.mem_comap, funext_iff, RingHom.pi_apply, RingHom.comp_apply, Pi.zero_apply,872 Ideal.Quotient.eq_zero_iff_mem]873 exact ⟨(Ideal.quotEquivOfEq hker.symm).trans (RingHom.quotientKerEquivOfSurjective hs),874 fun a => rfl⟩875 876/-- Chinese remainder theorem: `A` modulo the finitely supported kernel is the product of the877completed local quotients. -/878theorem finite_support_quotient_equiv (A : Type) [CommRing A] [IsNoetherianRing A] (ι : Type)Lemma 4.3879 [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P) (L : ι → ℕ)880 (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (hJ : ∀ i,881 ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map882 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ J i) :883 ∃ E : (A ⧸ finiteSupportKernel A ι P J) ≃+* (∀ i, CompletedLocalAt A (P i) ⧸ J i), ∀ a : A, E884 (Ideal.Quotient.mk (finiteSupportKernel A ι P J) a) = finiteSupportQuotientMap A ι P J a :=885 finite_support_quotient_equiv_aux A ι P J (finite_support_quotient_surjective A ι P hP L J hJ)886 887/-- If `e` is a nonzerodivisor modulo `g`, then the annihilator of `e` in `C/(g, e^j)` is888generated by `e^(j−1)`. -/889private theorem finite_curve_exceptional_annihilator (C : Type) [CommRing C] (e g : C)890 (he : Function.Injective (fun a : C ⧸ Ideal.span {g} => Ideal.Quotient.mk (Ideal.span {g}) e *891 a)) (j : ℕ) (hj : 0 < j) (b : C ⧸ Ideal.span {g, e^j})892 (hb : Ideal.Quotient.mk (Ideal.span {g, e^j}) e * b = 0) :893 ∃ c : C ⧸ Ideal.span {g, e^j}, b = (Ideal.Quotient.mk (Ideal.span {g, e^j}) e)^(j-1)*c := by894 obtain ⟨b0, rfl⟩ := Ideal.Quotient.mk_surjective b895 rw [← map_mul, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_pair] at hb896 obtain ⟨a, c0, hac⟩ := hb897 have hej : e ^ j = e * e ^ (j - 1) := by898 rw [← pow_succ']; congr 1; omega899 have key : Ideal.Quotient.mk (Ideal.span {g}) b0900 = Ideal.Quotient.mk (Ideal.span {g}) (e ^ (j - 1) * c0) := by901 apply he902 have hg : Ideal.Quotient.mk (Ideal.span {g}) g = 0 :=903 Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span rfl)904 simp only [← map_mul]905 rw [← hac, hej]906 simp only [map_add, map_mul, hg, mul_zero, zero_add]907 ring908 refine ⟨Ideal.Quotient.mk _ c0, ?_⟩909 rw [← map_pow, ← map_mul, Ideal.Quotient.eq]910 rw [Ideal.Quotient.eq] at key911 exact Ideal.span_mono (by simp) key912 913/-- If `e^j = 0` and annihilators of `φ e` lie in `(φ e)^(j−1)`, then914`ker φ ∩ (e) ⊆ (e) · ker φ`. -/915private theorem kernel_saturation_from_top_layer_annihilators (A B : Type) [CommRing A] [CommRing B]916 (φ : A →+* B) (hφ : Function.Surjective φ) (e : A) (j : ℕ) (hj : 0 < j) (he : e ^ j = 0)917 (hann : ∀ b : B, φ e * b = 0 → ∃ c : B, b = (φ e)^(j-1)*c) :918 RingHom.ker φ ⊓ Ideal.span {e} ≤ Ideal.span {e} * RingHom.ker φ := by919 intro x hxx920 obtain ⟨hx, hxe⟩ := Ideal.mem_inf.mp hxx921 obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp hxe922 rw [RingHom.mem_ker, map_mul, mul_comm] at hx923 obtain ⟨b, hb⟩ := hann (φ a) hx924 obtain ⟨c, rfl⟩ := hφ b925 have hy : a - e^(j-1) * c ∈ RingHom.ker φ := by926 rw [RingHom.mem_ker, map_sub, map_mul, map_pow, hb, sub_self]927 have hj' : e * e^(j-1) = e^j := by928 rw [← pow_succ']; congr 1; omega929 have : a * e = e * (a - e^(j-1) * c) := by930 rw [mul_sub, ← mul_assoc, hj', he, zero_mul, sub_zero, mul_comm]931 rw [this]932 exact Ideal.mul_mem_mul (Ideal.mem_span_singleton_self e) hy933 934private theorem finite_curve_support_kernel_saturated_aux (A : Type) [CommRing A]935 [IsNoetherianRing A] (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsPrime]936 (hmax : ∀ i, (P i).IsMaximal) (hP : Function.Injective P)937 (e : A) (j : ℕ) (hj : 0 < j) (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ)938 (hfinite : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map939 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤940 finiteLocalCurveIdeal A (P i) e (g i) j)941 (htransverse : ∀ i, Function.Injective (fun a : CompletedLocalAt A (P i) ⧸ Ideal.span {g i}942 => Ideal.Quotient.mk (Ideal.span {g i}) (completedPointMap A (P i) e) * a)) :943 (finiteSupportLevelKernel A ι P (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) e j) ⊓944 Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)} ≤ Ideal.span945 {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)} * (finiteSupportLevelKernel A ι P946 (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) e j) := by947 set J : ∀ i, Ideal (CompletedLocalAt A (P i)) := fun i => finiteLocalCurveIdeal A (P i) e (g i) j948 with hJdef949 set Φ := finiteSupportQuotientMap A ι P J with hΦ950 have hker : RingHom.ker Φ = finiteSupportKernel A ι P J := by951 ext a952 simp only [RingHom.mem_ker, finiteSupportKernel, Ideal.mem_iInf, Ideal.mem_comap, hΦ,953 finiteSupportQuotientMap, funext_iff, RingHom.pi_apply, RingHom.comp_apply, Pi.zero_apply,954 Ideal.Quotient.eq_zero_iff_mem]955 have hle : (Ideal.span {e})^j ≤ RingHom.ker Φ := by956 rw [Ideal.span_singleton_pow, Ideal.span_le]957 rintro x rfl958 rw [SetLike.mem_coe, RingHom.mem_ker]959 funext i960 change Ideal.Quotient.mk (J i) (completedPointMap A (P i) (e ^ j)) = 0961 rw [Ideal.Quotient.eq_zero_iff_mem, map_pow]962 exact Ideal.subset_span (Set.mem_insert_of_mem _ rfl)963 set φ := Ideal.Quotient.lift ((Ideal.span {e})^j) Φ hle with hφ964 have hsurj : Function.Surjective φ := fun y ↦ by965 obtain ⟨a, rfl⟩ := finite_support_quotient_surjective_of_isPrime A ι P hmax hP L J hfinite y966 exact ⟨Ideal.Quotient.mk _ a, rfl⟩967 have hkerφ : RingHom.ker φ = finiteSupportLevelKernel A ι P J e j := by968 ext x969 obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x970 rw [RingHom.mem_ker, finiteSupportLevelKernel, Ideal.mem_quotient_iff_mem (hker ▸ hle), ← hker,971 RingHom.mem_ker]972 rfl973 have key := kernel_saturation_from_top_layer_annihilators _ _ φ hsurj974 (Ideal.Quotient.mk ((Ideal.span {e})^j) e) j hj (by975 rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem, Ideal.span_singleton_pow]976 exact Ideal.mem_span_singleton_self _) fun b hb ↦ by977 choose c hc using fun i ↦ finite_curve_exceptional_annihilator _978 (completedPointMap A (P i) e) (g i) (htransverse i) j hj (b i) (congrFun hb i)979 exact ⟨c, funext hc⟩980 rwa [hkerφ] at key981 982/-- The level kernel of transverse finite curve data is saturated with respect to `e`. -/983theorem finite_curve_support_kernel_saturated (A : Type) [CommRing A] [IsNoetherianRing A]984 (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P)985 (e : A) (j : ℕ) (hj : 0 < j) (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ)986 (hfinite : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map987 (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤988 finiteLocalCurveIdeal A (P i) e (g i) j)989 (htransverse : ∀ i, Function.Injective (fun a : CompletedLocalAt A (P i) ⧸ Ideal.span {g i}990 => Ideal.Quotient.mk (Ideal.span {g i}) (completedPointMap A (P i) e) * a)) :991 (finiteSupportLevelKernel A ι P (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) e j) ⊓992 Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)} ≤ Ideal.span993 {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)} * (finiteSupportLevelKernel A ι P994 (fun i => finiteLocalCurveIdeal A (P i) e (g i) j) e j) :=995 finite_curve_support_kernel_saturated_aux A ι P (fun _ ↦ inferInstance) hP e j hj g L hfinite996 htransverse997 998/-! ### Miscellaneous -/999 1000/-- A division-chart decomposition `C ≃ O^n × C` with second factor multiplied by `g`1001induces `C/(g) ≃ O^n`. -/1002theorem division_equiv_child_coordinates (O C : Type) [CommRing O] [CommRing C] [Algebra O C]1003 (n : ℕ) (g : C) (bc : Fin n → C) (E : C ≃ₗ[O] ((Fin n → O) × C))1004 (hE : ∀ w, E.symm w = divisionMap g bc w) :1005 ∃ EC : (C ⧸ Ideal.span {g}) ≃ₗ[O] (Fin n → O), ∀ w : C, EC1006 (Ideal.Quotient.mk (Ideal.span {g}) w) = (E w).1 := by1007 have hlift0 : coordinateLift (O := O) bc 0 = 0 := by1008 simp [coordinateLift]1009 have hker : ∀ v : C, (E (g * v)).1 = 0 := by1010 intro v1011 have h : E.symm (0, v) = g * v := by rw [hE]; simp [divisionMap, hlift0]1012 have : E (g * v) = (0, v) := by rw [← h]; simp1013 rw [this]1014 let P : Submodule O C := (Ideal.span {g}).restrictScalars O1015 have hP : P ≤ LinearMap.ker ((LinearMap.fst O (Fin n → O) C) ∘ₗ E.toLinearMap) := by1016 intro w hw1017 obtain ⟨v, rfl⟩ := Ideal.mem_span_singleton'.mp hw1018 simpa [mul_comm] using hker v1019 let f : (C ⧸ P) →ₗ[O] (Fin n → O) := P.liftQ _ hP1020 have hf : ∀ w : C, f (Submodule.Quotient.mk w) = (E w).1 := fun w => rfl1021 have hinj : Function.Injective f := by1022 rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']1023 intro q hq1024 induction q using Submodule.Quotient.induction_on with1025 | _ w =>1026 rw [hf] at hq1027 have h1 : E.symm ((E w).1, (E w).2) = w := by simp1028 rw [hq, hE] at h11029 have : w = g * (E w).2 := by1030 have h2 : divisionMap g bc ((0 : Fin n → O), (E w).2) = g * (E w).2 := by simp1031 [divisionMap, hlift0]1032 rw [← h2]; exact h1.symm1033 rw [Submodule.Quotient.mk_eq_zero, this]1034 exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self g)1035 have hsurj : Function.Surjective f := by1036 intro z1037 refine ⟨Submodule.Quotient.mk (coordinateLift bc z), ?_⟩1038 rw [hf]1039 have h : E.symm (z, 0) = coordinateLift bc z := by rw [hE]; simp [divisionMap]1040 rw [← h]; simp1041 exact ⟨LinearEquiv.ofBijective f ⟨hinj, hsurj⟩, fun w => hf w⟩1042 1043/-- The length of `R/((f) + (y))` is the contact of `f` and `y`. -/1044theorem ideal_contact_generator (R : Type) [CommRing R] (f y : R) :1045 Module.length R (R ⧸ (Ideal.span {f} ⊔ Ideal.span {y})) = contact f y := by1046 have h : Ideal.span {f} ⊔ Ideal.span {y} = Ideal.span ({f, y} : Set R) := by1047 rw [Set.insert_eq, Ideal.span_union]1048 rw [contact, h]1049 1050end SurfaceBlowup