Derivation bundle #
In this file we define the derivations at a point of a manifold on the algebra of smooth functions. 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.
def
smoothFunctionsAlgebra
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_4)
[TopologicalSpace M]
[ChartedSpace H M]
:
Algebra 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
Equations
- Eq (smoothFunctionsAlgebra 𝕜 I M) inferInstance
Instances For
theorem
smooth_functions_tower
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_4)
[TopologicalSpace M]
[ChartedSpace H M]
:
IsScalarTower 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
def
PointedContMDiffMap
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_4)
[TopologicalSpace M]
[ChartedSpace H M]
(n : WithTop ENat)
:
M → Type (max 0 u_4 u_1)
Type synonym, introduced to put a different SMul action on C^n⟮I, M; 𝕜⟯
which is defined as f • r = f(x) * r.
Denoted as C^n⟮I, M; 𝕜⟯⟨x⟩ within the Derivation namespace.
Equations
- Eq (PointedContMDiffMap 𝕜 I M n x✝) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
Instances For
@[deprecated PointedContMDiffMap (since := "2025-01-09")]
def
PointedSmoothMap
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_4)
[TopologicalSpace M]
[ChartedSpace H M]
(n : WithTop ENat)
:
M → Type (max 0 u_4 u_1)
Alias of PointedContMDiffMap.
Type synonym, introduced to put a different SMul action on C^n⟮I, M; 𝕜⟯
which is defined as f • r = f(x) * r.
Denoted as C^n⟮I, M; 𝕜⟯⟨x⟩ within the Derivation namespace.
Equations
Instances For
Type synonym, introduced to put a different SMul action on C^n⟮I, M; 𝕜⟯
which is defined as f • r = f(x) * r.
Denoted as C^n⟮I, M; 𝕜⟯⟨x⟩ within the Derivation namespace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
PointedContMDiffMap.instFunLike
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
FunLike (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x) M 𝕜
Equations
Instances For
def
PointedContMDiffMap.instCommRingSomeENatTop
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
CommRing (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
Instances For
def
PointedContMDiffMap.instAlgebraSomeENatTop
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
Algebra 𝕜 (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
Instances For
def
PointedContMDiffMap.instInhabitedSomeENatTop
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
Inhabited (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
Equations
- Eq (PointedContMDiffMap.instInhabitedSomeENatTop I) { default := 0 }
Instances For
def
PointedContMDiffMap.instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
Algebra (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
Equations
Instances For
theorem
PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
IsScalarTower 𝕜 (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
def
PointedContMDiffMap.evalAlgebra
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
Algebra (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x) 𝕜
ContMDiffMap.evalRingHom gives rise to an algebra structure of C^∞⟮I, M; 𝕜⟯ on 𝕜.
Instances For
def
PointedContMDiffMap.eval
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
AlgHom (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top)) 𝕜
With the evalAlgebra algebra structure evaluation is actually an algebra morphism.
Equations
- Eq (PointedContMDiffMap.eval x) (Algebra.ofId (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x) 𝕜)
Instances For
theorem
PointedContMDiffMap.smul_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
(f : PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x)
(k : 𝕜)
:
Eq (HSMul.hSMul f k) (HMul.hMul (DFunLike.coe f x) k)
theorem
PointedContMDiffMap.instIsScalarTowerSomeENatTop
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
IsScalarTower 𝕜 (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x) 𝕜
@[reducible, inline]
abbrev
PointDerivation
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
Type (max (max u_4 u_1) u_1)
The derivations at a point of a manifold. Some regard this as a possible definition of the tangent space
Equations
- Eq (PointDerivation I x) (Derivation 𝕜 (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x) 𝕜)
Instances For
def
ContMDiffFunction.evalAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
LinearMap (RingHom.id (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x))
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top)) 𝕜
Evaluation at a point gives rise to a C^∞⟮I, M; 𝕜⟯-linear map between C^∞⟮I, M; 𝕜⟯ and 𝕜.
Equations
Instances For
@[deprecated ContMDiffFunction.evalAt (since := "2025-01-09")]
def
SmoothFunction.evalAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
LinearMap (RingHom.id (PointedContMDiffMap 𝕜 I M (WithTop.some Top.top) x))
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top)) 𝕜
Alias of ContMDiffFunction.evalAt.
Evaluation at a point gives rise to a C^∞⟮I, M; 𝕜⟯-linear map between C^∞⟮I, M; 𝕜⟯ and 𝕜.
Equations
Instances For
def
Derivation.evalAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
LinearMap (RingHom.id 𝕜)
(Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top)))
(PointDerivation I x)
The evaluation at a point as a linear map.
Equations
- Eq (Derivation.evalAt x) (ContMDiffFunction.evalAt I x).compDer
Instances For
theorem
Derivation.evalAt_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(X :
Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top)))
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some Top.top))
(x : M)
:
Eq (DFunLike.coe (DFunLike.coe (evalAt x) X) f) (DFunLike.coe (DFunLike.coe X f) x)
def
hfdifferential
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : ContMDiffMap I I' M M' (WithTop.some Top.top)}
{x : M}
{y : M'}
(h : Eq (DFunLike.coe f x) y)
:
LinearMap (RingHom.id 𝕜) (PointDerivation I x) (PointDerivation I' y)
The heterogeneous differential as a linear map, denoted as 𝒅ₕ within the Manifold namespace.
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
- One or more equations did not get rendered due to their size.
Instances For
def
fdifferential
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(f : ContMDiffMap I I' M M' (WithTop.some Top.top))
(x : M)
:
LinearMap (RingHom.id 𝕜) (PointDerivation I x) (PointDerivation I' (DFunLike.coe f x))
The homogeneous differential as a linear map, denoted as 𝒅 within the Manifold namespace.
Equations
- Eq (fdifferential f x) (hfdifferential ⋯)
Instances For
The homogeneous differential as a linear map, denoted as 𝒅 within the Manifold namespace.
Equations
- Eq Manifold.«term𝒅» (Lean.ParserDescr.node `Manifold.«term𝒅» 1024 (Lean.ParserDescr.symbol "𝒅"))
Instances For
The heterogeneous differential as a linear map, denoted as 𝒅ₕ within the Manifold namespace.
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
- Eq Manifold.«term𝒅ₕ» (Lean.ParserDescr.node `Manifold.«term𝒅ₕ» 1024 (Lean.ParserDescr.symbol "𝒅ₕ"))
Instances For
theorem
fdifferential_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(f : ContMDiffMap I I' M M' (WithTop.some Top.top))
{x : M}
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 (WithTop.some Top.top))
:
Eq (DFunLike.coe (DFunLike.coe (fdifferential f x) v) g) (DFunLike.coe v (g.comp f))
@[deprecated fdifferential_apply (since := "2024-11-11")]
theorem
apply_fdifferential
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(f : ContMDiffMap I I' M M' (WithTop.some Top.top))
{x : M}
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 (WithTop.some Top.top))
:
Eq (DFunLike.coe (DFunLike.coe (fdifferential f x) v) g) (DFunLike.coe v (g.comp f))
Alias of fdifferential_apply.
theorem
hfdifferential_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : ContMDiffMap I I' M M' (WithTop.some Top.top)}
{x : M}
{y : M'}
(h : Eq (DFunLike.coe f x) y)
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 (WithTop.some Top.top))
:
Eq (DFunLike.coe (DFunLike.coe (hfdifferential h) v) g) (DFunLike.coe (DFunLike.coe (fdifferential f x) v) g)
@[deprecated hfdifferential_apply (since := "2024-11-11")]
theorem
apply_hfdifferential
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : ContMDiffMap I I' M M' (WithTop.some Top.top)}
{x : M}
{y : M'}
(h : Eq (DFunLike.coe f x) y)
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 (WithTop.some Top.top))
:
Eq (DFunLike.coe (DFunLike.coe (hfdifferential h) v) g) (DFunLike.coe (DFunLike.coe (fdifferential f x) v) g)
Alias of hfdifferential_apply.
theorem
fdifferential_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
(g : ContMDiffMap I' I'' M' M'' (WithTop.some Top.top))
(f : ContMDiffMap I I' M M' (WithTop.some Top.top))
(x : M)
:
Eq (fdifferential (g.comp f) x) ((fdifferential g (DFunLike.coe f x)).comp (fdifferential f x))