Derivation bundle

In this file we define the derivations at a point of a manifold on the algebra of smooth functions. Moreover, we define the differential of a function in terms of derivations.

The content of this file is not meant to be regarded as an alternative definition to the current tangent bundle but rather as a purely algebraic theory that provides a purely algebraic definition of the Lie algebra for a Lie group. This theory coincides with the usual tangent bundle in the case of finite-dimensional C^∞ real manifolds, but not in the general case.

instance smoothFunctionsAlgebra (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : Algebra 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)

instance smooth_functions_tower (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : IsScalarTower 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)

def PointedContMDiffMap (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (n : WithTop ℕ∞) : M → Type (max 0 u_4 u_1)

Type synonym, introduced to put a different SMul action on C^n⟮I, M; 𝕜⟯ which is defined as f • r = f(x) * r. Denoted as C^n⟮I, M; 𝕜⟯⟨x⟩ within the Derivation namespace.

def Derivation.«termC^_⟮_,_;_⟯⟨_⟩» : Lean.ParserDescr

Type synonym, introduced to put a different SMul action on C^n⟮I, M; 𝕜⟯ which is defined as f • r = f(x) * r. Denoted as C^n⟮I, M; 𝕜⟯⟨x⟩ within the Derivation namespace.

instance PointedContMDiffMap.instFunLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : FunLike (PointedContMDiffMap 𝕜 I M (↑⊤) x) M 𝕜

instance PointedContMDiffMap.instCommRingSomeENatTop {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : CommRing (PointedContMDiffMap 𝕜 I M (↑⊤) x)

instance PointedContMDiffMap.instAlgebraSomeENatTop {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : Algebra 𝕜 (PointedContMDiffMap 𝕜 I M (↑⊤) x)

instance PointedContMDiffMap.instInhabitedSomeENatTop {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : Inhabited (PointedContMDiffMap 𝕜 I M (↑⊤) x)

instance PointedContMDiffMap.instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : Algebra (PointedContMDiffMap 𝕜 I M (↑⊤) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)

instance PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : IsScalarTower 𝕜 (PointedContMDiffMap 𝕜 I M (↑⊤) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)

instance PointedContMDiffMap.evalAlgebra {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : Algebra (PointedContMDiffMap 𝕜 I M (↑⊤) x) 𝕜

ContMDiffMap.evalRingHom gives rise to an algebra structure of C^∞⟮I, M; 𝕜⟯ on 𝕜.

def PointedContMDiffMap.eval {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤ →ₐ[PointedContMDiffMap 𝕜 I M (↑⊤) x] 𝕜

With the evalAlgebra algebra structure evaluation is actually an algebra morphism.

theorem PointedContMDiffMap.smul_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) (f : PointedContMDiffMap 𝕜 I M (↑⊤) x) (k : 𝕜) : f • k = f x * k

instance PointedContMDiffMap.instIsScalarTowerSomeENatTop {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : IsScalarTower 𝕜 (PointedContMDiffMap 𝕜 I M (↑⊤) x) 𝕜

@[reducible, inline]

abbrev PointDerivation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : Type (max (max u_4 u_1) u_1)

The derivations at a point of a manifold. Some regard this as a possible definition of the tangent space, as this coincides with the usual tangent space for finite-dimensional C^∞ real manifolds. The identification is not true in general, though.

def ContMDiffFunction.evalAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤ →ₗ[PointedContMDiffMap 𝕜 I M (↑⊤) x] 𝕜

Evaluation at a point gives rise to a C^∞⟮I, M; 𝕜⟯-linear map between C^∞⟮I, M; 𝕜⟯ and 𝕜.

def Derivation.evalAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) →ₗ[𝕜] PointDerivation I x

The evaluation at a point as a linear map.

theorem Derivation.evalAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (X : Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (x : M) : ((evalAt x) X) f = (X f) x

def hfdifferential {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : ContMDiffMap I I' M M' ↑⊤} {x : M} {y : M'} (h : f x = y) : PointDerivation I x →ₗ[𝕜] PointDerivation I' y

The heterogeneous differential as a linear map, denoted as 𝒅ₕ within the Manifold namespace. Instead of taking a function as an argument this differential takes h : f x = y. It is particularly handy to deal with situations where the points on where it has to be evaluated are equal but not definitionally equal.

def fdifferential {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ↑⊤) (x : M) : PointDerivation I x →ₗ[𝕜] PointDerivation I' (f x)

The homogeneous differential as a linear map, denoted as 𝒅 within the Manifold namespace.

def Manifold.«term𝒅» : Lean.ParserDescr

The homogeneous differential as a linear map, denoted as 𝒅 within the Manifold namespace.

def Manifold.«term𝒅ₕ» : Lean.ParserDescr

The heterogeneous differential as a linear map, denoted as 𝒅ₕ within the Manifold namespace. Instead of taking a function as an argument this differential takes h : f x = y. It is particularly handy to deal with situations where the points on where it has to be evaluated are equal but not definitionally equal.

@[simp]

theorem fdifferential_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ↑⊤) {x : M} (v : PointDerivation I x) (g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤) : ((fdifferential f x) v) g = v (g.comp f)

@[simp]

theorem hfdifferential_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : ContMDiffMap I I' M M' ↑⊤} {x : M} {y : M'} (h : f x = y) (v : PointDerivation I x) (g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤) : ((hfdifferential h) v) g = ((fdifferential f x) v) g

@[simp]

theorem fdifferential_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] (g : ContMDiffMap I' I'' M' M'' ↑⊤) (f : ContMDiffMap I I' M M' ↑⊤) (x : M) : fdifferential (g.comp f) x = fdifferential g (f x) ∘ₗ fdifferential f x