Theory of topological monoids #
In this file we define mixin classes
has_continuous_add. While in many
applications the underlying type is a monoid (multiplicative or additive), we do not require this in
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
add_monoid M and
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
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
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.
Construct a bundled additive monoid homomorphism from a pointwise limit of additive monoid homomorphisms
The (topological-space) closure of a submonoid of a space
itself a submonoid.
The (topological-space) closure of an additive submonoid of a space
has_continuous_add is itself an additive submonoid.
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,
because the predicate
has_continuous_inv has not yet been defined.