add Octahedron₁

Author: justus-springer

Mathlib/CategoryTheory/Shift/Basic.lean

@@ -438,6 +438,18 @@ abbrev shiftNegShift (i : A) : X⟦-i⟧⟦i⟧ ≅ X :=
 
 variable {X Y}
 
+@[simp]
+theorem shiftFunctorCompIsoId_shift_shift_neg' (i : A) :
+    (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)).inv.app X ≫ f⟦i⟧'⟦-i⟧' ≫
+    (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)).hom.app Y = f :=
+  NatIso.naturality_1 (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)) f
+
+@[simp]
+theorem shiftFunctorCompIsoId_shift_neg_shift' (i : A) :
+    (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)).inv.app X ≫ f⟦-i⟧'⟦i⟧' ≫
+    (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)).hom.app Y = f :=
+  NatIso.naturality_1 (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)) f
+
 theorem shift_shift_neg' (i : A) :
     f⟦i⟧'⟦-i⟧' = (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)).hom.app X ≫
       f ≫ (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)).inv.app Y :=

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

@@ -34,7 +34,39 @@ namespace Triangulated
 
 variable {C}
 
-/-- An octahedron is a type of datum whose existence is asserted by the octahedron axiom (TR 4). -/
+/-- An octahedron is a type of datum whose existence is asserted by the
+octahedron axiom (TR 4). The input is given by the following diagram:
+```
+     u₁₃      v₂₃
+  X₁ ────> X₃ ────> Z₂₃       Z₁₂⟦1⟧
+   🮡🮢      ^ 🮡🮢       🮡🮢      ^
+ u₁₂🮡🮢 u₂₃🮣🮠  🮡🮢v₁₃    🮡🮢w₂₃ 🮣🮠v₁₂⟦1⟧'
+     V   🮣🮠    V        V   🮣🮠
+      X₂       Z₁₃       X₂⟦1⟧
+       🮡🮢        🮡🮢      ^
+     v₁₂🮡🮢        🮡🮢w₁₃ 🮣🮠u₁₂⟦1⟧'
+         V         V   🮣🮠
+          Z₁₂ ───> X₁⟦1⟧
+              w₁₂
+```
+where `u₁₂ ≫ u₂₃ = u₁₃` and `(u₁₂,v₁₂,w₁₂), (u₁₃,v₁₃,w₁₃)` and `(u₂₃,v₂₃,w₂₃)`
+are distinguished triangles.. An `Octahedron` for this data consists of
+maps `m₁ : Z₁₂ ⟶ Z₁₃` and `m₃ : Z₁₃ ⟶ Z₂₃` such that `(m₁, m₃, w₂₃ ≫ v₁₂⟦1⟧')` is
+a distinguished triangle and the completed diagram commutes:
+```
+     u₁₃      v₂₃
+  X₁ ────> X₃ ────> Z₂₃ ────> Z₁₂⟦1⟧
+   🮡🮢      ^ 🮡🮢     ^ 🮡🮢      ^
+ u₁₂🮡🮢 u₂₃🮣🮠  🮡🮢v₁₃🮣🮠m₃🮡🮢w₂₃ 🮣🮠v₁₂⟦1⟧'
+     V   🮣🮠    V  🮣🮠    V   🮣🮠
+      X₂       Z₁₃       X₂⟦1⟧
+       🮡🮢     ^  🮡🮢      ^
+     v₁₂🮡🮢   🮣🮠m₁ 🮡🮢w₁₃ 🮣🮠u₁₂⟦1⟧'
+         V  🮣🮠     V   🮣🮠
+          Z₁₂ ───> X₁⟦1⟧
+              w₁₂
+```
+-/
 @[stacks 05QK]
 structure Octahedron
   {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
@@ -159,6 +191,114 @@ def ofIso {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C} (u₁₂' : X₁' 
 
 end Octahedron
 
+/-- An octahedron₁ is a type of datum whose existence follows from
+the octahedron axiom (TR 4). It is a rotated version of an octahedron.
+The input is given by the following diagram:
+```
+       v₁₂       u₁₃      w₂₃
+  Z₁₂ ────> X₁ ─────> X₃ ─────> Z₂₃⟦1⟧
+          ^  🮡🮢      ^ 🮡🮢
+      v₁₃🮣🮠u₁₂🮡🮢 u₂₃🮣🮠  🮡🮢w₁₃
+        🮣🮠     V   🮣🮠    V
+      Z₁₃        X₂       Z₁₃⟦1⟧
+                ^  🮡🮢
+           v₂₃🮣🮠    🮡🮢w₁₂
+             🮣🮠      V
+           Z₂₃      Z₁₂⟦1⟧
+```
+where `u₁₂ ≫ u₂₃ = u₁₃` and `(v₁₂,u₁₂,w₁₂), (v₁₃,u₁₃,w₁₃)` and `(v₂₃,u₂₃,w₂₃)`
+are distinguished triangles.. An `Octahedron₁` for this data consists of
+maps `m₁ : Z₁₂ ⟶ Z₁₃` and `m₃ : Z₁₃ ⟶ Z₂₃` such that `(m₁, m₃, v₂₃ ≫ w₁₂)` is
+a distinguished triangle and the completed diagram commutes:
+```
+       v₁₂       u₁₃      w₂₃
+  Z₁₂ ────> X₁ ─────> X₃ ─────> Z₂₃⟦1⟧
+   🮡🮢      ^  🮡🮢      ^ 🮡🮢      ^
+  m₁🮡🮢 v₁₃🮣🮠u₁₂🮡🮢 u₂₃🮣🮠  🮡🮢w₁₃ 🮣🮠m₃⟦1⟧'
+     V   🮣🮠     V   🮣🮠    V   🮣🮠
+      Z₁₃        X₂       Z₁₃⟦1⟧
+       🮡🮢       ^  🮡🮢      ^
+      m₃🮡🮢 v₂₃🮣🮠    🮡🮢w₁₂ 🮣🮠m₁⟦1⟧'
+         V   🮣🮠      V   🮣🮠
+          Z₂₃ ────> Z₁₂⟦1⟧
+```
+-/
+structure Octahedron₁
+  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
+  {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃)
+  {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ Z₁₂⟦(1 : ℤ)⟧} (h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distTriang C)
+  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ Z₂₃⟦(1 : ℤ)⟧} (h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distTriang C)
+  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ Z₁₃⟦(1 : ℤ)⟧} (h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distTriang C) where
+  /-- `m₁` is the morphism `a` of (TR 4) as presented in Stacks. -/
+  m₁ : Z₁₂ ⟶ Z₁₃
+  /-- `m₁` is the morphism `b` of (TR 4) as presented in Stacks. -/
+  m₃ : Z₁₃ ⟶ Z₂₃
+  comm₁ : m₁ ≫ v₁₃ = v₁₂
+  comm₂ : w₁₂ ≫ m₁⟦1⟧' = u₂₃ ≫ w₁₃
+  comm₃ : w₁₃ ≫ m₃⟦1⟧' = w₂₃
+  comm₄ : m₃ ≫ v₂₃ = v₁₃ ≫ u₁₂
+  mem : Triangle.mk m₁ m₃ (v₂₃ ≫ w₁₂) ∈ distTriang C
+
+set_option backward.isDefEq.respectTransparency false in
+instance (X : C) :
+    Nonempty (Octahedron₁ (comp_id (𝟙 X)) (inv_rot_of_distTriang _ (contractible_distinguished X))
+      (inv_rot_of_distTriang _ (contractible_distinguished X))
+      (inv_rot_of_distTriang _ (contractible_distinguished X))) :=
+ ⟨⟨0, 0, by simp, by simp, by simp, by simp, isomorphic_distinguished _
+   (contractible_distinguished (0 : C)) _ <| Triangle.isoMk _ (contractibleTriangle (0 : C))
+     (Functor.mapZeroObject _) (Functor.mapZeroObject _) (Functor.mapZeroObject _)⟩⟩
+
+
+namespace Octahedron₁
+
+attribute [reassoc] comm₁ comm₂ comm₃ comm₄
+
+variable {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
+  {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃)
+  {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ Z₁₂⟦(1 : ℤ)⟧} (h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distTriang C)
+  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ Z₂₃⟦(1 : ℤ)⟧} (h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distTriang C)
+  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ Z₁₃⟦(1 : ℤ)⟧} (h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distTriang C)
+  (h : Octahedron₁ comm h₁₂ h₂₃ h₁₃)
+
+/-- The triangle `Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧` given by an octahedron₂. -/
+@[simps!]
+def triangle : Triangle C :=
+  Triangle.mk h.m₁ h.m₃ (v₂₃ ≫ w₁₂)
+
+/-- The first morphism of triangles given by an octahedron₂. -/
+@[simps]
+def triangleMorphism₁ : Triangle.mk v₁₂ u₁₂ w₁₂ ⟶ Triangle.mk v₁₃ u₁₃ w₁₃ where
+  hom₁ := h.m₁
+  hom₂ := 𝟙 X₁
+  hom₃ := u₂₃
+  comm₁ := by
+    dsimp
+    rw [comp_id, h.comm₁]
+  comm₂ := by
+    dsimp
+    rw [id_comp, comm]
+  comm₃ := by
+    dsimp
+    rw [h.comm₂]
+
+/-- The second morphism of triangles given an octahedron₂. -/
+@[simps]
+def triangleMorphism₂ : Triangle.mk v₁₃ u₁₃ w₁₃ ⟶ Triangle.mk v₂₃ u₂₃ w₂₃ where
+  hom₁ := h.m₃
+  hom₂ := u₁₂
+  hom₃ := 𝟙 X₃
+  comm₁ := by
+    dsimp
+    rw [h.comm₄]
+  comm₂ := by
+    dsimp
+    rw [comp_id, comm]
+  comm₃ := by
+    dsimp
+    rw [id_comp, h.comm₃]
+
+end Octahedron₁
+
 end Triangulated
 
 open Triangulated
