Algebraic structures over smooth functions #
In this file, we define instances of algebraic structures over smooth functions.
theorem
SmoothMap.instAdd.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_2}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
instance
SmoothMap.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]
{G : Type u_10}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
Add (ContMDiffMap I I' N G ⊤)
instance
SmoothMap.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]
{G : Type u_10}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
Mul (ContMDiffMap I I' N G ⊤)
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
@[simp]
theorem
SmoothMap.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']
{G : Type u_10}
[Add G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I'' I' N' G ⊤)
(g : ContMDiffMap I'' I' N' G ⊤)
(h : ContMDiffMap I I'' N N' ⊤)
:
ContMDiffMap.comp (f + g) h = ContMDiffMap.comp f h + ContMDiffMap.comp g h
@[simp]
theorem
SmoothMap.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']
{G : Type u_10}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
(f : ContMDiffMap I'' I' N' G ⊤)
(g : ContMDiffMap I'' I' N' G ⊤)
(h : ContMDiffMap I I'' N N' ⊤)
:
ContMDiffMap.comp (f * g) h = ContMDiffMap.comp f h * ContMDiffMap.comp g h
instance
SmoothMap.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]
{G : Type u_10}
[Zero G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
Zero (ContMDiffMap I I' N G ⊤)
instance
SmoothMap.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]
{G : Type u_10}
[One G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
One (ContMDiffMap I I' N G ⊤)
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Zero G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
↑0 = 0
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[One G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
↑1 = 1
instance
SmoothMap.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]
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
SMul ℕ (ContMDiffMap I I' N G ⊤)
instance
SmoothMap.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]
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
Pow (ContMDiffMap I I' N G ⊤) ℕ
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(n : ℕ)
:
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
(f : ContMDiffMap I I' N G ⊤)
(n : ℕ)
:
Group structure #
In this section we show that smooth functions valued in a Lie group inherit a group structure under pointwise multiplication.
theorem
SmoothMap.addSemigroup.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[TopologicalSpace G]
[ChartedSpace H' G]
:
Function.Injective fun f => ↑f
instance
SmoothMap.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]
{G : Type u_10}
[AddSemigroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
AddSemigroup (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addSemigroup.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddSemigroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
instance
SmoothMap.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]
{G : Type u_10}
[Semigroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
Semigroup (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addMonoid.proof_3
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addMonoid.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[TopologicalSpace G]
[ChartedSpace H' G]
:
Function.Injective fun f => ↑f
instance
SmoothMap.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]
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
AddMonoid (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addMonoid.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
↑0 = 0
instance
SmoothMap.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]
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
Monoid (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.coeFnAddMonoidHom.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
↑0 = 0
def
SmoothMap.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]
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
ContMDiffMap I I' N G ⊤ →+ N → G
Coercion to a function as an AddMonoidHom.
Similar to AddMonoidHom.coeFn.
Instances For
theorem
SmoothMap.coeFnAddMonoidHom.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
∀ (a : ContMDiffMap I I' N G ⊤) (a_1 : N), ↑SmoothMap.coeFnAddMonoidHom a a_1 = ↑a a_1
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
∀ (a : ContMDiffMap I I' N G ⊤) (a_1 : N), ↑SmoothMap.coeFnMonoidHom a a_1 = ↑a a_1
def
SmoothMap.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]
{G : Type u_10}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
ContMDiffMap I I' N G ⊤ →* N → G
Coercion to a function as a MonoidHom. Similar to MonoidHom.coeFn.
Instances For
theorem
SmoothMap.compLeftAddMonoidHom.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_10}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_9}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_1)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_5}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_3}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G' : Type u_8}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
{G'' : Type u_2}
[AddMonoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[SmoothAdd I'' G'']
(φ : G' →+ G'')
(hφ : Smooth I' I'' ↑φ)
:
(fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 0 = 0
def
SmoothMap.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''}
{G' : Type u_10}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
{G'' : Type u_11}
[AddMonoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[SmoothAdd I'' G'']
(φ : G' →+ G'')
(hφ : Smooth I' I'' ↑φ)
:
ContMDiffMap I I' N G' ⊤ →+ ContMDiffMap I I'' N G'' ⊤
For a manifold N and a smooth homomorphism φ between additive Lie groups G',
G'', the 'left-composition-by-φ' group homomorphism from C^∞⟮I, N; I', G'⟯ to
C^∞⟮I, N; I'', G''⟯.
Instances For
theorem
SmoothMap.compLeftAddMonoidHom.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_10}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_9}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_4)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_3}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_2}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G' : Type u_8}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
{G'' : Type u_1}
[AddMonoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
(φ : G' →+ G'')
(hφ : Smooth I' I'' ↑φ)
(f : ContMDiffMap I I' N G' ⊤)
(x : N)
:
ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x
theorem
SmoothMap.compLeftAddMonoidHom.proof_3
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_2)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_10}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G' : Type u_1}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
{G'' : Type u_8}
[AddMonoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[SmoothAdd I'' G'']
(φ : G' →+ G'')
(hφ : Smooth I' I'' ↑φ)
(f : ContMDiffMap I I' N G' ⊤)
(g : ContMDiffMap I I' N G' ⊤)
:
ZeroHom.toFun
{ toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
map_zero' :=
(_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 0 = 0) }
(f + g) = ZeroHom.toFun
{ toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
map_zero' :=
(_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 0 = 0) }
f + ZeroHom.toFun
{ toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
map_zero' :=
(_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 0 = 0) }
g
def
SmoothMap.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''}
{G' : Type u_10}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothMul I' G']
{G'' : Type u_11}
[Monoid G'']
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[SmoothMul I'' G'']
(φ : G' →* G'')
(hφ : Smooth I' I'' ↑φ)
:
ContMDiffMap I I' N G' ⊤ →* ContMDiffMap I I'' N G'' ⊤
For a manifold N and a smooth homomorphism φ between Lie groups G', G'', the
'left-composition-by-φ' group homomorphism from C^∞⟮I, N; I', G'⟯ to C^∞⟮I, N; I'', G''⟯.
Instances For
theorem
SmoothMap.restrictAddMonoidHom.proof_3
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_3}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
(G : Type u_1)
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
{U : TopologicalSpace.Opens N}
{V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
∀ (x x_1 : ContMDiffMap I I' { x // x ∈ V } G ⊤),
ZeroHom.toFun
{ toFun := fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) },
map_zero' :=
(_ :
(fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) }) 0 = (fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) }) 0) }
(x + x_1) = ZeroHom.toFun
{ toFun := fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) },
map_zero' :=
(_ :
(fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) }) 0 = (fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) }) 0) }
(x + x_1)
theorem
SmoothMap.restrictAddMonoidHom.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_2}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
(G : Type u_1)
[TopologicalSpace G]
[ChartedSpace H' G]
{U : TopologicalSpace.Opens N}
{V : TopologicalSpace.Opens N}
(h : U ≤ V)
(f : ContMDiffMap I I' { x // x ∈ V } G ⊤)
:
Smooth I I' (↑f ∘ Set.inclusion h)
def
SmoothMap.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]
(G : Type u_10)
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
{U : TopologicalSpace.Opens N}
{V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
ContMDiffMap I I' { x // x ∈ V } G ⊤ →+ ContMDiffMap I I' { x // x ∈ U } G ⊤
For an additive Lie group G and open sets U ⊆ V in N, the 'restriction' group
homomorphism from C^∞⟮I, V; I', G⟯ to C^∞⟮I, U; I', G⟯.
Instances For
theorem
SmoothMap.restrictAddMonoidHom.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_3}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
(G : Type u_1)
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
{U : TopologicalSpace.Opens N}
{V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
(fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) }) 0 = (fun f => { val := ↑f ∘ Set.inclusion h, property := (_ : Smooth I I' (↑f ∘ Set.inclusion h)) }) 0
def
SmoothMap.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]
(G : Type u_10)
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
{U : TopologicalSpace.Opens N}
{V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
ContMDiffMap I I' { x // x ∈ V } G ⊤ →* ContMDiffMap I I' { x // x ∈ U } G ⊤
For a Lie group G and open sets U ⊆ V in N, the 'restriction' group homomorphism from
C^∞⟮I, V; I', G⟯ to C^∞⟮I, U; I', G⟯.
Instances For
theorem
SmoothMap.addCommMonoid.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
↑0 = 0
theorem
SmoothMap.addCommMonoid.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[TopologicalSpace G]
[ChartedSpace H' G]
:
Function.Injective fun f => ↑f
theorem
SmoothMap.addCommMonoid.proof_3
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
instance
SmoothMap.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]
{G : Type u_10}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
:
AddCommMonoid (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addCommMonoid.proof_4
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothAdd I' G]
(f : ContMDiffMap I I' N G ⊤)
(n : ℕ)
:
instance
SmoothMap.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]
{G : Type u_10}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H' G]
[SmoothMul I' G]
:
CommMonoid (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addGroup.proof_5
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_2}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_9
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_3
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(x : ContMDiffMap I I' N G ⊤)
:
AddMonoid.nsmul 0 x = 0
instance
SmoothMap.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]
{G : Type u_10}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
:
AddGroup (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addGroup.proof_12
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
:
∀ (a : ContMDiffMap I I' N G ⊤), zsmulRec 0 a = zsmulRec 0 a
theorem
SmoothMap.addGroup.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_8
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
:
↑0 = 0
theorem
SmoothMap.addGroup.proof_15
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_14
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
:
∀ (n : ℕ) (a : ContMDiffMap I I' N G ⊤), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
theorem
SmoothMap.addGroup.proof_6
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_2}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_7
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_4
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(n : ℕ)
(x : ContMDiffMap I I' N G ⊤)
:
AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
theorem
SmoothMap.addGroup.proof_13
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
:
theorem
SmoothMap.addGroup.proof_10
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
(b : ContMDiffMap I I' N G ⊤)
(c : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_11
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_2}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_1
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
:
instance
SmoothMap.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]
{G : Type u_10}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' G]
:
Group (ContMDiffMap I I' N G ⊤)
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
:
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
:
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
@[simp]
theorem
SmoothMap.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]
{G : Type u_10}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
instance
SmoothMap.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]
{G : Type u_10}
[AddCommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
:
AddCommGroup (ContMDiffMap I I' N G ⊤)
theorem
SmoothMap.addCommGroup.proof_1
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_1}
[AddCommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
:
SmoothAdd I' G
theorem
SmoothMap.addCommGroup.proof_3
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddCommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
(b : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addCommGroup.proof_2
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_3}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_2}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_1}
[AddCommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
:
instance
SmoothMap.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]
{G : Type u_10}
[CommGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I' G]
:
CommGroup (ContMDiffMap I I' N G ⊤)
Ring stucture #
In this section we show that smooth functions valued in a smooth ring R inherit a ring structure
under pointwise multiplication.
instance
SmoothMap.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]
{R : Type u_10}
[Semiring R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
:
Semiring (ContMDiffMap I I' N R ⊤)
instance
SmoothMap.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]
{R : Type u_10}
[Ring R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
:
Ring (ContMDiffMap I I' N R ⊤)
instance
SmoothMap.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]
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
:
CommRing (ContMDiffMap I I' N R ⊤)
def
SmoothMap.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''}
{R' : Type u_10}
[Ring R']
[TopologicalSpace R']
[ChartedSpace H' R']
[SmoothRing I' R']
{R'' : Type u_11}
[Ring R'']
[TopologicalSpace R'']
[ChartedSpace H'' R'']
[SmoothRing I'' R'']
(φ : R' →+* R'')
(hφ : Smooth I' I'' ↑φ)
:
ContMDiffMap I I' N R' ⊤ →+* ContMDiffMap I I'' N R'' ⊤
For a manifold N and a smooth homomorphism φ between smooth rings R', R'', the
'left-composition-by-φ' ring homomorphism from C^∞⟮I, N; I', R'⟯ to C^∞⟮I, N; I'', R''⟯.
Instances For
def
SmoothMap.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]
(R : Type u_10)
[Ring R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
{U : TopologicalSpace.Opens N}
{V : TopologicalSpace.Opens N}
(h : U ≤ V)
:
ContMDiffMap I I' { x // x ∈ V } R ⊤ →+* ContMDiffMap I I' { x // x ∈ U } R ⊤
For a "smooth ring" R and open sets U ⊆ V in N, the "restriction" ring homomorphism from
C^∞⟮I, V; I', R⟯ to C^∞⟮I, U; I', R⟯.
Instances For
@[simp]
theorem
SmoothMap.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]
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
:
∀ (a : ContMDiffMap I I' N R ⊤) (a_1 : N), ↑SmoothMap.coeFnRingHom a a_1 = ↑a a_1
def
SmoothMap.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]
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
:
ContMDiffMap I I' N R ⊤ →+* N → R
Coercion to a function as a RingHom.
Instances For
def
SmoothMap.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]
{R : Type u_10}
[CommRing R]
[TopologicalSpace R]
[ChartedSpace H' R]
[SmoothRing I' R]
(n : N)
:
ContMDiffMap I I' N R ⊤ →+* R
Function.eval as a RingHom on the ring of smooth functions.
Instances For
Semimodule stucture #
In this section we show that smooth functions valued in a vector space M over a normed
field 𝕜 inherit a vector space structure.
instance
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
SMul 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤)
@[simp]
theorem
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(r : 𝕜)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤)
:
@[simp]
theorem
SmoothMap.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']
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(r : 𝕜)
(g : ContMDiffMap I'' (modelWithCornersSelf 𝕜 V) N' V ⊤)
(h : ContMDiffMap I I'' N N' ⊤)
:
ContMDiffMap.comp (r • g) h = r • ContMDiffMap.comp g h
instance
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
Module 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤)
@[simp]
theorem
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
∀ (a : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤) (a_1 : N), ↑SmoothMap.coeFnLinearMap a a_1 = ↑a a_1
def
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤ →ₗ[𝕜] N → V
Coercion to a function as a LinearMap.
Instances For
Algebra structure #
In this section we show that smooth functions valued in a normed algebra A over a normed field 𝕜
inherit an algebra structure.
def
SmoothMap.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]
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[SmoothRing (modelWithCornersSelf 𝕜 A) A]
:
𝕜 →+* ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A ⊤
Smooth constant functions as a RingHom.
Instances For
instance
SmoothMap.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]
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[SmoothRing (modelWithCornersSelf 𝕜 A) A]
:
Algebra 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A ⊤)
@[simp]
theorem
SmoothMap.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]
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[SmoothRing (modelWithCornersSelf 𝕜 A) A]
:
∀ (a : ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A ⊤) (a_1 : N), ↑SmoothMap.coeFnAlgHom a a_1 = ↑a a_1
def
SmoothMap.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]
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[SmoothRing (modelWithCornersSelf 𝕜 A) A]
:
ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A ⊤ →ₐ[𝕜] N → A
Coercion to a function as an AlgHom.
Instances For
Structure as module over scalar functions #
If V is a module over 𝕜, then we show that the space of smooth functions from N to V
is naturally a vector space over the ring of smooth functions from N to 𝕜.
instance
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
SMul (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 ⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤)
@[simp]
theorem
SmoothMap.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']
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(f : ContMDiffMap I'' (modelWithCornersSelf 𝕜 𝕜) N' 𝕜 ⊤)
(g : ContMDiffMap I'' (modelWithCornersSelf 𝕜 V) N' V ⊤)
(h : ContMDiffMap I I'' N N' ⊤)
:
ContMDiffMap.comp (f • g) h = ContMDiffMap.comp f h • ContMDiffMap.comp g h
instance
SmoothMap.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]
{V : Type u_10}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
Module (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 ⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤)