# Documentation

Mathlib.Geometry.Manifold.DerivationBundle

# Derivation bundle #

In this file we define the derivations at a point of a manifold on the algebra of smooth fuctions. 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.

instance smoothFunctionsAlgebra (𝕜 : Type u_1) {E : Type u_2} [] {H : Type u_3} [] (I : ) (M : Type u_4) [] [] :
Algebra 𝕜 (ContMDiffMap I () M 𝕜 )
instance smooth_functions_tower (𝕜 : Type u_1) {E : Type u_2} [] {H : Type u_3} [] (I : ) (M : Type u_4) [] [] :
IsScalarTower 𝕜 (ContMDiffMap I () M 𝕜 ) (ContMDiffMap I () M 𝕜 )
def PointedSmoothMap (𝕜 : Type u_1) {E : Type u_2} [] {H : Type u_3} [] (I : ) (M : Type u_4) [] [] (n : ℕ∞) :
MType (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.

Instances For
Instances For
instance PointedSmoothMap.funLike {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {x : M} :
FunLike () M fun x => 𝕜
instance PointedSmoothMap.instCommRingPointedSmoothMapTopENatInstENatTop {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {x : M} :
instance PointedSmoothMap.instInhabitedPointedSmoothMapTopENatInstENatTop {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {x : M} :
instance PointedSmoothMap.evalAlgebra {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} :
Algebra () 𝕜

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

def PointedSmoothMap.eval {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] (x : M) :
ContMDiffMap I () M 𝕜 →ₐ[] 𝕜

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

Instances For
theorem PointedSmoothMap.smul_def {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] (x : M) (f : ) (k : 𝕜) :
f k = f x * k
@[reducible]
def PointDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] (x : M) :
Type (max (max u_1 u_4) u_1)

The derivations at a point of a manifold. Some regard this as a possible definition of the tangent space

Instances For
def SmoothFunction.evalAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] (x : M) :
ContMDiffMap I () M 𝕜 →ₗ[] 𝕜

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

Instances For
def Derivation.evalAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] (x : M) :
Derivation 𝕜 (ContMDiffMap I () M 𝕜 ) (ContMDiffMap I () M 𝕜 ) →ₗ[𝕜]

The evaluation at a point as a linear map.

Instances For
theorem Derivation.evalAt_apply {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] (X : Derivation 𝕜 (ContMDiffMap I () M 𝕜 ) (ContMDiffMap I () M 𝕜 )) (f : ContMDiffMap I () M 𝕜 ) (x : M) :
↑(↑() X) f = ↑(X f) x
def hfdifferential {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : ContMDiffMap I I' M M' } {x : M} {y : M'} (h : f x = y) :
→ₗ[𝕜]

The heterogeneous differential as a linear map. 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.

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

The homogeneous differential as a linear map.

Instances For
Instances For
Instances For
@[simp]
theorem apply_fdifferential {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ) {x : M} (v : ) (g : ContMDiffMap I' () M' 𝕜 ) :
↑(↑() v) g = v ()
@[simp]
theorem apply_hfdifferential {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : ContMDiffMap I I' M M' } {x : M} {y : M'} (h : f x = y) (v : ) (g : ContMDiffMap I' () M' 𝕜 ) :
↑(↑() v) g = ↑(↑() v) g
@[simp]
theorem fdifferential_comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] (g : ContMDiffMap I' I'' M' M'' ) (f : ContMDiffMap I I' M M' ) (x : M) :
= LinearMap.comp (fdifferential g (f x)) ()