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.
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
- smoothFunctionsAlgebra 𝕜 I M = inferInstance
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 𝕜 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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 : ℕ∞)
:
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.
Equations
- PointedSmoothMap 𝕜 I M n x = ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
PointedSmoothMap.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 (PointedSmoothMap 𝕜 I M ⊤ x) M 𝕜
Equations
- PointedSmoothMap.instFunLike I = ContMDiffMap.instFunLike
instance
PointedSmoothMap.instCommRingPointedSmoothMapTopENatInstENatTop
{𝕜 : 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 (PointedSmoothMap 𝕜 I M ⊤ x)
Equations
- PointedSmoothMap.instCommRingPointedSmoothMapTopENatInstENatTop I = SmoothMap.commRing
instance
PointedSmoothMap.instAlgebraPointedSmoothMapTopENatInstENatTopToCommSemiringToSemifieldToFieldToNormedFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTop
{𝕜 : 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 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x)
Equations
- One or more equations did not get rendered due to their size.
instance
PointedSmoothMap.instInhabitedPointedSmoothMapTopENatInstENatTop
{𝕜 : 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 (PointedSmoothMap 𝕜 I M ⊤ x)
Equations
- PointedSmoothMap.instInhabitedPointedSmoothMapTopENatInstENatTop I = { default := 0 }
instance
PointedSmoothMap.instAlgebraPointedSmoothMapTopENatInstENatTopContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopSemiringToSemiringToDivisionSemiringToSemifieldToFieldFieldSmoothRing
{𝕜 : 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 (PointedSmoothMap 𝕜 I M ⊤ x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤)
Equations
- One or more equations did not get rendered due to their size.
instance
PointedSmoothMap.instIsScalarTowerPointedSmoothMapTopENatInstENatTopContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfToSMulToCommSemiringToSemifieldToFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopInstAlgebraPointedSmoothMapTopENatInstENatTopToCommSemiringToSemifieldToFieldToNormedFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopToSMulSemiringToSemiringToDivisionSemiringFieldSmoothRingInstAlgebraPointedSmoothMapTopENatInstENatTopContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopSemiringToSemiringToDivisionSemiringToSemifieldToFieldFieldSmoothRingInstSMul
{𝕜 : 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 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤)
Equations
- (_ : IsScalarTower 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤)) = (_ : IsScalarTower 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) (PointedSmoothMap 𝕜 I M ⊤ x))
instance
PointedSmoothMap.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 (PointedSmoothMap 𝕜 I M ⊤ x) 𝕜
SmoothMap.evalRingHom gives rise to an algebra structure of C^∞⟮I, M; 𝕜⟯ on 𝕜.
Equations
- PointedSmoothMap.evalAlgebra = RingHom.toAlgebra (SmoothMap.evalRingHom x)
def
PointedSmoothMap.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)
:
ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤ →ₐ[PointedSmoothMap 𝕜 I M ⊤ x] 𝕜
With the evalAlgebra algebra structure evaluation is actually an algebra morphism.
Equations
- PointedSmoothMap.eval x = Algebra.ofId (PointedSmoothMap 𝕜 I M ⊤ x) 𝕜
Instances For
theorem
PointedSmoothMap.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 : PointedSmoothMap 𝕜 I M ⊤ x)
(k : 𝕜)
:
instance
PointedSmoothMap.instIsScalarTowerPointedSmoothMapTopENatInstENatTopToSMulToCommSemiringToSemifieldToFieldToNormedFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopInstAlgebraPointedSmoothMapTopENatInstENatTopToCommSemiringToSemifieldToFieldToNormedFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopToSMulToSemiringToDivisionSemiringEvalAlgebraToSMulToAlgebraToSeminormedRingToSeminormedCommRingToNormedCommRingId
{𝕜 : 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 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) 𝕜
Equations
- (_ : IsScalarTower 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) 𝕜) = (_ : IsScalarTower 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) 𝕜)
@[reducible]
def
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_1 u_4) u_1)
The derivations at a point of a manifold. Some regard this as a possible definition of the tangent space
Equations
- PointDerivation I x = Derivation 𝕜 (PointedSmoothMap 𝕜 I M ⊤ x) 𝕜
Instances For
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)
:
ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤ →ₗ[PointedSmoothMap 𝕜 I M ⊤ x] 𝕜
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)
:
Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤) →ₗ[𝕜] PointDerivation I x
The evaluation at a point as a linear map.
Equations
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 𝕜 ⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤))
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ⊤)
(x : M)
:
((Derivation.evalAt x) X) f = (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' ⊤}
{x : M}
{y : M'}
(h : f x = y)
:
PointDerivation I x →ₗ[𝕜] PointDerivation 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.
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' ⊤)
(x : M)
:
PointDerivation I x →ₗ[𝕜] PointDerivation I' (f x)
The homogeneous differential as a linear map.
Equations
- fdifferential f x = hfdifferential (_ : f x = f x)
Instances For
Equations
- Manifold.«term𝒅» = Lean.ParserDescr.node `Manifold.term𝒅 1024 (Lean.ParserDescr.symbol "𝒅")
Instances For
Equations
- Manifold.«term𝒅ₕ» = Lean.ParserDescr.node `Manifold.term𝒅ₕ 1024 (Lean.ParserDescr.symbol "𝒅ₕ")
Instances For
@[simp]
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' 𝕜 ⊤)
:
((fdifferential f x) v) g = v (ContMDiffMap.comp g f)
@[simp]
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' 𝕜 ⊤)
:
((hfdifferential h) v) g = ((fdifferential f x) v) g
@[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)
:
fdifferential (ContMDiffMap.comp g f) x = fdifferential g (f x) ∘ₗ fdifferential f x