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.

def CategoryTheory.nerve₂Adj.counit.app (C : Type u) [SmallCategory C] : Functor (Nerve.nerveFunctor₂.obj (Cat.of C)).HomotopyCategory C

The components of the counit of nerve₂Adj.

@[simp]

theorem CategoryTheory.nerve₂Adj.counit.app_map (C : Type u) [SmallCategory C] (a b : Quotient SSet.Truncated.HoRel₂) (hf : a ⟶ b) : (app C).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => (ReflQuiv.adj.counit.app (Cat.of C)).map (Quot.liftOn f (fun (f : a.as.as ⟶ b.as.as) => (Cat.FreeRefl.quotientFunctor C).map ((SSet.OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C)).mapPath f)) ⋯)) ⋯

@[simp]

theorem CategoryTheory.nerve₂Adj.counit.app_obj (C : Type u) [SmallCategory C] (a : Quotient SSet.Truncated.HoRel₂) : (app C).obj a = (ReflQuiv.adj.counit.app (Cat.of C)).obj ((Cat.freeRefl.map (SSet.OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C))).obj a.as)

@[simp]

theorem CategoryTheory.nerve₂Adj.counit.app_eq (C : Type u) [SmallCategory C] : (SSet.Truncated.HomotopyCategory.quotientFunctor (Nerve.nerveFunctor₂.obj (Cat.of C))).comp (app C) = (CategoryStruct.comp (Functor.whiskerRight SSet.OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl) ReflQuiv.adj.counit).app (Cat.of C)

theorem CategoryTheory.nerve₂Adj.counit.naturality {C D : Type u} [SmallCategory C] [SmallCategory D] (F : Functor C D) : Functor.comp ((Nerve.nerveFunctor₂.comp SSet.Truncated.hoFunctor₂).map F) (app D) = (app C).comp F

The naturality of nerve₂Adj.counit.app.

def CategoryTheory.nerve₂Adj.counit : Nerve.nerveFunctor₂.comp SSet.Truncated.hoFunctor₂ ⟶ Functor.id Cat

The counit of nerve₂Adj.

@[simp]

theorem CategoryTheory.nerve₂Adj.counit_app (x✝ : Cat) : counit.app x✝ = counit.app ↑x✝

def CategoryTheory.toNerve₂.mk.app {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (n : SimplexCategory.Truncated 2) : X.obj (Opposite.op n) ⟶ (Nerve.nerveFunctor₂.obj (Cat.of C)).obj (Opposite.op n)

Because nerves are 2-coskeletal, the components of a map of 2-truncated simplicial sets valued in a nerve can be recovered from the underlying ReflPrefunctor.

@[simp]

theorem CategoryTheory.toNerve₂.mk.app_zero {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) : app F { obj := SimplexCategory.mk 0, property := ⋯ } x = ComposableArrows.mk₀ (F.obj x)

@[simp]

theorem CategoryTheory.toNerve₂.mk.app_one {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (f : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })) : app F { obj := SimplexCategory.mk 1, property := ⋯ } f = ComposableArrows.mk₁ (F.map { edge := f, src_eq := ⋯, tgt_eq := ⋯ })

@[simp]

theorem CategoryTheory.toNerve₂.mk.app_two {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) : app F { obj := SimplexCategory.mk 2, property := ⋯ } φ = ComposableArrows.mk₂ (F.map (SSet.Truncated.ev01₂ φ)) (F.map (SSet.Truncated.ev12₂ φ))

noncomputable def CategoryTheory.nerve₂.seagull (C : Type u) [Category.{u_1, u} C] : (Nerve.nerveFunctor₂.obj (Cat.of C)).obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ }) ⟶ (Nerve.nerveFunctor₂.obj (Cat.of C)).obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ }) ⨯ (Nerve.nerveFunctor₂.obj (Cat.of C)).obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })

This is similar to one of the famous Segal maps, except valued in a product rather than a pullback.

instance CategoryTheory.instMonoObjOppositeTruncatedOfNatNatCatTruncatedNerveFunctor₂OfOpMkSimplexCategoryLeLenMkProdSeagull (C : Type u) [Category.{u_1, u} C] : Mono (nerve₂.seagull C)

@[reducible, inline]

abbrev CategoryTheory.toNerve₂.mk.naturalityProperty {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) : MorphismProperty (SimplexCategory.Truncated 2)

Naturality of the components defined by toNerve₂.mk.app as a morphism property of maps in SimplexCategory.Truncated 2.

theorem CategoryTheory.ReflPrefunctor.congr_mk₁_map {Y : Type u'} [ReflQuiver Y] {C : Type u} [Category.{v, u} C] (F : Y ⥤rq ↑(ReflQuiv.of C)) {x₁ y₁ x₂ y₂ : Y} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂) (hx : x₁ = x₂) (hy : y₁ = y₂) (hfg : Quiver.homOfEq f hx hy = g) : ComposableArrows.mk₁ (F.map f) = ComposableArrows.mk₁ (F.map g)

theorem CategoryTheory.toNerve₂.mk_naturality_σ00 {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) : mk.naturalityProperty F (SSet.σ₂ 0 ⋯ ⋯)

theorem CategoryTheory.toNerve₂.mk_naturality_δ0i {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (i : Fin 2) : mk.naturalityProperty F (SSet.δ₂ i ⋯ ⋯)

theorem CategoryTheory.toNerve₂.mk_naturality_δ1i {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp (F.map (SSet.Truncated.ev01₂ φ)) (F.map (SSet.Truncated.ev12₂ φ))) (i : Fin 3) : mk.naturalityProperty F (SSet.δ₂ i ⋯ ⋯)

theorem CategoryTheory.toNerve₂.mk_naturality_σ1i {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp (F.map (SSet.Truncated.ev01₂ φ)) (F.map (SSet.Truncated.ev12₂ φ))) (i : Fin 2) : mk.naturalityProperty F (SSet.σ₂ i ⋯ ⋯)

theorem CategoryTheory.toNerve₂.mk_naturality {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp (F.map (SSet.Truncated.ev01₂ φ)) (F.map (SSet.Truncated.ev12₂ φ))) : mk.naturalityProperty F = ⊤

A proof that the components defined by toNerve₂.mk.app are natural.

def CategoryTheory.toNerve₂.mk {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp (F.map (SSet.Truncated.ev01₂ φ)) (F.map (SSet.Truncated.ev12₂ φ))) : X ⟶ Nerve.nerveFunctor₂.obj (Cat.of C)

The morphism X ⟶ nerveFunctor₂.obj (Cat.of C) of 2-truncated simplicial sets that is constructed from a refl prefunctor F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C assuming ∀ (φ : : X _⦋2⦌₂), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ).

@[simp]

theorem CategoryTheory.toNerve₂.mk_app {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp (F.map (SSet.Truncated.ev01₂ φ)) (F.map (SSet.Truncated.ev12₂ φ))) (n : (SimplexCategory.Truncated 2)ᵒᵖ) (a✝ : X.obj (Opposite.op (Opposite.unop n))) : (mk F hyp).app n a✝ = mk.app F (Opposite.unop n) a✝

def CategoryTheory.toNerve₂.mk' {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ SSet.oneTruncation₂.obj (Nerve.nerveFunctor₂.obj (Cat.of C))) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp ((CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev01₂ φ)) ((CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev12₂ φ))) : X ⟶ Nerve.nerveFunctor₂.obj (Cat.of C)

An alternate version of toNerve₂.mk, which constructs a map of 2-truncated simplicial sets X ⟶ nerveFunctor₂.obj (Cat.of C) from the underlying refl prefunctor under a composition hypothesis, where that prefunctor the central hypothesis is conjugated by the isomorphism nerve₂Adj.NatIso.app C.

@[simp]

theorem CategoryTheory.toNerve₂.mk'_app {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ SSet.oneTruncation₂.obj (Nerve.nerveFunctor₂.obj (Cat.of C))) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp ((CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev01₂ φ)) ((CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev12₂ φ))) (n : (SimplexCategory.Truncated 2)ᵒᵖ) (a✝ : X.obj (Opposite.op (Opposite.unop n))) : (mk' F hyp).app n a✝ = mk.app (CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C))) (Opposite.unop n) a✝

