Commit 2025-02-28 01:41 6dba2e5d

View on Github →

feat(AlgebraicTopology/NerveAdjunction): nerve adjunction, Cat has colimits (#16784) 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 eriehl@jhu.edu and Pietro Monticone 38562595+pitmonticone@users.noreply.github.com

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

added def CategoryTheory.nerve₂Adj.unit.app

added theorem CategoryTheory.nerve₂Adj.unit.map_app_eq

added theorem CategoryTheory.nerve₂Adj.unit.naturality

added def CategoryTheory.nerve₂Adj.unit

Modified Mathlib/CategoryTheory/Category/Cat.lean

added theorem CategoryTheory.Cat.coe_of

Created Mathlib/CategoryTheory/Category/Cat/Colimit.lean

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

modified def CategoryTheory.ReflQuiv.adj.counit.app

added theorem CategoryTheory.ReflQuiv.adj.counit.comp_app_eq

deleted theorem CategoryTheory.ReflQuiv.adj.counit.component_eq'

deleted theorem CategoryTheory.ReflQuiv.adj.counit.component_eq

modified def CategoryTheory.ReflQuiv.adj.unit.app

deleted theorem CategoryTheory.ReflQuiv.adj.unit.component_eq

added theorem CategoryTheory.ReflQuiv.adj.unit.map_app_eq

deleted theorem CategoryTheory.ReflQuiv.forget.Faithful

Modified Mathlib/Combinatorics/Quiver/ReflQuiver.lean

added theorem CategoryTheory.Functor.toReflPrefunctor.map_comp