Mathlib.Topology.Algebra.Module.Basic

ContinuousSMul.of_nhds_zero theorem

 [IsTopologicalRing R] [IsTopologicalAddGroup M] (hmul : Tendsto (fun p : R × M => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0))
  (hmulleft : ∀ m : M, Tendsto (fun a : R => a • m) (𝓝 0) (𝓝 0))
  (hmulright : ∀ a : R, Tendsto (fun m : M => a • m) (𝓝 0) (𝓝 0)) : ContinuousSMul R M

Full source

theorem ContinuousSMul.of_nhds_zero [IsTopologicalRing R] [IsTopologicalAddGroup M]
    (hmul : Tendsto (fun p : R × M => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0))
    (hmulleft : ∀ m : M, Tendsto (fun a : R => a • m) (𝓝 0) (𝓝 0))
    (hmulright : ∀ a : R, Tendsto (fun m : M => a • m) (𝓝 0) (𝓝 0)) : ContinuousSMul R M where
  continuous_smul := by
    rw [← nhds_prod_eq] at hmul
    refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_ <;>
      simpa [ContinuousAt]

Joint Continuity of Scalar Multiplication via Zero Neighborhood Conditions

Informal description

Let $R$ be a topological ring and $M$ be a topological additive group. Suppose the following conditions hold: 1. The scalar multiplication operation $(a, m) \mapsto a \cdot m$ tends to $0$ as $(a, m)$ tends to $(0, 0)$ in $R \times M$. 2. For each fixed $m \in M$, the scalar multiplication $a \mapsto a \cdot m$ tends to $0$ as $a$ tends to $0$ in $R$. 3. For each fixed $a \in R$, the scalar multiplication $m \mapsto a \cdot m$ tends to $0$ as $m$ tends to $0$ in $M$. Then the scalar multiplication operation $R \times M \to M$ is jointly continuous, i.e., $M$ is a topological module over $R$.

ContinuousNeg.of_continuousConstSMul theorem

[ContinuousConstSMul R M] : ContinuousNeg M

Full source

/-- A topological module over a ring has continuous negation.

This cannot be an instance, because it would cause search for `[Module ?R M]` with unknown `R`. -/
theorem ContinuousNeg.of_continuousConstSMul [ContinuousConstSMul R M] : ContinuousNeg M where
  continuous_neg := by simpa using continuous_const_smul (T := M) (-1 : R)

Continuity of Negation in Topological Modules with Continuous Scalar Multiplication

Informal description

If a topological module $M$ over a ring $R$ has continuous scalar multiplication in the second variable (i.e., for each fixed $r \in R$, the map $m \mapsto r \cdot m$ is continuous), then the negation operation on $M$ is continuous.

Module.punctured_nhds_neBot theorem

[Nontrivial M] [NeBot (𝓝[≠] (0 : R))] [NoZeroSMulDivisors R M] (x : M) : NeBot (𝓝[≠] x)

Full source

/-- Let `R` be a topological ring such that zero is not an isolated point (e.g., a nontrivially
normed field, see `NormedField.punctured_nhds_neBot`). Let `M` be a nontrivial module over `R`
such that `c • x = 0` implies `c = 0 ∨ x = 0`. Then `M` has no isolated points. We formulate this
using `NeBot (𝓝[≠] x)`.

This lemma is not an instance because Lean would need to find `[ContinuousSMul ?m_1 M]` with
unknown `?m_1`. We register this as an instance for `R = ℝ` in `Real.punctured_nhds_module_neBot`.
One can also use `haveI := Module.punctured_nhds_neBot R M` in a proof.
-/
theorem Module.punctured_nhds_neBot [Nontrivial M] [NeBot (𝓝[≠] (0 : R))] [NoZeroSMulDivisors R M]
    (x : M) : NeBot (𝓝[≠] x) := by
  rcases exists_ne (0 : M) with ⟨y, hy⟩
  suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot
  refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)
  · convert tendsto_const_nhds.add ((@tendsto_id R _).smul_const y)
    rw [zero_smul, add_zero]
  · intro c hc
    simpa [hy] using hc

