Theorems · Theorem · category theory

AlgebraicTopology.alternatingFaceMapComplex_obj_d

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  ((AlgebraicTopology.alternatingFaceMapComplex C).obj X).d (n + 1) n =
    AlgebraicTopology.AlternatingFaceMapComplex.objD X n

Defined in: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Cited by: 3 results in Mathlib
Foundations: Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Preadditive

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites17

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
Quiver.Homstatement · cited by 32,603
CategoryTheory.Functor.objstatement · cited by 19,642
Oppositestatement · cited by 8,081
Finset.sumproof · cited by 5,195
Finset.univproof · cited by 3,473
CategoryTheory.Preadditivestatement and proof · cited by 3,309
SimplexCategorystatement · cited by 2,204
HomologicalComplex.Xstatement · cited by 1,839
ComplexShape.downstatement · cited by 605
HomologicalComplex.dstatement · cited by 598
CategoryTheory.SimplicialObjectstatement and proof · cited by 548

Cited by3

Results whose statement or proof uses this declaration.

AlgebraicTopology.map_alternatingFaceMapComplexproof · cited by 1
Rep.standardComplex.d_eqproof · cited by 1
SSet.ιChainComplex_dproof · cited by 1