Commit 2023-02-21 07:31 23092673

View on Github →

feat: port CategoryTheory.Category.Ulift (#2312)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/ULift.lean

added def CategoryTheory.AsSmall.down

added def CategoryTheory.AsSmall.equiv

added def CategoryTheory.AsSmall.up

added def CategoryTheory.AsSmall.{w,

added def CategoryTheory.ULift.downFunctor

added def CategoryTheory.ULift.equivalence

added def CategoryTheory.ULift.upFunctor

added def CategoryTheory.ULiftHom.down

added def CategoryTheory.ULiftHom.equiv

added def CategoryTheory.ULiftHom.objDown

added def CategoryTheory.ULiftHom.objUp

added def CategoryTheory.ULiftHom.up

added def CategoryTheory.ULiftHom.{w,u}

added def CategoryTheory.ULiftHomULiftCategory.equiv.{v',

added theorem CategoryTheory.objDown_objUp

added theorem CategoryTheory.objUp_objDown