@@ -179,15 +319,14 @@ class IsTriangulated : Prop where
 namespace Triangulated
 
 variable {C}
-variable {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
+
+/-- A choice of octahedron given by the octahedron axiom. -/
+def someOctahedron' [IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
   {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃)
   {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ X₁⟦(1 : ℤ)⟧} {h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distTriang C}
   {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ X₂⟦(1 : ℤ)⟧} {h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distTriang C}
-  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ X₁⟦(1 : ℤ)⟧} {h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distTriang C}
-  (h : Octahedron comm h₁₂ h₂₃ h₁₃)
-
-/-- A choice of octahedron given by the octahedron axiom. -/
-def someOctahedron' [IsTriangulated C] : Octahedron comm h₁₂ h₂₃ h₁₃ :=
+  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ X₁⟦(1 : ℤ)⟧} {h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distTriang C} :
+  Octahedron comm h₁₂ h₂₃ h₁₃ :=
   (IsTriangulated.octahedron_axiom comm h₁₂ h₂₃ h₁₃).some
 
 /-- A choice of octahedron given by the octahedron axiom. -/
@@ -200,6 +339,58 @@ def someOctahedron [IsTriangulated C]
     Octahedron comm h₁₂ h₂₃ h₁₃ :=
   someOctahedron' _
 
