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 : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : Prop

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.

class ContinuousVAdd (M : Type u_1) (X : Type u_2) [VAdd M X] [TopologicalSpace M] [TopologicalSpace X] : Prop

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.

instance instContinuousVAddULiftVaddLeftTopologicalSpace {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] : ContinuousVAdd (ULift.{u_5, u_1} M) X

Equations

• ⋯ = ⋯

instance instContinuousSMulULiftSmulLeftTopologicalSpace {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] : ContinuousSMul (ULift.{u_5, u_1} M) X

Equations

• ⋯ = ⋯

instance ContinuousVAdd.continuousConstVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] : ContinuousConstVAdd M X

Equations

• ⋯ = ⋯

instance ContinuousSMul.continuousConstSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] : ContinuousConstSMul M X

Equations

• ⋯ = ⋯

theorem Filter.Tendsto.vadd {M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X} (hf : Filter.Tendsto f l (nhds c)) (hg : Filter.Tendsto g l (nhds a)) : Filter.Tendsto (fun (x : α) => f x +ᵥ g x) l (nhds (c +ᵥ a))

theorem Filter.Tendsto.smul {M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X} (hf : Filter.Tendsto f l (nhds c)) (hg : Filter.Tendsto g l (nhds a)) : Filter.Tendsto (fun (x : α) => f x • g x) l (nhds (c • a))

theorem Filter.Tendsto.vadd_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {f : α → M} {l : Filter α} {c : M} (hf : Filter.Tendsto f l (nhds c)) (a : X) : Filter.Tendsto (fun (x : α) => f x +ᵥ a) l (nhds (c +ᵥ a))

theorem Filter.Tendsto.smul_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {f : α → M} {l : Filter α} {c : M} (hf : Filter.Tendsto f l (nhds c)) (a : X) : Filter.Tendsto (fun (x : α) => f x • a) l (nhds (c • a))

theorem ContinuousWithinAt.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {b : Y} {s : Set Y} (hf : ContinuousWithinAt f s b) (hg : ContinuousWithinAt g s b) : ContinuousWithinAt (fun (x : Y) => f x +ᵥ g x) s b

theorem ContinuousWithinAt.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y} {s : Set Y} (hf : ContinuousWithinAt f s b) (hg : ContinuousWithinAt g s b) : ContinuousWithinAt (fun (x : Y) => f x • g x) s b

theorem ContinuousAt.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {b : Y} (hf : ContinuousAt f b) (hg : ContinuousAt g b) : ContinuousAt (fun (x : Y) => f x +ᵥ g x) b

theorem ContinuousAt.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y} (hf : ContinuousAt f b) (hg : ContinuousAt g b) : ContinuousAt (fun (x : Y) => f x • g x) b

theorem ContinuousOn.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {s : Set Y} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : Y) => f x +ᵥ g x) s

theorem ContinuousOn.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {s : Set Y} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : Y) => f x • g x) s

theorem Continuous.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : Y) => f x +ᵥ g x

theorem Continuous.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : Y) => f x • g x

instance ContinuousVAdd.op {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] : ContinuousVAdd Mᵃᵒᵖ X

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

Equations

• ⋯ = ⋯

instance ContinuousSMul.op {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : ContinuousSMul Mᵐᵒᵖ X

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

Equations

• ⋯ = ⋯

instance AddOpposite.continuousVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] : ContinuousVAdd M Xᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.continuousSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] : ContinuousSMul M Xᵐᵒᵖ

Equations

• ⋯ = ⋯

theorem Specializes.vadd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {a : M} {b : M} {x : X} {y : X} (h₁ : a ⤳ b) (h₂ : x ⤳ y) : (a +ᵥ x) ⤳ (b +ᵥ y)

theorem Specializes.smul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {a : M} {b : M} {x : X} {y : X} (h₁ : a ⤳ b) (h₂ : x ⤳ y) : (a • x) ⤳ (b • y)

theorem Inseparable.vadd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {a : M} {b : M} {x : X} {y : X} (h₁ : Inseparable a b) (h₂ : Inseparable x y) : Inseparable (a +ᵥ x) (b +ᵥ y)

theorem Inseparable.smul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {a : M} {b : M} {x : X} {y : X} (h₁ : Inseparable a b) (h₂ : Inseparable x y) : Inseparable (a • x) (b • y)