theorem CategoryTheory.oneTruncation₂_toNerve₂Mk' {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F : SSet.oneTruncation₂.obj X ⟶ SSet.oneTruncation₂.obj (Nerve.nerveFunctor₂.obj (Cat.of C))) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev02₂ φ) = CategoryStruct.comp ((CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev01₂ φ)) ((CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (SSet.Truncated.ev12₂ φ))) : SSet.oneTruncation₂.map (toNerve₂.mk' F hyp) = F

A computation about toNerve₂.mk'.

theorem CategoryTheory.toNerve₂.ext {C : Type u} [SmallCategory C] {X : SSet.Truncated 2} (F G : X ⟶ Nerve.nerveFunctor₂.obj (Cat.of C)) (hyp : SSet.oneTruncation₂.map F = SSet.oneTruncation₂.map G) : F = G

An equality between maps into the 2-truncated nerve is detected by an equality between their underlying refl prefunctors.

def CategoryTheory.nerve₂Adj.unit.app (X : SSet.Truncated 2) : X ⟶ Nerve.nerveFunctor₂.obj (SSet.Truncated.hoFunctor₂.obj X)

The components of the 2-truncated nerve adjunction unit.

theorem CategoryTheory.nerve₂Adj.unit.map_app_eq (X : SSet.Truncated 2) : SSet.oneTruncation₂.map (app X) = ReflQuiv.adj.unit.app (SSet.oneTruncation₂.obj X) ⋙rq (SSet.Truncated.HomotopyCategory.quotientFunctor X).toReflPrefunctor ⋙rq SSet.OneTruncation₂.ofNerve₂.natIso.inv.app (SSet.Truncated.hoFunctor₂.obj X)

theorem CategoryTheory.nerve₂Adj.unit.naturality {X Y : SSet.Truncated 2} (f : X ⟶ Y) : CategoryStruct.comp f (app Y) = CategoryStruct.comp (app X) (Nerve.nerveFunctor₂.map (SSet.Truncated.hoFunctor₂.map f))

theorem CategoryTheory.nerve₂Adj.unit.naturality_assoc {X Y : SSet.Truncated 2} (f : X ⟶ Y) {Z : SSet.Truncated 2} (h : Nerve.nerveFunctor₂.obj (SSet.Truncated.hoFunctor₂.obj Y) ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (app Y) h) = CategoryStruct.comp (app X) (CategoryStruct.comp (Nerve.nerveFunctor₂.map (SSet.Truncated.hoFunctor₂.map f)) h)

def CategoryTheory.nerve₂Adj.unit : Functor.id (SSet.Truncated 2) ⟶ SSet.Truncated.hoFunctor₂.comp Nerve.nerveFunctor₂

The 2-truncated nerve adjunction unit.

@[simp]

theorem CategoryTheory.nerve₂Adj.unit_app (X : SSet.Truncated 2) : unit.app X = unit.app X

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

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

instance CategoryTheory.nerveFunctor₂.faithful : Nerve.nerveFunctor₂.Faithful

instance CategoryTheory.nerveFunctor₂.full : Nerve.nerveFunctor₂.Full

noncomputable def CategoryTheory.nerveFunctor₂.fullyfaithful : Nerve.nerveFunctor₂.FullyFaithful

The 2-truncated nerve functor is both full and faithful and thus is fully faithful.

instance CategoryTheory.nerve₂Adj.reflective : 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