Lean sources / SurfaceBlowup / Surfaces / Lengths.lean
Concrete surfaces, chart substitutions and lengths
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.HenselProducts7import Mathlib.FieldTheory.Finite.Extension8import Mathlib.RingTheory.AdicCompletion.Noetherian9import Mathlib.RingTheory.MvPowerSeries.Equiv10import Mathlib.RingTheory.PicardGroup11 12/-!13# Concrete surfaces, chart substitutions and lengths14 15This file sets up the local models used throughout the surface blow-up argument: power series16`k[[T,X]]` in two variables, the special fibers `k[[T,X]]/(T^a X^b)`, the concrete surfaces17`O[[T,X]]/(π - u T^a X^b)` over a discrete valuation ring `O`, the chart substitutions of the18blow-up, and the abstract `SurfaceData` with its state sets. It then proves the supporting19commutative algebra: ideals of `k[[T,X]]`, Gauss's count of irreducible polynomials over a finite20field, adic completeness of local rings and their quotients, and additivity of lengths of quotients.21 22## Main results23 24* `card_pow_eq_sum_irreducible_degrees`, `irreducible_count_moebius`: counting irreducible25 polynomials over a finite field.26* `axis_ideal_pow_mem_iff`, `axis_span_isPrime`: ideals generated by the variables of `k[[T,X]]`.27* `mvPowerSeries_fin_two_span_C_var_isPrime`: primality of `(c, X s)` in `A[[T,X]]`.28* `concrete_surface_contact_eq_special_fiber_contact`, `concrete_crossing_state_eq_union_cells`,29 `concrete_single_state_eq_union_cells`: state sets of the concrete surface via the special fiber.30* `iInf_sup_pow_eq_of_isLocalRing`, `isAdicComplete_of_isAdicComplete_maximalIdeal`,31 `isAdicComplete_quotient_of_iInf_sup_pow`: Krull intersection and adic completeness.32* `length_quotient_sup_mul_eq_add`, `length_quotient_sup_pow_eq_mul`: lengths of quotients.33 34Provenance: `Def_SurfaceBlowupV2_{LinearTowers, ResidueIdeals, ConcreteSurfaces, KillX,35SuccessorCharts, SurfaceData, TwoTermCokernels}` and the `Thm_SurfaceBlowupV2_*` nodes named after36the theorems of this file.37-/38 39noncomputable section40 41namespace SurfaceBlowup42 43/-! ### Definitions -/44 45section46variable (k : Type) [CommRing k] (V : ℕ → Type)47 [∀ j, AddCommGroup (V j)] [∀ j, Module k (V j)]48/-- The difference map `x ↦ (x j - r j (x (j+1)))_j` of an inverse system `(V j, r j)`. -/49def towerDelta (r : ∀ j, V (j + 1) →ₗ[k] V j) : (∀ j, V j) →ₗ[k] (∀ j, V j) where50 toFun x j := x j - r j (x (j+1))51 map_add' x y := by ext j; simp only [Pi.add_apply, map_add]; abel52 map_smul' a x := by ext j; simp only [Pi.smul_apply, map_smul, smul_sub, RingHom.id_apply]53/-- The compatible threads of an inverse system: the kernel of `towerDelta`. -/54def towerThreads (r : ∀ j, V (j + 1) →ₗ[k] V j) : Submodule k (∀ j, V j) :=55 LinearMap.ker (towerDelta k V r)56end57 58/-- Power series in two variables `T = X 0`, `X = X 1` over `k`. -/59abbrev TwoSeries (k : Type) [CommRing k] := MvPowerSeries (Fin 2) k60/-- The first variable `T` of `k[[T,X]]`. -/61noncomputable def axisT (k : Type) [CommRing k] : TwoSeries k := MvPowerSeries.X 062/-- The second variable `X` of `k[[T,X]]`. -/63noncomputable def axisX (k : Type) [CommRing k] : TwoSeries k := MvPowerSeries.X 164/-- The principal monomial ideal `(T^a X^b)` of `k[[T,X]]`. -/65noncomputable def monomialIdeal (k : Type) [CommRing k] (a b : ℕ) : Ideal (TwoSeries k) :=66 Ideal.span {axisT k ^ a * axisX k ^ b}67/-- The model special fiber `k[[T,X]] / (T^a X^b)`. -/68abbrev SpecialFiber (k : Type) [CommRing k] (a b : ℕ) := TwoSeries k ⧸ monomialIdeal k a b69/-- The image of `T` in the special fiber. -/70noncomputable def fiberT (k : Type) [CommRing k] (a b : ℕ) : SpecialFiber k a b :=71 Ideal.Quotient.mk _ (axisT k)72/-- The image of `X` in the special fiber. -/73noncomputable def fiberX (k : Type) [CommRing k] (a b : ℕ) : SpecialFiber k a b :=74 Ideal.Quotient.mk _ (axisX k)75/-- The contact number of `f` and `t`: the length of `B / (f, t)` as a `B`-module. -/76def contact {B : Type} [CommRing B] (f t : B) : ℕ∞ :=77 Module.length B (B ⧸ Ideal.span {f,t})78/-- Principal ideals of `k[[T,X]]/(T^a)` with contact `c` against `T`. -/79def singleResidueIdeals (k : Type) [CommRing k] (a c : ℕ) :=Allowed residue ideals, cells, occupied points80 {I : Ideal (SpecialFiber k a 0) // ∃ f, I=Ideal.span {f} ∧ contact f (fiberT k a 0)=c}81/-- Principal ideals of `k[[T,X]]/(T^a X^b)` with contacts `c` against `T` and `h` against `X`. -/82def crossingResidueIdeals (k : Type) [CommRing k] (a b c h : ℕ) :=Allowed residue ideals, cells, occupied points83 {I : Ideal (SpecialFiber k a b) // ∃ f, I=Ideal.span {f} ∧84 contact f (fiberT k a b)=c ∧ contact f (fiberX k a b)=h}85 86section Surface87variable (O : Type) [CommRing O]88/-- The defining relation `π - u T^a X^b` of the concrete surface. -/89noncomputable def surfaceRelation (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) : TwoSeries O :=90 MvPowerSeries.C pi - (u : TwoSeries O) * axisT O ^ a * axisX O ^ b91/-- The principal ideal generated by `surfaceRelation`. -/92noncomputable def surfaceIdeal (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) : Ideal (TwoSeries O) :=93 Ideal.span {surfaceRelation O pi u a b}94/-- The concrete surface `O[[T,X]] / (π - u T^a X^b)`. -/95abbrev ConcreteSurface (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :=(2.1)96 TwoSeries O ⧸ surfaceIdeal O pi u a b97/-- The quotient map onto the concrete surface. -/98noncomputable def surfaceMk (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :99 TwoSeries O →+* ConcreteSurface O pi u a b :=100 Ideal.Quotient.mk (surfaceIdeal O pi u a b)101/-- The image of `T` in the concrete surface. -/102noncomputable def surfaceT (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) : ConcreteSurface O pi u a b :=103 surfaceMk O pi u a b (axisT O)104/-- The image of `X` in the concrete surface. -/105noncomputable def surfaceX (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) : ConcreteSurface O pi u a b :=106 surfaceMk O pi u a b (axisX O)107/-- The image of the unit `u` in the concrete surface. -/108noncomputable def surfaceUnit (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :109 (ConcreteSurface O pi u a b)ˣ :=110 Units.map (surfaceMk O pi u a b).toMonoidHom u111/-- The ideal `(T, X)` of `O[[T,X]]`. -/112noncomputable def variableIdeal : Ideal (TwoSeries O) := Ideal.span {axisT O, axisX O}113/-- The ideal `(t, x)` of the concrete surface generated by the images of `T` and `X`. -/114noncomputable def surfaceParameterIdeal (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :115 Ideal (ConcreteSurface O pi u a b) :=116 Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b}117/-- Reduction of coefficients `O[[T,X]] → k[[T,X]]` to the residue field `k` of `O`. -/118noncomputable def residueSeries [IsLocalRing O] :119 TwoSeries O →+* TwoSeries (IsLocalRing.ResidueField O) :=120 MvPowerSeries.map (IsLocalRing.residue O)121end Surface122section Basis123variable {O M : Type} [CommRing O] [AddCommGroup M] [Module O M]124/-- `β` is a basis of `M / π M` over `O / π`: it spans modulo `π`, and its relations modulo `π`125have all coefficients divisible by `π`. -/126def ResidueBasisFamily (pi : O) {N : ℕ} (β : Fin N → M) : Prop :=127 (∀ m : M, ∃ z : Fin N → O, ∃ m' : M, m = (∑ i, z i • β i) + pi • m') ∧128 (∀ z : Fin N → O, (∃ m' : M, (∑ i, z i • β i) = pi • m') → ∀ i, pi ∣ z i)129end Basis130 131section132variable (O : Type) [CommRing O]133/-- The family killing X: the first variable goes to the one-variable variable, the second to 0. -/134noncomputable def killXFamily : Fin 2 → PowerSeries O := ![PowerSeries.X, 0]135/-- The family `killXFamily` is substitutable (zero constant coefficients). -/136theorem killXFamily_hasSubst : MvPowerSeries.HasSubst (killXFamily O) := by137 refine MvPowerSeries.hasSubst_of_constantCoeff_zero (fun s ↦ ?_)138 fin_cases s <;> simp [killXFamily, PowerSeries.X]139/-- `killX O : O[[T,X]] → O[[Y]]`, T ↦ Y, X ↦ 0 (Y the variable of the one-variable series ring). -/140noncomputable def killX : TwoSeries O →ₐ[O] PowerSeries O :=141 MvPowerSeries.substAlgHom (killXFamily_hasSubst O)142/-- `residueKillX O : O[[T,X]] → k[[Y]]`: kill the second variable, then reduce coefficients to143the residue field. -/144noncomputable def residueKillX [IsLocalRing O] :145 TwoSeries O →+* PowerSeries (IsLocalRing.ResidueField O) :=146 (MvPowerSeries.map (IsLocalRing.residue O)).comp (killX O).toRingHom147end148 149section Subst150variable (O : Type) [CommRing O]151/-- The substitution family of the t-chart point Z = α: T ↦ T, X ↦ T·(X + α) (x = tZ, Z = X + α). -/152noncomputable def tChartFamily (α : O) : Fin 2 → TwoSeries O :=153 ![axisT O, axisT O * (axisX O + MvPowerSeries.C α)]154/-- The family `tChartFamily` is substitutable (zero constant coefficients). -/155theorem tChartFamily_hasSubst (α : O) : MvPowerSeries.HasSubst (tChartFamily O α) := by156 refine MvPowerSeries.hasSubst_of_constantCoeff_zero (fun s ↦ ?_)157 fin_cases s <;> simp [tChartFamily, axisT, axisX]158/-- `chartSubst O α : O[[T,X]] → O[[T,X]]`, T ↦ T, X ↦ T·(X + α), as an O-algebra homomorphism. -/159noncomputable def chartSubst (α : O) : TwoSeries O →ₐ[O] TwoSeries O :=160 MvPowerSeries.substAlgHom (tChartFamily_hasSubst O α)161/-- The substitution family of the x-chart point W = 0: T ↦ T·X, X ↦ T (t = xW, T = x, X = W). -/162noncomputable def xChartFamily : Fin 2 → TwoSeries O := ![axisT O * axisX O, axisT O]163/-- The family `xChartFamily` is substitutable (zero constant coefficients). -/164theorem xChartFamily_hasSubst : MvPowerSeries.HasSubst (xChartFamily O) := by165 refine MvPowerSeries.hasSubst_of_constantCoeff_zero (fun s ↦ ?_)166 fin_cases s <;> simp [xChartFamily, axisT, axisX]167/-- `xChartSubst O : O[[T,X]] → O[[T,X]]`, T ↦ T·X, X ↦ T. -/168noncomputable def xChartSubst : TwoSeries O →ₐ[O] TwoSeries O :=169 MvPowerSeries.substAlgHom (xChartFamily_hasSubst O)170/-- The image of a unit under `chartSubst O α`. -/171noncomputable def substUnit (α : O) (u : (TwoSeries O)ˣ) : (TwoSeries O)ˣ :=172 Units.map (chartSubst O α).toRingHom.toMonoidHom u173/-- The image of a unit under `xChartSubst O`. -/174noncomputable def xSubstUnit (u : (TwoSeries O)ˣ) : (TwoSeries O)ˣ :=175 Units.map (xChartSubst O).toRingHom.toMonoidHom u176/-- `X + α` is a unit of `O[[T,X]]` when `α` is a unit of `O`. -/177private theorem isUnit_axisX_add_C (α : O) (hα : IsUnit α) : IsUnit178 (axisX O + MvPowerSeries.C α) := by179 rw [MvPowerSeries.isUnit_iff_constantCoeff]180 simpa [axisX] using hα181/-- The unit X + α of O[[T,X]] for a unit α of O. -/182noncomputable def shiftUnit (α : O) (hα : IsUnit α) : (TwoSeries O)ˣ :=183 (isUnit_axisX_add_C O α hα).unit184/-- Coefficient extension of a unit of O[[T,X]] along a ring homomorphism O → O'. -/185noncomputable def baseChangeUnit {O' : Type} [CommRing O'] (ρ : O →+* O') (u : (TwoSeries O)ˣ) :186 (TwoSeries O')ˣ :=187 Units.map (MvPowerSeries.map ρ).toMonoidHom u188/-- The family killing T: T ↦ 0, X ↦ X, with values in one-variable power series. -/189noncomputable def killTFamily : Fin 2 → PowerSeries O := ![0, PowerSeries.X]190/-- The family `killTFamily` is substitutable (zero constant coefficients). -/191theorem killTFamily_hasSubst : MvPowerSeries.HasSubst (killTFamily O) := by192 refine MvPowerSeries.hasSubst_of_constantCoeff_zero (fun s ↦ ?_)193 fin_cases s <;> simp [killTFamily, PowerSeries.X]194/-- `killT O : O[[T,X]] → O[[X]]`, T ↦ 0, X ↦ X. -/195noncomputable def killT : TwoSeries O →ₐ[O] PowerSeries O :=196 MvPowerSeries.substAlgHom (killTFamily_hasSubst O)197/-- `residueKillT O : O[[T,X]] → k[[X]]`: kill T, then reduce coefficients to the residue field. -/198noncomputable def residueKillT [IsLocalRing O] :199 TwoSeries O →+* PowerSeries (IsLocalRing.ResidueField O) :=200 (MvPowerSeries.map (IsLocalRing.residue O)).comp (killT O).toRingHom201end Subst202section Eval203variable {O S : Type} [CommRing O] [CommRing S]204/-- The constant family (e, z) of a ring S, viewed in `MvPowerSeries Unit S`. -/205noncomputable def nilpotentFamily (e z : S) : Fin 2 → MvPowerSeries Unit S :=206 ![MvPowerSeries.C e, MvPowerSeries.C z]207/-- A family of two nilpotent constants is substitutable. -/208theorem nilpotentFamily_hasSubst (e z : S) (he : IsNilpotent e) (hz : IsNilpotent z) :209 MvPowerSeries.HasSubst (nilpotentFamily e z) := by210 refine MvPowerSeries.hasSubst_of_constantCoeff_nilpotent (fun s ↦ ?_)211 fin_cases s <;> simpa [nilpotentFamily]212/-- Evaluation of a series of `O[[T,X]]` at two nilpotent elements `e, z` of a ring `S` along213`φ : O → S`: `nilpotentEval φ e z he hz f = f(e, z)`, a ring homomorphism (substitution followed214by the constant coefficient of the resulting constant series in `MvPowerSeries Unit S`). -/215noncomputable def nilpotentEval (φ : O →+* S) (e z : S) (he : IsNilpotent e) (hz : IsNilpotent z) :216 TwoSeries O →+* S :=217 (MvPowerSeries.constantCoeff : MvPowerSeries Unit S →+* S).comp218 ((MvPowerSeries.substAlgHom (nilpotentFamily_hasSubst e z he hz)).toRingHom.comp219 (MvPowerSeries.map φ))220end Eval221 222section223variable (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]224 [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]225/-- Data of a regular complete two-dimensional local `O`-algebra `R` with parameters `t, x`,226residue field identified with that of `O`, and vertical equation `π = unit · t^a x^b`. -/227structure SurfaceData where(2.1)228 pi : O229 pi_irreducible : Irreducible pi230 t : R231 x : R232 unit : Rˣ233 a : ℕ234 b : ℕ235 a_pos : 0 < a236 parameters : Ideal.span {t,x} = IsLocalRing.maximalIdeal R237 dimension : ringKrullDim R = 2238 complete : IsAdicComplete (IsLocalRing.maximalIdeal R) R239 base_injective : Function.Injective (algebraMap O R)240 residueEquiv : IsLocalRing.ResidueField O ≃+* IsLocalRing.ResidueField R241 residue_compat : ∀ c : O, residueEquiv (IsLocalRing.residue O c) =242 IsLocalRing.residue R (algebraMap O R c)243 vertical : algebraMap O R pi = (unit : R) * t^a * x^b244/-- The contact length of an ideal `J` against `y`: the length of `R / (J + (y))`. -/245def idealContact (J : Ideal R) (y : R) : ℕ∞ :=246 Module.length R (R ⧸ (J ⊔ Ideal.span {y}))247/-- The principal ideals of `R` realising the combinatorial state `s` relative to `S`. -/248def surfaceStateSet (S : SurfaceData O R) (s : State) : Set (Ideal R) :=(2.1)249 {J | (∃ f : R, J = Ideal.span {f}) ∧ s.Valid ∧250 match s with251 | .single a c => S.a = a ∧ S.b = 0 ∧ idealContact R J S.t = c252 | .crossing a b c h => S.a = a ∧ S.b = b ∧253 idealContact R J S.t = c ∧ idealContact R J S.x = h}254/-- `J` has multiplicity `d`: it lies in `𝔪^d` but not in `𝔪^(d+1)`. -/255def HasMultiplicity (J : Ideal R) (d : ℕ) : Prop :=256 J ≤ (IsLocalRing.maximalIdeal R)^d ∧ ¬ J ≤ (IsLocalRing.maximalIdeal R)^(d+1)257end258 259section260variable {O A0 A1 B0 B1 : Type} [CommRing O]261 [AddCommGroup A0] [Module O A0] [AddCommGroup A1] [Module O A1]262 [AddCommGroup B0] [Module O B0] [AddCommGroup B1] [Module O B1]263/-- The map on cokernels induced by a morphism of two-term complexes. -/264def twoTermCokerMap (dA : A0 →ₗ[O] A1) (dB : B0 →ₗ[O] B1)265 (u0 : A0 →ₗ[O] B0) (u1 : A1 →ₗ[O] B1)266 (h : u1.comp dA = dB.comp u0) :267 (A1 ⧸ LinearMap.range dA) →ₗ[O] (B1 ⧸ LinearMap.range dB) :=268 (LinearMap.range dA).mapQ (LinearMap.range dB) u1 (by269 rintro y ⟨x, rfl⟩270 change u1 (dA x) ∈ LinearMap.range dB271 refine ⟨u0 x, ?_⟩272 exact (congrArg (fun v : A0 →ₗ[O] B1 ↦ v x) h).symm)273end274 275/-! ### Finite fields -/276 277/-- Over a finite field with `q` elements, `X^(q^m) - X` is the product of the monic irreducible278polynomials whose degree divides `m`. -/279private theorem X_pow_card_pow_sub_X_eq_prod_irreducible (k : Type) [Field k] [Finite k] (m : ℕ)280 (hm : 0 < m) (S : Finset (Polynomial k))281 (hS : ∀ g, g ∈ S ↔ g.Monic ∧ Irreducible g ∧ g.natDegree ∣ m) :282 (Polynomial.X ^ (Nat.card k) ^ m - Polynomial.X : Polynomial k) = ∏ g ∈ S, g := by283 classical284 set P : Polynomial k := Polynomial.X ^ (Nat.card k) ^ m - Polynomial.X with hPdef285 have hq : 1 < Nat.card k := Finite.one_lt_card286 have hP0 : P ≠ 0 := FiniteField.X_pow_card_pow_sub_X_ne_zero k hm.ne' hq287 have hPsep : Squarefree P := by288 obtain ⟨p, hp⟩ := CharP.exists k289 have := Fintype.ofFinite k290 have : Fact p.Prime := ⟨CharP.char_is_prime k p⟩291 obtain ⟨n, hn, hcard⟩ := FiniteField.card k p292 have hdvd : p ∣ Nat.card k ^ m := by293 rw [Nat.card_eq_fintype_card, hcard, ← pow_mul]294 exact dvd_pow_self p (Nat.mul_ne_zero n.ne_zero hm.ne')295 exact (galois_poly_separable p _ hdvd).squarefree296 set N := UniqueFactorizationMonoid.normalizedFactors P with hN297 have hnodup : N.Nodup :=298 (UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hP0).mp hPsep299 have hmonic : ∀ g ∈ N, g.Monic ∧ Irreducible g := fun g hg ↦ by300 have hirr := UniqueFactorizationMonoid.irreducible_of_normalized_factor g hg301 refine ⟨?_, hirr⟩302 rw [← UniqueFactorizationMonoid.normalize_normalized_factor g hg]303 exact Polynomial.monic_normalize hirr.ne_zero304 have hprod : N.prod = P := by305 apply Polynomial.eq_of_monic_of_associated306 · simpa using Polynomial.monic_multiset_prod_of_monic N id (fun g hg ↦ (hmonic g hg).1)307 · rw [hPdef]308 apply Polynomial.Monic.sub_of_left (Polynomial.monic_X_pow _)309 rw [Polynomial.degree_X, Polynomial.degree_X_pow]310 exact_mod_cast Nat.one_lt_pow hm.ne' hq311 · exact UniqueFactorizationMonoid.prod_normalizedFactors hP0312 have hset : N.toFinset = S := by313 ext g314 rw [Multiset.mem_toFinset, hS]315 constructor316 · intro hg317 obtain ⟨h1, h2⟩ := hmonic g hg318 exact ⟨h1, h2, h2.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X319 (UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hg)⟩320 · rintro ⟨h1, h2, h3⟩321 have hd : g ∣ P := h2.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_X.mp h3322 obtain ⟨g', hg', hass⟩ :=323 UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd hP0 h2 hd324 rwa [Polynomial.eq_of_monic_of_associated h1 (hmonic g' hg').1 hass]325 rw [← hset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val, Multiset.map_id',326 Multiset.dedup_eq_self.mpr hnodup, hprod]327 328/-- Gauss's formula: `q^m = ∑_{d ∣ m} d · #{monic irreducible polynomials of degree d}`. -/329theorem card_pow_eq_sum_irreducible_degrees (k : Type) [Field k] [Finite k] (m : ℕ) (hm : 0 < m) :(6.2)330 (Nat.card k) ^ m = ∑ d ∈ m.divisors, d *331 Nat.card {g : Polynomial k // g.Monic ∧ Irreducible g ∧ g.natDegree = d} := by332 have hMD : ∀ d, ({F : Polynomial k | F.Monic ∧ F.natDegree = d} : Set _).Finite := by333 intro d334 rw [← Set.finite_coe_iff]335 apply Nat.finite_of_card_ne_zero336 change Nat.card {F : Polynomial k // F.Monic ∧ F.natDegree = d} ≠ 0337 rw [monic_residue_polynomial_count]338 exact pow_ne_zero _ Nat.card_pos.ne'339 have hSig : ({g : Polynomial k | g.Monic ∧ Irreducible g ∧ g.natDegree ∣ m} : Set _).Finite := by340 apply Set.Finite.subset ((Finset.finite_toSet m.divisors).biUnion (fun d _ ↦ hMD d))341 intro g hg342 simp only [Set.mem_ofPred_eq] at hg343 simp only [Set.mem_iUnion, Set.mem_ofPred_eq, Finset.mem_coe, Nat.mem_divisors]344 exact ⟨g.natDegree, ⟨hg.2.2, hm.ne'⟩, hg.1, rfl⟩345 set S := hSig.toFinset with hSdef346 have hS : ∀ g, g ∈ S ↔ g.Monic ∧ Irreducible g ∧ g.natDegree ∣ m := by347 intro g; rw [hSdef, Set.Finite.mem_toFinset]; rfl348 have hprod := X_pow_card_pow_sub_X_eq_prod_irreducible k m hm S hS349 have hdeg := congrArg Polynomial.natDegree hprod350 rw [FiniteField.X_pow_card_pow_sub_X_natDegree_eq k hm.ne' Finite.one_lt_card,351 Polynomial.natDegree_prod_of_monic _ _ (fun g hg ↦ ((hS g).1 hg).1)] at hdeg352 rw [hdeg, ← Finset.sum_fiberwise_of_maps_to (g := Polynomial.natDegree) (t := m.divisors)353 (fun g hg ↦ Nat.mem_divisors.2 ⟨((hS g).1 hg).2.2, hm.ne'⟩)]354 apply Finset.sum_congr rfl355 intro d hd356 have hd' := (Nat.mem_divisors.1 hd).1357 rw [Finset.sum_congr rfl (g := fun _ ↦ d) (fun g hg ↦ (Finset.mem_filter.1 hg).2),358 Finset.sum_const, smul_eq_mul, mul_comm]359 congr 1360 rw [← Nat.card_eq_finsetCard]361 refine Nat.card_congr (Equiv.subtypeEquivRight fun g ↦ ?_)362 rw [Finset.mem_filter, hS]363 exact ⟨fun ⟨⟨h1, h2, _⟩, h4⟩ ↦ ⟨h1, h2, h4⟩, fun ⟨h1, h2, h4⟩ ↦ ⟨⟨h1, h2, h4 ▸ hd'⟩, h4⟩⟩364 365/-- Möbius inversion of Gauss's formula: `δ · N_δ = ∑_{j ∣ δ} μ(j) q^(δ/j)`. -/366theorem irreducible_count_moebius (k : Type) [Field k] [Finite k] (δ : ℕ) (hδ : 0 < δ) :(6.2)367 (δ : ℚ) * (Nat.card {g : Polynomial k // g.Monic ∧ Irreducible g ∧ g.natDegree = δ} : ℕ) =368 ∑ j ∈ δ.divisors, ((ArithmeticFunction.moebius j : ℤ) : ℚ) * (Nat.card k : ℚ) ^ (δ / j) := by369 have h := (ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq (R := ℚ)370 (f := fun d ↦371 (d : ℚ) * (Nat.card {g : Polynomial k // g.Monic ∧ Irreducible g ∧ g.natDegree = d} : ℕ))372 (g := fun n ↦ (Nat.card k : ℚ) ^ n)).mp (by373 intro n hn374 have := congrArg (fun x : ℕ ↦ (x : ℚ))375 (card_pow_eq_sum_irreducible_degrees k n hn)376 simpa [Nat.cast_sum, Nat.cast_mul, Nat.cast_pow] using this.symm) δ hδ377 rw [← h, Nat.sum_divisorsAntidiagonal378 (fun i j ↦ ((ArithmeticFunction.moebius i : ℤ) : ℚ) * (Nat.card k : ℚ) ^ j)]379 380/-! ### Ideals of `k[[T,X]]` -/381 382private noncomputable def lowOrderIdeal (k : Type) [CommRing k] (n : ℕ) : Ideal (TwoSeries k) where383 carrier := {φ | ∀ m : Fin 2 →₀ ℕ, m 0 + m 1 < n → MvPowerSeries.coeff m φ = 0}384 zero_mem' := by simp385 add_mem' ha hb m hm := by simp [ha m hm, hb m hm]386 smul_mem' c x hx m hm := by387 rw [smul_eq_mul, MvPowerSeries.coeff_mul]388 apply Finset.sum_eq_zero389 intro p hp390 rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp391 have h0 := congrArg (fun f ↦ f 0) hp392 have h1 := congrArg (fun f ↦ f 1) hp393 simp only [Finsupp.add_apply] at h0 h1394 rw [hx p.2 (by omega), mul_zero]395 396private lemma lowOrderIdeal_mul (k : Type) [CommRing k]397 (a b : ℕ) : lowOrderIdeal k a * lowOrderIdeal k b ≤ lowOrderIdeal k (a + b) := by398 rw [Ideal.mul_le]399 intro x hx y hy m hm400 rw [MvPowerSeries.coeff_mul]401 apply Finset.sum_eq_zero402 intro p hp403 rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp404 have h0 := congrArg (fun f ↦ f 0) hp405 have h1 := congrArg (fun f ↦ f 1) hp406 simp only [Finsupp.add_apply] at h0 h1407 by_cases h : p.1 0 + p.1 1 < a408 · rw [hx p.1 h, zero_mul]409 · rw [hy p.2 (by omega), mul_zero]410 411private lemma lowOrderIdeal_zero (k : Type) [CommRing k] : lowOrderIdeal k 0 = ⊤ :=412 eq_top_iff.2 fun _ _ _ hm ↦ by omega413 414private lemma span_le_lowOrderIdeal_one (k : Type) [CommRing k] : Ideal.span415 {axisT k, axisX k} ≤ lowOrderIdeal k 1 := by416 rw [Ideal.span_le]417 have key (s : Fin 2) : (MvPowerSeries.X s : TwoSeries k) ∈ lowOrderIdeal k 1 := fun m hm ↦ by418 obtain rfl : m = 0 := by ext i; fin_cases i <;> simp <;> omega419 exact MvPowerSeries.coeff_zero_X s420 rintro x (rfl | rfl)421 exacts [key 0, key 1]422 423private lemma pow_le_lowOrderIdeal (k : Type) [CommRing k] (L : ℕ) :424 (Ideal.span {axisT k, axisX k})^L ≤ lowOrderIdeal k L := by425 induction L with426 | zero => rw [pow_zero, Ideal.one_eq_top, lowOrderIdeal_zero]427 | succ L ih =>428 rw [pow_succ]429 exact (Ideal.mul_mono ih (span_le_lowOrderIdeal_one k)).trans (lowOrderIdeal_mul k L 1)430 431private lemma lowOrderIdeal_le_pow (k : Type) [CommRing k] (L : ℕ) :432 lowOrderIdeal k L ≤ (Ideal.span {axisT k, axisX k})^L := by433 have key (s : Fin 2) (a : TwoSeries k) (m : Fin 2 →₀ ℕ) :434 MvPowerSeries.coeff (m + Finsupp.single s 1) (MvPowerSeries.X s * a) =435 MvPowerSeries.coeff m a := by436 rw [MvPowerSeries.X, MvPowerSeries.coeff_monomial_mul, if_pos le_add_self,437 add_tsub_cancel_right, one_mul]438 induction L with439 | zero => simp440 | succ N ih =>441 intro g hg442 -- split `g = T a + X b`, where `X b` collects the terms not divisible by `T`443 set g1 : TwoSeries k := fun m ↦ if m 0 = 0 then MvPowerSeries.coeff m g else 0444 have c1 (m) : MvPowerSeries.coeff m g1 = if m 0 = 0 then MvPowerSeries.coeff m g else 0 :=445 rfl446 obtain ⟨a, ha⟩ : MvPowerSeries.X 0 ∣ g - g1 := by447 refine MvPowerSeries.X_dvd_iff.2 fun m hm ↦ ?_448 rw [map_sub, c1, if_pos hm, sub_self]449 obtain ⟨b, hb⟩ : MvPowerSeries.X 1 ∣ g1 := by450 refine MvPowerSeries.X_dvd_iff.2 fun m hm ↦ ?_451 rw [c1]452 split_ifs with h453 · exact hg m (by omega)454 · rfl455 have hA : a ∈ lowOrderIdeal k N := fun m hm ↦ by456 rw [← key 0 a m, ← ha, map_sub, c1, if_neg (by simp), sub_zero]457 exact hg _ (by simp; omega)458 have hB : b ∈ lowOrderIdeal k N := fun m hm ↦ by459 rw [← key 1 b m, ← hb, c1]460 split_ifs with h461 · exact hg _ (by simp; omega)462 · rfl463 rw [show g = (g - g1) + g1 by ring, ha, hb, pow_succ']464 exact Ideal.add_mem _ (Ideal.mul_mem_mul (Ideal.subset_span (by simp [axisT])) (ih hA))465 (Ideal.mul_mem_mul (Ideal.subset_span (by simp [axisX])) (ih hB))466 467/-- A series lies in `(T, X)^L` iff all its coefficients of total degree `< L` vanish. -/468theorem axis_ideal_pow_mem_iff (k : Type) [CommRing k] (L : ℕ) (φ : TwoSeries k) :469 φ ∈ (Ideal.span {axisT k, axisX k})^L ↔ ∀ m : Fin 2 →₀ ℕ, m 0 + m 1 < L →470 MvPowerSeries.coeff m φ = 0 :=471 ⟨fun h ↦ pow_le_lowOrderIdeal k L h, fun h ↦ lowOrderIdeal_le_pow k L h⟩472 473/-- The quotient of `k[[T,X]]` by one variable has infinite length. -/474theorem axis_quotient_length_top (k : Type) [Field k] (s t : Fin 2) (hst : s ≠ t) :475 Module.length (TwoSeries k) (TwoSeries k ⧸ Ideal.span {(MvPowerSeries.X s : TwoSeries k)}) =476 ⊤ := by477 set P : Ideal (TwoSeries k) := Ideal.span {(MvPowerSeries.X s : TwoSeries k)} with hP478 let N : ℕ → Submodule (TwoSeries k) (TwoSeries k ⧸ P) := fun j ↦479 Submodule.map P.mkQ (Ideal.span {(MvPowerSeries.X t : TwoSeries k) ^ j})480 have hle : ∀ j, N (j+1) ≤ N j := fun j ↦ by481 apply Submodule.map_mono482 rw [Ideal.span_singleton_le_span_singleton]483 exact pow_dvd_pow _ (Nat.le_succ j)484 have hlt : ∀ j, N (j+1) < N j := fun j ↦ by485 refine lt_of_le_of_ne (hle j) fun heq ↦ ?_486 have hmem : P.mkQ ((MvPowerSeries.X t : TwoSeries k) ^ j) ∈ N j :=487 Submodule.mem_map_of_mem (Ideal.mem_span_singleton_self _)488 rw [← heq] at hmem489 obtain ⟨y, hy, hyeq⟩ := hmem490 rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.eq] at hyeq491 rw [hP, Ideal.mem_span_singleton] at hyeq492 rw [SetLike.mem_coe, Ideal.mem_span_singleton] at hy493 have h1 := (MvPowerSeries.X_dvd_iff).1 hyeq (Finsupp.single t j)494 (Finsupp.single_eq_of_ne (by simpa [eq_comm] using hst))495 have h2 := (MvPowerSeries.X_pow_dvd_iff).1 hy (Finsupp.single t j)496 (by rw [Finsupp.single_eq_same]; omega)497 rw [map_sub, h2, MvPowerSeries.coeff_X_pow] at h1498 simp at h1499 -- a strictly descending chain of submodules rules out finite length500 by_contra h501 rw [← ne_eq, Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at h502 have := h.2503 obtain ⟨n, hn⟩ := WellFounded.not_rel_apply_succ (r := (· < ·)) N504 exact hn (hlt n)505 506/-- Coefficients of a substitution `T ↦ Y, X ↦ 0` (or `T ↦ 0, X ↦ Y`) into one-variable power507series: the `n`-th coefficient is the coefficient of `Y^n` on the surviving axis `t`. -/508theorem coeff_substAlgHom_kill (O : Type) [CommRing O] (f : Fin 2 → PowerSeries O)509 (hf : MvPowerSeries.HasSubst f) (s t : Fin 2) (hst : s ≠ t) (hs : f s = 0)510 (ht : f t = PowerSeries.X) (g : TwoSeries O) (n : ℕ) :511 PowerSeries.coeff n (MvPowerSeries.substAlgHom hf g) =512 MvPowerSeries.coeff (Finsupp.single t n) g := by513 have hprod (d : Fin 2 →₀ ℕ) : d.prod (fun i e ↦ f i ^ e) = f s ^ d s * f t ^ d t := by514 rw [Finsupp.prod_fintype _ _ (by simp), Fin.prod_univ_two]515 obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ : s = 0 ∧ t = 1 ∨ s = 1 ∧ t = 0 := by omega516 exacts [rfl, mul_comm _ _]517 rw [MvPowerSeries.coe_substAlgHom, PowerSeries.coeff_def (s := Finsupp.single () n) (by simp),518 MvPowerSeries.coeff_subst hf, finsum_eq_single _ (Finsupp.single t n)]519 · simp [hprod, hs, ht, Finsupp.single_eq_of_ne hst, ← PowerSeries.coeff_def]520 · intro d hd521 rw [hprod, hs, ht]522 by_cases h0 : d s = 0523 · have h1 : d t ≠ n := fun h1 ↦ hd (by524 ext i525 obtain rfl | rfl : i = s ∨ i = t := by omega526 exacts [by simp [h0, Finsupp.single_eq_of_ne hst], by simp [h1]])527 rw [← PowerSeries.coeff_def (n := n) (by simp)]528 simp [h0, PowerSeries.coeff_X_pow, Ne.symm h1]529 · simp [zero_pow h0]530 531/-- A series lies in `(c, X s)` iff `c` divides every coefficient whose `s`-exponent is zero. -/532theorem mvPowerSeries_mem_span_C_var_iff (σ A : Type) [CommRing A] (c : A) (s : σ)533 (g : MvPowerSeries σ A) :534 g ∈ Ideal.span {(MvPowerSeries.C c : MvPowerSeries σ A), MvPowerSeries.X s} ↔535 ∀ m : σ →₀ ℕ, m s = 0 → c ∣ MvPowerSeries.coeff m g := by536 rw [Ideal.mem_span_pair]537 constructor538 · rintro ⟨a, b, rfl⟩ m hm539 have hX : MvPowerSeries.coeff m (b * MvPowerSeries.X s) = 0 :=540 MvPowerSeries.X_dvd_iff.mp (dvd_mul_left _ _) m hm541 rw [map_add, hX, add_zero, MvPowerSeries.coeff_mul_C]542 exact dvd_mul_left _ _543 · intro h544 let q : MvPowerSeries σ A := fun m ↦545 if hm : m s = 0 then Classical.choose (h m hm) else 0546 have hq : ∀ m, m s = 0 → MvPowerSeries.coeff m (MvPowerSeries.C c * q) =547 MvPowerSeries.coeff m g := by548 intro m hm549 rw [MvPowerSeries.coeff_C_mul]550 have : MvPowerSeries.coeff m q = Classical.choose (h m hm) := by551 change (if hm : m s = 0 then _ else 0) = _552 rw [dif_pos hm]553 rw [this]554 exact (Classical.choose_spec (h m hm)).symm555 obtain ⟨r, hr⟩ : (MvPowerSeries.X s : MvPowerSeries σ A) ∣ g - MvPowerSeries.C c * q := by556 rw [MvPowerSeries.X_dvd_iff]557 intro m hm558 rw [map_sub, hq m hm, sub_self]559 refine ⟨q, r, ?_⟩560 rw [mul_comm q, mul_comm r, ← hr]561 ring562 563/-- If `(c)` is prime in `A`, then `(c, X s)` is prime in `A[[X 0, X 1]]`: it is the kernel of564killing `X s` and reducing the coefficients modulo `c`, with values in the domain `(A/(c))[[Y]]`. -/565theorem mvPowerSeries_fin_two_span_C_var_isPrime (A : Type) [CommRing A] (c : A)566 (hc : (Ideal.span {c}).IsPrime) (s : Fin 2) :567 (Ideal.span {(MvPowerSeries.C c : MvPowerSeries (Fin 2) A), MvPowerSeries.X s}).IsPrime := by568 obtain ⟨t, hts, φ, hφ⟩ : ∃ t ≠ s, ∃ φ : TwoSeries A →+* PowerSeries A,569 ∀ g n, PowerSeries.coeff n (φ g) = MvPowerSeries.coeff (Finsupp.single t n) g := by570 obtain rfl | rfl : s = 0 ∨ s = 1 := by omega571 exacts [⟨1, by decide, _, coeff_substAlgHom_kill A _ (killTFamily_hasSubst A) 0 1572 (by decide) rfl rfl⟩, ⟨0, by decide, _, coeff_substAlgHom_kill A _573 (killXFamily_hasSubst A) 1 0 (by decide) rfl rfl⟩]574 convert RingHom.ker_isPrime ((PowerSeries.map (Ideal.Quotient.mk (Ideal.span {c}))).comp φ)575 ext g576 rw [mvPowerSeries_mem_span_C_var_iff, RingHom.mem_ker, PowerSeries.ext_iff]577 simp only [RingHom.comp_apply, PowerSeries.coeff_map, hφ, map_zero,578 Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]579 refine ⟨fun h n ↦ h _ (by simp [hts.symm]), fun h m hm ↦ ?_⟩580 convert h (m t)581 ext i582 obtain rfl | rfl : i = s ∨ i = t := by omega583 · simp [hm, hts.symm]584 · simp585 586/-- Each variable generates a prime ideal of `k[[T,X]]`. -/587theorem axis_span_isPrime (k : Type) [CommRing k] [IsDomain k] (s : Fin 2) :588 (Ideal.span {(MvPowerSeries.X s : TwoSeries k)}).IsPrime := by589 simpa using mvPowerSeries_fin_two_span_C_var_isPrime k 0 (by simpa using Ideal.isPrime_bot) s590 591/-- If `F` is not divisible by the variable `X s`, then `X s ^ n * G ∈ (F)` implies `G ∈ (F)`. -/592theorem axis_pow_mul_mem_span_cancel (k : Type) [Field k] (s : Fin 2) (F : TwoSeries k)593 (hF : F ∉ Ideal.span {(MvPowerSeries.X s : TwoSeries k)}) (n : ℕ) (G : TwoSeries k)594 (hG : (MvPowerSeries.X s : TwoSeries k) ^ n * G ∈ Ideal.span {F}) :595 G ∈ Ideal.span {F} := by596 have hX : (MvPowerSeries.X s : TwoSeries k) ≠ 0 := fun h ↦ by597 simpa [h] using MvPowerSeries.coeff_index_single_self_X (R := k) s598 have step : ∀ H : TwoSeries k, (MvPowerSeries.X s : TwoSeries k) * H ∈ Ideal.span {F} →599 H ∈ Ideal.span {F} := by600 intro H hH601 obtain ⟨Y, hY⟩ := Ideal.mem_span_singleton'.mp hH602 have hmem : Y * F ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k)} := by603 rw [hY]; exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)604 rcases (axis_span_isPrime k s).mem_or_mem hmem with hY1 | hF1605 · obtain ⟨Y₁, rfl⟩ := Ideal.mem_span_singleton'.mp hY1606 have : H = Y₁ * F := by607 apply mul_left_cancel₀ hX608 rw [← hY]; ring609 rw [this]; exact Ideal.mul_mem_left _ _ (Ideal.subset_span rfl)610 · exact absurd hF1 hF611 induction n generalizing G with612 | zero => simpa using hG613 | succ n ih => exact step _ (ih _ (by rwa [← mul_assoc, ← pow_succ]))614 615/-! ### Chart substitutions -/616 617/-- Values of the chart substitutions `chartSubst`, `xChartSubst` and `killT` on constants and618on the two variables. -/619theorem chartSubst_apply_generators (O : Type) [CommRing O] (α : O) :620 (∀ c : O, chartSubst O α (MvPowerSeries.C c) = MvPowerSeries.C c) ∧621 chartSubst O α (axisT O) = axisT O ∧622 chartSubst O α (axisX O) = axisT O * (axisX O + MvPowerSeries.C α) ∧623 (∀ c : O, xChartSubst O (MvPowerSeries.C c) = MvPowerSeries.C c) ∧624 xChartSubst O (axisT O) = axisT O * axisX O ∧ xChartSubst O (axisX O) = axisT O ∧625 (∀ c : O, killT O (MvPowerSeries.C c) = PowerSeries.C c) ∧ killT O (axisT O) = 0 ∧626 killT O (axisX O) = PowerSeries.X := by627 have h₁ := tChartFamily_hasSubst O α628 have h₂ := xChartFamily_hasSubst O629 have h₃ := killTFamily_hasSubst O630 refine ⟨fun c ↦ ?_, ?_, ?_, fun c ↦ ?_, ?_, ?_, fun c ↦ ?_, ?_, ?_⟩ <;>631 simp only [chartSubst, xChartSubst, killT, MvPowerSeries.substAlgHom_apply, axisT, axisX,632 MvPowerSeries.subst_X h₁, MvPowerSeries.subst_X h₂, MvPowerSeries.subst_X h₃] <;>633 simp [MvPowerSeries.subst_C, tChartFamily, xChartFamily, killTFamily, axisT, axisX]634 rfl635 636/-- The t-chart substitution at `α` of the base-changed surface relation. -/637private theorem chartSubst_surfaceRelation (O O' : Type) [CommRing O] [CommRing O'] (ρ : O →+* O')638 (α : O')639 (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :640 chartSubst O' α (MvPowerSeries.map ρ (surfaceRelation O pi u a b)) = MvPowerSeries.C (ρ pi) -641 (substUnit O' α (baseChangeUnit O ρ u) : TwoSeries O') * axisT O' ^ (a + b) *642 (axisX O' + MvPowerSeries.C α) ^ b := by643 obtain ⟨hC, hT, hX, -⟩ := chartSubst_apply_generators O' α644 have mT : MvPowerSeries.map ρ (axisT O) = axisT O' := MvPowerSeries.map_X _ _645 have mX : MvPowerSeries.map ρ (axisX O) = axisX O' := MvPowerSeries.map_X _ _646 simp only [surfaceRelation, map_sub, map_mul, map_pow, MvPowerSeries.map_C, mT, mX, hC, hT, hX]647 have : ((substUnit O' α (baseChangeUnit O ρ u) : (TwoSeries O')ˣ) : TwoSeries O') =648 chartSubst O' α (MvPowerSeries.map ρ (u : TwoSeries O)) := rfl649 rw [this, pow_add, mul_pow]650 ring651 652/-- The surface relation after the t-chart substitution at a unit `θ` (with base change)653and after the x-chart substitution is again a surface relation. -/654theorem chartSubst_surfaceRelation_base_change_and_x_chart (O O' : Type) [CommRing O] [CommRing O']655 (ρ : O →+* O') (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :656 (∀ (θ : O') (hθ : IsUnit θ), chartSubst O' θ657 (MvPowerSeries.map ρ (surfaceRelation O pi u a b)) =658 surfaceRelation O' (ρ pi) (substUnit O' θ (baseChangeUnit O ρ u) * shiftUnit O' θ hθ ^ b)659 (a + b) 0) ∧660 xChartSubst O (surfaceRelation O pi u a b) =661 surfaceRelation O pi (xSubstUnit O u) (a + b) a := by662 constructor663 · intro θ hθ664 rw [chartSubst_surfaceRelation]665 have h : ((shiftUnit O' θ hθ : (TwoSeries O')ˣ) : TwoSeries O') =666 axisX O' + MvPowerSeries.C θ := rfl667 simp only [surfaceRelation, Units.val_mul, Units.val_pow_eq_pow_val, h, pow_zero, mul_one]668 ring669 · obtain ⟨hC, -, -, hxC, hxT, hxX, -⟩ := chartSubst_apply_generators O 0670 have hx : ((xSubstUnit O u : (TwoSeries O)ˣ) : TwoSeries O) =671 xChartSubst O (u : TwoSeries O) := rfl672 simp only [surfaceRelation, map_sub, map_mul, map_pow, hxC, hxT, hxX, hx]673 ring674 675/-- The surface relation after the t-chart substitution at the origin and at a unit point is676again a surface relation. -/677theorem chartSubst_surfaceRelation_origin_and_unit_point (O : Type) [CommRing O] (pi : O)678 (u : (TwoSeries O)ˣ) (a b : ℕ) :679 chartSubst O 0 (surfaceRelation O pi u a b) = surfaceRelation O pi (substUnit O 0 u) (a + b) b ∧680 ∀ (α : O) (hα : IsUnit α), chartSubst O α (surfaceRelation O pi u a b) =681 surfaceRelation O pi (substUnit O α u * shiftUnit O α hα ^ b) (a + b) 0 := by682 have key : ∀ α : O, chartSubst O α (surfaceRelation O pi u a b) =683 MvPowerSeries.C pi - (substUnit O α u : TwoSeries O) * axisT O ^ (a + b) *684 (axisX O + MvPowerSeries.C α) ^ b := by685 intro α686 have h := chartSubst_surfaceRelation O O (RingHom.id O) α pi u a b687 have hb : baseChangeUnit O (RingHom.id O) u = u := by688 ext1; simp [baseChangeUnit]689 rw [hb] at h690 simpa using h691 refine ⟨?_, ?_⟩692 · rw [key 0]; simp [surfaceRelation]693 · intro α hα694 rw [key α]695 have : (shiftUnit O α hα : TwoSeries O) = axisX O + MvPowerSeries.C α := rfl696 simp only [surfaceRelation, Units.val_mul, Units.val_pow_eq_pow_val, this, pow_zero, mul_one]697 ring698 699/-! ### Concrete surfaces -/700 701/-- The pullback of the maximal ideal of a local ring `S` along `Λ : A → S` is maximal when702`Λ` is surjective modulo the maximal ideal. -/703theorem chart_point_isMaximal_of_residue_surjective (A S : Type) [CommRing A] [CommRing S]704 [IsLocalRing S] (Λ : A →+* S) (hsurj : ∀ y : S, ∃ x : A, Λ x - y ∈ IsLocalRing.maximalIdeal S) :705 ((IsLocalRing.maximalIdeal S).comap Λ).IsMaximal := by706 let : Field (S ⧸ IsLocalRing.maximalIdeal S) := Ideal.Quotient.field _707 have hs : Function.Surjective ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal S)).comp Λ) := by708 intro q709 obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective q710 obtain ⟨x, hx⟩ := hsurj y711 exact ⟨x, (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).2 hx⟩712 have h := Ideal.comap_isMaximal_of_surjective713 (K := (⊥ : Ideal (S ⧸ IsLocalRing.maximalIdeal S))) _ hs714 rwa [← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker] at h715 716/-- The concrete surface over a Noetherian ring is Noetherian. -/717theorem concrete_surface_isNoetherianRing (O : Type) [CommRing O] (pi : O) (u : (TwoSeries O)ˣ)718 (a b : ℕ) [IsNoetherianRing O] :719 IsNoetherianRing (ConcreteSurface O pi u a b) :=720 inferInstance721 722/-- An element of the concrete surface whose image in the special fiber is a nonzerodivisor723is a nonzerodivisor modulo `π`. -/724theorem concrete_surface_residue_regular_of_special_fiber (O : Type) [CommRing O] [IsDomain O]725 [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)726 (f : ConcreteSurface O pi u a b)727 (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})728 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)729 (hreg : Function.Injective730 (fun w : SpecialFiber (IsLocalRing.ResidueField O) a b ↦ e731 (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f) * w)) :732 Function.Injective733 (fun w : ConcreteSurface O pi u a b ⧸ Ideal.span734 {algebraMap O (ConcreteSurface O pi u a b) pi} => Ideal.Quotient.mk735 (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f * w) :=736 fun w₁ w₂ h ↦ e.injective <| hreg <| by simpa only [map_mul] using congrArg e h737 738/-- A special-fiber identification compatible with reduction sends `t`, `x` and constants to739the corresponding elements of `k[[T,X]]/(T^a X^b)`. -/740theorem concrete_surface_special_fiber_equiv_parameters (O : Type) [CommRing O] [IsDomain O]741 [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)742 (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})743 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)744 (he : ∀ s : TwoSeries O, e745 (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})746 (surfaceMk O pi u a b s)) =747 Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b) (residueSeries O s)) :748 e (Ideal.Quotient.mk _ (surfaceT O pi u a b)) = fiberT (IsLocalRing.ResidueField O) a b ∧749 e (Ideal.Quotient.mk _ (surfaceX O pi u a b)) = fiberX (IsLocalRing.ResidueField O) a b ∧750 ∀ c : O, e (Ideal.Quotient.mk _ (algebraMap O (ConcreteSurface O pi u a b) c)) =751 Ideal.Quotient.mk _ (MvPowerSeries.C (IsLocalRing.residue O c)) := by752 have hres : ∀ s, residueSeries O s = MvPowerSeries.map (IsLocalRing.residue O) s := fun s ↦ rfl753 refine ⟨?_, ?_, ?_⟩754 · have := he (axisT O)755 rw [hres] at this756 simpa [surfaceT, fiberT, axisT, axisX, MvPowerSeries.map_X] using this757 · have := he (axisX O)758 rw [hres] at this759 simpa [surfaceX, fiberX, axisT, axisX, MvPowerSeries.map_X] using this760 · intro c761 have h1 : algebraMap O (ConcreteSurface O pi u a b) c =762 surfaceMk O pi u a b (MvPowerSeries.C c) := by763 change algebraMap O (TwoSeries O ⧸ surfaceIdeal O pi u a b) c = _764 rw [← Ideal.Quotient.mk_algebraMap]765 rfl766 rw [h1, he, hres, MvPowerSeries.map_C]767 768/-- The vertical equation `π = u · t^a · x^b` holds in the concrete surface. -/769theorem concrete_surface_vertical (O : Type) [CommRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :770 algebraMap O (ConcreteSurface O pi u a b) pi =771 (surfaceUnit O pi u a b : ConcreteSurface O pi u a b) * surfaceT O pi u a b ^ a *772 surfaceX O pi u a b ^ b := by773 have h : surfaceMk O pi u a b (surfaceRelation O pi u a b) = 0 :=774 Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span rfl)775 rw [surfaceRelation, map_sub, sub_eq_zero, map_mul, map_mul, map_pow, map_pow] at h776 have h2 : algebraMap O (ConcreteSurface O pi u a b) pi =777 surfaceMk O pi u a b (MvPowerSeries.C pi) := rfl778 rw [h2, h]779 rfl780 781private theorem length_quotient_sup_eq_contact {R SF : Type} [CommRing R] [CommRing SF] (p : R)782 (e : (R ⧸ Ideal.span {p}) ≃+* SF) (g c : R) (hp : p ∈ Ideal.span {c}) :783 Module.length R (R ⧸ (Ideal.span {g} ⊔ Ideal.span {c})) =784 contact (e (Ideal.Quotient.mk (Ideal.span {p}) g))785 (e (Ideal.Quotient.mk (Ideal.span {p}) c)) := by786 let I : Ideal R := Ideal.span {p}787 let φ : R →+* SF := e.toRingHom.comp (Ideal.Quotient.mk I)788 have hφ : Function.Surjective φ :=789 e.surjective.comp Ideal.Quotient.mk_surjective790 let _ : Algebra R SF := φ.toAlgebra791 have hsurj : Function.Surjective (algebraMap R SF) := hφ792 unfold contact793 rw [← Module.length_eq_of_surjective (S := R) hsurj]794 let ψ : R →ₐ[R] SF ⧸ Ideal.span {φ g, φ c} := Algebra.ofId R _795 have hψ : Function.Surjective ψ := Ideal.Quotient.mk_surjective.comp hφ796 have hkerφ : RingHom.ker φ = I := by797 ext x798 simp [φ, RingHom.mem_ker, Ideal.Quotient.eq_zero_iff_mem]799 have hker : RingHom.ker ψ = Ideal.span {g} ⊔ Ideal.span {c} := by800 ext x801 rw [RingHom.mem_ker]802 change Ideal.Quotient.mk _ (φ x) = 0 ↔ _803 rw [Ideal.Quotient.eq_zero_iff_mem]804 have h1 : Ideal.span {φ g, φ c} = (Ideal.span {g} ⊔ Ideal.span {c}).map φ := by805 rw [← Ideal.span_insert, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]806 rw [h1, ← Ideal.mem_comap, Ideal.comap_map_of_surjective' _ hφ, hkerφ]807 have : I ≤ Ideal.span {g} ⊔ Ideal.span {c} :=808 le_sup_of_le_right ((Ideal.span_singleton_le_iff_mem _).2 hp)809 rw [sup_eq_left.2 this]810 have E := (Ideal.quotientKerAlgEquivOfSurjective hψ).toLinearEquiv811 exact ((Submodule.quotEquivOfEq _ _ hker).symm.trans E).length_eq812 813/-- Contact lengths against `t` (and against `x` when `b > 0`) in the concrete surface agree814with the corresponding contacts in the special fiber. -/815theorem concrete_surface_contact_eq_special_fiber_contact (O : Type) [CommRing O] [IsDomain O]816 [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)817 (ha : 0 < a)818 (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})819 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)820 (he : ∀ s : TwoSeries O, e821 (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})822 (surfaceMk O pi u a b s)) =823 Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b) (residueSeries O s))824 (g : ConcreteSurface O pi u a b) :825 Module.length (ConcreteSurface O pi u a b)826 (ConcreteSurface O pi u a b ⧸ (Ideal.span {g} ⊔ Ideal.span {surfaceT O pi u a b})) =827 contact (e ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})) g))828 (fiberT (IsLocalRing.ResidueField O) a b) ∧829 (0 < b →830 Module.length (ConcreteSurface O pi u a b)831 (ConcreteSurface O pi u a b ⧸ (Ideal.span {g} ⊔ Ideal.span {surfaceX O pi u a b})) =832 contact (e833 ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})) g))834 (fiberX (IsLocalRing.ResidueField O) a b)) := by835 obtain ⟨hT, hX, -⟩ := concrete_surface_special_fiber_equiv_parameters O pi u a b e he836 have hv := concrete_surface_vertical O pi u a b837 refine ⟨?_, fun hb ↦ ?_⟩838 · rw [← hT]839 refine length_quotient_sup_eq_contact _ e g _ ?_840 rw [Ideal.mem_span_singleton, hv]841 exact Dvd.dvd.mul_right (Dvd.dvd.mul_left (dvd_pow_self _ ha.ne') _) _842 · rw [← hX]843 refine length_quotient_sup_eq_contact _ e g _ ?_844 rw [Ideal.mem_span_singleton, hv]845 exact Dvd.dvd.mul_left (dvd_pow_self _ hb.ne') _846 847private theorem ideal_map_span_singleton {R R' F : Type} [Semiring R] [Semiring R'] [FunLike F R R']848 [RingHomClass F R R'] (f : F) (x : R) : (Ideal.span {x}).map f = Ideal.span {f x} := by849 rw [Ideal.map_span, Set.image_singleton]850 851private theorem span_singleton_eq_of_ringEquiv {A B : Type} [CommRing A] [CommRing B] (e : A ≃+* B)852 {x y : A} (h : Ideal.span {e x} = Ideal.span {e y}) : Ideal.span {x} = Ideal.span {y} := by853 simpa [ideal_map_span_singleton] using congrArg (Ideal.map e.symm) h854 855private theorem contact_congr_span {B : Type} [CommRing B] {f f' : B} (t : B)856 (h : Ideal.span {f} = Ideal.span {f'}) : contact f t = contact f' t := by857 unfold contact858 rw [Ideal.span_insert, Ideal.span_insert, h]859 860/-- Residue cells lifting distinct principal residue ideals are disjoint. -/861private theorem pairwise_disjoint_residueIdealCell {R SF : Type} [CommRing R] [CommRing SF]862 (p : R) (e : (R ⧸ Ideal.span {p}) ≃+* SF) {P : Ideal SF → Prop} (F : Subtype P → R)863 (hF : ∀ I, Ideal.span {e (Ideal.Quotient.mk (Ideal.span {p}) (F I))} = I.val) :864 Pairwise fun I J ↦ Disjoint (residueIdealCell p (F I)) (residueIdealCell p (F J)) := by865 intro I I' hII'866 rw [Set.disjoint_left]867 rintro J ⟨⟨g, rfl⟩, h1⟩ ⟨_, h2⟩868 refine hII' (Subtype.ext ?_)869 rw [← hF I, ← hF I', ← ideal_map_span_singleton e, ← ideal_map_span_singleton e, ← h1, ← h2]870 871/-- The crossing state set of the concrete surface is the disjoint union of the residue cells872lifting the crossing residue ideals. -/873theorem concrete_crossing_state_eq_union_cells (O : Type) [CommRing O] [IsDomain O]874 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]875 [Finite (IsLocalRing.ResidueField O)] (pi : O) (u : (TwoSeries O)ˣ)876 (a b : ℕ) (ha : 0 < a) (hb : 0 < b) [IsDomain (ConcreteSurface O pi u a b)]877 [IsRegularLocalRing (ConcreteSurface O pi u a b)]878 (S : SurfaceData O (ConcreteSurface O pi u a b))879 (hSt : S.t = surfaceT O pi u a b) (hSx : S.x = surfaceX O pi u a b) (hSa : S.a = a)880 (hSb : S.b = b)881 (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})882 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)883 (he : ∀ s : TwoSeries O, e884 (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})885 (surfaceMk O pi u a b s)) =886 Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b) (residueSeries O s))887 (c h : ℕ) (hc : 0 < c) (hh : 0 < h)888 (F : crossingResidueIdeals (IsLocalRing.ResidueField O) a b c h → ConcreteSurface O pi u a b)889 (hF : ∀ I, Ideal.span890 {e ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})) (F I))} =891 I.val) :892 surfaceStateSet O (ConcreteSurface O pi u a b) S (State.crossing a b c h) =893 ⋃ I, residueIdealCell (algebraMap O (ConcreteSurface O pi u a b) pi) (F I) ∧894 Pairwise895 (fun I J ↦ Disjoint (residueIdealCell (algebraMap O (ConcreteSurface O pi u a b) pi) (F I))896 (residueIdealCell (algebraMap O (ConcreteSurface O pi u a b) pi) (F J))) := by897 have hIC : ∀ g : ConcreteSurface O pi u a b,898 idealContact (ConcreteSurface O pi u a b) (Ideal.span {g}) S.t =899 contact900 (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) g))901 (fiberT (IsLocalRing.ResidueField O) a b) := fun g ↦ by902 rw [idealContact, hSt]903 exact (concrete_surface_contact_eq_special_fiber_contact O pi u a b ha e he g).1904 have hIX : ∀ g : ConcreteSurface O pi u a b,905 idealContact (ConcreteSurface O pi u a b) (Ideal.span {g}) S.x =906 contact907 (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) g))908 (fiberX (IsLocalRing.ResidueField O) a b) := fun g ↦ by909 rw [idealContact, hSx]910 exact (concrete_surface_contact_eq_special_fiber_contact O pi u a b ha e he g).2 hb911 refine ⟨?_, ?_⟩912 · ext J913 simp only [surfaceStateSet, Set.mem_ofPred_eq, Set.mem_iUnion, residueIdealCell,914 State.Valid]915 constructor916 · rintro ⟨⟨g, rfl⟩, _, _, _, hJ, hJ'⟩917 let I : crossingResidueIdeals (IsLocalRing.ResidueField O) a b c h :=918 ⟨_, _, rfl, (hIC g).symm.trans hJ, (hIX g).symm.trans hJ'⟩919 refine ⟨I, ⟨g, rfl⟩, ?_⟩920 rw [ideal_map_span_singleton]; apply span_singleton_eq_of_ringEquiv e; rw [hF I]921 · rintro ⟨I, ⟨g, rfl⟩, hJ⟩922 rw [ideal_map_span_singleton] at hJ923 obtain ⟨f, hf1, hf2, hf3⟩ := I.2924 have hspan : Ideal.span {e (Ideal.Quotient.mk _ g)} = Ideal.span {f} := by925 rw [← hf1, ← hF I, ← ideal_map_span_singleton e, ← ideal_map_span_singleton e, hJ]926 exact ⟨⟨g, rfl⟩, ⟨ha, hb, hc, hh⟩, hSa, hSb, by rw [hIC, ← hf2, contact_congr_span _ hspan],927 by rw [hIX, ← hf3, contact_congr_span _ hspan]⟩928 · exact pairwise_disjoint_residueIdealCell _ e F hF929 930/-- The single state set of the concrete surface is the disjoint union of the residue cells931lifting the single residue ideals. -/932theorem concrete_single_state_eq_union_cells (O : Type) [CommRing O] [IsDomain O]933 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]934 [Finite (IsLocalRing.ResidueField O)] (pi : O) (u : (TwoSeries O)ˣ)935 (a : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a 0)]936 [IsRegularLocalRing (ConcreteSurface O pi u a 0)]937 (S : SurfaceData O (ConcreteSurface O pi u a 0))938 (hSt : S.t = surfaceT O pi u a 0) (hSa : S.a = a) (hSb : S.b = 0)939 (e : (ConcreteSurface O pi u a 0 ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})940 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a 0)941 (he : ∀ s : TwoSeries O, e942 (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})943 (surfaceMk O pi u a 0 s)) =944 Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a 0) (residueSeries O s))945 (c : ℕ) (hc : 0 < c)946 (F : singleResidueIdeals (IsLocalRing.ResidueField O) a c → ConcreteSurface O pi u a 0)947 (hF : ∀ I, Ideal.span948 {e ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})) (F I))} =949 I.val) :950 surfaceStateSet O (ConcreteSurface O pi u a 0) S (State.single a c) =951 ⋃ I, residueIdealCell (algebraMap O (ConcreteSurface O pi u a 0) pi) (F I) ∧952 Pairwise953 (fun I J ↦ Disjoint (residueIdealCell (algebraMap O (ConcreteSurface O pi u a 0) pi) (F I))954 (residueIdealCell (algebraMap O (ConcreteSurface O pi u a 0) pi) (F J))) := by955 have hIC : ∀ g : ConcreteSurface O pi u a 0,956 idealContact (ConcreteSurface O pi u a 0) (Ideal.span {g}) S.t =957 contact958 (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi}) g))959 (fiberT (IsLocalRing.ResidueField O) a 0) := fun g ↦ by960 rw [idealContact, hSt]961 exact (concrete_surface_contact_eq_special_fiber_contact O pi u a 0 ha e he g).1962 refine ⟨?_, ?_⟩963 · ext J964 simp only [surfaceStateSet, Set.mem_ofPred_eq, Set.mem_iUnion, residueIdealCell,965 State.Valid]966 constructor967 · rintro ⟨⟨g, rfl⟩, _, _, _, hJ⟩968 let I : singleResidueIdeals (IsLocalRing.ResidueField O) a c :=969 ⟨_, _, rfl, (hIC g).symm.trans hJ⟩970 refine ⟨I, ⟨g, rfl⟩, ?_⟩971 rw [ideal_map_span_singleton]; apply span_singleton_eq_of_ringEquiv e; rw [hF I]972 · rintro ⟨I, ⟨g, rfl⟩, hJ⟩973 rw [ideal_map_span_singleton] at hJ974 obtain ⟨f, hf1, hf2⟩ := I.2975 refine ⟨⟨g, rfl⟩, ⟨ha, hc⟩, hSa, hSb, ?_⟩976 rw [hIC, ← hf2]977 apply contact_congr_span978 rw [← hf1, ← hF I, ← ideal_map_span_singleton e, ← ideal_map_span_singleton e, hJ]979 · exact pairwise_disjoint_residueIdealCell _ e F hF980 981/-! ### Complete local rings -/982 983/-- A complete DVR is adically complete for the ideal generated by any uniformizer. -/984theorem dvr_isAdicComplete_span_uniformizer (O : Type) [CommRing O] [IsDomain O]985 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)986 (hpi : Irreducible pi) :987 IsAdicComplete (Ideal.span {pi}) O := by988 rw [← hpi.maximalIdeal_eq]989 infer_instance990 991/-- Krull intersection: in a Noetherian local ring, `⋂ₙ (J + Iⁿ) = J` for every proper `I`. -/992theorem iInf_sup_pow_eq_of_isLocalRing (S : Type) [CommRing S] [IsNoetherianRing S] [IsLocalRing S]993 (I J : Ideal S) (hI : I ≠ ⊤) :994 (⨅ n : ℕ, J ⊔ I ^ n) = J := by995 apply le_antisymm _ (le_iInf fun n ↦ le_sup_left)996 intro s hs997 have h := Ideal.iInf_pow_smul_eq_bot_of_isLocalRing (I := I) (M := S ⧸ J) hI998 have hm : Submodule.Quotient.mk s ∈ (⨅ n : ℕ, I ^ n • (⊤ : Submodule S (S ⧸ J))) := by999 rw [Submodule.mem_iInf]1000 intro n1001 have := (Submodule.mem_iInf _).1 hs n1002 obtain ⟨j, hj, x, hx, rfl⟩ := Submodule.mem_sup.1 this1003 have hjx : (Submodule.Quotient.mk (j + x) : S ⧸ J) = x • (Submodule.Quotient.mk 1 : S ⧸ J) := by1004 rw [← Submodule.Quotient.mk_smul, smul_eq_mul, mul_one]1005 rw [Submodule.Quotient.mk_add, (Submodule.Quotient.mk_eq_zero J).2 hj, zero_add]1006 rw [hjx]1007 exact Submodule.smul_mem_smul hx Submodule.mem_top1008 rw [h, Submodule.mem_bot] at hm1009 exact (Submodule.Quotient.mk_eq_zero J).1 hm1010 1011/-- Every ideal of a Noetherian local ring is closed in the `𝔪`-adic topology. -/1012theorem ideal_closed_noetherian_local (A : Type) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]1013 (I : Ideal A) :1014 ⨅ n : ℕ, (I ⊔ (IsLocalRing.maximalIdeal A)^n) = I :=1015 iInf_sup_pow_eq_of_isLocalRing A _ I (Ideal.IsMaximal.ne_top inferInstance)1016 1017/-- A Noetherian local ring complete for `𝔪` is complete for every proper ideal. -/1018theorem isAdicComplete_of_isAdicComplete_maximalIdeal (A : Type) [CommRing A] [IsNoetherianRing A]1019 [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (J : Ideal A) (hJ : J ≠ ⊤) :1020 IsAdicComplete J A := by1021 have key : ∀ (I : Ideal A) (n : ℕ) (x y : A),1022 x ≡ y [SMOD (I ^ n • ⊤ : Submodule A A)] ↔ x - y ∈ I ^ n := by1023 intro I n x y1024 rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top]1025 set m := IsLocalRing.maximalIdeal A1026 have hJm : J ≤ m := IsLocalRing.le_maximalIdeal hJ1027 have := IsHausdorff.of_isLocalRing J A hJ1028 have : IsPrecomplete J A := ⟨fun f hf ↦ ?_⟩1029 · exact {}1030 have hf' : ∀ {a b : ℕ}, a ≤ b → f a ≡ f b [SMOD (m ^ a • ⊤ : Submodule A A)] := by1031 intro a b hab1032 rw [key]1033 exact Ideal.pow_right_mono hJm a ((key J a _ _).1 (hf hab))1034 obtain ⟨L, hL⟩ := IsPrecomplete.prec (inferInstance : IsPrecomplete m A) hf'1035 refine ⟨L, fun n ↦ ?_⟩1036 rw [key, ← iInf_sup_pow_eq_of_isLocalRing A m (J ^ n) (Ideal.IsMaximal.ne_top inferInstance),1037 Ideal.mem_iInf]1038 intro N1039 have h1 : f n - f (max n N) ∈ J ^ n := (key J n _ _).1 (hf (le_max_left n N))1040 have h2 : f (max n N) - L ∈ m ^ N :=1041 Ideal.pow_le_pow_right (le_max_right n N) ((key m _ _ _).1 (hL (max n N)))1042 simpa using Ideal.add_mem _ (Ideal.mem_sup_left h1) (Ideal.mem_sup_right h2)1043 1044/-- A product of two `I`-adically complete modules is `I`-adically complete. -/1045theorem isAdicComplete_prod (O M N : Type) [CommRing O] [AddCommGroup M] [Module O M]1046 [AddCommGroup N] [Module O N] (I : Ideal O) [IsAdicComplete I M] [IsAdicComplete I N] :1047 IsAdicComplete I (M × N) := by1048 have key : ∀ (n : ℕ) (x : M × N), x ∈ (I ^ n • ⊤ : Submodule O (M × N)) ↔1049 x.1 ∈ (I ^ n • ⊤ : Submodule O M) ∧ x.2 ∈ (I ^ n • ⊤ : Submodule O N) := by1050 intro n x1051 constructor1052 · intro h1053 constructor1054 · have := Submodule.mem_map_of_mem (f := LinearMap.fst O M N) h1055 rwa [Submodule.map_smul'', Submodule.map_top, Submodule.range_fst] at this1056 · have := Submodule.mem_map_of_mem (f := LinearMap.snd O M N) h1057 rwa [Submodule.map_smul'', Submodule.map_top, Submodule.range_snd] at this1058 · rintro ⟨h1, h2⟩1059 have e : x = LinearMap.inl O M N x.1 + LinearMap.inr O M N x.2 := by simp1060 rw [e]1061 refine Submodule.add_mem _ ?_ ?_1062 · have := Submodule.mem_map_of_mem (f := LinearMap.inl O M N) h11063 rw [Submodule.map_smul''] at this1064 exact Submodule.smul_mono le_rfl le_top this1065 · have := Submodule.mem_map_of_mem (f := LinearMap.inr O M N) h21066 rw [Submodule.map_smul''] at this1067 exact Submodule.smul_mono le_rfl le_top this1068 have hmod (n : ℕ) (x y : M × N) : x ≡ y [SMOD (I ^ n • ⊤ : Submodule O (M × N))] ↔1069 x.1 ≡ y.1 [SMOD (I ^ n • ⊤ : Submodule O M)] ∧1070 x.2 ≡ y.2 [SMOD (I ^ n • ⊤ : Submodule O N)] := by1071 simp only [SModEq.sub_mem, key, Prod.fst_sub, Prod.snd_sub]1072 refine { haus' := fun x hx ↦ ?_, prec' := fun f hf ↦ ?_ }1073 · exact Prod.ext (IsHausdorff.haus inferInstance x.1 fun n ↦ ((hmod n x 0).1 (hx n)).1)1074 (IsHausdorff.haus inferInstance x.2 fun n ↦ ((hmod n x 0).1 (hx n)).2)1075 · obtain ⟨a, ha⟩ := IsPrecomplete.prec (I := I) (M := M) inferInstance (f := fun n ↦ (f n).1)1076 fun hmn ↦ ((hmod _ _ _).1 (hf hmn)).11077 obtain ⟨b, hb⟩ := IsPrecomplete.prec (I := I) (M := N) inferInstance (f := fun n ↦ (f n).2)1078 fun hmn ↦ ((hmod _ _ _).1 (hf hmn)).21079 exact ⟨(a, b), fun n ↦ (hmod _ _ _).2 ⟨ha n, hb n⟩⟩1080 1081/-- The quotient of an `I`-adically complete ring by an `I`-closed ideal `J` is complete for1082the image of `I`. -/1083theorem isAdicComplete_quotient_of_iInf_sup_pow (S : Type) [CommRing S] (I J : Ideal S)1084 [IsAdicComplete I S] (hJ : (⨅ n : ℕ, J ⊔ I ^ n) = J) :1085 IsAdicComplete (I.map (Ideal.Quotient.mk J)) (S ⧸ J) := by1086 have key : ∀ (n : ℕ) (y : S ⧸ J),1087 y ∈ ((I.map (Ideal.Quotient.mk J)) ^ n • ⊤ : Submodule (S ⧸ J) (S ⧸ J)) ↔1088 ∃ x ∈ I ^ n, Ideal.Quotient.mk J x = y := by1089 intro n y1090 rw [smul_eq_mul, Ideal.mul_top, ← Ideal.map_pow]1091 exact Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective1092 have keyS : ∀ (n : ℕ) (x : S), x ∈ (I ^ n • ⊤ : Submodule S S) ↔ x ∈ I ^ n := by1093 intro n x1094 rw [smul_eq_mul, Ideal.mul_top]1095 have h1 : IsHausdorff (I.map (Ideal.Quotient.mk J)) (S ⧸ J) := ⟨fun y hy ↦ by1096 obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y1097 refine Ideal.Quotient.eq_zero_iff_mem.mpr (hJ ▸ Ideal.mem_iInf.2 fun n ↦ ?_)1098 obtain ⟨x, hx, hxs⟩ := (key n _).1 (by simpa only [SModEq.sub_mem, sub_zero] using hy n)1099 simpa using Submodule.add_mem_sup (Ideal.Quotient.eq.1 hxs.symm) hx⟩1100 have h2 : IsPrecomplete (I.map (Ideal.Quotient.mk J)) (S ⧸ J) := by1101 refine ⟨fun f hf ↦ ?_⟩1102 -- lift `f` to a `I`-adic Cauchy sequence of partial sums in `S`1103 have hstep (n : ℕ) : ∃ x ∈ I ^ n, Ideal.Quotient.mk J x = f (n + 1) - f n := by1104 obtain ⟨x, hx, hxe⟩ := (key n _).1 (SModEq.sub_mem.1 (hf (Nat.le_succ n)))1105 exact ⟨-x, neg_mem hx, by rw [map_neg, hxe, neg_sub]⟩1106 choose x hxI hxe using hstep1107 obtain ⟨s0, hs0⟩ := Ideal.Quotient.mk_surjective (f 0)1108 let s : ℕ → S := fun n ↦ s0 + ∑ i ∈ Finset.range n, x i1109 have hs : ∀ n, Ideal.Quotient.mk J (s n) = f n := by1110 intro n1111 induction n with1112 | zero => simp [s, hs0]1113 | succ n ih =>1114 have : s (n + 1) = s n + x n := by1115 simp only [s, Finset.sum_range_succ]; ring1116 rw [this, map_add, ih, hxe]; ring1117 have hdiff : ∀ m n, m ≤ n → s n - s m ∈ I ^ m := by1118 intro m n hmn1119 have : s n - s m = ∑ i ∈ Finset.Ico m n, x i := by1120 simp only [s]1121 rw [← Finset.sum_range_add_sum_Ico _ hmn]; ring1122 rw [this]1123 exact Ideal.sum_mem _ fun i hi ↦1124 Ideal.pow_le_pow_right (Finset.mem_Ico.mp hi).1 (hxI i)1125 obtain ⟨L, hL⟩ := (inferInstance : IsPrecomplete I S).prec (f := s) fun hmn ↦ by1126 rw [SModEq.sub_mem, keyS, ← neg_sub]1127 exact neg_mem (hdiff _ _ hmn)1128 refine ⟨Ideal.Quotient.mk J L, fun n ↦ ?_⟩1129 have := hL n1130 rw [SModEq.sub_mem, keyS] at this1131 rw [SModEq.sub_mem, key]1132 exact ⟨s n - L, this, by rw [map_sub, hs]⟩1133 exact { toIsHausdorff := h1, toIsPrecomplete := h2 }1134 1135/-- A nontrivial ring with a nonzerodivisor `e` generating a prime ideal and with1136`⋂ₙ (e)ⁿ = 0` is a domain. -/1137theorem isDomain_of_regular_prime_element (A : Type) [CommRing A] [Nontrivial A] (e : A)1138 (he : Function.Injective (fun a : A ↦ e * a)) (hprime : (Ideal.span {e}).IsPrime)1139 (hinf : (⨅ n : ℕ, (Ideal.span {e})^n) = ⊥) :1140 IsDomain A := by1141 have key : ∀ n : ℕ, ∀ f : A, f ∉ (Ideal.span {e})^n →1142 ∃ m : ℕ, ∃ f' : A, f = e^m * f' ∧ f' ∉ Ideal.span {e} := by1143 intro n1144 induction n with1145 | zero => intro f hf; simp at hf1146 | succ n ih =>1147 intro f hf1148 by_cases hfe : f ∈ Ideal.span {e}1149 · obtain ⟨g, rfl⟩ := Ideal.mem_span_singleton'.mp hfe1150 have hg : g ∉ (Ideal.span {e})^n := by1151 intro hg1152 apply hf1153 rw [pow_succ]1154 exact Ideal.mul_mem_mul hg (Ideal.mem_span_singleton_self e)1155 obtain ⟨m, f', rfl, hf'⟩ := ih g hg1156 exact ⟨m+1, f', by ring, hf'⟩1157 · exact ⟨0, f, by simp, hfe⟩1158 have dec (f : A) (hf : f ≠ 0) : ∃ m : ℕ, ∃ f' : A, f = e^m * f' ∧ f' ∉ Ideal.span {e} := by1159 obtain ⟨n, hn⟩ : ∃ n, f ∉ Ideal.span {e} ^ n := by1160 by_contra! h1161 exact hf (by simpa [hinf] using Ideal.mem_iInf.2 h)1162 exact key n f hn1163 have cancel (k : ℕ) (x : A) (hx : e ^ k * x = 0) : x = 0 :=1164 IsLeftRegular.pow k he (hx.trans (mul_zero _).symm)1165 have : NoZeroDivisors A := ⟨fun {f g} hfg ↦ by1166 by_contra! ⟨hf, hg⟩1167 obtain ⟨m, f', rfl, hf'⟩ := dec f hf1168 obtain ⟨n, g', rfl, hg'⟩ := dec g hg1169 have h0 : f' * g' = 0 := cancel (m + n) _ (by rw [← hfg]; ring)1170 exact (hprime.mem_or_mem (h0 ▸ Ideal.zero_mem _)).elim hf' hg'⟩1171 exact NoZeroDivisors.to_isDomain A1172 1173/-! ### Lengths of quotients -/1174 1175/-- Length of `(A/J)/I(A/J)` over `A/J` equals the length of `A/(J + I)` over `A`. -/1176theorem length_double_quotient_eq (A : Type) [CommRing A] (J I : Ideal A) :1177 Module.length (A ⧸ J) ((A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I) =1178 Module.length A (A ⧸ (J ⊔ I)) := by1179 have hs : Function.Surjective (algebraMap A (A ⧸ J)) := by1180 rw [Ideal.Quotient.algebraMap_eq]; exact Ideal.Quotient.mk_surjective1181 rw [← Module.length_eq_of_surjective (S := A) (R := A ⧸ J)1182 (M := (A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I) hs]1183 exact (DoubleQuot.quotQuotEquivQuotSupₐ A J I).toLinearEquiv.length_eq1184 1185/-- If `s` is a nonzerodivisor modulo `I`, then1186`ℓ(R/(I + (t s))) = ℓ(R/(I + (t))) + ℓ(R/(I + (s)))`. -/1187theorem length_quotient_sup_mul_eq_add (R : Type) [CommRing R] (I : Ideal R) (s t : R)1188 (hs : ∀ x, s * x ∈ I → x ∈ I) :1189 Module.length R (R ⧸ (I ⊔ Ideal.span {t * s})) = Module.length R (R ⧸ (I ⊔ Ideal.span {t})) +1190 Module.length R (R ⧸ (I ⊔ Ideal.span {s})) := by1191 have mem : ∀ r x, x ∈ I ⊔ Ideal.span {r} ↔ ∃ i ∈ I, ∃ u : R, x = i + u * r := fun r x ↦ by1192 simp only [Submodule.mem_sup, Ideal.mem_span_singleton']1193 constructor1194 · rintro ⟨i, hi, _, ⟨u, rfl⟩, rfl⟩; exact ⟨i, hi, u, rfl⟩1195 · rintro ⟨i, hi, u, rfl⟩; exact ⟨i, hi, _, ⟨u, rfl⟩, rfl⟩1196 set K₁ : Submodule R R := I ⊔ Ideal.span {t}1197 set K : Submodule R R := I ⊔ Ideal.span {t * s}1198 set K₂ : Submodule R R := I ⊔ Ideal.span {s}1199 have ha : K ≤ K₂ := by1200 intro x hx1201 obtain ⟨i, hi, u, rfl⟩ := (mem (t * s) x).1 hx1202 exact (mem s _).2 ⟨i, hi, u * t, by ring⟩1203 let μ : R →ₗ[R] R := LinearMap.mulLeft R s1204 have hb : K₁ ≤ K.comap μ := by1205 intro x hx1206 obtain ⟨i, hi, u, rfl⟩ := (mem t x).1 hx1207 rw [Submodule.mem_comap]1208 exact (mem (t * s) _).2 ⟨s * i, I.mul_mem_left s hi, u, by simp [μ]; ring⟩1209 let f := Submodule.mapQ K₁ K μ hb1210 let g := Submodule.mapQ K K₂ LinearMap.id ha1211 have hf : Function.Injective f := by1212 rw [injective_iff_map_eq_zero]1213 intro y hy1214 obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ y1215 simp only [f, Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero] at hy ⊢1216 obtain ⟨i, hi, u, hu⟩ := (mem (t * s) _).1 hy1217 have : y - u * t ∈ I := hs _ (by1218 have : s * (y - u * t) = i := by simp [μ] at hu; linear_combination hu1219 rw [this]; exact hi)1220 exact (mem t _).2 ⟨_, this, u, by ring⟩1221 have hg : Function.Surjective g := Submodule.factor_surjective ha1222 have H : Function.Exact f g := by1223 rw [LinearMap.exact_iff]1224 ext z1225 obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ z1226 simp only [LinearMap.mem_ker, LinearMap.mem_range, g, f, Submodule.mapQ_apply,1227 LinearMap.id_apply, Submodule.Quotient.mk_eq_zero]1228 constructor1229 · intro hx1230 obtain ⟨i, hi, u, rfl⟩ := (mem s _).1 hx1231 refine ⟨Submodule.Quotient.mk u, ?_⟩1232 rw [Submodule.mapQ_apply, Submodule.Quotient.eq]1233 exact (mem (t * s) _).2 ⟨-i, I.neg_mem hi, 0, by simp [μ]; ring⟩1234 · rintro ⟨w, hw⟩1235 obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ w1236 rw [Submodule.mapQ_apply, Submodule.Quotient.eq] at hw1237 obtain ⟨i, hi, u, hu⟩ := (mem (t * s) _).1 hw1238 exact (mem s _).2 ⟨-i, I.neg_mem hi, y - u * t, by simp [μ] at hu; linear_combination -hu⟩1239 exact Module.length_eq_add_of_exact f g hf hg H1240 1241/-- If `t` is a nonzerodivisor modulo `I`, then `ℓ(R/(I + (tⁿ))) = n · ℓ(R/(I + (t)))`. -/1242theorem length_quotient_sup_pow_eq_mul (R : Type) [CommRing R] (I : Ideal R) (t : R)1243 (ht : ∀ x, t * x ∈ I → x ∈ I) (n : ℕ) :1244 Module.length R (R ⧸ (I ⊔ Ideal.span {t ^ n})) = (n : ℕ∞) *1245 Module.length R (R ⧸ (I ⊔ Ideal.span {t})) := by1246 induction n with1247 | zero =>1248 have : Subsingleton (R ⧸ (I ⊔ Ideal.span {t ^ 0})) := by1249 rw [pow_zero, Ideal.span_singleton_one, sup_top_eq]1250 exact Ideal.Quotient.subsingleton_iff.mpr rfl1251 rw [Module.length_eq_zero]1252 simp1253 | succ n ih =>1254 rw [pow_succ, length_quotient_sup_mul_eq_add R I t (t ^ n) ht, ih]1255 push_cast1256 rw [add_mul, one_mul]1257 1258/-- Lengths of quotients are invariant under ring isomorphisms. -/1259theorem module_length_quotient_ringEquiv (S S' : Type) [CommRing S] [CommRing S'] (e : S ≃+* S')1260 (I : Ideal S) :1261 Module.length S (S ⧸ I) = Module.length S' (S' ⧸ Ideal.map (e : S →+* S') I) := by1262 let q := Ideal.quotientEquiv I (I.map (e : S →+* S')) e rfl1263 have := RingHomInvPair.of_ringEquiv e1264 have := RingHomInvPair.of_ringEquiv_symm e1265 let f : (S ⧸ I) ≃ₛₗ[(e : S →+* S')] (S' ⧸ Ideal.map (e : S →+* S') I) :=1266 { toFun := q1267 invFun := q.symm1268 left_inv := q.left_inv1269 right_inv := q.right_inv1270 map_add' := map_add q1271 map_smul' := by1272 intro s x1273 induction x using Quotient.inductionOn' with1274 | h x =>1275 change q (Ideal.Quotient.mk I (s * x)) = _1276 simp only [q, Ideal.quotientEquiv_mk, map_mul]1277 rfl }1278 apply WithBot.coe_injective1279 rw [Module.coe_length, Module.coe_length,1280 Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComap f)]1281 1282end SurfaceBlowup1283 1284end