Theorems · Definition · category theory
AlgebraicTopology.AlternatingFaceMapComplex.obj
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.SimplicialObject C → ChainComplex C ℕThe alternating face map complex, on objects
- Cited by
- 146 results in Mathlib
- Foundations
- Depth 71 from the axioms, rests on 1,980 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- CategoryTheory.SimplicialObjectstatement and proof · cited by 548
- ChainComplexstatement · cited by 350
- AlgebraicTopology.AlternatingFaceMapComplex.objDproof · cited by 5
- ChainComplex.ofproof · cited by 4
- AlgebraicTopology.AlternatingFaceMapComplex.d_squaredproof · cited by 1
Cited by167
Results whose statement or proof uses this declaration.
- AlgebraicTopology.DoldKan.PInftystatement · cited by 94
- AlgebraicTopology.DoldKan.N₁proof · cited by 43
- AlgebraicTopology.DoldKan.Pstatement · cited by 38
- AlgebraicTopology.alternatingFaceMapComplexproof · cited by 25
- AlgebraicTopology.DoldKan.QInftystatement and proof · cited by 20
- AlgebraicTopology.DoldKan.Qstatement and proof · cited by 18
- AlgebraicTopology.DoldKan.Hσstatement · cited by 13
- AlgebraicTopology.DoldKan.hσ'statement · cited by 12
- AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplexstatement · cited by 10
- CategoryTheory.SimplicialObject.Splitting.toNondegComplexstatement · cited by 9
- AlgebraicTopology.DoldKan.HigherFacesVanish.of_Pstatement · cited by 7
- AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eqstatement · cited by 7