Basic

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

Statistics

Metric	Count
Definitions PreservesColimit, PreservesColimits, PreservesColimitsOfShape, PreservesColimitsOfSize, PreservesLimit, PreservesLimitsOfShape, PreservesLimitsOfSize, ReflectsColimit, ReflectsColimits, ReflectsColimitsOfShape, ReflectsColimitsOfSize, ReflectsLimit, ReflectsLimits, ReflectsLimitsOfShape, ReflectsLimitsOfSize, isColimitOfPreserves, isColimitOfReflects, isLimitOfPreserves, isLimitOfReflects	19
Theorems preserves, preservesColimit, preservesColimitsOfShape, preserves, preservesLimit, preservesLimitsOfShape, reflects, reflectsColimit, reflectsColimitsOfShape, reflects, reflectsLimit, reflectsLimitsOfShape, comp_preservesColimit, comp_preservesColimits, comp_preservesColimitsOfShape, comp_preservesLimit, comp_preservesLimits, comp_preservesLimitsOfShape, comp_reflectsColimit, comp_reflectsColimits, comp_reflectsColimitsOfShape, comp_reflectsLimit, comp_reflectsLimits, comp_reflectsLimitsOfShape, fullyFaithful_reflectsColimits, fullyFaithful_reflectsLimits, id_preservesColimitsOfSize, id_preservesLimitsOfSize, id_reflectsColimits, id_reflectsLimits, instHasColimitCompOfPreservesColimit, instHasLimitCompOfPreservesLimit, isIso_app_coconePt_of_preservesColimit, preservesColimit_of_iso_diagram, preservesColimit_of_natIso, preservesColimit_of_preserves_colimit_cocone, preservesColimit_of_reflects_of_preserves, preservesColimit_subsingleton, preservesColimitsOfShape_of_equiv, preservesColimitsOfShape_of_natIso, preservesColimitsOfShape_of_reflects_of_preserves, preservesColimitsOfShape_subsingleton, preservesColimitsOfSize_of_univLE, preservesColimitsOfSize_shrink, preservesColimitsOfSize_subsingleton, preservesColimits_of_natIso, preservesColimits_of_reflects_of_preserves, preservesLimit_of_iso_diagram, preservesLimit_of_natIso, preservesLimit_of_preserves_limit_cone, preservesLimit_of_reflects_of_preserves, preservesLimit_subsingleton, preservesLimitsOfShape_of_equiv, preservesLimitsOfShape_of_natIso, preservesLimitsOfShape_of_reflects_of_preserves, preservesLimitsOfShape_subsingleton, preservesLimitsOfSize_of_univLE, preservesLimitsOfSize_shrink, preservesLimitsOfSize_subsingleton, preservesLimits_of_natIso, preservesLimits_of_reflects_of_preserves, preservesSmallestColimits_of_preservesColimits, preservesSmallestLimits_of_preservesLimits, reflectsColimit_of_iso_diagram, reflectsColimit_of_natIso, reflectsColimit_of_reflectsColimitsOfShape, reflectsColimit_of_reflectsIsomorphisms, reflectsColimit_subsingleton, reflectsColimitsOfShape_of_equiv, reflectsColimitsOfShape_of_natIso, reflectsColimitsOfShape_of_reflectsColimits, reflectsColimitsOfShape_of_reflectsIsomorphisms, reflectsColimitsOfShape_subsingleton, reflectsColimitsOfSize_of_univLE, reflectsColimitsOfSize_shrink, reflectsColimits_of_natIso, reflectsColimits_of_reflectsIsomorphisms, reflectsLimit_of_iso_diagram, reflectsLimit_of_natIso, reflectsLimit_of_reflectsIsomorphisms, reflectsLimit_of_reflectsLimitsOfShape, reflectsLimit_subsingleton, reflectsLimitsOfShape_of_equiv, reflectsLimitsOfShape_of_natIso, reflectsLimitsOfShape_of_reflectsIsomorphisms, reflectsLimitsOfShape_of_reflectsLimits, reflectsLimitsOfShape_subsingleton, reflectsLimitsOfSize_of_univLE, reflectsLimitsOfSize_shrink, reflectsLimits_of_natIso, reflectsLimits_of_reflectsIsomorphisms, reflectsSmallestColimits_of_reflectsColimits, reflectsSmallestLimits_of_reflectsLimits, reflects_colimits_subsingleton, reflects_limits_subsingleton	95
Total	114

CategoryTheory.Limits

Definitions

