feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor

[digama0]

This defines SSet.hoFunctor, which constructs a category from a simplicial set.

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

• Prerequisite for feat(AlgebraicTopology/NerveAdjunction): nerve adjunction, Cat has colimits #16784.

[github-actions]

PR summary 2de082ee18

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet	785	791	+6 (+0.76%)
Mathlib.AlgebraicTopology.Nerve	790	796	+6 (+0.76%)

Import changes for all files

Files	Import difference
6 files Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.AlgebraicTopology.SingularSet Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.AlgebraicTopology.ExtraDegeneracy	3
Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialCategory.Basic	5
4 files Mathlib.AlgebraicTopology.SimplicialSet Mathlib.AlgebraicTopology.Quasicategory Mathlib.AlgebraicTopology.Nerve Mathlib.AlgebraicTopology.KanComplex	6
Mathlib.Combinatorics.Quiver.ReflQuiver	359
Mathlib.CategoryTheory.Category.ReflQuiv	360
Mathlib.AlgebraicTopology.HomotopyCat	802

---

Declarations diff

+ CompClosure.congruence
+ Fin.hom_succ
+ Fin.le_succ
+ FreeRefl
+ FreeRefl.lift_unique'
+ FreeRefl.quotientFunctor
+ FreeReflRel
+ Functor.toReflPrefunctor
+ Functor.toReflPrefunctor_toPrefunctor
+ Hom.ext
+ ReflPrefunctor
+ ReflQuiv
+ ReflQuiver
+ ReflQuiver.id_eq_id
+ 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₂.nerve₂.natIso
+ SSet.OneTruncation₂.nerve₂Iso
+ 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.σ₂
+ Truncated.uliftFunctor
+ adj
+ adj.counit.app
+ adj.counit.component_eq
+ adj.counit.component_eq'
+ adj.unit.app
+ adj.unit.component_eq
+ ar
+ ar'
+ ar'succ
+ catToReflQuiver
+ category
+ comp
+ comp_assoc
+ comp_id
+ congr_map
+ const_fac_thru_zero
+ cosk2Iso
+ cosk2NatIso.component
+ cosk2NatTrans
+ cosk2RightExtension.component.hom.iso
+ cosk2RightExtension.hom
+ cosk2RightExtension.hom_isIso
+ coskAdj
+ coskAdj.reflective
+ coskeleton.faithful
+ coskeleton.full
+ coskeleton.fullyFaithful
+ coskeleton_reflective
+ discreteReflQuiver
+ eq_const_of_zero
+ eq_const_to_zero
+ eq_of_one_to_one
+ eq_of_one_to_two
+ exists_eq_const_of_zero
+ ext
+ fact.map.arr
+ fact.obj.arr
+ forget
+ forget.Faithful
+ forgetToQuiv
+ forgetToQuiv.Faithful
+ forgetToQuiv_faithful
+ forget_faithful
+ forget_forgetToQuiv
+ freeRefl
+ freeReflNatTrans
+ freeRefl_naturality
+ hoFunctor.ofTwoTruncation.iso
+ hoFunctor.ofTwoTruncation.natIso
+ id
+ id_comp
+ inclusion.fullyFaithful
+ 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 (V : Type*) [ReflQuiver V] : Inhabited (ReflPrefunctor V V)
+ instance (V) [ReflQuiver V] : Category (FreeRefl V)
+ instance : CoeSort ReflQuiv (Type u) where coe := Bundled.α
+ instance : Inhabited ReflQuiv := ⟨ReflQuiv.of (Discrete default)⟩
+ isPointwiseRightKanExtension
+ isPointwiseRightKanExtension.isUniversal
+ isPointwiseRightKanExtensionAt
+ isRightKanExtension
+ mkOfLe
+ mkOfLeComp
+ mkOfSucc
+ mk_map
+ mk_obj
+ nerveFunctor₂
+ nerveRightExtension
+ nerveRightExtension.coneAt
+ nerve₂
+ nerve₂RestrictedIso
+ nerve₂_restrictedNerve
+ of
+ of_val
+ of_α
+ opposite
+ opstuff.{w}
+ pt
+ pt'
+ ran.lift
+ ran.lift'
+ ran.lift.eq
+ ran.lift.eq₂
+ ran.lift.map
+ skAdj
+ skAdj.coreflective
+ skeleton.faithful
+ skeleton.full
+ skeleton.fullyFaithful
+ skeleton_reflective
+ str'
+ strArr.homEv
+ strArr.homEv.map
+ strArr.homEvSucc
+ toFunctor
+ toQuiv
+ Δ
+ Δ.ι
++ truncation
+++ comp_eq_comp
+++ id_eq_id
-- sk

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
  By Dependent Issues (🤖). Happy coding!

[joelriou]

I would suggest moving the file AlgebraicTopology.HomotopyCat to AlgebraicTopology.SimplicialSet.HomotopyCat (and then SimplicalSet should become SimplicialSet.Basic).