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
- has_continuous_add_of_discrete_topology
- topological_add_group.to_has_continuous_add
- topological_ring.to_has_continuous_add
- has_lipschitz_add.has_continuous_add
- prod.has_continuous_add
- pi.has_continuous_add
- pi.has_continuous_add'
- add_submonoid.has_continuous_add
- add_submonoid.topological_closure_has_continuous_add
- additive.has_continuous_add
- order_dual.has_continuous_add
- ennreal.has_continuous_add
- weak_dual.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
- has_continuous_mul_of_discrete_topology
- topological_group.to_has_continuous_mul
- linear_ordered_field.has_continuous_mul
- topological_ring.to_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'
- submonoid.has_continuous_mul
- submonoid.topological_closure_has_continuous_mul
- mul_opposite.has_continuous_mul
- units.has_continuous_mul
- multiplicative.has_continuous_mul
- order_dual.has_continuous_mul
- topological_ring.top_monoid_units
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.
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
.
Put the same topological space structure on the opposite monoid as on the original space.
If multiplication is continuous in the monoid α
, then it also is in the monoid αᵐᵒᵖ
.
The units of a monoid are equipped with a topology, via the embedding into α × α
.
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.