Skip to content

Commit 9e508f5

Browse files
joelrioujoelriou
committed
feat(CategoryTheory): the opposite of a triangulated category is triangulated (leanprover-community#32535)
1 parent 89111f4 commit 9e508f5

File tree

6 files changed

+210
-3
lines changed

6 files changed

+210
-3
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3102,6 +3102,7 @@ public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic
31023102
public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor
31033103
public import Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
31043104
public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
3105+
public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
31053106
public import Mathlib.CategoryTheory.Triangulated.Orthogonal
31063107
public import Mathlib.CategoryTheory.Triangulated.Pretriangulated
31073108
public import Mathlib.CategoryTheory.Triangulated.Rotate

‎Mathlib/CategoryTheory/Shift/Basic.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -659,6 +659,20 @@ lemma shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app (m₁ m₂ m
659659
shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃
660660
(m₁ + m₂) (m₂ + m₃) (m₁ + (m₂ + m₃)) rfl rfl (add_assoc _ _ _) X]
661661

662+
@[reassoc]
663+
lemma shiftFunctorComm_hom_app_of_add_eq_zero (m n : A) (hmn : m + n = 0) (X : C) :
664+
(shiftFunctorComm C m n).hom.app X =
665+
(shiftFunctorCompIsoId C m n hmn).hom.app X ≫
666+
(shiftFunctorCompIsoId C n m (by rw [add_comm, hmn])).inv.app X := by
667+
simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]
668+
669+
@[reassoc]
670+
lemma shiftFunctorComm_inv_app_of_add_eq_zero (m n : A) (hmn : m + n = 0) (X : C) :
671+
(shiftFunctorComm C m n).inv.app X =
672+
(shiftFunctorCompIsoId C n m (by rw [add_comm, hmn])).hom.app X ≫
673+
(shiftFunctorCompIsoId C m n hmn).inv.app X := by
674+
simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]
675+
662676
end AddCommMonoid
663677

664678
namespace Functor.FullyFaithful

‎Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -239,6 +239,71 @@ lemma opShiftFunctorEquivalence_counitIso_hom_app_shift (X : Cᵒᵖ) (n : ℤ)
239239
((opShiftFunctorEquivalence C n).unitIso.inv.app X)⟦n⟧' :=
240240
(opShiftFunctorEquivalence C n).counit_app_functor X
241241

