Commit 2025-06-19 04:46 2806fcd6

View on Github →

feat(Bicategory/Grothendieck): functoriality of the grothendieck construction (#18285) This PR is the start towards proving functoriality of the Grothendieck construction.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

modified def CategoryTheory.Pseudofunctor.Grothendieck.forget

added def CategoryTheory.Pseudofunctor.Grothendieck.map

added def CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso

added def CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_comp_eq

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_comp_forget

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_id_eq

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_id_map

modified structure CategoryTheory.Pseudofunctor.Grothendieck

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv

added theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso

Modified Mathlib/CategoryTheory/Category/Cat.lean

added theorem CategoryTheory.Cat.ext