Commit 2025-04-02 22:43 164bfe1e

View on Github →

feat(Category Theory): unbundled quiver adjunction data (#22443) This unbundles the unit and counit components from Quiv.adj and proves they equal the previously defined (pre)functors Paths.of and pathComposition. The unbundled Quiv.adj adjunction data is used to golf the construction of ReflQuiv.adj.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/CategoryTheory/Category/Cat.lean

added def CategoryTheory.Functor.ofCatHom

added theorem CategoryTheory.Functor.of_toCatHom

added def CategoryTheory.Functor.toCatHom

added theorem CategoryTheory.Functor.to_ofCatHom

Modified Mathlib/CategoryTheory/Category/Quiv.lean

added def CategoryTheory.Cat.freeMap

added def CategoryTheory.Cat.freeMapCompIso

added def CategoryTheory.Cat.freeMapIdIso

added theorem CategoryTheory.Cat.freeMap_comp

added theorem CategoryTheory.Cat.freeMap_id

added def CategoryTheory.Prefunctor.ofQuivHom

added theorem CategoryTheory.Prefunctor.of_toQuivHom

added def CategoryTheory.Prefunctor.toQuivHom

added theorem CategoryTheory.Prefunctor.to_ofQuivHom

added theorem CategoryTheory.Quiv.adj_homEquiv

added def CategoryTheory.Quiv.freeMapPathsOfCompPathCompositionIso

added theorem CategoryTheory.Quiv.freeMap_pathsOf_pathComposition

modified def CategoryTheory.Quiv.lift

added def CategoryTheory.Quiv.pathCompositionNaturality

added theorem CategoryTheory.Quiv.pathComposition_naturality

added def CategoryTheory.Quiv.pathsEquiv

added theorem CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor

added theorem CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

modified def CategoryTheory.Cat.FreeRefl.quotientFunctor

modified def CategoryTheory.Cat.FreeRefl

added def CategoryTheory.Cat.freeReflMap

added theorem CategoryTheory.Cat.freeReflMap_naturality

deleted theorem CategoryTheory.Cat.freeRefl_naturality

Modified Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

modified def CategoryTheory.Localization.Construction.ψ₁

Modified Mathlib/CategoryTheory/PathCategory/Basic.lean

modified theorem CategoryTheory.Paths.lift_spec

Modified Mathlib/CategoryTheory/PathCategory/MorphismProperty.lean

added def CategoryTheory.Paths.liftNatIso

added def CategoryTheory.Paths.liftNatTrans

added theorem CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative

Modified Mathlib/Combinatorics/Quiver/Path.lean

added theorem Prefunctor.mapPath_comp_apply

added theorem Prefunctor.mapPath_id