Limits

📁 Source: Mathlib/Condensed/Limits.lean

Statistics

Metric	Count
Definitions	0
Theorems instHasColimitsCondensedMod, instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology, instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology, instHasFiniteLimitsCondensed, instHasLimitsCondensedMod, instHasLimitsCondensedSet, instHasLimitsOfShapeCondensed, instHasLimitsOfSizeCondensedMod, instHasLimitsOfSizeCondensedSet	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimitsCondensedMod 📖	mathematical	—	CategoryTheory.Limits.HasColimits CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Sheaf.instHasColimitsOfSize CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize
instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape Condensed instCategoryCondensed	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.instHasColimitsOfShape
instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits Condensed instCategoryCondensed	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.instHasFiniteColimits
instHasFiniteLimitsCondensed 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits Condensed instCategoryCondensed	—	CategoryTheory.Sheaf.instHasFiniteLimits
instHasLimitsCondensedMod 📖	mathematical	—	CategoryTheory.Limits.HasLimits CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Sheaf.hasLimitsOfSize ModuleCat.hasLimits'
instHasLimitsCondensedSet 📖	mathematical	—	CategoryTheory.Limits.HasLimits CondensedSet instCategoryCondensed CategoryTheory.types	—	CategoryTheory.Sheaf.hasLimitsOfSize CategoryTheory.Limits.Types.hasLimitsOfSize UnivLE.self
instHasLimitsOfShapeCondensed 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape Condensed instCategoryCondensed	—	CategoryTheory.Sheaf.instHasLimitsOfShape
instHasLimitsOfSizeCondensedMod 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Limits.hasLimitsOfSizeShrink instHasLimitsCondensedMod
instHasLimitsOfSizeCondensedSet 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CondensedSet instCategoryCondensed CategoryTheory.types	—	CategoryTheory.Limits.hasLimitsOfSizeShrink instHasLimitsCondensedSet

---

← Back to Index