Strong topologies on the space of continuous linear maps

In this file, we define the strong topologies on E →L[𝕜] F associated with a family 𝔖 : Set (Set E) to be the topology of uniform convergence on the elements of 𝔖 (also called the topology of 𝔖-convergence).

The lemma UniformOnFun.continuousSMul_of_image_bounded tells us that this is a vector space topology if the continuous linear image of any element of 𝔖 is bounded (in the sense of Bornology.IsVonNBounded).

We then declare an instance for the case where 𝔖 is exactly the set of all bounded subsets of E, giving us the so-called "topology of uniform convergence on bounded sets" (or "topology of bounded convergence"), which coincides with the operator norm topology in the case of NormedSpaces.

Other useful examples include the weak-* topology (when 𝔖 is the set of finite sets or the set of singletons) and the topology of compact convergence (when 𝔖 is the set of relatively compact sets).

Main definitions

• ContinuousLinearMap.strongTopology is the topology mentioned above for an arbitrary 𝔖.
• ContinuousLinearMap.topologicalSpace is the topology of bounded convergence. This is declared as an instance.

Main statements

• ContinuousLinearMap.strongTopology.topologicalAddGroup and ContinuousLinearMap.strongTopology.continuousSMul show that the strong topology makes E →L[𝕜] F a topological vector space, with the assumptions on 𝔖 mentioned above.
• ContinuousLinearMap.topologicalAddGroup and ContinuousLinearMap.continuousSMul register these facts as instances for the special case of bounded convergence.

References

• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

TODO

• add a type alias for continuous linear maps with the topology of 𝔖-convergence?

Tags

uniform convergence, bounded convergence

def ContinuousLinearMap.strongTopology {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalSpace (E →SL[σ] F)

Given E and F two topological vector spaces and 𝔖 : Set (Set E), then strongTopology σ F 𝔖 is the "topology of uniform convergence on the elements of 𝔖" on E →L[𝕜] F.

If the continuous linear image of any element of 𝔖 is bounded, this makes E →L[𝕜] F a topological vector space.

Equations

• ContinuousLinearMap.strongTopology σ F 𝔖 = TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖)

def ContinuousLinearMap.strongUniformity {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformSpace (E →SL[σ] F)

The uniform structure associated with ContinuousLinearMap.strongTopology. We make sure that this has nice definitional properties.

Equations

• ContinuousLinearMap.strongUniformity σ F 𝔖 = UniformSpace.replaceTopology (UniformSpace.comap DFunLike.coe (UniformOnFun.uniformSpace E F 𝔖)) ⋯

@[simp]

theorem ContinuousLinearMap.strongUniformity_topology_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformSpace.toTopologicalSpace = ContinuousLinearMap.strongTopology σ F 𝔖

theorem ContinuousLinearMap.strongUniformity.uniformEmbedding_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformEmbedding DFunLike.coe

theorem ContinuousLinearMap.strongTopology.embedding_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : Embedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

theorem ContinuousLinearMap.strongUniformity.uniformAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformAddGroup (E →SL[σ] F)

theorem ContinuousLinearMap.strongTopology.topologicalAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalAddGroup (E →SL[σ] F)

theorem ContinuousLinearMap.strongTopology.t2Space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] [T2Space F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) : T2Space (E →SL[σ] F)

theorem ContinuousLinearMap.strongTopology.continuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] (𝔖 : Set (Set E)) (h𝔖₃ : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S) : ContinuousSMul 𝕜₂ (E →SL[σ] F)

theorem ContinuousLinearMap.strongTopology.hasBasis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] {ι : Type u_7} (𝔖 : Set (Set E)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun (x x_1 : Set E) => x ⊆ x_1) 𝔖) {p : ι → Prop} {b : ι → Set F} (h : Filter.HasBasis (nhds 0) p b) : Filter.HasBasis (nhds 0) (fun (Si : Set E × ι) => Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Set E × ι) => {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem ContinuousLinearMap.strongTopology.hasBasis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun (x x_1 : Set E) => x ⊆ x_1) 𝔖) : Filter.HasBasis (nhds 0) (fun (SV : Set E × Set F) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}

theorem ContinuousLinearMap.strongTopology.uniformContinuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] (M : Type u_7) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) : UniformContinuousConstSMul M (E →SL[σ] F)

theorem ContinuousLinearMap.strongTopology.continuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] (M : Type u_7) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : ContinuousConstSMul M (E →SL[σ] F)

instance ContinuousLinearMap.topologicalSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] : TopologicalSpace (E →SL[σ] F)

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.

Equations

• ContinuousLinearMap.topologicalSpace = ContinuousLinearMap.strongTopology σ F {S : Set E | Bornology.IsVonNBounded 𝕜₁ S}

