Equalizers

📁 Source: Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean

Statistics

Metric	Count
Definitions	0
Theorems closedUnderLimitsOfShape_walkingParallelPair_isIndObject, isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair, isIndObject_limit_comp_yoneda_comp_colim	3
Total	3

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedUnderLimitsOfShape_walkingParallelPair_isIndObject 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category IsIndObject WalkingParallelPair walkingParallelPairHomCategory	—	isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair
isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category IsIndObject WalkingParallelPair walkingParallelPairHomCategory	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk' IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType CategoryTheory.nonempty_indParallelPairPresentation IsIndObject.map functorCategoryHasColimitsOfShape Types.hasColimitsOfShape UnivLE.small UnivLE.self functorCategoryHasLimit Types.hasLimit univLE_of_max CategoryTheory.Iso.isIso_hom isIndObject_limit_comp_yoneda_comp_colim CategoryTheory.instIsFilteredI isIndObject_limit_comp_yoneda hasLimitOfHasLimitsOfShape
isIndObject_limit_comp_yoneda_comp_colim 📖	mathematical	IsIndObject limit CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.flip CategoryTheory.yoneda functorCategoryHasLimit Types.hasLimit UnivLE.small univLE_of_max UnivLE.self	CategoryTheory.Functor.whiskeringRight colim functorCategoryHasColimitsOfShape Types.hasColimitsOfShape	—	functorCategoryHasLimit Types.hasLimit UnivLE.small univLE_of_max UnivLE.self IsIndObject.map functorCategoryHasColimit hasColimitOfHasColimitsOfShape functorCategoryHasColimitsOfShape Types.hasColimitsOfShape CategoryTheory.Iso.isIso_hom hasLimitOfHasLimitsOfShape functorCategoryHasLimitsOfShape Types.hasLimitsOfShape CategoryTheory.instPreservesLimitsOfShapeFunctorColim filtered_colim_preservesFiniteLimits ReflectsFiniteLimits.reflects reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget hasFiniteLimits_of_hasLimits Types.hasLimitsOfSize PreservesLimits.preservesFiniteLimits CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom isIndObject_colimit hasLimitCompEvaluation CategoryTheory.Iso.isIso_inv

---

← Back to Index