Mathlib.Topology.Algebra.Module.StrongTopology

UniformConvergenceCLM definition

[TopologicalSpace F] (_ : Set (Set E))

Full source

/-- Given `E` and `F` two topological vector spaces and `𝔖 : Set (Set E)`, then
`UniformConvergenceCLM σ F 𝔖` is a type synonym of `E →SL[σ] F` equipped with the "topology of
uniform convergence on the elements of `𝔖`".

If the continuous linear image of any element of `𝔖` is bounded, this makes `E →SL[σ] F` a
topological vector space. -/
@[nolint unusedArguments]
def UniformConvergenceCLM [TopologicalSpace F] (_ : Set (Set E)) := E →SL[σ] F

Topology of uniform convergence on $\mathfrak{S}$ for continuous semilinear maps

Informal description

Given two topological vector spaces $E$ and $F$ over a field with a ring homomorphism $\sigma$, and a family $\mathfrak{S}$ of subsets of $E$, the type `UniformConvergenceCLM σ F 𝔖` is a type synonym for the space of continuous $\sigma$-semilinear maps from $E$ to $F$, equipped with the topology of uniform convergence on the elements of $\mathfrak{S}$. This topology makes $E \to_{SL[\sigma]} F$ a topological vector space when the continuous linear image of any element of $\mathfrak{S}$ is bounded.

UniformConvergenceCLM.instFunLike instance

[TopologicalSpace F] (𝔖 : Set (Set E)) : FunLike (UniformConvergenceCLM σ F 𝔖) E F

Full source

instance instFunLike [TopologicalSpace F] (𝔖 : Set (Set E)) :
    FunLike (UniformConvergenceCLM σ F 𝔖) E F :=
  ContinuousLinearMap.funLike

Function-Like Structure on Uniformly Convergent Continuous Semilinear Maps

Informal description

For any topological space $F$ and any family $\mathfrak{S}$ of subsets of $E$, the type `UniformConvergenceCLM σ F 𝔖` of continuous $\sigma$-semilinear maps from $E$ to $F$ with the topology of uniform convergence on $\mathfrak{S}$ has a function-like structure, where each map can be treated as a function from $E$ to $F$.

UniformConvergenceCLM.instContinuousSemilinearMapClass instance

[TopologicalSpace F] (𝔖 : Set (Set E)) : ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F

Full source

instance instContinuousSemilinearMapClass [TopologicalSpace F] (𝔖 : Set (Set E)) :
    ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F :=
  ContinuousLinearMap.continuousSemilinearMapClass

Continuous Semilinear Maps with Uniform Convergence Topology

Informal description

For any topological space $F$ and any family $\mathfrak{S}$ of subsets of $E$, the type `UniformConvergenceCLM σ F 𝔖` of continuous $\sigma$-semilinear maps from $E$ to $F$ with the topology of uniform convergence on $\mathfrak{S}$ forms a class of continuous semilinear maps. This means each map in this type is both $\sigma$-semilinear (i.e., additive and satisfies $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in R$ and $x \in E$) and continuous with respect to the given topologies on $E$ and $F$.

