Induced representations #
Given a commutative ring k
, a group homomorphism φ : G →* H
, and a k
-linear
G
-representation A
, this file introduces the induced representation $Ind_G^H(A)$ of A
as
an H
-representation.
By ind φ A
we mean the (k[H] ⊗[k] A)_G
with the G
-representation on k[H]
defined by φ
.
We define a representation of H
on this submodule by sending h : H
and ⟦h₁ ⊗ₜ a⟧
to
⟦h₁h⁻¹ ⊗ₜ a⟧
.
We also prove that the restriction functor Rep k H ⥤ Rep k G
along φ
is right adjoint to the
induction functor and hence that the induction functor preserves colimits.
Additionally, we show that the functor Rep k H ⥤ ModuleCat k
sending B : Rep k H
to
(Ind(φ)(A) ⊗ B))_H
is naturally isomorphic to the one sending B
to (A ⊗ Res(φ)(B))_G
. This
is used to prove Shapiro's lemma in
Mathlib/RepresentationTheory/Homological/GroupHomology/Shapiro.lean
.
Main definitions #
Representation.ind φ ρ
: given a group homomorphismφ : G →* H
, this is the induction of aG
-representation(A, ρ)
alongφ
, defined as(k[H] ⊗[k] A)_G
and withH
-action given byh • ⟦h₁ ⊗ₜ a⟧ := ⟦h₁h⁻¹ ⊗ₜ a⟧
forh, h₁ : H
,a : A
.Rep.indResAdjunction k φ
: given a group homomorphismφ : G →* H
, this is the adjunction between the induction functor alongφ
and the restriction functorRep k H ⥤ Rep k G
alongφ
.Rep.coinvariantsTensorIndNatIso φ A
: given a group homomorphismφ : G →* H
andA : Rep k G
, this is a natural isomorphism between the functor sendingB : Rep k H
to(Ind(φ)(A) ⊗ B))_H
and the one sendingB
to(A ⊗ Res(φ)(B))_G
. Used to prove Shapiro's lemma.
Given a group homomorphism φ : G →* H
and a G
-representation (A, ρ)
, this is the
k
-module (k[H] ⊗[k] A)_G
with the G
-representation on k[H]
defined by φ
.
See Representation.ind
for the induced H
-representation on IndV φ ρ
.
Equations
- Representation.IndV φ ρ = (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ).Coinvariants
Instances For
Given a group homomorphism φ : G →* H
and a G
-representation (A, ρ)
, this is the
H → A →ₗ[k] (k[H] ⊗[k] A)_G
sending h, a
to ⟦h ⊗ₜ a⟧
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group homomorphism φ : G →* H
and a G
-representation A
, this is
(k[H] ⊗[k] A)_G
equipped with the H
-representation defined by sending h : H
and ⟦h₁ ⊗ₜ a⟧
to ⟦h₁h⁻¹ ⊗ₜ a⟧
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group homomorphism φ : G →* H
and a G
-representation A
, this is
(k[H] ⊗[k] A)_G
equipped with the H
-representation defined by sending h : H
and ⟦h₁ ⊗ₜ a⟧
to ⟦h₁h⁻¹ ⊗ₜ a⟧
.
Equations
- Rep.ind φ A = Rep.of (Representation.ind φ A.ρ)
Instances For
Given a group homomorphism φ : G →* H
, a morphism of G
-representations f : A ⟶ B
induces
a morphism of H
-representations (k[H] ⊗[k] A)_G ⟶ (k[H] ⊗[k] B)_G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group homomorphism φ : G →* H
, this is the functor sending a G
-representation A
to the induced H
-representation ind φ A
, with action on maps induced by left tensoring.
Equations
- Rep.indFunctor k φ = { obj := fun (A : Rep k G) => Rep.ind φ A, map := fun {X Y : Rep k G} (f : X ⟶ Y) => Rep.indMap φ f, map_id := ⋯, map_comp := ⋯ }
Instances For
Given a group homomorphism φ : G →* H
, an H
-representation B
, and a G
-representation
A
, there is a k
-linear equivalence between the H
-representation morphisms ind φ A ⟶ B
and
the G
-representation morphisms A ⟶ B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group homomorphism φ : G →* H
, the induction functor Rep k G ⥤ Rep k H
is left
adjoint to the restriction functor along φ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group hom φ : G →* H
, A : Rep k G
and B : Rep k H
, this is the k
-linear map
(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G
sending ⟦h ⊗ₜ a⟧ ⊗ₜ b
to ⟦a ⊗ ρ(h)(b)⟧
for all
h : H
, a : A
, and b : B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group hom φ : G →* H
, A : Rep k G
and B : Rep k H
, this is the k
-linear map
(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H
sending ⟦a ⊗ₜ b⟧
to ⟦1 ⊗ₜ a⟧ ⊗ₜ b
for all
a : A
, and b : B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a group hom φ : G →* H
, A : Rep k G
and B : Rep k H
, this is the k
-linear
isomorphism (Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G
sending ⟦h ⊗ₜ a⟧ ⊗ₜ b
to ⟦a ⊗ ρ(h)(b)⟧
for all h : H
, a : A
, and b : B
.
Equations
- Rep.coinvariantsTensorIndIso φ A B = { hom := Rep.coinvariantsTensorIndHom φ A B, inv := Rep.coinvariantsTensorIndInv φ A B, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Given a group hom φ : G →* H
and A : Rep k G
, the functor Rep k H ⥤ ModuleCat k
sending
B ↦ (Ind(φ)(A) ⊗ B))_H
is naturally isomorphic to the one sending B ↦ (A ⊗ Res(φ)(B))_G
.
Equations
- Rep.coinvariantsTensorIndNatIso φ A = CategoryTheory.NatIso.ofComponents (fun (B : Rep k H) => Rep.coinvariantsTensorIndIso φ A B) ⋯