Limits

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Limits.lean

Statistics

Metric	Count
Definitions preservesColimitIso, preservesColimitNatIso, preservesLimitIso, preservesLimitNatIso	4
Theorems instIsIsoPost, instIsIsoPost_1, lift_comp_preservesLimitIso_hom, lift_comp_preservesLimitIso_hom_assoc, preservesColimitIso_inv_comp_desc, preservesColimitIso_inv_comp_desc_assoc, preservesColimitNatIso_hom_app, preservesColimitNatIso_inv_app, preservesColimit_of_isIso_post, preservesLimitIso_hom_π, preservesLimitIso_hom_π_assoc, preservesLimitIso_inv_π, preservesLimitIso_inv_π_assoc, preservesLimitNatIso_hom_app, preservesLimitNatIso_inv_app, preservesLimit_of_isIso_post, preserves_desc_mapCocone, preserves_lift_mapCone, ι_preservesColimitIso_hom, ι_preservesColimitIso_hom_assoc, ι_preservesColimitIso_inv, ι_preservesColimitIso_inv_assoc	22
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
preservesColimitIso 📖	CompOp	10 math math: preservesColimitNatIso_inv_app, ι_preservesColimitIso_inv_assoc, ι_preservesColimitIso_hom_assoc, preservesColimitIso_inv_comp_desc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, preservesColimitNatIso_hom_app, preservesColimitIso_inv_comp_desc_assoc, PresheafOfModules.colimitPresheafOfModules_map, ι_preservesColimitIso_hom, ι_preservesColimitIso_inv
preservesColimitNatIso 📖	CompOp	2 math math: preservesColimitNatIso_inv_app, preservesColimitNatIso_hom_app
preservesLimitIso 📖	CompOp	11 math math: PresheafOfModules.limitPresheafOfModules_map, Limits.fiberwiseColimitLimitIso_hom_app, preservesLimitIso_inv_π_assoc, lift_comp_preservesLimitIso_hom_assoc, preservesLimitIso_inv_π, preservesLimitNatIso_inv_app, lift_comp_preservesLimitIso_hom, Limits.fiberwiseColimitLimitIso_inv_app, preservesLimitIso_hom_π_assoc, preservesLimitIso_hom_π, preservesLimitNatIso_hom_app
preservesLimitNatIso 📖	CompOp	2 math math: preservesLimitNatIso_inv_app, preservesLimitNatIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoPost 📖	mathematical	—	IsIso Functor.obj Limits.limit Functor.comp Limits.instHasLimitCompOfPreservesLimit Limits.limit.post	—	Limits.instHasLimitCompOfPreservesLimit Iso.isIso_hom
instIsIsoPost_1 📖	mathematical	—	IsIso Limits.colimit Functor.comp Limits.instHasColimitCompOfPreservesColimit Functor.obj Limits.colimit.post	—	Limits.instHasColimitCompOfPreservesColimit Iso.isIso_inv
lift_comp_preservesLimitIso_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.Cone.pt Limits.limit Functor.comp Limits.instHasLimitCompOfPreservesLimit Functor.map Limits.limit.lift Iso.hom preservesLimitIso Functor.mapCone	—	Limits.limit.hom_ext Limits.instHasLimitCompOfPreservesLimit Category.assoc preservesLimitIso_hom_π Functor.map_comp Limits.limit.lift_π
lift_comp_preservesLimitIso_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.Cone.pt Limits.limit Functor.map Limits.limit.lift Functor.comp Limits.instHasLimitCompOfPreservesLimit Iso.hom preservesLimitIso Functor.mapCone	—	Limits.instHasLimitCompOfPreservesLimit Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_preservesLimitIso_hom
preservesColimitIso_inv_comp_desc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.colimit Functor.comp Limits.instHasColimitCompOfPreservesColimit Functor.obj Limits.Cocone.pt Iso.inv preservesColimitIso Functor.map Limits.colimit.desc Functor.mapCocone	—	Limits.colimit.hom_ext Limits.instHasColimitCompOfPreservesColimit ι_preservesColimitIso_inv_assoc Functor.map_comp Limits.colimit.ι_desc
preservesColimitIso_inv_comp_desc_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.colimit Functor.comp Limits.instHasColimitCompOfPreservesColimit Functor.obj Iso.inv preservesColimitIso Limits.Cocone.pt Functor.map Limits.colimit.desc Functor.mapCocone	—	Limits.instHasColimitCompOfPreservesColimit Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preservesColimitIso_inv_comp_desc
preservesColimitNatIso_hom_app 📖	mathematical	—	NatTrans.app Functor Functor.category Functor.comp Limits.colim Functor.obj Functor.whiskeringRight Iso.hom preservesColimitNatIso Limits.colimit Limits.hasColimitOfHasColimitsOfShape preservesColimitIso Limits.PreservesColimitsOfShape.preservesColimit	—	—
preservesColimitNatIso_inv_app 📖	mathematical	—	NatTrans.app Functor Functor.category Functor.comp Functor.obj Functor.whiskeringRight Limits.colim Iso.inv preservesColimitNatIso Limits.colimit Limits.hasColimitOfHasColimitsOfShape preservesColimitIso Limits.PreservesColimitsOfShape.preservesColimit	—	—
preservesColimit_of_isIso_post 📖	mathematical	—	Limits.PreservesColimit	—	Limits.preservesColimit_of_preserves_colimit_cocone
preservesLimitIso_hom_π 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.limit Functor.comp Limits.instHasLimitCompOfPreservesLimit Iso.hom preservesLimitIso Limits.limit.π Functor.map	—	Limits.IsLimit.conePointUniqueUpToIso_hom_comp Limits.instHasLimitCompOfPreservesLimit
preservesLimitIso_hom_π_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.limit Functor.comp Limits.instHasLimitCompOfPreservesLimit Iso.hom preservesLimitIso Limits.limit.π Functor.map	—	Limits.instHasLimitCompOfPreservesLimit Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preservesLimitIso_hom_π
preservesLimitIso_inv_π 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.limit Functor.comp Limits.instHasLimitCompOfPreservesLimit Functor.obj Iso.inv preservesLimitIso Functor.map Limits.limit.π	—	Limits.IsLimit.conePointUniqueUpToIso_inv_comp Limits.instHasLimitCompOfPreservesLimit
preservesLimitIso_inv_π_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.limit Functor.comp Limits.instHasLimitCompOfPreservesLimit Functor.obj Iso.inv preservesLimitIso Functor.map Limits.limit.π	—	Limits.instHasLimitCompOfPreservesLimit Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preservesLimitIso_inv_π
preservesLimitNatIso_hom_app 📖	mathematical	—	NatTrans.app Functor Functor.category Functor.comp Limits.lim Functor.obj Functor.whiskeringRight Iso.hom preservesLimitNatIso Limits.limit Limits.hasLimitOfHasLimitsOfShape preservesLimitIso Limits.PreservesLimitsOfShape.preservesLimit	—	—
preservesLimitNatIso_inv_app 📖	mathematical	—	NatTrans.app Functor Functor.category Functor.comp Functor.obj Functor.whiskeringRight Limits.lim Iso.inv preservesLimitNatIso Limits.limit Limits.hasLimitOfHasLimitsOfShape preservesLimitIso Limits.PreservesLimitsOfShape.preservesLimit	—	—
preservesLimit_of_isIso_post 📖	mathematical	—	Limits.PreservesLimit	—	Limits.preservesLimit_of_preserves_limit_cone
preserves_desc_mapCocone 📖	mathematical	—	Limits.IsColimit.desc Functor.comp Functor.mapCocone Limits.isColimitOfPreserves Functor.map Limits.Cocone.pt	—	Limits.IsColimit.uniq Functor.map_comp Limits.IsColimit.fac
preserves_lift_mapCone 📖	mathematical	—	Limits.IsLimit.lift Functor.comp Functor.mapCone Limits.isLimitOfPreserves Functor.map Limits.Cone.pt	—	Limits.IsLimit.uniq Functor.map_comp Limits.IsLimit.fac
ι_preservesColimitIso_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.colimit Functor.comp Limits.instHasColimitCompOfPreservesColimit Functor.map Limits.colimit.ι Iso.hom preservesColimitIso	—	Limits.IsColimit.comp_coconePointUniqueUpToIso_hom Limits.instHasColimitCompOfPreservesColimit
ι_preservesColimitIso_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.colimit Functor.map Limits.colimit.ι Functor.comp Limits.instHasColimitCompOfPreservesColimit Iso.hom preservesColimitIso	—	Limits.instHasColimitCompOfPreservesColimit Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_preservesColimitIso_hom
ι_preservesColimitIso_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.comp Limits.colimit Limits.instHasColimitCompOfPreservesColimit Limits.colimit.ι Iso.inv preservesColimitIso Functor.map	—	Limits.IsColimit.comp_coconePointUniqueUpToIso_inv Limits.instHasColimitCompOfPreservesColimit
ι_preservesColimitIso_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Limits.colimit Functor.comp Limits.instHasColimitCompOfPreservesColimit Limits.colimit.ι Iso.inv preservesColimitIso Functor.map	—	Limits.instHasColimitCompOfPreservesColimit Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_preservesColimitIso_inv

---

← Back to Index