Documentation

Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Triangles in the opposite category of a (pre)triangulated category #

Let C be a (pre)triangulated category. In CategoryTheory.Triangulated.Opposite.Basic, we have constructed a shift on Cᵒᵖ that will be part of a structure of (pre)triangulated category. In this file, we construct an equivalence of categories between (Triangle C)ᵒᵖ and Triangle Cᵒᵖ, called CategoryTheory.Pretriangulated.triangleOpEquivalence. It sends a triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ in C to the triangle op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧ in Cᵒᵖ (without introducing signs).

References #

source
noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)

The functor which sends a triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ in C to the triangle op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧ in Cᵒᵖ (without introducing signs).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) :
    ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₂ = φ.unop.hom₂.op
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) :
    ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₃ = φ.unop.hom₁.op
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (T : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ) :
    (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).obj T = CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop T).mor₂.op (Opposite.unop T).mor₁.op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T).obj₁)) ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop T).mor₃.op))
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) :
    ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₁ = φ.unop.hom₃.op
    source
    noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
    CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ

    The functor which sends a triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ in Cᵒᵖ to the triangle Z.unop ⟶ Y.unop ⟶ X.unop ⟶ Z.unop⟦1⟧ in C (without introducing signs).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
      (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).obj T = Opposite.op (CategoryTheory.Pretriangulated.Triangle.mk T.mor₂.unop T.mor₁.unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop ((CategoryTheory.shiftFunctor C 1).map T.mor₃.unop)))
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ} (φ : T₁ ⟶ T₂) :
      (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).map φ = Quiver.Hom.op { hom₁ := φ.hom₃.unop, hom₂ := φ.hom₂.unop, hom₃ := φ.hom₁.unop, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
      source
      noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
      CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ ≅ (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).comp (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C)

      The unit isomorphism of the equivalence triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ .

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ) :
        (CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).inv.app X = ((Opposite.unop X).homMk (CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op
        source
        @[simp]
        theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ) :
        (CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).hom.app X = ((CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))).homMk (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op
        source
        noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
        (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).comp (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C) ≅ CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)

        The counit isomorphism of the equivalence triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ .

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
          ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
          ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
          ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
          ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
          ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) :
          ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
          source
          noncomputable def CategoryTheory.Pretriangulated.triangleOpEquivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
          (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ ≌ CategoryTheory.Pretriangulated.Triangle Cᵒᵖ

          An anti-equivalence between the categories of triangles in C and in Cᵒᵖ. A triangle in Cᵒᵖ shall be distinguished iff it correspond to a distinguished triangle in C via this equivalence.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
            (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor = CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_counitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
            (CategoryTheory.Pretriangulated.triangleOpEquivalence C).counitIso = CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_unitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
            (CategoryTheory.Pretriangulated.triangleOpEquivalence C).unitIso = CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] :
            (CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse = CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C