Commit 2021-04-16 22:20 6b182fcd

View on Github →

feat(category_theory/triangulated/pretriangulated): add definition of pretriangulated categories and triangulated functors between them (#7153) Adds a definition of pretriangulated categories and triangulated functors between them.

Estimated changes

Modified src/category_theory/preadditive/additive_functor.lean

Modified src/category_theory/triangulated/basic.lean

modified def category_theory.triangulated.contractible_triangle

added def category_theory.triangulated.triangle.mk

modified structure category_theory.triangulated.triangle

Created src/category_theory/triangulated/pretriangulated.lean

added theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₁₂

added theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₂₃

added theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₃₁

added theorem category_theory.triangulated.pretriangulated.inv_rot_of_dist_triangle

added theorem category_theory.triangulated.pretriangulated.rot_of_dist_triangle

added theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_distinguished

added def category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle

added structure category_theory.triangulated.pretriangulated.triangulated_functor

added def category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle

added structure category_theory.triangulated.pretriangulated.triangulated_functor_struct

Modified src/category_theory/triangulated/rotate.lean

modified def category_theory.triangulated.inv_rot_comp_rot

modified def category_theory.triangulated.inv_rot_comp_rot_hom

modified def category_theory.triangulated.inv_rot_comp_rot_inv

modified def category_theory.triangulated.rot_comp_inv_rot

modified def category_theory.triangulated.rot_comp_inv_rot_hom

modified def category_theory.triangulated.rot_comp_inv_rot_inv

modified def category_theory.triangulated.triangle.rotate