Theorems · Definition · group theory

groupCohomology.resNatTrans

(k : Type u) →
  {G H : Type u} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (f : G →* H) →
            (n : ℕ) → groupCohomology.functor k H n ⟶ (Rep.resFunctor f).comp (groupCohomology.functor k G n)

Given a group homomorphism f : G →* H, this is a natural transformation between the functors sending A : Rep k H to Hⁿ(H, A) and to Hⁿ(G, Res(f)(A)).

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup