Documentation

Mathlib.RepresentationTheory.Induced

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 #

@[reducible, inline]
abbrev Representation.IndV {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) :
Type (max u_4 u_1 u_3)

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
Instances For
    @[reducible, inline]
    noncomputable abbrev Representation.IndV.mk {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) :
    A →ₗ[k] IndV φ ρ

    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
      theorem Representation.IndV.hom_ext {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] (ρ : Representation k G A) [AddCommGroup B] [Module k B] {f g : IndV φ ρ →ₗ[k] B} (hfg : ∀ (h : H), f ∘ₗ mk φ ρ h = g ∘ₗ mk φ ρ h) :
      f = g
      theorem Representation.IndV.hom_ext_iff {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] {φ : G →* H} {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] {ρ : Representation k G A} [AddCommGroup B] [Module k B] {f g : IndV φ ρ →ₗ[k] B} :
      f = g ∀ (h : H), f ∘ₗ mk φ ρ h = g ∘ₗ mk φ ρ h
      noncomputable def Representation.ind {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) :
      Representation k H (IndV φ ρ)

      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
        @[simp]
        theorem Representation.ind_apply {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) :
        (ind φ ρ) h = Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (LinearMap.rTensor A (Finsupp.lmapDomain k k fun (x : H) => x * h⁻¹))
        theorem Representation.ind_mk {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h₁ h₂ : H) (a : A) :
        ((ind φ ρ) h₁) ((IndV.mk φ ρ h₂) a) = (IndV.mk φ ρ (h₂ * h₁⁻¹)) a
        @[reducible, inline]
        noncomputable abbrev Rep.ind {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) :
        Rep k H

        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
        Instances For
          noncomputable def Rep.indMap {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A B : Rep k G} (f : A B) :
          ind φ A ind φ B

          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
            noncomputable def Rep.indFunctor (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) :

            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
            Instances For
              @[simp]
              theorem Rep.indFunctor_obj (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) :
              (indFunctor k φ).obj A = ind φ A
              @[simp]
              theorem Rep.indFunctor_map (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {X✝ Y✝ : Rep k G} (f : X✝ Y✝) :
              (indFunctor k φ).map f = indMap φ f
              noncomputable def Rep.indResHomEquiv {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) :
              (ind φ A B) ≃ₗ[k] A (Action.res (ModuleCat k) φ).obj B

              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
                @[simp]
                @[simp]
                theorem Rep.indResHomEquiv_apply_hom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) (f : ind φ A B) :
                noncomputable def Rep.indResAdjunction (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) :

                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
                  @[simp]
                  theorem Rep.indResAdjunction_unit_app_hom_hom (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) :
                  instance Rep.instIsLeftAdjointIndFunctor {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) :
                  noncomputable def Rep.coinvariantsTensorIndHom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) :

                  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
                    theorem Rep.coinvariantsTensorIndHom_mk_tmul_indVMk {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Rep k G} {B : Rep k H} (h : H) (x : A.V) (y : B.V) :
                    noncomputable def Rep.coinvariantsTensorIndInv {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) :

                    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
                      theorem Rep.coinvariantsTensorIndInv_mk_tmul_indMk {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Rep k G} {B : Rep k H} (x : A.V) (y : B.V) :
                      noncomputable def Rep.coinvariantsTensorIndIso {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) :

                      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
                      Instances For
                        @[simp]
                        theorem Rep.coinvariantsTensorIndIso_inv {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) :
                        @[simp]
                        theorem Rep.coinvariantsTensorIndIso_hom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) :
                        noncomputable def Rep.coinvariantsTensorIndNatIso {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) :

                        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
                        Instances For
                          @[simp]
                          theorem Rep.coinvariantsTensorIndNatIso_inv_app {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (X : Rep k H) :
                          @[simp]
                          theorem Rep.coinvariantsTensorIndNatIso_hom_app {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (X : Rep k H) :