feat(CategoryTheory/Shift/Adjunction): commutation with shifts and ad…

…junctions, part 2 (leanprover-community#20273)

Given categories `C` and `D` that have shifts by an additive group `A`, functors `F : C ⥤ D` and `G : C ⥤ D`, an adjunction `F ⊣ G` and a `CommShift` structure on `G`, this file constructs a `CommShift` structure on `F`. This is a sequel to PR leanprover-community#20033, which was doing the construction in the other direction.

Mathlib/CategoryTheory/Shift/Adjunction.lean

@@ -11,11 +11,15 @@ import Mathlib.CategoryTheory.Adjunction.Mates
 
 Given categories `C` and `D` that have shifts by an additive group `A`, functors `F : C ⥤ D`
 and `G : C ⥤ D`, an adjunction `F ⊣ G` and a `CommShift` structure on `F`, this file constructs
-a `CommShift` structure on `G`. As an easy application, if `E : C ≌ D` is an equivalence and
-`E.functor` has a `CommShift` structure, we get a `CommShift` structure on `E.inverse`.
-
-The `CommShift` structure on `G` must be compatible with the one on `F` in the following sense
-(cf. `Adjunction.CommShift`):
+a `CommShift` structure on `G`. We also do the construction in the other direction: given a
+`CommShift` structure on `G`, we construct a `CommShift` structure on `G`; we could do this
+using opposite categories, but the construction is simple enough that it is not really worth it.
+As an easy application, if `E : C ≌ D` is an equivalence and `E.functor` has a `CommShift`
+structure, we get a `CommShift` structure on `E.inverse`.
+
+We now explain the construction of a `CommShift` structure on `G` given a `CommShift` structure
+on `F`; the other direction is similar. The `CommShift` structure on `G` must be compatible with
+the one on `F` in the following sense (cf. `Adjunction.CommShift`):
 for every `a` in `A`, the natural transformation `adj.unit : 𝟭 C ⟶ G ⋙ F` commutes with
 the isomorphism `shiftFunctor C A ⋙ G ⋙ F ≅ G ⋙ F ⋙ shiftFunctor C A` induces by
 `F.commShiftIso a` and `G.commShiftIso a`. We actually require a similar condition for
@@ -37,9 +41,6 @@ Once we have established all this, the compatibility of the commutation isomorph
 `F` expressed in `CommShift.zero` and `CommShift.add` immediately implies the similar
 statements for the commutation isomorphisms for `G`.
 
-TODO: Construct a `CommShift` structure on `F` from a `CommShift` structure on `G`, using
-opposite categories.
-
 -/
 
 namespace CategoryTheory
@@ -142,12 +143,13 @@ lemma compatibilityUnit_unique_right (h : CompatibilityUnit adj e₁ e₂)
 /-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
 `e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
 `e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
-counit of the adjunction `adj`, then `e₂` uniquely determines `e₁`.
+unit of the adjunction `adj`, then `e₂` uniquely determines `e₁`.
 -/
-lemma compatibilityCounit_unique_left (h : CompatibilityCounit adj e₁ e₂)
-    (h' : CompatibilityCounit adj e₁' e₂) : e₁ = e₁' := by
+lemma compatibilityUnit_unique_left (h : CompatibilityUnit adj e₁ e₂)
+    (h' : CompatibilityUnit adj e₁' e₂) : e₁ = e₁' := by
   ext
-  rw [compatibilityCounit_left adj e₁ e₂ h, compatibilityCounit_left adj e₁' e₂ h']
+  rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
+    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]
 
 /--
 The isomorphisms `Functor.CommShift.isoZero F` and `Functor.CommShift.isoZero G` are
@@ -271,8 +273,7 @@ lemma iso_hom_app (X : D) :
               (G.map ((shiftFunctorCompIsoId D a b
                 (by rw [← add_left_inj a, add_assoc, h, zero_add, add_zero])).hom.app X))⟦a⟧' := by
   obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]
-  simp [iso, iso']
-  rfl
+  simp [iso, iso', shiftEquiv']
 
 @[reassoc]
 lemma iso_inv_app (Y : D) :
@@ -327,12 +328,12 @@ the unique compatible `CommShift` structure on `G`.
 noncomputable def rightAdjointCommShift [F.CommShift A] : G.CommShift A where
   iso a := iso adj a
   zero := by
-    refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0)  _ _
+    refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0) _ _
       (compatibilityUnit_iso adj 0) ?_
     rw [F.commShiftIso_zero]
     exact CommShift.compatibilityUnit_isoZero adj
   add a b := by
-    refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b))  _ _
+    refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _
       (compatibilityUnit_iso adj (a + b)) ?_
     rw [F.commShiftIso_add]
     exact CommShift.compatibilityUnit_isoAdd adj _ _ _ _
