Restricting a continuous representation to an invariant submodule

This file restricts a continuous representation of a monoid to a submodule preserved by every action operator, the continuous counterpart of Mathlib's Representation.subrepresentation.

Main definitions

• ContRepresentation.subrepresentation: the restriction of a continuous representation to an invariant submodule.
• ContRepresentation.subrepresentationInclusion: the continuous intertwiner including a subrepresentation into its ambient representation.

Main results

• ContRepresentation.mem_invariants_subrepresentation: a vector of the submodule is invariant for the restricted representation exactly when it is invariant for the ambient one.
• ContRepresentation.toRepresentation_subrepresentation: the underlying representation of a restricted continuous representation is the restriction of the underlying representation.
• Subrepresentation.toRepresentation_subrepresentation_toSubmodule: restricting to the submodule a subrepresentation carries has that subrepresentation's own representation underneath.
• ContRepresentation.continuous_subrepresentation: the restriction of a continuous representation to an invariant submodule is again continuous.

def ContRepresentation.subrepresentation {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (W : Submodule R V) (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) : ContRepresentation R G ↥W

The restriction of a continuous representation to an invariant submodule. This is the continuous counterpart of Representation.subrepresentation.

Equations

• π.subrepresentation W hW = { toMonoidHom := { toFun := fun (g : G) => (π g).restrict ⋯, map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem ContRepresentation.coe_subrepresentation_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {π : ContRepresentation R G V} {W : Submodule R V} {hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W} (g : G) (v : ↥W) : ↑(((π.subrepresentation W hW) g) v) = (π g) ↑v

The restricted action is the ambient action, read on the underlying vectors.

noncomputable def ContRepresentation.subrepresentationInclusion {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (σ : Subrepresentation (toRepresentation R G V π)) : ContIntertwiningMap (π.subrepresentation σ.toSubmodule ⋯) π

The inclusion of a subrepresentation into its ambient continuous representation, packaged as a continuous intertwiner.

Equations

• π.subrepresentationInclusion σ = { toContinuousLinearMap := σ.toSubmodule.subtypeL, isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.subrepresentationInclusion_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (σ : Subrepresentation (toRepresentation R G V π)) (v : ↥σ.toSubmodule) : (π.subrepresentationInclusion σ) v = ↑v

The subrepresentation inclusion sends a vector to the same vector in the ambient space.

theorem ContRepresentation.mem_invariants_subrepresentation {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {π : ContRepresentation R G V} {W : Submodule R V} {hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W} {x : ↥W} : x ∈ (π.subrepresentation W hW).invariants ↔ ↑x ∈ π.invariants

A vector of an invariant submodule is invariant for the restricted representation exactly when it is invariant for the ambient one: the restricted action is the ambient action.

@[simp]

theorem ContRepresentation.toRepresentation_subrepresentation {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {π : ContRepresentation R G V} {W : Submodule R V} {hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W} : toRepresentation R G (↥W) (π.subrepresentation W hW) = (toRepresentation R G V π).subrepresentation W ⋯

The underlying representation of a restricted continuous representation is the restriction of the underlying representation.

theorem Subrepresentation.toRepresentation_subrepresentation_toSubmodule {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {π : ContRepresentation R G V} (σ : Subrepresentation (ContRepresentation.toRepresentation R G V π)) : ContRepresentation.toRepresentation R G (↥σ.toSubmodule) (π.subrepresentation σ.toSubmodule ⋯) = σ.toRepresentation

Restricting π to the submodule a subrepresentation σ of π.toRepresentation carries has σ.toRepresentation as its underlying representation: both restrict the ambient action to the same submodule.

theorem ContRepresentation.continuous_subrepresentation {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NormedField 𝕜] [Monoid G] [TopologicalSpace G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module 𝕜 V] [ContinuousConstSMul 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} {hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W} (hπ : Continuous ⇑π) : Continuous ⇑(π.subrepresentation W hW)

Restricting a continuous representation to an invariant submodule preserves continuity: from continuity of g ↦ π g as a map into the continuous linear endomorphisms of V, the restricted action g ↦ subrepresentation π W hW g is continuous into those of W. This supplies the continuity argument that matrixCoeff and the rest of the continuous-representation API take explicitly, so a subrepresentation can be used wherever a continuous representation is expected.