Limits

📁 Source: Mathlib/Algebra/Homology/ShortComplex/Limits.lean

Statistics

Metric	Count
Definitions colimitCocone, isColimitColimitCocone, isColimitOfIsColimitπ, isColimitπ₁MapCoconeColimitCocone, isColimitπ₂MapCoconeColimitCocone, isColimitπ₃MapCoconeColimitCocone, isLimitLimitCone, isLimitOfIsLimitπ, isLimitπ₁MapConeLimitCone, isLimitπ₂MapConeLimitCone, isLimitπ₃MapConeLimitCone, limitCone	12
Theorems hasColimit_of_hasColimitπ, hasColimitsOfShape, hasFiniteColimits, hasFiniteLimits, hasLimit_of_hasLimitπ, hasLimitsOfShape, instPreservesColimitsOfShapeπ₁, instPreservesColimitsOfShapeπ₂, instPreservesColimitsOfShapeπ₃, instPreservesColimitπ₁, instPreservesColimitπ₂, instPreservesColimitπ₃, instPreservesFiniteColimitsπ₁, instPreservesFiniteColimitsπ₂, instPreservesFiniteColimitsπ₃, instPreservesFiniteLimitsπ₁, instPreservesFiniteLimitsπ₂, instPreservesFiniteLimitsπ₃, instPreservesLimitsOfShapeπ₁, instPreservesLimitsOfShapeπ₂, instPreservesLimitsOfShapeπ₃, instPreservesLimitπ₁, instPreservesLimitπ₂, instPreservesLimitπ₃, preservesEpimorphisms_π₁, preservesEpimorphisms_π₂, preservesEpimorphisms_π₃, preservesMonomorphisms_π₁, preservesMonomorphisms_π₂, preservesMonomorphisms_π₃	30
Total	42

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
colimitCocone 📖	CompOp	—
isColimitColimitCocone 📖	CompOp	—
isColimitOfIsColimitπ 📖	CompOp	—
isColimitπ₁MapCoconeColimitCocone 📖	CompOp	—
isColimitπ₂MapCoconeColimitCocone 📖	CompOp	—
isColimitπ₃MapCoconeColimitCocone 📖	CompOp	—
isLimitLimitCone 📖	CompOp	—
isLimitOfIsLimitπ 📖	CompOp	—
isLimitπ₁MapConeLimitCone 📖	CompOp	—
isLimitπ₂MapConeLimitCone 📖	CompOp	—
isLimitπ₃MapConeLimitCone 📖	CompOp	—
limitCone 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit_of_hasColimitπ 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.ShortComplex instCategory	—	—
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.ShortComplex instCategory	—	hasColimit_of_hasColimitπ CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
hasFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits CategoryTheory.ShortComplex instCategory	—	hasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits CategoryTheory.ShortComplex instCategory	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
hasLimit_of_hasLimitπ 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.ShortComplex instCategory	—	—
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.ShortComplex instCategory	—	hasLimit_of_hasLimitπ CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instPreservesColimitsOfShapeπ₁ 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.ShortComplex instCategory π₁	—	instPreservesColimitπ₁ CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instPreservesColimitsOfShapeπ₂ 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.ShortComplex instCategory π₂	—	instPreservesColimitπ₂ CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeπ₁
instPreservesColimitsOfShapeπ₃ 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.ShortComplex instCategory π₃	—	instPreservesColimitπ₃ CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeπ₁ instPreservesColimitsOfShapeπ₂
instPreservesColimitπ₁ 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.ShortComplex instCategory π₁	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
instPreservesColimitπ₂ 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.ShortComplex instCategory π₂	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
instPreservesColimitπ₃ 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.ShortComplex instCategory π₃	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
instPreservesFiniteColimitsπ₁ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex instCategory π₁	—	instPreservesColimitsOfShapeπ₁ CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
instPreservesFiniteColimitsπ₂ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex instCategory π₂	—	instPreservesColimitsOfShapeπ₂ CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
instPreservesFiniteColimitsπ₃ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex instCategory π₃	—	instPreservesColimitsOfShapeπ₃ CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
instPreservesFiniteLimitsπ₁ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex instCategory π₁	—	instPreservesLimitsOfShapeπ₁ CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
instPreservesFiniteLimitsπ₂ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex instCategory π₂	—	instPreservesLimitsOfShapeπ₂ CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
instPreservesFiniteLimitsπ₃ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex instCategory π₃	—	instPreservesLimitsOfShapeπ₃ CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
instPreservesLimitsOfShapeπ₁ 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.ShortComplex instCategory π₁	—	instPreservesLimitπ₁ CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instPreservesLimitsOfShapeπ₂ 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.ShortComplex instCategory π₂	—	instPreservesLimitπ₂ CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape hasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit instPreservesLimitsOfShapeπ₁
instPreservesLimitsOfShapeπ₃ 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.ShortComplex instCategory π₃	—	instPreservesLimitπ₃ CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape hasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit instPreservesLimitsOfShapeπ₁ instPreservesLimitsOfShapeπ₂
instPreservesLimitπ₁ 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.ShortComplex instCategory π₁	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
instPreservesLimitπ₂ 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.ShortComplex instCategory π₂	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
instPreservesLimitπ₃ 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.ShortComplex instCategory π₃	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
preservesEpimorphisms_π₁ 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ShortComplex instCategory π₁	—	CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape instPreservesColimitsOfShapeπ₁
preservesEpimorphisms_π₂ 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ShortComplex instCategory π₂	—	CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape instPreservesColimitsOfShapeπ₂
preservesEpimorphisms_π₃ 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ShortComplex instCategory π₃	—	CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape instPreservesColimitsOfShapeπ₃
preservesMonomorphisms_π₁ 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.ShortComplex instCategory π₁	—	CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape instPreservesLimitsOfShapeπ₁
preservesMonomorphisms_π₂ 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.ShortComplex instCategory π₂	—	CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape instPreservesLimitsOfShapeπ₂
preservesMonomorphisms_π₃ 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.ShortComplex instCategory π₃	—	CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape instPreservesLimitsOfShapeπ₃

---

← Back to Index