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.

@[instance]
def smooth_functions_algebra (๐•œ : Type u_1) [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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 ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
Equations
@[instance]
def smooth_functions_tower (๐•œ : Type u_1) [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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 ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
@[nolint]
def pointed_smooth_map (๐•œ : Type u_1) [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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 : with_top โ„•) (x : M) :
Type (max u_4 u_1)

Type synonym, introduced to put a different has_scalar action on C^nโŸฎI, M; ๐•œโŸฏ which is defined as f โ€ข r = f(x) * r.

Equations
@[instance]
def pointed_smooth_map.has_coe_to_fun {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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
@[instance]
def pointed_smooth_map.comm_ring {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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
@[instance]
def pointed_smooth_map.algebra {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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
@[instance]
def pointed_smooth_map.inhabited {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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
@[instance]
def pointed_smooth_map.times_cont_mdiff_map.algebra {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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
@[instance]
def pointed_smooth_map.times_cont_mdiff_map.is_scalar_tower {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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} :
@[instance]
def pointed_smooth_map.eval_algebra {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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} :

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} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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) :

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

Equations
theorem pointed_smooth_map.smul_def {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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 : C^โŠคโŸฎI,M;๐•œโŸฏโŸจxโŸฉ) (k : ๐•œ) :
f โ€ข k = (โ‡‘f x) * k
@[instance]
def pointed_smooth_map.is_scalar_tower {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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) :
def point_derivation {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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) :

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} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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 ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ โ†’โ‚—[๐•œ] point_derivation I x

The evaluation at a point as a linear map.

Equations
theorem derivation.eval_at_apply {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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 ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ) (f : C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ) (x : M) :
def hfdifferential {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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_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 : C^โŠคโŸฎI, M; I', 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} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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_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 : C^โŠคโŸฎI, M; I', M'โŸฏ) (x : M) :

The homogeneous differential as a linear map.

Equations
@[simp]
theorem apply_fdifferential {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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_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 : C^โŠคโŸฎI, M; I', M'โŸฏ) {x : M} (v : point_derivation I x) (g : C^โŠคโŸฎI', M'; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ) :
@[simp]
theorem apply_hfdifferential {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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_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 : C^โŠคโŸฎI, M; I', M'โŸฏ} {x : M} {y : M'} (h : โ‡‘f x = y) (v : point_derivation I x) (g : C^โŠคโŸฎI', M'; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ) :
@[simp]
theorem fdifferential_comp {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_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_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_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 : C^โŠคโŸฎI', M'; I'', M''โŸฏ) (f : C^โŠคโŸฎI, M; I', M'โŸฏ) (x : M) :
๐’… (g.comp f) x = (๐’… g (โ‡‘f x)).comp (๐’… f x)