Theorems · Theorem · group theory

Rep.coindResAdjunction_homEquiv_apply

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S)
  {B : Rep.{max (max u v) w, u, v} k G} (f : Rep.coind.{u, v, v, max (max u v) w} S.subtype A ⟶ B),
  ((Rep.coindResAdjunction k S).homEquiv A B) f =
    (Rep.indResHomEquiv S.subtype A B) (CategoryTheory.CategoryStruct.comp A.indCoindIso.hom f)

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableRelSubgroup.FiniteIndex