Theorems · Definition · group theory

groupHomology.cyclesMap

{k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (n : ℕ) → groupHomology.cycles A n ⟶ groupHomology.cycles B n

Given a group homomorphism f : G →* H and a representation morphism φ : A ⟶ Res(f)(B), this is the induced map Zₙ(G, A) ⟶ Zₙ(H, B) sending ∑ aᵢ·gᵢ : Gⁿ →₀ A to ∑ φ(aᵢ)·(f ∘ gᵢ) : Hⁿ →₀ B.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Cited by

21 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup