Theorems · Definition · group theory

groupCohomology.mapIso

{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) →
                (∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') → (n : ℕ) → groupCohomology B n ≅ groupCohomology A n

The isomorphism between cohomology groups induced by a group isomorphism e : G ≃* H and a isomorphism between representations (restricted by e).

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup