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_isClosedUnderIsomorphisms, ge_of_isGE, ge_one_le, ge_shift, instIsClosedUnderIsomorphismsBounded, 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_isClosedUnderIsomorphisms, le_monotone, le_of_isLE, le_shift, le_zero_le, shift_ge, shift_le, zero, zero', zero_of_isLE_of_isGE	38
Total	45

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
IsGE 📖	CompData	8 math math: isGE_of_iso, isGE_shift_iff, instIsGEObj₃ObjTriangleTriangleLTGE, isGE_of_GE, instIsGEObjTruncGE, isGE_shift, isGE_of_ge, isGE_of_shift
IsLE 📖	CompData	8 math math: instIsLEObjTruncLTHSubIntOfNat, isLE_of_LE, isLE_shift_iff, isLE_shift, isLE_of_iso, isLE_of_le, instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, isLE_of_shift
bounded 📖	CompOp	2 math math: instIsStableUnderShiftBoundedInt, instIsClosedUnderIsomorphismsBounded
ge 📖	CompOp	6 math math: ge_isClosedUnderIsomorphisms, shift_ge, ge_of_isGE, ge_antitone, IsGE.ge, ge_one_le
le 📖	CompOp	6 math math: le_of_isLE, le_monotone, shift_le, IsLE.le, le_zero_le, le_isClosedUnderIsomorphisms
minus 📖	CompOp	2 math math: instIsClosedUnderIsomorphismsMinus, instIsStableUnderShiftMinusInt
plus 📖	CompOp	2 math math: instIsClosedUnderIsomorphismsPlus, instIsStableUnderShiftPlusInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_triangle 📖	mathematical	CategoryTheory.Functor.Additive 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.Linear.units_smul_comp CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Linear.comp_units_smul 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	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_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	CategoryTheory.Functor.obj	—	—
instIsClosedUnderIsomorphismsBounded 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms bounded	—	CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMin instIsClosedUnderIsomorphismsPlus instIsClosedUnderIsomorphismsMinus
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	—	CategoryTheory.ObjectProperty.instIsStableUnderShiftMin instIsStableUnderShiftPlusInt instIsStableUnderShiftMinusInt
instIsStableUnderShiftMinusInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsStableUnderShift minus	—	isLE_shift
instIsStableUnderShiftPlusInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsStableUnderShift plus	—	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	—	ge_shift ge_of_isGE
isGE_shift_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj	—	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	—	le_shift le_of_isLE
isLE_shift_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj	—	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_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	CategoryTheory.Functor.obj	—	—
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	—	CategoryTheory.ObjectProperty.prop_iff_of_iso ge_isClosedUnderIsomorphisms ge_shift
shift_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.shift le	—	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