mathlib documentation

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) [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) (M : Type u_4) [topological_space M] [charted_space H M] :
algebra ๐•œ (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค)
Equations
@[protected, instance]
def smooth_functions_tower (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) (M : Type u_4) [topological_space M] [charted_space H M] :
is_scalar_tower ๐•œ (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค) (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค)
@[nolint]
def pointed_smooth_map (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) (M : Type u_4) [topological_space M] [charted_space H 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
Instances for pointed_smooth_map
@[protected, instance]
def pointed_smooth_map.has_coe_to_fun {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
has_coe_to_fun (pointed_smooth_map ๐•œ I M โŠค x) (ฮป (_x : pointed_smooth_map ๐•œ I M โŠค x), M โ†’ ๐•œ)
Equations
@[protected, instance]
def pointed_smooth_map.comm_ring {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
Equations
@[protected, instance]
def pointed_smooth_map.algebra {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
algebra ๐•œ (pointed_smooth_map ๐•œ I M โŠค x)
Equations
@[protected, instance]
def pointed_smooth_map.inhabited {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
Equations
@[protected, instance]
def pointed_smooth_map.cont_mdiff_map.algebra {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
algebra (pointed_smooth_map ๐•œ I M โŠค x) (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค)
Equations
@[protected, instance]
def pointed_smooth_map.cont_mdiff_map.is_scalar_tower {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
is_scalar_tower ๐•œ (pointed_smooth_map ๐•œ I M โŠค x) (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค)
@[protected, instance]
def pointed_smooth_map.eval_algebra {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H 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} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] (x : M) :
cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค โ†’โ‚[pointed_smooth_map ๐•œ 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} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] (x : M) (f : pointed_smooth_map ๐•œ I M โŠค x) (k : ๐•œ) :
f โ€ข k = โ‡‘f x * k
@[protected, instance]
def pointed_smooth_map.is_scalar_tower {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] (x : M) :
is_scalar_tower ๐•œ (pointed_smooth_map ๐•œ I M โŠค x) ๐•œ
@[reducible]
def point_derivation {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H 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} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners ๐•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] (x : M) :
cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค โ†’โ‚—[pointed_smooth_map ๐•œ 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} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] (x : M) :
derivation ๐•œ (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค) (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค) โ†’โ‚—[๐•œ] point_derivation I x

The evaluation at a point as a linear map.

Equations
theorem derivation.eval_at_apply {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] (X : derivation ๐•œ (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค) (cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค)) (f : cont_mdiff_map I (model_with_corners_self ๐•œ ๐•œ) M ๐•œ โŠค) (x : M) :
def hfdifferential {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space ๐•œ E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : cont_mdiff_map 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.

Equations
def fdifferential {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space ๐•œ E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : cont_mdiff_map I I' M M' โŠค) (x : M) :

The homogeneous differential as a linear map.

Equations
@[simp]
theorem apply_fdifferential {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space ๐•œ E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : cont_mdiff_map I I' M M' โŠค) {x : M} (v : point_derivation I x) (g : cont_mdiff_map I' (model_with_corners_self ๐•œ ๐•œ) M' ๐•œ โŠค) :
@[simp]
theorem apply_hfdifferential {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space ๐•œ E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : cont_mdiff_map I I' M M' โŠค} {x : M} {y : M'} (h : โ‡‘f x = y) (v : point_derivation I x) (g : cont_mdiff_map I' (model_with_corners_self ๐•œ ๐•œ) M' ๐•œ โŠค) :
@[simp]
theorem fdifferential_comp {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space ๐•œ E] {H : Type u_3} [topological_space H] {I : model_with_corners ๐•œ E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space ๐•œ E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space ๐•œ E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners ๐•œ E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] (g : cont_mdiff_map I' I'' M' M'' โŠค) (f : cont_mdiff_map I I' M M' โŠค) (x : M) :