Partial derivatives in a chart: coordinates, restriction, germs, the Taylor homomorphism

Properties of the partial derivative coordDeriv in the chart (φ, ψ) on the sections over V ⊆ φ.source and of its stalk version coordDerivStalk (Hironaka/Manifold/Germ/CoordDeriv.lean), the operators ∂/∂x_i of Bierstone–Milman's regular coordinate charts [BM97, (0.3)] and of Kollár's derivative ideals [Kol07, Definition 73]:

• coordDeriv_coordSection: ∂_i x_j = δ_ij — near φ(x) the function x_j ∘ φ⁻¹ is the linear form ψ_j, whose derivative along ψ⁻¹ e_i is e_i(j);
• coordDeriv_map: ∂_i commutes with restriction to a smaller open W ⊆ V — the derivative at φ(x), x ∈ W, sees only the germ of f ∘ φ⁻¹ at φ(x) (Filter.EventuallyEq.fderiv_eq);
• coordDerivStalk_germ: the stalk operator is the germ of the section operator, ∂_i (germ f) = germ (∂_i f) — both sides transport to the germ of y ↦ D(f ∘ φ⁻¹)(y)(ψ⁻¹ e_i) at φ(a); coordDerivStalk_coord: ∂_i x_j = δ_ij on the coordinate germs;
• IsTaylorHom.pderiv: T_a (∂_i s) = ∂_{X_i} (T_a s) for any T_a satisfying the specification IsTaylorHom — Bierstone–Milman's "T_a commutes with differentiation" [BM97, (0.3)], from IsTaylorHom.pderiv' of Hironaka/Manifold/Germ/PDeriv.lean read through the chart transport.

These are the facts used to compute orders and derivative ideals in a chart (Hironaka/Manifold/Chart/, Hironaka/Manifold/BlowUp/Transform/).

theorem Manifold.coordDeriv_coordSection {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (i j : Fin n) : (coordDeriv E ψ φ hφ V hV i) (coordSection E ψ φ hφ V hV j) = (algebraMap 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (if i = j then 1 else 0)

∂_i x_j = δ_ij [BM97, (0.3)]: the partial derivative of the coordinate x_j = ψ_j ∘ φ is the constant δ_ij.

theorem Manifold.coordDeriv_map {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (W : TopologicalSpace.Opens M) (hW : ↑W ⊆ φ.source) (hWV : W ≤ V) (i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (coordDeriv E ψ φ hφ W hW i) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.map (CategoryTheory.homOfLE hWV).op)) f) = (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.map (CategoryTheory.homOfLE hWV).op)) ((coordDeriv E ψ φ hφ V hV i) f)

∂_i commutes with restriction to a smaller open W ⊆ V: the derivative at φ(x) only sees the germ of f ∘ φ⁻¹ at φ(x).

theorem Manifold.germ_coordSection {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) {a : M} (ha : a ∈ φ.source) (haV : a ∈ V) (j : Fin n) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V a haV)) (coordSection E ψ φ hφ V hV j) = coord E ψ φ hφ ha j

The germ at a ∈ V of the coordinate section x_j over V is the coordinate germ coord.

theorem Manifold.germ_algebraMap {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (V : TopologicalSpace.Opens M) {a : M} (haV : a ∈ V) (c : 𝕜) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V a haV)) ((algebraMap 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) c) = (const 𝕜 E M a) c

The germ of the constant section c is the constant c of the stalk (const, algebraMap 𝕜 𝒪_{M,a}).

theorem Manifold.coordDerivStalk_germ {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (haV : a ∈ V) (i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (coordDerivStalk E ψ φ hφ ha i) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V a haV)) f) = (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V a haV)) ((coordDeriv E ψ φ hφ V hV i) f)

At the stalk: ∂_i (germ f) = germ (∂_i f) — both sides transport to the germ of y ↦ D(f ∘ φ⁻¹)(y)(ψ⁻¹ e_i) at φ(a).

theorem Manifold.coordDerivStalk_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i j : Fin n) : (coordDerivStalk E ψ φ hφ ha i) (coord E ψ φ hφ ha j) = (const 𝕜 E M a) (if i = j then 1 else 0)

At the stalk: ∂_i x_j = δ_ij on the coordinate germs ([BM97, (0.3)]; [Kol07, Definition 73]).

theorem Manifold.coordDerivStalk_coord_sub_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i j : Fin n) : (coordDerivStalk E ψ φ hφ ha i) (coord E ψ φ hφ ha j - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha j))) = if i = j then 1 else 0

At the stalk: ∂_i (x_j − x_j(a)) = δ_ij on the centred coordinate germs — the axiom pderiv_x of the Hironaka library's regular coordinates (IsLocalRing.RegularCoords).

theorem Manifold.IsTaylorHom.pderiv {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) (i : Fin n) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : T ((coordDerivStalk E ψ φ hφ ha i) s) = (MvPowerSeries.pderiv i) (T s)

"T_a commutes with differentiation" [BM97, (0.3)]: for any T satisfying the specification IsTaylorHom, T (∂_i s) = ∂_{X_i} (T s) — IsTaylorHom.pderiv' read through the chart transport.