The Taylor homomorphism of the structure sheaf

In a chart φ of the maximal atlas containing a, with coordinates ψ : E ≃L[𝕜] 𝕜ⁿ, the Taylor homomorphism T_a : 𝒪_{M,a} →+* 𝕜[[X₁, …, Xₙ]] sends the germ of a section f to the power series of f ∘ φ⁻¹ ∘ ψ⁻¹ at ψ(φ(a)): it is the chart transport (Hironaka/Manifold/Germ/ChartTransport.lean) followed by the power series of an analytic germ (taylorGerm, Hironaka/Manifold/Germ/Taylor.lean, valued in the ring Conv 𝕜 n of convergent series). This is Bierstone–Milman's injective "Taylor series homomorphism" [BM97, (0.3)]. taylorHom satisfies the specification IsTaylorHom of Hironaka/Manifold/StructureSheaf.lean (isTaylorHom_taylorHom); any map satisfying it is unique (IsTaylorHom.eq), injective (IsTaylorHom.injective': a germ whose power series vanishes is eventually zero) and has the value at a as constant term (IsTaylorHom.constantCoeff'). Its range, its behaviour on the maximal ideal and the induced isomorphism of completions are in Hironaka/Manifold/Germ/TaylorIdeal.lean and Hironaka/Manifold/Germ/TaylorCompletion.lean.

noncomputable def Manifold.taylorHom {𝕜 : 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) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜

The Taylor homomorphism T_a : 𝒪_{M,a} →+* 𝕜[[X₁, …, Xₙ]] in the chart φ with coordinates ψ [BM97, (0.3)]: the chart transport of germs followed by the power series of an analytic germ.

Equations

• Manifold.taylorHom E ψ φ ha hφ = ((Analytic.Conv 𝕜 n).val.comp (Manifold.taylorGerm ψ (↑φ a))).comp (Manifold.chartTransport E φ ha hφ).toRingHom

theorem Manifold.taylorHom_apply {𝕜 : 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)) : (taylorHom E ψ φ ha hφ) s = ↑((taylorGerm ψ (↑φ a)) ((chartTransport E φ ha hφ) s))

theorem Manifold.taylorHom_mem_conv {𝕜 : 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)) : (taylorHom E ψ φ ha hφ) s ∈ Analytic.Conv 𝕜 n

theorem Manifold.isTaylorHom_taylorHom {𝕜 : 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) : IsTaylorHom E ψ φ a (taylorHom E ψ φ ha hφ)

taylorHom satisfies the specification IsTaylorHom.

theorem Manifold.IsTaylorHom.eq {𝕜 : 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} {T T' : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) (hT' : IsTaylorHom E ψ φ a T') : T = T'

Two maps satisfying the specification agree (uniqueness of the power series of a germ, eq_of_evalSeries_eventuallyEq).

theorem Manifold.IsTaylorHom.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) {T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) : Function.Injective ⇑T

A map satisfying the specification is injective [BM97, (0.3)]: two germs with the same power series have the same germ in the chart, hence the same germ.

theorem Manifold.IsTaylorHom.constantCoeff' {𝕜 : 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) {T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : MvPowerSeries.constantCoeff (T s) = (eval 𝕜 E M a) s

The constant term of the power series of a germ is its value at a.