Continuous monoid action #
In this file we define class
has_continuous_smul. We say
has_continuous_smul M α if
M acts on
α and the map
(c, x) ↦ c • x is continuous on
M × α. We reuse this class for topological
(semi)modules, vector spaces and algebras.
Main definitions #
has_continuous_smul M α: typeclass saying that the map
(c, x) ↦ c • xis continuous on
M × α;
homeomorph.smul_of_ne_zero: if a group with zero
G₀(e.g., a field) acts on
c : G₀is a nonzero element of
G₀, then scalar multiplication by
cis a homeomorphism of
homeomorph.smul: scalar multiplication by an element of a group
αis a homeomorphism of
units.has_continuous_smul: scalar multiplication by
units Mis continuous when scalar multiplication by
Mis continuous. This allows
homeomorph.smulto be used with on monoids with
G = units M.
Main results #
has_continuous_smul M α says that the scalar multiplication
(•) : M → α → α
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.
Scalar multiplication by a unit of a monoid
M acting on
α is a homeomorphism from
Scalar multiplication by a non-zero element of a group with zero acting on
α is a
α onto itself.
smul is a closed map in the second argument.
The lemma that
smul is a closed map in the first argument (for a normed space over a complete
normed field) is