TruncLTGE

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

Statistics

Metric	Count
Definitions triangleLTGE, truncGE, truncGEδLT, truncGEπ, truncLT, truncLTι	6
Theorems instAdditiveTruncGE, instAdditiveTruncLT, instIsGEObjTruncGE, instIsGEObj₃ObjTriangleTriangleLTGE, instIsLEObjTruncLTHSubIntOfNat, instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, triangleLTGE_distinguished, triangleLTGE_map_hom₁, triangleLTGE_map_hom₂, triangleLTGE_map_hom₃, triangleLTGE_obj_mor₁, triangleLTGE_obj_mor₂, triangleLTGE_obj_mor₃, triangleLTGE_obj_obj₁, triangleLTGE_obj_obj₂, triangleLTGE_obj_obj₃, triangle_iso_exists, triangle_map_exists, triangle_map_ext	19
Total	25

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
triangleLTGE 📖	CompOp	12 math math: triangleLTGE_obj_mor₁, triangleLTGE_obj_obj₃, instIsGEObj₃ObjTriangleTriangleLTGE, triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, triangleLTGE_obj_obj₁, instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, triangleLTGE_distinguished, triangleLTGE_obj_mor₂, triangleLTGE_map_hom₁, triangleLTGE_obj_obj₂
truncGE 📖	CompOp	8 math math: triangleLTGE_obj_obj₃, triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, instIsGEObjTruncGE, instAdditiveTruncGE, triangleLTGE_obj_mor₂, triangleLTGE_map_hom₁
truncGEδLT 📖	CompOp	4 math math: triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, triangleLTGE_map_hom₁
truncGEπ 📖	CompOp	4 math math: triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₂, triangleLTGE_map_hom₁
truncLT 📖	CompOp	8 math math: instIsLEObjTruncLTHSubIntOfNat, triangleLTGE_obj_mor₁, triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, triangleLTGE_obj_obj₁, triangleLTGE_map_hom₁, instAdditiveTruncLT
truncLTι 📖	CompOp	4 math math: triangleLTGE_obj_mor₁, triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_map_hom₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveTruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	truncGE	—	CategoryTheory.Functor.map_add
instAdditiveTruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	truncLT	—	CategoryTheory.Functor.map_add
instIsGEObjTruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGE	—	—
instIsGEObj₃ObjTriangleTriangleLTGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	instIsGEObjTruncGE
instIsLEObjTruncLTHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLT	—	—
instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	instIsLEObjTruncLTHSubIntOfNat
triangleLTGE_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ CategoryTheory.Functor.comp truncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ CategoryTheory.Functor.comp truncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ CategoryTheory.Functor.comp truncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE CategoryTheory.NatTrans.app truncLT CategoryTheory.Functor.id truncLTι	—	—
triangleLTGE_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGE truncGEπ	—	—
triangleLTGE_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE CategoryTheory.NatTrans.app truncGE CategoryTheory.Functor.comp truncLT truncGEδLT	—	—
triangleLTGE_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE truncLT	—	—
triangleLTGE_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE truncGE	—	—
triangle_iso_exists 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Triangle.obj₂	—	triangle_map_exists triangle_map_ext CategoryTheory.Iso.hom_inv_id CategoryTheory.Iso.inv_hom_id
triangle_map_exists 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂	—	CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ zero CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism
triangle_map_ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂	—	—	CategoryTheory.Pretriangulated.Triangle.hom_ext CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Limits.comp_zero add_neg_cancel zero_of_isLE_of_isGE isGE_shift CategoryTheory.Preadditive.comp_neg CategoryTheory.Limits.zero_comp neg_zero CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ isLE_shift sub_eq_zero sub_self

---

← Back to Index