Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-02 06:11 19786714

View on Github →

feat(category_theory/triangulated): changing namespaces, introducing triangulated categories (#17284) This PR moves the namespace category_theory.triangulated.pretriangulated to category_theory.pretriangulated, and introduces triangulated categories.

Estimated changes

Modified src/category_theory/triangulated/basic.lean

added def category_theory.pretriangulated.contractible_triangle

added def category_theory.pretriangulated.triangle.mk

added structure category_theory.pretriangulated.triangle

added def category_theory.pretriangulated.triangle_morphism.comp

added structure category_theory.pretriangulated.triangle_morphism

added def category_theory.pretriangulated.triangle_morphism_id

deleted def category_theory.triangulated.contractible_triangle

deleted def category_theory.triangulated.triangle.mk

deleted structure category_theory.triangulated.triangle

deleted def category_theory.triangulated.triangle_morphism.comp

deleted structure category_theory.triangulated.triangle_morphism

deleted def category_theory.triangulated.triangle_morphism_id

Modified src/category_theory/triangulated/pretriangulated.lean

added theorem category_theory.pretriangulated.comp_dist_triangle_mor_zero₁₂

added theorem category_theory.pretriangulated.comp_dist_triangle_mor_zero₂₃

added theorem category_theory.pretriangulated.comp_dist_triangle_mor_zero₃₁

added theorem category_theory.pretriangulated.inv_rot_of_dist_triangle

added theorem category_theory.pretriangulated.rot_of_dist_triangle

added theorem category_theory.pretriangulated.triangulated_functor.map_distinguished

added def category_theory.pretriangulated.triangulated_functor.map_triangle

added structure category_theory.pretriangulated.triangulated_functor

added def category_theory.pretriangulated.triangulated_functor_struct.id

added def category_theory.pretriangulated.triangulated_functor_struct.map_triangle

added structure category_theory.pretriangulated.triangulated_functor_struct

deleted theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₁₂

deleted theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₂₃

deleted theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₃₁

deleted theorem category_theory.triangulated.pretriangulated.inv_rot_of_dist_triangle

deleted theorem category_theory.triangulated.pretriangulated.rot_of_dist_triangle

deleted theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_distinguished

deleted def category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle

deleted structure category_theory.triangulated.pretriangulated.triangulated_functor

deleted def category_theory.triangulated.pretriangulated.triangulated_functor_struct.id

deleted def category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle

deleted structure category_theory.triangulated.pretriangulated.triangulated_functor_struct

Modified src/category_theory/triangulated/rotate.lean

added def category_theory.pretriangulated.from_inv_rotate_rotate

added def category_theory.pretriangulated.from_rotate_inv_rotate

added def category_theory.pretriangulated.inv_rot_comp_rot

added def category_theory.pretriangulated.inv_rot_comp_rot_hom

added def category_theory.pretriangulated.inv_rot_comp_rot_inv

added def category_theory.pretriangulated.inv_rotate

added def category_theory.pretriangulated.rot_comp_inv_rot

added def category_theory.pretriangulated.rot_comp_inv_rot_hom

added def category_theory.pretriangulated.rot_comp_inv_rot_inv

added def category_theory.pretriangulated.rotate

added def category_theory.pretriangulated.to_inv_rotate_rotate

added def category_theory.pretriangulated.to_rotate_inv_rotate

added def category_theory.pretriangulated.triangle.inv_rotate

added def category_theory.pretriangulated.triangle.rotate

added def category_theory.pretriangulated.triangle_morphism.inv_rotate

added def category_theory.pretriangulated.triangle_morphism.rotate

added def category_theory.pretriangulated.triangle_rotation

deleted def category_theory.triangulated.from_inv_rotate_rotate

deleted def category_theory.triangulated.from_rotate_inv_rotate

deleted def category_theory.triangulated.inv_rot_comp_rot

deleted def category_theory.triangulated.inv_rot_comp_rot_hom

deleted def category_theory.triangulated.inv_rot_comp_rot_inv

deleted def category_theory.triangulated.inv_rotate

deleted def category_theory.triangulated.rot_comp_inv_rot

deleted def category_theory.triangulated.rot_comp_inv_rot_hom

deleted def category_theory.triangulated.rot_comp_inv_rot_inv

deleted def category_theory.triangulated.rotate

deleted def category_theory.triangulated.to_inv_rotate_rotate

deleted def category_theory.triangulated.to_rotate_inv_rotate

deleted def category_theory.triangulated.triangle.inv_rotate

deleted def category_theory.triangulated.triangle.rotate

deleted def category_theory.triangulated.triangle_morphism.inv_rotate

deleted def category_theory.triangulated.triangle_morphism.rotate

deleted def category_theory.triangulated.triangle_rotation

Created src/category_theory/triangulated/triangulated.lean

added def category_theory.triangulated.octahedron.triangle

added def category_theory.triangulated.octahedron.triangle_morphism₁

added def category_theory.triangulated.octahedron.triangle_morphism₂

added structure category_theory.triangulated.octahedron

added def category_theory.triangulated.some_octahedron