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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_2} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [Add G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
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] :
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] :
@[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' โŠค) :
@[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] :
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] :
@[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] :
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] :
@[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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [TopologicalSpace G] [ChartedSpace H' G] :
Function.Injective fun f => โ†‘f
instance SmoothMap.addSemigroup {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [AddSemigroup G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] :
theorem SmoothMap.addSemigroup.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddSemigroup G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
โ†‘(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] :
theorem SmoothMap.addMonoid.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
โ†‘(f + g) = โ†‘f + โ†‘g
theorem SmoothMap.addMonoid.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [TopologicalSpace G] [ChartedSpace H' G] :
Function.Injective fun f => โ†‘f
instance SmoothMap.addMonoid {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] :
theorem SmoothMap.addMonoid.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] :
โ†‘0 = 0
instance SmoothMap.monoid {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothMul I' G] :
theorem SmoothMap.coeFnAddMonoidHom.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] :
โ†‘0 = 0
def SmoothMap.coeFnAddMonoidHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] :
ContMDiffMap I I' N G โŠค โ†’+ N โ†’ G

Coercion to a function as an AddMonoidHom. Similar to AddMonoidHom.coeFn.

Instances For
    theorem SmoothMap.coeFnAddMonoidHom.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
    โ†‘(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 โŠค โ†’* N โ†’ G

    Coercion to a function as a MonoidHom. Similar to MonoidHom.coeFn.

    Instances For
      theorem SmoothMap.compLeftAddMonoidHom.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_1) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_5} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_3} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_8} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothAdd I' G'] {G'' : Type u_2} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [SmoothAdd I'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ†‘ฯ†) :
      (fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }) 0 = 0
      def SmoothMap.compLeftAddMonoidHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_6) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_7} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_8} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_10} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothAdd I' G'] {G'' : Type u_11} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [SmoothAdd I'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ†‘ฯ†) :

      For a manifold N and a smooth homomorphism ฯ† between additive Lie groups G', G'', the 'left-composition-by-ฯ†' group homomorphism from C^โˆžโŸฎI, N; I', G'โŸฏ to C^โˆžโŸฎI, N; I'', G''โŸฏ.

      Instances For
        theorem SmoothMap.compLeftAddMonoidHom.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_4) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_3} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_2} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_8} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] {G'' : Type u_1} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ†‘ฯ†) (f : ContMDiffMap I I' N G' โŠค) (x : N) :
        ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x
        theorem SmoothMap.compLeftAddMonoidHom.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_2) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_1} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothAdd I' G'] {G'' : Type u_8} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [SmoothAdd I'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ†‘ฯ†) (f : ContMDiffMap I I' N G' โŠค) (g : ContMDiffMap I I' N G' โŠค) :
        ZeroHom.toFun { toFun := fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }, map_zero' := (_ : (fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }) 0 = 0) } (f + g) = ZeroHom.toFun { toFun := fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }, map_zero' := (_ : (fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }) 0 = 0) } f + ZeroHom.toFun { toFun := fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }, map_zero' := (_ : (fun f => { val := โ†‘ฯ† โˆ˜ โ†‘f, property := (_ : โˆ€ (x : N), ContMDiffAt I I'' โŠค (โ†‘ฯ† โˆ˜ โ†‘f) x) }) 0 = 0) } g
        def SmoothMap.compLeftMonoidHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_6) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_7} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_8} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_10} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothMul I' G'] {G'' : Type u_11} [Monoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [SmoothMul I'' G''] (ฯ† : G' โ†’* G'') (hฯ† : Smooth I' I'' โ†‘ฯ†) :

        For a manifold N and a smooth homomorphism ฯ† between Lie groups G', G'', the 'left-composition-by-ฯ†' group homomorphism from C^โˆžโŸฎI, N; I', G'โŸฏ to C^โˆžโŸฎI, N; I'', G''โŸฏ.

        Instances For
          theorem SmoothMap.restrictAddMonoidHom.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_3} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_1) [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
          โˆ€ (x x_1 : ContMDiffMap I I' { x // x โˆˆ V } G โŠค), ZeroHom.toFun { toFun := fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }, map_zero' := (_ : (fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }) 0 = (fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }) 0) } (x + x_1) = ZeroHom.toFun { toFun := fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }, map_zero' := (_ : (fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }) 0 = (fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }) 0) } (x + x_1)
          theorem SmoothMap.restrictAddMonoidHom.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_2} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_1) [TopologicalSpace G] [ChartedSpace H' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) (f : ContMDiffMap I I' { x // x โˆˆ V } G โŠค) :
          Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)
          def SmoothMap.restrictAddMonoidHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_10) [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
          ContMDiffMap I I' { x // x โˆˆ V } G โŠค โ†’+ ContMDiffMap I I' { x // x โˆˆ U } G โŠค

          For an additive Lie group G and open sets U โŠ† V in N, the 'restriction' group homomorphism from C^โˆžโŸฎI, V; I', GโŸฏ to C^โˆžโŸฎI, U; I', GโŸฏ.

          Instances For
            theorem SmoothMap.restrictAddMonoidHom.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_3} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_1) [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
            (fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }) 0 = (fun f => { val := โ†‘f โˆ˜ Set.inclusion h, property := (_ : Smooth I I' (โ†‘f โˆ˜ Set.inclusion h)) }) 0
            def SmoothMap.restrictMonoidHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_10) [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothMul I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
            ContMDiffMap I I' { x // x โˆˆ V } G โŠค โ†’* ContMDiffMap I I' { x // x โˆˆ U } G โŠค

            For a Lie group G and open sets U โŠ† V in N, the 'restriction' group homomorphism from C^โˆžโŸฎI, V; I', GโŸฏ to C^โˆžโŸฎI, U; I', GโŸฏ.

            Instances For
              theorem SmoothMap.addCommMonoid.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] :
              โ†‘0 = 0
              theorem SmoothMap.addCommMonoid.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [TopologicalSpace G] [ChartedSpace H' G] :
              Function.Injective fun f => โ†‘f
              theorem SmoothMap.addCommMonoid.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
              โ†‘(f + g) = โ†‘f + โ†‘g
              instance SmoothMap.addCommMonoid {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] :
              theorem SmoothMap.addCommMonoid.proof_4 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (n : โ„•) :
              โ†‘(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] :
              theorem SmoothMap.addGroup.proof_5 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_2} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) :
              Smooth I I' fun x => -โ†‘f x
              theorem SmoothMap.addGroup.proof_9 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
              โ†‘(f + g) = โ†‘f + โ†‘g
              theorem SmoothMap.addGroup.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (x : ContMDiffMap I I' N G โŠค) :
              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] :
              theorem SmoothMap.addGroup.proof_12 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              โˆ€ (a : ContMDiffMap I I' N G โŠค), zsmulRec 0 a = zsmulRec 0 a
              theorem SmoothMap.addGroup.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) :
              a + 0 = a
              theorem SmoothMap.addGroup.proof_8 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] :
              โ†‘0 = 0
              theorem SmoothMap.addGroup.proof_15 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) :
              -a + a = 0
              theorem SmoothMap.addGroup.proof_14 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              โˆ€ (n : โ„•) (a : ContMDiffMap I I' N G โŠค), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
              theorem SmoothMap.addGroup.proof_6 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_2} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
              Smooth I I' (โ†‘f - โ†‘g)
              theorem SmoothMap.addGroup.proof_7 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
              f - g = f + -g
              theorem SmoothMap.addGroup.proof_4 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (n : โ„•) (x : ContMDiffMap I I' N G โŠค) :
              theorem SmoothMap.addGroup.proof_13 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              โˆ€ (n : โ„•) (a : ContMDiffMap I I' N G โŠค), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a
              theorem SmoothMap.addGroup.proof_10 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) (b : ContMDiffMap I I' N G โŠค) (c : ContMDiffMap I I' N G โŠค) :
              a + b + c = a + (b + c)
              theorem SmoothMap.addGroup.proof_11 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_2} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) :
              Smooth I I' fun x => -โ†‘f x
              theorem SmoothMap.addGroup.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) :
              0 + a = 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] :
              @[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
              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] :
              theorem SmoothMap.addCommGroup.proof_1 {๐•œ : Type u_4} [NontriviallyNormedField ๐•œ] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              theorem SmoothMap.addCommGroup.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) (b : ContMDiffMap I I' N G โŠค) :
              a + b = b + a
              theorem SmoothMap.addCommGroup.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) :
              -a + a = 0
              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] :

              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] :
              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] :
              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] :
              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'' โ†‘ฯ†) :

              For a manifold N and a smooth homomorphism ฯ† between smooth rings R', R'', the 'left-composition-by-ฯ†' ring homomorphism from C^โˆžโŸฎI, N; I', R'โŸฏ to C^โˆžโŸฎI, N; I'', R''โŸฏ.

              Instances For
                def SmoothMap.restrictRingHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] (R : Type u_10) [Ring R] [TopologicalSpace R] [ChartedSpace H' R] [SmoothRing I' R] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
                ContMDiffMap I I' { x // x โˆˆ V } R โŠค โ†’+* ContMDiffMap I I' { x // x โˆˆ U } R โŠค

                For a "smooth ring" R and open sets U โŠ† V in N, the "restriction" ring homomorphism from C^โˆžโŸฎI, V; I', RโŸฏ to C^โˆžโŸฎI, U; I', RโŸฏ.

                Instances For
                  @[simp]
                  theorem SmoothMap.coeFnRingHom_apply {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {R : Type u_10} [CommRing R] [TopologicalSpace R] [ChartedSpace H' R] [SmoothRing I' R] :
                  โˆ€ (a : ContMDiffMap I I' N R โŠค) (a_1 : N), โ†‘SmoothMap.coeFnRingHom a a_1 = โ†‘a a_1
                  def SmoothMap.coeFnRingHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {R : Type u_10} [CommRing R] [TopologicalSpace R] [ChartedSpace H' R] [SmoothRing I' R] :
                  ContMDiffMap I I' N R โŠค โ†’+* N โ†’ R

                  Coercion to a function as a RingHom.

                  Instances For
                    def SmoothMap.evalRingHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {R : Type u_10} [CommRing R] [TopologicalSpace R] [ChartedSpace H' R] [SmoothRing I' R] (n : N) :

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

                    Instances For

                      Semimodule stucture #

                      In this section we show that smooth functions valued in a vector space M over a normed field ๐•œ inherit a vector space structure.

                      instance SmoothMap.instSMul {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] :
                      SMul ๐•œ (ContMDiffMap I (modelWithCornersSelf ๐•œ V) N V โŠค)
                      @[simp]
                      theorem SmoothMap.coe_smul {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] (r : ๐•œ) (f : ContMDiffMap I (modelWithCornersSelf ๐•œ V) N V โŠค) :
                      โ†‘(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' โŠค) :
                      instance SmoothMap.module {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] :
                      Module ๐•œ (ContMDiffMap I (modelWithCornersSelf ๐•œ V) N V โŠค)
                      @[simp]
                      theorem SmoothMap.coeFnLinearMap_apply {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] :
                      โˆ€ (a : ContMDiffMap I (modelWithCornersSelf ๐•œ V) N V โŠค) (a_1 : N), โ†‘SmoothMap.coeFnLinearMap a a_1 = โ†‘a a_1
                      def SmoothMap.coeFnLinearMap {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] :
                      ContMDiffMap I (modelWithCornersSelf ๐•œ V) N V โŠค โ†’โ‚—[๐•œ] N โ†’ V

                      Coercion to a function as a LinearMap.

                      Instances For

                        Algebra structure #

                        In this section we show that smooth functions valued in a normed algebra A over a normed field ๐•œ inherit an algebra structure.

                        def SmoothMap.C {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                        ๐•œ โ†’+* ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค

                        Smooth constant functions as a RingHom.

                        Instances For
                          instance SmoothMap.algebra {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                          Algebra ๐•œ (ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค)
                          @[simp]
                          theorem SmoothMap.coeFnAlgHom_apply {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                          โˆ€ (a : ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค) (a_1 : N), โ†‘SmoothMap.coeFnAlgHom a a_1 = โ†‘a a_1
                          def SmoothMap.coeFnAlgHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                          ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค โ†’โ‚[๐•œ] N โ†’ A

                          Coercion to a function as an AlgHom.

                          Instances For

                            Structure as module over scalar functions #

                            If V is a module over ๐•œ, then we show that the space of smooth functions from N to V is naturally a vector space over the ring of smooth functions from N to ๐•œ.

                            instance SmoothMap.instSMul' {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] :
                            SMul (ContMDiffMap I (modelWithCornersSelf ๐•œ ๐•œ) N ๐•œ โŠค) (ContMDiffMap I (modelWithCornersSelf ๐•œ V) N V โŠค)
                            @[simp]
                            theorem SmoothMap.smul_comp' {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_7} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_8} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {N' : Type u_9} [TopologicalSpace N'] [ChartedSpace H'' N'] {V : Type u_10} [NormedAddCommGroup V] [NormedSpace ๐•œ V] (f : ContMDiffMap I'' (modelWithCornersSelf ๐•œ ๐•œ) N' ๐•œ โŠค) (g : ContMDiffMap I'' (modelWithCornersSelf ๐•œ V) N' V โŠค) (h : ContMDiffMap I I'' N N' โŠค) :
                            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 โŠค)