Theorems · Definition · group theory

Rep.resIndAdjunction

(k : Type u) →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            [S.FiniteIndex] → Rep.resFunctor S.subtype ⊣ Rep.indFunctor k S.subtype

Given a finite index subgroup S ≤ G, Ind_S^G is right adjoint to the restriction functor Res k G ⥤ Res k S, since it is naturally isomorphic to Coind_S^G.

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

4 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingGroupDecidableRelSubgroup.FiniteIndex