Commit 2024-10-19 13:51 92412db7

View on Github →

feat(FiberedCategory/Fiber): define the fibers of a functor (#13603) We define the fibers of a functor p : 𝒳 ⥤ 𝒮 over objects S : 𝒮, and develop some basic API. Relatively little API is developed as in an upcoming PR we introduce a class HasFibers which should be preferred.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/FiberedCategory/Fiber.lean

added def CategoryTheory.Functor.Fiber.fiberInclusion

added def CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst

added theorem CategoryTheory.Functor.Fiber.fiberInclusion_comp_eq_const

added theorem CategoryTheory.Functor.Fiber.fiberInclusion_homMk

added theorem CategoryTheory.Functor.Fiber.fiberInclusion_mk

added def CategoryTheory.Functor.Fiber.homMk

added theorem CategoryTheory.Functor.Fiber.homMk_comp

added theorem CategoryTheory.Functor.Fiber.homMk_id

added theorem CategoryTheory.Functor.Fiber.hom_ext

added def CategoryTheory.Functor.Fiber.inducedFunctor

added def CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf

added theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp

added theorem CategoryTheory.Functor.Fiber.inducedFunctor_map

added def CategoryTheory.Functor.Fiber.mk

added def CategoryTheory.Functor.Fiber

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

added theorem CategoryTheory.IsHomLift.of_commsq