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 CategoryTheory.Category.Cat.Colimit 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.

Equations

• One or more equations did not get rendered due to their size.

@[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 (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.

Equations

• CategoryTheory.nerve₂Adj.counit = { app := fun (x : CategoryTheory.Cat) => CategoryTheory.nerve₂Adj.counit.app ↑x, naturality := CategoryTheory.nerve₂Adj.counit.proof_1 }

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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₂ φ).

Equations

• CategoryTheory.toNerve₂.mk F hyp = { app := fun (n : (SimplexCategory.Truncated 2)ᵒᵖ) => CategoryTheory.toNerve₂.mk.app F (Opposite.unop n), naturality := ⋯ }

@[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.

Equations

• CategoryTheory.toNerve₂.mk' F hyp = CategoryTheory.toNerve₂.mk (CategoryTheory.CategoryStruct.comp F (SSet.OneTruncation₂.ofNerve₂.natIso.app (CategoryTheory.Cat.of C)).hom) hyp

@[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 beteween 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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CategoryTheory.nerve₂Adj.unit = { app := CategoryTheory.nerve₂Adj.unit.app, naturality := CategoryTheory.nerve₂Adj.unit.proof_1 }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CategoryTheory.nerveFunctor₂.fullyfaithful = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful CategoryTheory.Nerve.nerveFunctor₂

instance CategoryTheory.nerve₂Adj.reflective : Reflective Nerve.nerveFunctor₂

Equations

• CategoryTheory.nerve₂Adj.reflective = CategoryTheory.Reflective.mk SSet.Truncated.hoFunctor₂ CategoryTheory.nerve₂Adj

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.

Equations

• CategoryTheory.nerveAdjunction = ((SSet.coskAdj 2).comp CategoryTheory.nerve₂Adj).ofNatIsoRight CategoryTheory.Nerve.cosk₂Iso.symm

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.

Equations

• CategoryTheory.nerveFunctor.fullyfaithful = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful CategoryTheory.nerveFunctor

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.

Equations

• CategoryTheory.nerveFunctorCompHoFunctorIso = CategoryTheory.asIso CategoryTheory.nerveAdjunction.counit

noncomputable instance CategoryTheory.instReflectiveSSetCatNerveFunctor : Reflective nerveFunctor

Equations

• CategoryTheory.instReflectiveSSetCatNerveFunctor = CategoryTheory.Reflective.mk SSet.hoFunctor CategoryTheory.nerveAdjunction