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
- ContMDiffMap.instMul = { mul := fun (f g : ContMDiffMap I I' N G n) => ⟨⇑f * ⇑g, ⋯⟩ }
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
- ContMDiffMap.instAdd = { add := fun (f g : ContMDiffMap I I' N G n) => ⟨⇑f + ⇑g, ⋯⟩ }
@[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
- ContMDiffMap.instOne = { one := ContMDiffMap.const 1 }
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
- ContMDiffMap.instZero = { zero := ContMDiffMap.const 0 }
@[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
- ContMDiffMap.instNSMul = { smul := fun (n_1 : ℕ) (f : ContMDiffMap I I' N G n) => ⟨n_1 • ⇑f, ⋯⟩ }
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
- ContMDiffMap.instPow = { pow := fun (f : ContMDiffMap I I' N G n) (n_1 : ℕ) => ⟨⇑f ^ n_1, ⋯⟩ }
@[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
- ContMDiffMap.semigroup = Function.Injective.semigroup (fun (f : ContMDiffMap I I' N G n) => ⇑f) ⋯ ⋯
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
- ContMDiffMap.addSemigroup = Function.Injective.addSemigroup (fun (f : ContMDiffMap I I' N G n) => ⇑f) ⋯ ⋯
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
- ContMDiffMap.monoid = Function.Injective.monoid (fun (f : ContMDiffMap I I' N G n) => ⇑f) ⋯ ⋯ ⋯ ⋯
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
- ContMDiffMap.addMonoid = Function.Injective.addMonoid (fun (f : ContMDiffMap I I' N G n) => ⇑f) ⋯ ⋯ ⋯ ⋯
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
- ContMDiffMap.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }
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
- ContMDiffMap.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
@[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)
:
@[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)
:
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
- ContMDiffMap.compLeftMonoidHom I N φ hφ = { toFun := fun (f : ContMDiffMap I I' N G' n) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
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
- ContMDiffMap.compLeftAddMonoidHom I N φ hφ = { toFun := fun (f : ContMDiffMap I I' N G' n) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
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
- ContMDiffMap.restrictMonoidHom I I' G h = { toFun := fun (f : ContMDiffMap I I' (↥V) G n) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
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
- ContMDiffMap.restrictAddMonoidHom I I' G h = { toFun := fun (f : ContMDiffMap I I' (↥V) G n) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
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
- ContMDiffMap.commMonoid = Function.Injective.commMonoid (fun (f : ContMDiffMap I I' N G n) => ⇑f) ⋯ ⋯ ⋯ ⋯
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
- ContMDiffMap.addCommMonoid = Function.Injective.addCommMonoid (fun (f : ContMDiffMap I I' N G n) => ⇑f) ⋯ ⋯ ⋯ ⋯
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
@[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
- ContMDiffMap.commGroup = { toGroup := ContMDiffMap.group, mul_comm := ⋯ }
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
- ContMDiffMap.addCommGroup = { toAddGroup := ContMDiffMap.addGroup, add_comm := ⋯ }
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- ContMDiffMap.compLeftRingHom I N φ hφ = { toFun := fun (f : ContMDiffMap I I' N R' n) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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
- ContMDiffMap.restrictRingHom I I' R h = { toFun := fun (f : ContMDiffMap I I' (↥V) R n) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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
- ContMDiffMap.coeFnRingHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
@[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
- ContMDiffMap.evalRingHom m = (Pi.evalRingHom (fun (a : N) => R) m).comp ContMDiffMap.coeFnRingHom
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
- ContMDiffMap.instSMul = { smul := fun (r : 𝕜) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n) => ⟨r • ⇑f, ⋯⟩ }
@[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)
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
- ContMDiffMap.coeFnLinearMap = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }
@[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
- ContMDiffMap.C = { toFun := fun (c : 𝕜) => ⟨fun (x : N) => (algebraMap 𝕜 A) c, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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
- ContMDiffMap.algebra = { smul := fun (r : 𝕜) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n) => ⟨r • ⇑f, ⋯⟩, algebraMap := ContMDiffMap.C, commutes' := ⋯, smul_def' := ⋯ }
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
- ContMDiffMap.coeFnAlgHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
@[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
- ContMDiffMap.instSMul' = { smul := fun (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 n) (g : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n) => ⟨fun (x : N) => f x • g x, ⋯⟩ }
@[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 𝕜.
Equations
- One or more equations did not get rendered due to their size.