Documentation Verification Report

Local

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Local.lean

Statistics

Metric	Count
Definitions `isColocal`, `isLocal`	2
Theorems `instIsClosedUnderColimitsOfShapeIsColocal`, `instIsClosedUnderIsomorphismsIsColocal`, `instIsClosedUnderIsomorphismsIsLocal`, `instIsClosedUnderLimitsOfShapeIsLocal`, `isColocal_iff`, `isLocal_iff`	6
Total	8

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`isColocal` 📖	CompOp	8 math math: `instIsClosedUnderIsomorphismsIsColocal`, `CategoryTheory.ObjectProperty.galoisConnection_isColocal`, `CategoryTheory.ObjectProperty.le_isColocal_iff`, `CategoryTheory.ObjectProperty.isColocal_trW`, `le_isColocal_isColocal`, `CategoryTheory.ObjectProperty.le_isColocal_isColocal`, `instIsClosedUnderColimitsOfShapeIsColocal`, `isColocal_iff`
`isLocal` 📖	CompOp	22 math math: `CategoryTheory.Localization.LeftBousfield.galoisConnection`, `isRightAdjoint_ι_isLocal`, `CategoryTheory.OrthogonalReflection.isRightAdjoint_ι`, `CategoryTheory.Localization.LeftBousfield.le_W_iff`, `CategoryTheory.OrthogonalReflection.isLocal_isLocal_reflection`, `CategoryTheory.OrthogonalReflection.leftBousfieldW_isLocal_toSucc`, `CategoryTheory.OrthogonalReflection.isLocal_reflectionObj`, `le_isLocal_isLocal`, `CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc`, `CategoryTheory.ObjectProperty.le_isLocal_iff`, `CategoryTheory.ObjectProperty.le_isLocal_isLocal`, `instIsClosedUnderIsomorphismsIsLocal`, `isLocal_iff`, `CategoryTheory.OrthogonalReflection.isIso_toSucc_iff`, `le_leftBousfieldW_isLocal`, `instIsClosedUnderLimitsOfShapeIsLocal`, `CategoryTheory.ObjectProperty.galoisConnection_isLocal`, `isClosedUnderColimitsOfShape_isLocal`, `isCardinalAccessible_ι_isLocal`, `CategoryTheory.ObjectProperty.le_isLocal_W`, `CategoryTheory.ObjectProperty.isLocal_trW`, `isLocallyPresentable_isLocal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedUnderColimitsOfShapeIsColocal` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape` `isColocal`	—	`CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsColimit.fac_assoc`
`instIsClosedUnderIsomorphismsIsColocal` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `isColocal`	—	`Function.Bijective.of_comp_iff` `Equiv.bijective` `CategoryTheory.Category.assoc` `Function.Bijective.comp`
`instIsClosedUnderIsomorphismsIsLocal` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `isLocal`	—	`Function.Bijective.of_comp_iff` `Equiv.bijective` `CategoryTheory.Category.assoc` `Function.Bijective.comp`
`instIsClosedUnderLimitsOfShapeIsLocal` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape` `isLocal`	—	`CategoryTheory.Limits.IsLimit.hom_ext` `CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.LimitPresentation.w` `CategoryTheory.Limits.IsLimit.fac`
`isColocal_iff` 📖	mathematical	—	`isColocal` `Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp`	—	—
`isLocal_iff` 📖	mathematical	—	`isLocal` `Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp`	—	—

---

← Back to Index