Theorems · Definition · group theory
Rep.standardComplex
(k G : Type u) → [inst : CommRing k] → [inst_1 : Monoid G] → ChainComplex (Rep.{u, u, u} k G) ℕThe standard resolution of k as a trivial representation, defined as the alternating
face map complex of a simplicial k-linear G-representation.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- CategoryTheory.Functor.objproof · cited by 19,642
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functor.compproof · cited by 6,529
- Monoidstatement and proof · cited by 3,887
- Repstatement and proof · cited by 843
- ChainComplexstatement · cited by 350
- AlgebraicTopology.alternatingFaceMapComplexproof · cited by 25
- Rep.linearizationproof · cited by 13
- classifyingSpaceUniversalCoverproof · cited by 4
Cited by12
Results whose statement or proof uses this declaration.
- Rep.standardComplex.forget₂ToModuleCatproof · cited by 3
- Rep.standardComplex.εToSingle₀statement and proof · cited by 2
- Rep.standardComplex.d_eqstatement and proof · cited by 1
- Rep.standardComplex.d_applystatement and proof · cited by 1
- Rep.standardComplex.quasiIso_forget₂_εToSingle₀statement · cited by 0
- Rep.standardComplex.xIsostatement and proof · cited by 0
- Rep.standardComplex.εToSingle₀_comp_eqstatement · cited by 0
- Rep.standardResolution.extIsostatement · cited by 0
- Rep.standardResolutionproof · cited by 0
- Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eqstatement and proof · cited by 0
- Rep.barComplex.isoStandardComplexstatement · cited by 0
- Rep.standardComplex.d_comp_εstatement and proof · cited by 0