Commit 2024-06-04 16:04 17552eb4

View on Github →

feat(FiberedCategory/HomLift): definition of IsHomLift (#12978) We define the notion IsHomLift which aims to provide API for working with equalities p(\phi) = f for a functor p and morphisms \phi, f. This API is extensively used in an upcoming PR defining the notion of fibered categories. See the repository Stacks-project for WIP using this notion.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

added theorem CategoryTheory.IsHomLift.codomain_eq

added theorem CategoryTheory.IsHomLift.commSq

added theorem CategoryTheory.IsHomLift.comp_eqToHom_lift_iff

added theorem CategoryTheory.IsHomLift.comp_lift_id_left

added theorem CategoryTheory.IsHomLift.comp_lift_id_right

added theorem CategoryTheory.IsHomLift.domain_eq

added theorem CategoryTheory.IsHomLift.eqToHom_codomain_lift_id

added theorem CategoryTheory.IsHomLift.eqToHom_comp_lift_iff

added theorem CategoryTheory.IsHomLift.eqToHom_domain_lift_id

added theorem CategoryTheory.IsHomLift.eq_of_isHomLift

added theorem CategoryTheory.IsHomLift.fac'

added theorem CategoryTheory.IsHomLift.fac

added theorem CategoryTheory.IsHomLift.id_lift_eqToHom_codomain

added theorem CategoryTheory.IsHomLift.id_lift_eqToHom_domain

added theorem CategoryTheory.IsHomLift.isIso_of_lift_isIso

added def CategoryTheory.IsHomLift.isoOfIsoLift

added theorem CategoryTheory.IsHomLift.isoOfIsoLift_hom_inv_id

added theorem CategoryTheory.IsHomLift.isoOfIsoLift_inv_hom_id

added theorem CategoryTheory.IsHomLift.lift_comp_eqToHom_iff

added theorem CategoryTheory.IsHomLift.lift_eqToHom_comp_iff

added theorem CategoryTheory.IsHomLift.of_commSq

added theorem CategoryTheory.IsHomLift.of_fac'

added theorem CategoryTheory.IsHomLift.of_fac

added inductive CategoryTheory.IsHomLiftAux