Theorems · Definition · category theory

CategoryTheory.SimplicialObject.diagonal

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n : ℕ} → X.obj (Opposite.op { len := n }) ⟶ X.obj (Opposite.op { len := 1 })

The diagonal of a simplex is the long edge of the simplex.

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Basic

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category