Commit 2024-07-19 09:35 b6c5f73a

View on Github →

feat(FiberedCategory/Cartesian): define strongly cartesian morphisms (#13410) We define strongly cartesian morphisms with respect to a functor p : 𝒳 ⥤ 𝒮, as in 02XK. We provide some basic API, and prove some basic properties.

Estimated changes

Modified Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

deleted theorem CategoryTheory.Functor.IsCartesian.eq_of_fac

added theorem CategoryTheory.Functor.IsStronglyCartesian.fac

added theorem CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIso

added theorem CategoryTheory.Functor.IsStronglyCartesian.map_comp_map

added theorem CategoryTheory.Functor.IsStronglyCartesian.map_self

added theorem CategoryTheory.Functor.IsStronglyCartesian.map_uniq

added theorem CategoryTheory.Functor.IsStronglyCartesian.universal_property