Mathlib.Topology.Algebra.ConstMulAction

ContinuousConstSMul structure

(Γ : Type*) (T : Type*) [TopologicalSpace T] [SMul Γ T]

Full source

/-- Class `ContinuousConstSMul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
is continuous in the second argument. We use the same class for all kinds of multiplicative
actions, including (semi)modules and algebras.

Note that both `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α` are
weaker versions of `ContinuousMul α`. -/
class ContinuousConstSMul (Γ : Type*) (T : Type*) [TopologicalSpace T] [SMul Γ T] : Prop where
  /-- The scalar multiplication `(•) : Γ → T → T` is continuous in the second argument. -/
  continuous_const_smul : ∀ γ : Γ, Continuous fun x : T => γ • x

Continuous scalar multiplication in the second variable

Informal description

The structure `ContinuousConstSMul Γ T` is a typeclass that asserts for a topological space `T` with a scalar multiplication action by `Γ`, the map `x ↦ γ • x` is continuous in the second argument for each fixed `γ ∈ Γ`. This is a weaker condition than requiring joint continuity in both variables.

ContinuousConstVAdd structure

(Γ : Type*) (T : Type*) [TopologicalSpace T] [VAdd Γ T]

Full source

/-- Class `ContinuousConstVAdd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
is continuous in the second argument. We use the same class for all kinds of additive actions,
including (semi)modules and algebras.

Note that both `ContinuousConstVAdd α α` and `ContinuousConstVAdd αᵐᵒᵖ α` are
weaker versions of `ContinuousVAdd α`. -/
class ContinuousConstVAdd (Γ : Type*) (T : Type*) [TopologicalSpace T] [VAdd Γ T] : Prop where
  /-- The additive action `(+ᵥ) : Γ → T → T` is continuous in the second argument. -/
  continuous_const_vadd : ∀ γ : Γ, Continuous fun x : T => γ +ᵥ x

Continuous Additive Action in Second Variable

Informal description

The structure `ContinuousConstVAdd Γ T` asserts that for a topological space `T` with an additive action by `Γ`, the map `x ↦ γ +ᵥ x` is continuous for each fixed `γ ∈ Γ`. This class is used for various types of additive actions, including (semi)modules and algebras.

instContinuousConstSMulULift instance

: ContinuousConstSMul (ULift M) α

Full source

@[to_additive]
instance : ContinuousConstSMul (ULift M) α := ⟨fun γ ↦ continuous_const_smul (ULift.down γ)⟩

Continuity of Lifted Scalar Multiplication in Second Variable

Informal description

For any topological space $\alpha$ with a scalar multiplication action by $M$, the lifted action via `ULift M` on $\alpha$ is continuous in the second variable. That is, for each fixed $\gamma$ in `ULift M`, the map $x \mapsto \gamma \cdot x$ is continuous on $\alpha$.

Filter.Tendsto.const_smul theorem

 {f : β → α} {l : Filter β} {a : α} (hf : Tendsto f l (𝓝 a)) (c : M) : Tendsto (fun x => c • f x) l (𝓝 (c • a))

Full source

@[to_additive]
theorem Filter.Tendsto.const_smul {f : β → α} {l : Filter β} {a : α} (hf : Tendsto f l (𝓝 a))
    (c : M) : Tendsto (fun x => c • f x) l (𝓝 (c • a)) :=
  ((continuous_const_smul _).tendsto _).comp hf

Scalar Multiplication Preserves Filter Limits

Informal description

Let $f : \beta \to \alpha$ be a function between topological spaces, and let $l$ be a filter on $\beta$. If $f$ tends to $a \in \alpha$ along $l$, then for any scalar $c \in M$, the function $x \mapsto c \cdot f(x)$ tends to $c \cdot a$ along $l$.

ContinuousWithinAt.const_smul theorem

(hg : ContinuousWithinAt g s b) (c : M) : ContinuousWithinAt (fun x => c • g x) s b

Full source

@[to_additive]
nonrec theorem ContinuousWithinAt.const_smul (hg : ContinuousWithinAt g s b) (c : M) :
    ContinuousWithinAt (fun x => c • g x) s b :=
  hg.const_smul c

Scalar Multiplication Preserves Continuity Within a Set at a Point

Informal description

Let $g$ be a function between topological spaces that is continuous within a set $s$ at a point $b$. Then for any scalar $c \in M$, the function $x \mapsto c \cdot g(x)$ is continuous within $s$ at $b$.

ContinuousAt.const_smul theorem

(hg : ContinuousAt g b) (c : M) : ContinuousAt (fun x => c • g x) b

Full source

@[to_additive (attr := fun_prop)]
nonrec theorem ContinuousAt.const_smul (hg : ContinuousAt g b) (c : M) :
    ContinuousAt (fun x => c • g x) b :=
  hg.const_smul c

Continuity of Scalar Multiplication at a Point

Informal description

Let $g$ be a function between topological spaces that is continuous at a point $b$. Then for any scalar $c \in M$, the function $x \mapsto c \cdot g(x)$ is continuous at $b$.

ContinuousOn.const_smul theorem

(hg : ContinuousOn g s) (c : M) : ContinuousOn (fun x => c • g x) s

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousOn.const_smul (hg : ContinuousOn g s) (c : M) :
    ContinuousOn (fun x => c • g x) s := fun x hx => (hg x hx).const_smul c

Scalar Multiplication Preserves Continuity on a Set

Informal description

Let $g$ be a function between topological spaces that is continuous on a set $s$. Then for any scalar $c \in M$, the function $x \mapsto c \cdot g(x)$ is continuous on $s$.

Continuous.const_smul theorem

(hg : Continuous g) (c : M) : Continuous fun x => c • g x

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem Continuous.const_smul (hg : Continuous g) (c : M) : Continuous fun x => c • g x :=
  (continuous_const_smul _).comp hg

Continuity of scalar multiplication of a continuous function

Informal description

Let $g$ be a continuous function and let $c$ be an element of $M$. Then the function $x \mapsto c \cdot g(x)$ is continuous.

ContinuousConstSMul.op instance

[SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : ContinuousConstSMul Mᵐᵒᵖ α

Full source

/-- If a scalar is central, then its right action is continuous when its left action is. -/
@[to_additive "If an additive action is central, then its right action is continuous when its left
action is."]
instance ContinuousConstSMul.op [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] :
    ContinuousConstSMul Mᵐᵒᵖ α :=
  ⟨MulOpposite.rec' fun c => by simpa only [op_smul_eq_smul] using continuous_const_smul c⟩

Continuity of Central Right Scalar Multiplication from Left Action

Informal description

For any topological space $\alpha$ with a scalar multiplication action by $M$ where the action is central (i.e., left and right actions coincide), if the left action is continuous in the second variable, then the right action is also continuous in the second variable.

MulOpposite.continuousConstSMul instance

: ContinuousConstSMul M αᵐᵒᵖ

Full source

@[to_additive]
instance MulOpposite.continuousConstSMul : ContinuousConstSMul M αᵐᵒᵖ :=
  ⟨fun c => MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.const_smul c⟩

Continuous Scalar Multiplication on Opposite Monoids

Informal description

For any topological space $\alpha$ with a scalar multiplication action by $M$, the opposite monoid $\alpha^{\text{op}}$ inherits a continuous scalar multiplication structure in the second variable from $\alpha$.

instContinuousConstSMulOrderDual instance

: ContinuousConstSMul M αᵒᵈ

Full source

@[to_additive]
instance : ContinuousConstSMul M αᵒᵈ := ‹ContinuousConstSMul M α›

Continuous Scalar Multiplication on Order Duals

Informal description

For any type $M$ acting on a topological space $\alpha$ with continuous scalar multiplication in the second variable, the order dual $\alpha^\circ$ also has a continuous scalar multiplication structure in the second variable.

OrderDual.continuousConstSMul' instance

: ContinuousConstSMul Mᵒᵈ α

Full source

@[to_additive]
instance OrderDual.continuousConstSMul' : ContinuousConstSMul Mᵒᵈ α :=
  ‹ContinuousConstSMul M α›

Continuous Scalar Multiplication on Order Duals

Informal description

For any type `M` with an order dual structure and a topological space `α` with a scalar multiplication action by `Mᵒᵈ`, the map `x ↦ γ • x` is continuous in the second argument for each fixed `γ ∈ Mᵒᵈ`.

Prod.continuousConstSMul instance

[SMul M β] [ContinuousConstSMul M β] : ContinuousConstSMul M (α × β)

Full source

@[to_additive]
instance Prod.continuousConstSMul [SMul M β] [ContinuousConstSMul M β] :
    ContinuousConstSMul M (α × β) :=
  ⟨fun _ => (continuous_fst.const_smul _).prodMk (continuous_snd.const_smul _)⟩

Continuous Scalar Multiplication on Product Spaces

Informal description

For any topological space $\alpha$ and any type $M$ acting on another topological space $\beta$ with continuous scalar multiplication in the second variable, the product space $\alpha \times \beta$ also has a continuous scalar multiplication structure in the second variable.

instContinuousConstSMulForall instance

 {ι : Type*} {γ : ι → Type*} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)] [∀ i, ContinuousConstSMul M (γ i)] :
  ContinuousConstSMul M (∀ i, γ i)

Full source

@[to_additive]
instance {ι : Type*} {γ : ι → Type*} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)]
    [∀ i, ContinuousConstSMul M (γ i)] : ContinuousConstSMul M (∀ i, γ i) :=
  ⟨fun _ => continuous_pi fun i => (continuous_apply i).const_smul _⟩

Continuous Scalar Multiplication on Product Spaces

Informal description

For any family of topological spaces $\{\gamma_i\}_{i \in \iota}$ where each $\gamma_i$ has a scalar multiplication action by $M$ that is continuous in the second variable, the product space $\prod_{i \in \iota} \gamma_i$ also has a continuous scalar multiplication structure in the second variable.

IsCompact.smul theorem

 {α β} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α) {s : Set β} (hs : IsCompact s) :
  IsCompact (a • s)

Full source

@[to_additive]
theorem IsCompact.smul {α β} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α)
    {s : Set β} (hs : IsCompact s) : IsCompact (a • s) :=
  hs.image (continuous_id.const_smul a)

Compactness is Preserved under Scalar Multiplication

Informal description

Let $\alpha$ and $\beta$ be types with a scalar multiplication action of $\alpha$ on $\beta$, and suppose $\beta$ is equipped with a topological space structure such that scalar multiplication is continuous in the second variable. For any element $a \in \alpha$ and any compact subset $s \subseteq \beta$, the image of $s$ under scalar multiplication by $a$, denoted $a \cdot s$, is also compact.

Specializes.const_smul theorem

{x y : α} (h : x ⤳ y) (c : M) : (c • x) ⤳ (c • y)

Full source

@[to_additive]
theorem Specializes.const_smul {x y : α} (h : x ⤳ y) (c : M) : (c • x) ⤳ (c • y) :=
  h.map (continuous_const_smul c)

Scalar Multiplication Preserves Specialization

Informal description

For any elements $x$ and $y$ in a topological space $\alpha$ with a scalar multiplication action by $M$, if $x$ specializes to $y$ (denoted $x \rightsquigarrow y$), then for any scalar $c \in M$, the scalar multiple $c \cdot x$ specializes to $c \cdot y$ (denoted $c \cdot x \rightsquigarrow c \cdot y$).

Inseparable.const_smul theorem

{x y : α} (h : Inseparable x y) (c : M) : Inseparable (c • x) (c • y)

Full source

@[to_additive]
theorem Inseparable.const_smul {x y : α} (h : Inseparable x y) (c : M) :
    Inseparable (c • x) (c • y) :=
  h.map (continuous_const_smul c)

Scalar Multiplication Preserves Topological Inseparability

Informal description

For any elements $x$ and $y$ in a topological space $\alpha$ with a scalar multiplication action by $M$, if $x$ and $y$ are topologically inseparable, then for any scalar $c \in M$, the scalar multiples $c \cdot x$ and $c \cdot y$ are also topologically inseparable.

Topology.IsInducing.continuousConstSMul theorem

 {N β : Type*} [SMul N β] [TopologicalSpace β] {g : β → α} (hg : IsInducing g) (f : N → M)
  (hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x) : ContinuousConstSMul N β

Full source

@[to_additive]
theorem Topology.IsInducing.continuousConstSMul {N β : Type*} [SMul N β] [TopologicalSpace β]
    {g : β → α} (hg : IsInducing g) (f : N → M) (hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x) :
    ContinuousConstSMul N β where
  continuous_const_smul c := by
    simpa only [Function.comp_def, hf, hg.continuous_iff] using hg.continuous.const_smul (f c)

Induced Topology Preserves Continuity of Scalar Multiplication in the Second Variable

Informal description

Let $N$ and $\beta$ be types with a scalar multiplication action by $N$ on $\beta$, and let $\beta$ be equipped with a topological space structure. Suppose $g : \beta \to \alpha$ is an inducing map (i.e., the topology on $\beta$ is induced by $g$ from the topology on $\alpha$). If there exists a function $f : N \to M$ such that for all $c \in N$ and $x \in \beta$, the relation $g(c \cdot x) = f(c) \cdot g(x)$ holds, then the scalar multiplication action of $N$ on $\beta$ is continuous in the second variable (i.e., $\beta$ has the `ContinuousConstSMul N β` property).

Units.continuousConstSMul instance

: ContinuousConstSMul Mˣ α

Full source

@[to_additive]
instance Units.continuousConstSMul : ContinuousConstSMul Mˣ α where
  continuous_const_smul m := continuous_const_smul (m : M)

Continuity of Scalar Multiplication by Units

Informal description

For any topological space $\alpha$ with a scalar multiplication action by the group of units $M^\times$, the map $x \mapsto u \cdot x$ is continuous in $x$ for each fixed unit $u \in M^\times$.

smul_closure_subset theorem

(c : M) (s : Set α) : c • closure s ⊆ closure (c • s)

Full source

@[to_additive]
theorem smul_closure_subset (c : M) (s : Set α) : c • closure s ⊆ closure (c • s) :=
  ((Set.mapsTo_image _ _).closure <| continuous_const_smul c).image_subset

Scalar Multiplication Preserves Closure Inclusion

Informal description

