Commit 2024-11-30 19:56 4fafb9f5

View on Github →

feat(CategoryTheory): Relation between the Grothendieck construction and AsSmall (#19539)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Cat.asSmallFunctor

Modified Mathlib/CategoryTheory/Category/ULift.lean

added theorem CategoryTheory.down_comp

added theorem CategoryTheory.eqToHom_down

Modified Mathlib/CategoryTheory/Grothendieck.lean

added def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence

added def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor

added def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse

added def CategoryTheory.Grothendieck.mapWhiskerRightAsSmallFunctor