instance ContinuousLinearMap.topologicalAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] : TopologicalAddGroup (E →SL[σ] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMap.continuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (E →SL[σ] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMap.uniformSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] : UniformSpace (E →SL[σ] F)

Equations

• ContinuousLinearMap.uniformSpace = ContinuousLinearMap.strongUniformity σ F {S : Set E | Bornology.IsVonNBounded 𝕜₁ S}

instance ContinuousLinearMap.uniformAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [UniformAddGroup F] : UniformAddGroup (E →SL[σ] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMap.instT2SpaceContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToSemiringToDivisionSemiringToSemifieldToFieldToAddCommMonoidToAddCommMonoidTopologicalSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] : T2Space (E →SL[σ] F)

Equations

• ⋯ = ⋯

theorem ContinuousLinearMap.hasBasis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] {ι : Type u_9} {p : ι → Prop} {b : ι → Set F} (h : Filter.HasBasis (nhds 0) p b) : Filter.HasBasis (nhds 0) (fun (Si : Set E × ι) => Bornology.IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2) fun (Si : Set E × ι) => {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem ContinuousLinearMap.hasBasis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup F] : Filter.HasBasis (nhds 0) (fun (SV : Set E × Set F) => Bornology.IsVonNBounded 𝕜₁ SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}

instance ContinuousLinearMap.uniformContinuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] {M : Type u_9} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] : UniformContinuousConstSMul M (E →SL[σ] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMap.continuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] {M : Type u_9} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] : ContinuousConstSMul M (E →SL[σ] F)

Equations

• ⋯ = ⋯

@[simp]

theorem ContinuousLinearMap.precomp_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) : (ContinuousLinearMap.precomp G L) f = ContinuousLinearMap.comp f L

@[simp]

theorem ContinuousLinearMap.precomp_toFun {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) : (ContinuousLinearMap.precomp G L) f = ContinuousLinearMap.comp f L

def ContinuousLinearMap.precomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) : (F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G

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.

Equations

• ContinuousLinearMap.precomp G L = { toLinearMap := { toAddHom := { toFun := fun (f : F →SL[τ] G) => ContinuousLinearMap.comp f L, map_add' := ⋯ }, map_smul' := ⋯ }, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.postcomp_toFun {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F) : (ContinuousLinearMap.postcomp E L) f = ContinuousLinearMap.comp L f

@[simp]

theorem ContinuousLinearMap.postcomp_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F) : (ContinuousLinearMap.postcomp E L) f = ContinuousLinearMap.comp L f

def ContinuousLinearMap.postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : (E →SL[σ] F) →SL[τ] E →SL[ρ] G

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.

Equations

• ContinuousLinearMap.postcomp E L = { toLinearMap := { toAddHom := { toFun := fun (f : E →SL[σ] F) => ContinuousLinearMap.comp L f, map_add' := ⋯ }, map_smul' := ⋯ }, cont := ⋯ }

def ContinuousLinearMap.toLinearMap₂ {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) : E →ₗ[𝕜] F →ₗ[𝕜] G

Send a continuous bilinear map to an abstract bilinear map (forgetting continuity).

Equations

• ContinuousLinearMap.toLinearMap₂ L = LinearMap.comp (ContinuousLinearMap.coeLM 𝕜) ↑L

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : E →SL[σ₁₄] H) : (ContinuousLinearEquiv.arrowCongrSL e₁₂ e₄₃) L = ContinuousLinearMap.comp (↑e₄₃) (ContinuousLinearMap.comp L ↑(ContinuousLinearEquiv.symm e₁₂))

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : F →SL[σ₂₃] G) : (ContinuousLinearEquiv.symm (ContinuousLinearEquiv.arrowCongrSL e₁₂ e₄₃)) L = ContinuousLinearMap.comp (↑(ContinuousLinearEquiv.symm e₄₃)) (ContinuousLinearMap.comp L ↑e₁₂)

def ContinuousLinearEquiv.arrowCongrSL {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G

A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps.

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : E →SL[σ₁₄] H) : (ContinuousLinearEquiv.arrowCongrSL e₁₂ e₄₃).toLinearEquiv L = ContinuousLinearMap.comp (↑e₄₃) (ContinuousLinearMap.comp L ↑(ContinuousLinearEquiv.symm e₁₂))

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : F →SL[σ₂₃] G) : (LinearEquiv.symm (ContinuousLinearEquiv.arrowCongrSL e₁₂ e₄₃).toLinearEquiv) L = ContinuousLinearMap.comp (↑(ContinuousLinearEquiv.symm e₄₃)) (ContinuousLinearMap.comp L ↑e₁₂)

def ContinuousLinearEquiv.arrowCongr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G

A pair of continuous linear equivalences generates a continuous linear equivalence between the spaces of continuous linear maps.

Equations

• ContinuousLinearEquiv.arrowCongr e₁ e₂ = ContinuousLinearEquiv.arrowCongrSL e₁ e₂