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. This theory coincides with the usual tangent bundle in the
case of finite-dimensional C^∞ real manifolds, but not in the general case.
instance
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 𝕜 ↑⊤)
Equations
instance
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 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
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 ℕ∞)
:
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
- PointedContMDiffMap 𝕜 I M n x✝ = ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n
@[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 ℕ∞)
:
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
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.
instance
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 (↑⊤) x) M 𝕜
instance
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 (↑⊤) x)
instance
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 (↑⊤) x)
instance
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 (↑⊤) x)
Equations
- PointedContMDiffMap.instInhabitedSomeENatTop I = { default := 0 }
instance
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 (↑⊤) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
Equations
instance
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 (↑⊤) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
instance
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 (↑⊤) x) 𝕜
ContMDiffMap.evalRingHom gives rise to an algebra structure of C^∞⟮I, M; 𝕜⟯ on 𝕜.
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)
:
With the evalAlgebra algebra structure evaluation is actually an algebra morphism.
Equations
- PointedContMDiffMap.eval x = Algebra.ofId (PointedContMDiffMap 𝕜 I M (↑⊤) x) 𝕜
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 (↑⊤) x)
(k : 𝕜)
:
instance
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 (↑⊤) 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, as this coincides with the usual tangent space for finite-dimensional C^∞ real
manifolds. The identification is not true in general, though.
Equations
- PointDerivation I x = Derivation 𝕜 (PointedContMDiffMap 𝕜 I M (↑⊤) x) 𝕜
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)
:
Evaluation at a point gives rise to a C^∞⟮I, M; 𝕜⟯-linear map between C^∞⟮I, M; 𝕜⟯ and 𝕜.
Equations
@[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)
:
Alias of ContMDiffFunction.evalAt.
Evaluation at a point gives rise to a C^∞⟮I, M; 𝕜⟯-linear map between C^∞⟮I, M; 𝕜⟯ and 𝕜.
Equations
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)
:
Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) →ₗ[𝕜] PointDerivation I x
The evaluation at a point as a linear map.
Equations
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 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤))
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
(x : M)
:
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' ↑⊤}
{x : M}
{y : M'}
(h : f x = 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.
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' ↑⊤)
(x : M)
:
The homogeneous differential as a linear map, denoted as 𝒅 within the Manifold namespace.
Equations
- fdifferential f x = hfdifferential ⋯
The homogeneous differential as a linear map, denoted as 𝒅 within the Manifold namespace.
Equations
- Manifold.«term𝒅» = Lean.ParserDescr.node `Manifold.«term𝒅» 1024 (Lean.ParserDescr.symbol "𝒅")
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
- Manifold.«term𝒅ₕ» = Lean.ParserDescr.node `Manifold.«term𝒅ₕ» 1024 (Lean.ParserDescr.symbol "𝒅ₕ")
@[simp]
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' ↑⊤)
{x : M}
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤)
:
@[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' ↑⊤)
{x : M}
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤)
:
Alias of fdifferential_apply.
@[simp]
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' ↑⊤}
{x : M}
{y : M'}
(h : f x = y)
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤)
:
@[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' ↑⊤}
{x : M}
{y : M'}
(h : f x = y)
(v : PointDerivation I x)
(g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤)
:
Alias of hfdifferential_apply.
@[simp]
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'' ↑⊤)
(f : ContMDiffMap I I' M M' ↑⊤)
(x : M)
: