Partial derivatives in a chart as operators on the structure sheaf

A manifold of Bierstone–Milman's category is covered by regular coordinate charts U with coordinates x = (x_1, …, x_n), x_i ∈ 𝒪_M(U), on which "the partial derivatives ∂^{|α|}/∂x^α make sense as transformations 𝒪_M(U) → 𝒪_M(U)" [BM97, (0.3)]; Kollár's derivative of an ideal sheaf is formed with the derivations ∂/∂x_1, …, ∂/∂x_n of local coordinates [Kol07, Definition 73]. For a chart φ of the maximal atlas with coordinates ψ : E ≃L[𝕜] (Fin n → 𝕜) (the coordinate functions x_i = ψ_i ∘ φ) and an open V ⊆ φ.source, the i-th partial derivative in the chart of a section f of 𝒪_M over V is the section

(∂_i f)(x) = D(f ∘ φ⁻¹)(φ x)(ψ⁻¹ e_i),

the derivative at φ(x) of the analytic function f ∘ φ⁻¹ on the model space along the i-th coordinate vector. It is analytic (an analytic function has analytic derivative, Mathlib's AnalyticAt.fderiv, composed with the analytic chart), so ∂_i is an operator on 𝒪_M(V); it is additive, 𝕜-linear and satisfies the Leibniz rule (fderiv_add, fderiv_const_smul, fderiv_mul), so it is a 𝕜-derivation coordDeriv E ψ φ hφ V hV i : Derivation 𝕜 𝒪_M(V) 𝒪_M(V).

At the stalk 𝒪_{M,a} the same operator is coordDerivStalk E ψ φ hφ ha i : Derivation 𝕜 𝒪_{M,a} 𝒪_{M,a}, defined through the chart transport 𝒪_{M,a} ≃+* 𝒪_{E, φ(a)} as the partial derivative pderivGerm of analytic germs (that the germ of ∂_i f is ∂_i of the germ of f is coordDerivStalk_germ in Hironaka/Manifold/Germ/CoordDerivChart.lean). The 𝕜-algebra structures used are the pointwise one on the sections (Mathlib's ContMDiffMap.algebra) and the constants const 𝕜 E M a : 𝕜 →+* 𝒪_{M,a} on the stalk, with the ℚ-algebra structure through ℚ → 𝕜 that the regular coordinates of the Hironaka library (IsLocalRing.RegularCoords) require.

These derivations make the analytic stalk an instance of the Hironaka library's regular coordinates (Hironaka/Manifold/Germ/CoordDerivCoords.lean) and enter the derivative ideal sheaves of the maximal-contact construction (Hironaka/Manifold/IdealSheaf/Deriv.lean).

@[instance_reducible]

noncomputable instance Manifold.instAlgebraSections {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (V : TopologicalSpace.Opens M) : Algebra 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))

The 𝕜-algebra structure of the sections 𝒪_M(V): pointwise scalars, Mathlib's ContMDiffMap.algebra (the scalar c acts as the constant section c).

Equations

• Manifold.instAlgebraSections E V = { smul := Manifold.instAlgebraSections._aux_1 E V, algebraMap := Manifold.instAlgebraSections._aux_3 E V, commutes' := ⋯, smul_def' := ⋯ }

theorem Manifold.algebraMap_sections_apply {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (V : TopologicalSpace.Opens M) (c : 𝕜) (x : ↥V) : ↑((algebraMap 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) c) x = c

@[instance_reducible]

noncomputable instance Manifold.instAlgebraStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (a : M) : Algebra 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The 𝕜-algebra structure of the stalk 𝒪_{M,a} through the constants const 𝕜 E M a : 𝕜 →+* 𝒪_{M,a}.

Equations

• Manifold.instAlgebraStalk E a = (Manifold.const 𝕜 E M a).toAlgebra

theorem Manifold.algebraMap_stalk_eq {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (a : M) : algebraMap 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a) = const 𝕜 E M a

@[instance_reducible]

noncomputable instance Manifold.instAlgebraRatStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [CharZero 𝕜] (a : M) : Algebra ℚ ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The ℚ-algebra structure of the stalk 𝒪_{M,a}, ℚ → 𝕜 → 𝒪_{M,a}, as the regular coordinates of the Hironaka library require (RegularCoords takes [Algebra ℚ R]).

Equations

• Manifold.instAlgebraRatStalk E a = ((Manifold.const 𝕜 E M a).comp (algebraMap ℚ 𝕜)).toAlgebra

theorem Manifold.algebraMap_rat_stalk_eq {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [CharZero 𝕜] (a : M) : algebraMap ℚ ↑((structureSheaf 𝕜 E M).presheaf.stalk a) = (const 𝕜 E M a).comp (algebraMap ℚ 𝕜)

instance Manifold.instIsScalarTowerRatStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [CharZero 𝕜] (a : M) : IsScalarTower ℚ 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

theorem Manifold.extendSection_add {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {V : TopologicalSpace.Opens M} (f g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : extendSection 𝕜 E (f + g) = extendSection 𝕜 E f + extendSection 𝕜 E g

theorem Manifold.extendSection_mul {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {V : TopologicalSpace.Opens M} (f g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : extendSection 𝕜 E (f * g) = extendSection 𝕜 E f * extendSection 𝕜 E g

theorem Manifold.extendSection_smul {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {V : TopologicalSpace.Opens M} (c : 𝕜) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : extendSection 𝕜 E (c • f) = c • extendSection 𝕜 E f

theorem Manifold.analyticAt_extendSection_comp_symm {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (x : ↥V) : AnalyticAt 𝕜 (extendSection 𝕜 E f ∘ ↑φ.symm) (↑φ ↑x)

A section f of 𝒪_M over V ⊆ φ.source, read in the chart, is analytic at φ(x) for every x ∈ V.

noncomputable def Manifold.coordDerivFun {𝕜 : 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) (V : TopologicalSpace.Opens M) (i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : ↥V → 𝕜

The i-th partial derivative in the chart of a section f over V, as a function on V: x ↦ D(f ∘ φ⁻¹)(φ x)(ψ⁻¹ e_i).

Equations

• Manifold.coordDerivFun E ψ φ V i f x = (fderiv 𝕜 (Manifold.extendSection 𝕜 E f ∘ ↑φ.symm) (↑φ ↑x)) (ψ.symm (Pi.single i 1))

theorem Manifold.contMDiff_coordDerivFun {𝕜 : 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 : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ (coordDerivFun E ψ φ V i f)

Analytic functions have analytic partial derivatives: the partial derivative in the chart of an analytic section is analytic — AnalyticAt.fderiv on the model space, composed with the analytic chart φ.

noncomputable def Manifold.coordDerivSection {𝕜 : 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 : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))

The partial derivative ∂_i f as a section of 𝒪_M over V.

Equations

• Manifold.coordDerivSection E ψ φ hφ V hV i f = ⟨Manifold.coordDerivFun E ψ φ V i f, ⋯⟩

theorem Manifold.coordDerivSection_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (x : ↥V) : ↑(coordDerivSection E ψ φ hφ V hV i f) x = (fderiv 𝕜 (extendSection 𝕜 E f ∘ ↑φ.symm) (↑φ ↑x)) (ψ.symm (Pi.single i 1))

theorem Manifold.coordDerivSection_add {𝕜 : 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 : Fin n) (f g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : coordDerivSection E ψ φ hφ V hV i (f + g) = coordDerivSection E ψ φ hφ V hV i f + coordDerivSection E ψ φ hφ V hV i g

theorem Manifold.coordDerivSection_smul {𝕜 : 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 : Fin n) (c : 𝕜) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : coordDerivSection E ψ φ hφ V hV i (c • f) = c • coordDerivSection E ψ φ hφ V hV i f

theorem Manifold.coordDerivSection_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (i : Fin n) (f g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : coordDerivSection E ψ φ hφ V hV i (f * g) = f * coordDerivSection E ψ φ hφ V hV i g + g * coordDerivSection E ψ φ hφ V hV i f

The Leibniz rule: ∂_i (f g) = f ∂_i g + g ∂_i f.

noncomputable def Manifold.coordDeriv {𝕜 : 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 : Fin n) : Derivation 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V)) ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))

The i-th partial derivative in the chart ∂_i : 𝒪_M(V) → 𝒪_M(V), for V ⊆ φ.source, as a 𝕜-derivation of the sections [BM97, (0.3)].

Equations

• Manifold.coordDeriv E ψ φ hφ V hV i = Derivation.mk' { toFun := Manifold.coordDerivSection E ψ φ hφ V hV i, map_add' := ⋯, map_smul' := ⋯ } ⋯

theorem Manifold.coordDeriv_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (x : ↥V) : ↑((coordDeriv E ψ φ hφ V hV i) f) x = (fderiv 𝕜 (extendSection 𝕜 E f ∘ ↑φ.symm) (↑φ ↑x)) (ψ.symm (Pi.single i 1))

noncomputable def Manifold.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) (j : Fin n) : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))

The coordinate x_j = ψ_j ∘ φ as a section of 𝒪_M over V ⊆ φ.source (chartSection restricted to V).

Equations

• Manifold.coordSection E ψ φ hφ V hV j = (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (Manifold.chartSection E ψ φ hφ j)

theorem Manifold.coordSection_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (j : Fin n) (x : ↥V) : ↑(coordSection E ψ φ hφ V hV j) x = ψ (↑φ ↑x) j

theorem Manifold.pderivGerm_coe' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (i : Fin n) {b : E} {g : ↥(analyticGermsAt 𝕜 E b)} {F : E → 𝕜} (hF : ↑g = ↑F) : ↑(pderivGerm E ψ i b g) = ↑fun (y : E) => (fderiv 𝕜 F y) (ψ.symm (Pi.single i 1))

theorem Manifold.pderivGerm_add {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (i : Fin n) (b : E) (g h : ↥(analyticGermsAt 𝕜 E b)) : pderivGerm E ψ i b (g + h) = pderivGerm E ψ i b g + pderivGerm E ψ i b h

At the level of germs: ∂_i (pderivGerm) is additive.

theorem Manifold.pderivGerm_mul {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (i : Fin n) (b : E) (g h : ↥(analyticGermsAt 𝕜 E b)) : pderivGerm E ψ i b (g * h) = g * pderivGerm E ψ i b h + h * pderivGerm E ψ i b g

At the level of germs: the Leibniz rule for ∂_i (pderivGerm).

noncomputable def Manifold.coordDerivStalkFun {𝕜 : 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 : Fin n) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The partial derivative ∂_i on 𝒪_{M,a}, as a function: pderivGerm on analytic germs, transported by the chart transport.

Equations

• Manifold.coordDerivStalkFun E ψ φ hφ ha i s = (Manifold.chartTransport E φ ha hφ).symm (Manifold.pderivGerm E ψ i (↑φ a) ((Manifold.chartTransport E φ ha hφ) s))

theorem Manifold.coordDerivStalkFun_add {𝕜 : 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 : Fin n) (s t : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : coordDerivStalkFun E ψ φ hφ ha i (s + t) = coordDerivStalkFun E ψ φ hφ ha i s + coordDerivStalkFun E ψ φ hφ ha i t

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

theorem Manifold.chartTransport_const {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (c : 𝕜) : ↑((chartTransport E φ ha hφ) ((const 𝕜 E M a) c)) = ↑fun (x : E) => c

The chart transport of a constant germ is the constant germ.

theorem Manifold.coordDerivStalkFun_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 : Fin n) (c : 𝕜) : coordDerivStalkFun E ψ φ hφ ha i ((const 𝕜 E M a) c) = 0

∂_i kills the constants.

noncomputable def Manifold.coordDerivStalk {𝕜 : 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 : Fin n) : Derivation 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The partial derivative ∂_i on 𝒪_{M,a} as a 𝕜-derivation, for a chart φ of the maximal atlas containing a with coordinates ψ ([BM97, (0.3)]; the derivations ∂/∂x_1, …, ∂/∂x_n of [Kol07, Definition 73]).

Equations

• Manifold.coordDerivStalk E ψ φ hφ ha i = Derivation.mk' { toFun := Manifold.coordDerivStalkFun E ψ φ hφ ha i, map_add' := ⋯, map_smul' := ⋯ } ⋯

theorem Manifold.coordDerivStalk_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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i : Fin n) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (coordDerivStalk E ψ φ hφ ha i) s = (chartTransport E φ ha hφ).symm (pderivGerm E ψ i (↑φ a) ((chartTransport E φ ha hφ) s))

theorem Manifold.coordDerivStalk_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 : Fin n) (c : 𝕜) : (coordDerivStalk E ψ φ hφ ha i) ((const 𝕜 E M a) c) = 0