The Taylor homomorphism and the maximal ideal

The Taylor homomorphism T_a of a chart φ (coordinates ψ) maps onto the ring of convergent series (range_taylorHom), sends the coordinate germ x_i − x_i(a) to X_i (taylorHom_coord_sub) and the constants to the constants (taylorHom_const). With the division of a series without constant term by the coordinates (Hironaka/Analytic/ConvSeries/CoordDivision.lean) this gives Hadamard's lemma for germs — a germ vanishing at a is ∑_i (x_i − x_i(a)) g_i (exists_eq_sum_coord_mul') — and, by induction on k, that T_a reflects the powers of the maximal ideal: T_a s ∈ (X)^k ↔ s ∈ 𝔪_a^k (taylorHom_mem_maximalIdeal_pow_iff), hence T_a(𝔪_a^k) = (X)^k ∩ T_a(𝒪_{M,a}) (IsTaylorHom.image_maximalIdeal_pow), 𝔪_a = (x_1 − a_1, …, x_n − a_n) (maximalIdeal_eq_span_coord') and 𝔪_a^k spanned by the degree-k monomials in the x_i − a_i (maximalIdeal_pow_eq_span_monomials'). These are the facts behind the isomorphism 𝒪̂_{M,a} ≅ 𝕜[[X]] of [BM97, (0.3)] (Hironaka/Manifold/Germ/TaylorCompletion.lean) and behind the order of a germ at a point (Hironaka/Manifold/IdealSheaf/Order.lean).

noncomputable def Manifold.seriesGerm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (c : MvPowerSeries (Fin n) 𝕜) : (nhds b).Germ 𝕜

The germ at b of the function of a convergent series c, read in the coordinates ψ: z ↦ c(ψ z − ψ b).

Equations

• Manifold.seriesGerm ψ b c = ↑fun (z : E) => Analytic.evalSeries c (ψ z - ψ b)

theorem Manifold.isSeriesOf_seriesGerm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) {c : MvPowerSeries (Fin n) 𝕜} (hc : c ∈ Analytic.Conv 𝕜 n) : IsSeriesOf ψ b (seriesGerm ψ b c) c

theorem Manifold.seriesGerm_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) {c : MvPowerSeries (Fin n) 𝕜} (hc : c ∈ Analytic.Conv 𝕜 n) : seriesGerm ψ b c ∈ analyticGermsAt 𝕜 E b

theorem Manifold.taylorGerm_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : Function.Surjective ⇑(taylorGerm ψ b)

Every convergent series is the power series of an analytic germ.

theorem Manifold.range_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) : Set.range ⇑(taylorHom E ψ φ ha hφ) = ↑(Analytic.Conv 𝕜 n)

The range of the Taylor homomorphism is the ring of convergent series.

theorem Manifold.taylorHom_const {𝕜 : 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) (c : 𝕜) : (taylorHom E ψ φ ha hφ) ((const 𝕜 E M a) c) = MvPowerSeries.C c

The Taylor series of a constant is the constant.

theorem Manifold.taylorHom_coord {𝕜 : 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) (i : Fin n) : (taylorHom E ψ φ ha hφ) (coord E ψ φ hφ ha i) = MvPowerSeries.X i + MvPowerSeries.C (ψ (↑φ a) i)

The Taylor series of the coordinate germ x_i = ψ_i ∘ φ is X_i + x_i(a).

theorem Manifold.taylorHom_coord_sub {𝕜 : 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) (i : Fin n) : (taylorHom E ψ φ ha hφ) (coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i))) = MvPowerSeries.X i

T_a (x_i − x_i(a)) = X_i.

theorem Manifold.exists_eq_sum_coord_mul_of_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (hs : MvPowerSeries.constantCoeff ((taylorHom E ψ φ ha hφ) s) = 0) : ∃ (g : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk a)), s = ∑ i : Fin n, (coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i))) * g i ∧ ∀ (i : Fin n), (taylorHom E ψ φ ha hφ) (g i) = Analytic.divPart i ((taylorHom E ψ φ ha hφ) s)

Hadamard's lemma at the stalk, through the division of series by the coordinates: a germ whose Taylor series has no constant term is ∑_i (x_i − x_i(a)) g_i, where T_a g_i is the i-th part of T_a s.

theorem Manifold.taylorHom_mem_maximalIdeal_pow_iff {𝕜 : 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)) (k : ℕ) : (taylorHom E ψ φ ha hφ) s ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k ↔ s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k

The Taylor homomorphism reflects the powers of the maximal ideal, T_a s ∈ (X)^k ↔ s ∈ 𝔪_a^k (induction on k through the division by the coordinates).

theorem Manifold.IsTaylorHom.mem_maximalIdeal_pow_iff {𝕜 : 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) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (k : ℕ) : T s ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k ↔ s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k

The previous statement for any map satisfying the specification IsTaylorHom.

theorem Manifold.IsTaylorHom.image_maximalIdeal_pow {𝕜 : 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) (k : ℕ) : ⇑T '' ↑(IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k) = ↑(IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜) ^ k) ∩ Set.range ⇑T

T_a(𝔪_aᵏ) = (X)ᵏ ∩ T_a(𝒪_{M,a}) [BM97, (0.3)].

theorem Manifold.exists_eq_sum_coord_mul' {𝕜 : 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)) (hs : (eval 𝕜 E M a) s = 0) : ∃ (g : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk a)), s = ∑ i : Fin n, (coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i))) * g i

Hadamard's lemma: a germ vanishing at a is ∑_i (x_i − x_i(a)) g_i.

theorem Manifold.maximalIdeal_eq_span_coord' {𝕜 : 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) : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) = Ideal.span (Set.range fun (i : Fin n) => coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i)))

𝔪_a = (x_1 − a_1, …, x_n − a_n).

theorem Ideal.prod_pow_mem_pow_sum {R : Type u_2} [CommRing R] (I : Ideal R) {ι : Type u_3} (s : Finset ι) {y : ι → R} (hy : ∀ (i : ι), y i ∈ I) (ν : ι → ℕ) : ∏ i ∈ s, y i ^ ν i ∈ I ^ ∑ i ∈ s, ν i

A product of powers of elements of I lies in the corresponding power of I.

theorem Manifold.maximalIdeal_pow_eq_span_monomials' {𝕜 : 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 : ℕ) : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k = Ideal.span (Set.range fun (ν : { ν : Fin n →₀ ℕ // Finsupp.degree ν = k }) => ∏ i : Fin n, (coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i))) ^ ↑ν i)

𝔪_aᵏ is generated by the monomials of degree k in the x_i − a_i.