Structures · Category theory
CategoryTheory.Limits.ReflectsFiniteProducts
A functor F preserves finite products if it reflects limits of shape Discrete J for finite J.
We require this for J = Fin n in the definition,
then generalize to J : Type u in the instance.
- Shape
- One type argument · adds reflects
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp
- CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite
- CategoryTheory.Limits.comp_reflectsFiniteProducts
- CategoryTheory.Limits.ReflectsFiniteProducts.reflects
- CategoryTheory.Limits.reflectsFiniteCoproducts_leftOp
- Condensed.ofSheafForgetStonean
- CategoryTheory.Limits.reflectsFiniteCoproducts_op
- CategoryTheory.Limits.reflectsFiniteCoproducts_rightOp
- CategoryTheory.Limits.reflectsFiniteCoproducts_unop
- CategoryTheory.Limits.preservesFiniteProducts_of_reflects_of_preserves
Ancestors0
No ancestors.