feat: the shift induced on a localized category (#6655)

This PR shows that when a morphism property `W` on a category is compatible with the shift by a monoid `A`, then the localized category can also be equipped with a shift.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib.lean

@@ -1155,6 +1155,7 @@ import Mathlib.CategoryTheory.Quotient
 import Mathlib.CategoryTheory.Shift.Basic
 import Mathlib.CategoryTheory.Shift.CommShift
 import Mathlib.CategoryTheory.Shift.Induced
+import Mathlib.CategoryTheory.Shift.Localization
 import Mathlib.CategoryTheory.Shift.Quotient
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Simple

Mathlib/CategoryTheory/Shift/Localization.lean

@@ -0,0 +1,87 @@
+/-
+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.Shift.Induced
+import Mathlib.CategoryTheory.Localization.Predicate
+
+/-!
+# The shift induced on a localized category
+
+Let `C` be a category equipped with a shift by a monoid `A`. A morphism property `W`
+on `C` satisfies `W.IsCompatibleWithShift A` when for all `a : A`,
+a morphism `f` is in `W` iff `f⟦a⟧'` is. When this compatibility is satisfied,
+then the corresponding localized category can be equipped with
+a shift by `A`, and the localization functor is compatible with the shift.
+
+--/
+
+universe v₁ v₂ u₁ u₂ w
+
+namespace CategoryTheory
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
+  (L : C ⥤ D) (W : MorphismProperty C) [L.IsLocalization W]
+  (A : Type w) [AddMonoid A] [HasShift C A]
+
+namespace MorphismProperty
+
+/-- A morphism property `W` on a category `C` is compatible with the shift by a
+monoid `A` when for all `a : A`, a morphism `f` belongs to `W`
+if and only if `f⟦a⟧'` does. -/
+class IsCompatibleWithShift : Prop :=
+  /-- the condition that for all `a : A`, the morphism property `W` is not changed when
+  we take its inverse image by the shift functor by `a` -/
+  condition : ∀ (a : A), W.inverseImage (shiftFunctor C a) = W
+
+variable [W.IsCompatibleWithShift A]
+
+namespace IsCompatibleWithShift
+
+variable {A}
+
+lemma iff {X Y : C} (f : X ⟶ Y) (a : A) : W (f⟦a⟧') ↔ W f := by
+  conv_rhs => rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]
+
+lemma shiftFunctor_comp_inverts (a : A) :
+    W.IsInvertedBy (shiftFunctor C a ⋙ L) := fun _ _ f hf =>
+  Localization.inverts L W _ (by simpa only [iff] using hf)
+
+end IsCompatibleWithShift
+
+end MorphismProperty
+
+variable [W.IsCompatibleWithShift A]
+
+/-- When `L : C ⥤ D` is a localization functor with respect to a morphism property `W`
+that is compatible with the shift by a monoid `A` on `C`, this is the induced
+shift on the category `D`. -/
+noncomputable def HasShift.localized  : HasShift D A :=
+  HasShift.induced L A
+    (fun a => Localization.lift (shiftFunctor C a ⋙ L)
+      (MorphismProperty.IsCompatibleWithShift.shiftFunctor_comp_inverts L W a) L)
+    (fun _ => Localization.fac _ _ _)
+    ⟨⟨(inferInstance : Full (Localization.whiskeringLeftFunctor' L W D))⟩,
+      (inferInstance : Faithful (Localization.whiskeringLeftFunctor' L W D))⟩
+
+/-- The localization functor `L : C ⥤ D` is compatible with the shift. -/
+noncomputable def Functor.CommShift.localized :
+    @Functor.CommShift _ _ _ _ L A _ _ (HasShift.localized L W A) :=
+  Functor.CommShift.ofInduced _ _ _ _ _
+
+attribute [irreducible] HasShift.localized Functor.CommShift.localized
+
+/-- The localized category `W.Localization` is endowed with the induced shift.  -/
+noncomputable instance HasShift.localization :
+    HasShift W.Localization A :=
+  HasShift.localized W.Q W A
+
+/-- The localization functor `W.Q : C ⥤ W.Localization` is compatible with the shift. -/
+noncomputable instance MorphismProperty.commShift_Q :
+    W.Q.CommShift A :=
+  Functor.CommShift.localized W.Q W A
+
+attribute [irreducible] HasShift.localization MorphismProperty.commShift_Q
+
+end CategoryTheory