feat(AlgebraicTopology/NerveAdjunction): nerve adjunction, Cat has colimits

[digama0]

The construction of the adjunction between nerve and SSet.hoFunctor. As a consequence, we can conclude that Cat.{u,u} has colimits.

Co-Authored-By: Emily Riehl [email protected] and Pietro Monticone [email protected]

---

• depends on: [Merged by Bors] - feat(CategoryTheory/EqToHom): simp lemmas for heq + eqToHom #16779
• depends on: [Merged by Bors] - feat(Combinatorics/Quiver/ReflQuiver): reflexive quivers #16780
• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): SimplicialSet (co)skeleton properties #16781
• depends on: feat(AlgebraicTopology/Nerve): nerve is 2-coskeletal #16782
• depends on: feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor #16783

[github-actions]

PR summary 0a0d5f1ef5

Import changes exceeding 2%

%	File
+89.98%	Mathlib.CategoryTheory.Category.Cat.Limit

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Category.Cat.Limit	429	815	+386 (+89.98%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Category.Cat.Limit	386
Mathlib.AlgebraicTopology.HomotopyCat	809
Mathlib.AlgebraicTopology.NerveAdjunction	810

---

Declarations diff

+ CompClosure.congruence
+ SSet.HoRel
+ SSet.HoRel.ext_triangle
+ SSet.HoRel₂
+ SSet.HoRel₂.ext_triangle
+ SSet.OneTruncation
+ SSet.OneTruncation.Hom
+ SSet.OneTruncation.ofNerve
+ SSet.OneTruncation.ofNerve.hom
+ SSet.OneTruncation.ofNerve.inv
+ SSet.OneTruncation.ofNerve.map
+ SSet.OneTruncation.ofNerve.natIso
+ SSet.OneTruncation.src
+ SSet.OneTruncation.tgt
+ SSet.OneTruncation₂
+ SSet.OneTruncation₂.Hom
+ SSet.OneTruncation₂.ofTwoTruncationIso
+ SSet.OneTruncation₂.src
+ SSet.OneTruncation₂.tgt
+ SSet.hoCat
+ SSet.hoFunctor
+ SSet.hoFunctor'
+ SSet.hoFunctorMap
+ SSet.hoFunctor₂
+ SSet.hoFunctor₂Map
+ SSet.hoFunctor₂Obj
+ SSet.hoFunctor₂Obj.lift_unique'
+ SSet.hoFunctor₂Obj.quotientFunctor
+ SSet.hoFunctor₂_naturality
+ SSet.oneTruncation
+ SSet.oneTruncation₂
+ SSet.δ₂
+ SSet.σ₂
+ ar
+ ar'
+ ar'succ
+ cosk2Iso
+ cosk2NatIso.component
+ cosk2NatTrans
+ cosk2RightExtension.component.hom.iso
+ cosk2RightExtension.hom
+ cosk2RightExtension.hom_isIso
+ fact.map.arr
+ fact.obj.arr
+ forgetToReflQuiv.natIso
+ hoFunctor.ofTwoTruncation.iso
+ hoFunctor.ofTwoTruncation.natIso
+ instance (C : Cat) : Mono (nerve₂.seagull C)
+ instance (S : SSet) : ReflQuiver (SSet.OneTruncation S)
+ instance (S : SSet.Truncated 2) : ReflQuiver (SSet.OneTruncation₂ S)
+ instance (V : SSet.Truncated.{u} 2) : Category.{u} (SSet.hoFunctor₂Obj V)
+ instance (V : SSet.{u}) : Category.{u} (SSet.hoCat V)
+ instance : HasColimits Cat.{v, v}
+ instance : Reflective nerveFunctor
+ isPointwiseRightKanExtension
+ isPointwiseRightKanExtension.isUniversal
+ isPointwiseRightKanExtensionAt
+ isRightKanExtension
+ nerveAdjunction
+ nerveCounitNatIso
+ nerveCounit_isIso
+ nerveFunctor.faithful
+ nerveFunctor.full
+ nerveFunctor.fullyfaithful
+ nerveFunctor₂
+ nerveFunctor₂.faithful
+ nerveFunctor₂.full
+ nerveFunctor₂.fullyfaithful
+ nerveRightExtension
+ nerveRightExtension.coneAt
+ nerve₂
+ nerve₂.seagull
+ nerve₂Adj
+ nerve₂Adj.counit
+ nerve₂Adj.counit.component
+ nerve₂Adj.counit.component_eq
+ nerve₂Adj.counit.naturality'
+ nerve₂Adj.reflective
+ nerve₂Adj.unit
+ nerve₂Adj.unit.component
+ nerve₂Adj.unit.component_eq
+ nerve₂RestrictedIso
+ nerve₂_restrictedNerve
+ oneTruncation₂_toNerve₂Mk'
+ opstuff.{w}
+ pt
+ pt'
+ ran.lift
+ ran.lift'
+ ran.lift.eq
+ ran.lift.eq₂
+ ran.lift.map
+ strArr.homEv
+ strArr.homEv.map
+ strArr.homEvSucc
+ toNerve₂.ext
+ toNerve₂.ext'
+ toNerve₂.mk
+ toNerve₂.mk'
+ toNerve₂.mk.app
+ toNerve₂.mk.app_one
+ toNerve₂.mk.app_two
+ toNerve₂.mk.app_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/EqToHom): simp lemmas for heq + eqToHom #16779
• [Merged by Bors] - feat(Combinatorics/Quiver/ReflQuiver): reflexive quivers #16780
• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): SimplicialSet (co)skeleton properties #16781
• feat(AlgebraicTopology/Nerve): nerve is 2-coskeletal #16782
• feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor #16783
  By Dependent Issues (🤖). Happy coding!