Algebraic structures over smooth functions #
In this file, we define instances of algebraic structures over smooth functions.
Group structure #
In this section we show that smooth functions valued in a Lie group inherit a group structure under pointwise multiplication.
Coercion to a function as an AddMonoidHom
.
Similar to AddMonoidHom.coeFn
.
Instances For
Coercion to a function as a MonoidHom
. Similar to MonoidHom.coeFn
.
Instances For
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
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
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
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
Ring stucture #
In this section we show that smooth functions valued in a smooth ring R
inherit a ring structure
under pointwise multiplication.
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
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
Coercion to a function as a RingHom
.
Instances For
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.
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.
Smooth constant functions as a RingHom
.
Instances For
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 𝕜
.