Commit 2021-03-26 08:06 5c93c2d0

View on Github →

feat(category_theory/triangulated/rotate): add definition of rotation and inverse rotation of triangles and their morphisms (#6803) This PR adds the definition of rotation and inverse rotation of triangles and triangle morphisms. It also shows that rotation is an equivalence on the category of triangles in an additive category.

Estimated changes

Modified src/category_theory/triangulated/basic.lean

added def category_theory.triangulated.contractible_triangle

Created src/category_theory/triangulated/rotate.lean

added def category_theory.triangulated.inv_rot_comp_rot

added def category_theory.triangulated.inv_rot_comp_rot_hom

added def category_theory.triangulated.inv_rot_comp_rot_inv

added def category_theory.triangulated.inv_rotate

added def category_theory.triangulated.rot_comp_inv_rot

added def category_theory.triangulated.rot_comp_inv_rot_hom

added def category_theory.triangulated.rot_comp_inv_rot_inv

added def category_theory.triangulated.rotate

added def category_theory.triangulated.triangle.inv_rotate

added def category_theory.triangulated.triangle.rotate

added def category_theory.triangulated.triangle_morphism.inv_rotate

added def category_theory.triangulated.triangle_morphism.rotate

added def category_theory.triangulated.triangle_rotation