Structures · Category theory
CategoryTheory.Limits.PreservesFiniteProducts
A functor F preserves finite products if it preserves all from 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 preserves
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- CategoryTheory.Functor
- CategoryTheory.Under
- SSet
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by94
- LightCondensed.isoFinYonedaComponents
- Condensed.isoFinYonedaComponents
- CompHausLike.LocallyConstant.counitApp
- CompHausLike.LocallyConstant.counitAppApp
- CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts
- LightCondensed.isoFinYoneda
- Condensed.isoFinYoneda
- CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory
- CompHausLike.LocallyConstant.incl_of_counitAppApp
- CompHausLike.LocallyConstant.presheaf_ext
- CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts
- CategoryTheory.coherentTopology.isLocallySurjective_iff
- LightCondensed.isoLocallyConstantOfIsColimit
- CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts
- Condensed.epi_iff_locallySurjective_on_compHaus
- CategoryTheory.Functor.Monoidal.tensorObjComp
- Condensed.isoLocallyConstantOfIsColimit
- CategoryTheory.Functor.Braided.ofChosenFiniteProducts
- Condensed.epi_iff_surjective_on_stonean
- LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite
- CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff
- CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff
- LightCondensed.isoFinYonedaComponents_hom_apply
- Condensed.isoFinYonedaComponents_inv_comp
- CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types
- LightCondensed.ofSheafForgetLightProfinite
- LightCondensed.isoFinYonedaComponents_inv_comp
- CategoryTheory.extensiveTopology.isLocallySurjective_iff
- Condensed.isoFinYonedaComponents_hom_apply
- CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesFiniteProducts
- CategoryTheory.IsSifted.of_colim_preservesFiniteProducts
- CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types
- LightCondensed.ofSheafLightProfinite
- CompHausLike.isIsoSigmaComparison
- CondensedMod.ofSheafCompHaus
- Condensed.ofSheafStonean
- CategoryTheory.Limits.preservesFiniteCoproducts_unop
- CategoryTheory.Limits.preservesFiniteCoproducts_op
- LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteObjFinite
- Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite
- CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory
- LightCondensed.isoFinYonedaComponents.congr_simp
- CategoryTheory.Limits.preservesFiniteCoproducts_rightOp
- CompHausLike.LocallyConstant.counitAppApp.congr_simp
- Condensed.isoFinYoneda_inv_app_hom_apply
- CompHausLike.LocallyConstant.counitApp_app
- instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf
- LightCondensed.isoFinYoneda_hom_app_hom_apply
- CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
- CategoryTheory.Functor.EssImageSubcategory.tensor_obj
Ancestors0
No ancestors.