Commit 2024-06-18 06:24 edd8186c

View on Github →

feat(FiberedCategory/Cartesian): define cartesian morphisms (#13393) We define cartesian morphisms with respect to a functor p : 𝒳 ⥤ 𝒮, as in SGA 1 VI 5.1. We also provide some basic API for working with the universal property.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

added theorem CategoryTheory.Functor.IsCartesian.eq_of_fac

added theorem CategoryTheory.Functor.IsCartesian.fac

added theorem CategoryTheory.Functor.IsCartesian.map_self

added theorem CategoryTheory.Functor.IsCartesian.map_uniq

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

added theorem CategoryTheory.IsHomLift.comp_lift_id_left'

deleted theorem CategoryTheory.IsHomLift.comp_lift_id_left

added theorem CategoryTheory.IsHomLift.comp_lift_id_right'

deleted theorem CategoryTheory.IsHomLift.comp_lift_id_right