@@ -348,6 +349,90 @@ lemma commShift_of_leftAdjoint [F.CommShift A] :
   simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
     Functor.commShiftIso_comp_hom_app] using RightAdjointCommShift.compatibilityUnit_iso adj a X
 
+namespace LeftAdjointCommShift
+
+variable {A} (a b : A) (h : a + b = 0) [G.CommShift A]
+
+/-- Auxiliary definition for `iso`. -/
+noncomputable def iso' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a :=
+  (conjugateIsoEquiv (Adjunction.comp adj (shiftEquiv' D a b h).toAdjunction)
+    (Adjunction.comp (shiftEquiv' C a b h).toAdjunction adj)).invFun (G.commShiftIso b)
+
+/--
+Given an adjunction `F ⊣ G` and a `CommShift` structure on `G`, these are the candidate
+`CommShift.iso a` isomorphisms for a compatible `CommShift` structure on `F`.
+-/
+noncomputable def iso : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a :=
+  iso' adj _ _ (add_neg_cancel a)
+
+@[reassoc]
+lemma iso_hom_app (X : C) :
+    (iso adj a).hom.app X = F.map ((adj.unit.app X)⟦a⟧') ≫
+      F.map (G.map (((shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))⟦a⟧') ≫
+        F.map (((G.commShiftIso b).hom.app ((F.obj X)⟦a⟧))⟦a⟧') ≫
+          F.map ((shiftFunctorCompIsoId C b a (by simp [eq_neg_of_add_eq_zero_left h])).hom.app
+            (G.obj ((F.obj X)⟦a⟧))) ≫ adj.counit.app ((F.obj X)⟦a⟧) := by
+  obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
+  simp [iso, iso', shiftEquiv']
+
+@[reassoc]
+lemma iso_inv_app (Y : C) :
+    (iso adj a).inv.app Y = (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y))⟦a⟧' ≫
+      (F.map ((adj.unit.app (Y⟦a⟧))⟦b⟧'))⟦a⟧' ≫ (F.map ((G.commShiftIso b).inv.app
+        (F.obj (Y⟦a⟧))))⟦a⟧' ≫ (adj.counit.app ((F.obj (Y⟦a⟧))⟦b⟧))⟦a⟧' ≫
+          (shiftFunctorCompIsoId D b a (by simp [eq_neg_of_add_eq_zero_left h])).hom.app
+            (F.obj (Y⟦a⟧)) := by
+  obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
+  simp [iso, iso', shiftEquiv']
+
+/--
+The commutation isomorphisms of `Adjunction.LeftAdjointCommShift.iso` are compatible with
+the unit of the adjunction.
+-/
+lemma compatibilityUnit_iso (a : A) :
+    CommShift.CompatibilityUnit adj (iso adj a) (G.commShiftIso a) := by
+  intro
+  rw [LeftAdjointCommShift.iso_hom_app adj _ _ (add_neg_cancel a)]
+  simp only [Functor.id_obj, Functor.comp_obj, Functor.map_shiftFunctorCompIsoId_inv_app,
+    Functor.map_comp, assoc, unit_naturality_assoc, right_triangle_components_assoc]
+  slice_rhs 4 5 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
+  simp only [Functor.comp_obj, Functor.map_id, id_comp]
+  rw [shift_shiftFunctorCompIsoId_inv_app, ← Functor.comp_map,
+    (shiftFunctorCompIsoId C _ _ (neg_add_cancel a)).hom.naturality_assoc]
+  simp
+
+end LeftAdjointCommShift
+
+open LeftAdjointCommShift in
+/--
+Given an adjunction `F ⊣ G` and a `CommShift` structure on `G`, this constructs
+the unique compatible `CommShift` structure on `F`.
+-/
+@[simps]
+noncomputable def leftAdjointCommShift [G.CommShift A] : F.CommShift A where
+  iso a := iso adj a
+  zero := by
+    refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso 0)
+      (compatibilityUnit_iso adj 0) ?_
+    rw [G.commShiftIso_zero]
+    exact CommShift.compatibilityUnit_isoZero adj
+  add a b := by
+    refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso (a + b))
+      (compatibilityUnit_iso adj (a + b)) ?_
+    rw [G.commShiftIso_add]
+    exact CommShift.compatibilityUnit_isoAdd adj _ _ _ _
+      (compatibilityUnit_iso adj a) (compatibilityUnit_iso adj b)
+
+lemma commShift_of_rightAdjoint [G.CommShift A] :
+    letI := adj.leftAdjointCommShift A
+    adj.CommShift A := by
+  letI := adj.leftAdjointCommShift A
+  refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩
+  ext X
+  dsimp
+  simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
+    Functor.commShiftIso_comp_hom_app] using LeftAdjointCommShift.compatibilityUnit_iso adj a X
+
 end Adjunction
 
 namespace Equivalence