Mathlib Map

Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : C) → (CategoryTheory.SimplicialObject.Augmented.const.obj X).ExtraDegeneracy

The constant augmented simplicial object has an extra degeneracy.

Defined in
Mathlib.AlgebraicTopology.ExtraDegeneracy
Cited by
2 results in Mathlib
Foundations
Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s · cited by 0ExtraDegeneracy.const_sCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s' · cited by 0ExtraDegeneracy.const_s'ChainComplex.alternatingConstHomotopyEquiv · cited by 0ChainComplex.alternatingC…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Functor.obj · cited by 19642Functor.objCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.Comma.left · cited by 886Comma.leftCategoryTheory.Comma.right · cited by 727Comma.rightCategoryTheory.SimplicialObject.Augmented · cited by 113SimplicialObject.AugmentedCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy · cited by 24Augmented.ExtraDegeneracyCategoryTheory.SimplicialObject.Augmented.const · cited by 7Augmented.constExtraDegeneracy.constCITED BYCITES

Cites8

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

Cited by3

Results whose statement or proof uses this declaration.