PreservesLimits

📁 Source: Mathlib/CategoryTheory/Sites/PreservesLimits.lean

Statistics

Metric	Count
Definitions PreservesLimits	1
Theorems instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf, instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf, instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1, instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf, instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf, instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf, instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf, instPreservesLimitsOfShapeSheafTypeUliftYoneda, instPreservesLimitsOfShapeSheafTypeYoneda	9
Total	10

CategoryTheory.Limits

Definitions

Name	Category	Theorems
PreservesLimits 📖	MathDef	57 math math: ModuleCat.forget_preservesLimits, preservesLimits_of_leftOp, Profinite.forget_preservesLimits, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, AddGrpCat.forget_preservesLimits, CommGrpCat.forget_preservesLimits, RingCat.forget₂AddCommGroup_preservesLimits, AddCommGrpCat.forget_preservesLimits, preservesLimits_unop, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, AlgebraicGeometry.AffineScheme.forgetToScheme_preservesLimits, CommGrpCat.forget₂Group_preservesLimits, evaluationPreservesLimits, AlgebraicGeometry.AffineScheme.Γ_preservesLimits, CategoryTheory.instPreservesLimitsIndYoneda, ModuleCat.forget₂AddCommGroup_preservesLimits, AddCommMonCat.forget_preservesLimits, AlgCat.forget_preservesLimits, CategoryTheory.preservesLimits_preadditiveCoyoneda_obj, GrpCat.forget₂Mon_preservesLimits, AddCommMonCat.forget₂Mon_preservesLimits, CommSemiRingCat.forget₂SemiRing_preservesLimits, CommSemiRingCat.forget_preservesLimits, GrpCat.forget_preservesLimits, Action.preservesLimits_forget, CommRingCat.forget₂CommSemiRing_preservesLimits, Stonean.forget.preservesLimits, AddCommGrpCat.forget₂AddGroup_preservesLimits, CategoryTheory.preservesLimits_preadditiveYoneda_obj, CategoryTheory.preservesLimits_preadditiveYonedaObj, CommRingCat.forget₂Ring_preservesLimits, AddMonCat.forget_preservesLimits, preservesLimits_op, CommMonCat.forget_preservesLimits, AlgCat.forget₂Module_preservesLimits, RingCat.forget₂SemiRing_preservesLimits, SemiRingCat.forget₂AddCommMon_preservesLimits, SemiRingCat.forget_preservesLimits, CategoryTheory.GrothendieckTopology.preservesLimits_diagramFunctor, TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, CommMonCat.forget₂Mon_preservesLimits, AlgCat.forget₂Ring_preservesLimits, RingCat.forget_preservesLimits, TopCat.forget_preservesLimits, preservesLimits_of_rightOp, preservesLimits_of_unop, MonCat.forget_preservesLimits, CategoryTheory.Cat.instPreservesLimitsObjects, CommRingCat.forget_preservesLimits, CategoryTheory.preservesLimits_preadditiveCoyonedaObj, CategoryTheory.Adjunction.lim_preservesLimits, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, preservesLimits_of_op, preservesLimits_leftOp, SemiRingCat.forget₂Mon_preservesLimits, preservesLimits_rightOp, AddGrpCat.forget₂Mon_preservesLimits

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf 📖	mathematical	CategoryTheory.Limits.PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesColimit CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.uliftYoneda	—	CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.coyonedaFunctor_reflectsLimits
instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf 📖	mathematical	CategoryTheory.Limits.PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesColimit CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.yoneda	—	CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.coyonedaFunctor_reflectsLimits
instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1 📖	mathematical	CategoryTheory.Limits.PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesColimit CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.yoneda	—	CategoryTheory.Limits.preservesColimit_of_natIso instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf
instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.uliftYoneda	—	instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.yoneda	—	instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf 📖	mathematical	CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesFiniteCoproducts CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.uliftYoneda	—	instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf CategoryTheory.Limits.instPreservesLimitsOfShapeOppositeOfIsGroupoid CategoryTheory.instIsGroupoidDiscrete CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf 📖	mathematical	CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Limits.PreservesFiniteCoproducts CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.yoneda	—	instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf CategoryTheory.Limits.instPreservesLimitsOfShapeOppositeOfIsGroupoid CategoryTheory.instIsGroupoidDiscrete CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
instPreservesLimitsOfShapeSheafTypeUliftYoneda 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.uliftYoneda	—	CategoryTheory.Limits.preservesLimitsOfShape_of_natIso CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.uliftYonedaFunctor_preservesLimits CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
instPreservesLimitsOfShapeSheafTypeYoneda 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.yoneda	—	CategoryTheory.Limits.preservesLimitsOfShape_of_natIso CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.yonedaFunctor_preservesLimits CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι

---

← Back to Index