Mathlib Map

Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      X.ExtraDegeneracy → (n : ℕ) → X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })

the extra degeneracy

Defined in
Mathlib.AlgebraicTopology.ExtraDegeneracy
Cited by
13 results in Mathlib
Foundations
Depth 34 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.homotopy.h · cited by 3homotopy.hCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ext · cited by 1ExtraDegeneracy.extCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ · cited by 1ExtraDegeneracy.s_comp_δCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀ · cited by 1ExtraDegeneracy.s_comp_δ₀CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ · cited by 1ExtraDegeneracy.s_comp_σCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁ · cited by 1ExtraDegeneracy.s₀_comp_δ₁CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq · cited by 1homotopy.h_eqCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s · cited by 0ExtraDegeneracy.const_sCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ext_iff · cited by 0ExtraDegeneracy.ext_iffCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv · cited by 0ExtraDegeneracy.homotopyE…CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.map · cited by 0ExtraDegeneracy.mapCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ofIso · cited by 0ExtraDegeneracy.ofIsoCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc · cited by 0ExtraDegeneracy.s_comp_δ_…CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc · cited by 0ExtraDegeneracy.s_comp_δ₀…CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc · cited by 0ExtraDegeneracy.s_comp_σ_…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor.obj · cited by 19642Functor.objOpposite · cited by 8081OppositeCategoryTheory.Functor.id · cited by 3333Functor.idSimplexCategory · cited by 2204SimplexCategoryCategoryTheory.Comma.left · cited by 886Comma.leftCategoryTheory.SimplicialObject · cited by 548CategoryTheory.Simplicial…CategoryTheory.SimplicialObject.Augmented · cited by 113SimplicialObject.AugmentedCategoryTheory.SimplicialObject.const · cited by 110SimplicialObject.constCategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy · cited by 24Augmented.ExtraDegeneracyExtraDegeneracy.sCITED BYCITES

Cites11

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

Cited by17

Results whose statement or proof uses this declaration.