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 #

-- Porting note: These have all moved

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
      theorem IsScalarTower.continuousSMul {M : Type u_5} (N : Type u_6) {α : Type u_7} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace α] [ContinuousSMul M N] [ContinuousSMul N α] :
      theorem ContinuousSMul.induced {R : Type u_5} {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [TopologicalSpace R] [LinearMapClass F R α β] [tβ : TopologicalSpace β] [ContinuousSMul R β] (f : F) :
      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 {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_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 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 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 : YM} {g : YX} {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.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 : YM} {g : YX} {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.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 : YM} {g : YX} {b : Y} (hf : ContinuousAt f b) (hg : ContinuousAt g b) :
      ContinuousAt (fun (x : Y) => f x g x) 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 : YM} {g : YX} {b : Y} (hf : ContinuousAt f b) (hg : ContinuousAt g b) :
      ContinuousAt (fun (x : Y) => f x +ᵥ g x) b
      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 : YM} {g : YX} {s : Set Y} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
      ContinuousOn (fun (x : Y) => f x g x) s
      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 : YM} {g : YX} {s : Set Y} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
      ContinuousOn (fun (x : Y) => f x +ᵥ g x) s
      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 : YM} {g : YX} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : Y) => f x g x
      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 : YM} {g : YX} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : Y) => f x +ᵥ g x

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

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

      theorem Specializes.smul {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {a b : M} {x y : X} (h₁ : a b) (h₂ : x y) :
      (a x) (b y)
      theorem Specializes.vadd {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {a b : M} {x y : X} (h₁ : a b) (h₂ : x y) :
      (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 b : M} {x y : X} (h₁ : Inseparable a b) (h₂ : Inseparable x y) :
      Inseparable (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 b : M} {x y : X} (h₁ : Inseparable a b) (h₂ : Inseparable x y) :
      Inseparable (a +ᵥ x) (b +ᵥ y)
      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) :
      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) :
      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) :
      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) :
      theorem Topology.IsInducing.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 : YX} {N : Type u_5} [SMul N Y] [TopologicalSpace N] {f : NM} (hg : Topology.IsInducing g) (hf : Continuous f) (hsmul : ∀ {c : N} {x : Y}, g (c x) = f c g x) :

      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.

      theorem Topology.IsInducing.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 : YX} {N : Type u_5} [VAdd N Y] [TopologicalSpace N] {f : NM} (hg : Topology.IsInducing g) (hf : Continuous f) (hsmul : ∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x) :

      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.

      @[deprecated Topology.IsInducing.continuousSMul]
      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 : YX} {N : Type u_5} [SMul N Y] [TopologicalSpace N] {f : NM} (hg : Topology.IsInducing g) (hf : Continuous f) (hsmul : ∀ {c : N} {x : Y}, g (c x) = f c g x) :

      Alias of Topology.IsInducing.continuousSMul.


      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.

      theorem 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) :
      theorem 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) :
      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) :

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

      The stabilizer of a continuous group action on a discrete space is an open subgroup.

      theorem 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] :
      theorem 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] :
      theorem instContinuousSMulForall {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 instContinuousVAddForall {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)
      theorem continuousSMul_sInf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [SMul M X] {ts : Set (TopologicalSpace X)} (h : tts, ContinuousSMul M X) :
      theorem continuousVAdd_sInf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [VAdd M X] {ts : Set (TopologicalSpace X)} (h : tts, 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) :
      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) :
      theorem continuousSMul_inf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [SMul M X] {t₁ t₂ : TopologicalSpace X} [ContinuousSMul M X] [ContinuousSMul M X] :
      theorem continuousVAdd_inf {M : Type u_2} {X : Type u_3} [TopologicalSpace M] [VAdd M X] {t₁ t₂ : TopologicalSpace X} [ContinuousVAdd M X] [ContinuousVAdd M X] :

      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.