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 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.
See also:
ContMDiffMul I n Gfor continuous differentiability of multiplicationG × G → Gin a single typeG,ContinuousSMul G Mfor continuity of an actionG × M → M.
Unlike for continuous actions, we do not currently have a class ContMDiffConstSMul. If there are
interesting examples satisfying ContMDiffConstSMul but not ContMDiffSMul, this can be added
later. (Note that such examples may be harder to find: in fact, 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.)
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
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)
:
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
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
instContMDiffSMulContinuousLinearMapIdModelWithCornersSelfOfCompleteSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace 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.