Limits

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

Statistics

Metric	Count
Definitions coconesIso, coconesIsoComponentHom, coconesIsoComponentInv, conesIso, conesIsoComponentHom, conesIsoComponentInv, functorialityAdjunction, functorialityAdjunction', functorialityCounit, functorialityCounit', functorialityLeftAdjoint, functorialityRightAdjoint, functorialityUnit, functorialityUnit', createsColimitsOfIsEquivalence, createsLimitsOfIsEquivalence	16
Theorems colim_preservesColimits, functorialityCounit'_app_hom, functorialityCounit_app_hom, functorialityUnit'_app_hom, functorialityUnit_app_hom, hasColimit_comp_equivalence, hasColimit_of_comp_equivalence, hasColimitsOfShape_of_equivalence, hasLimit_comp_equivalence, hasLimit_of_comp_equivalence, hasLimitsOfShape_of_equivalence, has_colimits_of_equivalence, has_limits_of_equivalence, isEquivalencePreservesLimits, isEquivalence_preservesColimits, leftAdjoint_preservesColimits, lim_preservesLimits, rightAdjoint_preservesLimits, instPreservesColimitsOfShapeOfIsLeftAdjoint, instPreservesColimitsOfSizeOfIsLeftAdjoint, instPreservesLimitsOfShapeOfIsRightAdjoint, instPreservesLimitsOfSizeOfIsRightAdjoint, reflectsColimits_of_isEquivalence, reflectsLimits_of_isEquivalence	24
Total	40

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
coconesIso 📖	CompOp	—
coconesIsoComponentHom 📖	CompOp	—
coconesIsoComponentInv 📖	CompOp	—
conesIso 📖	CompOp	—
conesIsoComponentHom 📖	CompOp	—
conesIsoComponentInv 📖	CompOp	—
functorialityAdjunction 📖	CompOp	—
functorialityAdjunction' 📖	CompOp	—
functorialityCounit 📖	CompOp	1 math math: functorialityCounit_app_hom
functorialityCounit' 📖	CompOp	1 math math: functorialityCounit'_app_hom
functorialityLeftAdjoint 📖	CompOp	2 math math: functorialityUnit'_app_hom, functorialityCounit'_app_hom
functorialityRightAdjoint 📖	CompOp	2 math math: functorialityUnit_app_hom, functorialityCounit_app_hom
functorialityUnit 📖	CompOp	1 math math: functorialityUnit_app_hom
functorialityUnit' 📖	CompOp	1 math math: functorialityUnit'_app_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colim_preservesColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesColimits CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colim	—	leftAdjoint_preservesColimits
functorialityCounit'_app_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.comp CategoryTheory.Limits.Cones.functoriality functorialityLeftAdjoint CategoryTheory.Functor.id CategoryTheory.NatTrans.app functorialityCounit' counit CategoryTheory.Limits.Cone.pt	—	—
functorialityCounit_app_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category functorialityRightAdjoint CategoryTheory.Limits.Cocones.functoriality CategoryTheory.Functor.id CategoryTheory.NatTrans.app functorialityCounit counit CategoryTheory.Limits.Cocone.pt	—	—
functorialityUnit'_app_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.id functorialityLeftAdjoint CategoryTheory.Limits.Cones.functoriality CategoryTheory.NatTrans.app functorialityUnit' unit CategoryTheory.Limits.Cone.pt	—	—
functorialityUnit_app_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Limits.Cocones.functoriality functorialityRightAdjoint CategoryTheory.NatTrans.app functorialityUnit unit CategoryTheory.Limits.Cocone.pt	—	—
hasColimit_comp_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Functor.comp	—	CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape isEquivalence_preservesColimits
hasColimit_of_comp_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasColimit	—	CategoryTheory.Limits.hasColimit_iff_of_iso hasColimit_comp_equivalence CategoryTheory.Functor.isEquivalence_inv
hasColimitsOfShape_of_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape	—	hasColimit_of_comp_equivalence CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
hasLimit_comp_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Functor.comp	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape isEquivalencePreservesLimits
hasLimit_of_comp_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasLimit	—	CategoryTheory.Limits.hasLimit_iff_of_iso hasLimit_comp_equivalence CategoryTheory.Functor.isEquivalence_inv
hasLimitsOfShape_of_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape	—	hasLimit_of_comp_equivalence CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
has_colimits_of_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize	—	hasColimitsOfShape_of_equivalence CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
has_limits_of_equivalence 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize	—	hasLimitsOfShape_of_equivalence CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
isEquivalencePreservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize	—	rightAdjoint_preservesLimits
isEquivalence_preservesColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize	—	leftAdjoint_preservesColimits
leftAdjoint_preservesColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize	—	—
lim_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.lim	—	rightAdjoint_preservesLimits
rightAdjoint_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
createsColimitsOfIsEquivalence 📖	CompOp	—
createsLimitsOfIsEquivalence 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitsOfShapeOfIsLeftAdjoint 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape	—	CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Adjunction.leftAdjoint_preservesColimits
instPreservesColimitsOfSizeOfIsLeftAdjoint 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize	—	instPreservesColimitsOfShapeOfIsLeftAdjoint
instPreservesLimitsOfShapeOfIsRightAdjoint 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Adjunction.rightAdjoint_preservesLimits
instPreservesLimitsOfSizeOfIsRightAdjoint 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize	—	instPreservesLimitsOfShapeOfIsRightAdjoint
reflectsColimits_of_isEquivalence 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfSize	—	CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Adjunction.isEquivalence_preservesColimits isEquivalence_inv
reflectsLimits_of_isEquivalence 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfSize	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Adjunction.isEquivalencePreservesLimits isEquivalence_inv

---

← Back to Index