For any element $c$ in a monoid $M$ acting on a topological space $\alpha$, and any subset $s \subseteq \alpha$, the scalar multiplication of $c$ with the closure of $s$ is contained in the closure of the scalar multiplication of $c$ with $s$. In other words, $c \cdot \overline{s} \subseteq \overline{c \cdot s}$.

smul_closure_orbit_subset theorem

(c : M) (x : α) : c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x)

Full source

@[to_additive]
theorem smul_closure_orbit_subset (c : M) (x : α) :
    c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x) :=
  (smul_closure_subset c _).trans <| closure_mono <| MulAction.smul_orbit_subset _ _

Scalar Multiplication Preserves Closure of Orbit

Informal description

For any element $c$ in a monoid $M$ acting on a topological space $\alpha$, and any element $x \in \alpha$, the scalar multiplication of $c$ with the closure of the orbit of $x$ under $M$ is contained in the closure of the orbit of $x$. In other words, $c \cdot \overline{\text{orbit}_M(x)} \subseteq \overline{\text{orbit}_M(x)}$.

isClosed_setOf_map_smul theorem

 {N : Type*} [Monoid N] (α β) [MulAction M α] [MulAction N β] [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β]
  (σ : M → N) : IsClosed {f : α → β | ∀ c x, f (c • x) = σ c • f x}

Full source

theorem isClosed_setOf_map_smul {N : Type*} [Monoid N] (α β) [MulAction M α] [MulAction N β]
    [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : M → N) :
    IsClosed { f : α → β | ∀ c x, f (c • x) = σ c • f x } := by
  simp only [Set.setOf_forall]
  exact isClosed_iInter fun c => isClosed_iInter fun x =>
    isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)

Closedness of $\sigma$-Equivariant Function Space under Monoid Actions

Informal description

Let $M$ and $N$ be monoids acting on topological spaces $\alpha$ and $\beta$ respectively, with $\beta$ being a Hausdorff space and having continuous scalar multiplication in the second variable by $N$. Given a map $\sigma: M \to N$, the set of functions $\{f : \alpha \to \beta \mid \forall c \in M, \forall x \in \alpha, f(c \cdot x) = \sigma(c) \cdot f(x)\}$ is closed in the function space $\alpha \to \beta$.

tendsto_const_smul_iff theorem

 {f : β → α} {l : Filter β} {a : α} (c : G) : Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a)

Full source

@[to_additive]
theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G) :
    TendstoTendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
  ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩

Equivalence of Filter Limits under Scalar Multiplication

Informal description

Let $f : \beta \to \alpha$ be a function between topological spaces, and let $l$ be a filter on $\beta$. For any element $c$ in a group $G$ acting on $\alpha$, the function $x \mapsto c \cdot f(x)$ tends to $c \cdot a$ along $l$ if and only if $f$ tends to $a$ along $l$.

continuousWithinAt_const_smul_iff theorem

(c : G) : ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b

Full source

@[to_additive]
theorem continuousWithinAt_const_smul_iff (c : G) :
    ContinuousWithinAtContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b :=
  tendsto_const_smul_iff c

Continuity Within a Subset under Scalar Multiplication by a Fixed Group Element

Informal description

For a fixed element $c$ in a group $G$ acting on a topological space, the function $x \mapsto c \cdot x$ is continuous within a subset $s$ at a point $b$ if and only if the identity function is continuous within $s$ at $b$. In other words, the map $f(x) = c \cdot x$ is continuous within $s$ at $b$ precisely when $f$ itself is continuous within $s$ at $b$.

continuousOn_const_smul_iff theorem

(c : G) : ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s

Full source

@[to_additive]
theorem continuousOn_const_smul_iff (c : G) :
    ContinuousOnContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s :=
  forall₂_congr fun _ _ => continuousWithinAt_const_smul_iff c

Continuity on a Subset under Scalar Multiplication by a Fixed Group Element

Informal description

For a fixed element $c$ in a group $G$ acting on a topological space, the function $x \mapsto c \cdot f(x)$ is continuous on a subset $s$ if and only if $f$ is continuous on $s$.

continuousAt_const_smul_iff theorem

(c : G) : ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b

Full source

@[to_additive]
theorem continuousAt_const_smul_iff (c : G) :
    ContinuousAtContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b :=
  tendsto_const_smul_iff c

Continuity at a Point under Scalar Multiplication by a Fixed Group Element

Informal description

For a fixed element $c$ in a group $G$ acting on a topological space, the function $x \mapsto c \cdot x$ is continuous at a point $b$ if and only if the identity function is continuous at $b$. In other words, the map $f(x) = c \cdot x$ is continuous at $b$ precisely when $f$ itself is continuous at $b$.

continuous_const_smul_iff theorem

(c : G) : (Continuous fun x => c • f x) ↔ Continuous f

Full source

@[to_additive]
theorem continuous_const_smul_iff (c : G) : (Continuous fun x => c • f x) ↔ Continuous f := by
  simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]

Continuity of Scalar Multiplication by a Fixed Group Element

Informal description

For a fixed element $c$ in a group $G$ acting on a topological space, the map $x \mapsto c \cdot x$ is continuous if and only if the identity map is continuous. In other words, the function $f$ defined by $f(x) = c \cdot x$ is continuous precisely when the original function $f$ is continuous.

Homeomorph.smul definition

(γ : G) : α ≃ₜ α

Full source

/-- The homeomorphism given by scalar multiplication by a given element of a group `Γ` acting on
  `T` is a homeomorphism from `T` to itself. -/
@[to_additive (attr := simps!)]
def Homeomorph.smul (γ : G) : α ≃ₜ α where
  toEquiv := MulAction.toPerm γ
  continuous_toFun := continuous_const_smul γ
  continuous_invFun := continuous_const_smul γ⁻¹

Homeomorphism induced by scalar multiplication

Informal description

For a group $G$ acting on a topological space $\alpha$, the scalar multiplication by a fixed element $\gamma \in G$ is a homeomorphism of $\alpha$ to itself. This means the map $x \mapsto \gamma \cdot x$ is continuous with a continuous inverse given by scalar multiplication with $\gamma^{-1}$.

isOpenMap_smul theorem

(c : G) : IsOpenMap fun x : α => c • x

Full source

@[to_additive]
theorem isOpenMap_smul (c : G) : IsOpenMap fun x : α => c • x :=
  (Homeomorph.smul c).isOpenMap

Openness of Scalar Multiplication by a Group Element

Informal description

For any element $c$ in a group $G$ acting on a topological space $\alpha$, the map $x \mapsto c \cdot x$ is an open map. That is, the image of any open set under this map is open in $\alpha$.

IsOpen.smul theorem

{s : Set α} (hs : IsOpen s) (c : G) : IsOpen (c • s)

Full source

@[to_additive]
theorem IsOpen.smul {s : Set α} (hs : IsOpen s) (c : G) : IsOpen (c • s) :=
  isOpenMap_smul c s hs

Openness of Scalar Multiplication Image for Open Sets

Informal description

For any open subset $s$ of a topological space $\alpha$ and any element $c$ of a group $G$ acting on $\alpha$, the image of $s$ under scalar multiplication by $c$ (denoted $c \cdot s$) is open in $\alpha$.

isClosedMap_smul theorem

(c : G) : IsClosedMap fun x : α => c • x

Full source

@[to_additive]
theorem isClosedMap_smul (c : G) : IsClosedMap fun x : α => c • x :=
  (Homeomorph.smul c).isClosedMap

