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.
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 Ξ±
.
- compatible : β {e e' : PartialHomeomorph G H}, e β atlas H G β e' β atlas H G β e.symm.trans e' β contDiffGroupoid (ββ€) I
Instances
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
.
- compatible : β {e e' : PartialHomeomorph G H}, e β atlas H G β e' β atlas H G β e.symm.trans e' β contDiffGroupoid (ββ€) I
Instances
Alias of contMDiff_mul
.
Alias of contMDiff_add
.
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].
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].
Alias of ContMDiffWithinAt.mul
.
Alias of ContMDiffAt.mul
.
Alias of ContMDiffOn.mul
.
Alias of ContMDiff.mul
.
Alias of ContMDiffWithinAt.add
.
Alias of ContMDiffAt.add
.
Alias of ContMDiffOn.add
.
Alias of ContMDiff.add
.
Alias of contMDiff_mul_left
.
Alias of contMDiff_add_left
.
Alias of contMDiff_mul_right
.
Alias of contMDiff_add_right
.
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.
Equations
- smoothLeftMul I g = β¨leftMul g, β―β©
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.
Equations
- smoothRightMul I g = β¨rightMul g, β―β©
Instances For
Equations
- LieGroup.Β«termπ³Β» = Lean.ParserDescr.node `LieGroup.Β«termπ³Β» 1024 (Lean.ParserDescr.symbol "π³")
Instances For
Equations
- LieGroup.Β«termπΉΒ» = Lean.ParserDescr.node `LieGroup.Β«termπΉΒ» 1024 (Lean.ParserDescr.symbol "πΉ")
Instances For
Equations
- β― = β―
Equations
- β― = β―
Alias of contMDiff_pow
.
Alias of contMDiff_nsmul
.
Morphism of additive smooth monoids.
- toFun : G β G'
Instances For
Morphism of smooth monoids.
- toFun : G β G'
Instances For
Equations
- instOneSmoothMonoidMorphism = { one := { toMonoidHom := 1, smooth_toFun := β― } }
Equations
- instZeroSmoothAddMonoidMorphism = { zero := { toAddMonoidHom := 0, smooth_toFun := β― } }
Equations
- instInhabitedSmoothMonoidMorphism = { default := 1 }
Equations
- instInhabitedSmoothAddMonoidMorphism = { default := 0 }
Equations
- instFunLikeSmoothMonoidMorphism = { coe := fun (a : SmoothMonoidMorphism I I' G G') => (βa.toMonoidHom).toFun, coe_injective' := β― }
Equations
- instFunLikeSmoothAddMonoidMorphism = { coe := fun (a : SmoothAddMonoidMorphism I I' G G') => (βa.toAddMonoidHom).toFun, coe_injective' := β― }
Equations
- β― = β―
Equations
- β― = β―
Equations
- β― = β―
Equations
- β― = β―
Differentiability of finite point-wise sums and products #
Finite point-wise products (resp. sums) of differentiable/smooth functions M β G
(at x
/on s
)
into a commutative monoid G
are differentiable/smooth at x
/on s
.
Alias of contMDiffAt_finprod
.
Alias of contMDiffAt_finsum
.
Alias of contMDiffWithinAt_finset_prod'
.
Alias of contMDiffWithinAt_finset_sum'
.
Alias of contMDiffWithinAt_finset_prod
.
Alias of contMDiffWithinAt_finset_sum
.
Alias of contMDiffAt_finset_prod'
.
Alias of contMDiffAt_finset_sum'
.
Alias of contMDiffAt_finset_prod
.
Alias of contMDiffAt_finset_sum
.
Alias of contMDiffOn_finset_prod'
.
Alias of contMDiffOn_finset_sum'
.
Alias of contMDiffOn_finset_prod
.
Alias of contMDiffOn_finset_sum
.
Alias of contMDiffOn_finset_prod'
.
Alias of contMDiffOn_finset_sum'
.
Alias of contMDiff_finset_prod
.
Alias of contMDiff_finset_sum
.
Alias of contMDiff_finprod
.
Alias of contMDiff_finsum
.
Alias of contMDiff_finprod_cond
.
Alias of contMDiff_finsum_cond
.
Equations
- β― = β―
Alias of ContMDiffWithinAt.div_const
.
Alias of ContMDiffAt.div_const
.
Alias of ContMDiffOn.div_const
.
Alias of ContMDiff.div_const
.