The adjunction between the nerve and the homotopy category functor

We define an adjunction nerveAdjunction : hoFunctor ⊣ nerveFunctor between the functor that takes a simplicial set to its homotopy category and the functor that takes a category to its nerve.

Up to natural isomorphism, this is constructed as the composite of two other adjunctions, namely nerve₂Adj : hoFunctor₂ ⊣ nerveFunctor₂ between analogously-defined functors involving the category of 2-truncated simplicial sets and coskAdj 2 : truncation 2 ⊣ Truncated.cosk 2. The aforementioned natural isomorphism

cosk₂Iso : nerveFunctor ≅ nerveFunctor₂ ⋙ Truncated.cosk 2

exists because nerves of categories are 2-coskeletal.

We also prove that nerveFunctor is fully faithful, demonstrating that nerveAdjunction is reflective. Since the category of simplicial sets is cocomplete, we conclude in Mathlib/CategoryTheory/Category/Cat/Colimit.lean that the category of categories has colimits.

Finally we show that hoFunctor : SSet.{u} ⥤ Cat.{u, u} preserves finite cartesian products; note that it fails to preserve infinite products.

The goal of this section is to define SSet.Truncated.liftOfStrictSegal which allows to construct of morphism X ⟶ Y of 2-truncated simplicial sets from the data of maps on 0- and 1-simplices when Y is strict Segal.

def SSet.Truncated.liftOfStrictSegal.f₂ {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) : Y.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝¹ })

Auxiliary definition for SSet.Truncated.liftOfStrictSegal.

@[simp]

theorem SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) : ((hY.spineEquiv 2 f₂._proof_5) (f₂ f₀ f₁ hδ₁ hδ₀ hY x)).arrow 0 = f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x)

@[simp]

theorem SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) : ((hY.spineEquiv 2 f₂._proof_5) (f₂ f₀ f₁ hδ₁ hδ₀ hY x)).arrow 1 = f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁴ _proof_15✝).op x)

theorem SSet.Truncated.liftOfStrictSegal.hδ'₀ {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) : f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁵ _proof_15✝¹).op (f₂ f₀ f₁ hδ₁ hδ₀ hY x)

theorem SSet.Truncated.liftOfStrictSegal.hδ'₂ {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) : f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁵ _proof_15✝¹).op (f₂ f₀ f₁ hδ₁ hδ₀ hY x)

theorem SSet.Truncated.liftOfStrictSegal.hδ'₁ {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (H : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝¹ })), f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁵ _proof_15✝¹).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁶ _proof_15✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁷ _proof_15✝³).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁸ _proof_15✝⁴).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁹ _proof_15✝⁵).op y) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝² })) : f₁ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝¹⁰ _proof_15✝⁶).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝¹¹ _proof_15✝⁷).op (f₂ f₀ f₁ hδ₁ hδ₀ hY x)

theorem SSet.Truncated.liftOfStrictSegal.hσ'₀ {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hσ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁶ })), f₁ (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁴ _proof_11✝⁷).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁵ _proof_11✝⁸).op (f₀ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝⁴ })) : f₂ f₀ f₁ hδ₁ hδ₀ hY (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_15✝ _proof_12✝⁵).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_15✝¹ _proof_12✝⁶).op (f₁ x)

theorem SSet.Truncated.liftOfStrictSegal.hσ'₁ {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hσ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁶ })), f₁ (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁴ _proof_11✝⁷).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁵ _proof_11✝⁸).op (f₀ x)) (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝⁴ })) : f₂ f₀ f₁ hδ₁ hδ₀ hY (X.map (SimplexCategory.Truncated.σ₂ 1 _proof_15✝ _proof_12✝⁵).op x) = Y.map (SimplexCategory.Truncated.σ₂ 1 _proof_15✝¹ _proof_12✝⁶).op (f₁ x)

def SSet.Truncated.liftOfStrictSegal.app {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) (n : (SimplexCategory.Truncated 2)ᵒᵖ) : X.obj n ⟶ Y.obj n

Auxiliary definition for SSet.Truncated.liftOfStrictSegal.

@[reducible, inline]

abbrev SSet.Truncated.liftOfStrictSegal.naturalityProperty {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (hY : Y.StrictSegal) : CategoryTheory.MorphismProperty (SimplexCategory.Truncated 2)

The property of morphims in SimplexCategory.Truncated 2 for which liftOfStrictSegal.app is natural.

theorem SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (H : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝¹ })), f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁵ _proof_15✝¹).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁶ _proof_15✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁷ _proof_15✝³).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁸ _proof_15✝⁴).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁹ _proof_15✝⁵).op y) (hσ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁶ })), f₁ (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁴ _proof_11✝⁷).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁵ _proof_11✝⁸).op (f₀ x)) (hY : Y.StrictSegal) : naturalityProperty f₀ f₁ hδ₁ hδ₀ hY = ⊤

