Continuous and algebraic intertwiners

For finite-dimensional Hausdorff topological vector spaces, automatic continuity identifies continuous intertwiners and equivalences with their algebraic counterparts. The object and character side is already supplied by the universe-polymorphic FDRep.ofShrink, FDRep.ofShrinkEquiv, and FDRep.character_ofShrink; this file adds only the missing intertwiner side.

Main declarations

• ContIntertwiningMap.toIntertwiningMap_apply: the algebraic intertwiner underlying a continuous one has the same values.
• ContRepresentation.intertwiningMapEquiv: continuous intertwiners are linearly equivalent to algebraic intertwiners.
• ContRepresentation.nonempty_equiv_iff: continuous and algebraic representation equivalence agree.

References

• Representations of compact groups and the Peter-Weyl theorem, continuous-representation-to-FDRep correspondence.

@[simp]

theorem ContIntertwiningMap.toIntertwiningMap_apply {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [Monoid G] {V : Type w} {W : Type x} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} (f : ContIntertwiningMap π ρ) (v : V) : f.toIntertwiningMap v = f v

Evaluation of the algebraic intertwining map underlying a continuous one: forgetting continuity does not change the map.

noncomputable def ContRepresentation.intertwiningMapEquiv {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} {W : Type x} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} : ContIntertwiningMap π ρ ≃ₗ[𝕜] (toRepresentation 𝕜 G V π).IntertwiningMap (toRepresentation 𝕜 G W ρ)

In finite dimensions, forgetting continuity identifies continuous intertwining maps with algebraic intertwining maps. The inverse equips the underlying linear map with its automatic continuity.

Equations

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

theorem ContRepresentation.intertwiningMapEquiv_apply {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} {W : Type x} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} (f : ContIntertwiningMap π ρ) : intertwiningMapEquiv f = f.toIntertwiningMap

The forward intertwiner identification is the existing forgetful map.

@[simp]

theorem ContRepresentation.intertwiningMapEquiv_apply_apply {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} {W : Type x} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} (f : ContIntertwiningMap π ρ) (v : V) : (intertwiningMapEquiv f) v = f v

The forward intertwiner identification preserves pointwise evaluation.

@[simp]

theorem ContRepresentation.intertwiningMapEquiv_symm_apply_apply {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} {W : Type x} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} (f : (toRepresentation 𝕜 G V π).IntertwiningMap (toRepresentation 𝕜 G W ρ)) (v : V) : (intertwiningMapEquiv.symm f) v = f v

The inverse intertwiner identification preserves pointwise evaluation.

@[simp]

theorem ContRepresentation.intertwiningMapEquiv_id {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} : intertwiningMapEquiv ContIntertwiningMap.id = Representation.IntertwiningMap.id (toRepresentation 𝕜 G V π)

The intertwiner identification preserves identity maps.

@[simp]

theorem ContRepresentation.intertwiningMapEquiv_comp {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} {W : Type x} {U : Type y} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] [AddCommGroup U] [Module 𝕜 U] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul 𝕜 U] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} {τ : ContRepresentation 𝕜 G U} [T2Space W] [FiniteDimensional 𝕜 W] (f : ContIntertwiningMap ρ τ) (g : ContIntertwiningMap π ρ) : intertwiningMapEquiv (f.comp g) = (intertwiningMapEquiv f).comp (intertwiningMapEquiv g)

The intertwiner identification preserves composition.

@[simp]

theorem ContRepresentation.intertwiningMapEquiv_symm_id {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} : intertwiningMapEquiv.symm (Representation.IntertwiningMap.id (toRepresentation 𝕜 G V π)) = ContIntertwiningMap.id

The inverse intertwiner identification preserves identity maps.

@[simp]

theorem ContRepresentation.intertwiningMapEquiv_symm_comp {𝕜 : Type u} {G : Type v} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] {V : Type w} {W : Type x} {U : Type y} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] [AddCommGroup U] [Module 𝕜 U] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul 𝕜 U] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} {τ : ContRepresentation 𝕜 G U} [T2Space W] [FiniteDimensional 𝕜 W] (f : (toRepresentation 𝕜 G W ρ).IntertwiningMap (toRepresentation 𝕜 G U τ)) (g : (toRepresentation 𝕜 G V π).IntertwiningMap (toRepresentation 𝕜 G W ρ)) : intertwiningMapEquiv.symm (f.comp g) = (intertwiningMapEquiv.symm f).comp (intertwiningMapEquiv.symm g)

The inverse intertwiner identification preserves composition.

theorem ContRepresentation.nonempty_equiv_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] [T2Space W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} : Nonempty (π.Equiv ρ) ↔ Nonempty ((toRepresentation 𝕜 G V π).Equiv (toRepresentation 𝕜 G W ρ))

Two finite-dimensional Hausdorff continuous representations over a complete field are continuously equivalent exactly when their underlying algebraic representations are equivalent.