Intertwining maps: images, and the action of the monoid algebra

Mathlib records the image of an intertwining map as a subrepresentation (Representation.IntertwiningMap.range) and turns a bijective intertwining map into an equivalence (Representation.IntertwiningMap.ofBijective), but it does not connect the two: an injective intertwining map is an isomorphism onto its image, and that is the usual way a construction "W is the subrepresentation cut out by such and such an operator" is turned into an identification of W with a representation built independently.

This file supplies the corestriction and that identification. The subrepresentation is taken as an argument together with a proof that the image fills it, rather than being fixed to be IntertwiningMap.range f: in practice the target subrepresentation is defined some other way -- as the range of a different operator, say -- and matching the two ranges is a separate step that the caller has already done.

Main definitions

• Representation.IntertwiningMap.codRestrict: corestrict an intertwining map to a subrepresentation containing its image.
• Representation.IntertwiningMap.equivOfRange: an injective intertwining map is an equivalence onto a subrepresentation that its image fills.
• Representation.IntertwiningMap.lcomp: precomposition with an intertwining map, as an intertwining map of the conjugation representations Representation.linHom.

Main results

• Representation.IntertwiningMap.apply_asAlgebraHom: an intertwining map commutes with the action of the monoid algebra, not only with that of the group elements.

def Representation.IntertwiningMap.codRestrict {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (f : ρ.IntertwiningMap σ) (P : Subrepresentation σ) (hP : ∀ (v : V), f v ∈ P.toSubmodule) : ρ.IntertwiningMap P.toRepresentation

Corestrict an intertwining map to a subrepresentation of the target containing its image.

Equations

• f.codRestrict P hP = { toLinearMap := LinearMap.codRestrict P.toSubmodule f.toLinearMap hP, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.codRestrict_apply_coe {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (f : ρ.IntertwiningMap σ) (P : Subrepresentation σ) (hP : ∀ (v : V), f v ∈ P.toSubmodule) (v : V) : ↑((f.codRestrict P hP) v) = f v

noncomputable def Representation.IntertwiningMap.equivOfRange {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (f : ρ.IntertwiningMap σ) (hf : Function.Injective ⇑f) {P : Subrepresentation σ} (hP : f.range = P.toSubmodule) : ρ.Equiv P.toRepresentation

An injective intertwining map is an isomorphism onto its image, here onto any subrepresentation P that the image fills.

Equations

• f.equivOfRange hf hP = (f.codRestrict P ⋯).ofBijective ⋯

@[simp]

theorem Representation.IntertwiningMap.apply_asAlgebraHom {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (f : ρ.IntertwiningMap σ) (r : MonoidAlgebra A G) (v : V) : f ((ρ.asAlgebraHom r) v) = (σ.asAlgebraHom r) (f v)

An intertwining map commutes with the action of the monoid algebra, not only with that of the group elements.

@[simp]

theorem Representation.IntertwiningMap.equivOfRange_apply_coe {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (f : ρ.IntertwiningMap σ) (hf : Function.Injective ⇑f) {P : Subrepresentation σ} (hP : f.range = P.toSubmodule) (v : V) : ↑((f.equivOfRange hf hP) v) = f v

def Representation.IntertwiningMap.lcomp {A : Type u_5} {G : Type u_6} {V : Type u_7} {V' : Type u_8} {W : Type u_9} [CommSemiring A] [Group G] [AddCommMonoid V] [Module A V] [AddCommMonoid V'] [Module A V'] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {ρ' : Representation A G V'} (u : ρ'.IntertwiningMap ρ) (σ : Representation A G W) : (ρ.linHom σ).IntertwiningMap (ρ'.linHom σ)

Precomposition with an intertwining map. An intertwining map u : ρ' → ρ induces the intertwining map φ ↦ φ ∘ u from the conjugation representation linHom ρ σ to linHom ρ' σ.

Equations

• u.lcomp σ = { toLinearMap := LinearMap.lcomp A W u.toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.lcomp_apply {A : Type u_5} {G : Type u_6} {V : Type u_7} {V' : Type u_8} {W : Type u_9} [CommSemiring A] [Group G] [AddCommMonoid V] [Module A V] [AddCommMonoid V'] [Module A V'] [AddCommMonoid W] [Module A W] {ρ : Representation A G V} {ρ' : Representation A G V'} (u : ρ'.IntertwiningMap ρ) (σ : Representation A G W) (φ : V →ₗ[A] W) : (u.lcomp σ) φ = φ ∘ₗ u.toLinearMap