HomLift

📁 Source: Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

Statistics

Metric	Count
Definitions IsHomLift, isoOfIsoLift, tacticSubst_hom_lift___	3
Theorems codomain_eq, commSq, comp, comp_eqToHom_lift, comp_eqToHom_lift_iff, comp_id_lift, comp_lift_id_left, comp_lift_id_left', comp_lift_id_right, comp_lift_id_right', comp_of_lift_id, domain_eq, eqToHom_codomain_lift_id, eqToHom_comp_lift, eqToHom_comp_lift_iff, eqToHom_domain_lift_id, eq_of_isHomLift, fac, fac', id, id_comp_lift, id_lift_eqToHom_codomain, id_lift_eqToHom_domain, instIsHomLiftIdObj, inv, inv_lift, inv_lift_inv, isIso_of_lift_isIso, isoOfIsoLift_hom, isoOfIsoLift_hom_inv_id, isoOfIsoLift_inv_hom_id, lift_comp_eqToHom, lift_comp_eqToHom_iff, lift_comp_id, lift_eqToHom_comp, lift_eqToHom_comp_iff, lift_id_comp, lift_id_inv, lift_id_inv_isIso, map, of_commSq, of_commsq, of_fac, of_fac'	44
Total	47

CategoryTheory

Definitions

Name	Category	Theorems
tacticSubst_hom_lift___ 📖	CompOp	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsHomLift 📖	CompData	65 math math: CategoryTheory.IsHomLift.eqToHom_domain_lift_id, IsStronglyCartesian.domainUniqueUpToIso_hom_isHomLift, CategoryTheory.IsHomLift.comp_lift_id_right', CategoryTheory.IsHomLift.inv_lift, CategoryTheory.IsHomLift.map, CategoryTheory.IsHomLift.of_fac, CategoryTheory.IsHomLift.inv_lift_inv, CategoryTheory.IsHomLift.comp_eqToHom_lift_iff, CategoryTheory.IsHomLift.eqToHom_comp_lift, CategoryTheory.IsHomLift.of_fac', IsCocartesian.toIsHomLift, IsStronglyCocartesian.toIsHomLift, IsStronglyCocartesian.universal_property', IsCartesian.domainUniqueUpToIso_inv_isHomLift, HasFibers.homLift, CategoryTheory.IsHomLift.comp_lift_id_right, CategoryTheory.IsHomLift.lift_comp_eqToHom, CategoryTheory.BasedNatTrans.isHomLift', CategoryTheory.IsHomLift.id, CategoryTheory.BasedFunctor.isHomLift_map, CategoryTheory.IsHomLift.id_comp_lift, CategoryTheory.IsHomLift.comp, CategoryTheory.IsHomLift.lift_id_comp, IsCartesian.universal_property, IsStronglyCartesian.universal_property', IsStronglyCocartesian.map_isHomLift, HasFibers.Fib.mkIsoSelfIsHomLift, CategoryTheory.IsHomLift.lift_eqToHom_comp_iff, IsStronglyCartesian.domainUniqueUpToIso_inv_isHomLift, CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_cartesianLift, CategoryTheory.IsHomLift.comp_of_lift_id, CategoryTheory.IsHomLift.comp_lift_id_left', Fiber.instIsHomLiftIdMapFiberInclusion, IsCocartesian.universal_property, CategoryTheory.IsHomLift.lift_eqToHom_comp, CategoryTheory.IsHomLift.id_lift_eqToHom_domain, CategoryTheory.IsHomLift.comp_lift_id_left, CategoryTheory.IsHomLift.lift_comp_eqToHom_iff, IsCocartesian.map_isHomLift, CategoryTheory.IsHomLift.of_commSq, CategoryTheory.IsHomLift.lift_id_inv_isIso, CategoryTheory.IsHomLift.comp_id_lift, CategoryTheory.IsHomLift.id_lift_eqToHom_codomain, IsStronglyCartesian.universal_property, CategoryTheory.IsHomLift.of_commsq, CategoryTheory.IsHomLift.lift_id_inv, CategoryTheory.BasedFunctor.instIsHomLiftObjPIdObj, IsCartesian.domainUniqueUpToIso_hom_isHomLift, CategoryTheory.BasedFunctor.isHomLift_iff, CategoryTheory.BasedFunctor.preserves_isHomLift, IsStronglyCartesian.toIsHomLift, IsCartesian.map_isHomLift, CategoryTheory.IsHomLift.comp_eqToHom_lift, HasFibers.inducedFunctor_map_coe, CategoryTheory.IsHomLift.eqToHom_comp_lift_iff, CategoryTheory.IsHomLift.lift_comp_id, CategoryTheory.IsHomLift.eqToHom_codomain_lift_id, CategoryTheory.IsHomLift.instIsHomLiftIdObj, IsStronglyCartesian.map_isHomLift, CategoryTheory.IsHomLift.inv, CategoryTheory.BasedNatTrans.app_isHomLift, CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_homCartesianLift, IsStronglyCocartesian.universal_property, CategoryTheory.BasedNatTrans.isHomLift, IsCartesian.toIsHomLift

CategoryTheory.IsHomLift

Definitions

Name	Category	Theorems
isoOfIsoLift 📖	CompOp	4 math math: inv_lift, isoOfIsoLift_hom, isoOfIsoLift_hom_inv_id, isoOfIsoLift_inv_hom_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codomain_eq 📖	mathematical	—	CategoryTheory.Functor.obj	—	—
commSq 📖	mathematical	—	CategoryTheory.CommSq CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct domain_eq codomain_eq	—	domain_eq codomain_eq fac CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp
comp 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	of_commSq domain_eq codomain_eq CategoryTheory.Functor.map_comp CategoryTheory.CommSq.horiz_comp commSq
comp_eqToHom_lift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp
comp_eqToHom_lift_iff 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp comp_eqToHom_lift
comp_id_lift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp
comp_lift_id_left 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.id_comp comp
comp_lift_id_left' 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	comp_lift_id_left codomain_eq domain_eq
comp_lift_id_right 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id comp
comp_lift_id_right' 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	comp_lift_id_right codomain_eq domain_eq
comp_of_lift_id 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	—	comp CategoryTheory.Category.comp_id
domain_eq 📖	mathematical	—	CategoryTheory.Functor.obj	—	—
eqToHom_codomain_lift_id 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
eqToHom_comp_lift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id
eqToHom_comp_lift_iff 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id eqToHom_comp_lift
eqToHom_domain_lift_id 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
eq_of_isHomLift 📖	mathematical	—	CategoryTheory.Functor.map	—	domain_eq codomain_eq fac CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.eqToHom domain_eq CategoryTheory.Functor.map codomain_eq	—	domain_eq codomain_eq CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
fac' 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.eqToHom domain_eq codomain_eq	—	domain_eq codomain_eq CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
id 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	instIsHomLiftIdObj
id_comp_lift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.comp_id
id_lift_eqToHom_codomain 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsHomLift CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
id_lift_eqToHom_domain 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsHomLift CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
instIsHomLiftIdObj 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Functor.map_id map
inv 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.inv	—	inv_lift_inv
inv_lift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.Iso.inv isoOfIsoLift	—	of_commSq codomain_eq domain_eq CategoryTheory.CommSq.horiz_inv commSq
inv_lift_inv 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.Iso.inv	—	of_commSq codomain_eq domain_eq CategoryTheory.CommSq.horiz_inv commSq
isIso_of_lift_isIso 📖	mathematical	—	CategoryTheory.IsIso	—	domain_eq codomain_eq CategoryTheory.IsIso.comp_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.Functor.map_isIso fac
isoOfIsoLift_hom 📖	mathematical	—	CategoryTheory.Iso.hom isoOfIsoLift	—	—
isoOfIsoLift_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv isoOfIsoLift CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
isoOfIsoLift_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv isoOfIsoLift CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
lift_comp_eqToHom 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id
lift_comp_eqToHom_iff 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id lift_comp_eqToHom
lift_comp_id 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.comp_id
lift_eqToHom_comp 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp
lift_eqToHom_comp_iff 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp lift_eqToHom_comp
lift_id_comp 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp
lift_id_inv 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	CategoryTheory.IsIso.id inv_lift_inv CategoryTheory.IsIso.inv_id
lift_id_inv_isIso 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.inv	—	CategoryTheory.IsIso.id inv CategoryTheory.IsIso.inv_id
map 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
of_commSq 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.CommSq CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.IsHomLift	—	of_commsq CategoryTheory.CommSq.w
of_commsq 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.eqToHom	CategoryTheory.Functor.IsHomLift	—	map CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
of_fac 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor.map	CategoryTheory.Functor.IsHomLift	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
of_fac' 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	CategoryTheory.Functor.IsHomLift	—	map CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

---

← Back to Index