Commit 2024-06-23 15:38 41c8f830

View on Github →

feat(FiberedCategory/BasedCategory): add bicategory of based categories (#13545) We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean

added def CategoryTheory.BasedCategory.ofFunctor

added def CategoryTheory.BasedCategory.whiskerLeft

added def CategoryTheory.BasedCategory.whiskerRight

added structure CategoryTheory.BasedCategory

added def CategoryTheory.BasedFunctor.comp

added theorem CategoryTheory.BasedFunctor.comp_assoc

added theorem CategoryTheory.BasedFunctor.comp_id

added def CategoryTheory.BasedFunctor.id

added theorem CategoryTheory.BasedFunctor.id_comp

added theorem CategoryTheory.BasedFunctor.isHomLift_iff

added theorem CategoryTheory.BasedFunctor.isHomLift_map

added theorem CategoryTheory.BasedFunctor.w_obj

added structure CategoryTheory.BasedFunctor

added def CategoryTheory.BasedNatIso.id

added theorem CategoryTheory.BasedNatIso.isIso_of_toNatTrans_isIso

added def CategoryTheory.BasedNatIso.mkNatIso

added def CategoryTheory.BasedNatTrans.comp

added theorem CategoryTheory.BasedNatTrans.ext

added def CategoryTheory.BasedNatTrans.forgetful

added theorem CategoryTheory.BasedNatTrans.homCategory.ext

added def CategoryTheory.BasedNatTrans.id

added theorem CategoryTheory.BasedNatTrans.isHomLift

added structure CategoryTheory.BasedNatTrans

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean