Documentation

Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

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 ) :
Smooth I I' (f + 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 ) :
(f + g) = f + 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 ) :
(f * g) = f * 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' ) :
(f + g).comp h = f.comp h + g.comp 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' ) :
(f * g).comp h = f.comp h * g.comp 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
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
@[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] :
Equations
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
@[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 : ) :
(n f) = n f
@[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 : ) :
(f ^ n) = f ^ 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] :
Equations
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 ) :
(f + g) = f + 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] :
Equations
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 ) :
(f + g) = f + 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] :
Equations
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] :
Equations
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 →+ NG

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 ) :
    (f + g) = f + 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 →* NG

    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
      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
        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
          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
            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] :
              Equations
              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 ) :
              (f + g) = f + 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 : ) :
              (n f) = n f
              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] :
              Equations
              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 ) :
              Smooth I I' (f - 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 ) :
              f - g = f + -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] :
              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 ) :
              Smooth I I' fun (x : N) => -f x
              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 ) :
              -a + a = 0
              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 ) :
              Smooth I I' fun (x : N) => -f x
              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] :
              ∀ (n : ) (a : ContMDiffMap I I' N G ), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
              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] :
              Equations
              • SmoothMap.group = let __src := SmoothMap.monoid; Group.mk
              @[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 ) :
              (-f) = -f
              @[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 ) :
              f⁻¹ = (f)⁻¹
              @[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 ) :
              (f - g) = f - 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 ) :
              (f / g) = f / 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 ) :
              a + b = b + a
              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] :
              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] :
              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] :
              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] :
              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 )
              Equations
              • SmoothMap.ring = let __src := SmoothMap.semiring; let __src_1 := SmoothMap.addCommGroup; Ring.mk SubNegMonoid.zsmul
              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] :
              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 →+* NR

                  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) :

                    Function.eval as a RingHom on the ring of smooth functions.

                    Equations
                    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] :
                      Equations
                      @[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 ) :
                      (r f) = r f
                      @[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' ) :
                      (r g).comp h = r g.comp 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] :
                      Equations
                      @[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 →ₗ[𝕜] NV

                      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] :

                        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] :
                          Equations
                          @[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 →ₐ[𝕜] NA

                          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] :
                            Equations
                            @[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' ) :
                            (f g).comp h = f.comp h g.comp 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] :
                            Equations