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.
Type synonym, introduced to put a different
has_scalar action on
C^n⟮I, M; 𝕜⟯
which is defined as
f • r = f(x) * r.
smooth_map.eval_ring_hom gives rise to an algebra structure of
C^∞⟮I, M; 𝕜⟯ on
eval_algebra algebra structure evaluation is actually an algebra morphism.
The derivations at a point of a manifold. Some regard this as a possible definition of the tangent space
Evaluation at a point gives rise to a
C^∞⟮I, M; 𝕜⟯-linear map between
C^∞⟮I, M; 𝕜⟯ and
The evaluation at a point as a linear map.
The heterogeneous differential as a linear map. Instead of taking a function as an argument this
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.
The homogeneous differential as a linear map.