Nontriviality of Punctured Neighborhoods in Topological Modules without Zero Divisors

Informal description

Let $R$ be a topological ring where zero is not an isolated point (i.e., the punctured neighborhood filter $\mathcal{N}_{R\setminus\{0\}}(0)$ is nontrivial). Let $M$ be a nontrivial module over $R$ with no zero divisors (i.e., $c \cdot x = 0$ implies $c = 0$ or $x = 0$ for any $c \in R$ and $x \in M$). Then for any $x \in M$, the punctured neighborhood filter $\mathcal{N}_{M\setminus\{x\}}(x)$ is nontrivial.

continuousSMul_induced theorem

: @ContinuousSMul R M₁ _ u (t.induced f)

Full source

theorem continuousSMul_induced : @ContinuousSMul R M₁ _ u (t.induced f) :=
  let _ : TopologicalSpace M₁ := t.induced f
  IsInducing.continuousSMul ⟨rfl⟩ continuous_id (map_smul f _ _)

Continuity of Scalar Multiplication under Induced Topology

Informal description

Let $R$ and $M₁$ be types equipped with a scalar multiplication action of $R$ on $M₁$, and let $u$ and $t$ be topological space structures on $R$ and $M₁$ respectively. Given a function $f \colon M₁ \to M$ where $M$ has a topological space structure, the induced topology on $M₁$ via $f$ preserves the continuity of the scalar multiplication, i.e., the scalar multiplication action of $R$ on $M₁$ remains continuous with respect to the induced topology.

TopologicalSpace.IsSeparable.span theorem

 {R M : Type*} [AddCommMonoid M] [Semiring R] [Module R M] [TopologicalSpace M] [TopologicalSpace R] [SeparableSpace R]
  [ContinuousAdd M] [ContinuousSMul R M] {s : Set M} (hs : IsSeparable s) : IsSeparable (Submodule.span R s : Set M)

Full source

/-- The span of a separable subset with respect to a separable scalar ring is again separable. -/
lemma TopologicalSpace.IsSeparable.span {R M : Type*} [AddCommMonoid M] [Semiring R] [Module R M]
    [TopologicalSpace M] [TopologicalSpace R] [SeparableSpace R]
    [ContinuousAdd M] [ContinuousSMul R M] {s : Set M} (hs : IsSeparable s) :
    IsSeparable (Submodule.span R s : Set M) := by
  rw [Submodule.span_eq_iUnion_nat]
  refine .iUnion fun n ↦ .image ?_ ?_
  · have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
      apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)
    rwa [Set.univ_prod] at this
  · apply continuous_finset_sum _ (fun i _ ↦ ?_)
    exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))

Separability of the Span in Topological Modules

Informal description

Let $R$ be a separable topological semiring and $M$ a topological $R$-module with continuous addition and scalar multiplication. If a subset $s \subseteq M$ is separable, then the $R$-linear span of $s$ is also separable.

Submodule.topologicalAddGroup instance

 {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M]
  (S : Submodule R M) : IsTopologicalAddGroup S

Full source

