Commit 2024-08-12 22:49 577bed1b

View on Github →

feat(CategoryTheory/Adjunction): typeToCat is right adjoint to connectedComponents functor (#15614) The embedding of Type into Cat, which views a set as a discrete category, is right adjoint to the functor connectedComponents : Cat -> Set which maps a category to its set of connected components.

Estimated changes

Modified Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

added def CategoryTheory.Cat.connectedComponents

added def CategoryTheory.Cat.connectedComponentsTypeToCatAdj

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

added def CategoryTheory.ConnectedComponents.functorToDiscrete

added def CategoryTheory.ConnectedComponents.liftFunctor

added def CategoryTheory.ConnectedComponents.typeToCatHomEquiv

Modified Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.eq_of_zag

added theorem CategoryTheory.eq_of_zigzag