From 9fae0272e6f4dfce16a4cd23146025695464fa11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 5 Sep 2023 14:01:29 +0000 Subject: [PATCH] feat: the shift on the category of triangles (#6688) If a preadditive category `C` is equipped with a shift by the integers, then the category of triangles in `C` is also equipped with a shift. --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Shift/Basic.lean | 13 +- .../CategoryTheory/Triangulated/Basic.lean | 7 + .../Triangulated/TriangleShift.lean | 159 ++++++++++++++++++ 4 files changed, 179 insertions(+), 1 deletion(-) create mode 100644 Mathlib/CategoryTheory/Triangulated/TriangleShift.lean diff --git a/Mathlib.lean b/Mathlib.lean index bd52412f77243e..23f6ed26d15db5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1204,6 +1204,7 @@ import Mathlib.CategoryTheory.Thin import Mathlib.CategoryTheory.Triangulated.Basic import Mathlib.CategoryTheory.Triangulated.Pretriangulated import Mathlib.CategoryTheory.Triangulated.Rotate +import Mathlib.CategoryTheory.Triangulated.TriangleShift import Mathlib.CategoryTheory.Triangulated.Triangulated import Mathlib.CategoryTheory.Types import Mathlib.CategoryTheory.UnivLE diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index ee271249d13116..27a853fd3e491f 100644 --- a/Mathlib/CategoryTheory/Shift/Basic.lean +++ b/Mathlib/CategoryTheory/Shift/Basic.lean @@ -572,8 +572,13 @@ lemma shiftFunctorComm_eq (i j k : A) (h : i + j = k) : rfl #align category_theory.shift_functor_comm_eq CategoryTheory.shiftFunctorComm_eq +@[simp] +lemma shiftFunctorComm_eq_refl (i : A) : + shiftFunctorComm C i i = Iso.refl _ := by + rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id] + lemma shiftFunctorComm_symm (i j : A) : - (shiftFunctorComm C i j).symm = shiftFunctorComm C j i := by + (shiftFunctorComm C i j).symm = shiftFunctorComm C j i := by ext1 dsimp rw [shiftFunctorComm_eq C i j (i+j) rfl, shiftFunctorComm_eq C j i (i+j) (add_comm j i)] @@ -629,6 +634,12 @@ lemma shiftFunctorZero_inv_app_shift (n : A) : rw [Functor.map_id] #align category_theory.shift_functor_zero_inv_app_shift CategoryTheory.shiftFunctorZero_inv_app_shift +lemma shiftFunctorComm_zero_hom_app (a : A) : + (shiftFunctorComm C a 0).hom.app X = + (shiftFunctorZero C A).hom.app (X⟦a⟧) ≫ ((shiftFunctorZero C A).inv.app X)⟦a⟧' := by + simp only [shiftFunctorZero_hom_app_shift, Category.assoc, ← Functor.map_comp, + Iso.hom_inv_id_app, Functor.map_id, Functor.comp_obj, Category.comp_id] + @[reassoc] lemma shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app (m₁ m₂ m₃ : A) (X : C) : (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ diff --git a/Mathlib/CategoryTheory/Triangulated/Basic.lean b/Mathlib/CategoryTheory/Triangulated/Basic.lean index 250428384ec99a..5243ece32cdb47 100644 --- a/Mathlib/CategoryTheory/Triangulated/Basic.lean +++ b/Mathlib/CategoryTheory/Triangulated/Basic.lean @@ -192,4 +192,11 @@ def Triangle.isoMk (A B : Triangle C) Functor.map_id, Category.comp_id]) #align category_theory.pretriangulated.triangle.iso_mk CategoryTheory.Pretriangulated.Triangle.isoMk +lemma Triangle.eqToHom_hom₁ {A B : Triangle C} (h : A = B) : + (eqToHom h).hom₁ = eqToHom (by subst h; rfl) := by subst h; rfl +lemma Triangle.eqToHom_hom₂ {A B : Triangle C} (h : A = B) : + (eqToHom h).hom₂ = eqToHom (by subst h; rfl) := by subst h; rfl +lemma Triangle.eqToHom_hom₃ {A B : Triangle C} (h : A = B) : + (eqToHom h).hom₃ = eqToHom (by subst h; rfl) := by subst h; rfl + end CategoryTheory.Pretriangulated diff --git a/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean b/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean new file mode 100644 index 00000000000000..95767d70bb05ec --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2023 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.CategoryTheory.Triangulated.Rotate +import Mathlib.Algebra.GroupPower.NegOnePow + +/-! +# The shift on the category of triangles + +In this file, it is shown that if `C` is a preadditive category with +a shift by `ℤ`, then the category of triangles `Triangle C` is also +endowed with a shift. We also show that rotating triangles three times +identifies with the shift by `1`. + +The shift on the category of triangles was also obtained by Adam Topaz, +Johan Commelin and Andrew Yang during the Liquid Tensor Experiment. + +-/ + +universe v u + +namespace CategoryTheory + +open Category Preadditive + +variable (C : Type u) [Category.{v} C] [Preadditive C] [HasShift C ℤ] + [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] + +namespace Pretriangulated + +attribute [local simp] Triangle.eqToHom_hom₁ Triangle.eqToHom_hom₂ Triangle.eqToHom_hom₃ + shiftFunctorAdd_zero_add_hom_app shiftFunctorAdd_add_zero_hom_app + shiftFunctorAdd'_eq_shiftFunctorAdd shift_shiftFunctorCompIsoId_inv_app + +/-- The shift functor `Triangle C ⥤ Triangle C` by `n : ℤ` sends a triangle +to the triangle obtained by shifting the objects by `n` in `C` and by +multiplying the three morphisms by `(-1)^n`. -/ +@[simps] +noncomputable def Triangle.shiftFunctor (n : ℤ) : Triangle C ⥤ Triangle C where + obj T := Triangle.mk (n.negOnePow • T.mor₁⟦n⟧') (n.negOnePow • T.mor₂⟦n⟧') + (n.negOnePow • T.mor₃⟦n⟧' ≫ (shiftFunctorComm C 1 n).hom.app T.obj₁) + map f := + { hom₁ := f.hom₁⟦n⟧' + hom₂ := f.hom₂⟦n⟧' + hom₃ := f.hom₃⟦n⟧' + comm₁ := by + dsimp + simp only [zsmul_comp, comp_zsmul, ← Functor.map_comp, f.comm₁] + comm₂ := by + dsimp + simp only [zsmul_comp, comp_zsmul, ← Functor.map_comp, f.comm₂] + comm₃ := by + dsimp + rw [zsmul_comp, comp_zsmul, ← Functor.map_comp_assoc, ← f.comm₃, + Functor.map_comp, assoc, assoc] + erw [(shiftFunctorComm C 1 n).hom.naturality] + rfl } + +/-- The canonical isomorphism `Triangle.shiftFunctor C 0 ≅ 𝟭 (Triangle C)`. -/ +@[simps!] +noncomputable def Triangle.shiftFunctorZero : Triangle.shiftFunctor C 0 ≅ 𝟭 _ := + NatIso.ofComponents + (fun T => Triangle.isoMk _ _ ((CategoryTheory.shiftFunctorZero C ℤ).app _) + ((CategoryTheory.shiftFunctorZero C ℤ).app _) ((CategoryTheory.shiftFunctorZero C ℤ).app _) + (by aesop_cat) (by aesop_cat) (by + dsimp + simp only [one_zsmul, assoc, shiftFunctorComm_zero_hom_app, + ← Functor.map_comp, Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id, + comp_id, NatTrans.naturality, Functor.id_map])) + (by aesop_cat) + +/-- The canonical isomorphism +`Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b` +when `a + b = n`. -/ +@[simps!] +noncomputable def Triangle.shiftFunctorAdd' (a b n : ℤ) (h : a + b = n) : + Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b := + NatIso.ofComponents + (fun T => Triangle.isoMk _ _ + ((CategoryTheory.shiftFunctorAdd' C a b n h).app _) + ((CategoryTheory.shiftFunctorAdd' C a b n h).app _) + ((CategoryTheory.shiftFunctorAdd' C a b n h).app _) + (by + subst h + dsimp + rw [zsmul_comp, NatTrans.naturality, comp_zsmul, Functor.comp_map, Functor.map_zsmul, + comp_zsmul, smul_smul, Int.negOnePow_add, mul_comm]) + (by + subst h + dsimp + rw [zsmul_comp, NatTrans.naturality, comp_zsmul, Functor.comp_map, Functor.map_zsmul, + comp_zsmul, smul_smul, Int.negOnePow_add, mul_comm]) + (by + subst h + dsimp + rw [zsmul_comp, comp_zsmul, Functor.map_zsmul, zsmul_comp, comp_zsmul, smul_smul, + assoc, Functor.map_comp, assoc] + erw [← NatTrans.naturality_assoc] + simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Int.negOnePow_add, + shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, add_comm a])) + (by aesop_cat) + +/-- Rotating triangles three times identifies with the shift by `1`. -/ +noncomputable def rotateRotateRotateIso : + rotate C ⋙ rotate C ⋙ rotate C ≅ Triangle.shiftFunctor C 1 := + NatIso.ofComponents + (fun T => Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) + (by aesop_cat) (by aesop_cat) (by aesop_cat)) + (by aesop_cat) + +/-- Rotating triangles three times backwards identifies with the shift by `-1`. -/ +noncomputable def invRotateInvRotateInvRotateIso : + invRotate C ⋙ invRotate C ⋙ invRotate C ≅ Triangle.shiftFunctor C (-1) := + NatIso.ofComponents + (fun T => Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) + (by aesop_cat) + (by aesop_cat) + (by + dsimp [shiftFunctorCompIsoId] + simp [shiftFunctorComm_eq C _ _ _ (add_neg_self (1 : ℤ))])) + (by aesop_cat) + +/-- The inverse of the rotation of triangles can be expressed using a double +rotation and the shift by `-1`. -/ +noncomputable def invRotateIsoRotateRotateShiftFunctorNegOne : + invRotate C ≅ rotate C ⋙ rotate C ⋙ Triangle.shiftFunctor C (-1) := + calc + invRotate C ≅ invRotate C ⋙ 𝟭 _ := (Functor.rightUnitor _).symm + _ ≅ invRotate C ⋙ Triangle.shiftFunctor C 0 := + isoWhiskerLeft _ (Triangle.shiftFunctorZero C).symm + _ ≅ invRotate C ⋙ Triangle.shiftFunctor C 1 ⋙ Triangle.shiftFunctor C (-1) := + isoWhiskerLeft _ (Triangle.shiftFunctorAdd' C 1 (-1) 0 (add_neg_self 1)) + _ ≅ invRotate C ⋙ (rotate C ⋙ rotate C ⋙ rotate C) ⋙ Triangle.shiftFunctor C (-1) := + isoWhiskerLeft _ (isoWhiskerRight (rotateRotateRotateIso C).symm _) + _ ≅ (invRotate C ⋙ rotate C) ⋙ rotate C ⋙ rotate C ⋙ Triangle.shiftFunctor C (-1) := + isoWhiskerLeft _ (Functor.associator _ _ _ ≪≫ + isoWhiskerLeft _ (Functor.associator _ _ _)) ≪≫ (Functor.associator _ _ _).symm + _ ≅ 𝟭 _ ⋙ rotate C ⋙ rotate C ⋙ Triangle.shiftFunctor C (-1) := + isoWhiskerRight (triangleRotation C).counitIso _ + _ ≅ _ := Functor.leftUnitor _ + +noncomputable instance : HasShift (Triangle C) ℤ := + hasShiftMk (Triangle C) ℤ + { F := Triangle.shiftFunctor C + zero := Triangle.shiftFunctorZero C + add := fun a b => Triangle.shiftFunctorAdd' C a b _ rfl + assoc_hom_app := fun a b c T => by + ext + all_goals + dsimp + rw [← shiftFunctorAdd'_assoc_hom_app a b c _ _ _ rfl rfl (add_assoc a b c)] + dsimp only [CategoryTheory.shiftFunctorAdd'] + simp } + +end Pretriangulated + +end CategoryTheory