Cⁿ monoid actions #
In this file we define Cⁿ actions (e.g. by Lie groups or monoids) on manifolds: we say
ContMDiffSMul I I' n G M if G acts multiplicatively on M and the action map
fun p : G × M ↦ p.1 • p.2 is Cⁿ. We also provide API for additive actions using @[to_additive].
We also define ContMDiffConstSMul I n Γ M, stating that for each γ : Γ, the map
fun x : M ↦ γ • x is Cⁿ. Unlike ContMDiffSMul, this requires no topology or charted space
structure on Γ, so it applies for example to actions of discrete groups by Cⁿ maps, such as the
properly discontinuous actions used to construct quotient manifolds.
TODO: For actions of Lie groups the two classes are close: a continuous action of a Lie group G on
a finite-dimensional manifold M is C^n provided it is C^n in the second variable.)
We also provide ContMDiffSMul instances for scalar multiplication in normed spaces and for
the action of the monoid E →L[𝕜] E of continuous linear maps on any normed space E.
For a group G acting smoothly on M, we define Diffeomorph.smul, scalar multiplication by a
fixed g : G as a diffeomorphism of M (in analogy to Homeomorph.smul).
See also:
ContMDiffMul I n Gfor continuous differentiability of multiplicationG × G → Gin a single typeG,ContinuousSMul G Mfor continuity of an actionG × M → M,ContinuousConstSMul Γ Mfor continuity offun x ↦ γ • xfor eachγ : Γ.
class
ContMDiffVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(I' : ModelWithCorners 𝕜 E' H')
(n : WithTop ℕ∞)
(G : Type u_6)
[TopologicalSpace G]
[ChartedSpace H G]
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
:
Basic typeclass stating that the additive action of G on M is Cⁿ as a function G × M → M.
Unlike with ContMDiffAdd (the class stating that addition G × G → G within a single type G is
Cⁿ), we do not extend IsManifold because ContMDiffVAdd contains more
explicit arguments than IsManifold and so ContMDiffVAdd.toIsManifold could not be an instance
anyway: this means that in order for ContMDiffVAdd to be meaningful, smoothness of G and M
have to be required separately. For example, to state that G is a Cⁿ additive Lie group with a Cⁿ
additive action on a Cⁿ manifold M, one can use the typeclasses
[LieAddGroup I n G] [IsManifold I' n M] [ContMDiffVAdd I I' n G M].
Instances
class
ContMDiffSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(I' : ModelWithCorners 𝕜 E' H')
(n : WithTop ℕ∞)
(G : Type u_6)
[TopologicalSpace G]
[ChartedSpace H G]
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
:
Basic typeclass stating that the action of G on M is Cⁿ as a function G × M → M.
Unlike with ContMDiffMul (the class stating that multiplication G × G → G within a single type
G is Cⁿ), we do not extend IsManifold because ContMDiffSMul contains more
explicit arguments than IsManifold and so ContMDiffSMul.toIsManifold could not be an instance
anyway: this means that in order for ContMDiffSMul to be meaningful, smoothness of G and M
have to be required separately. For example, to state that G is a Cⁿ Lie group with a Cⁿ action on
a Cⁿ manifold M, one can use the typeclasses
[LieGroup I n G] [IsManifold I' n M] [ContMDiffSMul I I' n G M].
Instances
class
ContMDiffConstVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
(Γ : Type u_4)
(M : Type u_5)
[TopologicalSpace M]
[ChartedSpace H M]
[VAdd Γ M]
:
Typeclass stating that for each γ : Γ, the additive action fun x : M ↦ γ +ᵥ x is Cⁿ.
Unlike ContMDiffVAdd (which requires the action to be Cⁿ jointly as a map Γ × M → M), no
topology or manifold structure on Γ is required, so this class also covers additive actions of
discrete groups by Cⁿ maps.
For each
γ : Γ, the mapfun x : M ↦ γ +ᵥ xis Cⁿ.
Instances
class
ContMDiffConstSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
(Γ : Type u_4)
(M : Type u_5)
[TopologicalSpace M]
[ChartedSpace H M]
[SMul Γ M]
:
Typeclass stating that for each γ : Γ, the scalar multiplication fun x : M ↦ γ • x is Cⁿ.
Unlike ContMDiffSMul (which requires the action to be Cⁿ jointly as a map Γ × M → M), no
topology or manifold structure on Γ is required, so this class also covers actions of discrete
groups by Cⁿ maps, e.g. the properly discontinuous actions used to construct quotient manifolds.
For each
γ : Γ, the mapfun x : M ↦ γ • xis Cⁿ.
Instances
theorem
ContMDiffSMul.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
{n m : WithTop ℕ∞}
(h : n ≤ m)
[ContMDiffSMul I I' m G M]
:
ContMDiffSMul I I' n G M
theorem
ContMDiffVAdd.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
{n m : WithTop ℕ∞}
(h : n ≤ m)
[ContMDiffVAdd I I' m G M]
:
ContMDiffVAdd I I' n G M
instance
instContMDiffSMulOfSomeENatTopOfLEInfty
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' (↑⊤) G M]
[ENat.LEInfty n]
:
ContMDiffSMul I I' n G M
instance
instContMDiffVAddOfSomeENatTopOfLEInfty
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' (↑⊤) G M]
[ENat.LEInfty n]
:
ContMDiffVAdd I I' n G M
instance
instContMDiffSMulOfTopWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' ⊤ G M]
:
ContMDiffSMul I I' n G M
instance
instContMDiffVAddOfTopWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' ⊤ G M]
:
ContMDiffVAdd I I' n G M
instance
instContMDiffSMulOfNatWithTopENatOfContinuousSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
[ContinuousSMul G M]
:
ContMDiffSMul I I' 0 G M
instance
instContMDiffVAddOfNatWithTopENatOfContinuousVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
[ContinuousVAdd G M]
:
ContMDiffVAdd I I' 0 G M
instance
instContMDiffSMulOfNatWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
[ContMDiffSMul I I' 2 G M]
:
ContMDiffSMul I I' 1 G M
instance
instContMDiffVAddOfNatWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
[ContMDiffVAdd I I' 2 G M]
:
ContMDiffVAdd I I' 1 G M
theorem
ContMDiffSMul.continuousSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
(n : WithTop ℕ∞)
[ContMDiffSMul I I' n G M]
:
ContinuousSMul G M
If an action is Cⁿ for some n, it is also continuous. This has to be a theorem instead of an
instance because ContMDiffSMul depends on parameters I, I' and n that ContinuousSMul
doesn't.
theorem
ContMDiffVAdd.continuousVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
(n : WithTop ℕ∞)
[ContMDiffVAdd I I' n G M]
:
ContinuousVAdd G M
instance
ContMDiffMul.contMDiffSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
[Mul G]
{n : WithTop ℕ∞}
[ContMDiffMul I n G]
:
ContMDiffSMul I I n G G
For any G in which multiplication is Cⁿ, the action of G on itself via left multiplication
is Cⁿ too.
theorem
ContMDiffWithinAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
{f : N → G}
{g : N → M}
{s : Set N}
{x : N}
(hf : ContMDiffWithinAt I'' I n f s x)
(hg : ContMDiffWithinAt I'' I' n g s x)
:
ContMDiffWithinAt I'' I' n (f • g) s x
theorem
ContMDiffWithinAt.vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
{f : N → G}
{g : N → M}
{s : Set N}
{x : N}
(hf : ContMDiffWithinAt I'' I n f s x)
(hg : ContMDiffWithinAt I'' I' n g s x)
:
ContMDiffWithinAt I'' I' n (f +ᵥ g) s x
theorem
ContMDiffAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
{f : N → G}
{g : N → M}
{x : N}
(hf : ContMDiffAt I'' I n f x)
(hg : ContMDiffAt I'' I' n g x)
:
ContMDiffAt I'' I' n (f • g) x
theorem
ContMDiffAt.vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
{f : N → G}
{g : N → M}
{x : N}
(hf : ContMDiffAt I'' I n f x)
(hg : ContMDiffAt I'' I' n g x)
:
ContMDiffAt I'' I' n (f +ᵥ g) x
theorem
ContMDiffOn.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
{f : N → G}
{g : N → M}
{s : Set N}
(hf : ContMDiffOn I'' I n f s)
(hg : ContMDiffOn I'' I' n g s)
:
ContMDiffOn I'' I' n (f • g) s
theorem
ContMDiffOn.vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
{f : N → G}
{g : N → M}
{s : Set N}
(hf : ContMDiffOn I'' I n f s)
(hg : ContMDiffOn I'' I' n g s)
:
ContMDiffOn I'' I' n (f +ᵥ g) s
theorem
ContMDiff.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
{f : N → G}
{g : N → M}
(hf : ContMDiff I'' I n f)
(hg : ContMDiff I'' I' n g)
:
theorem
ContMDiff.vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
{f : N → G}
{g : N → M}
(hf : ContMDiff I'' I n f)
(hg : ContMDiff I'' I' n g)
:
theorem
ContMDiffSMul.contMDiff_const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[SMul G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
(g : G)
:
theorem
ContMDiffVAdd.contMDiff_const_vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[VAdd G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
(g : G)
:
instance
Prod.contMDiffSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[SMul G M]
[SMul G N]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
[ContMDiffSMul I I'' n G N]
:
ContMDiffSMul I (I'.prod I'') n G (M × N)
instance
Prod.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H'' N]
[VAdd G M]
[VAdd G N]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
[ContMDiffVAdd I I'' n G N]
:
ContMDiffVAdd I (I'.prod I'') n G (M × N)
theorem
IsScalarTower.contMDiffSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
(G' : Type u_11)
[TopologicalSpace G']
[ChartedSpace H'' G']
[Monoid G']
[SMul G G']
[MulAction G' M]
[SMul G M]
[IsScalarTower G G' M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I'' n G G']
[ContMDiffSMul I'' I' n G' M]
:
ContMDiffSMul I I' n G M
If G acts continuously differentiably on G' and G' acts continuously differentiably on
M, then G acts continuously differentiably on M.
theorem
VAddAssocClass.contMDiffVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
(G' : Type u_11)
[TopologicalSpace G']
[ChartedSpace H'' G']
[AddMonoid G']
[VAdd G G']
[AddAction G' M]
[VAdd G M]
[VAddAssocClass G G' M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I'' n G G']
[ContMDiffVAdd I'' I' n G' M]
:
ContMDiffVAdd I I' n G M
theorem
MulAction.contMDiffSMul_compHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[Monoid G]
[MulAction G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
{G' : Type u_11}
[TopologicalSpace G']
[ChartedSpace H'' G']
[Monoid G']
{f : G' →* G}
(hf : ContMDiff I'' I n ⇑f)
:
ContMDiffSMul I'' I' n G' M
If an action is continuously differentiable, then post-composing this action with a continuously differentiable homomorphism gives again a continuously differentiable action.
theorem
AddAction.contMDiffVAdd_compHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{H'' : Type u_6}
[TopologicalSpace H'']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G : Type u_8}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H' M]
[AddMonoid G]
[AddAction G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
{G' : Type u_11}
[TopologicalSpace G']
[ChartedSpace H'' G']
[AddMonoid G']
{f : G' →+ G}
(hf : ContMDiff I'' I n ⇑f)
:
ContMDiffVAdd I'' I' n G' M
instance
instContMDiffSMulModelWithCornersSelf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : WithTop ℕ∞}
:
ContMDiffSMul (modelWithCornersSelf 𝕜 𝕜) (modelWithCornersSelf 𝕜 E) n 𝕜 E
The scalar multiplication 𝕜 × E → E of any normed vector space E over 𝕜 is smooth.
instance
instContMDiffSMulContinuousLinearMapIdModelWithCornersSelf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : WithTop ℕ∞}
:
ContMDiffSMul (modelWithCornersSelf 𝕜 (E →L[𝕜] E)) (modelWithCornersSelf 𝕜 E) n (E →L[𝕜] E) E
The monoid E →L[𝕜] E of continuous linear endomorphisms of E acts smoothly on E.
theorem
ContMDiffConstSMul.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
{n m : WithTop ℕ∞}
(h : n ≤ m)
[ContMDiffConstSMul I m Γ M]
:
ContMDiffConstSMul I n Γ M
theorem
ContMDiffConstVAdd.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
{n m : WithTop ℕ∞}
(h : n ≤ m)
[ContMDiffConstVAdd I m Γ M]
:
ContMDiffConstVAdd I n Γ M
instance
instContMDiffConstSMulOfSomeENatTopOfLEInfty
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstSMul I (↑⊤) Γ M]
[ENat.LEInfty n]
:
ContMDiffConstSMul I n Γ M
instance
instContMDiffConstVAddOfSomeENatTopOfLEInfty
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I (↑⊤) Γ M]
[ENat.LEInfty n]
:
ContMDiffConstVAdd I n Γ M
instance
instContMDiffConstSMulOfTopWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstSMul I ⊤ Γ M]
:
ContMDiffConstSMul I n Γ M
instance
instContMDiffConstVAddOfTopWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I ⊤ Γ M]
:
ContMDiffConstVAdd I n Γ M
instance
instContMDiffConstSMulOfNatWithTopENatOfContinuousConstSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
[ContinuousConstSMul Γ M]
:
ContMDiffConstSMul I 0 Γ M
instance
instContMDiffConstVAddOfNatWithTopENatOfContinuousConstVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
[ContinuousConstVAdd Γ M]
:
ContMDiffConstVAdd I 0 Γ M
instance
instContMDiffConstSMulOfNatWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
[ContMDiffConstSMul I 2 Γ M]
:
ContMDiffConstSMul I 1 Γ M
instance
instContMDiffConstVAddOfNatWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
[ContMDiffConstVAdd I 2 Γ M]
:
ContMDiffConstVAdd I 1 Γ M
theorem
ContMDiffConstSMul.continuousConstSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
(n : WithTop ℕ∞)
[ContMDiffConstSMul I n Γ M]
:
If an action is Cⁿ for some n, it is also continuous. This has to be a theorem instead of an
instance because ContMDiffConstSMul depends on parameters I and n that ContinuousConstSMul
doesn't.
theorem
ContMDiffConstVAdd.continuousConstVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
(n : WithTop ℕ∞)
[ContMDiffConstVAdd I n Γ M]
:
theorem
ContMDiffWithinAt.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstSMul I n Γ M]
{f : N → M}
{s : Set N}
{x : N}
(hf : ContMDiffWithinAt I' I n f s x)
(γ : Γ)
:
ContMDiffWithinAt I' I n (γ • f) s x
theorem
ContMDiffWithinAt.const_vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I n Γ M]
{f : N → M}
{s : Set N}
{x : N}
(hf : ContMDiffWithinAt I' I n f s x)
(γ : Γ)
:
ContMDiffWithinAt I' I n (γ +ᵥ f) s x
theorem
ContMDiffAt.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstSMul I n Γ M]
{f : N → M}
{x : N}
(hf : ContMDiffAt I' I n f x)
(γ : Γ)
:
ContMDiffAt I' I n (γ • f) x
theorem
ContMDiffAt.const_vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I n Γ M]
{f : N → M}
{x : N}
(hf : ContMDiffAt I' I n f x)
(γ : Γ)
:
ContMDiffAt I' I n (γ +ᵥ f) x
theorem
ContMDiffOn.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstSMul I n Γ M]
{f : N → M}
{s : Set N}
(hf : ContMDiffOn I' I n f s)
(γ : Γ)
:
ContMDiffOn I' I n (γ • f) s
theorem
ContMDiffOn.const_vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I n Γ M]
{f : N → M}
{s : Set N}
(hf : ContMDiffOn I' I n f s)
(γ : Γ)
:
ContMDiffOn I' I n (γ +ᵥ f) s
theorem
ContMDiff.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstSMul I n Γ M]
{f : N → M}
(hf : ContMDiff I' I n f)
(γ : Γ)
:
theorem
ContMDiff.const_vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I n Γ M]
{f : N → M}
(hf : ContMDiff I' I n f)
(γ : Γ)
:
instance
Prod.contMDiffConstSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
[SMul Γ N]
[ContMDiffConstSMul I n Γ M]
[ContMDiffConstSMul I' n Γ N]
:
ContMDiffConstSMul (I.prod I') n Γ (M × N)
instance
Prod.contMDiffConstVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
[VAdd Γ N]
[ContMDiffConstVAdd I n Γ M]
[ContMDiffConstVAdd I' n Γ N]
:
ContMDiffConstVAdd (I.prod I') n Γ (M × N)
theorem
IsScalarTower.contMDiffConstSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[SMul Γ M]
{n : WithTop ℕ∞}
(Γ' : Type u_9)
[Monoid Γ']
[SMul Γ Γ']
[MulAction Γ' M]
[IsScalarTower Γ Γ' M]
[ContMDiffConstSMul I n Γ' M]
:
ContMDiffConstSMul I n Γ M
If the action on M by any element of Γ' is continuously differentiable, and Γ acts on Γ'
such that Γ, Γ' and M form a scalar tower, then the induced action on M by any element of
Γ is continuously differentiable as well.
theorem
VAddAssocClass.contMDiffConstVAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{Γ : Type u_8}
[VAdd Γ M]
{n : WithTop ℕ∞}
(Γ' : Type u_9)
[AddMonoid Γ']
[VAdd Γ Γ']
[AddAction Γ' M]
[VAddAssocClass Γ Γ' M]
[ContMDiffConstVAdd I n Γ' M]
:
ContMDiffConstVAdd I n Γ M
theorem
MulAction.contMDiffConstSMul_compHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{Γ : Type u_9}
{Γ' : Type u_10}
[Monoid Γ]
[MulAction Γ M]
[ContMDiffConstSMul I n Γ M]
[Monoid Γ']
{f : Γ' →* Γ}
:
ContMDiffConstSMul I n Γ' M
If the action on M by any element of Γ is continuously differentiable, then post-composing
this action with any homomorphism f : Γ' →* Γ makes again the action on M by any element of Γ'
continuously differentiable .
theorem
AddAction.contMDiffConstVAdd_compHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{Γ : Type u_9}
{Γ' : Type u_10}
[AddMonoid Γ]
[AddAction Γ M]
[ContMDiffConstVAdd I n Γ M]
[AddMonoid Γ']
{f : Γ' →+ Γ}
:
ContMDiffConstVAdd I n Γ' M
def
Diffeomorph.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(I' : ModelWithCorners 𝕜 E' H')
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[Group G]
[MulAction G M]
(n : WithTop ℕ∞)
[ContMDiffSMul I I' n G M]
(g : G)
:
Diffeomorph I' I' M M n
The diffeomorphism given by scalar multiplication by an element of a group G acting
Cⁿ-differentiably on a manifold M is a diffeomorphism from M to itself. Its inverse is scalar
multiplication by g⁻¹.
Equations
- Diffeomorph.smul I I' n g = { toEquiv := MulAction.toPerm g, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
def
Diffeomorph.vadd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(I' : ModelWithCorners 𝕜 E' H')
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[AddGroup G]
[AddAction G M]
(n : WithTop ℕ∞)
[ContMDiffVAdd I I' n G M]
(g : G)
:
Diffeomorph I' I' M M n
The diffeomorphism given by affine-addition of an element of an additive group G acting
Cⁿ-differentiably on a manifold M is a diffeomorphism from M to itself. Its inverse is
addition of -g.
Equations
- Diffeomorph.vadd I I' n g = { toEquiv := AddAction.toPerm g, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
@[simp]
theorem
Diffeomorph.smul_toHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[Group G]
[MulAction G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
(g : G)
:
@[simp]
theorem
Diffeomorph.vadd_toHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[AddGroup G]
[AddAction G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
(g : G)
:
@[simp]
theorem
Diffeomorph.smul_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[Group G]
[MulAction G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
(g : G)
(x : M)
:
@[simp]
theorem
Diffeomorph.vadd_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[AddGroup G]
[AddAction G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
(g : G)
(x : M)
:
@[simp]
theorem
Diffeomorph.smul_symm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[Group G]
[MulAction G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
(g : G)
(x : M)
:
@[simp]
theorem
Diffeomorph.vadd_symm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[AddGroup G]
[AddAction G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
(g : G)
(x : M)
:
theorem
Diffeomorph.smul_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[Group G]
[MulAction G M]
{n : WithTop ℕ∞}
[ContMDiffSMul I I' n G M]
(g : G)
:
theorem
Diffeomorph.vadd_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[TopologicalSpace G]
[ChartedSpace H G]
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
[AddGroup G]
[AddAction G M]
{n : WithTop ℕ∞}
[ContMDiffVAdd I I' n G M]
(g : G)
: