Theorems · Definition · group theory

Rep.standardComplex.xIso

(k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] → (n : ℕ) → (Rep.standardComplex k G).X n ≅ Rep.ofMulAction k G (Fin (n + 1) → G)

The nth object of the standard resolution of k is definitionally isomorphic to k[Gⁿ⁺¹] equipped with the representation induced by the diagonal action of G.

Defined in: Mathlib.RepresentationTheory.Homological.Resolution
Cited by: 0 results in Mathlib
Foundations: Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
CategoryTheory.Isostatement · cited by 3,963
Monoidstatement and proof · cited by 3,887
HomologicalComplex.Xstatement and proof · cited by 1,839
Repstatement · cited by 843
CategoryTheory.Iso.reflproof · cited by 727
ComplexShape.downstatement · cited by 605
Rep.standardComplexstatement and proof · cited by 6
Rep.ofMulActionstatement · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.