mathlib3 documentation

geometry.manifold.derivation_bundle

Derivation bundle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] :
Equations
@[protected, instance]
@[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.fun_like {𝕜 : 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} :
fun_like (pointed_smooth_map 𝕜 I M x) 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]
@[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) :

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) :

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) :

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' 𝕜 ) :
((fdifferential f x) v) g = v (g.comp f)
@[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) :