Cartesian

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

Statistics

Metric	Count
Definitions IsCartesian, domainUniqueUpToIso, map, IsStronglyCartesian, domainIsoOfBaseIso, map	6
Theorems domainUniqueUpToIso_hom, domainUniqueUpToIso_hom_isHomLift, domainUniqueUpToIso_inv, domainUniqueUpToIso_inv_isHomLift, ext, fac, fac_assoc, map_isHomLift, map_self, map_uniq, of_comp_iso, of_iso_comp, toIsHomLift, universal_property, comp, domainIsoOfBaseIso_hom, domainIsoOfBaseIso_inv, domainUniqueUpToIso_hom_isHomLift, domainUniqueUpToIso_inv_isHomLift, ext, fac, fac_assoc, isCartesian_of_isStronglyCartesian, isIso_of_base_isIso, map_comp_map, map_comp_map_assoc, map_isHomLift, map_self, map_uniq, of_comp, of_isIso, of_iso, toIsHomLift, universal_property, universal_property'	35
Total	41

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsCartesian 📖	CompData	9 math math: IsPreFibered.exists_isCartesian', IsFibered.comp, IsStronglyCartesian.isCartesian_of_isStronglyCartesian, IsCartesian.of_iso_comp, CategoryTheory.instIsCartesianCompOfIsFibered, IsCartesian.of_comp_iso, HasFibers.pullbackMap.isCartesian, IsPreFibered.pullbackMap.IsCartesian, CategoryTheory.IsPreFibered.exists_isCartesian
IsStronglyCartesian 📖	CompData	7 math math: IsStronglyCartesian.of_comp, IsStronglyCartesian.of_isIso, IsFibered.isStronglyCartesian_of_isCartesian, IsStronglyCartesian.comp, IsStronglyCartesian.of_iso, CategoryTheory.Pseudofunctor.CoGrothendieck.isStronglyCartesian_homCartesianLift, HasFibers.fiber_factorization

CategoryTheory.Functor.IsCartesian

Definitions

Name	Category	Theorems
domainUniqueUpToIso 📖	CompOp	4 math math: domainUniqueUpToIso_inv_isHomLift, domainUniqueUpToIso_inv, domainUniqueUpToIso_hom, domainUniqueUpToIso_hom_isHomLift
map 📖	CompOp	7 math math: map_self, fac_assoc, domainUniqueUpToIso_inv, domainUniqueUpToIso_hom, map_uniq, fac, map_isHomLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domainUniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom domainUniqueUpToIso map toIsHomLift	—	—
domainUniqueUpToIso_hom_isHomLift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv domainUniqueUpToIso	—	toIsHomLift map_isHomLift domainUniqueUpToIso_inv
domainUniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv domainUniqueUpToIso map toIsHomLift	—	—
domainUniqueUpToIso_inv_isHomLift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom domainUniqueUpToIso	—	toIsHomLift map_isHomLift domainUniqueUpToIso_hom
ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.IsHomLift.comp_lift_id_left toIsHomLift map_uniq
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map	—	universal_property
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
map_isHomLift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct map	—	universal_property
map_self 📖	mathematical	—	map toIsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	toIsHomLift map_uniq CategoryTheory.IsHomLift.instIsHomLiftIdObj CategoryTheory.Category.id_comp
map_uniq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	map	—	universal_property
of_comp_iso 📖	mathematical	—	CategoryTheory.Functor.IsCartesian CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	CategoryTheory.IsHomLift.comp_lift_id_right toIsHomLift CategoryTheory.IsHomLift.lift_id_inv map_isHomLift fac_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id map_uniq CategoryTheory.Iso.eq_comp_inv
of_iso_comp 📖	mathematical	—	CategoryTheory.Functor.IsCartesian CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	CategoryTheory.IsHomLift.comp_lift_id_left toIsHomLift CategoryTheory.IsHomLift.comp_of_lift_id map_isHomLift CategoryTheory.IsHomLift.lift_id_inv CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc fac CategoryTheory.Iso.eq_comp_inv map_uniq
toIsHomLift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift	—	—
universal_property 📖	mathematical	—	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.IsHomLift CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.comp	—	—

CategoryTheory.Functor.IsStronglyCartesian

Definitions

Name	Category	Theorems
domainIsoOfBaseIso 📖	CompOp	4 math math: domainUniqueUpToIso_hom_isHomLift, domainIsoOfBaseIso_hom, domainIsoOfBaseIso_inv, domainUniqueUpToIso_inv_isHomLift
map 📖	CompOp	9 math math: domainIsoOfBaseIso_hom, map_self, domainIsoOfBaseIso_inv, map_uniq, map_comp_map_assoc, fac, fac_assoc, map_isHomLift, map_comp_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	CategoryTheory.Functor.IsStronglyCartesian CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.IsHomLift.comp toIsHomLift CategoryTheory.Category.assoc map_isHomLift fac map_uniq
domainIsoOfBaseIso_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	domainIsoOfBaseIso map toIsHomLift	—	—
domainIsoOfBaseIso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Iso.inv domainIsoOfBaseIso map	—	—
domainUniqueUpToIso_hom_isHomLift 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Functor.IsHomLift CategoryTheory.Iso.inv domainIsoOfBaseIso	—	CategoryTheory.Iso.inv_hom_id_assoc map.congr_simp CategoryTheory.Functor.IsCartesian.toIsHomLift isCartesian_of_isStronglyCartesian map_isHomLift
domainUniqueUpToIso_inv_isHomLift 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Functor.IsHomLift domainIsoOfBaseIso	—	toIsHomLift map_isHomLift domainIsoOfBaseIso_hom
ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.IsHomLift.comp toIsHomLift map_uniq
fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	map	—	universal_property
fac_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
isCartesian_of_isStronglyCartesian 📖	mathematical	—	CategoryTheory.Functor.IsCartesian	—	toIsHomLift universal_property CategoryTheory.Category.id_comp
isIso_of_base_isIso 📖	mathematical	—	CategoryTheory.IsIso	—	toIsHomLift CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsHomLift.instIsHomLiftIdObj fac CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsHomLift.comp CategoryTheory.IsHomLift.map map_isHomLift ext CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_comp_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	map toIsHomLift	—	map_uniq toIsHomLift CategoryTheory.IsHomLift.comp map_isHomLift CategoryTheory.Category.assoc fac
map_comp_map_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	map toIsHomLift	—	toIsHomLift CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp_map
map_isHomLift 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.IsHomLift map	—	universal_property
map_self 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CategoryStruct.comp CategoryTheory.Category.id_comp toIsHomLift	—	toIsHomLift CategoryTheory.Category.id_comp map_uniq CategoryTheory.IsHomLift.instIsHomLiftIdObj
map_uniq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	map	—	universal_property
of_comp 📖	mathematical	—	CategoryTheory.Functor.IsStronglyCartesian	—	CategoryTheory.Category.assoc CategoryTheory.IsHomLift.comp toIsHomLift map_isHomLift ext fac map_uniq
of_isIso 📖	mathematical	—	CategoryTheory.Functor.IsStronglyCartesian	—	of_iso
of_iso 📖	mathematical	—	CategoryTheory.Functor.IsStronglyCartesian CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.IsHomLift.isoOfIsoLift_hom_inv_id CategoryTheory.IsHomLift.comp CategoryTheory.IsHomLift.inv_lift CategoryTheory.Iso.hom_inv_id
toIsHomLift 📖	mathematical	—	CategoryTheory.Functor.IsHomLift	—	—
universal_property 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.IsHomLift	—	universal_property'
universal_property' 📖	mathematical	—	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.IsHomLift CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp	—	—

---

← Back to Index