mathlibdocumentation

geometry.manifold.derivation_bundle

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.

@[protected, instance]
def smooth_functions_algebra (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) (M : Type u_4) [ M] :
algebra ๐ ๐) M ๐ โค)
Equations
@[protected, instance]
def smooth_functions_tower (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) (M : Type u_4) [ M] :
is_scalar_tower ๐ ๐) M ๐ โค) ๐) M ๐ โค)
@[nolint]
def pointed_smooth_map (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) (M : Type u_4) [ M] (n : โโ) (x : M) :
Type (max u_4 u_1)

Type synonym, introduced to put a different has_smul action on C^nโฎI, M; ๐โฏ which is defined as f โข r = f(x) * r.

Equations
• I M n x = ๐) M ๐ n
Instances for pointed_smooth_map
@[protected, instance]
def pointed_smooth_map.has_coe_to_fun {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] {x : M} :
has_coe_to_fun (pointed_smooth_map ๐ I M โค x) (ฮป (_x : I M โค x), M โ ๐)
Equations
@[protected, instance]
def pointed_smooth_map.comm_ring {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] {x : M} :
Equations
@[protected, instance]
def pointed_smooth_map.algebra {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] {x : M} :
algebra ๐ (pointed_smooth_map ๐ I M โค x)
Equations
@[protected, instance]
def pointed_smooth_map.inhabited {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] {x : M} :
Equations
@[protected, instance]
def pointed_smooth_map.cont_mdiff_map.algebra {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] {x : M} :
algebra (pointed_smooth_map ๐ I M โค x) ๐) M ๐ โค)
Equations
@[protected, instance]
def pointed_smooth_map.cont_mdiff_map.is_scalar_tower {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] {x : M} :
is_scalar_tower ๐ (pointed_smooth_map ๐ I M โค x) ๐) M ๐ โค)
@[protected, instance]
def pointed_smooth_map.eval_algebra {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {x : M} :
algebra (pointed_smooth_map ๐ I M โค x) ๐

smooth_map.eval_ring_hom gives rise to an algebra structure of C^โโฎI, M; ๐โฏ on ๐.

Equations
def pointed_smooth_map.eval {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] (x : M) :
๐) M ๐ โค โโ[ I M โค x] ๐

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

Equations
theorem pointed_smooth_map.smul_def {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] (x : M) (f : I M โค x) (k : ๐) :
f โข k = โf x * k
@[protected, instance]
def pointed_smooth_map.is_scalar_tower {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] (x : M) :
is_scalar_tower ๐ (pointed_smooth_map ๐ I M โค x) ๐
@[reducible]
def point_derivation {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
Type (max u_4 u_1)

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

Equations
def smooth_function.eval_at {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
๐) M ๐ โค โโ[ I M โค x] ๐

Evaluation at a point gives rise to a C^โโฎI, M; ๐โฏ-linear map between C^โโฎI, M; ๐โฏ and ๐.

Equations
def derivation.eval_at {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] (x : M) :
derivation ๐ ๐) M ๐ โค) ๐) M ๐ โค) โโ[๐]

The evaluation at a point as a linear map.

Equations
theorem derivation.eval_at_apply {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] (X : derivation ๐ ๐) M ๐ โค) ๐) M ๐ โค)) (f : ๐) M ๐ โค) (x : M) :
def hfdifferential {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {E' : Type u_5} [normed_space ๐ E'] {H' : Type u_6} {I' : E' H'} {M' : Type u_7} [ M'] {f : I' M M' โค} {x : M} {y : M'} (h : โf x = y) :
โโ[๐] 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.

Equations
def fdifferential {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {E' : Type u_5} [normed_space ๐ E'] {H' : Type u_6} {I' : E' H'} {M' : Type u_7} [ M'] (f : I' M M' โค) (x : M) :
โโ[๐] (โf x)

The homogeneous differential as a linear map.

Equations
@[simp]
theorem apply_fdifferential {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {E' : Type u_5} [normed_space ๐ E'] {H' : Type u_6} {I' : E' H'} {M' : Type u_7} [ M'] (f : I' M M' โค) {x : M} (v : x) (g : ๐) M' ๐ โค) :
โ(โ x) v) g = โv (g.comp f)
@[simp]
theorem apply_hfdifferential {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {E' : Type u_5} [normed_space ๐ E'] {H' : Type u_6} {I' : E' H'} {M' : Type u_7} [ M'] {f : I' M M' โค} {x : M} {y : M'} (h : โf x = y) (v : x) (g : ๐) M' ๐ โค) :
@[simp]
theorem fdifferential_comp {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {E' : Type u_5} [normed_space ๐ E'] {H' : Type u_6} {I' : E' H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [normed_space ๐ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] (g : I'' M' M'' โค) (f : I' M M' โค) (x : M) :
fdifferential (g.comp f) x = (โf x)).comp x)