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
    theorem ContinuousSMul.continuous_smul {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace M] [TopologicalSpace X] [self : ContinuousSMul M X] :
    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] :

    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 ContinuousVAdd.continuous_vadd {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace M] [TopologicalSpace X] [self : ContinuousVAdd M X] :
      Continuous fun (p : M × X) => p.1 +ᵥ p.2

      The additive action (+ᵥ) is continuous.

      Equations
      • =
      Equations
      • =
      @[instance 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =
      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.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 : 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.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 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 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 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 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 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
      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

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

      Equations
      • =

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

      Equations
      • =
      Equations
      • =
      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) :
      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 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 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 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 : YX} {N : Type u_5} [VAdd N Y] [TopologicalSpace N] {f : NM} (hg : Inducing 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.

      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 : Inducing 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.

      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) :
      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) :
      Equations
      • =
      Equations
      • =
      Equations
      • =
      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.

      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} :
      Equations
      • =
      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} :
      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] :
      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] :
      Equations
      • =
      instance 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)
      Equations
      • =
      instance 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)
      Equations
      • =
      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_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_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_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_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] :
      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] :

      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.