242+
@[reassoc]
243+
lemma shiftFunctorCompIsoId_op_hom_app (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0) :
244+
(shiftFunctorCompIsoId Cᵒᵖ n m hnm).hom.app X =
245+
((shiftFunctorOpIso C n m hnm).hom.app X)⟦m⟧' ≫
246+
(shiftFunctorOpIso C m n (by lia)).hom.app (Opposite.op (X.unop⟦m⟧)) ≫
247+
((shiftFunctorCompIsoId C m n (by lia)).inv.app X.unop).op := by
248+
simp [shiftFunctorCompIsoId, shiftFunctorZero_op_hom_app X,
249+
shiftFunctorAdd'_op_inv_app X n m 0 hnm m n 0 hnm (by lia) (add_zero 0)]
250+
251+
@[reassoc]
252+
lemma shiftFunctorCompIsoId_op_inv_app (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0) :
253+
(shiftFunctorCompIsoId Cᵒᵖ n m hnm).inv.app X =
254+
((shiftFunctorCompIsoId C m n (by omega)).hom.app X.unop).op ≫
255+
(shiftFunctorOpIso C m n (by omega)).inv.app (Opposite.op (X.unop⟦m⟧)) ≫
256+
((shiftFunctorOpIso C n m hnm).inv.app X)⟦m⟧' := by
257+
simp [shiftFunctorCompIsoId, shiftFunctorZero_op_inv_app X,
258+
shiftFunctorAdd'_op_hom_app X n m 0 hnm m n 0 hnm (by omega) (add_zero 0)]
259+
260+
@[reassoc]
261+
lemma shift_opShiftFunctorEquivalence_counitIso_inv_app (X : C) (m n : ℤ) (hmn : m + n = 0) :
262+
((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X))⟦m⟧' =
263+
(opShiftFunctorEquivalence C n).counitIso.inv.app ((Opposite.op X)⟦m⟧) ≫
264+
(((shiftFunctorOpIso C m n hmn).hom.app (Opposite.op X)).unop⟦n⟧').op⟦n⟧' ≫
265+
((shiftFunctorOpIso C m n hmn).inv.app (Opposite.op (X⟦n⟧)))⟦n⟧' ≫
266+
(shiftFunctorComm Cᵒᵖ n m).inv.app (Opposite.op (X⟦n⟧)) := by
267+
obtain rfl : m = -n := by lia
268+
dsimp [opShiftFunctorEquivalence]
269+
simp only [shiftFunctor_op_map (-n) n (by lia), shiftFunctor_op_map n (-n) (by lia),
270+
shiftFunctorComm_inv_app_of_add_eq_zero n (-n) (by lia), assoc,
271+
shiftFunctorCompIsoId_op_inv_app, shiftFunctorCompIsoId_op_hom_app,
272+
shift_shiftFunctorCompIsoId_hom_app, op_comp, unop_comp, Quiver.Hom.unop_op,
273+
Functor.map_comp, Iso.inv_hom_id_app_assoc, Functor.op_obj]
274+
apply Quiver.Hom.unop_inj
275+
dsimp
276+
simp only [Category.assoc, ← Functor.map_comp_assoc, Iso.unop_hom_inv_id_app_assoc]
277+
congr 3
278+
exact (NatIso.naturality_1 (shiftFunctorCompIsoId C n (-n) (by lia)) _).symm
279+
280+
/-- Given objects `X` and `Y` in `Cᵒᵖ`, this is the bijection
281+
`(op (X.unop⟦n⟧) ⟶ Y) ≃ (X ⟶ Y⟦n⟧)` for any `n : ℤ`. -/
282+
noncomputable def opShiftFunctorEquivalenceSymmHomEquiv {n : ℤ} {X Y : Cᵒᵖ} :
283+
(Opposite.op (X.unop⟦n⟧) ⟶ Y) ≃ (X ⟶ Y⟦n⟧) :=
284+
(opShiftFunctorEquivalence C n).symm.toAdjunction.homEquiv X Y
285+
286+
@[reassoc]
287+
lemma opShiftFunctorEquivalenceSymmHomEquiv_apply {n : ℤ} {X Y : Cᵒᵖ}
288+
(f : Opposite.op (X.unop⟦n⟧) ⟶ Y) :
289+
opShiftFunctorEquivalenceSymmHomEquiv f =
290+
(opShiftFunctorEquivalence C n).counitIso.inv.app X ≫ (shiftFunctor Cᵒᵖ n).map f := rfl
291+
292+
@[reassoc]
293+
lemma opShiftFunctorEquivalenceSymmHomEquiv_left_inv
294+
{n : ℤ} {X Y : Cᵒᵖ} (f : Opposite.op (X.unop⟦n⟧) ⟶ Y) :
295+
((opShiftFunctorEquivalence C n).unitIso.inv.app Y).unop ≫
296+
(opShiftFunctorEquivalenceSymmHomEquiv f).unop⟦n⟧' = f.unop :=
297+
Quiver.Hom.op_inj (opShiftFunctorEquivalenceSymmHomEquiv.left_inv f)
298+
299+
@[reassoc]
300+
lemma shift_opShiftFunctorEquivalenceSymmHomEquiv_unop
301+
{n : ℤ} {X Y : Cᵒᵖ} (f : Opposite.op (X.unop⟦n⟧) ⟶ Y) :
302+
(opShiftFunctorEquivalenceSymmHomEquiv f).unop⟦n⟧' =
303+
((opShiftFunctorEquivalence C n).unitIso.hom.app Y).unop ≫ f.unop := by
304+
rw [← opShiftFunctorEquivalenceSymmHomEquiv_left_inv]
305+
simp
306+
242307
end Pretriangulated
243308

244309
end CategoryTheory

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@ public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
99
public import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
1010

1111
/-!
12-
# The (pre)triangulated structure on the opposite category
12+
# The pretriangulated structure on the opposite category
1313
14-
In this file, we shall construct the (pre)triangulated structure
15-
on the opposite category `Cᵒᵖ` of a (pre)triangulated category `C`.
14+
In this file, we construct the pretriangulated structure
15+
on the opposite category `Cᵒᵖ` of a pretriangulated category `C`.
1616
1717
The shift on `Cᵒᵖ` was constructed in `Mathlib.CategoryTheory.Triangulated.Opposite.Basic`,
1818
and is such that shifting by `n : ℤ` on `Cᵒᵖ` corresponds to the shift by
@@ -28,6 +28,9 @@ shall be a distinguished triangle in `Cᵒᵖ`. This is equivalent to the defini
2828
in [Verdiers's thesis, p. 96][verdier1996] which would require that the triangle
2929
`(op X)⟦-1⟧ ⟶ op Z ⟶ op Y ⟶ op X` (without signs) is *antidistinguished*.
3030
31+
In the file `Mathlib.Triangulated.Opposite.Triangulated`, we show that `Cᵒᵖ` is
32+
triangulated if `C` is triangulated.
33+
3134
## References
3235
* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996]
3336

‎Mathlib/CategoryTheory/Triangulated/Opposite/Triangulated.lean‎

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
/-
2+
Copyright (c) 2023 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
9+
10+
/-!
11+
# The opposite of a triangulated category is triangulated
12+
13+
The pretriangulated structure on `Cᵒᵖ` was constructed in the file
14+
`CategoryTheory.Triangulated.Opposite.Pretriangulated`. Here, we show
15+
that `Cᵒᵖ` is triangulated if `C` is triangulated.
16+
17+
## References
18+
* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996]
19+
20+
-/
21+
22+
@[expose] public section
23+
24+
namespace CategoryTheory
25+
26+
open Preadditive Limits
27+
28+
namespace Pretriangulated
29+
30+
variable (C : Type*) [Category C] [HasShift C ℤ] [HasZeroObject C] [Preadditive C]
31+
[∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C]
32+
33+
namespace Opposite
34+
35+
scoped instance [IsTriangulated C] : IsTriangulated Cᵒᵖ := by
36+
have : ∀ ⦃X₁ X₂ X₃ : C⦄ (u₁₂ : X₁ ⟶ X₂) (u₂₃ : X₂ ⟶ X₃),
37+
∃ (Z₁₂ Z₂₃ Z₁₃ : C)
38+
(v₁₂ : Z₁₂ ⟶ X₁) (w₁₂ : X₂ ⟶ Z₁₂⟦(1 : ℤ)⟧) (h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distTriang C)
39+
(v₂₃ : Z₂₃ ⟶ X₂) (w₂₃ : X₃ ⟶ Z₂₃⟦(1 : ℤ)⟧) (h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distTriang C)
40+
(v₁₃ : Z₁₃ ⟶ X₁) (w₁₃ : X₃ ⟶ Z₁₃⟦(1 : ℤ)⟧)
41+
(h₁₃ : Triangle.mk v₁₃ (u₁₂ ≫ u₂₃) w₁₃ ∈ distTriang C),
42+
Nonempty (Triangulated.Octahedron rfl (rot_of_distTriang _ h₁₂)
43+
(rot_of_distTriang _ h₂₃) (rot_of_distTriang _ h₁₃)) := by
44+
intro X₁ X₂ X₃ u₁₂ u₂₃
45+
obtain ⟨Z₁₂, v₁₂, w₁₂, h₁₂⟩ := distinguished_cocone_triangle₁ u₁₂
46+
obtain ⟨Z₂₃, v₂₃, w₂₃, h₂₃⟩ := distinguished_cocone_triangle₁ u₂₃
47+
obtain ⟨Z₁₃, v₁₃, w₁₃, h₁₃⟩ := distinguished_cocone_triangle₁ (u₁₂ ≫ u₂₃)
48+
exact ⟨_, _, _, _, _, h₁₂, _, _, h₂₃, _, _, h₁₃, ⟨Triangulated.someOctahedron _ _ _ _⟩⟩
49+
refine IsTriangulated.mk' (fun X₁ X₂ X₃ u₁₂ u₂₃ ↦ ?_)
50+
obtain ⟨Z₁₂, Z₂₃, Z₁₃, v₁₂, w₁₂, h₁₂, v₂₃, w₂₃, h₂₃, v₁₃, w₁₃, h₁₃, ⟨H⟩⟩ :=
51+
this u₂₃.unop u₁₂.unop
52+
refine ⟨X₁, X₂, X₃, _, _, _, u₁₂, u₂₃, Iso.refl _, Iso.refl _, Iso.refl _, by simp, by simp,
53+
v₂₃.op, opShiftFunctorEquivalenceSymmHomEquiv w₂₃.op, ?_,
54+
v₁₂.op, opShiftFunctorEquivalenceSymmHomEquiv w₁₂.op, ?_,
55+
v₁₃.op, opShiftFunctorEquivalenceSymmHomEquiv w₁₃.op, ?_, ?_⟩
56+
· rw [mem_distTriang_op_iff]
57+
refine Pretriangulated.isomorphic_distinguished _ h₂₃ _ ?_
58+
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_
59+
simpa using opShiftFunctorEquivalenceSymmHomEquiv_left_inv w₂₃.op
60+
· rw [mem_distTriang_op_iff]
61+
refine Pretriangulated.isomorphic_distinguished _ h₁₂ _ ?_
62+
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_
63+
simpa using opShiftFunctorEquivalenceSymmHomEquiv_left_inv w₁₂.op
64+
· rw [mem_distTriang_op_iff]
65+
refine Pretriangulated.isomorphic_distinguished _ h₁₃ _ ?_
66+
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_
67+
simpa using opShiftFunctorEquivalenceSymmHomEquiv_left_inv w₁₃.op
68+
· obtain ⟨m₁, hm₁⟩ := (shiftFunctor C (1 : ℤ)).map_surjective H.m₃
69+
obtain ⟨m₃, hm₃⟩ := (shiftFunctor C (1 : ℤ)).map_surjective H.m₁
70+
exact ⟨{
71+
m₁ := m₁.op
72+
m₃ := m₃.op
73+
comm₁ := Quiver.Hom.unop_inj ((shiftFunctor C (1 : ℤ)).map_injective (by
74+
simpa [hm₁] using H.comm₄.symm))
75+
comm₂ := Quiver.Hom.unop_inj ((shiftFunctor C (1 : ℤ)).map_injective (by
76+
have := H.comm₃
77+
dsimp at this ⊢
78+
rw [← hm₁] at this
79+
rw [Functor.map_comp, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc,
80+
shift_opShiftFunctorEquivalenceSymmHomEquiv_unop,
81+
Quiver.Hom.unop_op, Quiver.Hom.unop_op, this]))
82+
comm₃ := Quiver.Hom.unop_inj ((shiftFunctor C (1 : ℤ)).map_injective (by
83+
simpa [hm₃] using H.comm₂))
84+
comm₄ := Quiver.Hom.unop_inj ((shiftFunctor C (1 : ℤ)).map_injective (by
85+
have := H.comm₁
86+
rw [← hm₃] at this
87+
dsimp at this ⊢
88+
rw [Functor.map_comp, Functor.map_comp,
89+
shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc,
90+
shift_opShiftFunctorEquivalenceSymmHomEquiv_unop,
91+
Quiver.Hom.unop_op, Quiver.Hom.unop_op, this,
92+
← unop_comp_assoc, opShiftFunctorEquivalence_unitIso_hom_naturality,
93+
unop_comp_assoc, Quiver.Hom.unop_op]))
94+
mem := by
95+
rw [← Triangle.shift_distinguished_iff _ (-1), mem_distTriang_op_iff']
96+
refine ⟨_, H.mem, ⟨Triangle.isoMk _ _
97+
((shiftFunctorOpIso C _ _ (neg_add_cancel 1)).app _)
98+
(-((shiftFunctorOpIso C _ _ (neg_add_cancel 1)).app _))
99+
((shiftFunctorOpIso C _ _ (neg_add_cancel 1)).app _)
100+
(by simp [← hm₁]) (by simp [← hm₃]) ?_⟩⟩
101+
have h₁ := (shiftFunctorComm Cᵒᵖ 1 (-1)).hom.naturality v₂₃.op
102+
have h₂ := (shiftFunctorComm Cᵒᵖ 1 (-1)).hom.naturality w₁₂.op
103+
dsimp at h₁ h₂ ⊢
104+
simp only [Int.negOnePow_neg, Int.negOnePow_one, Functor.map_comp, Category.assoc,
105+
Units.neg_smul, one_smul, neg_comp, Functor.map_neg, comp_neg, neg_inj]
106+
rw [reassoc_of% h₁, shiftFunctor_op_map _ _ (neg_add_cancel 1) v₂₃.op,
107+
← Functor.map_comp, Category.assoc, Category.assoc, Iso.inv_hom_id_app,
108+
Functor.map_comp, opShiftFunctorEquivalenceSymmHomEquiv_apply,
109+
Functor.map_comp_assoc, reassoc_of% h₂,
110+
shift_opShiftFunctorEquivalence_counitIso_inv_app _ _ _ (neg_add_cancel 1)]
111+
simp [← Functor.map_comp]}⟩
112+
113+
end Opposite
114+
115+
end Pretriangulated
116+
117+
end CategoryTheory

‎Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -403,6 +403,13 @@ lemma shift_distinguished (n : ℤ) :
403403
| zero => exact H_neg_one
404404
| succ n hn => exact H_add hn H_neg_one rfl
405405

406+
omit hT in
407+
lemma shift_distinguished_iff (n : ℤ) :
408+
(CategoryTheory.shiftFunctor (Triangle C) n).obj T ∈ (distTriang C) ↔ T ∈ distTriang C :=
409+
⟨fun hT ↦ isomorphic_distinguished _ (shift_distinguished _ hT (-n)) _
410+
((shiftEquiv (Triangle C) n).unitIso.app T),
411+
fun hT ↦ shift_distinguished T hT n⟩
412+
406413
end Triangle
407414

408415
instance : SplitEpiCategory C where

0 commit comments

Comments
 (0)