Theorems · Definition · group theory

groupHomology.coinfNatTrans

(k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [inst_2 : S.Normal] →
            (n : ℕ) →
              groupHomology.functor k G n ⟶
                (Rep.quotientToCoinvariantsFunctor k S).comp (groupHomology.functor k (G ⧸ S) n)

Given a normal subgroup S ≤ G, this sends A : Rep k G to the nth "coinflation" map Hₙ(G, A) ⟶ Hₙ(G ⧸ S, A_S) induced by the quotient maps G →* G ⧸ S and A →ₗ A_S.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupSubgroup.Normal