# Continuous monoid action #

In this file we define class `ContinuousSMul`

. We say `ContinuousSMul M X`

if `M`

acts on `X`

and
the map `(c, x) ↦ c • x`

is continuous on `M × X`

. We reuse this class for topological
(semi)modules, vector spaces and algebras.

## Main definitions #

`ContinuousSMul M X`

: typeclass saying that the map`(c, x) ↦ c • x`

is continuous on`M × X`

;`Units.continuousSMul`

: scalar multiplication by`Mˣ`

is continuous when scalar multiplication by`M`

is continuous. This allows`Homeomorph.smul`

to be used with on monoids with`G = Mˣ`

.

-- Porting note: These have all moved

`Homeomorph.smul_of_ne_zero`

: if a group with zero`G₀`

(e.g., a field) acts on`X`

and`c : G₀`

is a nonzero element of`G₀`

, then scalar multiplication by`c`

is a homeomorphism of`X`

;`Homeomorph.smul`

: scalar multiplication by an element of a group`G`

acting on`X`

is a homeomorphism of`X`

.

## Main results #

Besides homeomorphisms mentioned above, in this file we provide lemmas like `Continuous.smul`

or `Filter.Tendsto.smul`

that provide dot-syntax access to `ContinuousSMul`

.

Class `ContinuousSMul M X`

says that the scalar multiplication `(•) : M → X → X`

is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.

- continuous_smul : Continuous fun (p : M × X) => p.1 • p.2
The scalar multiplication

`(•)`

is continuous.

## Instances

The scalar multiplication `(•)`

is continuous.

Class `ContinuousVAdd M X`

says that the additive action `(+ᵥ) : M → X → X`

is continuous in both arguments. We use the same class for all kinds of additive actions,
including (semi)modules and algebras.

- continuous_vadd : Continuous fun (p : M × X) => p.1 +ᵥ p.2
The additive action

`(+ᵥ)`

is continuous.

## Instances

The additive action `(+ᵥ)`

is continuous.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

If an additive action is central, then its right action is continuous when its left action is.

## Equations

- ⋯ = ⋯

If a scalar action is central, then its right action is continuous when its left action is.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

Suppose that `N`

additively acts on `X`

and `M`

continuously additively acts on `Y`

.
Suppose that `g : Y → X`

is an additive action homomorphism in the following sense:
there exists a continuous function `f : N → M`

such that `g (c +ᵥ x) = f c +ᵥ g x`

.
Then the action of `N`

on `X`

is continuous as well.

In many cases, `f = id`

so that `g`

is an action homomorphism in the sense of `AddActionHom`

.
However, this version also works for `f = AddUnits.val`

.

Suppose that `N`

acts on `X`

and `M`

continuously acts on `Y`

.
Suppose that `g : Y → X`

is an action homomorphism in the following sense:
there exists a continuous function `f : N → M`

such that `g (c • x) = f c • g x`

.
Then the action of `N`

on `X`

is continuous as well.

In many cases, `f = id`

so that `g`

is an action homomorphism in the sense of `MulActionHom`

.
However, this version also works for semilinear maps and `f = Units.val`

.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

If an action is continuous, then composing this action with a continuous homomorphism gives again a continuous action.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

An `AddTorsor`

for a connected space is a connected space. This is not an instance because
it loops for a group as a torsor over itself.