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: has_smooth_mul
and its
additive counterpart has_smooth_add
. These structures are general enough to also talk about smooth
semigroups.
-
All smooth algebraic structures on
G
areProp
-valued classes that extendsmooth_manifold_with_corners I G
. This way we save users from adding both[smooth_manifold_with_corners I G]
and[has_smooth_mul I G]
to the assumptions. While many API lemmas hold true without thesmooth_manifold_with_corners I G
assumption, we're not aware of a mathematically interesting monoid on a topological manifold such that (a) the space is not asmooth_manifold_with_corners
; (b) the multiplication is smooth at(a, b)
in the chartsext_chart_at I a
,ext_chart_at I b
,ext_chart_at I (a * b)
. -
Because of
model_prod
we can't assume, e.g., that alie_group
is modelled on𝓘(𝕜, E)
. So, we formulate the definitions and lemmas for any model. -
While smoothness of an operation implies its continuity, lemmas like
has_continuous_mul_of_smooth
can't be instances becausen otherwise Lean would have to search forhas_smooth_mul I G
with unknown𝕜
,E
,H
, andI : model_with_corners 𝕜 E H
. If users needs[has_continuous_mul G]
in a proof about a smooth monoid, then they need to either add[has_continuous_mul G]
as an assumption (worse) or usehaveI
in the proof (better).
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- smooth_add : smooth (I.prod I) I (λ (p : G × G), 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 add_monoid α
and has_smooth_add α
.
Instances of this typeclass
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- smooth_mul : smooth (I.prod I) I (λ (p : G × G), 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 has_smooth_mul I G
.
Instances of this typeclass
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 smooth_left_mul
with the notation 𝑳
usually use L
instead of 𝑳
in the
names.
Equations
- smooth_left_mul I g = {to_fun := left_mul g, cont_mdiff_to_fun := _}
Right multiplication by g
. It is meant to mimic the usual notation in Lie groups.
Lemmas involving smooth_right_mul
with the notation 𝑹
usually use R
instead of 𝑹
in the
names.
Equations
- smooth_right_mul I g = {to_fun := right_mul g, cont_mdiff_to_fun := _}
- to_add_monoid_hom : G →+ G'
- smooth_to_fun : smooth I I' self.to_add_monoid_hom.to_fun
Morphism of additive smooth monoids.
Instances for smooth_add_monoid_morphism
- smooth_add_monoid_morphism.has_sizeof_inst
- smooth_add_monoid_morphism.has_zero
- smooth_add_monoid_morphism.inhabited
- smooth_add_monoid_morphism.has_coe_to_fun
- to_monoid_hom : G →* G'
- smooth_to_fun : smooth I I' self.to_monoid_hom.to_fun
Morphism of smooth monoids.
Instances for smooth_monoid_morphism
- smooth_monoid_morphism.has_sizeof_inst
- smooth_monoid_morphism.has_one
- smooth_monoid_morphism.inhabited
- smooth_monoid_morphism.has_coe_to_fun
Equations
- smooth_add_monoid_morphism.has_zero = {zero := {to_add_monoid_hom := 0, smooth_to_fun := _}}
Equations
- smooth_monoid_morphism.has_one = {one := {to_monoid_hom := 1, smooth_to_fun := _}}
Equations
Equations
Equations
- smooth_add_monoid_morphism.has_coe_to_fun = {coe := λ (a : smooth_add_monoid_morphism I I' G G'), a.to_add_monoid_hom.to_fun}
Equations
- smooth_monoid_morphism.has_coe_to_fun = {coe := λ (a : smooth_monoid_morphism I I' G G'), a.to_monoid_hom.to_fun}