AB

📁 Source: Mathlib/Condensed/AB.lean

Statistics

Metric	Count
Definitions	0
Theorems hasExactColimitsOfShape, hasExactLimitsOfShape, instAB4CondensedMod, instAB4StarCondensedMod, instAB5CondensedMod, instHasLimitsOfSizeModuleCat	6
Total	6

Condensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasExactColimitsOfShape 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite Stonean CategoryTheory.Category.opposite CompHausLike.category ExtremallyDisconnected TopCat.carrier TopCat.str CompHaus CategoryTheory.Functor.op Stonean.toCompHaus CategoryTheory.instCategoryStructuredArrow	CategoryTheory.HasExactColimitsOfShape Condensed instCategoryCondensed instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier Stonean.instPreregular Stonean.instProjective CategoryTheory.HasExactColimitsOfShape.domain_of_functor instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology CategoryTheory.Sheaf.instHasColimitsOfShape CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor instHasFiniteLimitsCondensed CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence
hasExactLimitsOfShape 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite Stonean CategoryTheory.Category.opposite CompHausLike.category ExtremallyDisconnected TopCat.carrier TopCat.str CompHaus CategoryTheory.Functor.op Stonean.toCompHaus CategoryTheory.instCategoryStructuredArrow	CategoryTheory.HasExactLimitsOfShape Condensed instCategoryCondensed instHasLimitsOfShapeCondensed	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier Stonean.instPreregular Stonean.instProjective CategoryTheory.HasExactLimitsOfShape.domain_of_functor instHasLimitsOfShapeCondensed CategoryTheory.Sheaf.instHasLimitsOfShape CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence
instAB4CondensedMod 📖	mathematical	—	CategoryTheory.AB4 CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology CategoryTheory.Discrete CategoryTheory.discreteCategory ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.sheafToPresheaf_isRightAdjoint CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.types CategoryTheory.forget ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.Functor.comp Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover 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 CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier	—	CategoryTheory.AB4.of_AB5 CategoryTheory.Abelian.hasFiniteBiproducts instHasFiniteLimitsCondensed CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits ModuleCat.hasLimits' CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize instHasColimitsCondensedMod instAB5CondensedMod
instAB4StarCondensedMod 📖	mathematical	—	CategoryTheory.AB4Star CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory instHasLimitsOfShapeCondensed CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasProductsOfShape_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits'	—	instHasLimitsOfShapeCondensed CategoryTheory.Limits.hasProductsOfShape_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits' hasExactLimitsOfShape instHasLimitsOfSizeModuleCat CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular 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 Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier CategoryTheory.AB4StarOfSize.ofShape instAB4StarModuleCat ModuleCat.instHasFiniteColimits
instAB5CondensedMod 📖	mathematical	—	CategoryTheory.AB5 CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize instHasColimitsCondensedMod	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize instHasColimitsCondensedMod hasExactColimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits instHasLimitsOfSizeModuleCat CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular 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 Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier CategoryTheory.AB5OfSize.ofShape ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize instAB5ModuleCat CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits ModuleCat.hasLimits'
instHasLimitsOfSizeModuleCat 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Limits.hasLimitsOfSizeShrink ModuleCat.hasLimits'

---

← Back to Index