Closedness of Scalar Multiplication by a Group Element

Informal description

For any element $c$ in a group $G$ acting on a topological space $\alpha$, the map $x \mapsto c \cdot x$ is a closed map. That is, the image of any closed set under this map is closed in $\alpha$.

IsClosed.smul theorem

{s : Set α} (hs : IsClosed s) (c : G) : IsClosed (c • s)

Full source

@[to_additive]
theorem IsClosed.smul {s : Set α} (hs : IsClosed s) (c : G) : IsClosed (c • s) :=
  isClosedMap_smul c s hs

Closedness of Scalar Multiplication Image for Closed Sets

Informal description

For any closed subset $s$ of a topological space $\alpha$ and any element $c$ of a group $G$ acting on $\alpha$, the image of $s$ under scalar multiplication by $c$ (denoted $c \cdot s$) is closed in $\alpha$.

closure_smul theorem

(c : G) (s : Set α) : closure (c • s) = c • closure s

Full source

@[to_additive]
theorem closure_smul (c : G) (s : Set α) : closure (c • s) = c • closure s :=
  ((Homeomorph.smul c).image_closure s).symm

Closure Commutes with Scalar Multiplication

Informal description

For any element $c$ of a group $G$ acting on a topological space $\alpha$, and any subset $s \subseteq \alpha$, the closure of the scaled set $c \cdot s$ is equal to the scaling of the closure of $s$ by $c$, i.e., $\overline{c \cdot s} = c \cdot \overline{s}$.

Dense.smul theorem

(c : G) {s : Set α} (hs : Dense s) : Dense (c • s)

Full source

@[to_additive]
theorem Dense.smul (c : G) {s : Set α} (hs : Dense s) : Dense (c • s) := by
  rw [dense_iff_closure_eq] at hs ⊢; rw [closure_smul, hs, smul_set_univ]

Density Preservation under Scalar Multiplication

Informal description

For any element $c$ of a group $G$ acting on a topological space $\alpha$, and any dense subset $s \subseteq \alpha$, the image of $s$ under scalar multiplication by $c$ (denoted $c \cdot s$) is dense in $\alpha$.

interior_smul theorem

(c : G) (s : Set α) : interior (c • s) = c • interior s

Full source

@[to_additive]
theorem interior_smul (c : G) (s : Set α) : interior (c • s) = c • interior s :=
  ((Homeomorph.smul c).image_interior s).symm

Interior Commutes with Scalar Multiplication

Informal description

For any element $c$ of a group $G$ acting on a topological space $\alpha$, and any subset $s \subseteq \alpha$, the interior of the scaled set $c \cdot s$ is equal to the scaling of the interior of $s$ by $c$, i.e., $\text{interior}(c \cdot s) = c \cdot \text{interior}(s)$.

IsOpen.smul_left theorem

{s : Set G} {t : Set α} (ht : IsOpen t) : IsOpen (s • t)

Full source

@[to_additive]
theorem IsOpen.smul_left {s : Set G} {t : Set α} (ht : IsOpen t) : IsOpen (s • t) := by
  rw [← iUnion_smul_set]
  exact isOpen_biUnion fun a _ => ht.smul _

Openness of Left Scalar Multiplication Image for Open Sets

Informal description

For any subset $s$ of a group $G$ acting on a topological space $\alpha$, and any open subset $t \subseteq \alpha$, the set $s \cdot t$ is open in $\alpha$.

subset_interior_smul_right theorem

{s : Set G} {t : Set α} : s • interior t ⊆ interior (s • t)

Full source

@[to_additive]
theorem subset_interior_smul_right {s : Set G} {t : Set α} : s • interior t ⊆ interior (s • t) :=
  interior_maximal (Set.smul_subset_smul_left interior_subset) isOpen_interior.smul_left

Inclusion of Scalar Multiplication with Interior in Interior of Scalar Multiplication

Informal description

For any subset $s$ of a group $G$ acting on a topological space $\alpha$, and any subset $t \subseteq \alpha$, the scalar multiplication of $s$ with the interior of $t$ is contained in the interior of the scalar multiplication of $s$ with $t$, i.e., $s \cdot \text{interior}(t) \subseteq \text{interior}(s \cdot t)$.

smul_mem_nhds_smul_iff theorem

{t : Set α} (g : G) {a : α} : g • t ∈ 𝓝 (g • a) ↔ t ∈ 𝓝 a

Full source

@[to_additive (attr := simp)]
theorem smul_mem_nhds_smul_iff {t : Set α} (g : G) {a : α} : g • t ∈ 𝓝 (g • a)g • t ∈ 𝓝 (g • a) ↔ t ∈ 𝓝 a :=
  (Homeomorph.smul g).isOpenEmbedding.image_mem_nhds

Neighborhood Invariance under Scalar Multiplication: $g \cdot t \in \mathcal{N}(g \cdot a) \leftrightarrow t \in \mathcal{N}(a)$

Informal description

For a group $G$ acting on a topological space $\alpha$, a set $t \subseteq \alpha$, and an element $a \in \alpha$, the set $g \cdot t$ is a neighborhood of $g \cdot a$ if and only if $t$ is a neighborhood of $a$.

smul_mem_nhds_self theorem

[TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G} : g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1

Full source

@[to_additive (attr := simp)]
theorem smul_mem_nhds_self [TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G} :
    g • s ∈ 𝓝 gg • s ∈ 𝓝 g ↔ s ∈ 𝓝 1 := by
  rw [← smul_mem_nhds_smul_iff g⁻¹]; simp

Neighborhood condition for scalar multiplication: $g \cdot s \in \mathcal{N}(g) \leftrightarrow s \in \mathcal{N}(1)$

Informal description

Let $G$ be a topological space with a continuous scalar multiplication action by itself. For any $g \in G$ and any subset $s \subseteq G$, the set $g \cdot s$ is a neighborhood of $g$ if and only if $s$ is a neighborhood of the identity element $1 \in G$.

tendsto_const_smul_iff₀ theorem

 {f : β → α} {l : Filter β} {a : α} {c : G₀} (hc : c ≠ 0) :
  Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a)

Full source

theorem tendsto_const_smul_iff₀ {f : β → α} {l : Filter β} {a : α} {c : G₀} (hc : c ≠ 0) :
    TendstoTendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
  tendsto_const_smul_iff (Units.mk0 c hc)

Limit Equivalence under Nonzero Scalar Multiplication: $c \cdot f(x) \to c \cdot a \leftrightarrow f(x) \to a$ for $c \neq 0$

Informal description

Let $G₀$ be a group with zero acting on a topological space $\alpha$, and let $f : \beta \to \alpha$ be a function. For any filter $l$ on $\beta$, any point $a \in \alpha$, and any nonzero element $c \in G₀$, the function $x \mapsto c \cdot f(x)$ tends to $c \cdot a$ along $l$ if and only if $f$ tends to $a$ along $l$.

continuousWithinAt_const_smul_iff₀ theorem

(hc : c ≠ 0) : ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b

Full source

theorem continuousWithinAt_const_smul_iff₀ (hc : c ≠ 0) :
    ContinuousWithinAtContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b :=
  tendsto_const_smul_iff (Units.mk0 c hc)

Continuity within a Set under Nonzero Scalar Multiplication: $c \cdot f(x)$ continuous at $b$ in $s$ $\leftrightarrow$ $f(x)$ continuous at $b$ in $s$ for $c \neq 0$

Informal description

Let $G₀$ be a group with zero acting on a topological space $\alpha$, and let $f : \beta \to \alpha$ be a function. For any subset $s \subseteq \beta$, any point $b \in \beta$, and any nonzero element $c \in G₀$, the function $x \mapsto c \cdot f(x)$ is continuous within $s$ at $b$ if and only if $f$ is continuous within $s$ at $b$.

continuousOn_const_smul_iff₀ theorem

(hc : c ≠ 0) : ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s

Full source

theorem continuousOn_const_smul_iff₀ (hc : c ≠ 0) :
    ContinuousOnContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s :=
  continuousOn_const_smul_iff (Units.mk0 c hc)

Continuity on a Set under Nonzero Scalar Multiplication: $c \cdot f(x)$ continuous on $s$ $\leftrightarrow$ $f$ continuous on $s$ for $c \neq 0$

Informal description

For a nonzero element $c$ in a group with zero $G_0$ acting on a topological space, and for any subset $s$ of the space, the function $x \mapsto c \cdot f(x)$ is continuous on $s$ if and only if $f$ is continuous on $s$.

continuousAt_const_smul_iff₀ theorem

(hc : c ≠ 0) : ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b

Full source

theorem continuousAt_const_smul_iff₀ (hc : c ≠ 0) :
    ContinuousAtContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b :=
  continuousAt_const_smul_iff (Units.mk0 c hc)

Continuity at a Point under Nonzero Scalar Multiplication: $c \cdot f(x)$ continuous at $b$ $\leftrightarrow$ $f$ continuous at $b$ for $c \neq 0$

Informal description

For a nonzero element $c$ in a group with zero $G_0$ acting on a topological space, the function $x \mapsto c \cdot f(x)$ is continuous at a point $b$ if and only if $f$ is continuous at $b$.

continuous_const_smul_iff₀ theorem

(hc : c ≠ 0) : (Continuous fun x => c • f x) ↔ Continuous f

Full source

theorem continuous_const_smul_iff₀ (hc : c ≠ 0) : (Continuous fun x => c • f x) ↔ Continuous f :=
  continuous_const_smul_iff (Units.mk0 c hc)

Continuity of Scalar Multiplication by Nonzero Element: $(x \mapsto c \cdot f(x))$ is continuous iff $f$ is continuous

Informal description

For a nonzero element $c$ in a group with zero $G_0$ acting on a topological space, the map $x \mapsto c \cdot f(x)$ is continuous if and only if the function $f$ is continuous.

Homeomorph.smulOfNeZero definition

(c : G₀) (hc : c ≠ 0) : α ≃ₜ α

Full source

/-- Scalar multiplication by a non-zero element of a group with zero acting on `α` is a
homeomorphism from `α` onto itself. -/
@[simps! -fullyApplied apply]
protected def Homeomorph.smulOfNeZero (c : G₀) (hc : c ≠ 0) : α ≃ₜ α :=
  Homeomorph.smul (Units.mk0 c hc)

Homeomorphism induced by nonzero scalar multiplication

Informal description

For a group with zero $ G_0 $ acting on a topological space $ \alpha $, scalar multiplication by a nonzero element $ c \in G_0 $ is a homeomorphism of $ \alpha $ onto itself. The inverse of this homeomorphism is given by scalar multiplication with $ c^{-1} $.

Homeomorph.smulOfNeZero_symm_apply theorem

{c : G₀} (hc : c ≠ 0) : ⇑(Homeomorph.smulOfNeZero c hc).symm = (c⁻¹ • · : α → α)

Full source

@[simp]
theorem Homeomorph.smulOfNeZero_symm_apply {c : G₀} (hc : c ≠ 0) :
    ⇑(Homeomorph.smulOfNeZero c hc).symm = (c⁻¹ • · : α → α) :=
  rfl

Inverse of Nonzero Scalar Multiplication Homeomorphism is $x \mapsto c^{-1} \cdot x$

Informal description

For a group with zero $G_0$ acting on a topological space $\alpha$, if $c \in G_0$ is nonzero, then the inverse of the homeomorphism induced by scalar multiplication by $c$ is given by scalar multiplication with $c^{-1}$. That is, the map $(Homeomorph.smulOfNeZero\; c\; hc).symm$ equals the function $x \mapsto c^{-1} \cdot x$.

isOpenMap_smul₀ theorem

{c : G₀} (hc : c ≠ 0) : IsOpenMap fun x : α => c • x

Full source

theorem isOpenMap_smul₀ {c : G₀} (hc : c ≠ 0) : IsOpenMap fun x : α => c • x :=
  (Homeomorph.smulOfNeZero c hc).isOpenMap

Nonzero Scalar Multiplication is an Open Map

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a group with zero $G_0$, if $c \in G_0$ is nonzero, then the map $x \mapsto c \cdot x$ is an open map.

IsOpen.smul₀ theorem

{c : G₀} {s : Set α} (hs : IsOpen s) (hc : c ≠ 0) : IsOpen (c • s)

Full source

theorem IsOpen.smul₀ {c : G₀} {s : Set α} (hs : IsOpen s) (hc : c ≠ 0) : IsOpen (c • s) :=
  isOpenMap_smul₀ hc s hs

Nonzero Scalar Multiplication Preserves Open Sets

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a group with zero $G_0$, if $s \subseteq \alpha$ is an open set and $c \in G_0$ is nonzero, then the scaled set $c \cdot s$ is open.

interior_smul₀ theorem

{c : G₀} (hc : c ≠ 0) (s : Set α) : interior (c • s) = c • interior s

Full source

theorem interior_smul₀ {c : G₀} (hc : c ≠ 0) (s : Set α) : interior (c • s) = c • interior s :=
  ((Homeomorph.smulOfNeZero c hc).image_interior s).symm

Interior Commutes with Nonzero Scalar Multiplication

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a group with zero $G_0$, if $c \in G_0$ is nonzero, then the interior of the scaled set $c \cdot s$ equals the scaling of the interior of $s$, i.e., $\text{interior}(c \cdot s) = c \cdot \text{interior}(s)$ for any subset $s \subseteq \alpha$.

closure_smul₀' theorem

{c : G₀} (hc : c ≠ 0) (s : Set α) : closure (c • s) = c • closure s

Full source

theorem closure_smul₀' {c : G₀} (hc : c ≠ 0) (s : Set α) :
    closure (c • s) = c • closure s :=
  ((Homeomorph.smulOfNeZero c hc).image_closure s).symm

Closure Commutes with Nonzero Scalar Multiplication

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a group with zero $G_0$, if $c \in G_0$ is nonzero, then the closure of the scaled set $c \cdot s$ equals the scaling of the closure of $s$, i.e., $\text{closure}(c \cdot s) = c \cdot \text{closure}(s)$ for any subset $s \subseteq \alpha$.

closure_smul₀ theorem

 {E} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀)
  (s : Set E) : closure (c • s) = c • closure s

Full source

