Commit 2024-12-29 10:18 e785d99a

View on Github →

chore(CategoryTheory/Pretriangulated/Opposite): split CategoryTheory.Triangulated.Opposite into three files (#20316) This splits the long (and getting longer with a new PR) file CatgeoryTheory.Triangulated.Opposite in three files:

Triangulated.Opposite.Basic: just the shift on the opposite category + lemmas
Triangulated.Opposite.Triangle: the equivalence triangleOpEquivalence
Triangulated.Opposite.Pretriangulated: the pretriangulated structure

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean

Modified Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean

Renamed Mathlib/CategoryTheory/Triangulated/Opposite.lean to Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean

deleted theorem CategoryTheory.Functor.map_distinguished_op_exact

deleted theorem CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism

deleted theorem CategoryTheory.Pretriangulated.Opposite.contractible_distinguished

deleted def CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles

deleted theorem CategoryTheory.Pretriangulated.Opposite.distinguished_cocone_triangle

deleted theorem CategoryTheory.Pretriangulated.Opposite.isomorphic_distinguished

deleted theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff'

deleted theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff

deleted theorem CategoryTheory.Pretriangulated.Opposite.rotate_distinguished_triangle

deleted theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff'

deleted theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff

deleted theorem CategoryTheory.Pretriangulated.op_distinguished

deleted theorem CategoryTheory.Pretriangulated.unop_distinguished

Created Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean

added theorem CategoryTheory.Functor.map_distinguished_op_exact

added theorem CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism

added theorem CategoryTheory.Pretriangulated.Opposite.contractible_distinguished

added def CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles

added theorem CategoryTheory.Pretriangulated.Opposite.distinguished_cocone_triangle

added theorem CategoryTheory.Pretriangulated.Opposite.isomorphic_distinguished

added theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff'

added theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff

added theorem CategoryTheory.Pretriangulated.Opposite.rotate_distinguished_triangle

added theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff'

added theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff

added theorem CategoryTheory.Pretriangulated.op_distinguished

added theorem CategoryTheory.Pretriangulated.unop_distinguished

Created Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean

Modified Mathlib/CategoryTheory/Triangulated/Yoneda.lean