Theorems · Definition · category theory

SSet.Truncated.HomotopyCategory.homToNerveMk

{X : SSet.Truncated 2} →
  {C : Type u} →
    [inst : CategoryTheory.SmallCategory C] →
      CategoryTheory.Functor X.HomotopyCategory C → (X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C))

Given a 2-truncated simplicial set X and a category C, this is the morphism X ⟶ (truncation 2).obj (nerve C) corresponding to a functor X.HomotopyCategory ⥤ C.

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Cited by: 5 results in Mathlib
Foundations: Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.SmallCategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites27

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

DFunLike.coeproof · cited by 62,936
Quiver.Homstatement · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Functor.mapproof · cited by 8,698
Oppositestatement · cited by 8,081
CategoryTheory.ConcreteCategory.homproof · cited by 4,022
Equiv.symmproof · cited by 3,681
SimplexCategorystatement · cited by 2,204
Quiver.Hom.opproof · cited by 1,948
SSetstatement · cited by 1,283
SimplexCategory.lenstatement · cited by 542

Cited by6

Results whose statement or proof uses this declaration.

SSet.Truncated.HomotopyCategory.homToNerveMk_app_edgestatement · cited by 1
SSet.Truncated.HomotopyCategory.homToNerveMk_app_onestatement · cited by 1
SSet.Truncated.HomotopyCategory.homToNerveMk_compstatement · cited by 1
SSet.Truncated.HomotopyCategory.homToNerveMk_app_zerostatement · cited by 0
SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assocstatement and proof · cited by 0
SSet.Truncated.HomotopyCategory.functorEquivproof · cited by 0