Algebraic structures over C^n functions #
In this file, we define instances of algebraic structures over C^n functions.
instance
ContMDiffMap.instMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
:
Mul (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.instAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
:
Add (ContMDiffMap I I' N G n)
Equations
@[simp]
theorem
ContMDiffMap.coe_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
(f g : ContMDiffMap I I' N G n)
:
@[simp]
theorem
ContMDiffMap.coe_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
(f g : ContMDiffMap I I' N G n)
:
@[simp]
theorem
ContMDiffMap.mul_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{N' : Type u_9}
[TopologicalSpace N']
[ChartedSpace H'' N']
{n : WithTop ℕ∞}
{G : Type u_10}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
(f g : ContMDiffMap I'' I' N' G n)
(h : ContMDiffMap I I'' N N' n)
:
@[simp]
theorem
ContMDiffMap.add_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{N' : Type u_9}
[TopologicalSpace N']
[ChartedSpace H'' N']
{n : WithTop ℕ∞}
{G : Type u_10}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
(f g : ContMDiffMap I'' I' N' G n)
(h : ContMDiffMap I I'' N N' n)
:
instance
ContMDiffMap.instOne
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[One G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
One (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.instZero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Zero G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
Zero (ContMDiffMap I I' N G n)
Equations
@[simp]
theorem
ContMDiffMap.coe_one
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[One G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
@[simp]
theorem
ContMDiffMap.coe_zero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Zero G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
instance
ContMDiffMap.instNSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
:
SMul ℕ (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.instPow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
:
Pow (ContMDiffMap I I' N G n) ℕ
Equations
@[simp]
theorem
ContMDiffMap.coe_pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
(f : ContMDiffMap I I' N G n)
(n✝ : ℕ)
:
@[simp]
theorem
ContMDiffMap.coe_nsmul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
(f : ContMDiffMap I I' N G n)
(n✝ : ℕ)
:
Group structure #
In this section we show that C^n functions valued in a Lie group inherit a group structure
under pointwise multiplication.
instance
ContMDiffMap.semigroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Semigroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
:
Semigroup (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.addSemigroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddSemigroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
:
AddSemigroup (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.monoid
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
:
Monoid (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.addMonoid
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
:
AddMonoid (ContMDiffMap I I' N G n)
Equations
def
ContMDiffMap.coeFnMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
:
Coercion to a function as a MonoidHom. Similar to MonoidHom.coeFn.
Equations
Instances For
def
ContMDiffMap.coeFnAddMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
:
Coercion to a function as an AddMonoidHom.
Similar to AddMonoidHom.coeFn.
Equations
Instances For
@[simp]
theorem
ContMDiffMap.coeFnMonoidHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
(a✝ : ContMDiffMap I I' N G n)
(a : N)
:
@[simp]
theorem
ContMDiffMap.coeFnAddMonoidHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
(a✝ : ContMDiffMap I I' N G n)
(a : N)
:
def
ContMDiffMap.compLeftMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_6)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{n : WithTop ℕ∞}
{G' : Type u_10}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[ContMDiffMul I' n G']
{G'' : Type u_11}
[Monoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[ContMDiffMul I'' n G'']
(φ : G' →* G'')
(hφ : ContMDiff I' I'' n ⇑φ)
:
For a manifold N and a C^n homomorphism φ between Lie groups G', G'', the
'left-composition-by-φ' group homomorphism from C^n⟮I, N; I', G'⟯ to C^n⟮I, N; I'', G''⟯.
Equations
Instances For
def
ContMDiffMap.compLeftAddMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_6)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{n : WithTop ℕ∞}
{G' : Type u_10}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[ContMDiffAdd I' n G']
{G'' : Type u_11}
[AddMonoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[ContMDiffAdd I'' n G'']
(φ : G' →+ G'')
(hφ : ContMDiff I' I'' n ⇑φ)
:
For a manifold N and a C^n homomorphism φ between additive Lie groups G',
G'', the 'left-composition-by-φ' group homomorphism from C^n⟮I, N; I', G'⟯ to
C^n⟮I, N; I'', G''⟯.
Equations
Instances For
def
ContMDiffMap.restrictMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
(G : Type u_10)
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
{U V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
For a Lie group G and open sets U ⊆ V in N, the 'restriction' group homomorphism from
C^n⟮I, V; I', G⟯ to C^n⟮I, U; I', G⟯.
Equations
Instances For
def
ContMDiffMap.restrictAddMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
(G : Type u_10)
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
{U V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
For an additive Lie group G and open sets U ⊆ V in N, the 'restriction'
group homomorphism from C^n⟮I, V; I', G⟯ to C^n⟮I, U; I', G⟯.
Equations
Instances For
instance
ContMDiffMap.commMonoid
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffMul I' n G]
:
CommMonoid (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.addCommMonoid
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[ContMDiffAdd I' n G]
:
AddCommMonoid (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.group
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' n G]
:
Group (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.addGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' n G]
:
AddGroup (ContMDiffMap I I' N G n)
Equations
@[simp]
theorem
ContMDiffMap.coe_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' n G]
(f : ContMDiffMap I I' N G n)
:
@[simp]
theorem
ContMDiffMap.coe_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' n G]
(f : ContMDiffMap I I' N G n)
:
@[simp]
theorem
ContMDiffMap.coe_div
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' n G]
(f g : ContMDiffMap I I' N G n)
:
@[simp]
theorem
ContMDiffMap.coe_sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' n G]
(f g : ContMDiffMap I I' N G n)
:
instance
ContMDiffMap.commGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[CommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' n G]
:
CommGroup (ContMDiffMap I I' N G n)
Equations
instance
ContMDiffMap.addCommGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{G : Type u_10}
[AddCommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' n G]
:
AddCommGroup (ContMDiffMap I I' N G n)
Equations
Ring structure #
In this section we show that C^n functions valued in a C^n ring R inherit a ring structure
under pointwise multiplication.
instance
ContMDiffMap.semiring
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{R : Type u_10}
[Semiring R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
:
Semiring (ContMDiffMap I I' N R n)
Equations
instance
ContMDiffMap.ring
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{R : Type u_10}
[Ring R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
:
Ring (ContMDiffMap I I' N R n)
Equations
instance
ContMDiffMap.commRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
:
CommRing (ContMDiffMap I I' N R n)
Equations
def
ContMDiffMap.compLeftRingHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_6)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{n : WithTop ℕ∞}
{R' : Type u_10}
[Ring R']
[TopologicalSpace R']
[ChartedSpace H' R']
[ContMDiffRing I' n R']
{R'' : Type u_11}
[Ring R'']
[TopologicalSpace R'']
[ChartedSpace H'' R'']
[ContMDiffRing I'' n R'']
(φ : R' →+* R'')
(hφ : ContMDiff I' I'' n ⇑φ)
:
For a manifold N and a C^n homomorphism φ between C^n rings R', R'', the
'left-composition-by-φ' ring homomorphism from C^n⟮I, N; I', R'⟯ to C^n⟮I, N; I'', R''⟯.
Equations
Instances For
def
ContMDiffMap.restrictRingHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
(R : Type u_10)
[Ring R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
{U V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
For a "C^n ring" R and open sets U ⊆ V in N, the "restriction" ring homomorphism from
C^n⟮I, V; I', R⟯ to C^n⟮I, U; I', R⟯.
Equations
Instances For
def
ContMDiffMap.coeFnRingHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
:
Coercion to a function as a RingHom.
Equations
Instances For
@[simp]
theorem
ContMDiffMap.coeFnRingHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
(a✝ : ContMDiffMap I I' N R n)
(a : N)
:
def
ContMDiffMap.evalRingHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[ContMDiffRing I' n R]
(m : N)
:
Function.eval as a RingHom on the ring of C^n functions.
Equations
Instances For
Semimodule structure #
In this section we show that C^n functions valued in a vector space M over a normed
field 𝕜 inherit a vector space structure.
instance
ContMDiffMap.instSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
SMul 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
Equations
@[simp]
theorem
ContMDiffMap.coe_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(r : 𝕜)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
:
@[simp]
theorem
ContMDiffMap.smul_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{N' : Type u_9}
[TopologicalSpace N']
[ChartedSpace H'' N']
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(r : 𝕜)
(g : ContMDiffMap I'' (modelWithCornersSelf 𝕜 V) N' V n)
(h : ContMDiffMap I I'' N N' n)
:
instance
ContMDiffMap.module
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
Module 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
Equations
def
ContMDiffMap.coeFnLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
Coercion to a function as a LinearMap.
Equations
Instances For
@[simp]
theorem
ContMDiffMap.coeFnLinearMap_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(a✝ : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
(a : N)
:
Algebra structure #
In this section we show that C^n functions valued in a normed algebra A over a normed field 𝕜
inherit an algebra structure.
def
ContMDiffMap.C
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[ContMDiffRing (modelWithCornersSelf 𝕜 A) n A]
:
C^n constant functions as a RingHom.
Equations
Instances For
instance
ContMDiffMap.algebra
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[ContMDiffRing (modelWithCornersSelf 𝕜 A) n A]
:
Algebra 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n)
Equations
def
ContMDiffMap.coeFnAlgHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[ContMDiffRing (modelWithCornersSelf 𝕜 A) n A]
:
Coercion to a function as an AlgHom.
Equations
Instances For
@[simp]
theorem
ContMDiffMap.coeFnAlgHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[ContMDiffRing (modelWithCornersSelf 𝕜 A) n A]
(a✝ : ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n)
(a : N)
:
Structure as module over scalar functions #
If V is a module over 𝕜, then we show that the space of C^n functions from N to V
is naturally a vector space over the ring of C^n functions from N to 𝕜.
instance
ContMDiffMap.instSMul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
SMul (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 n) (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
C^n scalar-valued functions act by left-multiplication on C^n functions.
Equations
@[simp]
theorem
ContMDiffMap.smul_comp'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{N' : Type u_9}
[TopologicalSpace N']
[ChartedSpace H'' N']
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(f : ContMDiffMap I'' (modelWithCornersSelf 𝕜 𝕜) N' 𝕜 n)
(g : ContMDiffMap I'' (modelWithCornersSelf 𝕜 V) N' V n)
(h : ContMDiffMap I I'' N N' n)
:
The left multiplication with a C^n scalar function commutes with composition.
instance
ContMDiffMap.module'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H N]
{n : WithTop ℕ∞}
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
Module (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 n) (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
The space of C^n functions with values in a space V is a module over the space of C^n
functions with values in 𝕜.