Basic facts on the topology of pointwise convergence

Scalar multiplication on E →SLₚₜ[σ] F is jointly continuous whenever it is on F, since it is computed pointwise (PointwiseConvergenceCLM.continuousSMul). Passing from E →SL[σ] F to its pointwise-convergence copy is injective (ContinuousLinearMap.toPointwiseConvergenceCLM_injective).

instance PointwiseConvergenceCLM.continuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {M : Type u_3} {E : Type u_4} {F : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₂ F] [Monoid M] [TopologicalSpace M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [ContinuousSMul M F] : ContinuousSMul M (E →SLₚₜ[σ] F)

Scalar multiplication is jointly continuous for the topology of pointwise convergence, since it is computed pointwise.

theorem ContinuousLinearMap.toPointwiseConvergenceCLM_injective {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [ContinuousSMul 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₂ F] [ContinuousConstSMul 𝕜₂ F] : Function.Injective ⇑(toPointwiseConvergenceCLM 𝕜₂ σ E F)

Passing to the topology of pointwise convergence does not identify distinct maps.