refactor(category_theory/shift): make shifts more flexible (#10573)

Co-authored-by: Andrew Yang <the.erd.one@gmail.com>



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: erd1 <the.erd.one@gmail.com>

Author: jcommelin

src/algebra/homology/differential_object.lean

@@ -54,6 +54,8 @@ by { cases h, simp }
 
 variables (b V)
 
+local attribute [reducible] graded_object.has_shift
+
 /--
 The functor from differential graded objects to homological complexes.
 -/
@@ -63,20 +65,23 @@ def dgo_to_homological_complex :
     homological_complex V (complex_shape.up' b) :=
 { obj := λ X,
   { X := λ i, X.X i,
-    d := λ i j, if h : i + b = j then X.d i ≫ eq_to_hom (congr_arg X.X h) else 0,
-    shape' := λ i j w, by { dsimp at w, rw dif_neg w, },
+    d := λ i j, if h : i + b = j then
+      X.d i ≫ X.X_eq_to_hom (show i + (1 : ℤ) • b = j, by simp [h]) else 0,
+    shape' := λ i j w, by { dsimp at w, convert dif_neg w },
     d_comp_d' := λ i j k hij hjk, begin
       dsimp at hij hjk, substs hij hjk,
-      simp only [category.comp_id, eq_to_hom_refl, dif_pos rfl],
-      exact congr_fun (X.d_squared) i,
+      have : X.d i ≫ X.d _ = _ := (congr_fun X.d_squared i : _),
+      reassoc! this,
+      simp [this],
     end },
   map := λ X Y f,
   { f := f.f,
     comm' := λ i j h, begin
       dsimp at h ⊢,
       subst h,
-      simp only [category.comp_id, eq_to_hom_refl, dif_pos rfl],
-      exact (congr_fun f.comm i).symm
+      have : f.f i ≫ Y.d i = X.d i ≫ f.f (i + 1 • b) := (congr_fun f.comm i).symm,
+      reassoc! this,
+      simp only [category.comp_id, eq_to_hom_refl, dif_pos rfl, this, category.assoc, eq_to_hom_f]
     end, } }
 
 /--
@@ -88,7 +93,7 @@ def homological_complex_to_dgo :
     differential_object (graded_object_with_shift b V) :=
 { obj := λ X,
   { X := λ i, X.X i,
-    d := λ i, X.d i (i + b),
+    d := λ i, X.d i (i + 1 • b),
     d_squared' := by { ext i, dsimp, simp, } },
   map := λ X Y f,
   { f := f.f,
@@ -117,13 +122,15 @@ nat_iso.of_components (λ X,
     { f := λ i, 𝟙 (X.X i),
       comm' := λ i j h, begin
         dsimp at h ⊢, subst h,
-        simp only [category.comp_id, category.id_comp, dif_pos rfl, eq_to_hom_refl],
+        delta homological_complex_to_dgo,
+        simp,
       end },
     inv :=
     { f := λ i, 𝟙 (X.X i),
       comm' := λ i j h, begin
         dsimp at h ⊢, subst h,
-        simp only [category.comp_id, category.id_comp, dif_pos rfl, eq_to_hom_refl],
+        delta homological_complex_to_dgo,
+        simp,
       end }, }) (by tidy)
 
 /--

src/category_theory/differential_object.lean

@@ -25,7 +25,8 @@ namespace category_theory
 
 variables (C : Type u) [category.{v} C]
 
-variables [has_zero_morphisms C] [has_shift C]
+-- TODO: generaize to `has_shift C A` for an arbitrary `[add_monoid A]` `[has_one A]`.
+variables [has_zero_morphisms C] [has_shift C ℤ]
 
 /--
 A differential object in a category with zero morphisms and a shift is
@@ -126,7 +127,7 @@ from an isomorphism of the underlying objects that commutes with the differentia
   (f : X.X ≅ Y.X) (hf : X.d ≫ f.hom⟦1⟧' = f.hom ≫ Y.d) : X ≅ Y :=
 { hom := ⟨f.hom, hf⟩,
   inv := ⟨f.inv, by { dsimp, rw [← functor.map_iso_inv, iso.comp_inv_eq, category.assoc,
-    iso.eq_inv_comp, functor.map_iso_hom, ← hf], congr }⟩,
+    iso.eq_inv_comp, functor.map_iso_hom, hf] }⟩,
   hom_inv_id' := by { ext1, dsimp, exact f.hom_inv_id },
   inv_hom_id' := by { ext1, dsimp, exact f.inv_hom_id } }
 
@@ -136,20 +137,21 @@ namespace functor
 
 universes v' u'
 variables (D : Type u') [category.{v'} D]
-variables [has_zero_morphisms D] [has_shift D]
+variables [has_zero_morphisms D] [has_shift D ℤ]
 
 /--
 A functor `F : C ⥤ D` which commutes with shift functors on `C` and `D` and preserves zero morphisms
 can be lifted to a functor `differential_object C ⥤ differential_object D`.
 -/
 @[simps]
-def map_differential_object (F : C ⥤ D) (η : (shift C).functor.comp F ⟶ F.comp (shift D).functor)
+def map_differential_object (F : C ⥤ D)
+  (η : (shift_functor C (1:ℤ)).comp F ⟶ F.comp (shift_functor D (1:ℤ)))
   (hF : ∀ c c', F.map (0 : c ⟶ c') = 0) :
   differential_object C ⥤ differential_object D :=
 { obj := λ X, { X := F.obj X.X,
     d := F.map X.d ≫ η.app X.X,
     d_squared' := begin
-      dsimp, rw [functor.map_comp, ← functor.comp_map F (shift D).functor],
+      rw [functor.map_comp, ← functor.comp_map F (shift_functor D (1:ℤ))],
       slice_lhs 2 3 { rw [← η.naturality X.d] },
       rw [functor.comp_map],
       slice_lhs 1 2 { rw [← F.map_comp, X.d_squared, hF] },
@@ -158,7 +160,7 @@ def map_differential_object (F : C ⥤ D) (η : (shift C).functor.comp F ⟶ F.c
   map := λ X Y f, { f := F.map f.f,
     comm' := begin
       dsimp,
-      slice_lhs 2 3 { rw [← functor.comp_map F (shift D).functor, ← η.naturality f.f] },
+      slice_lhs 2 3 { rw [← functor.comp_map F (shift_functor D (1:ℤ)), ← η.naturality f.f] },
       slice_lhs 1 2 { rw [functor.comp_map, ← F.map_comp, f.comm, F.map_comp] },
       rw [category.assoc]
     end },
@@ -175,7 +177,7 @@ namespace differential_object
 
 variables (C : Type u) [category.{v} C]
 
-variables [has_zero_object C] [has_zero_morphisms C] [has_shift C]
+variables [has_zero_object C] [has_zero_morphisms C] [has_shift C ℤ]
 
 open_locale zero_object
 
@@ -191,7 +193,7 @@ end differential_object
 namespace differential_object
 
 variables (C : Type (u+1)) [large_category C] [concrete_category C]
-  [has_zero_morphisms C] [has_shift C]
+  [has_zero_morphisms C] [has_shift C ℤ]
 
 instance concrete_category_of_differential_objects :
   concrete_category (differential_object C) :=
@@ -206,132 +208,54 @@ end differential_object
 namespace differential_object
 
 variables (C : Type u) [category.{v} C]
-variables [has_zero_morphisms C] [has_shift C]
+variables [has_zero_morphisms C] [has_shift C ℤ]
+
+noncomputable theory
 
 /-- The shift functor on `differential_object C`. -/
 @[simps]
-def shift_functor : differential_object C ⥤ differential_object C :=
+def shift_functor (n : ℤ) : differential_object C ⥤ differential_object C :=
 { obj := λ X,
-  { X := X.X⟦1⟧,
-    d := X.d⟦1⟧',
-    d_squared' := begin
-      dsimp,
-      rw [←functor.map_comp, X.d_squared, is_equivalence_preserves_zero_morphisms],
-    end },
-  map := λ X Y f,
-  { f := f.f⟦1⟧',
-    comm' := begin dsimp, rw [←functor.map_comp, f.comm, ←functor.map_comp], end, }, }
-
-/-- The inverse shift functor on `differential C`, at the level of objects. -/
-@[simps]
-def shift_inverse_obj : differential_object C → differential_object C :=
-λ X,
-{ X := X.X⟦-1⟧,
-  d := X.d⟦-1⟧' ≫ (shift C).unit_inv.app X.X ≫ (shift C).counit_inv.app X.X,
-  d_squared' := begin
-    dsimp,
-    rw functor.map_comp,
-    slice_lhs 3 4 { erw ←(shift C).counit_inv.naturality, },
-    slice_lhs 2 3 { erw ←(shift C).unit_inv.naturality, },
-    slice_lhs 1 2 { erw [←functor.map_comp, X.d_squared], },
-    simp,
-  end, }
-
-/-- The inverse shift functor on `differential C`. -/
-@[simps]
-def shift_inverse : differential_object C ⥤ differential_object C :=
-{ obj := shift_inverse_obj C,
+  { X := X.X⟦n⟧,
+    d := X.d⟦n⟧' ≫ (shift_comm _ _ _).hom,
+    d_squared' := by rw [functor.map_comp, category.assoc, shift_comm_hom_comp_assoc,
+        ←functor.map_comp_assoc, X.d_squared, is_equivalence_preserves_zero_morphisms, zero_comp] },
   map := λ X Y f,
-  { f := f.f⟦-1⟧',
-    comm' := begin
-      dsimp,
-      slice_lhs 3 4 { erw ←(shift C).counit_inv.naturality, },
-      slice_lhs 2 3 { erw ←(shift C).unit_inv.naturality, },
-      slice_lhs 1 2 { erw [←functor.map_comp, f.comm, functor.map_comp], },
-      rw [category.assoc, category.assoc],
-    end, }, }.
-
-/-- The unit for the shift functor on `differential_object C`. -/
-@[simps]
-def shift_unit : 𝟭 (differential_object C) ⟶ shift_functor C ⋙ shift_inverse C :=
-{ app := λ X,
-  { f := (shift C).unit.app X.X,
-    comm' := begin
-      dsimp,
-      slice_rhs 1 2 { erw ←(shift C).unit.naturality, },
-      simp only [category.comp_id, functor.id_map, iso.hom_inv_id_app,
-        category.assoc, equivalence.counit_inv_app_functor],
-    end, }, }
-
-/-- The inverse of the unit for the shift functor on `differential_object C`. -/
+  { f := f.f⟦n⟧',
+    comm' := by { dsimp, rw [category.assoc, shift_comm_hom_comp, ← functor.map_comp_assoc,
+      f.comm, functor.map_comp_assoc], }, },
+  map_id' := by { intros X, ext1, dsimp, rw functor.map_id },
+  map_comp' := by { intros X Y Z f g, ext1, dsimp, rw functor.map_comp } }
+
+local attribute [instance] endofunctor_monoidal_category discrete.add_monoidal
+local attribute [reducible] endofunctor_monoidal_category discrete.add_monoidal shift_comm
+
+/-- The shift functor on `differential_object C` is additive. -/
+@[simps] def shift_functor_add (m n : ℤ) :
+  shift_functor C (m + n) ≅ shift_functor C m ⋙ shift_functor C n :=
+begin
+  refine nat_iso.of_components (λ X, mk_iso (shift_add X.X _ _) _) _,
+  { dsimp,
+    simp only [obj_μ_app, μ_naturality_assoc, μ_naturalityₗ_assoc, μ_inv_hom_app_assoc,
+      category.assoc, obj_μ_inv_app, functor.map_comp, μ_inv_naturalityᵣ_assoc],
+    simp [opaque_eq_to_iso] },
+  { intros X Y f, ext, dsimp, exact nat_trans.naturality _ _ }
+end
+
+/-- The shift by zero is naturally isomorphic to the identity. -/
 @[simps]
-def shift_unit_inv : shift_functor C ⋙ shift_inverse C ⟶ 𝟭 (differential_object C) :=
-{ app := λ X,
-  { f := (shift C).unit_inv.app X.X,
-    comm' := begin
-      dsimp,
-      slice_rhs 1 2 { erw ←(shift C).unit_inv.naturality, },
-      rw [equivalence.counit_inv_app_functor],
-      slice_lhs 3 4 { rw ←functor.map_comp, },
-      simp only [iso.hom_inv_id_app, functor.comp_map, iso.hom_inv_id_app_assoc,
-        nat_iso.cancel_nat_iso_inv_left, equivalence.inv_fun_map, category.assoc],
-      dsimp,
-      rw category_theory.functor.map_id,
-    end, }, }.
-
-/-- The unit isomorphism for the shift functor on `differential_object C`. -/
-@[simps]
-def shift_unit_iso : 𝟭 (differential_object C) ≅ shift_functor C ⋙ shift_inverse C :=
-{ hom := shift_unit C,
-  inv := shift_unit_inv C, }.
-
-/-- The counit for the shift functor on `differential_object C`. -/
-@[simps]
-def shift_counit : shift_inverse C ⋙ shift_functor C ⟶ 𝟭 (differential_object C) :=
-{ app := λ X,
-  { f := (shift C).counit.app X.X,
-    comm' :=
-    begin
-      dsimp,
-      slice_rhs 1 2 { erw ←(shift C).counit.naturality, },
-      rw [(shift C).functor.map_comp, (shift C).functor.map_comp],
-      slice_lhs 3 4 { erw [←functor.map_comp, iso.inv_hom_id_app, functor.map_id], },
-      erw equivalence.counit_app_functor,
-      rw category.comp_id,
-      refl,
-    end, }, }
-
-/-- The inverse of the counit for the shift functor on `differential_object C`. -/
-@[simps]
-def shift_counit_inv : 𝟭 (differential_object C) ⟶ shift_inverse C ⋙ shift_functor C :=
-{ app := λ X,
-  { f := (shift C).counit_inv.app X.X,
-    comm' :=
-    begin
-      dsimp,
-      rw [(shift C).functor.map_comp, (shift C).functor.map_comp],
-      slice_rhs 1 2 { erw ←(shift C).counit_inv.naturality, },
-      rw ←equivalence.counit_app_functor,
-      slice_rhs 2 3 { rw iso.inv_hom_id_app, },
-      rw category.id_comp,
-      refl,
-    end, }, }
-
-/-- The counit isomorphism for the shift functor on `differential_object C`. -/
-@[simps]
-def shift_counit_iso : shift_inverse C ⋙ shift_functor C ≅ 𝟭 (differential_object C) :=
-{ hom := shift_counit C,
-  inv := shift_counit_inv C, }
-
-/--
-The category of differential objects in `C` itself has a shift functor.
--/
-instance : has_shift (differential_object C) :=
-{ shift :=
-  { functor := shift_functor C,
-    inverse := shift_inverse C,
-    unit_iso := shift_unit_iso C,
-    counit_iso := shift_counit_iso C, } }
+def shift_ε : 𝟭 (differential_object C) ≅ shift_functor C 0 :=
+begin
+  refine nat_iso.of_components (λ X, mk_iso ((shift_monoidal_functor C ℤ).ε_iso.app X.X) _) _,
+  { dsimp, simp, dsimp, simp },
+  { introv, ext, dsimp, simp }
+end
+
+instance : has_shift (differential_object C) ℤ :=
+has_shift_mk _ _
+{ F := shift_functor C,
+  ε := shift_ε C,
+  μ := λ m n, (shift_functor_add C m n).symm }
 
 end differential_object
 

src/category_theory/graded_object.lean

@@ -83,8 +83,8 @@ begin
 end
 
 @[simp] lemma eq_to_hom_apply {β : Type w} {X Y : Π b : β, C} (h : X = Y) (b : β) :
-   (eq_to_hom h : X ⟶ Y) b = eq_to_hom (by subst h) :=
- by { subst h, refl }
+  (eq_to_hom h : X ⟶ Y) b = eq_to_hom (by subst h) :=
+by { subst h, refl }
 
 /--
 The equivalence between β-graded objects and γ-graded objects,
@@ -101,21 +101,26 @@ def comap_equiv {β γ : Type w} (e : β ≃ γ) :
 
 end
 
+local attribute [reducible, instance] endofunctor_monoidal_category discrete.add_monoidal
+
 instance has_shift {β : Type*} [add_comm_group β] (s : β) :
-  has_shift (graded_object_with_shift s C) :=
-{ shift := comap_equiv C
-  { to_fun := λ b, b-s,
-    inv_fun := λ b, b+s,
-    left_inv := λ x, (by simp),
-    right_inv := λ x, (by simp), } }
-
-@[simp] lemma shift_functor_obj_apply {β : Type*} [add_comm_group β] (s : β) (X : β → C) (t : β) :
-  (shift (graded_object_with_shift s C)).functor.obj X t = X (t + s) :=
+  has_shift (graded_object_with_shift s C) ℤ :=
+has_shift_mk _ _
+{ F := λ n, comap (λ _, C) $ λ (b : β), b + n • s,
+  ε := (comap_id β (λ _, C)).symm ≪≫ (comap_eq C (by { ext, simp })),
+  μ := λ m n, comap_comp _ _ _ ≪≫ comap_eq C (by { ext, simp [add_zsmul, add_comm] }),
+  left_unitality := by { introv, ext, dsimp, simpa },
+  right_unitality := by { introv, ext, dsimp, simpa },
+  associativity := by { introv, ext, dsimp, simp } }
+
+@[simp] lemma shift_functor_obj_apply {β : Type*} [add_comm_group β]
+  (s : β) (X : β → C) (t : β) (n : ℤ) :
+  (shift_functor (graded_object_with_shift s C) n).obj X t = X (t + n • s) :=
 rfl
 
 @[simp] lemma shift_functor_map_apply {β : Type*} [add_comm_group β] (s : β)
-  {X Y : graded_object_with_shift s C} (f : X ⟶ Y) (t : β) :
-  (shift (graded_object_with_shift s C)).functor.map f t = f (t + s) :=
+  {X Y : graded_object_with_shift s C} (f : X ⟶ Y) (t : β) (n : ℤ) :
+  (shift_functor (graded_object_with_shift s C) n).map f t = f (t + n • s) :=
 rfl
 
 instance has_zero_morphisms [has_zero_morphisms C] (β : Type w) :