Theorems · Theorem · category theory

SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge

∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (F : CategoryTheory.Functor X.HomotopyCategory C)
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })} (e : SSet.Truncated.Edge x y),
  (CategoryTheory.ConcreteCategory.hom
        ((SSet.Truncated.HomotopyCategory.homToNerveMk F).app
          (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })))
      e.edge =
    CategoryTheory.ComposableArrows.mk₁ (F.map (SSet.Truncated.HomotopyCategory.homMk e))

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.SmallCategory