Theorems · Theorem · group theory

Representation.Coinvariants.map_comp

∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {X : Type u_5} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddCommGroup X] [inst_7 : Module k X] {ρ : Representation k G V} {τ : Representation k G W}
  (υ : Representation k G X) (φ : ρ.IntertwiningMap τ) (ψ : τ.IntertwiningMap υ),
  Representation.Coinvariants.map τ υ ψ ∘ₗ Representation.Coinvariants.map ρ τ φ =
    Representation.Coinvariants.map ρ υ (ψ.comp φ)

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingMonoidAddCommGroupModuleAddCommGroupModuleAddCommGroupModule