theorem closure_smul₀ {E} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E]
    [ContinuousConstSMul G₀ E] (c : G₀) (s : Set E) : closure (c • s) = c • closure s := by
  rcases eq_or_ne c 0 with (rfl | hc)
  · rcases eq_empty_or_nonempty s with (rfl | hs)
    · simp
    · rw [zero_smul_set hs, zero_smul_set hs.closure]
      exact closure_singleton
  · exact closure_smul₀' hc s

Closure Commutes with Scalar Multiplication in $T_1$ Spaces

Informal description

Let $E$ be a topological space with a zero element, equipped with a scalar multiplication action by a group with zero $G_0$. Assume $E$ is a $T_1$ space and the scalar multiplication is continuous in the second variable. Then for any $c \in G_0$ and any subset $s \subseteq E$, the closure of the scaled set $c \cdot s$ equals the scaling of the closure of $s$, i.e., $\overline{c \cdot s} = c \cdot \overline{s}$.

isClosedMap_smul_of_ne_zero theorem

{c : G₀} (hc : c ≠ 0) : IsClosedMap fun x : α => c • x

Full source

/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `isClosedMap_smul_left` in `Analysis.Normed.Module.FiniteDimension`. -/
theorem isClosedMap_smul_of_ne_zero {c : G₀} (hc : c ≠ 0) : IsClosedMap fun x : α => c • x :=
  (Homeomorph.smulOfNeZero c hc).isClosedMap

Closedness of Nonzero Scalar Multiplication

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a group with zero $G_0$, if $c \in G_0$ is nonzero, then the map $x \mapsto c \cdot x$ is a closed map on $\alpha$.

IsClosed.smul_of_ne_zero theorem

{c : G₀} {s : Set α} (hs : IsClosed s) (hc : c ≠ 0) : IsClosed (c • s)

Full source

theorem IsClosed.smul_of_ne_zero {c : G₀} {s : Set α} (hs : IsClosed s) (hc : c ≠ 0) :
    IsClosed (c • s) :=
  isClosedMap_smul_of_ne_zero hc s hs

Closedness of Scaled Sets under Nonzero Scalar Multiplication

Informal description

Let $\alpha$ be a topological space with a scalar multiplication action by a group with zero $G_0$. For any closed subset $s \subseteq \alpha$ and any nonzero element $c \in G_0$, the scaled set $c \cdot s$ is closed in $\alpha$.

isClosedMap_smul₀ theorem

 {E : Type*} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) :
  IsClosedMap fun x : E => c • x

Full source

/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `isClosedMap_smul_left` in `Analysis.Normed.Module.FiniteDimension`. -/
theorem isClosedMap_smul₀ {E : Type*} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E]
    [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) : IsClosedMap fun x : E => c • x := by
  rcases eq_or_ne c 0 with (rfl | hne)
  · simp only [zero_smul]
    exact isClosedMap_const
  · exact (Homeomorph.smulOfNeZero c hne).isClosedMap

Closedness of Scalar Multiplication by $c$ in $T_1$ Spaces with Continuous Action

Informal description

Let $E$ be a topological space with a zero element, equipped with a multiplicative action by a group with zero $G_0$ and the structure of a $T_1$ space. If scalar multiplication by any element of $G_0$ is continuous in the second variable, then for any $c \in G_0$, the map $x \mapsto c \cdot x$ is a closed map on $E$.

IsClosed.smul₀ theorem

 {E : Type*} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀)
  {s : Set E} (hs : IsClosed s) : IsClosed (c • s)

Full source

theorem IsClosed.smul₀ {E : Type*} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E]
    [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) {s : Set E} (hs : IsClosed s) :
    IsClosed (c • s) :=
  isClosedMap_smul₀ c s hs

Closedness of scaled sets under continuous scalar multiplication in $T_1$ spaces

Informal description

Let $E$ be a $T_1$ topological space with a zero element, equipped with a multiplicative action by a group with zero $G_0$ such that scalar multiplication is continuous in the second variable. For any closed subset $s \subseteq E$ and any $c \in G_0$, the scaled set $c \cdot s$ is closed in $E$.

HasCompactMulSupport.comp_smul theorem

 {β : Type*} [One β] {f : α → β} (h : HasCompactMulSupport f) {c : G₀} (hc : c ≠ 0) :
  HasCompactMulSupport fun x => f (c • x)

Full source

theorem HasCompactMulSupport.comp_smul {β : Type*} [One β] {f : α → β} (h : HasCompactMulSupport f)
    {c : G₀} (hc : c ≠ 0) : HasCompactMulSupport fun x => f (c • x) :=
  h.comp_homeomorph (Homeomorph.smulOfNeZero c hc)

Compact Multiplicative Support Preservation under Nonzero Scalar Multiplication

Informal description

Let $\alpha$ be a topological space with a scalar multiplication action by a group with zero $G_0$, and let $f : \alpha \to \beta$ be a function with compact multiplicative support, where $\beta$ has a multiplicative identity. For any nonzero $c \in G_0$, the function $x \mapsto f(c \cdot x)$ also has compact multiplicative support.

HasCompactSupport.comp_smul theorem

 {β : Type*} [Zero β] {f : α → β} (h : HasCompactSupport f) {c : G₀} (hc : c ≠ 0) : HasCompactSupport fun x => f (c • x)

Full source

theorem HasCompactSupport.comp_smul {β : Type*} [Zero β] {f : α → β} (h : HasCompactSupport f)
    {c : G₀} (hc : c ≠ 0) : HasCompactSupport fun x => f (c • x) :=
  h.comp_homeomorph (Homeomorph.smulOfNeZero c hc)

Compact Support Preservation under Nonzero Scalar Multiplication

Informal description

Let $\alpha$ be a topological space with a scalar multiplication action by a group with zero $G_0$, and let $f : \alpha \to \beta$ be a function with compact support, where $\beta$ has a zero element. For any nonzero $c \in G_0$, the function $x \mapsto f(c \cdot x)$ also has compact support.

IsUnit.tendsto_const_smul_iff theorem

 {f : β → α} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) :
  Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a)

Full source

nonrec theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) :
    TendstoTendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
  tendsto_const_smul_iff hc.unit

Equivalence of Filter Limits under Scalar Multiplication by Units

Informal description

Let $f : \beta \to \alpha$ be a function between topological spaces, and let $l$ be a filter on $\beta$. For any element $c$ in a monoid $M$ acting on $\alpha$ such that $c$ is a unit, the function $x \mapsto c \cdot f(x)$ tends to $c \cdot a$ along $l$ if and only if $f$ tends to $a$ along $l$.

IsUnit.continuousWithinAt_const_smul_iff theorem

(hc : IsUnit c) : ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b

Full source

nonrec theorem continuousWithinAt_const_smul_iff (hc : IsUnit c) :
    ContinuousWithinAtContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b :=
  continuousWithinAt_const_smul_iff hc.unit

Continuity Within a Subset under Scalar Multiplication by a Unit Element

Informal description

For any unit element $c$ in a monoid $M$ acting on a topological space $\alpha$, and for any function $f : \alpha \to \alpha$, the function $x \mapsto c \cdot f(x)$ is continuous within a subset $s$ at a point $b$ if and only if $f$ is continuous within $s$ at $b$.

IsUnit.continuousOn_const_smul_iff theorem

(hc : IsUnit c) : ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s

Full source

