feat: the shift on a quotient category

Mathlib.lean

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

Mathlib/CategoryTheory/Quotient.lean

@@ -218,6 +218,57 @@ theorem lift_map_functor_map {X Y : C} (f : X ⟶ Y) :
   simp
 #align category_theory.quotient.lift_map_functor_map CategoryTheory.Quotient.lift_map_functor_map
 
+variable {r}
+
+lemma natTrans_ext {F G : Quotient r ⥤ D} (τ₁ τ₂ : F ⟶ G)
+    (h : whiskerLeft (Quotient.functor r) τ₁ = whiskerLeft (Quotient.functor r) τ₂) : τ₁ = τ₂ :=
+  NatTrans.ext _ _ (by ext1 ⟨X⟩ ; exact NatTrans.congr_app h X)
+
+variable (r)
+
+/-- In order to define a natural transformation `F ⟶ G` with `F G : Quotient r ⥤ D`, it suffices
+to do so after precomposing with `Quotient.functor r`. -/
+def natTransLift {F G : Quotient r ⥤ D} (τ : Quotient.functor r ⋙ F ⟶ Quotient.functor r ⋙ G) :
+    F ⟶ G where
+  app := fun ⟨X⟩ => τ.app X
+  naturality := fun ⟨X⟩ ⟨Y⟩ => by
+    rintro ⟨f⟩
+    exact τ.naturality f
+
+@[simp]
+lemma natTransLift_app (F G : Quotient r ⥤ D)
+    (τ : Quotient.functor r ⋙ F ⟶ Quotient.functor r ⋙ G) (X : C) :
+  (natTransLift r τ).app ((Quotient.functor r).obj X) = τ.app X := rfl
+
+@[reassoc]
+lemma comp_natTransLift {F G H : Quotient r ⥤ D}
+    (τ : Quotient.functor r ⋙ F ⟶ Quotient.functor r ⋙ G)
+    (τ' : Quotient.functor r ⋙ G ⟶ Quotient.functor r ⋙ H) :
+    natTransLift r τ ≫ natTransLift r τ' =  natTransLift r (τ ≫ τ') := by aesop_cat
+
+@[simp]
+lemma natTransLift_id (F : Quotient r ⥤ D) :
+    natTransLift r (𝟙 (Quotient.functor r ⋙ F)) = 𝟙 _ := by aesop_cat
+
+/-- In order to define a natural isomorphism `F ≅ G` with `F G : Quotient r ⥤ D`, it suffices
+to do so after precomposing with `Quotient.functor r`. -/
+@[simps]
+def natIsoLift {F G : Quotient r ⥤ D} (τ : Quotient.functor r ⋙ F ≅ Quotient.functor r ⋙ G) :
+    F ≅ G where
+  hom := natTransLift _ τ.hom
+  inv := natTransLift _ τ.inv
+  hom_inv_id := by rw [comp_natTransLift, τ.hom_inv_id, natTransLift_id]
+  inv_hom_id := by rw [comp_natTransLift, τ.inv_hom_id, natTransLift_id]
+
+variable (D)
+
+instance full_whiskeringLeft_functor :
+    Full ((whiskeringLeft C _ D).obj (functor r)) where
+  preimage := natTransLift r
+
+instance faithful_whiskeringLeft_functor :
+    Faithful ((whiskeringLeft C _ D).obj (functor r)) := ⟨by apply natTrans_ext⟩
+
 end Quotient
 
 end CategoryTheory

Mathlib/CategoryTheory/Shift/Quotient.lean

@@ -0,0 +1,80 @@
+/-
+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.Quotient
+
+/-!
+# Shift on a quotient category
+
+Let `C` be a category equipped a shift by a monoid `A`. If we have a relation
+on morphisms `r : HomRel C` that is compatible with the shift (i.e. if two
+morphisms `f` and `g` are related, then `f⟦a⟧'` and `g⟦a⟧'` are also related
+for all `a : A`), then the quotient category `Quotient r` is equipped with
+a shift.
+
+The condition `r.IsCompatibleWithShift A` on the relation `r` is a class so that
+the shift can be automatically infered on the quotient category.
+
+-/
+
+universe v u
+
+open CategoryTheory
+
+variable {C : Type u} [Category.{v} C]
+  (r : HomRel C) (A : Type _) [AddMonoid A] [HasShift C A]
+
+namespace HomRel
+
+class IsCompatibleWithShift : Prop :=
+  translate : ∀ (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y) (_ : r f g), r (f⟦a⟧') (g⟦a⟧')
+
+end HomRel
+
+namespace CategoryTheory
+
+variable (s : A → Quotient r ⥤ Quotient r)
+  (i : ∀ a, Quotient.functor r ⋙ s a ≅ shiftFunctor C a ⋙ Quotient.functor r)
+
+lemma HasShift.quotient'_aux :
+    Nonempty (Full ((whiskeringLeft C _ (Quotient r)).obj (Quotient.functor r))) ∧
+        Faithful ((whiskeringLeft C _ (Quotient r)).obj (Quotient.functor r)) :=
+  ⟨⟨inferInstance⟩, inferInstance⟩
+
+noncomputable def HasShift.quotient' :
+    HasShift (Quotient r) A :=
+  HasShift.induced (Quotient.functor r) A s i (HasShift.quotient'_aux r)
+
+noncomputable def Functor.CommShift.quotient' :
+    letI : HasShift (Quotient r) A := HasShift.quotient' r A s i
+    (Quotient.functor r).CommShift A :=
+  Functor.CommShift.ofInduced _ _ _ _ _
+
+variable {A}
+
+def Quotient.shiftFunctor' [r.IsCompatibleWithShift A] (a : A) : Quotient r ⥤ Quotient r :=
+  Quotient.lift r (CategoryTheory.shiftFunctor C a ⋙ Quotient.functor r)
+    (fun _ _ _ _ hfg => Quotient.sound r (HomRel.IsCompatibleWithShift.translate _ _ _ hfg))
+
+def Quotient.shiftFunctor'Factors [r.IsCompatibleWithShift A] (a : A) :
+    Quotient.functor r ⋙ Quotient.shiftFunctor' r a ≅
+      CategoryTheory.shiftFunctor C a ⋙ Quotient.functor r :=
+  Quotient.lift.isLift _ _ _
+
+variable (A)
+
+noncomputable instance HasShift.quotient [r.IsCompatibleWithShift A] :
+    HasShift (Quotient r) A :=
+  HasShift.quotient' r A (Quotient.shiftFunctor' r) (Quotient.shiftFunctor'Factors r)
+
+noncomputable instance Quotient.functor_commShift [r.IsCompatibleWithShift A] :
+    (Quotient.functor r).CommShift A :=
+  Functor.CommShift.quotient' _ _ _ _
+
+-- the construction is made irreducible in order to prevent timeouts and abuse of defeq
+attribute [irreducible] HasShift.quotient Quotient.functor_commShift
+
+end CategoryTheory