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 • xis continuous onM × X;Units.continuousSMul: scalar multiplication byMˣis continuous when scalar multiplication byMis continuous. This allowsHomeomorph.smulto be used with on monoids withG = Mˣ.
-- Porting note: These have all moved
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.
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]
:
- continuous_smul : Continuous fun p => p.fst • p.snd
The scalar multiplication
(•)is continuous.
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.
Instances
class
ContinuousVAdd
(M : Type u_1)
(X : Type u_2)
[VAdd M X]
[TopologicalSpace M]
[TopologicalSpace X]
:
- continuous_vadd : Continuous fun p => p.fst +ᵥ p.snd
The additive action
(+ᵥ)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.
Instances
instance
ContinuousVAdd.continuousConstVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
:
theorem
ContinuousVAdd.continuousConstVAdd.proof_1
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
:
instance
ContinuousSMul.continuousConstSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => f x • g x
theorem
ContinuousVAdd.op.proof_1
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
[VAdd Mᵃᵒᵖ X]
[IsCentralVAdd M 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]
:
If an additive action is central, then its right action is continuous when its left action is.
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]
:
If a scalar action is central, then its right action is continuous when its left action is.
theorem
AddOpposite.continuousVAdd.proof_1
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
:
instance
AddOpposite.continuousVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd 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]
:
theorem
AddUnits.continuousVAdd.proof_1
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddMonoid M]
[AddAction M X]
[ContinuousVAdd M X]
:
ContinuousVAdd (AddUnits M) X
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
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
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 { x // x ∈ S } X
theorem
AddSubmonoid.continuousVAdd.proof_1
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddGroup M]
[AddAction M X]
[ContinuousVAdd M X]
{S : AddSubmonoid M}
:
ContinuousVAdd { x // x ∈ 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 { x // x ∈ S } X
theorem
AddSubgroup.continuousVAdd.proof_1
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddGroup M]
[AddAction M X]
[ContinuousVAdd M X]
{S : AddSubgroup M}
:
ContinuousVAdd { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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)
theorem
Prod.continuousVAdd.proof_1
{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)
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)
theorem
instContinuousVAddForAllInstVAddTopologicalSpace.proof_1
{M : Type u_1}
[TopologicalSpace M]
{ι : Type u_2}
{γ : ι → Type u_3}
[(i : ι) → TopologicalSpace (γ i)]
[(i : ι) → VAdd M (γ i)]
[∀ (i : ι), ContinuousVAdd M (γ i)]
:
ContinuousVAdd M ((i : ι) → γ i)
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)
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)
theorem
continuousVAdd_sInf
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[VAdd M X]
{ts : Set (TopologicalSpace X)}
(h : ∀ (t : TopologicalSpace X), 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 : TopologicalSpace X), 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]
:
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.