Continuous monoid action #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define class has_continuous_smul. We say has_continuous_smul 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 #
has_continuous_smul M X: typeclass saying that the map(c, x) ↦ c • xis continuous onM × X;homeomorph.smul_of_ne_zero: if a group with zeroG₀(e.g., a field) acts onXandc : G₀is a nonzero element ofG₀, then scalar multiplication bycis a homeomorphism ofX;homeomorph.smul: scalar multiplication by an element of a groupGacting onXis a homeomorphism ofX.units.has_continuous_smul: scalar multiplication byMˣis continuous when scalar multiplication byMis continuous. This allowshomeomorph.smulto be used with on monoids withG = Mˣ.
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 continuous_smul.
@[class]
structure
has_continuous_smul
(M : Type u_1)
(X : Type u_2)
[has_smul M X]
[topological_space M]
[topological_space X] :
Prop
- continuous_smul : continuous (λ (p : M × X), p.fst • p.snd)
Class has_continuous_smul 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.
Instances of this typeclass
- has_bounded_smul.has_continuous_smul
- module_filter_basis.has_continuous_smul
- has_continuous_smul.op
- mul_opposite.has_continuous_smul
- units.has_continuous_smul
- prod.has_continuous_smul
- pi.has_continuous_smul
- has_continuous_mul.to_has_continuous_smul
- has_continuous_mul.to_has_continuous_smul_op
- add_monoid.has_continuous_smul_nat
- add_group.has_continuous_smul_int
- nnreal.has_continuous_smul
- submodule.has_continuous_smul
- submodule.has_continuous_smul_quotient
- subalgebra.has_continuous_smul
- star_subalgebra.has_continuous_smul
- continuous_linear_map.has_continuous_smul
- matrix.has_continuous_smul
- weak_bilin.has_continuous_smul
- weak_dual.has_continuous_smul
- pi.matrix.has_continuous_smul
@[class]
structure
has_continuous_vadd
(M : Type u_1)
(X : Type u_2)
[has_vadd M X]
[topological_space M]
[topological_space X] :
Prop
- continuous_vadd : continuous (λ (p : M × X), p.fst +ᵥ p.snd)
Class has_continuous_vadd 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.
@[protected, instance]
def
has_continuous_smul.has_continuous_const_smul
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[has_smul M X]
[has_continuous_smul M X] :
@[protected, instance]
def
has_continuous_vadd.has_continuous_const_vadd
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[has_vadd M X]
[has_continuous_vadd M X] :
theorem
filter.tendsto.vadd
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[topological_space M]
[topological_space X]
[has_vadd M X]
[has_continuous_vadd 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 (λ (x : α), f x +ᵥ g x) l (nhds (c +ᵥ a))
theorem
filter.tendsto.smul
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[topological_space M]
[topological_space X]
[has_smul M X]
[has_continuous_smul 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 (λ (x : α), f x • g x) l (nhds (c • a))
theorem
filter.tendsto.smul_const
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[topological_space M]
[topological_space X]
[has_smul M X]
[has_continuous_smul M X]
{f : α → M}
{l : filter α}
{c : M}
(hf : filter.tendsto f l (nhds c))
(a : X) :
filter.tendsto (λ (x : α), f x • a) l (nhds (c • a))
theorem
filter.tendsto.vadd_const
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[topological_space M]
[topological_space X]
[has_vadd M X]
[has_continuous_vadd M X]
{f : α → M}
{l : filter α}
{c : M}
(hf : filter.tendsto f l (nhds c))
(a : X) :
filter.tendsto (λ (x : α), f x +ᵥ a) l (nhds (c +ᵥ a))
theorem
continuous_within_at.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_smul M X]
[has_continuous_smul M X]
{f : Y → M}
{g : Y → X}
{b : Y}
{s : set Y}
(hf : continuous_within_at f s b)
(hg : continuous_within_at g s b) :
continuous_within_at (λ (x : Y), f x • g x) s b
theorem
continuous_within_at.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_vadd M X]
[has_continuous_vadd M X]
{f : Y → M}
{g : Y → X}
{b : Y}
{s : set Y}
(hf : continuous_within_at f s b)
(hg : continuous_within_at g s b) :
continuous_within_at (λ (x : Y), f x +ᵥ g x) s b
theorem
continuous_at.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_smul M X]
[has_continuous_smul M X]
{f : Y → M}
{g : Y → X}
{b : Y}
(hf : continuous_at f b)
(hg : continuous_at g b) :
continuous_at (λ (x : Y), f x • g x) b
theorem
continuous_at.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_vadd M X]
[has_continuous_vadd M X]
{f : Y → M}
{g : Y → X}
{b : Y}
(hf : continuous_at f b)
(hg : continuous_at g b) :
continuous_at (λ (x : Y), f x +ᵥ g x) b
theorem
continuous_on.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_vadd M X]
[has_continuous_vadd M X]
{f : Y → M}
{g : Y → X}
{s : set Y}
(hf : continuous_on f s)
(hg : continuous_on g s) :
continuous_on (λ (x : Y), f x +ᵥ g x) s
theorem
continuous_on.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_smul M X]
[has_continuous_smul M X]
{f : Y → M}
{g : Y → X}
{s : set Y}
(hf : continuous_on f s)
(hg : continuous_on g s) :
continuous_on (λ (x : Y), f x • g x) s
@[continuity]
theorem
continuous.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_smul M X]
[has_continuous_smul M X]
{f : Y → M}
{g : Y → X}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : Y), f x • g x)
@[continuity]
theorem
continuous.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_vadd M X]
[has_continuous_vadd M X]
{f : Y → M}
{g : Y → X}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : Y), f x +ᵥ g x)
@[protected, instance]
def
has_continuous_smul.op
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[has_smul M X]
[has_continuous_smul M X]
[has_smul Mᵐᵒᵖ X]
[is_central_scalar M X] :
If a scalar action is central, then its right action is continuous when its left action is.
@[protected, instance]
def
has_continuous_vadd.op
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[has_vadd M X]
[has_continuous_vadd M X]
[has_vadd Mᵃᵒᵖ X]
[is_central_vadd M X] :
If an additive action is central, then its right action is continuous when its left action is.
@[protected, instance]
def
add_opposite.has_continuous_vadd
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[has_vadd M X]
[has_continuous_vadd M X] :
@[protected, instance]
def
mul_opposite.has_continuous_smul
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[has_smul M X]
[has_continuous_smul M X] :
@[protected, instance]
def
units.has_continuous_smul
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[monoid M]
[mul_action M X]
[has_continuous_smul M X] :
@[protected, instance]
def
add_units.has_continuous_vadd
{M : Type u_1}
{X : Type u_2}
[topological_space M]
[topological_space X]
[add_monoid M]
[add_action M X]
[has_continuous_vadd M X] :
has_continuous_vadd (add_units M) X
@[protected, instance]
def
prod.has_continuous_smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_smul M X]
[has_smul M Y]
[has_continuous_smul M X]
[has_continuous_smul M Y] :
has_continuous_smul M (X × Y)
@[protected, instance]
def
prod.has_continuous_vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[topological_space M]
[topological_space X]
[topological_space Y]
[has_vadd M X]
[has_vadd M Y]
[has_continuous_vadd M X]
[has_continuous_vadd M Y] :
has_continuous_vadd M (X × Y)
@[protected, instance]
def
pi.has_continuous_vadd
{M : Type u_1}
[topological_space M]
{ι : Type u_2}
{γ : ι → Type u_3}
[Π (i : ι), topological_space (γ i)]
[Π (i : ι), has_vadd M (γ i)]
[∀ (i : ι), has_continuous_vadd M (γ i)] :
has_continuous_vadd M (Π (i : ι), γ i)
@[protected, instance]
def
pi.has_continuous_smul
{M : Type u_1}
[topological_space M]
{ι : Type u_2}
{γ : ι → Type u_3}
[Π (i : ι), topological_space (γ i)]
[Π (i : ι), has_smul M (γ i)]
[∀ (i : ι), has_continuous_smul M (γ i)] :
has_continuous_smul M (Π (i : ι), γ i)
theorem
has_continuous_vadd_Inf
{M : Type u_2}
{X : Type u_3}
[topological_space M]
[has_vadd M X]
{ts : set (topological_space X)}
(h : ∀ (t : topological_space X), t ∈ ts → has_continuous_vadd M X) :
theorem
has_continuous_smul_Inf
{M : Type u_2}
{X : Type u_3}
[topological_space M]
[has_smul M X]
{ts : set (topological_space X)}
(h : ∀ (t : topological_space X), t ∈ ts → has_continuous_smul M X) :
theorem
has_continuous_vadd_infi
{ι : Sort u_1}
{M : Type u_2}
{X : Type u_3}
[topological_space M]
[has_vadd M X]
{ts' : ι → topological_space X}
(h : ∀ (i : ι), has_continuous_vadd M X) :
theorem
has_continuous_smul_infi
{ι : Sort u_1}
{M : Type u_2}
{X : Type u_3}
[topological_space M]
[has_smul M X]
{ts' : ι → topological_space X}
(h : ∀ (i : ι), has_continuous_smul M X) :
theorem
has_continuous_vadd_inf
{M : Type u_2}
{X : Type u_3}
[topological_space M]
[has_vadd M X]
{t₁ t₂ : topological_space X}
[has_continuous_vadd M X]
[has_continuous_vadd M X] :
theorem
has_continuous_smul_inf
{M : Type u_2}
{X : Type u_3}
[topological_space M]
[has_smul M X]
{t₁ t₂ : topological_space X}
[has_continuous_smul M X]
[has_continuous_smul M X] :
@[protected]
theorem
add_torsor.connected_space
(G : Type u_1)
(P : Type u_2)
[add_group G]
[add_torsor G P]
[topological_space G]
[preconnected_space G]
[topological_space P]
[has_continuous_vadd G P] :
An add_torsor for a connected space is a connected space. This is not an instance because
it loops for a group as a torsor over itself.