Documentation Verification Report

MorphismProperty

📁 Source: Mathlib/CategoryTheory/Limits/MorphismProperty.lean

Statistics

Metric	Count
Definitions `forgetCreatesColimitOfClosed`, `forgetCreatesColimitsOfShapeOfClosed`, `forgetCreatesLimitOfClosed`, `forgetCreatesLimitsOfShapeOfClosed`, `createsLimitsOfShape_walkingCospan`, `instCreatesFiniteLimitsTopOverForget`, `instCreatesLimitsOfShapeTopOverDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso`, `instUniqueHomTopMkId`, `mkIdTerminal`	9
Theorems `closedUnderLimitsOfShape_discrete_empty`, `isClosedUnderColimitsOfShape`, `hasColimit_of_closedUnderColimitsOfShape`, `hasColimitsOfShape_of_closedUnderColimitsOfShape`, `hasLimit_of_closedUnderLimitsOfShape`, `hasLimitsOfShape_of_closedUnderLimitsOfShape`, `hasPullbacks`, `instHasTerminalTopOfContainsIdentities`, `instPreservesFiniteLimitsTopOverForget`, `instPreservesFiniteLimitsTopPullback`, `closedUnderLimitsOfShape_discrete_empty`, `closedUnderLimitsOfShape_pullback`	12
Total	21

CategoryTheory.CostructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedUnderLimitsOfShape_discrete_empty` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape` `CategoryTheory.CostructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.MorphismProperty.costructuredArrowObj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.MorphismProperty.costructuredArrowObj_iff` `CategoryTheory.MorphismProperty.costructuredArrow_iso_iff` `CategoryTheory.MorphismProperty.id_mem`
`isClosedUnderColimitsOfShape` 📖	mathematical	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.IsColimit.desc`	`CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape` `CategoryTheory.CostructuredArrow` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.MorphismProperty.costructuredArrowObj`	—	`CategoryTheory.Limits.comp_preservesColimit` `CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.CommaMorphism.w` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.MorphismProperty.costructuredArrowObj_iff` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `hasColimit` `CategoryTheory.preservesColimit_comp_of_createsColimit` `CategoryTheory.Limits.comp_preservesColimitsOfShape` `CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape` `CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj`

CategoryTheory.MorphismProperty.Comma

Definitions

Name	Category	Theorems
`forgetCreatesColimitOfClosed` 📖	CompOp	—
`forgetCreatesColimitsOfShapeOfClosed` 📖	CompOp	—
`forgetCreatesLimitOfClosed` 📖	CompOp	—
`forgetCreatesLimitsOfShapeOfClosed` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimit_of_closedUnderColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `CategoryTheory.MorphismProperty.Comma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.hasColimit_of_created`
`hasColimitsOfShape_of_closedUnderColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `CategoryTheory.MorphismProperty.Comma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `hasColimit_of_closedUnderColimitsOfShape` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape`
`hasLimit_of_closedUnderLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `CategoryTheory.MorphismProperty.Comma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.hasLimit_of_created`
`hasLimitsOfShape_of_closedUnderLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.MorphismProperty.Comma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `hasLimit_of_closedUnderLimitsOfShape` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape`

CategoryTheory.MorphismProperty.Over

Definitions

Name	Category	Theorems
`createsLimitsOfShape_walkingCospan` 📖	CompOp	—
`instCreatesFiniteLimitsTopOverForget` 📖	CompOp	—
`instCreatesLimitsOfShapeTopOverDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso` 📖	CompOp	—
`instUniqueHomTopMkId` 📖	CompOp	—
`mkIdTerminal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPullbacks` 📖	mathematical	—	`CategoryTheory.Limits.HasPullbacks` `CategoryTheory.MorphismProperty.Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape` `CategoryTheory.Over.instHasPullbacks` `CategoryTheory.Over.closedUnderLimitsOfShape_pullback`
`instHasTerminalTopOfContainsIdentities` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal` `CategoryTheory.MorphismProperty.Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.id_mem` `CategoryTheory.Limits.IsTerminal.hasTerminal`
`instPreservesFiniteLimitsTopOverForget` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `CategoryTheory.MorphismProperty.Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `forget`	—	`CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `instHasTerminalTopOfContainsIdentities` `hasPullbacks` `CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape` `CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight` `CategoryTheory.MorphismProperty.Respects.toRespectsLeft` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso` `CategoryTheory.MorphismProperty.Respects.toRespectsRight` `CategoryTheory.Over.instHasTerminal` `CategoryTheory.Over.instHasPullbacks`
`instPreservesFiniteLimitsTopPullback` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `CategoryTheory.MorphismProperty.Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `pullback` `CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks` `CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks` `CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.comp_preservesLimitsOfShape` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `instPreservesFiniteLimitsTopOverForget` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Over.pullbackIsRightAdjoint` `CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `CategoryTheory.MorphismProperty.instFullOverTopOverForget` `CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget`

CategoryTheory.Over

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedUnderLimitsOfShape_discrete_empty` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.overObj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty` `CategoryTheory.Functor.Faithful.id` `CategoryTheory.Functor.Full.id`
`closedUnderLimitsOfShape_pullback` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.overObj` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair`	—	`CategoryTheory.IsPullback.of_isLimit_cone` `CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `CategoryTheory.widePullbackShape_connected` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.MorphismProperty.overObj_iff` `w` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.of_isPullback` `CategoryTheory.IsPullback.flip` `CategoryTheory.MorphismProperty.of_postcomp` `CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj`

---

← Back to Index