nonrec theorem continuousOn_const_smul_iff (hc : IsUnit c) :
    ContinuousOnContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s :=
  continuousOn_const_smul_iff hc.unit

Continuity on a Subset under Scalar Multiplication by a Unit Element

Informal description

Let $M$ be a monoid acting on a topological space $\alpha$, and let $c \in M$ be a unit element. For any function $f : \alpha \to \alpha$ and subset $s \subseteq \alpha$, the function $x \mapsto c \cdot f(x)$ is continuous on $s$ if and only if $f$ is continuous on $s$.

IsUnit.continuousAt_const_smul_iff theorem

(hc : IsUnit c) : ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b

Full source

nonrec theorem continuousAt_const_smul_iff (hc : IsUnit c) :
    ContinuousAtContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b :=
  continuousAt_const_smul_iff hc.unit

Continuity at a Point under Scalar Multiplication by a Unit Element

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a monoid $M$, if $c \in M$ is a unit (i.e., invertible), then the function $x \mapsto c \cdot x$ is continuous at a point $b$ if and only if the identity function is continuous at $b$. In other words, the map $f(x) = c \cdot x$ is continuous at $b$ precisely when $f$ itself is continuous at $b$.

IsUnit.continuous_const_smul_iff theorem

(hc : IsUnit c) : (Continuous fun x => c • f x) ↔ Continuous f

Full source

nonrec theorem continuous_const_smul_iff (hc : IsUnit c) :
    (Continuous fun x => c • f x) ↔ Continuous f :=
  continuous_const_smul_iff hc.unit

Continuity of Scalar Multiplication by a Unit Element

Informal description

For a topological space $\alpha$ with a scalar multiplication action by a monoid $M$, and an element $c \in M$ that is a unit (i.e., invertible), the map $x \mapsto c \cdot x$ is continuous if and only if the identity map is continuous. In other words, the function $f$ defined by $f(x) = c \cdot x$ is continuous precisely when the original function $f$ is continuous.

IsUnit.isOpenMap_smul theorem

(hc : IsUnit c) : IsOpenMap fun x : α => c • x

Full source

nonrec theorem isOpenMap_smul (hc : IsUnit c) : IsOpenMap fun x : α => c • x :=
  isOpenMap_smul hc.unit

Openness of Scalar Multiplication by a Unit Element

Informal description

For any topological space $\alpha$ with a scalar multiplication action by a monoid $M$, if $c \in M$ is a unit (i.e., invertible), then the map $x \mapsto c \cdot x$ is an open map. That is, for any open set $U \subseteq \alpha$, the image $c \cdot U$ is open in $\alpha$.

IsUnit.isClosedMap_smul theorem

(hc : IsUnit c) : IsClosedMap fun x : α => c • x

Full source

nonrec theorem isClosedMap_smul (hc : IsUnit c) : IsClosedMap fun x : α => c • x :=
  isClosedMap_smul hc.unit

Closedness of Scalar Multiplication by a Unit Element

Informal description

For any topological space $\alpha$ with a scalar multiplication action by a monoid $M$, if $c \in M$ is a unit (i.e., invertible), then the map $x \mapsto c \cdot x$ is a closed map. That is, the image of any closed set under this map is closed in $\alpha$.

IsUnit.smul_mem_nhds_smul_iff theorem

(hc : IsUnit c) {s : Set α} {a : α} : c • s ∈ 𝓝 (c • a) ↔ s ∈ 𝓝 a

Full source

nonrec theorem smul_mem_nhds_smul_iff (hc : IsUnit c) {s : Set α} {a : α} :
    c • s ∈ 𝓝 (c • a)c • s ∈ 𝓝 (c • a) ↔ s ∈ 𝓝 a :=
  smul_mem_nhds_smul_iff hc.unit

Neighborhood Invariance under Scalar Multiplication by a Unit: $c \cdot s \in \mathcal{N}(c \cdot a) \leftrightarrow s \in \mathcal{N}(a)$

Informal description

Let $\alpha$ be a topological space with a scalar multiplication action by a monoid $M$, and let $c \in M$ be a unit element. For any subset $s \subseteq \alpha$ and any point $a \in \alpha$, the set $c \cdot s$ is a neighborhood of $c \cdot a$ if and only if $s$ is a neighborhood of $a$.

ProperlyDiscontinuousSMul structure

(Γ : Type*) (T : Type*) [TopologicalSpace T] [SMul Γ T]

Full source

/-- Class `ProperlyDiscontinuousSMul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
`γ:Γ` move `K` to have nontrivial intersection with `L`.
-/
class ProperlyDiscontinuousSMul (Γ : Type*) (T : Type*) [TopologicalSpace T] [SMul Γ T] :
    Prop where
  /-- Given two compact sets `K` and `L`, `γ • K ∩ L` is nonempty for finitely many `γ`. -/
  finite_disjoint_inter_image :
    ∀ {K L : Set T}, IsCompact K → IsCompact L → Set.Finite { γ : Γ | (γ • ·) '' K ∩ L ≠ ∅ }

Properly Discontinuous Scalar Multiplication

Informal description

A structure `ProperlyDiscontinuousSMul Γ T` indicates that the scalar multiplication action of `Γ` on `T` is properly discontinuous. This means that for any two compact subsets `K` and `L` of `T`, there are only finitely many elements `γ ∈ Γ` such that the image of `K` under the action of `γ` has non-empty intersection with `L`.

ProperlyDiscontinuousVAdd structure

(Γ : Type*) (T : Type*) [TopologicalSpace T] [VAdd Γ T]

Full source

/-- Class `ProperlyDiscontinuousVAdd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
`γ:Γ` move `K` to have nontrivial intersection with `L`.
-/
class ProperlyDiscontinuousVAdd (Γ : Type*) (T : Type*) [TopologicalSpace T] [VAdd Γ T] :
  Prop where
  /-- Given two compact sets `K` and `L`, `γ +ᵥ K ∩ L` is nonempty for finitely many `γ`. -/
  finite_disjoint_inter_image :
    ∀ {K L : Set T}, IsCompact K → IsCompact L → Set.Finite { γ : Γ | (γ +ᵥ ·) '' K ∩ L ≠ ∅ }

Properly discontinuous additive action

Informal description

The structure `ProperlyDiscontinuousVAdd Γ T` asserts that the additive action of a group `Γ` on a topological space `T` is properly discontinuous. This means that for any pair of compact subsets `K` and `L` of `T`, there are only finitely many elements `γ ∈ Γ` such that the translated set `γ +ᵥ K` intersects `L` nontrivially.

Finite.to_properlyDiscontinuousSMul instance

[Finite Γ] : ProperlyDiscontinuousSMul Γ T

Full source

/-- A finite group action is always properly discontinuous. -/
@[to_additive "A finite group action is always properly discontinuous."]
instance (priority := 100) Finite.to_properlyDiscontinuousSMul [Finite Γ] :
    ProperlyDiscontinuousSMul Γ T where finite_disjoint_inter_image _ _ := Set.toFinite _

Finite Group Actions are Properly Discontinuous

Informal description

For any finite group $\Gamma$ acting on a topological space $T$, the scalar multiplication action is properly discontinuous.

