Structures · Category theory
CategoryTheory.Limits.PreservesFilteredColimitsOfSize
PreservesFilteredColimitsOfSize.{w', w} F means that F sends all colimit cocones over any
filtered diagram J ⥤ C to colimit cocones, where J : Type w with [Category.{w'} J].
- Shape
- One type argument · adds preserves_filtered_colimits
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.Under
- PartOrdEmb
How is a type an instance?
Loading the hierarchy index…
Assumed by47
- CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms
- CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink
- CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective
- CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ
- CategoryTheory.Limits.preservesFilteredColimitsOfSize_of_univLE
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms
- CategoryTheory.ObjectProperty.ind_inverseImage_le
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_injective
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective₂
- CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor
- CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor
- AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_smallEtaleTopology
- CategoryTheory.Limits.preservesSmallestFilteredColimits_of_preservesFilteredColimits
- AlgebraicGeometry.Scheme.instAbelianSheafEtaleSmallEtaleTopology
- CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app_assoc
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε
- CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso.congr_simp
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_eq_iff'
- CategoryTheory.Limits.comp_preservesFilteredColimits
- CategoryTheory.GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber
- AlgebraicGeometry.Scheme.instHasSheafifyAffineEtaleTopology
- CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints
- AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_affineEtaleTopology
- CategoryTheory.GrothendieckTopology.Point.instMonoidalSheafSheafFiber
- AlgebraicGeometry.Scheme.instAbelianSheafAffineEtaleTopology
- CategoryTheory.FinallySmall.preservesColimitsOfShape_of_isFiltered
- CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber'
- AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveAffineEtaleTopology
- CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app
- CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app
- CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget
- AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveEtaleSmallEtaleTopology
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms
- AlgebraicGeometry.Scheme.instHasSheafifyEtaleSmallEtaleTopology
- CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits
- CategoryTheory.GrothendieckTopology.Point.instMonoidalFunctorOppositePresheafFiber
- CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc
Ancestors0
No ancestors.