Commit 2025-06-16 08:15 5f557fc4

View on Github →

feat(FiberedCategory/Grothendieck): the Grothendieck construction is fibered (#25645) This PR shows that the Grothendieck construction is fibered and comes equipped with a natural HasFibers instance. This is a combination of #21985 with some old work I had on this lying around.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Fiber.lean

added theorem CategoryTheory.Functor.Fiber.fiberInclusion_obj_inj

modified def CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf

added theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp_map

added theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp_obj

deleted theorem CategoryTheory.Functor.Fiber.inducedFunctor_map

Created Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean

added def CategoryTheory.Pseudofunctor.Grothendieck.compIso

added theorem CategoryTheory.Pseudofunctor.Grothendieck.comp_const

added theorem CategoryTheory.Pseudofunctor.Grothendieck.isStronglyCartesian_homCartesianLift

added def CategoryTheory.Pseudofunctor.Grothendieck.ι

Modified Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean