Algebraic structures over smooth functions #
In this file, we define instances of algebraic structures over smooth functions.
theorem
SmoothMap.instAdd.proof_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_7}
[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 ⊤)
Equations
- SmoothMap.instAdd = { add := fun (f g : ContMDiffMap I I' N G ⊤) => ⟨⇑f + ⇑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 ⊤)
Equations
- SmoothMap.instMul = { mul := fun (f g : ContMDiffMap I I' N G ⊤) => ⟨⇑f * ⇑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' ⊤)
:
@[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' ⊤)
:
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 ⊤)
Equations
- SmoothMap.instNSMul = { smul := fun (n : ℕ) (f : ContMDiffMap I I' N G ⊤) => ⟨n • ⇑f, ⋯⟩ }
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 ⊤) ℕ
Equations
- SmoothMap.instPow = { pow := fun (f : ContMDiffMap I I' N G ⊤) (n : ℕ) => ⟨⇑f ^ n, ⋯⟩ }
@[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_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_7}
[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
- SmoothMap.addSemigroup = Function.Injective.addSemigroup (fun (f : ContMDiffMap I I' N G ⊤) => ⇑f) ⋯ ⋯
theorem
SmoothMap.addSemigroup.proof_2
{𝕜 : 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_7}
[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
- SmoothMap.semigroup = Function.Injective.semigroup (fun (f : ContMDiffMap I I' N G ⊤) => ⇑f) ⋯ ⋯
theorem
SmoothMap.addMonoid.proof_3
{𝕜 : 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_7}
[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_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_7}
[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
- SmoothMap.addMonoid = Function.Injective.addMonoid (fun (f : ContMDiffMap I I' N G ⊤) => ⇑f) ⋯ ⋯ ⋯ ⋯
theorem
SmoothMap.addMonoid.proof_2
{𝕜 : Type u_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_7}
[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
- SmoothMap.monoid = Function.Injective.monoid (fun (f : ContMDiffMap I I' N G ⊤) => ⇑f) ⋯ ⋯ ⋯ ⋯
theorem
SmoothMap.coeFnAddMonoidHom.proof_1
{𝕜 : Type u_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_7}
[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
- SmoothMap.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
SmoothMap.coeFnAddMonoidHom.proof_2
{𝕜 : 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_7}
[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
- SmoothMap.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }
Instances For
theorem
SmoothMap.compLeftAddMonoidHom.proof_2
{𝕜 : Type u_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_8}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[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_7}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G' : Type u_10}
[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' ⊤) => ⟨⇑φ ∘ ⇑f, ⋯⟩) 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
- SmoothMap.compLeftAddMonoidHom I N φ hφ = { toFun := fun (f : ContMDiffMap I I' N G' ⊤) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
SmoothMap.compLeftAddMonoidHom.proof_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_9}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_10}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(N : Type u_4)
[TopologicalSpace N]
[ChartedSpace H N]
{E'' : Type u_5}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_6}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G' : Type u_8}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
{G'' : Type u_7}
[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_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_9}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_10}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G' : Type u_7}
[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' ⊤) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_zero' := ⋯ }.toFun (f + g) = { toFun := fun (f : ContMDiffMap I I' N G' ⊤) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_zero' := ⋯ }.toFun f + { toFun := fun (f : ContMDiffMap I I' N G' ⊤) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_zero' := ⋯ }.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
- SmoothMap.compLeftMonoidHom I N φ hφ = { toFun := fun (f : ContMDiffMap I I' N G' ⊤) => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
theorem
SmoothMap.restrictAddMonoidHom.proof_3
{𝕜 : 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_7)
[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 ⊤) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := fun (f : ContMDiffMap I I' (↥V) G ⊤) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_zero' := ⋯ }.toFun (x + x_1)
theorem
SmoothMap.restrictAddMonoidHom.proof_2
{𝕜 : Type u_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_7}
[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 ⊤) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩) 0 = (fun (f : ContMDiffMap I I' (↥V) G ⊤) => ⟨⇑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
- SmoothMap.restrictAddMonoidHom I I' G h = { toFun := fun (f : ContMDiffMap I I' (↥V) G ⊤) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
SmoothMap.restrictAddMonoidHom.proof_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
(G : Type u_7)
[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
- SmoothMap.restrictMonoidHom I I' G h = { toFun := fun (f : ContMDiffMap I I' (↥V) G ⊤) => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
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
- SmoothMap.addCommMonoid = Function.Injective.addCommMonoid (fun (f : ContMDiffMap I I' N G ⊤) => ⇑f) ⋯ ⋯ ⋯ ⋯
theorem
SmoothMap.addCommMonoid.proof_3
{𝕜 : 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_7}
[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_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_7}
[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_3}
[NontriviallyNormedField 𝕜]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_7}
[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_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_7}
[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
- SmoothMap.commMonoid = Function.Injective.commMonoid (fun (f : ContMDiffMap I I' N G ⊤) => ⇑f) ⋯ ⋯ ⋯ ⋯
theorem
SmoothMap.addGroup.proof_5
{𝕜 : 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_7}
[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_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_7}
[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_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_7}
[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 ⋯
theorem
SmoothMap.addGroup.proof_4
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_7}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_8
{𝕜 : 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_7}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(a : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_4}
[TopologicalSpace N]
[ChartedSpace H N]
{G : Type u_7}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieAddGroup I' G]
(f : ContMDiffMap I I' N G ⊤)
:
theorem
SmoothMap.addGroup.proof_7
{𝕜 : 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_7}
[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_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_7}
[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_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_7}
[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 ⋯
theorem
SmoothMap.addCommGroup.proof_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_2}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_4}
[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 ⋯
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
- SmoothMap.semiring = let __src := SmoothMap.addCommMonoid; let __src_1 := SmoothMap.monoid; Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
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 ⋯
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
- SmoothMap.coeFnRingHom = let __src := SmoothMap.coeFnMonoidHom; let __src := SmoothMap.coeFnAddMonoidHom; { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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 = (Pi.evalRingHom (fun (a : N) => R) n).comp 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
- SmoothMap.instSMul = { smul := fun (r : 𝕜) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤) => ⟨r • ⇑f, ⋯⟩ }
@[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' ⊤)
:
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
- SmoothMap.module = Function.Injective.module 𝕜 SmoothMap.coeFnAddMonoidHom ⋯ ⋯
@[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
- SmoothMap.coeFnLinearMap = let __src := SmoothMap.coeFnAddMonoidHom; { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }
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
- SmoothMap.C = { toFun := fun (c : 𝕜) => ⟨fun (x : N) => (algebraMap 𝕜 A) c, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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
- SmoothMap.algebra = Algebra.mk SmoothMap.C ⋯ ⋯
@[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
- SmoothMap.coeFnAlgHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
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
- SmoothMap.instSMul' = { smul := fun (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 ⊤) (g : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V ⊤) => ⟨fun (x : N) => f x • g x, ⋯⟩ }
@[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' ⊤)
:
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 ⊤)