Theorems · Theorem · group theory

groupCohomology.mapIso_inv

∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (e : G ≃* H) (e' : ↑B ≃ₗ[k] ↑A) (he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') (n : ℕ),
  (groupCohomology.mapIso e e' he n).inv =
    groupCohomology.map (↑e) (Rep.ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup