FiniteLimits

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

Statistics

Metric	Count
Definitions HasFiniteColimits, HasFiniteLimits, HasFiniteWidePullbacks, HasFiniteWidePushouts, fintypeHom, fintypeObj, fintypeHom, fintypeObj, finCategoryWidePullback, finCategoryWidePushout, fintypeWalkingPair, fintypeWalkingParallelPair, instCategoryULiftHomULiftOfSmallCategory, instFinCategoryWalkingParallelPair, instFintypeWalkingParallelPairHom	15
Theorems out, out, out, out, hasColimitsOfShape_of_hasFiniteColimits, hasColimitsOfShape_widePushoutShape, hasFiniteColimits_of_hasColimits, hasFiniteColimits_of_hasColimitsOfSize, hasFiniteColimits_of_hasColimitsOfSize₀, hasFiniteColimits_of_hasFiniteColimits_of_size, hasFiniteLimits_of_hasFiniteLimits_of_size, hasFiniteLimits_of_hasLimits, hasFiniteLimits_of_hasLimitsOfSize, hasFiniteLimits_of_hasLimitsOfSize₀, hasFiniteWidePullbacks_of_hasFiniteLimits, hasFiniteWidePushouts_of_has_finite_limits, hasLimitsOfShape_of_hasFiniteLimits, hasLimitsOfShape_widePullbackShape	18
Total	33

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasFiniteColimits 📖	CompData	23 math math: FintypeCat.hasFiniteColimits, hasFiniteColimits_of_hasColimitsOfSize, PresheafOfModules.Finite.hasFiniteColimits, HomotopicalAlgebra.ModelCategory.cm1b, hasFiniteColimits_of_hasInitial_and_pushouts, ModuleCat.instHasFiniteColimits, instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology, hasFiniteColimits_of_hasCountableColimits, CategoryTheory.Abelian.hasFiniteColimits, hasFiniteColimits_opposite, CategoryTheory.Sheaf.instHasFiniteColimits, FGModuleCat.instHasFiniteColimits, hasFiniteColimits_of_hasColimits, hasFiniteColimits_of_hasColimitsOfSize₀, CategoryTheory.ShortComplex.hasFiniteColimits, hasFiniteColimits_of_hasColimits_of_createsFiniteColimits, hasFiniteColimits_of_hasFiniteColimits_of_size, CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot, hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts, Action.instHasFiniteColimits, CategoryTheory.Over.instHasFiniteColimits, HomologicalComplex.instHasFiniteColimits, instHasFiniteColimitsFunctor
HasFiniteLimits 📖	CompData	34 math math: PresheafOfModules.hasFiniteLimits, hasFiniteLimits_of_hasLimits, HomotopicalAlgebra.ModelCategory.cm1a, CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop, hasFiniteLimits_of_hasLimitsOfSize₀, CategoryTheory.AsSmall.hasFiniteLimits, CategoryTheory.PreGaloisCategory.instHasFiniteLimits, instHasFiniteLimitsFunctor, CategoryTheory.ShrinkHoms.hasFiniteLimits, FintypeCat.hasFiniteLimits, AlgebraicGeometry.instHasFiniteLimitsScheme, CategoryTheory.Abelian.hasFiniteLimits, CategoryTheory.Regular.toHasFiniteLimits, CategoryTheory.MonoOver.hasFiniteLimits, CategoryTheory.Sheaf.instHasFiniteLimits, CategoryTheory.Over.hasFiniteLimits, hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits, hasFiniteLimits_of_hasTerminal_and_pullbacks, hasFiniteLimits_of_hasFiniteLimits_of_size, hasFiniteLimits_of_hasEqualizers_and_finite_products, CategoryTheory.ShortComplex.hasFiniteLimits, instHasFiniteLimitsLightCondSet, instHasFiniteLimitsLightCondMod, FGModuleCat.instHasFiniteLimits, SheafOfModules.Finite.hasFiniteLimits, instHasFiniteLimitsCondensed, FDRep.instHasFiniteLimits, hasFiniteLimits_opposite, hasFiniteLimits_of_hasLimitsOfSize, CategoryTheory.instHasFiniteLimitsInd, Action.instHasFiniteLimits, HomologicalComplex.instHasFiniteLimits, CategoryTheory.Subobject.hasFiniteLimits, hasFiniteLimits_of_hasCountableLimits
HasFiniteWidePullbacks 📖	CompData	1 math math: hasFiniteWidePullbacks_of_hasFiniteLimits
HasFiniteWidePushouts 📖	CompData	1 math math: hasFiniteWidePushouts_of_has_finite_limits
finCategoryWidePullback 📖	CompOp	1 math math: CategoryTheory.StructuredArrow.projectSubobject_mk
finCategoryWidePushout 📖	CompOp	1 math math: CategoryTheory.CostructuredArrow.projectQuotient_mk
fintypeWalkingPair 📖	CompOp	129 math math: TopCat.isInducing_pullback_to_prod, CategoryTheory.StructuredArrow.projectSubobject_mk, TopCat.pullbackIsoProdSubtype_hom_fst, CategoryTheory.NonPreadditiveAbelian.diag_σ, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions, Opens.pretopology_toGrothendieck, CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, TopCat.snd_isOpenEmbedding_of_left, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder, CompHausLike.HasExplicitPullbacksOfInclusions.hasProp, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, TopCat.pullback_topology, CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum, HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder, HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder, CommRingCat.Under.preservesFiniteLimits_of_flat, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, TopCat.fst_iso_of_right_embedding_range_subset, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, CategoryTheory.NonPreadditiveAbelian.σ_comp, CategoryTheory.Functor.EssImageSubcategory.tensor_obj, CategoryTheory.Dial.comp_le_lemma, HomotopicalAlgebra.PathObject.exists_very_good, TopCat.range_pullback_map, HomotopicalAlgebra.PathObject.ofFactorizationData_p, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, SSet.instFiniteCoprod, Opens.pretopology_ofGrothendieck, CommRingCat.HomTopology.isEmbedding_pushout, HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject, CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', CommRingCat.Under.instPreservesFiniteProductsUnderPushout, HomotopicalAlgebra.Cylinder.ofFactorizationData_i, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, TopCat.fst_isEmbedding_of_right, TopCat.isOpenEmbedding_of_pullback, CategoryTheory.NonPreadditiveAbelian.epi_r, CommRingCat.inr_injective_of_flat, CategoryTheory.NonPreadditiveAbelian.isIso_r, HomotopicalAlgebra.PathObject.instIsGoodTrans, TopCat.pullbackIsoProdSubtype_inv_snd_apply, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject, HomotopicalAlgebra.Cylinder.exists_very_good, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, TopCat.pullbackIsoProdSubtype_inv_fst, CategoryTheory.Dial.Hom.le, CompleteLattice.pushout_eq_sup, HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData, CategoryTheory.NonPreadditiveAbelian.mono_Δ, TopCat.pullbackIsoProdSubtype_hom_snd, TopCat.snd_iso_of_left_embedding_range_subset, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, CategoryTheory.NonPreadditiveAbelian.lift_sub_lift, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, CategoryTheory.Regular.instHasCoequalizerFstSnd, HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject, TopCat.range_pullback_to_prod, TopCat.pullback_fst_image_snd_preimage, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, CompleteLattice.pullback_eq_inf, CategoryTheory.FinitaryPreExtensive.hasPullbacksOfInclusions, AlgebraicGeometry.isPullback_Spec_map_pushout, TopCat.pullbackIsoProdSubtype_inv_fst_apply, AlgebraicGeometry.instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift, CommRingCat.inl_injective_of_flat, CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf, CategoryTheory.NonPreadditiveAbelian.lift_map_assoc, CommRingCat.tensorProdIsoPushout_app, TopCat.isEmbedding_pullback_to_prod, CategoryTheory.Regular.frobeniusMorphism_isPullback, TopCat.pullbackIsoProdSubtype_hom_apply, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, CategoryTheory.FinitaryExtensive.hasPullbacksOfInclusions, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData, TopCat.fst_isOpenEmbedding_of_right, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, CategoryTheory.NonPreadditiveAbelian.mono_r, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_id, TopCat.pullback_map_isOpenEmbedding, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, AlgebraicGeometry.isPullback_SpecMap_pushout, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, AlgebraicGeometry.isIso_pushoutSection_iff, CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor, CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, TopCat.pullback_map_isEmbedding, AlgebraicGeometry.IsImmersion.instLiftSchemeId, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, CategoryTheory.NonPreadditiveAbelian.diag_σ_assoc, CategoryTheory.NonPreadditiveAbelian.sub_def, Opens.toPretopology_grothendieckTopology, AlgebraicGeometry.Scheme.instIsClosedImmersionLiftIdOfIsSeparated, HomotopicalAlgebra.Cylinder.instIsGoodTrans, CategoryTheory.NonPreadditiveAbelian.lift_map, CategoryTheory.NonPreadditiveAbelian.lift_σ, CategoryTheory.NonPreadditiveAbelian.lift_σ_assoc, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, TopCat.pullback_snd_range, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', TopCat.snd_isEmbedding_of_left, CategoryTheory.Functor.EssImageSubcategory.lift_def, CategoryTheory.hoFunctor.isIso_prodComparison, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, SSet.instFinitePullback, TopCat.pullback_fst_range, CategoryTheory.CostructuredArrow.projectQuotient_mk, TopCat.pullback_snd_image_fst_preimage, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, RingHom.IsStableUnderBaseChange.pushout_inl, TopCat.isEmbedding_of_pullback, CategoryTheory.Regular.instMonoDesc, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
fintypeWalkingParallelPair 📖	CompOp	—
instCategoryULiftHomULiftOfSmallCategory 📖	CompOp	—
instFinCategoryWalkingParallelPair 📖	CompOp	7 math math: AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated, AlgebraicGeometry.IsImmersion.instιScheme, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, FGModuleCat.instIsIsoCoimageImageComparison
instFintypeWalkingParallelPairHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimitsOfShape_of_hasFiniteColimits 📖	mathematical	—	HasColimitsOfShape	—	hasColimitsOfShape_of_equivalence HasFiniteColimits.out
hasColimitsOfShape_widePushoutShape 📖	mathematical	—	HasColimitsOfShape WidePushoutShape WidePushoutShape.category	—	HasFiniteWidePushouts.out
hasFiniteColimits_of_hasColimits 📖	mathematical	—	HasFiniteColimits	—	hasFiniteColimits_of_hasColimitsOfSize
hasFiniteColimits_of_hasColimitsOfSize 📖	mathematical	—	HasFiniteColimits	—	hasColimitsOfShape_of_equivalence hasColimitsOfShapeOfHasColimitsOfSize hasColimitsOfSizeShrink
hasFiniteColimits_of_hasColimitsOfSize₀ 📖	mathematical	—	HasFiniteColimits	—	hasFiniteColimits_of_hasColimitsOfSize
hasFiniteColimits_of_hasFiniteColimits_of_size 📖	mathematical	HasColimitsOfShape	HasFiniteColimits	—	hasColimitsOfShape_of_equivalence
hasFiniteLimits_of_hasFiniteLimits_of_size 📖	mathematical	HasLimitsOfShape	HasFiniteLimits	—	hasLimitsOfShape_of_equivalence
hasFiniteLimits_of_hasLimits 📖	mathematical	—	HasFiniteLimits	—	hasFiniteLimits_of_hasLimitsOfSize
hasFiniteLimits_of_hasLimitsOfSize 📖	mathematical	—	HasFiniteLimits	—	hasLimitsOfShape_of_equivalence hasLimitsOfShapeOfHasLimits hasLimitsOfSizeShrink
hasFiniteLimits_of_hasLimitsOfSize₀ 📖	mathematical	—	HasFiniteLimits	—	hasFiniteLimits_of_hasLimitsOfSize
hasFiniteWidePullbacks_of_hasFiniteLimits 📖	mathematical	—	HasFiniteWidePullbacks	—	nonempty_fintype HasFiniteLimits.out
hasFiniteWidePushouts_of_has_finite_limits 📖	mathematical	—	HasFiniteWidePushouts	—	nonempty_fintype HasFiniteColimits.out
hasLimitsOfShape_of_hasFiniteLimits 📖	mathematical	—	HasLimitsOfShape	—	hasLimitsOfShape_of_equivalence HasFiniteLimits.out
hasLimitsOfShape_widePullbackShape 📖	mathematical	—	HasLimitsOfShape WidePullbackShape WidePullbackShape.category	—	HasFiniteWidePullbacks.out

CategoryTheory.Limits.HasFiniteColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape	—	—

CategoryTheory.Limits.HasFiniteLimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape	—	—

CategoryTheory.Limits.HasFiniteWidePullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category	—	—

CategoryTheory.Limits.HasFiniteWidePushouts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WidePushoutShape.category	—	—

CategoryTheory.Limits.WidePullbackShape

Definitions

Name	Category	Theorems
fintypeHom 📖	CompOp	—
fintypeObj 📖	CompOp	—

CategoryTheory.Limits.WidePushoutShape

Definitions

Name	Category	Theorems
fintypeHom 📖	CompOp	—
fintypeObj 📖	CompOp	—

---

← Back to Index