Structures · Category theory
CategoryTheory.Limits.HasFiniteProducts
A category has finite products if there exists a limit for every diagram
with shape Discrete J, where we have [Finite J].
We require this condition only for J = Fin n in the definition, then deduce a version for any
J : Type* as a corollary of this definition.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances8
- CategoryTheory.Functor
- Action
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.MorphismProperty.Localization
- CategoryTheory.Sheaf
- CategoryTheory.MorphismProperty.Localization'
- CategoryTheory.InjectiveObject
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by190
- CategoryTheory.Dial.src
- CategoryTheory.Dial.tgt
- CategoryTheory.Dial.Hom.f
- CategoryTheory.Dial.tensorObjImpl
- CategoryTheory.Dial.Hom.F
- CategoryTheory.Dial.tensorUnitImpl
- CategoryTheory.Dial.rel
- CategoryTheory.Dial.hom_ext
- CategoryTheory.Limits.FormalCoproduct.cech
- CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj
- CategoryTheory.Dial.braiding
- CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp
- CategoryTheory.Dial.braiding_hom_F
- CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology
- CategoryTheory.Dial.rightUnitorImpl
- CategoryTheory.Dial.associatorImpl
- CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal
- CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve
- CategoryTheory.Dial.associator_hom_F
- CategoryTheory.Dial.whiskerRight_F
- CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi
- CategoryTheory.Dial.leftUnitorImpl
- CategoryTheory.Dial.whiskerLeft_F
- CategoryTheory.Dial.isoMk
- CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone
- CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset
- CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve
- CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone
- CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts
- CategoryTheory.Limits.FormalCoproduct.cechFunctor
- CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi
- CategoryTheory.Dial.rightUnitor_hom_F
- CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π
- CategoryTheory.Dial.tensorHomImpl
- CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels
- CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products
- CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel
- CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered
- CategoryTheory.Dial.leftUnitor_hom_F
- CategoryTheory.Dial.Hom.le
- CategoryTheory.Functor.hasFiniteProducts_of_additive_of_essSurj
- CategoryTheory.Dial.associator_inv_F
- CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi
- CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels
- CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone
- CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
- CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π
- CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimIso
- CategoryTheory.preservesFinOfPreservesBinaryAndTerminal
- CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum
Ancestors0
No ancestors.