FiniteColimits

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/FiniteColimits.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_of_isColimit, hasDimensionLT_of_isColimit, iSup_range_eq_top_of_isColimit, instFiniteCoprod, instFiniteInitial, instFiniteSigmaObjOfFinite, range_eq_iSup_of_isColimit, range_eq_iSup_sigma_ι	8
Total	8

SSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_isColimit 📖	mathematical	Finite CategoryTheory.Functor.obj SSet largeCategory	CategoryTheory.Limits.Cocone.pt	—	finite_subcomplex_top_iff iSup_range_eq_top_of_isColimit finite_iSup_iff finite_range
hasDimensionLT_of_isColimit 📖	mathematical	HasDimensionLT CategoryTheory.Functor.obj SSet largeCategory	CategoryTheory.Limits.Cocone.pt	—	hasDimensionLT_subcomplex_top_iff iSup_range_eq_top_of_isColimit hasDimensionLT_iSup_iff instHasDimensionLTToSSetRange
iSup_range_eq_top_of_isColimit 📖	mathematical	—	iSup Subcomplex ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Subcomplex.range CategoryTheory.Functor.obj SSet largeCategory CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Subfunctor.ext Set.ext CategoryTheory.Subfunctor.iSup_obj CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.evaluation_preservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instFiniteCoprod 📖	mathematical	—	Finite CategoryTheory.Limits.coprod SSet largeCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits hasColimits Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair	—	finite_of_isColimit CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasColimits CategoryTheory.instFiniteDiscrete
instFiniteInitial 📖	mathematical	—	Finite CategoryTheory.Limits.initial SSet largeCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits hasColimits Finite.of_fintype Fintype.instPEmpty	—	finite_of_isColimit CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self Finite.of_fintype hasColimits CategoryTheory.instFiniteDiscrete
instFiniteSigmaObjOfFinite 📖	mathematical	Finite	CategoryTheory.Limits.sigmaObj SSet largeCategory	—	Finite.exists_equiv_fin CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self Finite.of_fintype finite_of_isColimit CategoryTheory.instFiniteDiscrete
range_eq_iSup_of_isColimit 📖	mathematical	—	Subcomplex.range CategoryTheory.Limits.Cocone.pt SSet largeCategory iSup Subcomplex ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Category.id_comp Subcomplex.range_comp Subcomplex.range_eq_top CategoryTheory.instEpiId iSup_range_eq_top_of_isColimit Subcomplex.image_iSup
range_eq_iSup_sigma_ι 📖	mathematical	—	Subcomplex.range CategoryTheory.Limits.sigmaObj SSet largeCategory iSup Subcomplex ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Sigma.ι	—	range_eq_iSup_of_isColimit le_antisymm le_trans le_refl le_iSup

---

← Back to Index