The completion of a stalk of the structure sheaf

Bierstone–Milman's Taylor series homomorphism "induces an isomorphism 𝒪̂_{M,a} ≅ F_a[[X]]" [BM97, (0.3)]. Since the Taylor homomorphism T_a reflects the powers of the maximal ideal (taylorHom_mem_maximalIdeal_pow_iff, Hironaka/Manifold/Germ/TaylorIdeal.lean) and its range, the convergent series, contains the polynomials, T_a induces isomorphisms 𝒪_{M,a}/𝔪_a^k ≅ 𝕜[[X]]/(X)^k for every k (taylorQuot); 𝕜[[X]] being (X)-adically complete (isAdicComplete_maximalIdeal of Hironaka/Analytic/Weierstrass/AdicComplete.lean), Mathlib's universal property IsAdicComplete.liftRingHom assembles them into a ring homomorphism taylorCompletion : AdicCompletion 𝔪_a 𝒪_{M,a} →+* 𝕜[[X]], which is injective (the quotient maps are) and surjective (a series is the limit of the images of the lifts of its truncations), and restricts to T_a on 𝒪_{M,a} (taylorCompletionEquiv, IsTaylorHom.exists_adicCompletion_equiv'). The isomorphism gives the Krull dimension of the stalk (Hironaka/Manifold/Germ/StalkNoetherian.lean) and, with the constants and coordinates, Kollár's 𝒪̂_{p,X} ≅ k(p)[[x_1, …, x_n]] (Hironaka/Manifold/Germ/ResidueCompletion.lean).

noncomputable def Manifold.taylorQuot {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ⧸ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k →+* MvPowerSeries (Fin n) 𝕜 ⧸ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k

The map 𝒪_{M,a}/𝔪_a^k →+* 𝕜[[X]]/(X)^k induced by T_a.

Equations

• Manifold.taylorQuot E ψ φ ha hφ k = Ideal.quotientMap (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k) (Manifold.taylorHom E ψ φ ha hφ) ⋯

theorem Manifold.taylorQuot_mk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (taylorQuot E ψ φ ha hφ k) ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k)) s) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k)) ((taylorHom E ψ φ ha hφ) s)

theorem Manifold.taylorQuot_injective {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) : Function.Injective ⇑(taylorQuot E ψ φ ha hφ k)

theorem Manifold.taylorQuot_surjective {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) : Function.Surjective ⇑(taylorQuot E ψ φ ha hφ k)

𝒪_{M,a}/𝔪_a^k → 𝕜[[X]]/(X)^k is onto: the truncation of a series is a polynomial, hence the Taylor series of a germ.

noncomputable def Manifold.taylorCompletionFamily {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) : AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜 ⧸ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k

The compatible family AdicCompletion 𝔪_a 𝒪_{M,a} →+* 𝕜[[X]]/(X)^k.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.taylorCompletionFamily_mk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) (f : AdicCompletion.AdicCauchySequence (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (taylorCompletionFamily E ψ φ ha hφ k) ((AdicCompletion.mk (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) f) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k)) ((taylorHom E ψ φ ha hφ) (↑f k))

theorem Manifold.taylorCompletionFamily_compat {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {m k : ℕ} (hle : m ≤ k) : (Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜)) hle).comp (taylorCompletionFamily E ψ φ ha hφ k) = taylorCompletionFamily E ψ φ ha hφ m

noncomputable def Manifold.taylorCompletion {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜

The ring homomorphism 𝒪̂_{M,a} →+* 𝕜[[X]] induced by T_a on the 𝔪_a-adic completion, by the universal property of the complete ring 𝕜[[X]].

Equations

• Manifold.taylorCompletion E ψ φ ha hφ = IsAdicComplete.liftRingHom (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜)) (Manifold.taylorCompletionFamily E ψ φ ha hφ) ⋯

theorem Manifold.mk_taylorCompletion {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (k : ℕ) (x : AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k)) ((taylorCompletion E ψ φ ha hφ) x) = (taylorCompletionFamily E ψ φ ha hφ k) x

theorem Manifold.eq_of_forall_mk_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {c c' : MvPowerSeries (Fin n) 𝕜} (h : ∀ (k : ℕ), (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k)) c = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k)) c') : c = c'

Two series equal modulo every (X)^k are equal (𝕜[[X]] is (X)-adically separated).

theorem Manifold.taylorCompletion_of {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (taylorCompletion E ψ φ ha hφ) ((AdicCompletion.of (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) s) = (taylorHom E ψ φ ha hφ) s

theorem Manifold.taylorCompletion_injective {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : Function.Injective ⇑(taylorCompletion E ψ φ ha hφ)

theorem Manifold.taylorCompletion_surjective {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : Function.Surjective ⇑(taylorCompletion E ψ φ ha hφ)

𝒪̂_{M,a} → 𝕜[[X]] is onto: a series is the limit of the Taylor series of the lifts of its truncations, an 𝔪_a-adic Cauchy sequence.

noncomputable def Manifold.taylorCompletionEquiv {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* MvPowerSeries (Fin n) 𝕜

𝒪̂_{M,a} ≅ 𝕜[[X₁, …, Xₙ]] through the Taylor homomorphism [BM97, (0.3)].

Equations

• Manifold.taylorCompletionEquiv E ψ φ ha hφ = RingEquiv.ofBijective (Manifold.taylorCompletion E ψ φ ha hφ) ⋯

theorem Manifold.taylorCompletionEquiv_algebraMap {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (taylorCompletionEquiv E ψ φ ha hφ) ((algebraMap (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a))) s) = (taylorHom E ψ φ ha hφ) s

theorem Manifold.IsTaylorHom.exists_adicCompletion_equiv' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) : ∃ (e : AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* MvPowerSeries (Fin n) 𝕜), ∀ (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)), e ((algebraMap (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a))) s) = T s

For any map satisfying the specification IsTaylorHom: the 𝔪_a-adic completion of 𝒪_{M,a} is 𝕜[[X₁, …, Xₙ]], through T_a.