Structures · Category theory
CategoryTheory.Limits.HasFiniteLimits
A category has all finite limits if every functor J ⥤ C with a FinCategory J
instance and J : Type has a limit.
This is often called 'finitely complete'.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances25
- CategoryTheory.Functor
- CategoryTheory.Over
- HomologicalComplex
- Action
- AlgebraicGeometry.Scheme
- CategoryTheory.ShrinkHoms
- SheafOfModules
- CategoryTheory.Ind
- CategoryTheory.Comma
- PresheafOfModules
- CategoryTheory.Sheaf
- CategoryTheory.StructuredArrow
- CategoryTheory.Arrow
- CategoryTheory.ShortComplex
- AlgebraicGeometry.Scheme.ProEt
- AlgebraicGeometry.Scheme.Etale
- FGModuleCat
- CategoryTheory.Subobject
- FintypeCat
- CochainComplex.Plus
- CategoryTheory.MorphismProperty.Over
- CategoryTheory.AsSmall
- CategoryTheory.MonoOver
- Condensed
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by80
- CategoryTheory.flat_of_preservesFiniteLimits
- CategoryTheory.StructuredArrow.projectSubobject
- CategoryTheory.IsCofiltered.of_hasFiniteLimits
- CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete
- CategoryTheory.hasExactColimitsOfShape_of_final
- CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite
- CategoryTheory.HasExactColimitsOfShape.domain_of_functor
- CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize
- CategoryTheory.Limits.preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits
- CategoryTheory.instCreatesFiniteLimitsIndFunctorOppositeTypeInclusionOfHasFiniteLimits
- CategoryTheory.flat_iff_lan_flat
- instHasFiniteLimitsCondensed
- CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits
- HomologicalComplex.hasExactColimitsOfShape
- CategoryTheory.StructuredArrow.projectSubobject.congr_simp
- CategoryTheory.Sheaf.ab5ofSize
- CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₁
- HomologicalComplex.ab5OfSize
- CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits
- CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover
- CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits
- CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits
- CategoryTheory.preservesFiniteLimits_iff_flat
- CategoryTheory.CountableAB4.of_countableAB5
- CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms
- CategoryTheory.AsSmall.hasFiniteLimits
- CategoryTheory.preservesFiniteLimits_liftToFinset
- CategoryTheory.StructuredArrow.projectSubobject_mk
- CategoryTheory.Limits.hasFiniteColimits_opposite
- CochainComplex.Plus.instHasFiniteLimits
- Condensed.hasExactColimitsOfShape
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful
- CategoryTheory.Subobject.hasFiniteLimits
- CategoryTheory.StructuredArrow.subobjectEquiv
- CategoryTheory.ShrinkHoms.hasFiniteLimits
- HomologicalComplex.instPreservesFiniteLimitsEvalOfHasFiniteLimits
- HomologicalComplex.instMonoFOfHasFiniteLimits
- CategoryTheory.instPreservesFiniteLimitsHomologicalComplexMapHomologicalComplexOfHasFiniteLimits
- CategoryTheory.Limits.HasFiniteLimits.out
- CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits
- CategoryTheory.Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits
- Action.instHasFiniteLimits
- CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits
- CategoryTheory.GrothendieckTopology.preservesFiniteLimits_sheafification
- HomotopicalAlgebra.ModelCategory.mk'
- CategoryTheory.Limits.instHasFiniteLimitsFunctor
- CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize
- CategoryTheory.Adjunction.hasExactColimitsOfShape
- CategoryTheory.Comma.hasFiniteLimits
- CategoryTheory.GrothendieckTopology.preserveFiniteLimits_plusFunctor
Ancestors0
No ancestors.