Documentation

TauCeti.RepresentationTheory.Rep.Subrepresentation

The inclusion of a subrepresentation as a morphism of Rep k G #

The inclusion Subrepresentation.subtype W of a subrepresentation W of ρ is an intertwining map, so Rep.ofHom W.subtype is a morphism of Rep k G into Rep.of ρ. This file records how the categorical properties of that morphism read off W: it is always a monomorphism, it is zero exactly when W = ⊥, and it is an isomorphism exactly when W = ⊤. These are the facts through which simplicity of an object of Rep k G or FDRep k G is compared with irreducibility of the representation it carries.

Main results #

Implementation notes #

Although Rep k G is defined over a Semiring k, forming Rep.of W.toRepresentation requires the carrier ↥W.toSubmodule to carry an AddCommGroup instance. For submodules over a general semiring, subsets need not be closed under negation (e.g. ℕ ⊆ ℤ as an ℕ-submodule), so Submodule.addCommGroup and these inclusion morphisms require [Ring k].

source
instance Subrepresentation.mono_ofHom_subtype {k : Type u} {G : Type v} [Ring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] {ρ : Representation k G V} (W : Subrepresentation ρ) :
CategoryTheory.Mono (Rep.ofHom W.subtype)

The inclusion of a subrepresentation is a monomorphism of Rep k G.

source
@[simp]
theorem Subrepresentation.ofHom_subtype_eq_zero_iff {k : Type u} {G : Type v} [Ring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] {ρ : Representation k G V} (W : Subrepresentation ρ) :
Rep.ofHom W.subtype = 0 ↔ W = ⊥

The inclusion of a subrepresentation is the zero morphism of Rep k G exactly when the subrepresentation is ⊥.

source
theorem Subrepresentation.isIso_ofHom_subtype_iff {k : Type u} {G : Type v} [Ring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] {ρ : Representation k G V} (W : Subrepresentation ρ) :
CategoryTheory.IsIso (Rep.ofHom W.subtype) ↔ W = ⊤

The inclusion of a subrepresentation is an isomorphism of Rep k G exactly when the subrepresentation is ⊤.