isOpenMap_quotient_mk'_mul theorem

 [ContinuousConstSMul Γ T] :
  letI := MulAction.orbitRel Γ T
  IsOpenMap (Quotient.mk' : T → Quotient (MulAction.orbitRel Γ T))

Full source

/-- The quotient map by a group action is open, i.e. the quotient by a group action is an open
  quotient. -/
@[to_additive "The quotient map by a group action is open, i.e. the quotient by a group
action is an open quotient. "]
theorem isOpenMap_quotient_mk'_mul [ContinuousConstSMul Γ T] :
    letI := MulAction.orbitRel Γ T
    IsOpenMap (Quotient.mk' : T → Quotient (MulAction.orbitRel Γ T)) := fun U hU => by
  rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
  exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU

Openness of Quotient Map for Group Actions Continuous in the Second Variable

Informal description

Let $\Gamma$ be a group acting continuously in the second variable on a topological space $T$ (i.e., for each $\gamma \in \Gamma$, the map $x \mapsto \gamma \cdot x$ is continuous). Then the quotient map $\pi : T \to T/\Gamma$, where $T/\Gamma$ is the orbit space under the action of $\Gamma$, is an open map.

MulAction.isOpenQuotientMap_quotientMk theorem

[ContinuousConstSMul Γ T] : IsOpenQuotientMap (Quotient.mk (MulAction.orbitRel Γ T))

Full source

@[to_additive]
theorem MulAction.isOpenQuotientMap_quotientMk [ContinuousConstSMul Γ T] :
    IsOpenQuotientMap (Quotient.mk (MulAction.orbitRel Γ T)) :=
  ⟨Quot.mk_surjective, continuous_quot_mk, isOpenMap_quotient_mk'_mul⟩

Open Quotient Map for Group Actions Continuous in the Second Variable

Informal description

Let $\Gamma$ be a group acting continuously in the second variable on a topological space $T$ (i.e., for each $\gamma \in \Gamma$, the map $x \mapsto \gamma \cdot x$ is continuous). Then the quotient map $\pi : T \to T/\Gamma$, where $T/\Gamma$ is the orbit space under the action of $\Gamma$, is an open quotient map.

t2Space_of_properlyDiscontinuousSMul_of_t2Space instance

 [T2Space T] [LocallyCompactSpace T] [ContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T] :
  T2Space (Quotient (MulAction.orbitRel Γ T))

Full source

/-- The quotient by a discontinuous group action of a locally compact t2 space is t2. -/
@[to_additive "The quotient by a discontinuous group action of a locally compact t2
space is t2."]
instance (priority := 100) t2Space_of_properlyDiscontinuousSMul_of_t2Space [T2Space T]
    [LocallyCompactSpace T] [ContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T] :
    T2Space (Quotient (MulAction.orbitRel Γ T)) := by
  letI := MulAction.orbitRel Γ T
  set Q := Quotient (MulAction.orbitRel Γ T)
  rw [t2Space_iff_nhds]
  let f : T → Q := Quotient.mk'
  have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
  rintro ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀)
  show ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _
  have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm :)
  obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀
  obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀
  let bad_Γ_set := { γ : Γ | (γ • ·) '' K₀ ∩ L₀ ≠ ∅ }
  have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
  choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)
  let U₀₀ := ⋂ γ ∈ bad_Γ_set, (γ • ·) ⁻¹' u γ
  let U₀ := U₀₀ ∩ K₀
  let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ
  let V₀ := V₀₀ ∩ L₀
  have U_nhds : f '' U₀f '' U₀ ∈ 𝓝 (f x₀) := by
    refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
    exact (continuous_const_smul _).continuousAt (hu γ)
  have V_nhds : f '' V₀f '' V₀ ∈ 𝓝 (f y₀) :=
    f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => hv γ) L₀_in)
  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩
  rintro x ⟨x_in_U₀₀, x_in_K₀⟩ γ
  by_cases H : γ ∈ bad_Γ_set
  · exact fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩
  · rintro ⟨-, h'⟩
    simp only [bad_Γ_set, image_smul, Classical.not_not, mem_setOf_eq, Ne] at H
    exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩

Hausdorff Property of Quotient by Properly Discontinuous Group Action

Informal description

Let $T$ be a locally compact Hausdorff topological space with a group action by $\Gamma$ that is continuous in the second variable and properly discontinuous. Then the quotient space $T/\Gamma$ is also Hausdorff.

ContinuousConstSMul.secondCountableTopology theorem

[SecondCountableTopology T] [ContinuousConstSMul Γ T] : SecondCountableTopology (Quotient (MulAction.orbitRel Γ T))

Full source

/-- The quotient of a second countable space by a group action is second countable. -/
@[to_additive "The quotient of a second countable space by an additive group action is second
countable."]
theorem ContinuousConstSMul.secondCountableTopology [SecondCountableTopology T]
    [ContinuousConstSMul Γ T] : SecondCountableTopology (Quotient (MulAction.orbitRel Γ T)) :=
  TopologicalSpace.Quotient.secondCountableTopology isOpenMap_quotient_mk'_mul

Second Countability of Quotient by Group Action Continuous in Second Variable

Informal description

Let $T$ be a second countable topological space with a group action by $\Gamma$ that is continuous in the second variable (i.e., for each $\gamma \in \Gamma$, the map $x \mapsto \gamma \cdot x$ is continuous). Then the quotient space $T/\Gamma$ under the orbit equivalence relation is also second countable.

smul_mem_nhds_smul_iff₀ theorem

{c : G₀} {s : Set α} {x : α} (hc : c ≠ 0) : c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x

Full source

/-- Scalar multiplication by a nonzero scalar preserves neighborhoods. -/
theorem smul_mem_nhds_smul_iff₀ {c : G₀} {s : Set α} {x : α} (hc : c ≠ 0) :
    c • s ∈ 𝓝 (c • x : α)c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x :=
  smul_mem_nhds_smul_iff (Units.mk0 c hc)

Neighborhood Invariance under Nonzero Scalar Multiplication: $c \cdot s \in \mathcal{N}(c \cdot x) \leftrightarrow s \in \mathcal{N}(x)$ for $c \neq 0$

Informal description

For a group with zero $G_0$ acting on a topological space $\alpha$, a nonzero element $c \in G_0$, a set $s \subseteq \alpha$, and a point $x \in \alpha$, the set $c \cdot s$ is a neighborhood of $c \cdot x$ if and only if $s$ is a neighborhood of $x$.

set_smul_mem_nhds_zero_iff theorem

{s : Set α} {c : G₀} (hc : c ≠ 0) : c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α)

Full source

theorem set_smul_mem_nhds_zero_iff {s : Set α} {c : G₀} (hc : c ≠ 0) :
    c • s ∈ 𝓝 (0 : α)c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α) := by
  refine Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)
  rw [smul_zero]

Neighborhood of Zero Invariance under Nonzero Scalar Multiplication: $c \cdot s \in \mathcal{N}(0) \leftrightarrow s \in \mathcal{N}(0)$ for $c \neq 0$

Informal description

For a group with zero $G_0$ acting on a topological space $\alpha$, a nonzero element $c \in G_0$, and a set $s \subseteq \alpha$, the set $c \cdot s$ is a neighborhood of $0$ in $\alpha$ if and only if $s$ is a neighborhood of $0$ in $\alpha$.

Mathlib.Topology.Algebra.ConstMulAction

Main definitions

Main results

Tags