def SSet.Truncated.liftOfStrictSegal {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (H : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝¹ })), f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁵ _proof_15✝¹).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁶ _proof_15✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁷ _proof_15✝³).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁸ _proof_15✝⁴).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁹ _proof_15✝⁵).op y) (hσ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁶ })), f₁ (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁴ _proof_11✝⁷).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁵ _proof_11✝⁸).op (f₀ x)) (hY : Y.StrictSegal) : X ⟶ Y

Constructor for morphisms X ⟶ Y between 2-truncated simplicial sets from the data of maps on 0- and 1-simplices when Y is strict Segal.

@[simp]

theorem SSet.Truncated.liftOfStrictSegal_app_0 {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (H : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝¹ })), f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁵ _proof_15✝¹).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁶ _proof_15✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁷ _proof_15✝³).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁸ _proof_15✝⁴).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁹ _proof_15✝⁵).op y) (hσ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁶ })), f₁ (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁴ _proof_11✝⁷).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁵ _proof_11✝⁸).op (f₀ x)) (hY : Y.StrictSegal) : (liftOfStrictSegal f₀ f₁ hδ₁ hδ₀ H hσ hY).app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁹ }) = f₀

@[simp]

theorem SSet.Truncated.liftOfStrictSegal_app_1 {X Y : Truncated 2} (f₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) (f₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) → Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) (hδ₁ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) (hδ₀ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })), f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) (H : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝¹ })), f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x) = Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁵ _proof_15✝¹).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁶ _proof_15✝²).op x) = Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁷ _proof_15✝³).op y → f₁ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁸ _proof_15✝⁴).op x) = Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝⁹ _proof_15✝⁵).op y) (hσ : ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝⁶ })), f₁ (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁴ _proof_11✝⁷).op x) = Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝⁵ _proof_11✝⁸).op (f₀ x)) (hY : Y.StrictSegal) : (liftOfStrictSegal f₀ f₁ hδ₁ hδ₀ H hσ hY).app (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹⁰ }) = f₁

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

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

@[simp]

theorem SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] (φ : X ⟶ (truncation 2).obj (CategoryTheory.nerve C)) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ })) : (descOfTruncation φ).obj (mk x) = CategoryTheory.nerveEquiv (φ.app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ }) x)

@[simp]

theorem SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] (φ : X ⟶ (truncation 2).obj (CategoryTheory.nerve C)) {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ })} (e : Edge x₀ x₁) : (descOfTruncation φ).map (homMk e) = CategoryTheory.nerve.homEquiv (e.map φ)

theorem SSet.Truncated.HomotopyCategory.descOfTruncation_comp {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] {X' : Truncated 2} (ψ : X ⟶ X') (φ : X' ⟶ (truncation 2).obj (CategoryTheory.nerve C)) : descOfTruncation (CategoryTheory.CategoryStruct.comp ψ φ) = (mapHomotopyCategory ψ).comp (descOfTruncation φ)

def SSet.Truncated.HomotopyCategory.homToNerveMk {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] (F : CategoryTheory.Functor X.HomotopyCategory C) : X ⟶ (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.

@[simp]

theorem SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] (F : CategoryTheory.Functor X.HomotopyCategory C) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ })) : (homToNerveMk F).app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ }) x = CategoryTheory.nerveEquiv.symm (F.obj (mk x))

theorem SSet.Truncated.HomotopyCategory.homToNerveMk_app_one {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] (F : CategoryTheory.Functor X.HomotopyCategory C) (f : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ })) : (homToNerveMk F).app (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ }) f = CategoryTheory.ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f)))

@[simp]

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

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

Given a 2-truncated simplicial set X and a category C, this is the bijection between morphism X.HomotopyCategory ⥤ C and X ⟶ (truncation 2).obj (nerve C) which is part of the adjunction SSet.Truncated.nerve₂Adj.

theorem SSet.Truncated.HomotopyCategory.homToNerveMk_comp {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] {D : Type u} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor X.HomotopyCategory C) (G : CategoryTheory.Functor C D) : homToNerveMk (F.comp G) = CategoryTheory.CategoryStruct.comp (homToNerveMk F) ((truncation 2).map (CategoryTheory.nerveMap G))

theorem SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc {X : Truncated 2} {C : Type u} [CategoryTheory.SmallCategory C] {D : Type u} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor X.HomotopyCategory C) (G : CategoryTheory.Functor C D) {Z : Truncated 2} (h : (truncation 2).obj (CategoryTheory.nerve D) ⟶ Z) : CategoryTheory.CategoryStruct.comp (homToNerveMk (F.comp G)) h = CategoryTheory.CategoryStruct.comp (homToNerveMk F) (CategoryTheory.CategoryStruct.comp ((truncation 2).map (CategoryTheory.nerveMap G)) h)

def SSet.Truncated.nerve₂Adj : hoFunctor₂ ⊣ CategoryTheory.Nerve.nerveFunctor₂

The adjunction between the 2-truncated homotopy category functor and the 2-truncated nerve functor.

def CategoryTheory.nerve.functorOfNerveMap {C D : Type u} [SmallCategory C] [SmallCategory D] (φ : Nerve.nerveFunctor₂.obj (Cat.of C) ⟶ Nerve.nerveFunctor₂.obj (Cat.of D)) : Functor C D

