Documentation

Mathlib.Topology.Algebra.Module.StrongTopology

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 #

Main statements #

References #

TODO #

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)) :

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
Instances For
    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)) :

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

    Equations
    Instances For
      @[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)) :
      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)) :
      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) :
      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)) :
      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)) :
      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] :

      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
      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] :
      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] :
      Equations
      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] :
      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] :
      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] :
      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] :
      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) :
      @[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) :
      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
      Instances For
        @[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) :
        @[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) :
        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
        Instances For
          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
          Instances For
            @[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) :
            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.
            Instances For
              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
              Instances For