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 𝕜 ⊤)
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
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.
Instances For
instance
PointedSmoothMap.funLike
{𝕜 : 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 fun x => 𝕜
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)
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)
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)
instance
PointedSmoothMap.instAlgebraPointedSmoothMapTopENatInstENatTopContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNormedRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopSemiringToSemiringToDivisionSemiringToSemifieldToFieldFieldSmoothRing
{𝕜 : 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 𝕜 ⊤)
instance
PointedSmoothMap.instIsScalarTowerPointedSmoothMapTopENatInstENatTopContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNormedRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfToSMulToCommSemiringToSemifieldToFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopInstAlgebraPointedSmoothMapTopENatInstENatTopToCommSemiringToSemifieldToFieldToNormedFieldToSemiringToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopToSMulSemiringToSemiringToDivisionSemiringFieldSmoothRingInstAlgebraPointedSmoothMapTopENatInstENatTopContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNormedRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfToCommSemiringInstCommRingPointedSmoothMapTopENatInstENatTopSemiringToSemiringToDivisionSemiringToSemifieldToFieldFieldSmoothRingInstSMul
{𝕜 : 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 𝕜 ⊤)
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 𝕜.
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.
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) 𝕜
@[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
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 𝕜.
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.
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.
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 = LinearMap.comp (fdifferential g (↑f x)) (fdifferential f x)