Scalar actions on discrete spaces #
Any scalar action of a discrete space on a discrete space is jointly continuous. This supplies the continuity hypothesis for discrete coefficient modules without requiring algebraic laws on the scalar action.
Main results #
TauCeti.continuousSMul_of_discreteTopology: scalar actions between discrete spaces are continuous.
@[instance 100]
instance
TauCeti.continuousSMul_of_discreteTopology
{R : Type u_1}
{M : Type u_2}
[TopologicalSpace R]
[TopologicalSpace M]
[DiscreteTopology R]
[DiscreteTopology M]
[SMul R M]
:
ContinuousSMul R M
A scalar action between discrete spaces is jointly continuous, since the product of the scalar space and the acted-on space is discrete.