Documentation Verification Report

Induced

📁 Source: Mathlib/CategoryTheory/Triangulated/TStructure/Induced.lean

Statistics

Metric	Count
Definitions `HasInducedTStructure`, `tStructure`, `onBounded`, `onMinus`, `onPlus`	5
Theorems `exists_triangle_zero_one`, `mk'`, `hasInducedTStructure_iff`, `instHasInducedTStructureMinOfIsClosedUnderIsomorphisms`, `mem_of_hasInductedTStructure`, `tStructure_isGE_iff`, `tStructure_isLE_iff`, `instHasInducedTStructureBounded`, `instHasInducedTStructureMinus`, `instHasInducedTStructurePlus`	10
Total	15

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`HasInducedTStructure` 📖	CompData	6 math math: `CategoryTheory.Triangulated.TStructure.instHasInducedTStructureBounded`, `instHasInducedTStructureMinOfIsClosedUnderIsomorphisms`, `CategoryTheory.Triangulated.TStructure.instHasInducedTStructureMinus`, `HasInducedTStructure.mk'`, `hasInducedTStructure_iff`, `CategoryTheory.Triangulated.TStructure.instHasInducedTStructurePlus`
`tStructure` 📖	CompOp	2 math math: `tStructure_isGE_iff`, `tStructure_isLE_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasInducedTStructure_iff` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`HasInducedTStructure` `CategoryTheory.Triangulated.TStructure.IsLE` `CategoryTheory.Triangulated.TStructure.IsGE` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `isoClosure`	—	—
`instHasInducedTStructureMinOfIsClosedUnderIsomorphisms` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`HasInducedTStructure` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder` `instIsTriangulatedMinOfIsClosedUnderIsomorphisms`	—	`HasInducedTStructure.mk'` `instIsTriangulatedMinOfIsClosedUnderIsomorphisms` `mem_of_hasInductedTStructure` `CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished` `CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE` `CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE`
`mem_of_hasInductedTStructure` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `CategoryTheory.Pretriangulated.Triangle.obj₂`	`CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₃`	—	`IsTriangulated.toIsStableUnderShift` `instHasZeroObjectFullSubcategoryOfContainsZero` `IsTriangulated.toContainsZero` `instAdditiveFullSubcategoryShiftFunctor` `CategoryTheory.Triangulated.TStructure.triangle_iso_exists` `CategoryTheory.Functor.map_distinguished` `instIsTriangulatedFullSubcategoryι` `CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished` `tStructure_isLE_iff` `CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE` `tStructure_isGE_iff` `CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE` `prop_iff_of_iso` `prop_ι_obj`
`tStructure_isGE_iff` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Triangulated.TStructure.IsGE` `FullSubcategory` `FullSubcategory.category` `CategoryTheory.Preadditive.fullSubcategory` `instHasZeroObjectFullSubcategoryOfContainsZero` `IsTriangulated.toContainsZero` `hasShift` `Int.instAddMonoid` `IsTriangulated.toIsStableUnderShift` `instAdditiveFullSubcategoryShiftFunctor` `instPretriangulatedFullSubcategory` `tStructure` `FullSubcategory.obj`	—	`instHasZeroObjectFullSubcategoryOfContainsZero` `IsTriangulated.toContainsZero` `IsTriangulated.toIsStableUnderShift` `instAdditiveFullSubcategoryShiftFunctor` `CategoryTheory.Triangulated.TStructure.IsGE.ge`
`tStructure_isLE_iff` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Triangulated.TStructure.IsLE` `FullSubcategory` `FullSubcategory.category` `CategoryTheory.Preadditive.fullSubcategory` `instHasZeroObjectFullSubcategoryOfContainsZero` `IsTriangulated.toContainsZero` `hasShift` `Int.instAddMonoid` `IsTriangulated.toIsStableUnderShift` `instAdditiveFullSubcategoryShiftFunctor` `instPretriangulatedFullSubcategory` `tStructure` `FullSubcategory.obj`	—	`instHasZeroObjectFullSubcategoryOfContainsZero` `IsTriangulated.toContainsZero` `IsTriangulated.toIsStableUnderShift` `instAdditiveFullSubcategoryShiftFunctor` `CategoryTheory.Triangulated.TStructure.IsLE.le`

CategoryTheory.ObjectProperty.HasInducedTStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_triangle_zero_one` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Triangulated.TStructure.IsLE` `CategoryTheory.Triangulated.TStructure.IsGE` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `CategoryTheory.ObjectProperty.isoClosure`	—	—
`mk'` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Functor.obj` `CategoryTheory.Triangulated.TStructure.truncLE` `CategoryTheory.Triangulated.TStructure.truncGE`	`CategoryTheory.ObjectProperty.HasInducedTStructure`	—	`CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE` `CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE` `CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished` `CategoryTheory.ObjectProperty.le_isoClosure`

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
`onBounded` 📖	CompOp	—
`onMinus` 📖	CompOp	—
`onPlus` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasInducedTStructureBounded` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.ObjectProperty.HasInducedTStructure` `bounded` `instIsTriangulatedBounded`	—	`instIsTriangulatedBounded` `CategoryTheory.ObjectProperty.instHasInducedTStructureMinOfIsClosedUnderIsomorphisms` `instIsTriangulatedPlus` `instIsTriangulatedMinus` `instHasInducedTStructurePlus` `instHasInducedTStructureMinus` `instIsClosedUnderIsomorphismsPlus` `instIsClosedUnderIsomorphismsMinus`
`instHasInducedTStructureMinus` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.ObjectProperty.HasInducedTStructure` `minus` `instIsTriangulatedMinus`	—	`CategoryTheory.ObjectProperty.HasInducedTStructure.mk'` `instIsTriangulatedMinus` `instIsLEObjTruncLE_1` `instIsLEObjTruncGE`
`instHasInducedTStructurePlus` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.ObjectProperty.HasInducedTStructure` `plus` `instIsTriangulatedPlus`	—	`CategoryTheory.ObjectProperty.HasInducedTStructure.mk'` `instIsTriangulatedPlus` `instIsGEObjTruncLE_1` `instIsGEObjTruncGE_1`

---

← Back to Index