Documentation Verification Report

ClosedUnderIsomorphisms

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

Statistics

Metric	Count
Definitions `IsClosedUnderIsomorphisms`, `isoClosure`	2
Theorems `of_iso`, `instIsClosedUnderIsomorphismsInverseImage`, `instIsClosedUnderIsomorphismsIsoClosure`, `instIsClosedUnderIsomorphismsMap`, `isClosedUnderIsomorphisms_iff_isoClosure_eq_self`, `isoClosure_eq_self`, `isoClosure_le_iff`, `isoClosure_strictMap`, `le_isoClosure`, `map_isoClosure`, `monotone_isoClosure`, `prop_iff_of_isIso`, `prop_iff_of_iso`, `prop_isoClosure`, `prop_isoClosure_iff`, `prop_of_isIso`, `prop_of_iso`	17
Total	19

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsClosedUnderIsomorphisms` 📖	CompData	48 math math: `instIsClosedUnderIsomorphismsMin`, `instIsClosedUnderIsomorphismsColimitsOfShape`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsIsColocal`, `IsClosedUnderIsomorphisms.of_inheritedFromSource`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso`, `IsLocal.toIsClosedUnderIsomorphisms`, `isClosedUnderIsomorphisms_iff_isoClosure_eq_self`, `CategoryTheory.instIsClosedUnderIsomorphismsIsCardinalPresentable`, `instIsClosedUnderIsomorphismsRightOrthogonal`, `instIsClosedUnderIsomorphisms_1`, `instIsClosedUnderIsomorphismsColimitsClosure`, `AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat`, `instIsClosedUnderIsomorphismsOppositeOp`, `CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsMinus`, `CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsPlus`, `instIsClosedUnderIsomorphismsLimitsOfShape`, `instIsClosedUnderIsomorphismsColimitsCardinalClosure`, `CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsBounded`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso`, `CategoryTheory.Functor.instIsClosedUnderIsomorphismsHomologicalKernel`, `instIsClosedUnderIsomorphisms`, `instIsClosedUnderIsomorphismsMax`, `instIsClosedUnderIsomorphismsShift`, `instIsClosedUnderIsomorphismsUnopOfOpposite`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso`, `AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover`, `CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms`, `CategoryTheory.Functor.LeftExtension.instIsClosedUnderIsomorphismsIsPointwiseLeftKanExtensionAt`, `CategoryTheory.Limits.IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsIsLocal`, `instIsClosedUnderIsomorphismsMap`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso`, `instIsClosedUnderIsomorphismsInd`, `CategoryTheory.Functor.RightExtension.instIsClosedUnderIsomorphismsIsPointwiseRightKanExtensionAt`, `CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms`, `CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms`, `instIsClosedUnderIsomorphismsTop`, `IsClosedUnderBinaryProducts.closedUnderIsomorphisms`, `instIsClosedUnderIsomorphismsIsoClosure`, `CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage`, `CategoryTheory.Functor.instIsClosedUnderIsomorphismsIsDenseAt`, `instIsClosedUnderIsomorphismsShiftClosure`, `CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`, `IsClosedUnderIsomorphisms.of_inheritedFromTarget`, `instIsClosedUnderIsomorphismsLeftOrthogonal`, `instIsClosedUnderIsomorphismsLimitsClosure`, `HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic`, `instIsClosedUnderIsomorphismsInverseImage`
`isoClosure` 📖	CompOp	47 math math: `isoClosure_strictMap`, `instIsTriangulatedIsoClosure`, `prop_isoClosure_iff`, `EssentiallySmall.exists_small`, `ext_of_isTriangulatedClosed₃'`, `le_isoClosure`, `IsTriangulatedClosed₂.ext₂'`, `limitsOfShape_isoClosure`, `unop_isoClosure`, `isClosedUnderIsomorphisms_iff_isoClosure_eq_self`, `EssentiallySmall.exists_small_le'`, `colimitsOfShape_isoClosure`, `isoClosure_isColocal`, `IsTriangulatedClosed₁.ext₁'`, `isoClosure_iSup`, `IsCardinalFilteredGenerator.isoClosure_iff`, `map_isoClosure`, `isoClosure_strictColimitsOfShape`, `colimitsClosure_isoClosure`, `monotone_isoClosure`, `IsCardinalFilteredGenerator.isoClosure`, `isoClosure_le_iff`, `isoClosure_strictLimitsClosureIter_eq_limitsClosure`, `prop_isoClosure`, `limitsClosure_isoClosure`, `EssentiallySmall.exists_small_le`, `instIsEquivalenceFullSubcategoryIsoClosureιOfLE`, `isoClosure_strictLimitsOfShape`, `ι_map_top`, `instIsStableUnderShiftByIsoClosure`, `instContainsZeroIsoClosure`, `isoClosure_sup`, `CategoryTheory.Localization.LeftBousfield.W_isoClosure`, `IsTriangulatedClosed₃.ext₃'`, `retractClosure_isoClosure`, `instEssentiallySmallIsoClosure`, `op_isoClosure`, `instIsStableUnderShiftIsoClosure`, `instIsClosedUnderIsomorphismsIsoClosure`, `ext_of_isTriangulatedClosed₂'`, `ext_of_isTriangulatedClosed₁'`, `trW_isoClosure`, `instIsTriangulatedClosed₂IsoClosure`, `isoClosure_eq_self`, `isEquivalence_ιOfLE_iff`, `isoClosure_isLocal`, `essSurj_ιOfLE_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedUnderIsomorphismsInverseImage` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `inverseImage`	—	`prop_of_iso`
`instIsClosedUnderIsomorphismsIsoClosure` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `isoClosure`	—	—
`instIsClosedUnderIsomorphismsMap` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `map`	—	—
`isClosedUnderIsomorphisms_iff_isoClosure_eq_self` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `isoClosure`	—	`isoClosure_eq_self` `instIsClosedUnderIsomorphismsIsoClosure`
`isoClosure_eq_self` 📖	mathematical	—	`isoClosure`	—	`le_antisymm` `prop_of_iso` `le_isoClosure`
`isoClosure_le_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `isoClosure`	—	`LE.le.trans` `le_isoClosure` `monotone_isoClosure` `isoClosure_eq_self` `le_refl`
`isoClosure_strictMap` 📖	mathematical	—	`isoClosure` `strictMap` `map`	—	`le_antisymm` `isoClosure_le_iff` `instIsClosedUnderIsomorphismsMap` `strictMap_le_map`
`le_isoClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `isoClosure`	—	—
`map_isoClosure` 📖	mathematical	—	`map` `isoClosure`	—	`le_antisymm` `map_monotone` `le_isoClosure`
`monotone_isoClosure` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`isoClosure`	—	—
`prop_iff_of_isIso` 📖	—	—	—	—	`prop_iff_of_iso`
`prop_iff_of_iso` 📖	—	—	—	—	`prop_of_iso`
`prop_isoClosure` 📖	mathematical	—	`isoClosure`	—	—
`prop_isoClosure_iff` 📖	mathematical	—	`isoClosure` `CategoryTheory.Iso`	—	—
`prop_of_isIso` 📖	—	—	—	—	`prop_of_iso`
`prop_of_iso` 📖	—	—	—	—	`IsClosedUnderIsomorphisms.of_iso`

CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_iso` 📖	—	—	—	—	—

---

← Back to Index