Theory of topological monoids #
In this file we define mixin classes has_continuous_mul
and has_continuous_add
. While in many
applications the underlying type is a monoid (multiplicative or additive), we do not require this in
the definitions.
- continuous_add : continuous (λ (p : M × M), p.fst + p.snd)
Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over M
, for example, is obtained by requiring both the
instances add_monoid M
and has_continuous_add M
.
Instances of this typeclass
- has_continuous_add_of_discrete_topology
- topological_add_group.to_has_continuous_add
- topological_semiring.to_has_continuous_add
- has_lipschitz_add.has_continuous_add
- prod.has_continuous_add
- pi.has_continuous_add
- pi.has_continuous_add'
- add_subsemigroup.has_continuous_add
- add_submonoid.has_continuous_add
- add_opposite.has_continuous_add
- add_units.has_continuous_add
- additive.has_continuous_add
- mul_opposite.has_continuous_add
- order_dual.has_continuous_add
- ennreal.has_continuous_add
- matrix.has_continuous_add
- continuous_map.has_continuous_add
- weak_bilin.has_continuous_add
- weak_dual.has_continuous_add
- weak_space.has_continuous_add
- continuous_mul : continuous (λ (p : M × M), p.fst * p.snd)
Basic hypothesis to talk about a topological monoid or a topological semigroup.
A topological monoid over M
, for example, is obtained by requiring both the instances monoid M
and has_continuous_mul M
.
Instances of this typeclass
- has_continuous_mul_of_discrete_topology
- topological_group.to_has_continuous_mul
- topological_semiring.to_has_continuous_mul
- linear_ordered_field.has_continuous_mul
- has_lipschitz_mul.has_continuous_mul
- semi_normed_ring_top_monoid
- linear_ordered_comm_group_with_zero.has_continuous_mul
- prod.has_continuous_mul
- pi.has_continuous_mul
- pi.has_continuous_mul'
- subsemigroup.has_continuous_mul
- submonoid.has_continuous_mul
- mul_opposite.has_continuous_mul
- units.has_continuous_mul
- multiplicative.has_continuous_mul
- add_opposite.has_continuous_mul
- topological_ring.top_monoid_units
- order_dual.has_continuous_mul
- matrix.has_continuous_mul
- continuous_map.has_continuous_mul
- metric.ball.has_continuous_mul
- metric.closed_ball.has_continuous_mul
Construct an additive unit from limits of additive units and their negatives.
Construct a unit from limits of units and their inverses.
A version of pi.has_continuous_mul
for non-dependent functions. It is needed because sometimes
Lean fails to use pi.has_continuous_mul
for non-dependent functions.
A version of pi.has_continuous_add
for non-dependent functions. It is needed
because sometimes Lean fails to use pi.has_continuous_add
for non-dependent functions.
Construct a bundled monoid homomorphism M₁ →* M₂
from a function f
and a proof that it
belongs to the closure of the range of the coercion from M₁ →* M₂
(or another type of bundled
homomorphisms that has a monoid_hom_class
instance) to M₁ → M₂
.
Construct a bundled additive monoid homomorphism M₁ →+ M₂
from a function f
and a proof that it belongs to the closure of the range of the coercion from M₁ →+ M₂
(or another
type of bundled homomorphisms that has a add_monoid_hom_class
instance) to M₁ → M₂
.
Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms.
Equations
Construct a bundled additive monoid homomorphism from a pointwise limit of additive monoid homomorphisms
Equations
The (topological-space) closure of a submonoid of a space M
with has_continuous_mul
is
itself a submonoid.
The (topological-space) closure of an additive submonoid of a space M
with
has_continuous_add
is itself an additive submonoid.
If a submonoid of a topological monoid is commutative, then so is its topological closure.
Equations
- s.comm_monoid_topological_closure hs = {mul := monoid.mul s.topological_closure.to_monoid, mul_assoc := _, one := monoid.one s.topological_closure.to_monoid, one_mul := _, mul_one := _, npow := monoid.npow s.topological_closure.to_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
If a submonoid of an additive topological monoid is commutative, then so is its topological closure.
Equations
- s.add_comm_monoid_topological_closure hs = {add := add_monoid.add s.topological_closure.to_add_monoid, add_assoc := _, zero := add_monoid.zero s.topological_closure.to_add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul s.topological_closure.to_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Given a open neighborhood U
of 0
there is a open neighborhood V
of 0
such that V + V ⊆ U
.
Given a neighborhood U
of 1
there is an open neighborhood V
of 1
such that VV ⊆ U
.
If R
acts on A
via A
, then continuous multiplication implies continuous scalar
multiplication by constants.
Notably, this instances applies when R = A
, or when [algebra R A]
is available.
If the action of R
on A
commutes with left-multiplication, then continuous multiplication
implies continuous scalar multiplication by constants.
Notably, this instances applies when R = Aᵐᵒᵖ
If multiplication is continuous in α
, then it also is in αᵐᵒᵖ
.
If addition is continuous in α
, then it also is in αᵃᵒᵖ
.
If multiplication on a monoid is continuous, then multiplication on the units of the monoid, with respect to the induced topology, is continuous.
Inversion is also continuous, but we register this in a later file, topology.algebra.group
,
because the predicate has_continuous_inv
has not yet been defined.
If addition on an additive monoid is continuous, then addition on the additive units of the monoid, with respect to the induced topology, is continuous.
Negation is also continuous, but we register this in a later file, topology.algebra.group
, because
the predicate has_continuous_neg
has not yet been defined.