Commit 2023-10-20 13:51 6f69c1ac

View on Github →

feat: the pretriangulated structure on the opposite category (#7336)

Estimated changes

Modified Mathlib/CategoryTheory/Opposites.lean

added theorem CategoryTheory.Iso.unop_hom_inv_id_app

added theorem CategoryTheory.Iso.unop_inv_hom_id_app

Modified Mathlib/CategoryTheory/Preadditive/Basic.lean

added theorem CategoryTheory.Preadditive.neg_iso_hom

added theorem CategoryTheory.Preadditive.neg_iso_inv

added theorem CategoryTheory.Preadditive.smul_iso_hom

added theorem CategoryTheory.Preadditive.smul_iso_inv

Modified Mathlib/CategoryTheory/Triangulated/Opposite.lean

added theorem CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism

added theorem CategoryTheory.Pretriangulated.Opposite.contractible_distinguished

added theorem CategoryTheory.Pretriangulated.Opposite.distinguished_cocone_triangle

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.opShiftFunctorEquivalence_counitIso_hom_naturality

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality

added theorem CategoryTheory.Pretriangulated.op_distinguished

added theorem CategoryTheory.Pretriangulated.unop_distinguished