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)
[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] :
Equations
- smooth_functions_algebra ๐ I M = smooth_map.algebra
@[protected, 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] :
@[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.
@[protected, 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} :
@[protected, 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
@[protected, 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
@[protected, 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
- pointed_smooth_map.inhabited I = {default := 0}
@[protected, 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} :
@[protected, 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} :
@[protected, 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
- pointed_smooth_map.eval x = algebra.of_id C^โคโฎI,M;๐โฏโจxโฉ ๐
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 : ๐) :
@[protected, 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
- point_derivation I x = derivation ๐ C^โคโฎI,M;๐โฏโจxโฉ ๐
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) :
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) :
point_derivation I x โโ[๐] point_derivation I' 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.
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) :
point_derivation I x โโ[๐] point_derivation I' (โf x)
The homogeneous differential as a linear map.
@[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) :