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

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

Equations
  • SmoothMap.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := โ‹ฏ, map_add' := โ‹ฏ }
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.

    Equations
    • SmoothMap.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := โ‹ฏ, map_mul' := โ‹ฏ }
    Instances For
      theorem SmoothMap.compLeftAddMonoidHom.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_1) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_5} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_3} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_8} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothAdd I' G'] {G'' : Type u_2} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [SmoothAdd I'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ‡‘ฯ†) :
      (fun (f : ContMDiffMap I I' N G' โŠค) => โŸจโ‡‘ฯ† โˆ˜ โ‡‘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'' โ‡‘ฯ†) :

      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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_4) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_3} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_2} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_8} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] {G'' : Type u_1} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ‡‘ฯ†) (f : ContMDiffMap I I' N G' โŠค) (x : N) :
        ContMDiffAt I I'' โŠค (โ‡‘ฯ† โˆ˜ โ‡‘f) x
        theorem SmoothMap.compLeftAddMonoidHom.proof_3 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} (N : Type u_2) [TopologicalSpace N] [ChartedSpace H N] {E'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {G' : Type u_1} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothAdd I' G'] {G'' : Type u_8} [AddMonoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [SmoothAdd I'' G''] (ฯ† : G' โ†’+ G'') (hฯ† : Smooth I' I'' โ‡‘ฯ†) (f : ContMDiffMap I I' N G' โŠค) (g : ContMDiffMap I I' N G' โŠค) :
        { toFun := fun (f : ContMDiffMap I I' N G' โŠค) => โŸจโ‡‘ฯ† โˆ˜ โ‡‘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'' โ‡‘ฯ†) :

        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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_3} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_1) [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
          โˆ€ (x x_1 : ContMDiffMap I I' (โ†ฅV) G โŠค), { toFun := fun (f : ContMDiffMap I I' (โ†ฅV) G โŠค) => โŸจโ‡‘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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_3} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_1) [AddMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
          (fun (f : ContMDiffMap I I' (โ†ฅV) G โŠค) => โŸจโ‡‘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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_2} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_1) [TopologicalSpace G] [ChartedSpace H' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) (f : ContMDiffMap I I' (โ†ฅV) G โŠค) :
            Smooth I I' (โ‡‘f โˆ˜ Set.inclusion h)
            def SmoothMap.restrictMonoidHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] (G : Type u_10) [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothMul I' G] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
            ContMDiffMap I I' (โ†ฅV) G โŠค โ†’* ContMDiffMap I I' (โ†ฅU) G โŠค

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

            Equations
            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_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
              theorem SmoothMap.addCommMonoid.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] :
              โ‡‘0 = 0
              theorem SmoothMap.addCommMonoid.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [TopologicalSpace G] [ChartedSpace H' G] :
              Function.Injective fun (f : ContMDiffMap I I' N G โŠค) => โ‡‘f
              theorem SmoothMap.addCommMonoid.proof_4 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothAdd I' G] (f : ContMDiffMap I I' N G โŠค) (n : โ„•) :
              โ‡‘(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_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              โˆ€ (a : ContMDiffMap I I' N G โŠค), zsmulRec 0 a = zsmulRec 0 a
              theorem SmoothMap.addGroup.proof_2 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_2} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) (g : ContMDiffMap I I' N G โŠค) :
              Smooth I I' (โ‡‘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] (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_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 : N) => -f x
              theorem SmoothMap.addGroup.proof_8 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (a : ContMDiffMap I I' N G โŠค) :
              -a + a = 0
              theorem SmoothMap.addGroup.proof_1 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_2} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] (f : ContMDiffMap I I' N G โŠค) :
              Smooth I I' fun (x : N) => -f x
              theorem SmoothMap.addGroup.proof_7 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              โˆ€ (n : โ„•) (a : ContMDiffMap I I' N G โŠค), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
              theorem SmoothMap.addGroup.proof_6 {๐•œ : Type u_7} [NontriviallyNormedField ๐•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ChartedSpace H' G] [LieAddGroup I' G] :
              โˆ€ (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_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
              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_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] :
              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] :
              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'' โ‡‘ฯ†) :

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def SmoothMap.restrictRingHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] (R : Type u_10) [Ring R] [TopologicalSpace R] [ChartedSpace H' R] [SmoothRing I' R] {U : TopologicalSpace.Opens N} {V : TopologicalSpace.Opens N} (h : U โ‰ค V) :
                ContMDiffMap I I' (โ†ฅV) R โŠค โ†’+* ContMDiffMap I I' (โ†ฅU) R โŠค

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

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

                  Coercion to a function as a RingHom.

                  Equations
                  • SmoothMap.coeFnRingHom = let __src := SmoothMap.coeFnMonoidHom; let __src := SmoothMap.coeFnAddMonoidHom; { toFun := DFunLike.coe, map_one' := โ‹ฏ, map_mul' := โ‹ฏ, map_zero' := โ‹ฏ, map_add' := โ‹ฏ }
                  Instances For
                    def SmoothMap.evalRingHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {R : Type u_10} [CommRing R] [TopologicalSpace R] [ChartedSpace H' R] [SmoothRing I' R] (n : N) :

                    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] :
                      SMul ๐•œ (ContMDiffMap I (modelWithCornersSelf ๐•œ V) N 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] :
                      Module ๐•œ (ContMDiffMap I (modelWithCornersSelf ๐•œ V) N 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 โŠค โ†’โ‚—[๐•œ] N โ†’ V

                      Coercion to a function as a LinearMap.

                      Equations
                      • SmoothMap.coeFnLinearMap = let __src := SmoothMap.coeFnAddMonoidHom; { toFun := DFunLike.coe, map_add' := โ‹ฏ, map_smul' := โ‹ฏ }
                      Instances For

                        Algebra structure #

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

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

                        Smooth constant functions as a RingHom.

                        Equations
                        • SmoothMap.C = { toFun := fun (c : ๐•œ) => โŸจfun (x : N) => (algebraMap ๐•œ A) c, โ‹ฏโŸฉ, map_one' := โ‹ฏ, map_mul' := โ‹ฏ, map_zero' := โ‹ฏ, map_add' := โ‹ฏ }
                        Instances For
                          instance SmoothMap.algebra {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                          Algebra ๐•œ (ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค)
                          Equations
                          • SmoothMap.algebra = Algebra.mk SmoothMap.C โ‹ฏ โ‹ฏ
                          @[simp]
                          theorem SmoothMap.coeFnAlgHom_apply {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                          โˆ€ (a : ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค) (a_1 : N), SmoothMap.coeFnAlgHom a a_1 = a a_1
                          def SmoothMap.coeFnAlgHom {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {A : Type u_10} [NormedRing A] [NormedAlgebra ๐•œ A] [SmoothRing (modelWithCornersSelf ๐•œ A) A] :
                          ContMDiffMap I (modelWithCornersSelf ๐•œ A) N A โŠค โ†’โ‚[๐•œ] N โ†’ A

                          Coercion to a function as an AlgHom.

                          Equations
                          • SmoothMap.coeFnAlgHom = { toFun := DFunLike.coe, map_one' := โ‹ฏ, map_mul' := โ‹ฏ, map_zero' := โ‹ฏ, map_add' := โ‹ฏ, commutes' := โ‹ฏ }
                          Instances For

                            Structure as module over scalar functions #

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

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