From fd7d069a08f2d88ae27088c12b5bf9b811f1b800 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sat, 8 Jun 2024 04:15:15 +0000 Subject: [PATCH] feat: shifted morphisms in categories with a shift (#13571) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Given a category `C` endowed with a shift by an additive monoid `M` and two objects `X` and `Y` in `C`, we consider the types `ShiftedHom X Y m` defined as `X ⟶ (Y⟦m⟧)` for all `m : M`, and the composition on these shifted hom. --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Shift/Basic.lean | 5 + Mathlib/CategoryTheory/Shift/ShiftedHom.lean | 126 +++++++++++++++++++ 3 files changed, 132 insertions(+) create mode 100644 Mathlib/CategoryTheory/Shift/ShiftedHom.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9e5c45d30b900..2364c27f620ac 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1584,6 +1584,7 @@ import Mathlib.CategoryTheory.Shift.Predicate import Mathlib.CategoryTheory.Shift.Pullback import Mathlib.CategoryTheory.Shift.Quotient import Mathlib.CategoryTheory.Shift.ShiftSequence +import Mathlib.CategoryTheory.Shift.ShiftedHom import Mathlib.CategoryTheory.Shift.SingleFunctors import Mathlib.CategoryTheory.Sigma.Basic import Mathlib.CategoryTheory.Simple diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index 65e713add28d8..7c15dfda5f93e 100644 --- a/Mathlib/CategoryTheory/Shift/Basic.lean +++ b/Mathlib/CategoryTheory/Shift/Basic.lean @@ -193,6 +193,11 @@ def shiftFunctorZero : shiftFunctor C (0 : A) ≅ 𝟭 C := (shiftMonoidalFunctor C A).εIso.symm #align category_theory.shift_functor_zero CategoryTheory.shiftFunctorZero +variable {A} in +/-- Shifting by `a` such that `a = 0` identifies to the identity functor. -/ +def shiftFunctorZero' (a : A) (ha : a = 0) : shiftFunctor C a ≅ 𝟭 C := + eqToIso (by rw [ha]) ≪≫ shiftFunctorZero C A + variable {C A} lemma ShiftMkCore.shiftFunctor_eq (h : ShiftMkCore C A) (a : A) : diff --git a/Mathlib/CategoryTheory/Shift/ShiftedHom.lean b/Mathlib/CategoryTheory/Shift/ShiftedHom.lean new file mode 100644 index 0000000000000..7211367069a8f --- /dev/null +++ b/Mathlib/CategoryTheory/Shift/ShiftedHom.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2024 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.Shift.Basic +import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor + +/-! Shifted morphisms + +Given a category `C` endowed with a shift by an additive monoid `M` and two +objects `X` and `Y` in `C`, we consider the types `ShiftedHom X Y m` +defined as `X ⟶ (Y⟦m⟧)` for all `m : M`, and the composition on these +shifted hom. + +## TODO + +* redefine Ext-groups in abelian categories using `ShiftedHom` in the derived category. +* study the `R`-module structures on `ShiftedHom` when `C` is `R`-linear + +-/ + +namespace CategoryTheory + +open Category + +variable {C : Type*} [Category C] + {M : Type*} [AddMonoid M] [HasShift C M] + +/-- In a category `C` equipped with a shift by an additive monoid, +this is the type of morphisms `X ⟶ (Y⟦n⟧)` for `m : M`. -/ +def ShiftedHom (X Y : C) (m : M) : Type _ := X ⟶ (Y⟦m⟧) + +instance [Preadditive C] (X Y : C) (n : M) : AddCommGroup (ShiftedHom X Y n) := by + dsimp only [ShiftedHom] + infer_instance + +namespace ShiftedHom + +variable {X Y Z T : C} + +/-- The composition of `f : X ⟶ Y⟦a⟧` and `g : Y ⟶ Z⟦b⟧`, as a morphism `X ⟶ Z⟦c⟧` +when `b + a = c`. -/ +noncomputable def comp {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) : + ShiftedHom X Z c := + f ≫ g⟦a⟧' ≫ (shiftFunctorAdd' C b a c h).inv.app _ + +lemma comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : M} + (α : ShiftedHom X Y a₁) (β : ShiftedHom Y Z a₂) (γ : ShiftedHom Z T a₃) + (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) : + (α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) = + α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h]) := by + simp only [comp, assoc, Functor.map_comp, + shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h, + ← NatTrans.naturality_assoc, Functor.comp_map] + +/-! In degree `0 : M`, shifted hom `ShiftedHom X Y 0` identify to morphisms `X ⟶ Y`. +We generalize this to `m₀ : M` such that `m₀ : 0` as it shall be convenient when we +apply this with `M := ℤ` and `m₀` the coercion of `0 : ℕ`. -/ + +/-- The element of `ShiftedHom X Y m₀` (when `m₀ = 0`) attached to a morphism `X ⟶ Y`. -/ +noncomputable def mk₀ (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : ShiftedHom X Y m₀ := + f ≫ (shiftFunctorZero' C m₀ hm₀).inv.app Y + +/-- The bijection `(X ⟶ Y) ≃ ShiftedHom X Y m₀` when `m₀ = 0`. -/ +@[simps apply] +noncomputable def homEquiv (m₀ : M) (hm₀ : m₀ = 0) : (X ⟶ Y) ≃ ShiftedHom X Y m₀ where + toFun f := mk₀ m₀ hm₀ f + invFun g := g ≫ (shiftFunctorZero' C m₀ hm₀).hom.app Y + left_inv f := by simp [mk₀] + right_inv g := by simp [mk₀] + +lemma mk₀_comp (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M} (g : ShiftedHom Y Z a) : + (mk₀ m₀ hm₀ f).comp g (by rw [hm₀, add_zero]) = f ≫ g := by + subst hm₀ + simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero'] + +@[simp] +lemma mk₀_id_comp (m₀ : M) (hm₀ : m₀ = 0) {a : M} (f : ShiftedHom X Y a) : + (mk₀ m₀ hm₀ (𝟙 X)).comp f (by rw [hm₀, add_zero]) = f := by + simp [mk₀_comp] + +lemma comp_mk₀ {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) : + f.comp (mk₀ m₀ hm₀ g) (by rw [hm₀, zero_add]) = f ≫ g⟦a⟧' := by + subst hm₀ + simp only [comp, shiftFunctorAdd'_zero_add_inv_app, mk₀, shiftFunctorZero', + eqToIso_refl, Iso.refl_trans, ← Functor.map_comp, assoc, Iso.inv_hom_id_app, + Functor.id_obj, comp_id] + +@[simp] +lemma comp_mk₀_id {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) : + f.comp (mk₀ m₀ hm₀ (𝟙 Y)) (by rw [hm₀, zero_add]) = f := by + simp [comp_mk₀] + +section Preadditive + +variable [Preadditive C] + +@[simp] +lemma comp_add [∀ (a : M), (shiftFunctor C a).Additive] + {a b c : M} (α : ShiftedHom X Y a) (β₁ β₂ : ShiftedHom Y Z b) (h : b + a = c) : + α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h := by + rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add] + +@[simp] +lemma add_comp + {a b c : M} (α₁ α₂ : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) : + (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h := by + rw [comp, comp, comp, Preadditive.add_comp] + +variable (Z) in +lemma comp_zero [∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms] + {a : M} (β : ShiftedHom X Y a) {b c : M} (h : b + a = c) : + β.comp (0 : ShiftedHom Y Z b) h = 0 := by + rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero] + +variable (X) in +lemma zero_comp (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) : + (0 : ShiftedHom X Y a).comp β h = 0 := by + rw [comp, Limits.zero_comp] + +end Preadditive + +end ShiftedHom + +end CategoryTheory