Basic

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

Statistics

Metric	Count
Definitions IsGE, IsLE, bounded, ge, le, minus, plus	7
Theorems ge, le, exists_triangle, exists_triangle_zero_one, ge_antitone, ge_iff_isGE, ge_isClosedUnderIsomorphisms, ge_of_isGE, ge_one_le, ge_shift, instIsClosedUnderIsomorphismsBounded, instIsClosedUnderIsomorphismsGe, instIsClosedUnderIsomorphismsLe, instIsClosedUnderIsomorphismsMinus, instIsClosedUnderIsomorphismsPlus, instIsStableUnderShiftBoundedInt, instIsStableUnderShiftMinusInt, instIsStableUnderShiftPlusInt, isGE_of_GE, isGE_of_ge, isGE_of_iso, isGE_of_shift, isGE_shift, isGE_shift_iff, isLE_of_LE, isLE_of_iso, isLE_of_le, isLE_of_shift, isLE_shift, isLE_shift_iff, isZero, le_iff_isLE, le_isClosedUnderIsomorphisms, le_monotone, le_of_isLE, le_shift, le_zero_le, shift_ge, shift_le, zero, zero', zero_of_isLE_of_isGE	42
Total	49

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
IsGE 📖	CompData	39 math math: instIsGEOfNat, CategoryTheory.ObjectProperty.tStructure_isGE_iff, isGE_truncGE_obj, instIsGEObjTruncGE_1, isGE_iff_isIso_truncGTπ_app, isGE_of_iso, isGE_shift_iff, isIso_truncLT_map_iff, instIsGEObjTruncLE_1, instIsGEObjEIntFunctorETruncGE, instIsGEObjTruncLT, instIsGEObj₃ObjTriangleTriangleLTGE, isGE₂, instIsGEObjTruncLE, instIsGEObjTruncGTHSubIntOfNat, CategoryTheory.ObjectProperty.hasInducedTStructure_iff, isGE_iff_isZero_truncLE_obj, isGE_iff_orthogonal, isGE_iff_isIso_truncGEπ_app, isGE_of_GE, instIsGEObjTruncGE, isGE_iff_isZero_truncLT_obj, isGE_of_isZero, isIso_truncLE_map_iff, instIsGEObjTruncGT, mem_heart_iff, CategoryTheory.ObjectProperty.HasInducedTStructure.exists_triangle_zero_one, ge_iff_isGE, isGE_shift, instIsGEObjEIntFunctorETruncLT, isGE_truncGT_obj, isGE_eTruncGE_obj_obj, instIsGEObjTruncGTHAddIntOfNat, instIsGEObjTruncLTGE, instIsGEObjιHeartOfNatInt, isGE_of_ge, instIsGEObjTruncGELT, isGE_of_shift, instIsGEObjTruncGELE
IsLE 📖	CompData	38 math math: instIsLEOfNat, isLE_iff_isZero_truncGE_obj, instIsLEObjTruncGELE, instIsLEObjTruncGT, instIsLEObjTruncLTHSubIntOfNat, isLE_of_LE, isLE_iff_isIso_truncLEι_app, instIsLEObjTruncLE_1, instIsLEObjTruncLT, isLE_shift_iff, isLE_iff_isZero_truncGT_obj, isLE_shift, isLE_truncLT_obj, instIsLEObjTruncLTGEHSubIntOfNat, instIsLEObjTruncGE, CategoryTheory.ObjectProperty.hasInducedTStructure_iff, isLE_of_isZero, instIsLEObjTruncGELTHSubIntOfNat, isLE₂, CategoryTheory.ObjectProperty.tStructure_isLE_iff, isIso_truncGT_map_iff, isLE_of_iso, instIsLEObjTruncLE, isLE_eTruncLT_obj_obj, isLE_of_le, instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, mem_heart_iff, CategoryTheory.ObjectProperty.HasInducedTStructure.exists_triangle_zero_one, isLE_iff_isIso_truncLTι_app, instIsLEObjEIntFunctorETruncGE, isLE_of_shift, isLE_truncLE_obj, le_iff_isLE, instIsLEObjEIntFunctorETruncLT, isLE_iff_orthogonal, instIsLEObjιHeartOfNatInt, instIsLEObjTruncLTHAddIntOfNat, isIso_truncGE_map_iff
bounded 📖	CompOp	4 math math: instHasInducedTStructureBounded, instIsStableUnderShiftBoundedInt, instIsClosedUnderIsomorphismsBounded, instIsTriangulatedBounded
ge 📖	CompOp	11 math math: exists_triangle, ge_isClosedUnderIsomorphisms, shift_ge, exists_triangle_zero_one, instIsClosedUnderIsomorphismsGe, ge_of_isGE, ge_antitone, IsGE.ge, ge_iff_isGE, ge_shift, ge_one_le
le 📖	CompOp	11 math math: le_of_isLE, le_monotone, exists_triangle, shift_le, le_shift, IsLE.le, exists_triangle_zero_one, instIsClosedUnderIsomorphismsLe, le_zero_le, le_isClosedUnderIsomorphisms, le_iff_isLE
minus 📖	CompOp	4 math math: instIsClosedUnderIsomorphismsMinus, instHasInducedTStructureMinus, instIsStableUnderShiftMinusInt, instIsTriangulatedMinus
plus 📖	CompOp	4 math math: instIsClosedUnderIsomorphismsPlus, instIsStableUnderShiftPlusInt, instHasInducedTStructurePlus, instIsTriangulatedPlus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_triangle 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	le ge Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	—	exists_triangle_zero_one CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Pretriangulated.Triangle.shift_distinguished Int.negOnePow_neg CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id le_shift neg_add_cancel ge_shift
exists_triangle_zero_one 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	le ge Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	—	—
ge_antitone 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Antitone CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Pi.preorder Prop.partialOrder ge	—	Nat.cast_zero add_zero le_refl shift_ge ge_one_le CategoryTheory.ObjectProperty.prop_shift_iff Nat.cast_one Nat.cast_add add_assoc LE.le.trans
ge_iff_isGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	ge IsGE	—	ge_of_isGE
ge_isClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms ge	—	—
ge_of_isGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	ge	—	IsGE.ge
ge_one_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le ge	—	—
ge_shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid ge	ge CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid	—	—
instIsClosedUnderIsomorphismsBounded 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms bounded	—	CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMin instIsClosedUnderIsomorphismsPlus instIsClosedUnderIsomorphismsMinus
instIsClosedUnderIsomorphismsGe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms ge	—	isGE_of_iso
instIsClosedUnderIsomorphismsLe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms le	—	isLE_of_iso
instIsClosedUnderIsomorphismsMinus 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms minus	—	isLE_of_iso
instIsClosedUnderIsomorphismsPlus 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms plus	—	isGE_of_iso
instIsStableUnderShiftBoundedInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsStableUnderShift bounded Int.instAddMonoid	—	CategoryTheory.ObjectProperty.instIsStableUnderShiftMin instIsStableUnderShiftPlusInt instIsStableUnderShiftMinusInt
instIsStableUnderShiftMinusInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsStableUnderShift minus Int.instAddMonoid	—	isLE_shift
instIsStableUnderShiftPlusInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsStableUnderShift plus Int.instAddMonoid	—	isGE_shift
isGE_of_GE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE	—	isGE_of_ge
isGE_of_ge 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE	—	ge_antitone ge_of_isGE
isGE_of_iso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE	—	CategoryTheory.ObjectProperty.prop_of_iso ge_isClosedUnderIsomorphisms ge_of_isGE
isGE_of_shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE	—	isGE_shift isGE_of_iso
isGE_shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid	—	ge_shift ge_of_isGE
isGE_shift_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid	—	isGE_of_shift isGE_shift
isLE_of_LE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE	—	isLE_of_le
isLE_of_iso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE	—	CategoryTheory.ObjectProperty.prop_of_iso le_isClosedUnderIsomorphisms le_of_isLE
isLE_of_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE	—	le_monotone le_of_isLE
isLE_of_shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE	—	isLE_shift isLE_of_iso
isLE_shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid	—	le_shift le_of_isLE
isLE_shift_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid	—	isLE_of_shift isLE_shift
isZero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.IsZero	—	CategoryTheory.Limits.IsZero.iff_id_eq_zero zero
le_iff_isLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	le IsLE	—	le_of_isLE
le_isClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms le	—	—
le_monotone 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Monotone CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Pi.preorder Prop.partialOrder le	—	Nat.cast_zero add_zero le_refl shift_le CategoryTheory.ObjectProperty.prop_shift_iff le_zero_le Nat.cast_add add_assoc LE.le.trans
le_of_isLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	le	—	IsLE.le
le_shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid le	le CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid	—	—
le_zero_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le le	—	—
shift_ge 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.shift ge Int.instAddMonoid	—	CategoryTheory.ObjectProperty.prop_iff_of_iso ge_isClosedUnderIsomorphisms ge_shift
shift_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.shift le Int.instAddMonoid	—	CategoryTheory.ObjectProperty.prop_iff_of_iso le_isClosedUnderIsomorphisms le_shift
zero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	isLE_shift add_zero isGE_shift isGE_of_ge CategoryTheory.Functor.map_injective CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive zero' le_of_isLE ge_of_isGE
zero' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid le ge	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
zero_of_isLE_of_isGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	zero

CategoryTheory.Triangulated.TStructure.IsGE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ge 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Triangulated.TStructure.ge	—	—

CategoryTheory.Triangulated.TStructure.IsLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Triangulated.TStructure.le	—	—

---

← Back to Index