+set_option backward.isDefEq.respectTransparency false in
+/-- A choice of octahedron₁ given by the octahedron axiom. -/
+def someOctahedron₁ [IsTriangulated C]
+    {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
+    {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃)
+    {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ Z₁₂⟦(1 : ℤ)⟧} (h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distTriang C)
+    {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ Z₂₃⟦(1 : ℤ)⟧} (h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distTriang C)
+    {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ Z₁₃⟦(1 : ℤ)⟧} (h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distTriang C) :
+    Octahedron₁ comm h₁₂ h₂₃ h₁₃ := by
+  let o := someOctahedron comm (rot_of_distTriang _ h₁₂) (rot_of_distTriang _ h₂₃)
+    (rot_of_distTriang _ h₁₃)
+  let m₁ := (shiftShiftNeg Z₁₂ 1).inv ≫ o.m₁⟦-1⟧' ≫ (shiftShiftNeg Z₁₃ 1).hom
+  let m₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ o.m₃⟦-1⟧' ≫ (shiftShiftNeg Z₂₃ 1).hom
+  have eq₁ := o.comm₁
+  have eq₂ := o.comm₂
+  have eq₃ := o.comm₃
+  have eq₄ := o.comm₄
+  dsimp only [Triangle.mk_obj₁, Triangle.mk_obj₂, Triangle.mk_mor₁, Triangle.mk_mor₃]
+    at eq₁ eq₂ eq₃ eq₄
+  rw [comp_neg, neg_inj] at eq₂
+  rw [neg_comp, comp_neg, neg_inj] at eq₄
+  refine ⟨m₁, m₃, ?_, ?_, ?_, ?_, ?_⟩
+  · rw [← shiftFunctorCompIsoId_shift_shift_neg' v₁₃ (1 : ℤ)]
+    unfold m₁
+    dsimp
+    rw [assoc, assoc, Iso.hom_inv_id_app_assoc]
+    nth_rw 2 [← assoc]
+    rw [← Functor.map_comp, eq₂, shiftFunctorCompIsoId_shift_shift_neg']
+  · unfold m₁
+    dsimp
+    rw [Functor.map_comp, Functor.map_comp, shift_shiftFunctorCompIsoId_hom_app,
+      shift_shiftFunctorCompIsoId_inv_app, shiftFunctorCompIsoId_shift_neg_shift', eq₁]
+  · unfold m₃
+    dsimp
+    rw [Functor.map_comp, Functor.map_comp, shift_shiftFunctorCompIsoId_hom_app,
+      shift_shiftFunctorCompIsoId_inv_app, shiftFunctorCompIsoId_shift_neg_shift', eq₃]
+  · rw [← shiftFunctorCompIsoId_shift_shift_neg' v₂₃ (1 : ℤ)]
+    unfold m₃
+    dsimp
+    rw [assoc, assoc, Iso.hom_inv_id_app_assoc]
+    nth_rw 2 [← assoc]
+    rw [← Functor.map_comp, ← eq₄, ← Functor.map_comp, shiftFunctorCompIsoId_shift_shift_neg']
+  · apply isomorphic_distinguished _ ((Triangle.shift_distinguished_iff _ (-1 : ℤ)).mpr o.mem)
+    refine Triangle.isoMk _ _ (shiftShiftNeg Z₁₂ (1 : ℤ)).symm
+      (-(shiftShiftNeg Z₁₃ (1 : ℤ)).symm) (shiftShiftNeg Z₂₃ (1 : ℤ)).symm (comm₃ := ?_)
+    dsimp
+    simp only [Int.reduceNeg, assoc, Int.negOnePow_neg, Int.negOnePow_one, neg_comp,
+      Functor.map_neg, Functor.map_comp, smul_neg, Units.neg_smul, one_smul, neg_neg]
+    rw [shift_shift_neg', shift_shift_neg', shift_shiftFunctorCompIsoId_inv_app,
+      shiftFunctorComm_hom_app_of_add_eq_zero _ _ (Int.add_right_neg 1)]
+    simp
+
 end Triangulated
 
 variable {C}