Theory of topological monoids #
In this file we define mixin classes ContinuousMul
and ContinuousAdd
. While in many
applications the underlying type is a monoid (multiplicative or additive), we do not require this in
the definitions.
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 AddMonoid M
and ContinuousAdd M
.
Continuity in only the left/right argument can be stated using
ContinuousConstVAdd α α
/ContinuousConstVAdd αᵐᵒᵖ α
.
- continuous_add : Continuous fun (p : M × M) => p.1 + p.2
Instances
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 ContinuousMul M
.
Continuity in only the left/right argument can be stated using
ContinuousConstSMul α α
/ContinuousConstSMul αᵐᵒᵖ α
.
- continuous_mul : Continuous fun (p : M × M) => p.1 * p.2
Instances
Construct a unit from limits of units and their inverses.
Equations
- h₁.units h₂ = { val := r₁, inv := r₂, val_inv := ⋯, inv_val := ⋯ }
Instances For
Construct an additive unit from limits of additive units and their negatives.
Equations
- h₁.addUnits h₂ = { val := r₁, neg := r₂, val_neg := ⋯, neg_val := ⋯ }
Instances For
A version of Pi.continuousMul
for non-dependent functions. It is needed because sometimes
Lean 3 fails to use Pi.continuousMul
for non-dependent functions.
A version of Pi.continuousAdd
for non-dependent functions. It is needed
because sometimes Lean fails to use Pi.continuousAdd
for non-dependent functions.
Construct a bundled semigroup 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 MulHomClass
instance) to M₁ → M₂
.
Equations
- mulHomOfMemClosureRangeCoe f hf = { toFun := f, map_mul' := ⋯ }
Instances For
Construct a bundled additive semigroup 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 an AddHomClass
instance) to M₁ → M₂
.
Equations
- addHomOfMemClosureRangeCoe f hf = { toFun := f, map_add' := ⋯ }
Instances For
Construct a bundled semigroup homomorphism from a pointwise limit of semigroup homomorphisms.
Equations
- mulHomOfTendsto f g h = mulHomOfMemClosureRangeCoe f ⋯
Instances For
Construct a bundled additive semigroup homomorphism from a pointwise limit of additive semigroup homomorphisms
Equations
- addHomOfTendsto f g h = addHomOfMemClosureRangeCoe f ⋯
Instances For
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 MonoidHomClass
instance) to M₁ → M₂
.
Equations
- monoidHomOfMemClosureRangeCoe f hf = { toFun := f, map_one' := ⋯, map_mul' := ⋯ }
Instances For
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 an AddMonoidHomClass
instance) to M₁ → M₂
.
Equations
- addMonoidHomOfMemClosureRangeCoe f hf = { toFun := f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms.
Equations
- monoidHomOfTendsto f g h = monoidHomOfMemClosureRangeCoe f ⋯
Instances For
Construct a bundled additive monoid homomorphism from a pointwise limit of additive monoid homomorphisms
Equations
Instances For
Alias of Topology.IsInducing.continuousMul
.
Given a neighborhood U
of 1
there is an open neighborhood V
of 1
such that V * V ⊆ U
.
Given an open neighborhood U
of 0
there is an open neighborhood V
of 0
such that V + V ⊆ U
.
The (topological-space) closure of a subsemigroup of a space M
with ContinuousMul
is
itself a subsemigroup.
Instances For
The (topological-space) closure of an additive submonoid of a space M
with
ContinuousAdd
is itself an additive submonoid.
Instances For
If a subsemigroup of a topological semigroup is commutative, then so is its topological closure.
See note [reducible non-instances]
Equations
- s.commSemigroupTopologicalClosure hs = CommSemigroup.mk ⋯
Instances For
If a submonoid of an additive topological monoid is commutative, then so is its topological closure.
See note [reducible non-instances]
Equations
- s.addCommSemigroupTopologicalClosure hs = AddCommSemigroup.mk ⋯
Instances For
The (topological-space) closure of a submonoid of a space M
with ContinuousMul
is
itself a submonoid.
Instances For
The (topological-space) closure of an additive submonoid of a space M
with
ContinuousAdd
is itself an additive submonoid.
Instances For
If a submonoid of a topological monoid is commutative, then so is its topological closure.
Equations
- s.commMonoidTopologicalClosure hs = CommMonoid.mk ⋯
Instances For
If a submonoid of an additive topological monoid is commutative, then so is its topological closure.
See note [reducible non-instances].
Equations
- s.addCommMonoidTopologicalClosure hs = AddCommMonoid.mk ⋯
Instances For
Left-multiplication by a left-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.
Right-multiplication by a right-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.
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 R
acts on A
via A
, then continuous addition implies
continuous affine addition by constants.
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 the action of R
on A
commutes with left-addition, then
continuous addition implies continuous affine addition 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 ContinuousInv
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 ContinuousNeg
has not yet been defined.
The continuous map fun y => y * x
Equations
- ContinuousMap.mulRight x = { toFun := fun (b : X) => b * x, continuous_toFun := ⋯ }
Instances For
The continuous map fun y => y + x
Equations
- ContinuousMap.addRight x = { toFun := fun (b : X) => b + x, continuous_toFun := ⋯ }
Instances For
The continuous map fun y => x * y
Equations
- ContinuousMap.mulLeft x = { toFun := fun (b : X) => x * b, continuous_toFun := ⋯ }
Instances For
The continuous map fun y => x + y
Equations
- ContinuousMap.addLeft x = { toFun := fun (b : X) => x + b, continuous_toFun := ⋯ }