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.
Equations
- smooth_functions_algebra ๐ I M = smooth_map.algebra
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
- pointed_smooth_map ๐ I M n x = cont_mdiff_map I (model_with_corners_self ๐ ๐) M ๐ n
Instances for pointed_smooth_map
Equations
Equations
Equations
- pointed_smooth_map.inhabited I = {default := 0}
Equations
- pointed_smooth_map.cont_mdiff_map.algebra I = algebra.id (cont_mdiff_map I (model_with_corners_self ๐ ๐) M ๐ โค)
smooth_map.eval_ring_hom
gives rise to an algebra structure of C^โโฎI, M; ๐โฏ
on ๐
.
Equations
With the eval_algebra
algebra structure evaluation is actually an algebra morphism.
Equations
- pointed_smooth_map.eval x = algebra.of_id (pointed_smooth_map ๐ I M โค x) ๐
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 ๐ (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
The evaluation at a point as a linear map.
Equations
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
- hfdifferential h = {to_fun := ฮป (v : point_derivation I x), derivation.mk' {to_fun := ฮป (g : pointed_smooth_map ๐ I' M' โค y), โv (cont_mdiff_map.comp g f), map_add' := _, map_smul' := _} _, map_add' := _, map_smul' := _}
The homogeneous differential as a linear map.
Equations
- fdifferential f x = hfdifferential _