UniformConvergenceCLM.instTopologicalSpace instance

 [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalSpace (UniformConvergenceCLM σ F 𝔖)

Full source

instance instTopologicalSpace [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    TopologicalSpace (UniformConvergenceCLM σ F 𝔖) :=
  (@UniformOnFun.topologicalSpace E F (IsTopologicalAddGroup.toUniformSpace F) 𝔖).induced
    (DFunLike.coe : (UniformConvergenceCLM σ F 𝔖) → (E →ᵤ[𝔖] F))

Topology of Uniform Convergence on $\mathfrak{S}$ for Continuous Semilinear Maps

Informal description

Given a topological space $F$ that is also a topological additive group, and a family $\mathfrak{S}$ of subsets of $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ forms a topological space. This topology is defined by requiring that a net of maps converges if and only if it converges uniformly on each subset in $\mathfrak{S}$.

UniformConvergenceCLM.topologicalSpace_eq theorem

 [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
  instTopologicalSpace σ F 𝔖 =
    TopologicalSpace.induced (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

Full source

theorem topologicalSpace_eq [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced (UniformOnFun.ofFunUniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)
      (UniformOnFun.topologicalSpace E F 𝔖) := by
  rw [instTopologicalSpace]
  congr
  exact IsUniformAddGroup.toUniformSpace_eq

Equality of Topologies for Uniform $\mathfrak{S}$-Convergence on Continuous Semilinear Maps

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a uniform space structure making it a uniform additive group. For any family $\mathfrak{S}$ of subsets of $E$, the topology on the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ with uniform convergence on $\mathfrak{S}$ is equal to the topology induced by the canonical embedding into the space of functions $E \to F$ equipped with the topology of uniform convergence on $\mathfrak{S}$.

UniformConvergenceCLM.instUniformSpace instance

[UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : UniformSpace (UniformConvergenceCLM σ F 𝔖)

Full source

/-- The uniform structure associated with `ContinuousLinearMap.strongTopology`. We make sure
that this has nice definitional properties. -/
instance instUniformSpace [UniformSpace F] [IsUniformAddGroup F]
    (𝔖 : Set (Set E)) : UniformSpace (UniformConvergenceCLM σ F 𝔖) :=
  UniformSpace.replaceTopology
    ((UniformOnFun.uniformSpace E F 𝔖).comap (UniformOnFun.ofFunUniformOnFun.ofFun 𝔖 ∘ DFunLike.coe))
    (by rw [UniformConvergenceCLM.instTopologicalSpace, IsUniformAddGroup.toUniformSpace_eq]; rfl)

Uniform Space Structure on Continuous Semilinear Maps with Uniform $\mathfrak{S}$-Convergence

Informal description

For any uniform space $F$ that is also a uniform additive group, and any family $\mathfrak{S}$ of subsets of $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ forms a uniform space. This uniform structure is defined by pulling back the uniform structure of $\mathfrak{S}$-convergence from the space of functions $E \to F$ via the canonical embedding.

UniformConvergenceCLM.uniformSpace_eq theorem

 [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
  instUniformSpace σ F 𝔖 = UniformSpace.comap (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)

Full source

theorem uniformSpace_eq [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    instUniformSpace σ F 𝔖 =
      UniformSpace.comap (UniformOnFun.ofFunUniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)
        (UniformOnFun.uniformSpace E F 𝔖) := by
  rw [instUniformSpace, UniformSpace.replaceTopology_eq]

Uniform Space Structure Equality for Continuous Semilinear Maps with $\mathfrak{S}$-Convergence

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a uniform space structure making it a uniform additive group. For any family $\mathfrak{S}$ of subsets of $E$, the uniform space structure on the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ with uniform convergence on $\mathfrak{S}$ is equal to the pullback of the uniform structure of $\mathfrak{S}$-convergence on the function space $E \to F$ via the canonical embedding map.

UniformConvergenceCLM.uniformity_toTopologicalSpace_eq theorem

 [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
  (UniformConvergenceCLM.instUniformSpace σ F 𝔖).toTopologicalSpace = UniformConvergenceCLM.instTopologicalSpace σ F 𝔖

Full source

@[simp]
theorem uniformity_toTopologicalSpace_eq [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    (UniformConvergenceCLM.instUniformSpace σ F 𝔖).toTopologicalSpace =
      UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 :=
  rfl

Equality of Topologies Induced by Uniform $\mathfrak{S}$-Convergence and $\mathfrak{S}$-Topology on Continuous Semilinear Maps

Informal description

Let $F$ be a uniform space that is also a uniform additive group, and let $\mathfrak{S}$ be a family of subsets of $E$. Then the topology induced by the uniformity of $\mathfrak{S}$-convergence on the space of continuous $\sigma$-semilinear maps from $E$ to $F$ coincides with the $\mathfrak{S}$-topology.

UniformConvergenceCLM.isUniformInducing_coeFn theorem

 [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
  IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)

Full source

theorem isUniformInducing_coeFn [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFunUniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
  ⟨rfl⟩

Uniform Inducing Property of the Canonical Embedding for Continuous Semilinear Maps with $\mathfrak{S}$-Convergence

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a uniform space structure that makes it a uniform additive group. Given a family $\mathfrak{S}$ of subsets of $E$, the canonical embedding of the space of continuous $\sigma$-semilinear maps $\text{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}$ into the space of functions $E \to_{\mathfrak{S}} F$ with the uniform $\mathfrak{S}$-convergence topology is a uniform inducing map. In other words, the uniformity on $\text{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}$ is the pullback of the uniformity on $E \to_{\mathfrak{S}} F$ under the composition of the coefficient function $\text{DFunLike.coe}$ and the uniform convergence embedding $\text{UniformOnFun.ofFun} \mathfrak{S}$.

UniformConvergenceCLM.isUniformEmbedding_coeFn theorem

 [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
  IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)

Full source

theorem isUniformEmbedding_coeFn [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFunUniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
  ⟨isUniformInducing_coeFn .., DFunLike.coe_injective⟩

Uniform Embedding Property of the Canonical Map for Continuous Semilinear Maps with $\mathfrak{S}$-Convergence

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a uniform space structure that makes it a uniform additive group. Given a family $\mathfrak{S}$ of subsets of $E$, the canonical embedding of the space of continuous $\sigma$-semilinear maps $\text{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}$ into the space of functions $E \to_{\mathfrak{S}} F$ with the uniform $\mathfrak{S}$-convergence topology is a uniform embedding. In other words, the map is injective, uniformly continuous, and the uniformity on $\text{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}$ is induced by the uniformity on $E \to_{\mathfrak{S}} F$ via the composition of the coefficient function and the uniform convergence embedding.

UniformConvergenceCLM.isEmbedding_coeFn theorem

 [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
  IsEmbedding (X := UniformConvergenceCLM σ F 𝔖) (Y := E →ᵤ[𝔖] F) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)

Full source

theorem isEmbedding_coeFn [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsEmbedding (X := UniformConvergenceCLM σ F 𝔖) (Y := E →ᵤ[𝔖] F)
      (UniformOnFun.ofFunUniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
  IsUniformEmbedding.isEmbedding (isUniformEmbedding_coeFn _ _ _)

Topological Embedding Property of the Canonical Map for Continuous Semilinear Maps with $\mathfrak{S}$-Convergence

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a uniform space structure that makes it a uniform additive group. Given a family $\mathfrak{S}$ of subsets of $E$, the canonical embedding of the space of continuous $\sigma$-semilinear maps $\text{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}$ into the space of functions $E \to_{\mathfrak{S}} F$ with the uniform $\mathfrak{S}$-convergence topology is a topological embedding. In other words, the map is injective, continuous, and the topology on $\text{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}$ is the coarsest topology that makes this map continuous.

UniformConvergenceCLM.instAddCommGroup instance

[TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : AddCommGroup (UniformConvergenceCLM σ F 𝔖)

Full source

instance instAddCommGroup [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    AddCommGroup (UniformConvergenceCLM σ F 𝔖) := ContinuousLinearMap.addCommGroup

Additive Commutative Group Structure on Continuous Semilinear Maps with Uniform Convergence Topology

Informal description

For any topological space $F$ that is an additive topological group, and any family $\mathfrak{S}$ of subsets of $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ forms an additive commutative group under pointwise addition and negation.

UniformConvergenceCLM.coe_zero theorem

[TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : ⇑(0 : UniformConvergenceCLM σ F 𝔖) = 0

Full source

@[simp]
theorem coe_zero [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    ⇑(0 : UniformConvergenceCLM σ F 𝔖) = 0 :=
  rfl

Zero Element in Uniformly Convergent Continuous Semilinear Maps is Zero Function

Informal description

For any topological space $F$ that is an additive topological group, and any family $\mathfrak{S}$ of subsets of $E$, the zero element in the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ corresponds to the zero function from $E$ to $F$.

UniformConvergenceCLM.instIsUniformAddGroup instance

[UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖)

Full source

instance instIsUniformAddGroup [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖) := by
  let φ : (UniformConvergenceCLM σ F 𝔖) →+ E →ᵤ[𝔖] F :=
    ⟨⟨(DFunLike.coe : (UniformConvergenceCLM σ F 𝔖) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩
  exact (isUniformEmbedding_coeFn _ _ _).isUniformAddGroup φ

Uniform Additive Group Structure on Continuous Semilinear Maps with Uniform $\mathfrak{S}$-Convergence

Informal description

For any uniform space $F$ that is also a uniform additive group, and any family $\mathfrak{S}$ of subsets of $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ forms a uniform additive group. This means that the addition and negation operations are uniformly continuous with respect to the uniform structure induced by $\mathfrak{S}$-convergence.

UniformConvergenceCLM.instIsTopologicalAddGroup instance

 [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖)

Full source

instance instIsTopologicalAddGroup [TopologicalSpace F] [IsTopologicalAddGroup F]
    (𝔖 : Set (Set E)) : IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖) := by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  infer_instance

Topological Additive Group Structure on Uniformly Convergent Continuous Semilinear Maps

Informal description

For any topological space $F$ that is an additive topological group, and any family $\mathfrak{S}$ of subsets of $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ forms a topological additive group. This means that the pointwise addition and negation operations are continuous with respect to this topology.

UniformConvergenceCLM.continuousEvalConst theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) :
  ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F

Full source

theorem continuousEvalConst [TopologicalSpace F] [IsTopologicalAddGroup F]
    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) :
    ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F where
  continuous_eval_const x := by
    letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
    haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
    exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp
      (isEmbedding_coeFn σ F 𝔖).continuous

Continuity of Point Evaluation for Continuous Semilinear Maps with Uniform $\mathfrak{S}$-Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces, where $F$ is a topological additive group, and let $\mathfrak{S}$ be a family of subsets of $E$ whose union covers $E$ (i.e., $\bigcup_{S \in \mathfrak{S}} S = E$). Then for any fixed $x \in E$, the evaluation map $\text{eval}_x : \text{UniformConvergenceCLM}_\sigma F \mathfrak{S} \to F$ given by $f \mapsto f(x)$ is continuous, where $\text{UniformConvergenceCLM}_\sigma F \mathfrak{S}$ is the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$.

UniformConvergenceCLM.t2Space theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) :
  T2Space (UniformConvergenceCLM σ F 𝔖)

Full source

theorem t2Space [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F]
    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) := by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
  exact (isEmbedding_coeFn σ F 𝔖).t2Space

Hausdorff Property for Space of Continuous Semilinear Maps with Uniform $\mathfrak{S}$-Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is a Hausdorff topological additive group. Given a family $\mathfrak{S}$ of subsets of $E$ whose union covers $E$ (i.e., $\bigcup_{S \in \mathfrak{S}} S = E$), the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ is a Hausdorff space.

UniformConvergenceCLM.instDistribMulAction instance

 (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : DistribMulAction M (UniformConvergenceCLM σ F 𝔖)

Full source

instance instDistribMulAction (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
    [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
    DistribMulAction M (UniformConvergenceCLM σ F 𝔖) := ContinuousLinearMap.distribMulAction

Distributive Monoid Action on Continuous Semilinear Maps with Uniform Convergence Topology

Informal description

For any monoid $M$ acting distributively on a topological vector space $F$ over $\Bbbk_2$, with the action commuting with the scalar multiplication by $\Bbbk_2$ and continuous in the second variable, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on a family $\mathfrak{S}$ of subsets of $E$ inherits a distributive multiplicative action by $M$. This means that for any $m \in M$ and any continuous $\sigma$-semilinear map $f$, the map $m \cdot f$ defined by $(m \cdot f)(x) = m \cdot (f(x))$ is also continuous and $\sigma$-semilinear, and the action satisfies the distributive laws: 1. $m \cdot (f + g) = m \cdot f + m \cdot g$ 2. $(m_1 + m_2) \cdot f = m_1 \cdot f + m_2 \cdot f$ (when $M$ is additive) 3. $m_1 \cdot (m_2 \cdot f) = (m_1 * m_2) \cdot f$ 4. $1 \cdot f = f$

UniformConvergenceCLM.instModule instance

 (R : Type*) [Semiring R] [Module R F] [SMulCommClass 𝕜₂ R F] [TopologicalSpace F] [ContinuousConstSMul R F]
  [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : Module R (UniformConvergenceCLM σ F 𝔖)

Full source

instance instModule (R : Type*) [Semiring R] [Module R F] [SMulCommClass 𝕜₂ R F]
    [TopologicalSpace F] [ContinuousConstSMul R F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    Module R (UniformConvergenceCLM σ F 𝔖) := ContinuousLinearMap.module

Module Structure on Continuous Semilinear Maps with Uniform Convergence Topology

Informal description

For any semiring $R$, topological space $F$ with a module structure over $R$ and compatible scalar multiplication with $\mathbb{K}_2$, and any family $\mathfrak{S}$ of subsets of $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ forms a module over $R$ under pointwise operations.

UniformConvergenceCLM.continuousSMul theorem

 [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F]
  (𝔖 : Set (Set E)) (h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S) : ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Full source

theorem continuousSMul [RingHomSurjective σ] [RingHomIsometric σ]
    [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] (𝔖 : Set (Set E))
    (h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S) :
    ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖) := by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  let φ : (UniformConvergenceCLM σ F 𝔖) →ₗ[𝕜₂] E → F :=
    ⟨⟨DFunLike.coe, fun _ _ => rfl⟩, fun _ _ => rfl⟩
  exact UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (UniformConvergenceCLM σ F 𝔖) φ
    ⟨rfl⟩ fun u s hs => (h𝔖₃ s hs).image u

Continuous Scalar Multiplication in the Topology of Uniform Convergence on Bounded Sets

Informal description

Let $\mathbb{K}_1$ and $\mathbb{K}_2$ be normed fields, and let $\sigma \colon \mathbb{K}_1 \to \mathbb{K}_2$ be a surjective and isometric ring homomorphism. Let $E$ be a topological vector space over $\mathbb{K}_1$ and $F$ a topological vector space over $\mathbb{K}_2$ that is also a topological additive group with continuous scalar multiplication. Given a family $\mathfrak{S}$ of subsets of $E$ such that every $S \in \mathfrak{S}$ is von Neumann bounded in $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ has continuous scalar multiplication by $\mathbb{K}_2$.

UniformConvergenceCLM.hasBasis_nhds_zero_of_basis theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type*} (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty)
  (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
  (𝓝 (0 : UniformConvergenceCLM σ F 𝔖)).HasBasis (fun Si : Set E × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
    {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

Full source

theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F]
    {ι : Type*} (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop}
    {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
    (𝓝 (0 : UniformConvergenceCLM σ F 𝔖)).HasBasis
      (fun Si : SetSet E × ι => Si.1 ∈ 𝔖Si.1 ∈ 𝔖 ∧ p Si.2)
      fun Si => { f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2 } := by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap]
  exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap DFunLike.coe

Basis for Zero Neighborhoods in Space of Continuous Semilinear Maps with Uniform $\mathfrak{S}$-Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$ a ring homomorphism. Let $\mathfrak{S}$ be a nonempty family of subsets of $E$ that is directed under inclusion. Suppose the neighborhood filter $\mathcal{N}_0$ of $0$ in $F$ has a basis $\{b_i \mid p i\}$ indexed by $\iota$. Then the neighborhood filter $\mathcal{N}_0$ of $0$ in the space of continuous $\sigma$-semilinear maps $E \to F$ with the topology of uniform convergence on $\mathfrak{S}$ has a basis consisting of sets of the form $$\{f : E \to_{SL[\sigma]} F \mid \forall x \in S, f(x) \in b_i\}$$ for $S \in \mathfrak{S}$ and $i \in \iota$ with $p i$.

UniformConvergenceCLM.hasBasis_nhds_zero theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
  (𝓝 (0 : UniformConvergenceCLM σ F 𝔖)).HasBasis (fun SV : Set E × Set F => SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 0 : Filter F))
    fun SV => {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ SV.1, f x ∈ SV.2}

Full source

theorem hasBasis_nhds_zero [TopologicalSpace F] [IsTopologicalAddGroup F]
    (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
    (𝓝 (0 : UniformConvergenceCLM σ F 𝔖)).HasBasis
      (fun SV : SetSet E × Set F => SV.1 ∈ 𝔖SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 0 : Filter F)) fun SV =>
      { f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ SV.1, f x ∈ SV.2 } :=
  hasBasis_nhds_zero_of_basis σ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets

Basis for Zero Neighborhoods in Space of Continuous Semilinear Maps with Uniform $\mathfrak{S}$-Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces, with $F$ being a topological additive group. Given a nonempty family $\mathfrak{S}$ of subsets of $E$ that is directed under inclusion, the neighborhood filter $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ has a basis consisting of sets of the form $$\{f : E \to_{SL[\sigma]} F \mid \forall x \in S, f(x) \in V\}$$ where $S \in \mathfrak{S}$ and $V$ is a neighborhood of $0$ in $F$.

UniformConvergenceCLM.nhds_zero_eq_of_basis theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) {ι : Type*} {p : ι → Prop} {b : ι → Set F}
  (h : (𝓝 0 : Filter F).HasBasis p b) :
  𝓝 (0 : UniformConvergenceCLM σ F 𝔖) =
    ⨅ (s : Set E) (_ : s ∈ 𝔖) (i : ι) (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s (b i)}

Full source

theorem nhds_zero_eq_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E))
    {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
    𝓝 (0 : UniformConvergenceCLM σ F 𝔖) =
      ⨅ (s : Set E) (_ : s ∈ 𝔖) (i : ι) (_ : p i),
        𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s (b i)} := by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap,
    UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero]
  simp [MapsTo]

Neighborhood Filter of Zero in $\mathfrak{S}$-Convergence Topology via Basis

Informal description

Let $F$ be a topological space and a topological additive group, and let $\mathfrak{S}$ be a family of subsets of $E$. Suppose the neighborhood filter $\mathcal{N}(0)$ of $0$ in $F$ has a basis $\{b_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the neighborhood filter $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ is given by: \[ \mathcal{N}(0) = \bigsqcap_{s \in \mathfrak{S}} \bigsqcap_{i \in \iota, p(i)} \mathcal{P}\{f \mid \forall x \in s, f(x) \in b_i\}, \] where $\mathcal{P}$ denotes the principal filter.

UniformConvergenceCLM.nhds_zero_eq theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
  𝓝 (0 : UniformConvergenceCLM σ F 𝔖) = ⨅ s ∈ 𝔖, ⨅ t ∈ 𝓝 (0 : F), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s t}

Full source

theorem nhds_zero_eq [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    𝓝 (0 : UniformConvergenceCLM σ F 𝔖) =
      ⨅ s ∈ 𝔖, ⨅ t ∈ 𝓝 (0 : F),
        𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s t} :=
  nhds_zero_eq_of_basis _ _ _ (𝓝 0).basis_sets

Neighborhood Filter of Zero in $\mathfrak{S}$-Convergence Topology

Informal description

Let $F$ be a topological space that is also a topological additive group, and let $\mathfrak{S}$ be a family of subsets of $E$. The neighborhood filter $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ is given by: \[ \mathcal{N}(0) = \bigsqcap_{s \in \mathfrak{S}} \bigsqcap_{t \in \mathcal{N}(0)} \mathcal{P}\{f \mid \forall x \in s, f(x) \in t\}, \] where $\mathcal{P}$ denotes the principal filter and $\mathcal{N}(0)$ is the neighborhood filter of $0$ in $F$.

UniformConvergenceCLM.eventually_nhds_zero_mapsTo theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] {𝔖 : Set (Set E)} {s : Set E} (hs : s ∈ 𝔖) {U : Set F} (hu : U ∈ 𝓝 0) :
  ∀ᶠ f : UniformConvergenceCLM σ F 𝔖 in 𝓝 0, MapsTo f s U

Full source

theorem eventually_nhds_zero_mapsTo [TopologicalSpace F] [IsTopologicalAddGroup F]
    {𝔖 : Set (Set E)} {s : Set E} (hs : s ∈ 𝔖) {U : Set F} (hu : U ∈ 𝓝 0) :
    ∀ᶠ f : UniformConvergenceCLM σ F 𝔖 in 𝓝 0, MapsTo f s U := by
  rw [nhds_zero_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

Uniform Convergence of Zero-Neighborhood Maps on $\mathfrak{S}$-Subsets

Informal description

Let $F$ be a topological space that is also a topological additive group, and let $\mathfrak{S}$ be a family of subsets of $E$. For any subset $s \in \mathfrak{S}$ and any neighborhood $U$ of $0$ in $F$, there exists a neighborhood $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ such that for all $f \in \mathcal{N}(0)$, the image $f(s)$ is contained in $U$.

UniformConvergenceCLM.isVonNBounded_image2_apply theorem

 {R : Type*} [SeminormedRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [DistribMulAction R F]
  [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {𝔖 : Set (Set E)} {S : Set (UniformConvergenceCLM σ F 𝔖)}
  (hS : IsVonNBounded R S) {s : Set E} (hs : s ∈ 𝔖) : IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s)

Full source

theorem isVonNBounded_image2_apply {R : Type*} [SeminormedRing R]
    [TopologicalSpace F] [IsTopologicalAddGroup F]
    [DistribMulAction R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F]
    {𝔖 : Set (Set E)} {S : Set (UniformConvergenceCLM σ F 𝔖)} (hS : IsVonNBounded R S)
    {s : Set E} (hs : s ∈ 𝔖) : IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) := by
  intro U hU
  filter_upwards [hS (eventually_nhds_zero_mapsTo σ hs hU)] with c hc
  rw [image2_subset_iff]
  intro f hf x hx
  rcases hc hf with ⟨g, hg, rfl⟩
  exact smul_mem_smul_set (hg hx)

Von Neumann Boundedness of Image under Uniformly Bounded Semilinear Maps

Informal description

Let $R$ be a seminormed ring, $F$ a topological space that is also a topological additive group, and $\mathfrak{S}$ a family of subsets of $E$. Suppose $F$ has a distributive multiplicative action by $R$ that is continuous in the second variable and commutes with scalar multiplication by $\Bbbk_2$. If $S$ is a von Neumann bounded subset of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$, then for any $s \in \mathfrak{S}$, the set $\{f(x) \mid f \in S, x \in s\}$ is von Neumann bounded in $F$.

UniformConvergenceCLM.isVonNBounded_iff theorem

 {R : Type*} [NormedDivisionRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module R F]
  [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {𝔖 : Set (Set E)} {S : Set (UniformConvergenceCLM σ F 𝔖)} :
  IsVonNBounded R S ↔ ∀ s ∈ 𝔖, IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s)

Full source

/-- A set `S` of continuous linear maps with topology of uniform convergence on sets `s ∈ 𝔖`
is von Neumann bounded iff for any `s ∈ 𝔖`,
the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded. -/
theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R]
    [TopologicalSpace F] [IsTopologicalAddGroup F]
    [Module R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F]
    {𝔖 : Set (Set E)} {S : Set (UniformConvergenceCLM σ F 𝔖)} :
    IsVonNBoundedIsVonNBounded R S ↔ ∀ s ∈ 𝔖, IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) := by
  refine ⟨fun hS s hs ↦ isVonNBounded_image2_apply hS hs, fun h ↦ ?_⟩
  simp_rw [isVonNBounded_iff_absorbing_le, nhds_zero_eq, le_iInf_iff, le_principal_iff]
  intro s hs U hU
  rw [Filter.mem_absorbing, Absorbs]
  filter_upwards [h s hs hU, eventually_ne_cobounded 0] with c hc hc₀ f hf
  rw [mem_smul_set_iff_inv_smul_mem₀ hc₀]
  intro x hx
  simpa only [mem_smul_set_iff_inv_smul_mem₀ hc₀] using hc (mem_image2_of_mem hf hx)

Von Neumann Boundedness Criterion for Uniformly Convergent Semilinear Maps

Informal description

Let $R$ be a normed division ring, $F$ a topological space that is also a topological additive group with a module structure over $R$, and $\mathfrak{S}$ a family of subsets of $E$. Suppose the scalar multiplication by $R$ on $F$ is continuous and commutes with scalar multiplication by $\Bbbk_2$. A subset $S$ of continuous $\sigma$-semilinear maps from $E$ to $F$ (equipped with the topology of uniform convergence on $\mathfrak{S}$) is von Neumann bounded if and only if for every subset $s \in \mathfrak{S}$, the set $\{f(x) \mid f \in S, x \in s\}$ is von Neumann bounded in $F$.

UniformConvergenceCLM.instUniformContinuousConstSMul instance

 (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [IsUniformAddGroup F]
  [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) : UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

Full source

instance instUniformContinuousConstSMul (M : Type*)
    [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
    [UniformSpace F] [IsUniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) :
    UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖) :=
  (isUniformInducing_coeFn σ F 𝔖).uniformContinuousConstSMul fun _ _ ↦ by rfl

Uniformly Continuous Scalar Multiplication on Continuous Semilinear Maps with $\mathfrak{S}$-Convergence

Informal description

For any monoid $M$ acting distributively on a uniform space $F$ that is also a uniform additive group, with the action commuting with the scalar multiplication by $\Bbbk_2$ and uniformly continuous in the second variable, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on a family $\mathfrak{S}$ of subsets of $E$ has uniformly continuous scalar multiplication by $M$. This means that for each $c \in M$, the map $f \mapsto c \cdot f$ is uniformly continuous on the space of continuous $\sigma$-semilinear maps with the $\mathfrak{S}$-convergence topology.

UniformConvergenceCLM.instContinuousConstSMul instance

 (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : ContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

Full source

instance instContinuousConstSMul (M : Type*)
    [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
    [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
    ContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖) :=
  let _ := IsTopologicalAddGroup.toUniformSpace F
  have _ : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  have _ := uniformContinuousConstSMul_of_continuousConstSMul M F
  inferInstance

Continuous Scalar Multiplication on Continuous Semilinear Maps with $\mathfrak{S}$-Convergence

Informal description

For any monoid $M$ acting distributively on a topological vector space $F$ over $\Bbbk_2$, with the action commuting with the scalar multiplication by $\Bbbk_2$ and continuous in the second variable, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on a family $\mathfrak{S}$ of subsets of $E$ has continuous scalar multiplication by $M$. This means that for each $c \in M$, the map $f \mapsto c \cdot f$ is continuous on the space of continuous $\sigma$-semilinear maps with the $\mathfrak{S}$-convergence topology.

UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn theorem

 {ι : Type*} {p : Filter ι} [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E))
  {a : ι → UniformConvergenceCLM σ F 𝔖} {a₀ : UniformConvergenceCLM σ F 𝔖} :
  Filter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (a · ·) a₀ p s

Full source

theorem tendsto_iff_tendstoUniformlyOn {ι : Type*} {p : Filter ι} [UniformSpace F]
    [IsUniformAddGroup F] (𝔖 : Set (Set E)) {a : ι → UniformConvergenceCLM σ F 𝔖}
    {a₀ : UniformConvergenceCLM σ F 𝔖} :
    Filter.TendstoFilter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (a · ·) a₀ p s := by
  rw [(isEmbedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
  rfl

Characterization of convergence in $\mathfrak{S}$-topology via uniform convergence on each set in $\mathfrak{S}$

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields, with $F$ equipped with a uniform space structure making it a uniform additive group. Given a family $\mathfrak{S}$ of subsets of $E$, a net of continuous $\sigma$-semilinear maps $(a_i : E \to_{SL[\sigma]} F)_{i \in \iota}$ converges to a continuous $\sigma$-semilinear map $a_0 : E \to_{SL[\sigma]} F$ in the topology of uniform convergence on $\mathfrak{S}$ if and only if for every set $s \in \mathfrak{S}$, the net $(a_i)$ converges uniformly to $a_0$ on $s$.

UniformConvergenceCLM.isUniformInducing_postcomp theorem

 {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] {𝕜₃ : Type*} [NormedField 𝕜₃] [Module 𝕜₃ G]
  {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F] [IsUniformAddGroup F] (g : F →SL[τ] G)
  (hg : IsUniformInducing g) (𝔖 : Set (Set E)) :
  IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := UniformConvergenceCLM ρ G 𝔖) g.comp

Full source

theorem isUniformInducing_postcomp
    {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G]
    {𝕜₃ : Type*} [NormedField 𝕜₃] [Module 𝕜₃ G]
    {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F] [IsUniformAddGroup F]
    (g : F →SL[τ] G) (hg : IsUniformInducing g) (𝔖 : Set (Set E)) :
    IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := UniformConvergenceCLM ρ G 𝔖)
      g.comp := by
  rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]
  exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)

Uniform Inducing Property of Post-Composition by a Uniform Inducing Continuous Semilinear Map under $\mathfrak{S}$-Convergence

Informal description

Let $E$, $F$, and $G$ be topological vector spaces over normed fields $\Bbbk_1$, $\Bbbk_2$, and $\Bbbk_3$ respectively, with ring homomorphisms $\sigma: \Bbbk_1 \to \Bbbk_2$, $\tau: \Bbbk_2 \to \Bbbk_3$, and $\rho: \Bbbk_1 \to \Bbbk_3$ such that $\rho = \tau \circ \sigma$. Suppose $F$ and $G$ are uniform additive groups, and let $g: F \to_{SL[\tau]} G$ be a continuous $\tau$-semilinear map that is uniform inducing. Given a family $\mathfrak{S}$ of subsets of $E$, the post-composition map $g \circ (\cdot): \text{UniformConvergenceCLM}_\sigma F \mathfrak{S} \to \text{UniformConvergenceCLM}_\rho G \mathfrak{S}$ is uniform inducing with respect to the $\mathfrak{S}$-convergence topologies.

UniformConvergenceCLM.completeSpace theorem

 [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] {𝔖 : Set (Set E)}
  (h𝔖 : IsCoherentWith 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) : CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Full source

theorem completeSpace [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
    {𝔖 : Set (Set E)} (h𝔖 : IsCoherentWith 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) :
    CompleteSpace (UniformConvergenceCLM σ F 𝔖) := by
  wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
    exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]
  rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]
  apply IsClosed.isComplete
  have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
    UniformOnFun.isClosed_setOf_continuous h𝔖
  convert H₁.inter <| (LinearMap.isClosed_range_coe E F σ).preimage
    (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous
  exact ContinuousLinearMap.range_coeFn_eq

Completeness of Continuous Semilinear Maps under Uniform $\mathfrak{S}$-Convergence

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\Bbbk_1$ and $\Bbbk_2$ with a ring homomorphism $\sigma : \Bbbk_1 \to \Bbbk_2$, where $F$ is a complete uniform space that is also a uniform additive group with continuous scalar multiplication. Given a family $\mathfrak{S}$ of subsets of $E$ such that: 1. The topology on $E$ is coherent with $\mathfrak{S}$ (i.e., a set is open in $E$ if and only if its intersection with each $S \in \mathfrak{S}$ is open in $S$) 2. The union of all sets in $\mathfrak{S}$ covers $E$ (i.e., $\bigcup_{S\in\mathfrak{S}} S = E$) Then the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on $\mathfrak{S}$ is complete.

UniformConvergenceCLM.uniformSpace_mono theorem

 [UniformSpace F] [IsUniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) : instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂

Full source

theorem uniformSpace_mono [UniformSpace F] [IsUniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
    instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂ := by
  simp_rw [uniformSpace_eq]
  exact UniformSpace.comap_mono (UniformOnFun.mono (le_refl _) h)

Monotonicity of Uniform Structure with Respect to Family of Sets for Continuous Semilinear Maps

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a uniform space structure making it a uniform additive group. For any two families $\mathfrak{S}_1$ and $\mathfrak{S}_2$ of subsets of $E$ with $\mathfrak{S}_2 \subseteq \mathfrak{S}_1$, the uniform structure of $\mathfrak{S}_1$-convergence on the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ is finer than the uniform structure of $\mathfrak{S}_2$-convergence.

UniformConvergenceCLM.topologicalSpace_mono theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
  instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂

Full source

theorem topologicalSpace_mono [TopologicalSpace F] [IsTopologicalAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
    instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂ := by
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  simp_rw [← uniformity_toTopologicalSpace_eq]
  exact UniformSpace.toTopologicalSpace_mono (uniformSpace_mono σ F h)

Monotonicity of Topology with Respect to Family of Sets for Continuous Semilinear Maps

Informal description

Let $E$ and $F$ be topological vector spaces over a field with a ring homomorphism $\sigma$, where $F$ is equipped with a topological space structure making it a topological additive group. For any two families $\mathfrak{S}_1$ and $\mathfrak{S}_2$ of subsets of $E$ with $\mathfrak{S}_2 \subseteq \mathfrak{S}_1$, the topology of $\mathfrak{S}_1$-convergence on the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ is finer than the topology of $\mathfrak{S}_2$-convergence.

ContinuousLinearMap.topologicalSpace instance

[TopologicalSpace F] [IsTopologicalAddGroup F] : TopologicalSpace (E →SL[σ] F)

Full source

/-- The topology of bounded convergence on `E →L[𝕜] F`. This coincides with the topology induced by
the operator norm when `E` and `F` are normed spaces. -/
instance topologicalSpace [TopologicalSpace F] [IsTopologicalAddGroup F] :
    TopologicalSpace (E →SL[σ] F) :=
  UniformConvergenceCLM.instTopologicalSpace σ F { S | IsVonNBounded 𝕜₁ S }

Topology of Uniform Convergence on Bounded Sets for Continuous Semilinear Maps

Informal description

The space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ is equipped with the topology of uniform convergence on bounded subsets of $E$, where $F$ is a topological space and a topological additive group. This topology coincides with the operator norm topology when $E$ and $F$ are normed spaces.

ContinuousLinearMap.topologicalAddGroup instance

[TopologicalSpace F] [IsTopologicalAddGroup F] : IsTopologicalAddGroup (E →SL[σ] F)

Full source

instance topologicalAddGroup [TopologicalSpace F] [IsTopologicalAddGroup F] :
    IsTopologicalAddGroup (E →SL[σ] F) :=
  UniformConvergenceCLM.instIsTopologicalAddGroup σ F _

Topological Additive Group Structure on Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

For any topological space $F$ that is a topological additive group, the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ equipped with the topology of uniform convergence on bounded subsets of $E$ forms a topological additive group. This means that the pointwise addition and negation operations are continuous with respect to this topology.

ContinuousLinearMap.continuousSMul instance

 [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] :
  ContinuousSMul 𝕜₂ (E →SL[σ] F)

Full source

instance continuousSMul [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F]
    [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (E →SL[σ] F) :=
  UniformConvergenceCLM.continuousSMul σ F { S | IsVonNBounded 𝕜₁ S } fun _ hs => hs

Continuous Scalar Multiplication on Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

Let $\mathbb{K}_1$ and $\mathbb{K}_2$ be normed fields, and let $\sigma \colon \mathbb{K}_1 \to \mathbb{K}_2$ be a surjective and isometric ring homomorphism. Let $E$ be a topological vector space over $\mathbb{K}_1$ and $F$ a topological vector space over $\mathbb{K}_2$ that is also a topological additive group with continuous scalar multiplication. Then the space of continuous $\sigma$-semilinear maps from $E$ to $F$, equipped with the topology of uniform convergence on bounded subsets of $E$, has continuous scalar multiplication by $\mathbb{K}_2$.

ContinuousLinearMap.uniformSpace instance

[UniformSpace F] [IsUniformAddGroup F] : UniformSpace (E →SL[σ] F)

Full source

instance uniformSpace [UniformSpace F] [IsUniformAddGroup F] : UniformSpace (E →SL[σ] F) :=
  UniformConvergenceCLM.instUniformSpace σ F { S | IsVonNBounded 𝕜₁ S }

Uniform Space Structure on Continuous Semilinear Maps via Bounded Convergence

Informal description

For any uniform space $F$ that is also a uniform additive group, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ can be equipped with a uniform space structure. This structure is induced by the topology of uniform convergence on bounded subsets of $E$.

ContinuousLinearMap.isUniformAddGroup instance

[UniformSpace F] [IsUniformAddGroup F] : IsUniformAddGroup (E →SL[σ] F)

Full source

instance isUniformAddGroup [UniformSpace F] [IsUniformAddGroup F] :
    IsUniformAddGroup (E →SL[σ] F) :=
  UniformConvergenceCLM.instIsUniformAddGroup σ F _

Uniform Additive Group Structure on Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

For any uniform space $F$ that is also a uniform additive group, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ forms a uniform additive group when equipped with the topology of uniform convergence on bounded subsets of $E$. This means that the addition and negation operations are uniformly continuous with respect to this topology.

ContinuousLinearMap.instContinuousEvalConst instance

[TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] : ContinuousEvalConst (E →SL[σ] F) E F

Full source

instance instContinuousEvalConst [TopologicalSpace F] [IsTopologicalAddGroup F]
    [ContinuousSMul 𝕜₁ E] : ContinuousEvalConst (E →SL[σ] F) E F :=
  UniformConvergenceCLM.continuousEvalConst σ F _ Bornology.isVonNBounded_covers

Continuity of Point Evaluation for Continuous Semilinear Maps

Informal description

For any topological space $F$ that is a topological additive group and any topological module $E$ over $\mathbb{K}_1$ with continuous scalar multiplication, the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ has the property that for any fixed $x \in E$, the evaluation map $\text{eval}_x : (E \toSL[\sigma] F) \to F$ given by $f \mapsto f(x)$ is continuous.

ContinuousLinearMap.instT2Space instance

[TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] : T2Space (E →SL[σ] F)

Full source

instance instT2Space [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E]
    [T2Space F] : T2Space (E →SL[σ] F) :=
  UniformConvergenceCLM.t2Space σ F _ Bornology.isVonNBounded_covers

Hausdorff Property for Space of Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

For any topological space $F$ that is a Hausdorff topological additive group and has a continuous scalar multiplication action by $\mathbb{K}_1$ on $E$, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on bounded subsets is a Hausdorff space.

ContinuousLinearMap.hasBasis_nhds_zero_of_basis theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type*} {p : ι → Prop} {b : ι → Set F}
  (h : (𝓝 0 : Filter F).HasBasis p b) :
  (𝓝 (0 : E →SL[σ] F)).HasBasis (fun Si : Set E × ι => IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2) fun Si =>
    {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

Full source

protected theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F]
    {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
    (𝓝 (0 : E →SL[σ] F)).HasBasis (fun Si : SetSet E × ι => IsVonNBoundedIsVonNBounded 𝕜₁ Si.1 ∧ p Si.2)
      fun Si => { f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2 } :=
  UniformConvergenceCLM.hasBasis_nhds_zero_of_basis σ F { S | IsVonNBounded 𝕜₁ S }
    ⟨∅, isVonNBounded_empty 𝕜₁ E⟩
    (directedOn_of_sup_mem fun _ _ => IsVonNBounded.union) h

Basis for Zero Neighborhoods in Space of Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$ a ring homomorphism. Suppose the neighborhood filter $\mathcal{N}_0$ of $0$ in $F$ has a basis $\{b_i \mid p i\}$ indexed by $\iota$, where $p : \iota \to \text{Prop}$ and $b : \iota \to \text{Set } F$. Then the neighborhood filter $\mathcal{N}_0$ of $0$ in the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ (equipped with the topology of uniform convergence on von Neumann bounded subsets of $E$) has a basis consisting of sets of the form $$\{f : E \toSL[\sigma] F \mid \forall x \in S, f(x) \in b_i\}$$ for $S \subseteq E$ von Neumann bounded and $i \in \iota$ with $p i$.

ContinuousLinearMap.hasBasis_nhds_zero theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] :
  (𝓝 (0 : E →SL[σ] F)).HasBasis (fun SV : Set E × Set F => IsVonNBounded 𝕜₁ SV.1 ∧ SV.2 ∈ (𝓝 0 : Filter F)) fun SV =>
    {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}

Full source

protected theorem hasBasis_nhds_zero [TopologicalSpace F] [IsTopologicalAddGroup F] :
    (𝓝 (0 : E →SL[σ] F)).HasBasis
      (fun SV : SetSet E × Set F => IsVonNBoundedIsVonNBounded 𝕜₁ SV.1 ∧ SV.2 ∈ (𝓝 0 : Filter F))
      fun SV => { f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2 } :=
  ContinuousLinearMap.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets

Basis for Zero Neighborhoods in Space of Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$ a ring homomorphism. Assume $F$ is a topological additive group. Then the neighborhood filter $\mathcal{N}_0$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ (equipped with the topology of uniform convergence on von Neumann bounded subsets of $E$) has a basis consisting of sets of the form $$\{f : E \toSL[\sigma] F \mid \forall x \in S, f(x) \in V\}$$ where $S \subseteq E$ is von Neumann bounded and $V$ is a neighborhood of $0$ in $F$.

ContinuousLinearMap.isUniformEmbedding_toUniformOnFun theorem

 [UniformSpace F] [IsUniformAddGroup F] :
  IsUniformEmbedding fun f : E →SL[σ] F ↦ UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f

Full source

theorem isUniformEmbedding_toUniformOnFun [UniformSpace F] [IsUniformAddGroup F] :
    IsUniformEmbedding
      fun f : E →SL[σ] F ↦ UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f :=
  UniformConvergenceCLM.isUniformEmbedding_coeFn ..

Uniform Embedding of Continuous Semilinear Maps into Function Space with Bounded Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields, where $F$ is equipped with a uniform space structure making it a uniform additive group. The canonical embedding from the space of continuous $\sigma$-semilinear maps $E \to_{SL[\sigma]} F$ (with the topology of uniform convergence on von Neumann bounded subsets of $E$) into the space of functions $E \to F$ (with the uniform structure of convergence on von Neumann bounded subsets) is a uniform embedding.

ContinuousLinearMap.uniformContinuousConstSMul instance

 {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [IsUniformAddGroup F]
  [UniformContinuousConstSMul M F] : UniformContinuousConstSMul M (E →SL[σ] F)

Full source

instance uniformContinuousConstSMul
    {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
    [UniformSpace F] [IsUniformAddGroup F] [UniformContinuousConstSMul M F] :
    UniformContinuousConstSMul M (E →SL[σ] F) :=
  UniformConvergenceCLM.instUniformContinuousConstSMul σ F _ _

Uniformly Continuous Scalar Multiplication on Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

For any monoid $M$ acting distributively on a uniform space $F$ that is also a uniform additive group, with the action commuting with the scalar multiplication by $\Bbbk_2$ and uniformly continuous in the second variable, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on bounded subsets of $E$ has uniformly continuous scalar multiplication by $M$. This means that for each $c \in M$, the map $f \mapsto c \cdot f$ is uniformly continuous on the space of continuous $\sigma$-semilinear maps with the bounded convergence topology.

ContinuousLinearMap.continuousConstSMul instance

 {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousConstSMul M F] : ContinuousConstSMul M (E →SL[σ] F)

Full source

instance continuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
    [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] :
    ContinuousConstSMul M (E →SL[σ] F) :=
  UniformConvergenceCLM.instContinuousConstSMul σ F _ _

Continuous Scalar Multiplication on Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

For any monoid $M$ acting distributively on a topological vector space $F$ over $\Bbbk_2$, with the action commuting with the scalar multiplication by $\Bbbk_2$ and continuous in the second variable, the space of continuous $\sigma$-semilinear maps from $E$ to $F$ equipped with the topology of uniform convergence on bounded subsets of $E$ has continuous scalar multiplication by $M$. This means that for each $c \in M$, the map $f \mapsto c \cdot f$ is continuous on the space of continuous $\sigma$-semilinear maps with the bounded convergence topology.

ContinuousLinearMap.nhds_zero_eq_of_basis theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type*} {p : ι → Prop} {b : ι → Set F}
  (h : (𝓝 0 : Filter F).HasBasis p b) :
  𝓝 (0 : E →SL[σ] F) = ⨅ (s : Set E) (_ : IsVonNBounded 𝕜₁ s) (i : ι) (_ : p i), 𝓟 {f : E →SL[σ] F | MapsTo f s (b i)}

Full source

protected theorem nhds_zero_eq_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F]
    {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
    𝓝 (0 : E →SL[σ] F) =
      ⨅ (s : Set E) (_ : IsVonNBounded 𝕜₁ s) (i : ι) (_ : p i),
        𝓟 {f : E →SL[σ] F | MapsTo f s (b i)} :=
  UniformConvergenceCLM.nhds_zero_eq_of_basis _ _ _ h

Neighborhood basis for zero in continuous semilinear maps with bounded convergence topology

Informal description

Let $F$ be a topological space and a topological additive group, and let $\{b_i\}_{i \in \iota}$ be a basis for the neighborhood filter of $0$ in $F$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the neighborhood filter $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ equipped with the topology of uniform convergence on bounded subsets of $E$ is given by: \[ \mathcal{N}(0) = \bigsqcap_{\substack{s \subseteq E \\ \text{von Neumann bounded}}} \bigsqcap_{\substack{i \in \iota \\ p(i)}} \mathcal{P}\{f \mid \forall x \in s, f(x) \in b_i\}, \] where $\mathcal{P}$ denotes the principal filter.

ContinuousLinearMap.nhds_zero_eq theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] :
  𝓝 (0 : E →SL[σ] F) =
    ⨅ (s : Set E) (_ : IsVonNBounded 𝕜₁ s) (U : Set F) (_ : U ∈ 𝓝 0), 𝓟 {f : E →SL[σ] F | MapsTo f s U}

Full source

protected theorem nhds_zero_eq [TopologicalSpace F] [IsTopologicalAddGroup F] :
    𝓝 (0 : E →SL[σ] F) =
      ⨅ (s : Set E) (_ : IsVonNBounded 𝕜₁ s) (U : Set F) (_ : U ∈ 𝓝 0),
        𝓟 {f : E →SL[σ] F | MapsTo f s U} :=
  UniformConvergenceCLM.nhds_zero_eq ..

Neighborhood Filter Characterization for Zero in Continuous Semilinear Maps with Bounded Convergence Topology

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$ a ring homomorphism. Assume $F$ is a topological additive group. The neighborhood filter $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$, equipped with the topology of uniform convergence on von Neumann bounded subsets of $E$, is given by: \[ \mathcal{N}(0) = \bigcap_{\substack{s \subseteq E \\ \text{von Neumann bounded}}} \bigcap_{U \in \mathcal{N}(0)} \mathcal{P}\{f \mid f(s) \subseteq U\}, \] where $\mathcal{P}$ denotes the principal filter and $\mathcal{N}(0)$ is the neighborhood filter of $0$ in $F$.

ContinuousLinearMap.eventually_nhds_zero_mapsTo theorem

 [TopologicalSpace F] [IsTopologicalAddGroup F] {s : Set E} (hs : IsVonNBounded 𝕜₁ s) {U : Set F} (hu : U ∈ 𝓝 0) :
  ∀ᶠ f : E →SL[σ] F in 𝓝 0, MapsTo f s U

Full source

/-- If `s` is a von Neumann bounded set and `U` is a neighbourhood of zero,
then sufficiently small continuous linear maps map `s` to `U`. -/
theorem eventually_nhds_zero_mapsTo [TopologicalSpace F] [IsTopologicalAddGroup F]
    {s : Set E} (hs : IsVonNBounded 𝕜₁ s) {U : Set F} (hu : U ∈ 𝓝 0) :
    ∀ᶠ f : E →SL[σ] F in 𝓝 0, MapsTo f s U :=
  UniformConvergenceCLM.eventually_nhds_zero_mapsTo _ hs hu

Neighborhood of zero maps von Neumann bounded sets into neighborhoods of zero

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$ a ring homomorphism. Assume $F$ is a topological additive group. For any von Neumann bounded subset $s \subseteq E$ and any neighborhood $U$ of $0$ in $F$, there exists a neighborhood $\mathcal{N}(0)$ of the zero map in the space of continuous $\sigma$-semilinear maps $E \toSL[\sigma] F$ such that for all $f \in \mathcal{N}(0)$, the image $f(s)$ is contained in $U$.

ContinuousLinearMap.isVonNBounded_image2_apply theorem

 {R : Type*} [SeminormedRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [DistribMulAction R F]
  [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)} (hS : IsVonNBounded R S) {s : Set E}
  (hs : IsVonNBounded 𝕜₁ s) : IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s)

Full source

/-- If `S` is a von Neumann bounded set of continuous linear maps `f : E →SL[σ] F`
and `s` is a von Neumann bounded set in the domain,
then the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.

See also `isVonNBounded_iff` for an `Iff` version with stronger typeclass assumptions. -/
theorem isVonNBounded_image2_apply {R : Type*} [SeminormedRing R]
    [TopologicalSpace F] [IsTopologicalAddGroup F]
    [DistribMulAction R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F]
    {S : Set (E →SL[σ] F)} (hS : IsVonNBounded R S) {s : Set E} (hs : IsVonNBounded 𝕜₁ s) :
    IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
  UniformConvergenceCLM.isVonNBounded_image2_apply hS hs

Von Neumann Boundedness of Continuous Semilinear Images of Bounded Sets

Informal description

Let $R$ be a seminormed ring, $F$ a topological space that is also a topological additive group, and $E$ a topological vector space over a normed field $\mathbb{K}_1$. Suppose $F$ has a distributive multiplicative action by $R$ that is continuous in the second variable and commutes with scalar multiplication by $\mathbb{K}_2$. If $S$ is a von Neumann bounded subset of continuous $\sigma$-semilinear maps from $E$ to $F$, and $s$ is a von Neumann bounded subset of $E$, then the set $\{f(x) \mid f \in S, x \in s\}$ is von Neumann bounded in $F$.

ContinuousLinearMap.isVonNBounded_iff theorem

 {R : Type*} [NormedDivisionRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module R F]
  [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)} :
  IsVonNBounded R S ↔ ∀ s, IsVonNBounded 𝕜₁ s → IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s)

Full source

/-- A set `S` of continuous linear maps is von Neumann bounded
iff for any von Neumann bounded set `s`,
the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.

For the forward implication with weaker typeclass assumptions, see `isVonNBounded_image2_apply`. -/
theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R]
    [TopologicalSpace F] [IsTopologicalAddGroup F]
    [Module R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F]
    {S : Set (E →SL[σ] F)} :
    IsVonNBoundedIsVonNBounded R S ↔
      ∀ s, IsVonNBounded 𝕜₁ s → IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
  UniformConvergenceCLM.isVonNBounded_iff

Von Neumann Boundedness Criterion for Continuous Semilinear Maps

Informal description

Let $R$ be a normed division ring, $F$ a topological space that is also a topological additive group with a module structure over $R$, and $E$ a topological vector space over a normed field $\mathbb{K}_1$. Suppose the scalar multiplication by $R$ on $F$ is continuous and commutes with scalar multiplication by $\mathbb{K}_2$. A subset $S$ of continuous $\sigma$-semilinear maps from $E$ to $F$ is von Neumann bounded if and only if for every von Neumann bounded subset $s \subseteq E$, the set $\{f(x) \mid f \in S, x \in s\}$ is von Neumann bounded in $F$.

ContinuousLinearMap.completeSpace theorem

 [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] [ContinuousSMul 𝕜₁ E]
  (h : IsCoherentWith {s : Set E | IsVonNBounded 𝕜₁ s}) : CompleteSpace (E →SL[σ] F)

Full source

theorem completeSpace [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
    [ContinuousSMul 𝕜₁ E] (h : IsCoherentWith {s : Set E | IsVonNBounded 𝕜₁ s}) :
    CompleteSpace (E →SL[σ] F) :=
  UniformConvergenceCLM.completeSpace _ _ h isVonNBounded_covers

Completeness of Continuous Semilinear Maps under Bounded Convergence

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$. Suppose that: 1. $F$ is a complete uniform space and a uniform additive group with continuous scalar multiplication. 2. The topology on $E$ is coherent with the family of von Neumann bounded subsets (i.e., a set is open in $E$ if and only if its intersection with every von Neumann bounded set is open in that bounded set). 3. Scalar multiplication on $E$ is continuous. Then the space of continuous $\sigma$-semilinear maps from $E$ to $F$, equipped with the topology of uniform convergence on von Neumann bounded subsets of $E$, is complete.

ContinuousLinearMap.instCompleteSpace instance

 [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E] [UniformSpace F] [IsUniformAddGroup F]
  [ContinuousSMul 𝕜₂ F] [CompleteSpace F] : CompleteSpace (E →SL[σ] F)

Full source

instance instCompleteSpace [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E]
    [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] :
    CompleteSpace (E →SL[σ] F) :=
  completeSpace <| .of_seq fun _ _ h ↦ (h.isVonNBounded_range 𝕜₁).insert _

Completeness of Continuous Semilinear Maps under Bounded Convergence in Sequential Spaces

Informal description

Let $E$ and $F$ be topological vector spaces over normed fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma : \mathbb{K}_1 \to \mathbb{K}_2$. Suppose that: 1. $E$ is a sequential space with continuous scalar multiplication and forms a topological additive group. 2. $F$ is a complete uniform space, forms a uniform additive group, and has continuous scalar multiplication. Then the space of continuous $\sigma$-semilinear maps from $E$ to $F$, equipped with the topology of uniform convergence on bounded subsets of $E$, is complete.

ContinuousLinearMap.precomp definition

 [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) :
  (F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G

Full source

/-- Pre-composition by a *fixed* continuous linear map as a continuous linear map.
Note that in non-normed space it is not always true that composition is continuous
in both variables, so we have to fix one of them. -/
@[simps]
def precomp [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ]
    [RingHomIsometric σ] (L : E →SL[σ] F) : (F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G where
  toFun f := f.comp L
  map_add' f g := add_comp f g L
  map_smul' a f := smul_comp a f L
  cont := by
    letI : UniformSpace G := IsTopologicalAddGroup.toUniformSpace G
    haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
    rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]
    apply (UniformOnFun.precomp_uniformContinuous fun S hS => hS.image L).continuous.comp
        (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous

Pre-composition by a fixed continuous semilinear map

Informal description

Given a continuous semilinear map $ L: E \toSL[\sigma] F $ and topological conditions on $ G $, the function `precomp` maps a continuous semilinear map $ f: F \toSL[\tau] G $ to its composition with $ L $, $ f \circ L: E \toSL[\rho] G $. This operation is itself a continuous linear map from the space of continuous semilinear maps $ F \toSL[\tau] G $ to the space $ E \toSL[\rho] G $. Here, $ \sigma: R_1 \to R_2 $, $ \tau: R_2 \to R_3 $, and $ \rho: R_1 \to R_3 $ are ring homomorphisms with $ \rho = \tau \circ \sigma $, and $ E $, $ F $, $ G $ are topological modules over $ R_1 $, $ R_2 $, $ R_3 $ respectively. The continuity of `precomp` relies on the topology of uniform convergence on bounded sets.

ContinuousLinearMap.postcomp definition

 [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F]
  (L : F →SL[τ] G) : (E →SL[σ] F) →SL[τ] E →SL[ρ] G

Full source

/-- Post-composition by a *fixed* continuous linear map as a continuous linear map.
Note that in non-normed space it is not always true that composition is continuous
in both variables, so we have to fix one of them. -/
@[simps]
def postcomp [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G]
    [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : (E →SL[σ] F) →SL[τ] E →SL[ρ] G where
  toFun f := L.comp f
  map_add' := comp_add L
  map_smul' := comp_smulₛₗ L
  cont := by
    letI : UniformSpace G := IsTopologicalAddGroup.toUniformSpace G
    haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
    letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
    haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
    rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]
    exact
      (UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
        (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous

Post-composition by a continuous semilinear map

Informal description

Given continuous semilinear maps $ L : F \toSL[\tau] G $ between topological modules $ F $ and $ G $, the post-composition map $ f \mapsto L \circ f $ is a continuous semilinear map from the space of continuous semilinear maps $ E \toSL[\sigma] F $ to the space of continuous semilinear maps $ E \toSL[\rho] G $. Here, $ E $, $ F $, and $ G $ are topological modules over appropriate semirings, and the maps respect the ring homomorphisms $ \sigma $, $ \tau $, and $ \rho $.

ContinuousLinearMap.toLinearMap₂ definition

(L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G

Full source

/-- Send a continuous bilinear map to an abstract bilinear map (forgetting continuity). -/
def toLinearMap₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G :=
  (coeLMₛₗ σ₂₃).comp L.toLinearMap

Underlying abstract bilinear map of a continuous bilinear map

Informal description

Given a continuous bilinear map $L: E \toSL[\sigma_{13}] (F \toSL[\sigma_{23}] G)$, the function returns the underlying abstract bilinear map $L: E \to_{SL[\sigma_{13}]} (F \to_{SL[\sigma_{23}]} G)$, forgetting the continuity properties.

ContinuousLinearMap.toLinearMap₂_apply theorem

(L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) : L.toLinearMap₂ v w = L v w

Full source

@[simp] lemma toLinearMap₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
    L.toLinearMap₂ v w = L v w := rfl

Equality of Abstract and Continuous Bilinear Map Applications

Informal description

For any continuous bilinear map $L \colon E \toSL[\sigma_{13}] (F \toSL[\sigma_{23}] G)$ and any vectors $v \in E$, $w \in F$, the application of the underlying abstract bilinear map $L.\text{toLinearMap}_2$ satisfies $L.\text{toLinearMap}_2(v)(w) = L(v)(w)$.

ContinuousLinearMap.isUniformEmbedding_restrictScalars theorem

: IsUniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F))

Full source

theorem isUniformEmbedding_restrictScalars :
    IsUniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := by
  rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]
  convert isUniformEmbedding_toUniformOnFun using 4 with s
  exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩

Uniform Embedding Property of Scalar Restriction on Continuous Linear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$, and let $E$, $F$ be topological vector spaces over $\mathbb{K}'$. The restriction of scalars map from the space of continuous $\mathbb{K}$-linear maps $E \to_{\mathbb{K}} F$ to the space of continuous $\mathbb{K}'$-linear maps $E \to_{\mathbb{K}'} F$ is a uniform embedding, where both spaces are equipped with the uniform structure of uniform convergence on von Neumann bounded subsets.

ContinuousLinearMap.uniformContinuous_restrictScalars theorem

: UniformContinuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F))

Full source

theorem uniformContinuous_restrictScalars :
    UniformContinuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
  (isUniformEmbedding_restrictScalars 𝕜').uniformContinuous

Uniform Continuity of Scalar Restriction on Continuous Linear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$, and let $E$, $F$ be topological vector spaces over $\mathbb{K}'$. The restriction of scalars map from the space of continuous $\mathbb{K}$-linear maps $E \to_{\mathbb{K}} F$ to the space of continuous $\mathbb{K}'$-linear maps $E \to_{\mathbb{K}'} F$ is uniformly continuous, where both spaces are equipped with the uniform structure of uniform convergence on von Neumann bounded subsets.

ContinuousLinearMap.isEmbedding_restrictScalars theorem

: IsEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F))

Full source

theorem isEmbedding_restrictScalars :
    IsEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  (isUniformEmbedding_restrictScalars _).isEmbedding

Topological Embedding Property of Scalar Restriction on Continuous Linear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$, and let $E$, $F$ be topological vector spaces over $\mathbb{K}'$. The restriction of scalars map from the space of continuous $\mathbb{K}$-linear maps $E \to_{\mathbb{K}} F$ to the space of continuous $\mathbb{K}'$-linear maps $E \to_{\mathbb{K}'} F$ is a topological embedding, where both spaces are equipped with the topology of uniform convergence on bounded subsets.

ContinuousLinearMap.continuous_restrictScalars theorem

: Continuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F))

Full source

@[continuity, fun_prop]
theorem continuous_restrictScalars :
    Continuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
   (isEmbedding_restrictScalars _).continuous

Continuity of Scalar Restriction for Continuous Linear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$, and let $E$, $F$ be topological vector spaces over $\mathbb{K}'$. The restriction of scalars map from the space of continuous $\mathbb{K}$-linear maps $E \to_{\mathbb{K}} F$ to the space of continuous $\mathbb{K}'$-linear maps $E \to_{\mathbb{K}'} F$ is continuous, where both spaces are equipped with the topology of uniform convergence on bounded subsets.

ContinuousLinearMap.restrictScalarsL definition

: (E →L[𝕜] F) →L[𝕜''] E →L[𝕜'] F

Full source

/-- `ContinuousLinearMap.restrictScalars` as a `ContinuousLinearMap`. -/
def restrictScalarsL : (E →L[𝕜] F) →L[𝕜''] E →L[𝕜'] F :=
  .mk.mk <| restrictScalarsₗ 𝕜 E F 𝕜' 𝕜''

Continuous linear scalar restriction map

Informal description

Given normed fields $\mathbb{K}$, $\mathbb{K}'$, and $\mathbb{K}''$ where $\mathbb{K}$ is a normed algebra over $\mathbb{K}'$, the continuous linear map `restrictScalarsL` takes a continuous $\mathbb{K}$-linear map $f \colon E \to F$ and returns a continuous $\mathbb{K}'$-linear map by restricting the scalar action from $\mathbb{K}$ to $\mathbb{K}'$. This operation is itself a continuous $\mathbb{K}''$-linear map between the spaces of continuous linear maps.

ContinuousLinearMap.coe_restrict_scalarsL' theorem

: ⇑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = restrictScalars 𝕜'

Full source

@[simp]
theorem coe_restrict_scalarsL' : ⇑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = restrictScalars 𝕜' :=
  rfl

Underlying function of scalar restriction map equals scalar restriction operation

Informal description

The underlying function of the continuous linear map `restrictScalarsL 𝕜 E F 𝕜' 𝕜''` is equal to the scalar restriction operation `restrictScalars 𝕜'` on continuous linear maps.

ContinuousLinearEquiv.arrowCongrSL definition

 (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G

Full source

/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
spaces of continuous (semi)linear maps. -/
@[simps apply symm_apply toLinearEquiv_apply toLinearEquiv_symm_apply]
def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
    (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
{ e₁₂.arrowCongrEquiv e₄₃ with
    -- given explicitly to help `simps`
    toFun := fun L => (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E))
    -- given explicitly to help `simps`
    invFun := fun L => (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F))
    map_add' := fun f g => by simp only [add_comp, comp_add]
    map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ]
    continuous_toFun := ((postcomp F e₄₃.toContinuousLinearMap).comp
      (precomp H e₁₂.symm.toContinuousLinearMap)).continuous
    continuous_invFun := ((precomp H e₁₂.toContinuousLinearMap).comp
      (postcomp F e₄₃.symm.toContinuousLinearMap)).continuous }

Continuous semilinear equivalence between spaces of continuous semilinear maps induced by equivalences

Informal description

Given continuous semilinear equivalences $ e_{12} : E \simeq_{SL[\sigma_{12}]} F $ and $ e_{43} : H \simeq_{SL[\sigma_{43}]} G $, the function constructs a continuous semilinear equivalence between the spaces of continuous semilinear maps $ E \to_{SL[\sigma_{14}]} H $ and $ F \to_{SL[\sigma_{23}]} G $. The forward map sends $ L $ to $ e_{43} \circ L \circ e_{12}^{-1} $, and the inverse map sends $ L' $ to $ e_{43}^{-1} \circ L' \circ e_{12} $. Both the forward and inverse maps are continuous and semilinear with respect to the appropriate ring homomorphisms.

ContinuousLinearEquiv.arrowCongr definition

(e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G

Full source

/-- A pair of continuous linear equivalences generates a continuous linear equivalence between
the spaces of continuous linear maps. -/
def arrowCongr (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G :=
  e₁.arrowCongrSL e₂

Continuous linear equivalence between spaces of continuous linear maps induced by equivalences

Informal description

Given continuous linear equivalences $ e_1 : E \simeq_L[\mathbb{K}] F $ and $ e_2 : H \simeq_L[\mathbb{K}] G $ between normed spaces over the field $\mathbb{K}$, the function constructs a continuous linear equivalence between the spaces of continuous linear maps $ E \to_L[\mathbb{K}] H $ and $ F \to_L[\mathbb{K}] G $. The forward map sends a continuous linear map $ L $ to $ e_2 \circ L \circ e_1^{-1} $, and the inverse map sends $ L' $ to $ e_2^{-1} \circ L' \circ e_1 $. Both the forward and inverse maps are continuous and linear.

ContinuousLinearEquiv.arrowCongr_apply theorem

 (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (f : E →L[𝕜] H) (x : F) : e₁.arrowCongr e₂ f x = e₂ (f (e₁.symm x))

Full source

@[simp] lemma arrowCongr_apply (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (f : E →L[𝕜] H) (x : F) :
    e₁.arrowCongr e₂ f x = e₂ (f (e₁.symm x)) := rfl

Evaluation Formula for Induced Continuous Linear Map via Equivalences

Informal description

Given continuous linear equivalences $e_1 : E \simeq_L[\mathbb{K}] F$ and $e_2 : H \simeq_L[\mathbb{K}] G$ between normed spaces over the field $\mathbb{K}$, and a continuous linear map $f : E \to_L[\mathbb{K}] H$, the evaluation of the induced map $e_1.arrowCongr\ e_2\ f$ at any point $x \in F$ is given by $e_2(f(e_1^{-1}(x)))$.

ContinuousLinearEquiv.arrowCongr_symm theorem

(e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

Full source

@[simp] lemma arrowCongr_symm (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) :
    (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm := rfl

Inverse of the Induced Continuous Linear Equivalence Between Mapping Spaces

Informal description

Given continuous linear equivalences $ e_1 : E \simeq_L[\mathbb{K}] F $ and $ e_2 : H \simeq_L[\mathbb{K}] G $ between normed spaces over the field $\mathbb{K}$, the inverse of the induced continuous linear equivalence $ e_1.arrowCongr e_2 : (E \to_L[\mathbb{K}] H) \simeq_L[\mathbb{K}] (F \to_L[\mathbb{K}] G) $ is equal to the continuous linear equivalence induced by the inverses $ e_1^{-1} $ and $ e_2^{-1} $, i.e., $ (e_1.arrowCongr e_2)^{-1} = e_1^{-1}.arrowCongr e_2^{-1} $.

Mathlib.Topology.Algebra.Module.StrongTopology

Main definitions

Main statements

References

TODO

Tags