Contragredient duality for representations

Dualizing an equivariant linear map gives an equivariant map in the reverse direction. These maps supply contragredient functors on categories of representations. For a representation on a reflexive module, evaluation identifies the representation with its double dual, naturally in the representation. In particular this applies to finite free integral representations.

@[reducible, inline]

abbrev Rep.dual {R : Type u} [CommRing R] {G : Type v} [Group G] (V : Rep R G) : Rep R G

The contragredient representation on the linear dual of the stored module.

Equations

• V.dual = Rep.of V.ρ.dual

def Rep.dualMap {R : Type u} [CommRing R] {G : Type v} [Group G] {V W : Rep R G} (f : V ⟶ W) : W.dual ⟶ V.dual

The transpose of an equivariant map, with the contragredient actions on both duals.

Equations

• Rep.dualMap f = Rep.ofHom (let __LinearMap := (Rep.Hom.hom f).dualMap; { toLinearMap := __LinearMap, isIntertwining' := ⋯ })

@[simp]

theorem Rep.dualMap_hom_apply {R : Type u} [CommRing R] {G : Type v} [Group G] {V W : Rep R G} (f : V ⟶ W) (φ : Module.Dual R ↑W) (x : ↑V) : ((Hom.hom (dualMap f)) φ) x = φ ((Hom.hom f) x)

@[simp]

theorem Rep.dualMap_id {R : Type u} [CommRing R] {G : Type v} [Group G] (V : Rep R G) : dualMap (CategoryTheory.CategoryStruct.id V) = CategoryTheory.CategoryStruct.id V.dual

Transposing the identity representation morphism gives the identity.

@[simp]

theorem Rep.dualMap_comp {R : Type u} [CommRing R] {G : Type v} [Group G] {U V W : Rep R G} (f : U ⟶ V) (g : V ⟶ W) : dualMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (dualMap g) (dualMap f)

Transposing a composite reverses the order of its factors.

@[simp]

theorem Rep.dualMap_eqToHom {R : Type u} [CommRing R] {G : Type v} [Group G] {V W : Rep R G} (h : V = W) : dualMap (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯

Transposing a transport morphism reverses the transport on dual representations.

noncomputable def Rep.doubleDualIso {R : Type u} [CommRing R] {G : Type v} [Group G] (V : Rep R G) [Module.IsReflexive R ↑V] : V ≅ V.dual.dual

Evaluation identifies a representation on a reflexive module with its double dual.

Equations

• V.doubleDualIso = Rep.mkIso (Representation.Equiv.mk (Module.evalEquiv R ↑V) ⋯)

@[simp]

theorem Rep.doubleDualIso_hom_apply {R : Type u} [CommRing R] {G : Type v} [Group G] (V : Rep R G) [Module.IsReflexive R ↑V] (x : ↑V) (φ : Module.Dual R ↑V) : ((Hom.hom V.doubleDualIso.hom) x) φ = φ x

theorem Rep.doubleDualIso_naturality {R : Type u} [CommRing R] {G : Type v} [Group G] {V W : Rep R G} [Module.IsReflexive R ↑V] [Module.IsReflexive R ↑W] (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f W.doubleDualIso.hom = CategoryTheory.CategoryStruct.comp V.doubleDualIso.hom (dualMap (dualMap f))

Evaluation into the double dual is natural on reflexive representations.

theorem Rep.doubleDualIso_naturality_assoc {R : Type u} [CommRing R] {G : Type v} [Group G] {V W : Rep R G} [Module.IsReflexive R ↑V] [Module.IsReflexive R ↑W] (f : V ⟶ W) {Z : Rep R G} (h : W.dual.dual ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp W.doubleDualIso.hom h) = CategoryTheory.CategoryStruct.comp V.doubleDualIso.hom (CategoryTheory.CategoryStruct.comp (dualMap (dualMap f)) h)

Evaluation into the double dual is natural on reflexive representations.