Name	Category	Theorems
PreservesColimit 📖	CompData	74 math math: PreservesColimitsOfShape.preservesColimit, preservesColimit_of_reflects_of_preserves, AlgebraicGeometry.preservesColimit_Γ, CategoryTheory.preservesColimit_comp_of_createsColimit, CategoryTheory.ShortComplex.instPreservesColimitπ₁, CategoryTheory.preserves_fin_of_preserves_binary_and_initial, PreservesCokernel.of_iso_comparison, of_iso_comparison, CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f', CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf', CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, PreservesColimitPair.of_iso_coprod_comparison, preservesColimit_rightOp, Action.instPreservesColimitForgetOfHasColimitComp, preservesColimit_unop, preservesColimit_leftOp, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, Action.Functor.mapActionPreservesColimit_of_preserves, preservesBinaryCoproduct_of_preservesBinaryBiproduct, AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf, AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, PreservesCoproduct.of_iso_comparison, CategoryTheory.ShortComplex.instPreservesColimitπ₃, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair, preservesColimit_subsingleton, CategoryTheory.ShortComplex.instPreservesColimitπ₂, CategoryTheory.IsGrothendieckAbelian.preservesColimit_coyoneda_obj_of_mono, CategoryTheory.Functor.PreservesHomology.preservesCokernels, preservesInitial_of_isIso, preservesColimit_of_op, HomologicalComplex.instPreservesColimitEval, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms, AlgebraicGeometry.Scheme.IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace, preservesColimit_of_iso_diagram, comp_preservesColimit, preservesCoproduct_of_preservesBiproduct, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.f, evaluation_preservesColimit, CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left, preservesColimit_of_leftOp, preservesSplitCoequalizers, preservesColimit_op, preservesColimit_coyoneda_of_finitePresentation, CategoryTheory.preservesColimit_of_isIso_post, CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair, PreservesInitial.of_iso_comparison, FormalCoproduct.instPreservesColimitDiscreteFunctorObjFunctorEval, preservesColimit_of_preserves_colimit_cocone, PreservesPushout.of_iso_comparison, CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit, CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_right, CategoryTheory.Functor.PreservesHomology.preservesCokernel, preservesInitial_of_iso, CategoryTheory.instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda, AlgebraicGeometry.instPreservesColimitOverSchemeTopMorphismPropertyOverForget, Action.preservesColimit_of_preserves, preservesPushout_symmetry, preservesColimit_of_natIso, CategoryTheory.SmallObject.preservesColimit, PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier, CategoryTheory.Functor.Final.comp_preservesColimit, CategoryTheory.Functor.Final.preservesColimit_of_comp, preservesColimit_of_rightOp, preservesCokernel_zero', preservesCokernel_zero, CategoryTheory.ObjectProperty.preservesColimit_iff, CommRingCat.preservesColimit_coyoneda_of_finitePresentation, preservesColimit_of_unop, CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out, ModuleCat.preservesColimit_restrictScalars
PreservesColimits 📖	MathDef	17 math math: preservesColimits_rightOp, preservesColimits_of_unop, AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace, TopCat.forget_preservesColimits, CategoryTheory.Adjunction.colim_preservesColimits, Action.preservesColimits_forget, CategoryTheory.instPreservesColimitsTensorLeft, preservesColimits_unop, preservesColimits_leftOp, evaluation_preservesColimits, AlgebraicGeometry.PresheafedSpace.forget_preservesColimits, preservesColimits_op, preservesColimits_of_leftOp, AlgebraicGeometry.SheafedSpace.instPreservesColimitsTopCatForgetOfHasLimits, preservesColimits_of_rightOp, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, preservesColimits_of_op
PreservesColimitsOfShape 📖	CompData	85 math math: preservesColimitsOfShape_of_reflects_of_preserves, preservesColimitsOfShape_rightOp, CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem, preservesColimitsOfShape_of_natIso, HomologicalComplex.instPreservesColimitsOfShapeSingle, CategoryTheory.Functor.preservesBinaryCoproducts_of_preservesCokernels, instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts, PresheafOfModules.evaluation_preservesColimitsOfShape, PreservesFilteredColimitsOfSize.preserves_filtered_colimits, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite, preservesBinaryCoproducts_of_preservesBinaryBiproducts, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups, CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial, CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₃, preservesCoproductsOfShape_of_preservesBiproductsOfShape, preservesColimitsOfShape_of_leftOp, CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall, CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall, CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₂, AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall, CategoryTheory.Functor.preservesColimitsOfShape_of_isZero, preservesColimit_of_preservesCoequalizers_and_coproduct, CategoryTheory.preservesShape_fin_of_preserves_binary_and_initial, CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final, preservesColimitsOfShape_subsingleton, AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite, CategoryTheory.IsMonoidalLeftDistrib.preservesBinaryCoproducts_tensorLeft, CategoryTheory.IsMonoidalRightDistrib.preservesBinaryCoproducts_tensorRight, CategoryTheory.Comma.preservesColimitsOfShape_snd, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec, CategoryTheory.whiskeringRight_preservesColimitsOfShape, PreservesColimitsOfSize.preservesColimitsOfShape, CategoryTheory.Arrow.preservesColimitsOfShape_leftFunc, preservesColimitsOfShape_of_op, comp_preservesColimitsOfShape, CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, HomologicalComplex.instPreservesColimitsOfShapeEvalOfHasColimitsOfShape, CategoryTheory.Comma.preservesColimitsOfShape_fst, evaluation_preservesColimitsOfShape, preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape, PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier, preservesColimitsOfShape_of_equiv, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite, PresheafOfModules.toPresheaf_preservesColimitsOfShape, CategoryTheory.instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape, FormalCoproduct.instPreservesColimitsOfShapeDiscreteObjFunctorEval, preservesBinaryCoproducts_of_preservesInitial_and_pushouts, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec, CategoryTheory.whiskeringLeft_preservesColimitsOfShape, preservesColimitsOfShape_leftOp, CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint, ModuleCat.forget₂PreservesColimitsOfShape, CategoryTheory.Arrow.preservesColimitsOfShape_rightFunc, CategoryTheory.rightAdjoint_preservesInitial_of_coreflective, AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite, CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₁, preservesColimitsOfShape_pempty_of_preservesInitial, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget, preservesBinaryCoproducts_of_isIso_coprodComparison, Action.Functor.mapActionPreservesColimitsOfShapeOfPreserves, CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible, preservesColimitsOfShapeOfPreservesFiniteColimits, PreservesFiniteCoproducts.preserves, CategoryTheory.ObjectProperty.preservesColimitsOfShape_iff, CategoryTheory.Functor.preservesCoequalizers_of_preservesCokernels, PreservesWellOrderContinuousOfShape.preservesColimitsOfShape, PreservesColimitsOfShape.underPost, Action.instPreservesColimitsOfShapeForgetOfHasColimitsOfShape, Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts, CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape, preservesColimitsOfShape_unop, preservesColimitsOfShape_op, Action.preservesColimitsOfShape_of_preserves, AlgebraicGeometry.LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, preservesColimitsOfShape_of_rightOp, AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer, preservesColimitsOfShape_of_unop, CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShape, preservesColimitsOfShape_of_discrete, CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable, CategoryTheory.instPreservesColimitsOfShapeFunctorLim, PreservesFiniteColimits.preservesFiniteColimits
PreservesColimitsOfSize 📖	CompData	45 math math: preservesColimitsOfSize_shrink, PreservesColimitsOfSize.underPost, ModuleCat.forget₂PreservesColimitsOfSize, CategoryTheory.whiskeringRightPreservesColimits, Types.instPreservesColimitsOfSizeUliftFunctor, CategoryTheory.Presheaf.isLeftKanExtension_along_yoneda_iff, preservesColimitsOfSize_subsingleton, preservesColimits_of_reflects_of_preserves, preservesColimits_of_preservesCoequalizers_and_coproducts, CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension, CategoryTheory.Functor.preservesColimitsOfSize_of_isZero, preservesColimitsOfSize_of_op, CategoryTheory.Adjunction.leftAdjoint_preservesColimits, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeFunctorOppositePresheafFiber, preservesColimitsOfSize_of_rightOp, preservesColimitsOfSize_unop, preservesColimitsOfSize_op, CategoryTheory.Over.preservesColimitsOfSize_map, preservesColimitsOfSize_of_unop, SheafOfModules.instPreservesColimitsOfSize, CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_iff, comp_preservesColimits, Action.preservesColimitsOfSize_of_preserves, CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom, CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeSheafSheafFiberOfHasSheafifyOfWEqualsLocallyBijectiveOfReflectsIsomorphismsOfPreservesFilteredColimitsOfSizeForgetOfLocallySmall, CategoryTheory.preservesColimits_of_createsColimits_and_hasColimits, CategoryTheory.whiskeringLeft_preservesColimit, PresheafOfModules.evaluation_preservesColimitsOfSize, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, CategoryTheory.Adjunction.isEquivalence_preservesColimits, preservesColimits_const, TopCat.instPreservesColimitsOfSizeUliftFunctor, preservesColimitsOfSize_leftOp, id_preservesColimitsOfSize, preservesColimitsOfSize_of_univLE, preservesColimitsOfSize_rightOp, Action.Functor.preservesColimitsOfSize_of_preserves, preservesColimits_of_natIso, TopCat.forget_preservesColimitsOfSize, PresheafOfModules.toPresheaf_preservesColimitsOfSize, CategoryTheory.Presheaf.preservesColimitsOfSize_leftKanExtension, AddCommGrpCat.instPreservesColimitsOfSizeUliftFunctor, preservesSmallestColimits_of_preservesColimits, preservesColimitsOfSize_of_leftOp
PreservesLimit 📖	CompData	119 math math: CategoryTheory.yoneda_preservesLimit, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl', CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr, TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg', AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj, CategoryTheory.Enriched.HasConicalLimit.preservesLimit_eCoyoneda, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg, CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve, CategoryTheory.Functor.PreservesHomology.preservesKernels, SheafOfModules.evaluationPreservesLimit, AddGrpCat.uliftFunctor_preservesLimit, CommGrpCat.forget₂Group_preservesLimit, PreservesLimitsOfShape.preservesLimit, CategoryTheory.Presieve.isSheafFor_iff_preservesProduct, Action.Functor.mapActionPreservesLimit_of_preserves, CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_right, CommGrpCat.uliftFunctor_preservesLimit, CategoryTheory.ShortComplex.instPreservesLimitπ₁, PreservesEqualizer.of_iso_comparison, PresheafOfModules.toPresheaf_preservesLimit, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, preservesLimit_of_natIso, preservesLimit_leftOp, CategoryTheory.IsSifted.colim_preservesLimits_pair_of_sSifted, preservesKernel_zero, preservesLimit_of_unop, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.g, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, PreservesTerminal.of_iso_comparison, preservesLimit_of_iso_diagram, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, preservesLimit_of_op, CategoryTheory.Functor.representable_preservesLimit, CategoryTheory.CartesianMonoidalCategory.preservesLimit_pair_of_isIso_prodComparison, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, preservesLimit_of_reflects_of_preserves, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.out, preservesPullback_symmetry, CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty, SSet.hoFunctor.preservesTerminal, CategoryTheory.Presieve.preservesProduct_of_isSheafFor, CategoryTheory.Functor.Initial.preservesLimit_of_comp, Action.instPreservesLimitForgetOfHasLimitComp, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g', preservesSplitEqualizers, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, PresheafOfModules.evaluation_preservesLimit, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl, comp_preservesLimit, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, preservesTerminal_of_iso, CommRingCat.Under.instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite, AddCommGrpCat.forget₂AddGroup_preservesLimit, PreservesPullback.of_iso_comparison, CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, FormalCoproduct.instPreservesLimitOppositeDiscreteFunctorCompOpObjFunctorEvalOp, HomologicalComplex.instPreservesLimitEval, GrpCat.uliftFunctor_preservesLimit, CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr', CategoryTheory.ShortComplex.instPreservesLimitπ₂, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, PreservesKernel.of_iso_comparison, FundamentalGroupoidFunctor.preservesProduct, AddCommGrpCat.uliftFunctor_preservesLimit, preservesLimit_of_leftOp, AlgebraicGeometry.preservesLimit_rightOp_Γ, CategoryTheory.preservesLimit_of_isIso_post, preservesLimit_op, preservesBinaryProduct_of_preservesBinaryBiproduct, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_left, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft, preservesLimit_unop, CategoryTheory.ShortComplex.instPreservesLimitπ₃, preservesLimit_subsingleton, CategoryTheory.preservesFinOfPreservesBinaryAndTerminal, CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit, CategoryTheory.preservesLimit_comp_of_createsLimit, CategoryTheory.coyoneda_preservesLimit, CategoryTheory.hoFunctor.preservesBinaryProduct, CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms, CategoryTheory.ObjectProperty.preservesLimit_iff, PreservesLimitPair.of_iso_prod_comparison, CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1, CategoryTheory.IsSifted.colim_preservesTerminal_of_isSifted, preservesTerminal_of_isIso, preservesLimit_of_preserves_limit_cone, ModuleCat.forget₂AddCommGroup_preservesLimit, PreservesProduct.of_iso_comparison, CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, evaluation_preservesLimit, preservesLimit_of_rightOp, ModuleCat.preservesLimit_restrictScalars, CategoryTheory.GrothendieckTopology.preservesLimit_diagramFunctor, CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier, CategoryTheory.Functor.Initial.comp_preservesLimit, preservesProduct_of_preservesBiproduct, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, CategoryTheory.Functor.PreservesHomology.preservesKernel, CategoryTheory.Functor.corepresentable_preservesLimit, AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair, preservesLimit_rightOp, preservesKernel_zero', CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit, Action.preservesLimit_of_preserves, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right
PreservesLimitsOfShape 📖	CompData	101 math math: AddCommGrpCat.forget₂AddGroup_preservesLimitsOfShape, HomologicalComplex.instPreservesLimitsOfShapeSingle, CommMonCat.forget_preservesLimitsOfShape, CommGrpCat.forget₂CommMon_preservesLimitsOfShape, PreservesLimitsOfShape.overPost, PreservesLimitsOfShape.ofWidePullbacks, Action.Functor.mapActionPreservesLimitsOfShapeOfPreserves, CategoryTheory.IsSifted.colim_preservesBinaryProducts_of_isSifted, CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_plusFunctor, CategoryTheory.whiskeringLeft_preservesLimitsOfShape, preservesLimitsOfShape_leftOp, CategoryTheory.preservesLimit_of_lan_preservesLimit, SSet.hoFunctor.preservesTerminal', MonCat.forget_preservesLimitsOfShape, PresheafOfModules.instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, comp_preservesLimitsOfShape, CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_diagramFunctor, SheafOfModules.evaluationPreservesLimitsOfShape, AddCommGrpCat.forget_preservesLimitsOfShape, CategoryTheory.leftAdjoint_preservesTerminal_of_reflective, CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_sheafification, AddMonCat.forget_preservesLimitsOfShape, CategoryTheory.preservesBinaryProducts_of_exponentialIdeal, CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₁, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks, preservesLimitsOfShape_of_rightOp, AddCommMonCat.forget_preservesLimitsOfShape, preservesBinaryProducts_of_isIso_prodComparison, Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite, CommRingCat.Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier, preservesLimitsOfShape_of_discrete, AddGrpCat.uliftFunctor_preservesLimitsOfShape, preservesBinaryProducts_of_preservesTerminal_and_pullbacks, preservesLimitsOfShape_op, CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint, AddGrpCat.forget_preservesLimitsOfShape, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, CategoryTheory.CartesianMonoidalCategory.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison, preservesLimit_of_preservesEqualizers_and_product, CategoryTheory.Functor.instPreservesLimitsOfShapeDiscreteWalkingPairOfIsHomological, CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected, PreservesFiniteLimits.preservesFiniteLimits, Action.preservesLimitsOfShape_of_preserves, CategoryTheory.yoneda_preservesLimitsOfShape, preservesLimitsOfShape_unop, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier, PreservesFiniteProducts.preserves, preservesLimitsOfShape_of_equiv, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesTerminalObjects, CategoryTheory.instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape, CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₂, CategoryTheory.Functor.Initial.preservesLimitsOfShape_of_initial, CategoryTheory.Functor.preservesLimitsOfShape_of_isZero, CommGrpCat.uliftFunctor_preservesLimitsOfShape, GrpCat.uliftFunctor_preservesLimitsOfShape, instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts, CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape, CategoryTheory.Over.forgetPreservesConnectedLimits, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape, CategoryTheory.hoFunctor.preservesBinaryProducts, CategoryTheory.Functor.representable_preservesLimitsOfShape, PresheafOfModules.instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, CategoryTheory.coyonedaPreservesLimitsOfShape, filtered_colim_preservesFiniteLimits, CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₃, preservesLimitsOfShape_of_op, TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, CategoryTheory.Localization.preservesProductsOfShape, preservesLimitsOfShape_of_natIso, Action.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape, AddCommGrpCat.uliftFunctor_preservesLimitsOfShape, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, HomologicalComplex.instPreservesLimitsOfShapeEvalOfHasLimitsOfShape, CategoryTheory.Functor.preservesBinaryProducts_of_preservesKernels, PreservesLimitsOfSize.preservesLimitsOfShape, preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.instPreservesLimitsOfShapeFunctorColim, CategoryTheory.Functor.preservesEqualizers_of_preservesKernels, preservesProductsOfShape_of_preservesBiproductsOfShape, GrpCat.forget_preservesLimitsOfShape, CategoryTheory.Mon.forget_preservesLimitsOfShape, preservesEqualizers_of_preservesPullbacks_and_binaryProducts, CategoryTheory.whiskeringRight_preservesLimitsOfShape, preservesLimitsOfShape_of_leftOp, CategoryTheory.IsSifted.colim_preservesLimitsOfShape_pempty_of_isSifted, preservesLimitsOfShape_of_unop, CategoryTheory.ObjectProperty.preservesLimitsOfShape_iff, preservesLimitsOfShapeOfPreservesFiniteLimits, preservesBinaryProducts_of_preservesBinaryBiproducts, SheafOfModules.forgetPreservesLimitsOfShape, preservesLimitsOfShape_subsingleton, preservesLimitsOfShape_rightOp, CategoryTheory.Functor.corepresentable_preservesLimitsOfShape, CategoryTheory.prod_preservesConnectedLimits, evaluation_preservesLimitsOfShape, preservesLimitsOfShape_pempty_of_preservesTerminal, CommGrpCat.forget₂Group_preservesLimitsOfShape, CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair, CategoryTheory.CostructuredArrow.instPreservesLimitsOfShapeProjOfIsConnected, CommGrpCat.forget_preservesLimitsOfShape, PreservesCofilteredLimitsOfSize.preserves_cofiltered_limits
PreservesLimitsOfSize 📖	CompData	82 math math: CommRingCat.forget₂Ring_preservesLimitsOfSize, CategoryTheory.whiskeringRightPreservesLimits, CommRingCat.forget_preservesLimitsOfSize, ModuleCat.forget_preservesLimitsOfSize, CommGrpCat.uliftFunctor_preservesLimitsOfSize, ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize, AddMonCat.forget_preservesLimitsOfSize, CategoryTheory.Functor.preservesLimitsOfSize_of_isZero, MonCat.forget_preservesLimitsOfSize, CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize, TopCat.instPreservesLimitsOfSizeUliftFunctor, AddCommMonCat.forget₂AddMonPreservesLimitsOfSize, SheafOfModules.evaluationPreservesLimitsOfSize, CommMonCat.forget_preservesLimitsOfSize, CommGrpCat.forget₂CommMon_preservesLimitsOfSize, preservesLimitsOfSize_op, TopCat.forget_preservesLimitsOfSize, preservesLimits_of_preservesEqualizers_and_products, AlgCat.forget₂Ring_preservesLimitsOfSize, SemiRingCat.forget₂Mon_preservesLimitsOfSize, preservesSmallestLimits_of_preservesLimits, PresheafOfModules.instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, CategoryTheory.coyoneda_preservesLimits, AddGrpCat.forget₂AddMonPreservesLimitsOfSize, RingCat.forget₂SemiRing_preservesLimitsOfSize, SemiRingCat.forget_preservesLimitsOfSize, preservesLimitsOfSize_leftOp, GrpCat.uliftFunctor_preservesLimitsOfSize, preservesLimitsOfSize_of_unop, AlgCat.forget₂Module_preservesLimitsOfSize, preservesLimitsOfSize_rightOp, AddCommGrpCat.uliftFunctor_preservesLimitsOfSize, CommMonCat.forget₂Mon_preservesLimitsOfSize, preservesLimitsOfSize_shrink, CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom, CategoryTheory.Functor.representable_preservesLimits, RingCat.forget_preservesLimitsOfSize, preservesLimitsOfSize_of_rightOp, CategoryTheory.whiskeringLeft_preservesLimits, preservesLimitsOfSize_of_op, AddGrpCat.uliftFunctor_preservesLimitsOfSize, CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint, CategoryTheory.Adjunction.isEquivalencePreservesLimits, CategoryTheory.yonedaFunctor_preservesLimits, PresheafOfModules.instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, AddCommGrpCat.forget₂AddGroup_preservesLimitsOfSize, CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda, preservesLimitsOfSize_subsingleton, id_preservesLimitsOfSize, preservesLimitsOfSize_unop, CategoryTheory.Adjunction.rightAdjoint_preservesLimits, preservesLimits_const, CommGrpCat.forget₂Group_preservesLimitsOfSize, AlgCat.forget_preservesLimitsOfSize, PreservesLimitsOfSize.overPost, SheafOfModules.forgetPreservesLimitsOfSize, ModuleCat.instPreservesLimitsOfSizeUliftFunctor, AddGrpCat.forget_preservesLimitsOfSize, Action.Functor.preservesLimitsOfSize_of_preserves, Types.instPreservesLimitsOfSizeUliftFunctor, CommSemiRingCat.forget₂SemiRing_preservesLimitsOfSize, Action.preservesLimitsOfSize_of_preserves, CommSemiRingCat.forget_preservesLimitsOfSize, RingCat.forget₂AddCommGroup_preservesLimitsOfSize, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize, CategoryTheory.yoneda_preservesLimits, preservesLimitsOfSize_of_univLE, AddCommMonCat.forget_preservesLimitsOfSize, preservesLimits_of_reflects_of_preserves, CommGrpCat.forget_preservesLimitsOfSize, comp_preservesLimits, preservesLimitsOfSize_of_leftOp, GrpCat.forget_preservesLimitsOfSize, SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize, CategoryTheory.coyonedaFunctor_preservesLimits, preservesLimits_of_natIso, CategoryTheory.uliftYonedaFunctor_preservesLimits, CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits, GrpCat.forget₂Mon_preservesLimitsOfSize, CategoryTheory.Under.preservesLimitsOfSize_map, CategoryTheory.Functor.corepresentable_preservesLimits, AddCommGrpCat.forget_preservesLimitsOfSize
ReflectsColimit 📖	CompData	15 math math: CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, reflectsColimit_of_reflectsIsomorphisms, CategoryTheory.CreatesColimit.toReflectsColimit, reflectsColimit_of_natIso, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair, CategoryTheory.Functor.Final.comp_reflectsColimit, CategoryTheory.Functor.Final.reflectsColimit_of_comp, reflectsColimit_subsingleton, ModuleCat.HasColimit.reflectsColimit, reflectsColimit_of_reflectsColimitsOfShape, ReflectsColimitsOfShape.reflectsColimit, reflectsColimit_of_iso_diagram, comp_reflectsColimit, Action.instReflectsColimitForget
ReflectsColimits 📖	MathDef	1 math math: Action.instReflectsColimitsForget
ReflectsColimitsOfShape 📖	CompData	16 math math: CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty, reflectsColimitsOfShape_of_equiv, CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape, ReflectsFilteredColimitsOfSize.reflects_filtered_colimits, reflectsColimitsOfShape_of_reflectsColimits, reflectsColimitsOfShape_of_natIso, CategoryTheory.Functor.Final.reflectsColimitsOfShape_of_final, ReflectsFiniteColimits.reflects, reflectsColimitsOfShape_of_reflectsIsomorphisms, Action.instReflectsColimitsOfShapeForget, instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite, ModuleCat.reflectsColimitsOfShape, ReflectsFiniteCoproducts.reflects, comp_reflectsColimitsOfShape, ReflectsColimitsOfSize.reflectsColimitsOfShape, reflectsColimitsOfShape_subsingleton
ReflectsColimitsOfSize 📖	CompData	12 math math: CategoryTheory.reflectsColimitsOfCreatesColimits, fullyFaithful_reflectsColimits, reflects_colimits_subsingleton, reflectsColimits_of_reflectsIsomorphisms, id_reflectsColimits, reflectsColimitsOfSize_shrink, CategoryTheory.Functor.reflectsColimits_of_isEquivalence, reflectsColimits_of_natIso, CategoryTheory.Types.instReflectsColimitsOfSizeForgetTypeHom, reflectsSmallestColimits_of_reflectsColimits, reflectsColimitsOfSize_of_univLE, comp_reflectsColimits
ReflectsLimit 📖	CompData	19 math math: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair, CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out, ReflectsLimitsOfShape.reflectsLimit, reflectsLimit_subsingleton, reflectsLimit_of_natIso, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, CategoryTheory.CreatesLimit.toReflectsLimit, CategoryTheory.Functor.Initial.reflectsLimit_of_comp, ModuleCat.forget₂AddCommGroup_reflectsLimit, comp_reflectsLimit, Action.instReflectsLimitForget, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, reflectsLimit_of_iso_diagram, CategoryTheory.Functor.Initial.comp_reflectsLimit, reflectsLimit_of_reflectsLimitsOfShape, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, reflectsLimit_of_reflectsIsomorphisms
ReflectsLimits 📖	MathDef	3 math math: ModuleCat.forget_reflectsLimits, Action.instReflectsLimitsForget, ModuleCat.forget₂_reflectsLimits
ReflectsLimitsOfShape 📖	CompData	16 math math: CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty, instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite, CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape, Action.instReflectsLimitsOfShapeForget, ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape, reflectsLimitsOfShape_of_reflectsIsomorphisms, reflectsLimitsOfShape_of_equiv, ReflectsLimitsOfSize.reflectsLimitsOfShape, reflectsLimitsOfShape_of_reflectsLimits, ReflectsFiniteProducts.reflects, CategoryTheory.Functor.Initial.reflectsLimitsOfShape_of_initial, ReflectsCofilteredLimitsOfSize.reflects_cofiltered_limits, reflectsLimitsOfShape_of_natIso, reflectsLimitsOfShape_subsingleton, ReflectsFiniteLimits.reflects, comp_reflectsLimitsOfShape
ReflectsLimitsOfSize 📖	CompData	17 math math: ModuleCat.forget₂_reflectsLimitsOfSize, fullyFaithful_reflectsLimits, CategoryTheory.Types.instReflectsLimitsOfSizeForgetTypeHom, ModuleCat.forget_reflectsLimitsOfSize, CategoryTheory.yonedaFunctor_reflectsLimits, comp_reflectsLimits, id_reflectsLimits, CategoryTheory.reflectsLimitsOfCreatesLimits, reflectsLimits_of_reflectsIsomorphisms, reflectsSmallestLimits_of_reflectsLimits, ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize, reflectsLimitsOfSize_shrink, reflects_limits_subsingleton, CategoryTheory.coyonedaFunctor_reflectsLimits, CategoryTheory.Functor.reflectsLimits_of_isEquivalence, reflectsLimitsOfSize_of_univLE, reflectsLimits_of_natIso
isColimitOfPreserves 📖	CompOp	6 math math: CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, CategoryTheory.Comma.coconeOfPreserves_ι_app_right, CategoryTheory.Comma.coconeOfPreserves_pt_hom, CategoryTheory.Comma.coconeOfPreserves_ι_app_left, SheafOfModules.Presentation.map_relations_I, CategoryTheory.preserves_desc_mapCocone
isColimitOfReflects 📖	CompOp	—
isLimitOfPreserves 📖	CompOp	4 math math: CategoryTheory.Comma.coneOfPreserves_π_app_right, CategoryTheory.Comma.coneOfPreserves_pt_hom, CategoryTheory.preserves_lift_mapCone, CategoryTheory.Comma.coneOfPreserves_π_app_left
isLimitOfReflects 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_preservesColimit 📖	mathematical	—	PreservesColimit CategoryTheory.Functor.comp	—	—
comp_preservesColimits 📖	mathematical	—	PreservesColimitsOfSize CategoryTheory.Functor.comp	—	comp_preservesColimitsOfShape PreservesColimitsOfSize.preservesColimitsOfShape
comp_preservesColimitsOfShape 📖	mathematical	—	PreservesColimitsOfShape CategoryTheory.Functor.comp	—	comp_preservesColimit PreservesColimitsOfShape.preservesColimit
comp_preservesLimit 📖	mathematical	—	PreservesLimit CategoryTheory.Functor.comp	—	—
comp_preservesLimits 📖	mathematical	—	PreservesLimitsOfSize CategoryTheory.Functor.comp	—	comp_preservesLimitsOfShape PreservesLimitsOfSize.preservesLimitsOfShape
comp_preservesLimitsOfShape 📖	mathematical	—	PreservesLimitsOfShape CategoryTheory.Functor.comp	—	comp_preservesLimit PreservesLimitsOfShape.preservesLimit
comp_reflectsColimit 📖	mathematical	—	ReflectsColimit CategoryTheory.Functor.comp	—	ReflectsColimit.reflects
comp_reflectsColimits 📖	mathematical	—	ReflectsColimitsOfSize CategoryTheory.Functor.comp	—	comp_reflectsColimitsOfShape reflectsColimitsOfShape_of_reflectsColimits
comp_reflectsColimitsOfShape 📖	mathematical	—	ReflectsColimitsOfShape CategoryTheory.Functor.comp	—	comp_reflectsColimit reflectsColimit_of_reflectsColimitsOfShape
comp_reflectsLimit 📖	mathematical	—	ReflectsLimit CategoryTheory.Functor.comp	—	ReflectsLimit.reflects
comp_reflectsLimits 📖	mathematical	—	ReflectsLimitsOfSize CategoryTheory.Functor.comp	—	comp_reflectsLimitsOfShape reflectsLimitsOfShape_of_reflectsLimits
comp_reflectsLimitsOfShape 📖	mathematical	—	ReflectsLimitsOfShape CategoryTheory.Functor.comp	—	comp_reflectsLimit reflectsLimit_of_reflectsLimitsOfShape
fullyFaithful_reflectsColimits 📖	mathematical	—	ReflectsColimitsOfSize	—	Cocones.functoriality_full CategoryTheory.Functor.map_injective Cocones.functoriality_faithful CategoryTheory.Functor.map_preimage IsColimit.uniq_cocone_morphism
fullyFaithful_reflectsLimits 📖	mathematical	—	ReflectsLimitsOfSize	—	Cones.functoriality_full CategoryTheory.Functor.map_injective Cones.functoriality_faithful CategoryTheory.Functor.map_preimage IsLimit.uniq_cone_morphism
id_preservesColimitsOfSize 📖	mathematical	—	PreservesColimitsOfSize CategoryTheory.Functor.id	—	CategoryTheory.NatTrans.naturality IsColimit.fac IsColimit.uniq
id_preservesLimitsOfSize 📖	mathematical	—	PreservesLimitsOfSize CategoryTheory.Functor.id	—	CategoryTheory.NatTrans.naturality IsLimit.fac IsLimit.uniq
id_reflectsColimits 📖	mathematical	—	ReflectsColimitsOfSize CategoryTheory.Functor.id	—	CategoryTheory.NatTrans.naturality IsColimit.fac IsColimit.uniq
id_reflectsLimits 📖	mathematical	—	ReflectsLimitsOfSize CategoryTheory.Functor.id	—	CategoryTheory.NatTrans.naturality IsLimit.fac IsLimit.uniq
instHasColimitCompOfPreservesColimit 📖	mathematical	—	HasColimit CategoryTheory.Functor.comp	—	—
instHasLimitCompOfPreservesLimit 📖	mathematical	—	HasLimit CategoryTheory.Functor.comp	—	—
isIso_app_coconePt_of_preservesColimit 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj Cocone.pt CategoryTheory.NatTrans.app	—	IsColimit.hom_ext CategoryTheory.NatTrans.naturality IsColimit.ι_map CategoryTheory.Iso.isIso_hom
preservesColimit_of_iso_diagram 📖	mathematical	—	PreservesColimit	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id
preservesColimit_of_natIso 📖	mathematical	—	PreservesColimit	—	—
preservesColimit_of_preserves_colimit_cocone 📖	mathematical	—	PreservesColimit	—	—
preservesColimit_of_reflects_of_preserves 📖	mathematical	—	PreservesColimit	—	—
preservesColimit_subsingleton 📖	mathematical	—	PreservesColimit	—	—
preservesColimitsOfShape_of_equiv 📖	mathematical	—	PreservesColimitsOfShape	—	PreservesColimitsOfShape.preservesColimit CategoryTheory.Equivalence.invFunIdAssoc_inv_app CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id
preservesColimitsOfShape_of_natIso 📖	mathematical	—	PreservesColimitsOfShape	—	preservesColimit_of_natIso PreservesColimitsOfShape.preservesColimit
preservesColimitsOfShape_of_reflects_of_preserves 📖	mathematical	—	PreservesColimitsOfShape	—	preservesColimit_of_reflects_of_preserves PreservesColimitsOfShape.preservesColimit reflectsColimit_of_reflectsColimitsOfShape
preservesColimitsOfShape_subsingleton 📖	mathematical	—	PreservesColimitsOfShape	—	—
preservesColimitsOfSize_of_univLE 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfShape_of_equiv UnivLE.small CategoryTheory.locallySmall_of_univLE PreservesColimitsOfSize.preservesColimitsOfShape
preservesColimitsOfSize_shrink 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfSize_of_univLE univLE_of_max UnivLE.self
preservesColimitsOfSize_subsingleton 📖	mathematical	—	PreservesColimitsOfSize	—	—
preservesColimits_of_natIso 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfShape_of_natIso PreservesColimitsOfSize.preservesColimitsOfShape
preservesColimits_of_reflects_of_preserves 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfShape_of_reflects_of_preserves PreservesColimitsOfSize.preservesColimitsOfShape reflectsColimitsOfShape_of_reflectsColimits
preservesLimit_of_iso_diagram 📖	mathematical	—	PreservesLimit	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.id_comp
preservesLimit_of_natIso 📖	mathematical	—	PreservesLimit	—	—
preservesLimit_of_preserves_limit_cone 📖	mathematical	—	PreservesLimit	—	—
preservesLimit_of_reflects_of_preserves 📖	mathematical	—	PreservesLimit	—	—
preservesLimit_subsingleton 📖	mathematical	—	PreservesLimit	—	—
preservesLimitsOfShape_of_equiv 📖	mathematical	—	PreservesLimitsOfShape	—	PreservesLimitsOfShape.preservesLimit CategoryTheory.Equivalence.invFunIdAssoc_hom_app Cone.w CategoryTheory.Category.id_comp
preservesLimitsOfShape_of_natIso 📖	mathematical	—	PreservesLimitsOfShape	—	preservesLimit_of_natIso PreservesLimitsOfShape.preservesLimit
preservesLimitsOfShape_of_reflects_of_preserves 📖	mathematical	—	PreservesLimitsOfShape	—	preservesLimit_of_reflects_of_preserves PreservesLimitsOfShape.preservesLimit reflectsLimit_of_reflectsLimitsOfShape
preservesLimitsOfShape_subsingleton 📖	mathematical	—	PreservesLimitsOfShape	—	—
preservesLimitsOfSize_of_univLE 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfShape_of_equiv UnivLE.small CategoryTheory.locallySmall_of_univLE PreservesLimitsOfSize.preservesLimitsOfShape
preservesLimitsOfSize_shrink 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfSize_of_univLE univLE_of_max UnivLE.self
preservesLimitsOfSize_subsingleton 📖	mathematical	—	PreservesLimitsOfSize	—	—
preservesLimits_of_natIso 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfShape_of_natIso PreservesLimitsOfSize.preservesLimitsOfShape
preservesLimits_of_reflects_of_preserves 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfShape_of_reflects_of_preserves PreservesLimitsOfSize.preservesLimitsOfShape reflectsLimitsOfShape_of_reflectsLimits
preservesSmallestColimits_of_preservesColimits 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfSize_shrink
preservesSmallestLimits_of_preservesLimits 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfSize_shrink
reflectsColimit_of_iso_diagram 📖	mathematical	—	ReflectsColimit	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp
reflectsColimit_of_natIso 📖	mathematical	—	ReflectsColimit	—	ReflectsColimit.reflects
reflectsColimit_of_reflectsColimitsOfShape 📖	mathematical	—	ReflectsColimit	—	ReflectsColimitsOfShape.reflectsColimit
reflectsColimit_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsColimit	—	IsColimit.hom_isIso CategoryTheory.isIso_of_reflects_iso Cocones.reflects_cocone_isomorphism CategoryTheory.Functor.map_isIso
reflectsColimit_subsingleton 📖	mathematical	—	ReflectsColimit	—	—
reflectsColimitsOfShape_of_equiv 📖	mathematical	—	ReflectsColimitsOfShape	—	reflectsColimit_of_reflectsColimitsOfShape
reflectsColimitsOfShape_of_natIso 📖	mathematical	—	ReflectsColimitsOfShape	—	reflectsColimit_of_natIso reflectsColimit_of_reflectsColimitsOfShape
reflectsColimitsOfShape_of_reflectsColimits 📖	mathematical	—	ReflectsColimitsOfShape	—	ReflectsColimitsOfSize.reflectsColimitsOfShape
reflectsColimitsOfShape_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsColimitsOfShape	—	reflectsColimit_of_reflectsIsomorphisms hasColimitOfHasColimitsOfShape PreservesColimitsOfShape.preservesColimit
reflectsColimitsOfShape_subsingleton 📖	mathematical	—	ReflectsColimitsOfShape	—	—
reflectsColimitsOfSize_of_univLE 📖	mathematical	—	ReflectsColimitsOfSize	—	reflectsColimitsOfShape_of_equiv UnivLE.small CategoryTheory.locallySmall_of_univLE reflectsColimitsOfShape_of_reflectsColimits
reflectsColimitsOfSize_shrink 📖	mathematical	—	ReflectsColimitsOfSize	—	reflectsColimitsOfSize_of_univLE univLE_of_max UnivLE.self
reflectsColimits_of_natIso 📖	mathematical	—	ReflectsColimitsOfSize	—	reflectsColimitsOfShape_of_natIso reflectsColimitsOfShape_of_reflectsColimits
reflectsColimits_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsColimitsOfSize	—	reflectsColimitsOfShape_of_reflectsIsomorphisms hasColimitsOfShapeOfHasColimitsOfSize PreservesColimitsOfSize.preservesColimitsOfShape
reflectsLimit_of_iso_diagram 📖	mathematical	—	ReflectsLimit	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.id_comp
reflectsLimit_of_natIso 📖	mathematical	—	ReflectsLimit	—	ReflectsLimit.reflects
reflectsLimit_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsLimit	—	IsLimit.hom_isIso CategoryTheory.isIso_of_reflects_iso Cones.reflects_cone_isomorphism CategoryTheory.Functor.map_isIso
reflectsLimit_of_reflectsLimitsOfShape 📖	mathematical	—	ReflectsLimit	—	ReflectsLimitsOfShape.reflectsLimit
reflectsLimit_subsingleton 📖	mathematical	—	ReflectsLimit	—	—
reflectsLimitsOfShape_of_equiv 📖	mathematical	—	ReflectsLimitsOfShape	—	reflectsLimit_of_reflectsLimitsOfShape
reflectsLimitsOfShape_of_natIso 📖	mathematical	—	ReflectsLimitsOfShape	—	reflectsLimit_of_natIso reflectsLimit_of_reflectsLimitsOfShape
reflectsLimitsOfShape_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsLimitsOfShape	—	reflectsLimit_of_reflectsIsomorphisms hasLimitOfHasLimitsOfShape PreservesLimitsOfShape.preservesLimit
reflectsLimitsOfShape_of_reflectsLimits 📖	mathematical	—	ReflectsLimitsOfShape	—	ReflectsLimitsOfSize.reflectsLimitsOfShape
reflectsLimitsOfShape_subsingleton 📖	mathematical	—	ReflectsLimitsOfShape	—	—
reflectsLimitsOfSize_of_univLE 📖	mathematical	—	ReflectsLimitsOfSize	—	reflectsLimitsOfShape_of_equiv UnivLE.small CategoryTheory.locallySmall_of_univLE reflectsLimitsOfShape_of_reflectsLimits
reflectsLimitsOfSize_shrink 📖	mathematical	—	ReflectsLimitsOfSize	—	reflectsLimitsOfSize_of_univLE univLE_of_max UnivLE.self
reflectsLimits_of_natIso 📖	mathematical	—	ReflectsLimitsOfSize	—	reflectsLimitsOfShape_of_natIso reflectsLimitsOfShape_of_reflectsLimits
reflectsLimits_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsLimitsOfSize	—	reflectsLimitsOfShape_of_reflectsIsomorphisms hasLimitsOfShapeOfHasLimits PreservesLimitsOfSize.preservesLimitsOfShape
reflectsSmallestColimits_of_reflectsColimits 📖	mathematical	—	ReflectsColimitsOfSize	—	reflectsColimitsOfSize_shrink
reflectsSmallestLimits_of_reflectsLimits 📖	mathematical	—	ReflectsLimitsOfSize	—	reflectsLimitsOfSize_shrink
reflects_colimits_subsingleton 📖	mathematical	—	ReflectsColimitsOfSize	—	—
reflects_limits_subsingleton 📖	mathematical	—	ReflectsLimitsOfSize	—	—

CategoryTheory.Limits.PreservesColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.Limits.IsColimit CategoryTheory.Functor.comp CategoryTheory.Functor.mapCocone	—	—

CategoryTheory.Limits.PreservesColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesColimit 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit	—	—

CategoryTheory.Limits.PreservesColimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape	—	—

CategoryTheory.Limits.PreservesLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.Limits.IsLimit CategoryTheory.Functor.comp CategoryTheory.Functor.mapCone	—	—

CategoryTheory.Limits.PreservesLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit	—	—

CategoryTheory.Limits.PreservesLimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape	—	—

CategoryTheory.Limits.ReflectsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.Limits.IsColimit	—	—

CategoryTheory.Limits.ReflectsColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsColimit 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimit	—	—

CategoryTheory.Limits.ReflectsColimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfShape	—	—

CategoryTheory.Limits.ReflectsLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.Limits.IsLimit	—	—

CategoryTheory.Limits.ReflectsLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsLimit 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimit	—	—

CategoryTheory.Limits.ReflectsLimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfShape	—	—

---

← Back to Index