Smooth monoid #
A smooth monoid is a monoid that is also a smooth manifold, in which multiplication is a smooth map
of the product manifold G
Γ G
into G
.
In this file we define the basic structures to talk about smooth monoids: SmoothMul
and its
additive counterpart SmoothAdd
. These structures are general enough to also talk about smooth
semigroups.
- compatible : β {e e' : LocalHomeomorph G H}, e β atlas H G β e' β atlas H G β LocalHomeomorph.trans (LocalHomeomorph.symm e) e' β contDiffGroupoid β€ I
- smooth_add : Smooth (ModelWithCorners.prod I I) I fun p => p.fst + p.snd
Basic hypothesis to talk about a smooth (Lie) additive monoid or a smooth additive
semigroup. A smooth additive monoid over Ξ±
, for example, is obtained by requiring both the
instances AddMonoid Ξ±
and SmoothAdd Ξ±
.
Instances
- compatible : β {e e' : LocalHomeomorph G H}, e β atlas H G β e' β atlas H G β LocalHomeomorph.trans (LocalHomeomorph.symm e) e' β contDiffGroupoid β€ I
- smooth_mul : Smooth (ModelWithCorners.prod I I) I fun p => p.fst * p.snd
Basic hypothesis to talk about a smooth (Lie) monoid or a smooth semigroup.
A smooth monoid over G
, for example, is obtained by requiring both the instances Monoid G
and SmoothMul I G
.
Instances
If the addition is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
If the multiplication is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
Left multiplication by g
. It is meant to mimic the usual notation in Lie groups.
Lemmas involving smoothLeftMul
with the notation π³
usually use L
instead of π³
in the
names.
Instances For
Right multiplication by g
. It is meant to mimic the usual notation in Lie groups.
Lemmas involving smoothRightMul
with the notation πΉ
usually use R
instead of πΉ
in the
names.
Instances For
- toFun : G β G'
- map_zero' : ZeroHom.toFun (βs.toAddMonoidHom) 0 = 0
- map_add' : β (x y : G), ZeroHom.toFun (βs.toAddMonoidHom) (x + y) = ZeroHom.toFun (βs.toAddMonoidHom) x + ZeroHom.toFun (βs.toAddMonoidHom) y
- smooth_toFun : Smooth I I' s.toFun
Morphism of additive smooth monoids.
Instances For
- toFun : G β G'
- map_one' : OneHom.toFun (βs.toMonoidHom) 1 = 1
- map_mul' : β (x y : G), OneHom.toFun (βs.toMonoidHom) (x * y) = OneHom.toFun (βs.toMonoidHom) x * OneHom.toFun (βs.toMonoidHom) y
- smooth_toFun : Smooth I I' s.toFun
Morphism of smooth monoids.