Structures · Category theory
CategoryTheory.Limits.PreservesLimitsOfSize
PreservesLimitsOfSize.{v u} F means that F sends all limit cones over any
diagram J ⥤ C to limit cones, where J : Type u with [Category.{v} J].
- Shape
- One type argument · adds preservesLimitsOfShape
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances23
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- Action
- AddCommGrpCat
- TopCat
- Rep
- CommGrpCat
- GrpCat
- AddGrpCat
- SheafOfModules
- CommRingCat
- PresheafOfModules
- CategoryTheory.Under
- AlgCat
- CommMonCat
- AddCommMonCat
- MonCat
- AddMonCat
- RingCat
- CommSemiRingCat
- SemiRingCat
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- TopCat.Sheaf.eq_of_locally_eq'
- TopCat.Sheaf.existsUnique_gluing
- TopCat.Sheaf.eq_of_locally_eq
- TopCat.Presheaf.isSheaf_iff_isSheaf_comp'
- CategoryTheory.Limits.preservesLimitsOfSize_shrink
- CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp
- TopCat.Sheaf.eq_app_of_locally_eq
- TopCat.Sheaf.existsUnique_gluing'
- CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits
- TopCat.Presheaf.IsSheaf.isSheafUniqueGluing
- CategoryTheory.Limits.preservesLimits_of_natIso
- TopCat.Sheaf.eq_of_locally_eq₂
- CategoryTheory.GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift
- CategoryTheory.Limits.preservesLimitsOfSize_of_univLE
- CategoryTheory.Presheaf.isSheaf_comp_of_isSheaf
- CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms
- CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits
- CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize
- CategoryTheory.StructuredArrow.createsLimitsOfSize
- CategoryTheory.Limits.preservesColimitsOfSize_of_unop
- CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction
- CategoryTheory.Limits.PreservesLimits.preservesCofilteredLimits
- CategoryTheory.Limits.preservesColimitsOfSize_of_op
- CategoryTheory.Limits.preservesColimitsOfSize_of_rightOp
- TopCat.Sheaf.eq_of_locally_eq_iff
- CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction
- TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing
- CategoryTheory.Comonad.forgetCreatesLimits
- CategoryTheory.Limits.preservesColimitsOfSize_leftOp
- CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits
- CategoryTheory.Limits.comp_preservesLimits
- CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
- CategoryTheory.Comma.hasLimitsOfSize
- CategoryTheory.Limits.preservesColimitsOfSize_rightOp
- CategoryTheory.GrothendieckTopology.instPreservesSheafification
- CategoryTheory.StructuredArrow.hasLimitsOfSize
- CategoryTheory.comonadicCreatesLimitsOfPreservesLimits
- CategoryTheory.Limits.preservesColimitsOfSize_op
- CategoryTheory.whiskeringRightPreservesLimits
- Action.Functor.preservesLimitsOfSize_of_preserves
- CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves
- CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv
- CategoryTheory.Limits.preservesColimitsOfSize_of_leftOp
- CategoryTheory.Limits.preservesColimitsOfSize_unop
- CategoryTheory.Limits.PreservesLimitsOfSize.overPost
- CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition
Ancestors0
No ancestors.