theorem IsCompact.vadd_set {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {k : Set M} {u : Set X} (hk : IsCompact k) (hu : IsCompact u) : IsCompact (k +ᵥ u)

theorem IsCompact.smul_set {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {k : Set M} {u : Set X} (hk : IsCompact k) (hu : IsCompact u) : IsCompact (k • u)

theorem vadd_set_closure_subset {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] (K : Set M) (L : Set X) : closure K +ᵥ closure L ⊆ closure (K +ᵥ L)

theorem smul_set_closure_subset {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] (K : Set M) (L : Set X) : closure K • closure L ⊆ closure (K • L)

theorem Inducing.continuousVAdd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [VAdd M X] [ContinuousVAdd M X] {g : Y → X} {N : Type u_5} [VAdd N Y] [TopologicalSpace N] {f : N → M} (hg : Inducing g) (hf : Continuous f) (hsmul : ∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x) : ContinuousVAdd N Y

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.

theorem Inducing.continuousSMul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [SMul M X] [ContinuousSMul M X] {g : Y → X} {N : Type u_5} [SMul N Y] [TopologicalSpace N] {f : N → M} (hg : Inducing g) (hf : Continuous f) (hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x) : ContinuousSMul N Y

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.

instance VAddMemClass.continuousVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {S : Type u_5} [SetLike S X] [VAddMemClass S M X] (s : S) : ContinuousVAdd M ↥s

Equations

• ⋯ = ⋯

instance SMulMemClass.continuousSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {S : Type u_5} [SetLike S X] [SMulMemClass S M X] (s : S) : ContinuousSMul M ↥s

Equations

• ⋯ = ⋯

instance AddUnits.continuousVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [AddMonoid M] [AddAction M X] [ContinuousVAdd M X] : ContinuousVAdd (AddUnits M) X

Equations

• ⋯ = ⋯

instance Units.continuousSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [Monoid M] [MulAction M X] [ContinuousSMul M X] : ContinuousSMul Mˣ X

Equations

• ⋯ = ⋯

theorem AddAction.continuousVAdd_compHom {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [AddMonoid M] [AddAction M X] [ContinuousVAdd M X] {N : Type u_5} [TopologicalSpace N] [AddMonoid N] {f : N →+ M} (hf : Continuous ⇑f) : ContinuousVAdd N X

theorem MulAction.continuousSMul_compHom {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [Monoid M] [MulAction M X] [ContinuousSMul M X] {N : Type u_5} [TopologicalSpace N] [Monoid N] {f : N →* M} (hf : Continuous ⇑f) : ContinuousSMul N X

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

instance AddSubmonoid.continuousVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [AddMonoid M] [AddAction M X] [ContinuousVAdd M X] {S : AddSubmonoid M} : ContinuousVAdd (↥S) X

Equations

• ⋯ = ⋯

instance Submonoid.continuousSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [Monoid M] [MulAction M X] [ContinuousSMul M X] {S : Submonoid M} : ContinuousSMul (↥S) X

Equations

• ⋯ = ⋯

instance AddSubgroup.continuousVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [AddGroup M] [AddAction M X] [ContinuousVAdd M X] {S : AddSubgroup M} : ContinuousVAdd (↥S) X

Equations

• ⋯ = ⋯

instance Subgroup.continuousSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [Group M] [MulAction M X] [ContinuousSMul M X] {S : Subgroup M} : ContinuousSMul (↥S) X

Equations

• ⋯ = ⋯

instance Prod.continuousVAdd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [VAdd M X] [VAdd M Y] [ContinuousVAdd M X] [ContinuousVAdd M Y] : ContinuousVAdd M (X × Y)

Equations

• ⋯ = ⋯

instance Prod.continuousSMul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace M] [TopologicalSpace X] [TopologicalSpace Y] [SMul M X] [SMul M Y] [ContinuousSMul M X] [ContinuousSMul M Y] : ContinuousSMul M (X × Y)

Equations

• ⋯ = ⋯

instance instContinuousVAddForAllInstVAddTopologicalSpace {M : Type u_1} [TopologicalSpace M] {ι : Type u_5} {γ : ι → Type u_6} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousVAdd M (γ i)] : ContinuousVAdd M ((i : ι) → γ i)

Equations

• ⋯ = ⋯

instance instContinuousSMulForAllInstSMulTopologicalSpace {M : Type u_1} [TopologicalSpace M] {ι : Type u_5} {γ : ι → Type u_6} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → SMul M (γ i)] [∀ (i : ι), ContinuousSMul M (γ i)] : ContinuousSMul M ((i : ι) → γ i)

Equations

• ⋯ = ⋯

theorem continuousVAdd_sInf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [VAdd M X] {ts : Set (TopologicalSpace X)} (h : ∀ t ∈ ts, ContinuousVAdd M X) : ContinuousVAdd M X

theorem continuousSMul_sInf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [SMul M X] {ts : Set (TopologicalSpace X)} (h : ∀ t ∈ ts, ContinuousSMul M X) : ContinuousSMul M X

theorem continuousVAdd_iInf {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [VAdd M X] {ts' : ι → TopologicalSpace X} (h : ∀ (i : ι), ContinuousVAdd M X) : ContinuousVAdd M X

theorem continuousSMul_iInf {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [SMul M X] {ts' : ι → TopologicalSpace X} (h : ∀ (i : ι), ContinuousSMul M X) : ContinuousSMul M X

theorem continuousVAdd_inf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [VAdd M X] {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} [ContinuousVAdd M X] [ContinuousVAdd M X] : ContinuousVAdd M X

theorem continuousSMul_inf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [SMul M X] {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} [ContinuousSMul M X] [ContinuousSMul M X] : ContinuousSMul M X

theorem AddTorsor.connectedSpace (G : Type u_1) (P : Type u_2) [AddGroup G] [AddTorsor G P] [TopologicalSpace G] [PreconnectedSpace G] [TopologicalSpace P] [ContinuousVAdd G P] : ConnectedSpace P

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.