instance topologicalAddGroup {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    [TopologicalSpace M] [IsTopologicalAddGroup M] (S : Submodule R M) : IsTopologicalAddGroup S :=
  inferInstanceAs (IsTopologicalAddGroup S.toAddSubgroup)

Submodules as Topological Additive Groups

Informal description

For any ring $R$, additive commutative group $M$ with a module structure over $R$, and topological space structure on $M$ where addition is continuous, every submodule $S$ of $M$ inherits a topological additive group structure where addition is continuous.

Submodule.mapsTo_smul_closure theorem

(s : Submodule R M) (c : R) : Set.MapsTo (c • ·) (closure s : Set M) (closure s)

Full source

theorem Submodule.mapsTo_smul_closure (s : Submodule R M) (c : R) :
    Set.MapsTo (c • ·) (closure s : Set M) (closure s) :=
  have : Set.MapsTo (c • ·) (s : Set M) s := fun _ h ↦ s.smul_mem c h
  this.closure (continuous_const_smul c)

Scalar multiplication preserves submodule closure

Informal description

Let $R$ be a ring, $M$ an $R$-module with a topological space structure, and $s$ a submodule of $M$. For any scalar $c \in R$, the scalar multiplication map $x \mapsto c \cdot x$ sends the closure of $s$ into itself. In other words, if $x$ is in the closure of $s$, then $c \cdot x$ is also in the closure of $s$.

Submodule.smul_closure_subset theorem

(s : Submodule R M) (c : R) : c • closure (s : Set M) ⊆ closure (s : Set M)

Full source

theorem Submodule.smul_closure_subset (s : Submodule R M) (c : R) :
    c • closure (s : Set M) ⊆ closure (s : Set M) :=
  (s.mapsTo_smul_closure c).image_subset

Scalar Multiplication Preserves Submodule Closure

Informal description

Let $R$ be a ring and $M$ be an $R$-module equipped with a topological space structure. For any submodule $s$ of $M$ and any scalar $c \in R$, the set obtained by scaling the closure of $s$ by $c$ is contained in the closure of $s$, i.e., $c \cdot \overline{s} \subseteq \overline{s}$.

Submodule.topologicalClosure definition

(s : Submodule R M) : Submodule R M

Full source

/-- The (topological-space) closure of a submodule of a topological `R`-module `M` is itself
a submodule. -/
def Submodule.topologicalClosure (s : Submodule R M) : Submodule R M :=
  { s.toAddSubmonoid.topologicalClosure with
    smul_mem' := s.mapsTo_smul_closure }

Topological closure of a submodule

Informal description

Given a topological module $M$ over a ring $R$ and a submodule $s$ of $M$, the topological closure of $s$ is itself a submodule of $M$. This means that the closure operation preserves the submodule structure, including closure under scalar multiplication and addition.

Submodule.topologicalClosure_coe theorem

(s : Submodule R M) : (s.topologicalClosure : Set M) = closure (s : Set M)

Full source

@[simp, norm_cast]
theorem Submodule.topologicalClosure_coe (s : Submodule R M) :
    (s.topologicalClosure : Set M) = closure (s : Set M) :=
  rfl

Equality of Submodule Closure and Set Closure in Topological Modules

Informal description

For any submodule $s$ of a topological module $M$ over a ring $R$, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$, i.e., $\overline{s} = \overline{(s : \text{Set } M)}$.

Submodule.le_topologicalClosure theorem

(s : Submodule R M) : s ≤ s.topologicalClosure

Full source

theorem Submodule.le_topologicalClosure (s : Submodule R M) : s ≤ s.topologicalClosure :=
  subset_closure

Submodule is Contained in its Topological Closure

Informal description

For any submodule $s$ of a topological module $M$ over a ring $R$, the submodule $s$ is contained in its topological closure, i.e., $s \subseteq \overline{s}$.

Submodule.closure_subset_topologicalClosure_span theorem

(s : Set M) : closure s ⊆ (span R s).topologicalClosure

Full source

theorem Submodule.closure_subset_topologicalClosure_span (s : Set M) :
    closureclosure s ⊆ (span R s).topologicalClosure := by
  rw [Submodule.topologicalClosure_coe]
  exact closure_mono subset_span

Inclusion of Set Closure in Span Closure for Topological Modules

Informal description

For any subset $s$ of a topological module $M$ over a ring $R$, the topological closure of $s$ is contained in the topological closure of the $R$-linear span of $s$, i.e., $\overline{s} \subseteq \overline{\operatorname{span}_R s}$.

Submodule.isClosed_topologicalClosure theorem

(s : Submodule R M) : IsClosed (s.topologicalClosure : Set M)

Full source

theorem Submodule.isClosed_topologicalClosure (s : Submodule R M) :
    IsClosed (s.topologicalClosure : Set M) := isClosed_closure

Topological Closure of a Submodule is Closed

Informal description

For any submodule $s$ of a topological module $M$ over a ring $R$, the topological closure $\overline{s}$ is a closed subset of $M$.

Submodule.topologicalClosure_minimal theorem

(s : Submodule R M) {t : Submodule R M} (h : s ≤ t) (ht : IsClosed (t : Set M)) : s.topologicalClosure ≤ t

Full source

theorem Submodule.topologicalClosure_minimal (s : Submodule R M) {t : Submodule R M} (h : s ≤ t)
    (ht : IsClosed (t : Set M)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Submodule Topological Closure: $\overline{s} \subseteq t$ for $s \subseteq t$ and $t$ closed

Informal description

Let $M$ be a topological module over a ring $R$, and let $s$ and $t$ be submodules of $M$ such that $s \subseteq t$. If $t$ is closed in the topological space $M$, then the topological closure of $s$ is also contained in $t$, i.e., $\overline{s} \subseteq t$.

Submodule.topologicalClosure_mono theorem

{s : Submodule R M} {t : Submodule R M} (h : s ≤ t) : s.topologicalClosure ≤ t.topologicalClosure

Full source

theorem Submodule.topologicalClosure_mono {s : Submodule R M} {t : Submodule R M} (h : s ≤ t) :
    s.topologicalClosure ≤ t.topologicalClosure :=
  closure_mono h

Monotonicity of Topological Closure for Submodules

Informal description

For any two submodules $s$ and $t$ of a topological module $M$ over a ring $R$, if $s \subseteq t$, then the topological closure of $s$ is contained in the topological closure of $t$, i.e., $\overline{s} \subseteq \overline{t}$.

IsClosed.submodule_topologicalClosure_eq theorem

{s : Submodule R M} (hs : IsClosed (s : Set M)) : s.topologicalClosure = s

Full source

/-- The topological closure of a closed submodule `s` is equal to `s`. -/
theorem IsClosed.submodule_topologicalClosure_eq {s : Submodule R M} (hs : IsClosed (s : Set M)) :
    s.topologicalClosure = s :=
  SetLike.ext' hs.closure_eq

Closure of Closed Submodule Equals Itself

Informal description

For any closed submodule $s$ of a topological module $M$ over a ring $R$, the topological closure of $s$ is equal to $s$ itself, i.e., $\overline{s} = s$.

Submodule.dense_iff_topologicalClosure_eq_top theorem

{s : Submodule R M} : Dense (s : Set M) ↔ s.topologicalClosure = ⊤

Full source

/-- A subspace is dense iff its topological closure is the entire space. -/
theorem Submodule.dense_iff_topologicalClosure_eq_top {s : Submodule R M} :
    DenseDense (s : Set M) ↔ s.topologicalClosure = ⊤ := by
  rw [← SetLike.coe_set_eq, dense_iff_closure_eq]
  simp

Density Criterion for Submodules: $\overline{s} = M$ iff $s$ is dense

Informal description

A submodule $s$ of a topological module $M$ over a ring $R$ is dense in $M$ if and only if the topological closure of $s$ is equal to the entire module $M$, i.e., $\overline{s} = M$.

Submodule.topologicalClosure.completeSpace instance

 {M' : Type*} [AddCommMonoid M'] [Module R M'] [UniformSpace M'] [ContinuousAdd M'] [ContinuousConstSMul R M']
  [CompleteSpace M'] (U : Submodule R M') : CompleteSpace U.topologicalClosure

Full source

instance Submodule.topologicalClosure.completeSpace {M' : Type*} [AddCommMonoid M'] [Module R M']
    [UniformSpace M'] [ContinuousAdd M'] [ContinuousConstSMul R M'] [CompleteSpace M']
    (U : Submodule R M') : CompleteSpace U.topologicalClosure :=
  isClosed_closure.completeSpace_coe

Completeness of Topological Closures of Submodules in Complete Topological Modules

Informal description

Let $M'$ be a topological module over a ring $R$ with a uniform space structure, continuous addition, and continuous scalar multiplication. If $M'$ is a complete uniform space, then for any submodule $U$ of $M'$, the topological closure $\overline{U}$ is also a complete uniform space.

Submodule.isClosed_or_dense_of_isCoatom theorem

(s : Submodule R M) (hs : IsCoatom s) : IsClosed (s : Set M) ∨ Dense (s : Set M)

Full source

/-- A maximal proper subspace of a topological module (i.e a `Submodule` satisfying `IsCoatom`)
is either closed or dense. -/
theorem Submodule.isClosed_or_dense_of_isCoatom (s : Submodule R M) (hs : IsCoatom s) :
    IsClosedIsClosed (s : Set M) ∨ Dense (s : Set M) := by
  refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr
  exact fun h ↦ h ▸ isClosed_closure

Maximal Proper Submodules in Topological Modules are Closed or Dense

Informal description

Let $M$ be a topological module over a ring $R$, and let $s$ be a maximal proper submodule of $M$ (i.e., $s$ is a coatom in the lattice of submodules). Then $s$ is either closed or dense in $M$.

Submodule.closure_coe_iSup_map_single theorem

 (s : ∀ i, Submodule R (M i)) :
  closure (↑(⨆ i, (s i).map (LinearMap.single R M i)) : Set (∀ i, M i)) = Set.univ.pi fun i ↦ closure (s i)

Full source

/-- If `s i` is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.

In case of a finite index type, this statement immediately follows from `Submodule.iSup_map_single`.
However, the statement is true for an infinite index type as well. -/
theorem closure_coe_iSup_map_single (s : ∀ i, Submodule R (M i)) :
    closure (↑(⨆ i, (s i).map (LinearMap.single R M i)) : Set (∀ i, M i)) =
      Set.univ.pi fun i ↦ closure (s i) := by
  rw [← closure_pi_set]
  refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure
  · exact SetLike.coe_mono <| iSup_map_single_le
  · simp only [Set.subset_def, mem_closure_iff]
    intro x hx U hU hxU
    rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
    refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
    · simp_all [Finset.sum_pi_single]
    · exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Closure of Span of Single Maps Equals Product of Closures in Indexed Modules

Informal description

Let $\{M_i\}_{i \in \iota}$ be a family of $R$-modules, and for each $i \in \iota$, let $s_i$ be a submodule of $M_i$. The closure of the span of the images of the submodules $s_i$ under the linear maps $\text{single}_i : M_i \to \prod_{j \in \iota} M_j$ is equal to the product of the closures of the submodules $s_i$ in their respective modules. That is, \[ \overline{\bigcup_i \text{span}(\text{single}_i(s_i))} = \prod_{i \in \iota} \overline{s_i}. \]

Submodule.topologicalClosure_iSup_map_single theorem

 [∀ i, ContinuousAdd (M i)] [∀ i, ContinuousConstSMul R (M i)] (s : ∀ i, Submodule R (M i)) :
  topologicalClosure (⨆ i, (s i).map (LinearMap.single R M i)) = pi Set.univ fun i ↦ (s i).topologicalClosure

Full source

/-- If `s i` is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.

In case of a finite index type, this statement immediately follows from `Submodule.iSup_map_single`.
However, the statement is true for an infinite index type as well.

This version is stated in terms of `Submodule.topologicalClosure`,
thus assumes that `M i`s are topological modules over `R`.
However, the statement is true without assuming continuity of the operations,
see `Submodule.closure_coe_iSup_map_single` above. -/
theorem topologicalClosure_iSup_map_single [∀ i, ContinuousAdd (M i)]
    [∀ i, ContinuousConstSMul R (M i)] (s : ∀ i, Submodule R (M i)) :
    topologicalClosure (⨆ i, (s i).map (LinearMap.single R M i)) =
      pi Set.univ fun i ↦ (s i).topologicalClosure :=
  SetLike.coe_injective <| closure_coe_iSup_map_single _

Closure of Span of Single Maps Equals Product of Closures in Topological Modules

Informal description

Let $\{M_i\}_{i \in \iota}$ be a family of topological $R$-modules with continuous addition and continuous scalar multiplication in the second variable. For each $i \in \iota$, let $s_i$ be a submodule of $M_i$. Then the topological closure of the span of the images of the submodules $s_i$ under the linear maps $\text{single}_i : M_i \to \prod_{j \in \iota} M_j$ equals the product of the topological closures of the submodules $s_i$ in their respective modules. That is, \[ \overline{\bigsqcup_i \text{span}(\text{single}_i(s_i))} = \prod_{i \in \iota} \overline{s_i}. \]

LinearMap.continuous_on_pi theorem

 {ι : Type*} {R : Type*} {M : Type*} [Finite ι] [Semiring R] [TopologicalSpace R] [AddCommMonoid M] [Module R M]
  [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] (f : (ι → R) →ₗ[R] M) : Continuous f

Full source

theorem LinearMap.continuous_on_pi {ι : Type*} {R : Type*} {M : Type*} [Finite ι] [Semiring R]
    [TopologicalSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M]
    [ContinuousSMul R M] (f : (ι → R) →ₗ[R] M) : Continuous f := by
  cases nonempty_fintype ι
  classical
    -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
    -- function.
    have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
      ext x
      exact f.pi_apply_eq_sum_univ x
    rw [this]
    refine continuous_finset_sum _ fun i _ => ?_
    exact (continuous_apply i).smul continuous_const

Continuity of Linear Maps on Finite-Dimensional Product Spaces

Informal description

Let $\iota$ be a finite type, $R$ a topological semiring, and $M$ a topological $R$-module with continuous addition and scalar multiplication. Then every linear map $f \colon (\iota \to R) \to M$ is continuous.

linearMapOfMemClosureRangeCoe definition

 (f : M₁ → M₂) (hf : f ∈ closure (Set.range ((↑) : (M₁ →ₛₗ[σ] M₂) → M₁ → M₂))) : M₁ →ₛₗ[σ] M₂

Full source

/-- Constructs a bundled linear map from a function and a proof that this function belongs to the
closure of the set of linear maps. -/
@[simps -fullyApplied]
def linearMapOfMemClosureRangeCoe (f : M₁ → M₂)
    (hf : f ∈ closure (Set.range ((↑) : (M₁ →ₛₗ[σ] M₂) → M₁ → M₂))) : M₁ →ₛₗ[σ] M₂ :=
  { addMonoidHomOfMemClosureRangeCoe f hf with
    map_smul' := (isClosed_setOf_map_smul M₁ M₂ σ).closure_subset_iff.2
      (Set.range_subset_iff.2 LinearMap.map_smulₛₗ) hf }

Linear map constructed from a function in the closure of linear maps

Informal description

Given a function $ f \colon M_1 \to M_2 $ that lies in the topological closure of the range of the canonical embedding of linear maps (from $ M_1 $ to $ M_2 $ with respect to a ring homomorphism $ \sigma $), this constructs a bundled linear map from $ f $. The linearity is ensured by the fact that the set of functions respecting scalar multiplication is closed, and $ f $ inherits this property by being in the closure.

linearMapOfTendsto definition

 (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [l.NeBot] (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →ₛₗ[σ] M₂

Full source

/-- Construct a bundled linear map from a pointwise limit of linear maps -/
@[simps! -fullyApplied]
def linearMapOfTendsto (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [l.NeBot]
    (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →ₛₗ[σ] M₂ :=
  linearMapOfMemClosureRangeCoe f <|
    mem_closure_of_tendsto h <| Eventually.of_forall fun _ => Set.mem_range_self _

Linear map constructed from pointwise limit of linear maps

Informal description

Given a function $ f \colon M_1 \to M_2 $ and a net $ g \colon \alpha \to (M_1 \to_{σ} M_2) $ of linear maps (with respect to a ring homomorphism $ \sigma $), if the net $ g $ converges pointwise to $ f $, then $ f $ is itself a linear map. Here, $ l $ is a non-trivial filter on the index type $ \alpha $, and the convergence is in the sense of the neighborhood filter of $ f $.

LinearMap.isClosed_range_coe theorem

: IsClosed (Set.range ((↑) : (M₁ →ₛₗ[σ] M₂) → M₁ → M₂))

Full source

theorem LinearMap.isClosed_range_coe : IsClosed (Set.range ((↑) : (M₁ →ₛₗ[σ] M₂) → M₁ → M₂)) :=
  isClosed_of_closure_subset fun f hf => ⟨linearMapOfMemClosureRangeCoe f hf, rfl⟩

Closedness of the Range of Linear Maps in Function Space

Informal description

The range of the canonical embedding from the space of linear maps $M_1 \to_{\sigma} M_2$ (with respect to a ring homomorphism $\sigma$) to the space of all functions $M_1 \to M_2$ is a closed subset in the function space equipped with the topology of pointwise convergence.

QuotientModule.Quotient.topologicalSpace instance

: TopologicalSpace (M ⧸ S)

Full source

instance _root_.QuotientModule.Quotient.topologicalSpace : TopologicalSpace (M ⧸ S) :=
  inferInstanceAs (TopologicalSpace (Quotient S.quotientRel))

Topology on Quotient Modules

Informal description

For any module $M$ over a ring $R$ and any submodule $S$ of $M$, the quotient module $M ⧸ S$ is equipped with a canonical topological space structure inherited from $M$.

Submodule.isOpenMap_mkQ theorem

[ContinuousAdd M] : IsOpenMap S.mkQ

Full source

theorem isOpenMap_mkQ [ContinuousAdd M] : IsOpenMap S.mkQ :=
  QuotientAddGroup.isOpenMap_coe

Quotient map of topological module is open

Informal description

Let $M$ be a topological module with continuous addition and $S$ a submodule of $M$. Then the quotient map $\pi : M \to M/S$ is an open map.

Submodule.isOpenQuotientMap_mkQ theorem

[ContinuousAdd M] : IsOpenQuotientMap S.mkQ

Full source

theorem isOpenQuotientMap_mkQ [ContinuousAdd M] : IsOpenQuotientMap S.mkQ :=
  QuotientAddGroup.isOpenQuotientMap_mk

Open Quotient Map Property of Module Quotients

Informal description

Let $M$ be a topological module with continuous addition. For any submodule $S$ of $M$, the canonical quotient map $M \to M/S$ is an open quotient map.

Submodule.topologicalAddGroup_quotient instance

[IsTopologicalAddGroup M] : IsTopologicalAddGroup (M ⧸ S)

Full source

instance topologicalAddGroup_quotient [IsTopologicalAddGroup M] : IsTopologicalAddGroup (M ⧸ S) :=
  inferInstanceAs <| IsTopologicalAddGroup (M ⧸ S.toAddSubgroup)

Quotient of a Topological Additive Group is a Topological Additive Group

Informal description

For any topological additive group $M$ and a submodule $S$ of $M$, the quotient $M ⧸ S$ is also a topological additive group.

Submodule.continuousSMul_quotient instance

[TopologicalSpace R] [IsTopologicalAddGroup M] [ContinuousSMul R M] : ContinuousSMul R (M ⧸ S)

Full source

instance continuousSMul_quotient [TopologicalSpace R] [IsTopologicalAddGroup M]
    [ContinuousSMul R M] : ContinuousSMul R (M ⧸ S) where
  continuous_smul := by
    rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]
    exact continuous_quot_mk.comp continuous_smul

Continuous Scalar Multiplication on Quotient Modules

Informal description

For any topological ring $R$, topological module $M$ over $R$ with continuous scalar multiplication, and submodule $S$ of $M$, the quotient module $M ⧸ S$ inherits a continuous scalar multiplication structure from $M$.

Submodule.t3_quotient_of_isClosed instance

[IsTopologicalAddGroup M] [IsClosed (S : Set M)] : T3Space (M ⧸ S)

Full source

instance t3_quotient_of_isClosed [IsTopologicalAddGroup M] [IsClosed (S : Set M)] :
    T3Space (M ⧸ S) :=
  letI : IsClosed (S.toAddSubgroup : Set M) := ‹_›
  QuotientAddGroup.instT3Space S.toAddSubgroup

Quotient of a Topological Additive Group by a Closed Submodule is $T_3$

Informal description

For any topological additive group $M$ and a closed submodule $S$ of $M$, the quotient space $M ⧸ S$ is a $T_3$ space (regular and $T_0$).