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 ⊤)
Equations
- SmoothMap.instZero = { zero := ContMDiffMap.const 0 }
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 ⊤)
Equations
- SmoothMap.instOne = { one := ContMDiffMap.const 1 }
@[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 : ContMDiffMap I I' N G ⊤) => ⇑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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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 : ContMDiffMap I I' N G ⊤) => ⇑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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
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.
Equations
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 : ContMDiffMap I I' N G' ⊤) => { 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''⟯.
Equations
- One or more equations did not get rendered due to their size.
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' ⊤)
:
{
toFun := fun (f : ContMDiffMap I I' N G' ⊤) =>
{ val := ⇑φ ∘ ⇑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (⇑φ ∘ ⇑f) x) },
map_zero' :=
(_ :
(fun (f : ContMDiffMap I I' N G' ⊤) =>
{ val := ⇑φ ∘ ⇑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (⇑φ ∘ ⇑f) x) })
0 = 0) }.toFun
(f + g) = {
toFun := fun (f : ContMDiffMap I I' N G' ⊤) =>
{ val := ⇑φ ∘ ⇑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (⇑φ ∘ ⇑f) x) },
map_zero' :=
(_ :
(fun (f : ContMDiffMap I I' N G' ⊤) =>
{ val := ⇑φ ∘ ⇑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (⇑φ ∘ ⇑f) x) })
0 = 0) }.toFun
f + {
toFun := fun (f : ContMDiffMap I I' N G' ⊤) =>
{ val := ⇑φ ∘ ⇑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (⇑φ ∘ ⇑f) x) },
map_zero' :=
(_ :
(fun (f : ContMDiffMap I I' N G' ⊤) =>
{ val := ⇑φ ∘ ⇑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (⇑φ ∘ ⇑f) x) })
0 = 0) }.toFun
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''⟯.
Equations
- One or more equations did not get rendered due to their size.
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' (↥V) G ⊤),
{
toFun := fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) },
map_zero' :=
(_ :
(fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) })
0 = (fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) })
0) }.toFun
(x + x_1) = {
toFun := fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) },
map_zero' :=
(_ :
(fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) })
0 = (fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) })
0) }.toFun
(x + x_1)
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 : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) })
0 = (fun (f : ContMDiffMap I I' (↥V) G ⊤) =>
{ val := ⇑f ∘ Set.inclusion h, property := (_ : Smooth I I' (⇑f ∘ Set.inclusion h)) })
0
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' (↥V) G ⊤ →+ ContMDiffMap I I' (↥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⟯.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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' (↥V) G ⊤)
:
Smooth I I' (⇑f ∘ Set.inclusion h)
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' (↥V) G ⊤ →* ContMDiffMap I I' (↥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⟯.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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 ⊤)
:
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 : ContMDiffMap I I' N G ⊤) => ⇑f
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
theorem
SmoothMap.addGroup.proof_5
{𝕜 : 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_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_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]
(f : ContMDiffMap I I' N G ⊤)
(g : ContMDiffMap I I' N G ⊤)
:
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 ⊤)
Equations
- SmoothMap.addGroup = let src := SmoothMap.addMonoid; AddGroup.mk (_ : ∀ (a : ContMDiffMap I I' N G ⊤), -a + a = 0)
theorem
SmoothMap.addGroup.proof_4
{𝕜 : 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_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]
[LieAddGroup I' G]
(a : 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_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_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]
:
∀ (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_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]
:
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 ⊤)
:
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 ⊤)
(b : 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 ⊤)
Equations
- SmoothMap.addCommGroup = let src := SmoothMap.addGroup; let src_1 := SmoothMap.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : ContMDiffMap I I' N G ⊤), a + b = b + a)
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
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 ⊤)
Equations
- SmoothMap.commGroup = let src := SmoothMap.group; let src_1 := SmoothMap.commMonoid; CommGroup.mk (_ : ∀ (a b : ContMDiffMap I I' N G ⊤), a * b = b * a)
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
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 ⊤)
Equations
- SmoothMap.commRing = let src := SmoothMap.semiring; let src_1 := SmoothMap.addCommGroup; let src_2 := SmoothMap.commMonoid; CommRing.mk (_ : ∀ (a b : ContMDiffMap I I' N R ⊤), a * b = b * a)
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''⟯.
Equations
- One or more equations did not get rendered due to their size.
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' (↥V) R ⊤ →+* ContMDiffMap I I' (↥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⟯.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- SmoothMap.evalRingHom n = RingHom.comp (Pi.evalRingHom (fun (a : N) => R) n) SmoothMap.coeFnRingHom
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
@[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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- One or more equations did not get rendered due to their size.
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 ⊤)
Equations
- One or more equations did not get rendered due to their size.
@[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 ⊤)
Equations
- One or more equations did not get rendered due to their size.