Documentation

Mathlib.Topology.Algebra.MulAction

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] :

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

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

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

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

(_ : ContinuousConstVAdd M X) = (_ : ContinuousConstVAdd M X)

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

(_ : ContinuousConstSMul M X) = (_ : ContinuousConstSMul M X)

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

(_ : ContinuousVAdd Mᵃᵒᵖ X) = (_ : ContinuousVAdd Mᵃᵒᵖ X)

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

(_ : ContinuousSMul Mᵐᵒᵖ X) = (_ : ContinuousSMul Mᵐᵒᵖ X)

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

(_ : ContinuousVAdd M Xᵃᵒᵖ) = (_ : ContinuousVAdd M Xᵃᵒᵖ)

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

(_ : ContinuousSMul M Xᵐᵒᵖ) = (_ : ContinuousSMul M Xᵐᵒᵖ)

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)

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

(_ : ContinuousVAdd (AddUnits M) X) = (_ : ContinuousVAdd (AddUnits M) X)

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

(_ : ContinuousSMul Mˣ X) = (_ : ContinuousSMul Mˣ X)

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] [AddGroup M] [AddAction M X] [ContinuousVAdd M X] {S : AddSubmonoid M} :

ContinuousVAdd (↥S) X

Equations

(_ : ContinuousVAdd (↥S) X) = (_ : ContinuousVAdd (↥S) X)

instance Submonoid.continuousSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [Group M] [MulAction M X] [ContinuousSMul M X] {S : Submonoid M} :

ContinuousSMul (↥S) X

Equations

(_ : ContinuousSMul (↥S) X) = (_ : ContinuousSMul (↥S) X)

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

(_ : ContinuousVAdd (↥S) X) = (_ : ContinuousVAdd (↥S) X)

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

(_ : ContinuousSMul (↥S) X) = (_ : ContinuousSMul (↥S) X)

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

(_ : ContinuousVAdd M (X × Y)) = (_ : ContinuousVAdd M (X × Y))

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

(_ : ContinuousSMul M (X × Y)) = (_ : ContinuousSMul M (X × Y))

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

(_ : ContinuousVAdd M ((i : ι) → γ i)) = (_ : ContinuousVAdd M ((i : ι) → γ i))

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

(_ : ContinuousSMul M ((i : ι) → γ i)) = (_ : ContinuousSMul M ((i : ι) → γ i))

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.