The functor C ⥤ D that is reconstructed for a morphism between the 2-truncated nerves.

@[simp]

theorem CategoryTheory.nerve.functorOfNerveMap_map {C D : Type u} [SmallCategory C] [SmallCategory D] (φ : Nerve.nerveFunctor₂.obj (Cat.of C) ⟶ Nerve.nerveFunctor₂.obj (Cat.of D)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (functorOfNerveMap φ).map f = homEquiv ((edgeMk f).toTruncated.map φ)

@[simp]

theorem CategoryTheory.nerve.functorOfNerveMap_obj {C D : Type u} [SmallCategory C] [SmallCategory D] (φ : Nerve.nerveFunctor₂.obj (Cat.of C) ⟶ Nerve.nerveFunctor₂.obj (Cat.of D)) (x : C) : (functorOfNerveMap φ).obj x = nerveEquiv (φ.app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) (nerveEquiv.symm x))

theorem CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap {C D : Type u} [SmallCategory C] [SmallCategory D] (φ : Nerve.nerveFunctor₂.obj (Cat.of C) ⟶ Nerve.nerveFunctor₂.obj (Cat.of D)) : Nerve.nerveFunctor₂.map (functorOfNerveMap φ).toCatHom = φ

theorem CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map {C D : Type u} [SmallCategory C] [SmallCategory D] (F : Functor C D) : functorOfNerveMap ((SSet.truncation 2).map (nerveMap F)) = F

def CategoryTheory.nerve.fullyFaithfulNerveFunctor₂ : Nerve.nerveFunctor₂.FullyFaithful

The 2-truncated nerve functor is fully faithful.

instance CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂ : Nerve.nerveFunctor₂.Faithful

instance CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂ : Nerve.nerveFunctor₂.Full

instance CategoryTheory.nerve.instReflectiveTruncatedOfNatNatCatNerveFunctor₂ : Reflective Nerve.nerveFunctor₂

noncomputable def CategoryTheory.nerveAdjunction : SSet.hoFunctor ⊣ nerveFunctor

The adjunction between the nerve functor and the homotopy category functor is, up to isomorphism, the composite of the adjunctions SSet.coskAdj 2 and nerve₂Adj.

instance CategoryTheory.nerveFunctor.faithful : nerveFunctor.Faithful

Repleteness exists for full and faithful functors but not fully faithful functors, which is why we do this inefficiently.

instance CategoryTheory.nerveFunctor.full : nerveFunctor.Full

noncomputable def CategoryTheory.nerveFunctor.fullyfaithful : nerveFunctor.FullyFaithful

The nerve functor is both full and faithful and thus is fully faithful.

instance CategoryTheory.nerveAdjunction.isIso_counit : IsIso nerveAdjunction.counit

noncomputable def CategoryTheory.nerveFunctorCompHoFunctorIso : nerveFunctor.comp SSet.hoFunctor ≅ Functor.id Cat

The counit map of nerveAdjunction is an isomorphism since the nerve functor is fully faithful.

noncomputable instance CategoryTheory.instReflectiveSSetCatNerveFunctor : Reflective nerveFunctor

instance CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf (C D : Type u) [Category.{u, u} C] [Category.{u, u} D] : IsIso (Limits.prodComparison (nerveFunctor.comp (SSet.hoFunctor.comp nerveFunctor)) (Cat.of C) (Cat.of D))

instance CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor : SSet.hoFunctor.IsLeftAdjoint

instance CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve (C D : Type u) [Category.{u, u} C] [Category.{u, u} D] : IsIso (Limits.prodComparison SSet.hoFunctor (nerve C) (nerve D))

instance CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex (n m : ℕ) : IsIso (Limits.prodComparison SSet.hoFunctor (SSet.stdSimplex.obj (SimplexCategory.mk n)) (SSet.stdSimplex.obj (SimplexCategory.mk m)))

theorem CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex {D : SSet} (X : SSet) (H : ∀ (m : ℕ), IsIso (Limits.prodComparison SSet.hoFunctor D (SSet.stdSimplex.obj (SimplexCategory.mk m)))) : IsIso (Limits.prodComparison SSet.hoFunctor D X)

instance CategoryTheory.hoFunctor.isIso_prodComparison (X Y : SSet) : IsIso (Limits.prodComparison SSet.hoFunctor X Y)

instance CategoryTheory.hoFunctor.preservesBinaryProduct (X Y : SSet) : Limits.PreservesLimit (Limits.pair X Y) SSet.hoFunctor

The functor hoFunctor : SSet ⥤ Cat preserves binary products of simplicial sets X and Y.

instance CategoryTheory.hoFunctor.preservesBinaryProducts : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) SSet.hoFunctor

The functor hoFunctor : SSet ⥤ Cat preserves limits of functors out of Discrete WalkingPair.

instance CategoryTheory.hoFunctor.preservesFiniteProducts : Limits.PreservesFiniteProducts SSet.hoFunctor

The functor hoFunctor : SSet ⥤ Cat preserves finite products of simplicial sets.