Adjoints commute with shifts

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. 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 adj.counit, but it follows from the one for adj.unit.

In order to simplify the construction of the CommShift structure on G, we first introduce the compatibility condition on adj.unit for a fixed a in A and for isomorphisms e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a and e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a. We then prove that:

• If e₁ and e₂ satisfy this condition, then e₁ uniquely determines e₂ and vice versa.
• If a = 0, the isomorphisms Functor.CommShift.isoZero F and Functor.CommShift.isoZero G satisfy the condition.
• The condition is stable by addition on A, if we use Functor.CommShift.isoAdd to deduce commutation isomorphism for a + b from such isomorphism from a and b.
• Given commutation isomorphisms for F, our candidate commutation isomorphisms for G, constructed in Adjunction.RightAdjointCommShift.iso, satisfy the compatibility condition.

Once we have established all this, the compatibility of the commutation isomorphism for F expressed in CommShift.zero and CommShift.add immediately implies the similar statements for the commutation isomorphisms for G.

@[reducible, inline]

abbrev CategoryTheory.Adjunction.CommShift.CompatibilityUnit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) : Prop

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, this expresses the compatibility of e₁ and e₂ with the unit of the adjunction adj.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Adjunction.CommShift.CompatibilityCounit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) : Prop

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, this expresses the compatibility of e₁ and e₂ with the counit of the adjunction adj.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Adjunction.CommShift.compatibilityCounit_of_compatibilityUnit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) (h : CompatibilityUnit adj e₁ e₂) : CompatibilityCounit 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, compatibility of e₁ and e₂ with the unit of the adjunction adj implies compatibility with the counit of adj.

theorem CategoryTheory.Adjunction.CommShift.compatibilityUnit_right {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) (h : CompatibilityUnit adj e₁ e₂) (Y : D) : e₂.inv.app Y = CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj (G.obj Y))) (CategoryStruct.comp (G.map (e₁.hom.app (G.obj Y))) (G.map ((shiftFunctor D a).map (adj.counit.app Y))))

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 unit of the adjunction adj, then we get a formula for e₂.inv in terms of e₁.

theorem CategoryTheory.Adjunction.CommShift.compatibilityCounit_left {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) (h : CompatibilityCounit adj e₁ e₂) (X : C) : e₁.hom.app X = CategoryStruct.comp (F.map ((shiftFunctor C a).map (adj.unit.app X))) (CategoryStruct.comp (F.map (e₂.inv.app (F.obj X))) (adj.counit.app ((shiftFunctor D a).obj (F.obj X))))

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 we get a formula for e₁.hom in terms of e₂.

theorem CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_right {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ e₂' : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) (h : CompatibilityUnit adj e₁ e₂) (h' : CompatibilityUnit adj e₁ e₂') : 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 unit of the adjunction adj, then e₁ uniquely determines e₂.

theorem CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_left {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a : A} (e₁ e₁' : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) (h : CompatibilityUnit adj e₁ e₂) (h' : CompatibilityUnit adj e₁' e₂) : 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 unit of the adjunction adj, then e₂ uniquely determines e₁.

theorem CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoZero {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] : CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)

The isomorphisms Functor.CommShift.isoZero F and Functor.CommShift.isoZero G are compatible with the unit of an adjunction F ⊣ G.

theorem CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoAdd {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] {a b : A} (e₁ : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)) (f₁ : (shiftFunctor C b).comp F ≅ F.comp (shiftFunctor D b)) (e₂ : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)) (f₂ : (shiftFunctor D b).comp G ≅ G.comp (shiftFunctor C b)) (h : CompatibilityUnit adj e₁ e₂) (h' : CompatibilityUnit adj f₁ f₂) : CompatibilityUnit adj (Functor.CommShift.isoAdd e₁ f₁) (Functor.CommShift.isoAdd e₂ f₂)

Given an adjunction adj : F ⊣ G, a, b in A and commutation isomorphisms between shifts by a (resp. b) and F and G, if these commutation isomorphisms are compatible with the unit of adj, then so are the commutation isomorphisms between shifts by a + b and F and G constructed by Functor.CommShift.isoAdd.

class CategoryTheory.Adjunction.CommShift {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] : Prop

The property for CommShift structures on F and G to be compatible with an adjunction F ⊣ G.

• commShift_unit : NatTrans.CommShift adj.unit A
• commShift_counit : NatTrans.CommShift adj.counit A

@[simp]

theorem CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (X : C) : CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj X)) (((F.comp G).commShiftIso a).hom.app X) = (shiftFunctor C a).map (adj.unit.app X)

@[simp]

theorem CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (X : C) {Z : C} (h : (shiftFunctor C a).obj (G.obj (F.obj X)) ⟶ Z) : CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (((F.comp G).commShiftIso a).hom.app X) h) = CategoryStruct.comp ((shiftFunctor C a).map (adj.unit.app X)) h

@[simp]

theorem CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (X : C) : CategoryStruct.comp ((shiftFunctor C a).map (adj.unit.app X)) (((F.comp G).commShiftIso a).inv.app X) = adj.unit.app ((shiftFunctor C a).obj X)

@[simp]

theorem CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (X : C) {Z : C} (h : G.obj (F.obj ((shiftFunctor C a).obj X)) ⟶ Z) : CategoryStruct.comp ((shiftFunctor C a).map (adj.unit.app X)) (CategoryStruct.comp (((F.comp G).commShiftIso a).inv.app X) h) = CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj X)) h

@[simp]

theorem CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (Y : D) : CategoryStruct.comp (((G.comp F).commShiftIso a).hom.app Y) ((shiftFunctor D a).map (adj.counit.app Y)) = adj.counit.app ((shiftFunctor D a).obj Y)

@[simp]

theorem CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (Y : D) {Z : D} (h : (shiftFunctor D a).obj Y ⟶ Z) : CategoryStruct.comp (((G.comp F).commShiftIso a).hom.app Y) (CategoryStruct.comp ((shiftFunctor D a).map (adj.counit.app Y)) h) = CategoryStruct.comp (adj.counit.app ((shiftFunctor D a).obj Y)) h

@[simp]

theorem CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (Y : D) : CategoryStruct.comp (((G.comp F).commShiftIso a).inv.app Y) (adj.counit.app ((shiftFunctor D a).obj Y)) = (shiftFunctor D a).map (adj.counit.app Y)

@[simp]

theorem CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (Y : D) {Z : D} (h : (shiftFunctor D a).obj Y ⟶ Z) : CategoryStruct.comp (((G.comp F).commShiftIso a).inv.app Y) (CategoryStruct.comp (adj.counit.app ((shiftFunctor D a).obj Y)) h) = CategoryStruct.comp ((shiftFunctor D a).map (adj.counit.app Y)) h

theorem CategoryTheory.Adjunction.CommShift.mk' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] (h : NatTrans.CommShift adj.unit A) : adj.CommShift A

Constructor for Adjunction.CommShift.

instance CategoryTheory.Adjunction.CommShift.instId {C : Type u_1} [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [HasShift C A] : id.CommShift A

The identity adjunction is compatible with the trivial CommShift structure on the identity functor.

instance CategoryTheory.Adjunction.CommShift.instComp {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] {E : Type u_4} [Category.{u_6, u_4} E] {F' : Functor D E} {G' : Functor E D} (adj' : F' ⊣ G') [HasShift E A] [F'.CommShift A] [G'.CommShift A] [adj.CommShift A] [adj'.CommShift A] : (adj.comp adj').CommShift A

Compatibility of Adjunction.Commshift with the composition of adjunctions.

theorem CategoryTheory.Adjunction.shift_unit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (X : C) : (shiftFunctor C a).map (adj.unit.app X) = CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (G.map ((F.commShiftIso a).hom.app X)) ((G.commShiftIso a).hom.app (F.obj X)))

theorem CategoryTheory.Adjunction.shift_unit_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (X : C) {Z : C} (h : (shiftFunctor C a).obj (G.obj (F.obj X)) ⟶ Z) : CategoryStruct.comp ((shiftFunctor C a).map (adj.unit.app X)) h = CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (G.map ((F.commShiftIso a).hom.app X)) (CategoryStruct.comp ((G.commShiftIso a).hom.app (F.obj X)) h))

theorem CategoryTheory.Adjunction.shift_counit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (Y : D) : (shiftFunctor D a).map (adj.counit.app Y) = CategoryStruct.comp ((F.commShiftIso a).inv.app (G.obj Y)) (CategoryStruct.comp (F.map ((G.commShiftIso a).inv.app Y)) (adj.counit.app ((shiftFunctor D a).obj Y)))

theorem CategoryTheory.Adjunction.shift_counit_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddMonoid A] [HasShift C A] [HasShift D A] [F.CommShift A] [G.CommShift A] [adj.CommShift A] (a : A) (Y : D) {Z : D} (h : (shiftFunctor D a).obj Y ⟶ Z) : CategoryStruct.comp ((shiftFunctor D a).map (adj.counit.app Y)) h = CategoryStruct.comp ((F.commShiftIso a).inv.app (G.obj Y)) (CategoryStruct.comp (F.map ((G.commShiftIso a).inv.app Y)) (CategoryStruct.comp (adj.counit.app ((shiftFunctor D a).obj Y)) h))

noncomputable def CategoryTheory.Adjunction.RightAdjointCommShift.iso' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)

Auxiliary definition for iso.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Adjunction.RightAdjointCommShift.iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a : A) [F.CommShift A] : (shiftFunctor D a).comp G ≅ G.comp (shiftFunctor C a)

Given an adjunction F ⊣ G and a CommShift structure on F, these are the candidate CommShift.iso a isomorphisms for a compatible CommShift structure on G.

Equations

• CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a = CategoryTheory.Adjunction.RightAdjointCommShift.iso' adj a (-a) ⋯

theorem CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (X : D) : (iso adj a).hom.app X = CategoryStruct.comp ((shiftFunctorCompIsoId C b a h).inv.app (G.obj ((shiftFunctor D a).obj X))) (CategoryStruct.comp ((shiftFunctor C a).map (adj.unit.app ((shiftFunctor C b).obj (G.obj ((shiftFunctor D a).obj X))))) (CategoryStruct.comp ((shiftFunctor C a).map (G.map ((F.commShiftIso b).hom.app (G.obj ((shiftFunctor D a).obj X))))) (CategoryStruct.comp ((shiftFunctor C a).map (G.map ((shiftFunctor D b).map (adj.counit.app ((shiftFunctor D a).obj X))))) ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b ⋯).hom.app X))))))

theorem CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (X : D) {Z : C} (h✝ : (shiftFunctor C a).obj (G.obj X) ⟶ Z) : CategoryStruct.comp ((iso adj a).hom.app X) h✝ = CategoryStruct.comp ((shiftFunctorCompIsoId C b a h).inv.app (G.obj ((shiftFunctor D a).obj X))) (CategoryStruct.comp ((shiftFunctor C a).map (adj.unit.app ((shiftFunctor C b).obj (G.obj ((shiftFunctor D a).obj X))))) (CategoryStruct.comp ((shiftFunctor C a).map (G.map ((F.commShiftIso b).hom.app (G.obj ((shiftFunctor D a).obj X))))) (CategoryStruct.comp ((shiftFunctor C a).map (G.map ((shiftFunctor D b).map (adj.counit.app ((shiftFunctor D a).obj X))))) (CategoryStruct.comp ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b ⋯).hom.app X))) h✝))))

theorem CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (Y : D) : (iso adj a).inv.app Y = CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj (G.obj Y))) (CategoryStruct.comp (G.map ((shiftFunctorCompIsoId D b a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y))))) (CategoryStruct.comp (G.map ((shiftFunctor D a).map ((shiftFunctor D b).map ((F.commShiftIso a).hom.app (G.obj Y))))) (CategoryStruct.comp (G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y))))) (G.map ((shiftFunctor D a).map (adj.counit.app Y))))))

theorem CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (Y : D) {Z : C} (h✝ : G.obj ((shiftFunctor D a).obj Y) ⟶ Z) : CategoryStruct.comp ((iso adj a).inv.app Y) h✝ = CategoryStruct.comp (adj.unit.app ((shiftFunctor C a).obj (G.obj Y))) (CategoryStruct.comp (G.map ((shiftFunctorCompIsoId D b a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y))))) (CategoryStruct.comp (G.map ((shiftFunctor D a).map ((shiftFunctor D b).map ((F.commShiftIso a).hom.app (G.obj Y))))) (CategoryStruct.comp (G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y))))) (CategoryStruct.comp (G.map ((shiftFunctor D a).map (adj.counit.app Y))) h✝))))

theorem CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] [F.CommShift A] (a : A) : CommShift.CompatibilityUnit adj (F.commShiftIso a) (iso adj a)

The commutation isomorphisms of Adjunction.RightAdjointCommShift.iso are compatible with the unit of the adjunction.

noncomputable def CategoryTheory.Adjunction.rightAdjointCommShift {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [F.CommShift A] : G.CommShift A

Given an adjunction F ⊣ G and a CommShift structure on F, this constructs the unique compatible CommShift structure on G.

Equations

• adj.rightAdjointCommShift A = { iso := fun (a : A) => CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a, zero := ⋯, add := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointCommShift_iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [F.CommShift A] (a : A) : Functor.CommShift.iso a = RightAdjointCommShift.iso adj a

theorem CategoryTheory.Adjunction.commShift_of_leftAdjoint {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [F.CommShift A] : adj.CommShift A

noncomputable def CategoryTheory.Adjunction.LeftAdjointCommShift.iso' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)

Auxiliary definition for iso.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Adjunction.LeftAdjointCommShift.iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a : A) [G.CommShift A] : (shiftFunctor C a).comp F ≅ F.comp (shiftFunctor D a)

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.

Equations

• CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a = CategoryTheory.Adjunction.LeftAdjointCommShift.iso' adj a (-a) ⋯

theorem CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (X : C) : (iso adj a).hom.app X = CategoryStruct.comp (F.map ((shiftFunctor C a).map (adj.unit.app X))) (CategoryStruct.comp (F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b h).inv.app (F.obj X))))) (CategoryStruct.comp (F.map ((shiftFunctor C a).map ((G.commShiftIso b).hom.app ((shiftFunctor D a).obj (F.obj X))))) (CategoryStruct.comp (F.map ((shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X))))) (adj.counit.app ((shiftFunctor D a).obj (F.obj X))))))

theorem CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (X : C) {Z : D} (h✝ : (shiftFunctor D a).obj (F.obj X) ⟶ Z) : CategoryStruct.comp ((iso adj a).hom.app X) h✝ = CategoryStruct.comp (F.map ((shiftFunctor C a).map (adj.unit.app X))) (CategoryStruct.comp (F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b h).inv.app (F.obj X))))) (CategoryStruct.comp (F.map ((shiftFunctor C a).map ((G.commShiftIso b).hom.app ((shiftFunctor D a).obj (F.obj X))))) (CategoryStruct.comp (F.map ((shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X))))) (CategoryStruct.comp (adj.counit.app ((shiftFunctor D a).obj (F.obj X))) h✝))))

theorem CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (Y : C) : (iso adj a).inv.app Y = CategoryStruct.comp ((shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y))) (CategoryStruct.comp ((shiftFunctor D a).map (F.map ((shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj Y))))) (CategoryStruct.comp ((shiftFunctor D a).map (F.map ((G.commShiftIso b).inv.app (F.obj ((shiftFunctor C a).obj Y))))) (CategoryStruct.comp ((shiftFunctor D a).map (adj.counit.app ((shiftFunctor D b).obj (F.obj ((shiftFunctor C a).obj Y))))) ((shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))))))

theorem CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (Y : C) {Z : D} (h✝ : F.obj ((shiftFunctor C a).obj Y) ⟶ Z) : CategoryStruct.comp ((iso adj a).inv.app Y) h✝ = CategoryStruct.comp ((shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y))) (CategoryStruct.comp ((shiftFunctor D a).map (F.map ((shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj Y))))) (CategoryStruct.comp ((shiftFunctor D a).map (F.map ((G.commShiftIso b).inv.app (F.obj ((shiftFunctor C a).obj Y))))) (CategoryStruct.comp ((shiftFunctor D a).map (adj.counit.app ((shiftFunctor D b).obj (F.obj ((shiftFunctor C a).obj Y))))) (CategoryStruct.comp ((shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))) h✝))))

theorem CategoryTheory.Adjunction.LeftAdjointCommShift.compatibilityUnit_iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [HasShift C A] [HasShift D A] [G.CommShift A] (a : A) : CommShift.CompatibilityUnit adj (iso adj a) (G.commShiftIso a)

The commutation isomorphisms of Adjunction.LeftAdjointCommShift.iso are compatible with the unit of the adjunction.

noncomputable def CategoryTheory.Adjunction.leftAdjointCommShift {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [G.CommShift A] : F.CommShift A

Given an adjunction F ⊣ G and a CommShift structure on G, this constructs the unique compatible CommShift structure on F.

Equations

• adj.leftAdjointCommShift A = { iso := fun (a : A) => CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a, zero := ⋯, add := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointCommShift_iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [G.CommShift A] (a : A) : Functor.CommShift.iso a = LeftAdjointCommShift.iso adj a

theorem CategoryTheory.Adjunction.commShift_of_rightAdjoint {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [G.CommShift A] : adj.CommShift A

@[reducible, inline]

abbrev CategoryTheory.Equivalence.CommShift {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] : Prop

If E : C ≌ D is an equivalence, this expresses the compatibility of CommShift structures on E.functor and E.inverse.

Equations

• E.CommShift A = E.toAdjunction.CommShift A

instance CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorUnitIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] [E.CommShift A] : NatTrans.CommShift E.unitIso.hom A

instance CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorCounitIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] [E.CommShift A] : NatTrans.CommShift E.counitIso.hom A

instance CategoryTheory.Equivalence.CommShift.instCommShiftInverseSymmOfFunctor {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [h : E.functor.CommShift A] : E.symm.inverse.CommShift A

Equations

• CategoryTheory.Equivalence.CommShift.instCommShiftInverseSymmOfFunctor E A = h

instance CategoryTheory.Equivalence.CommShift.instCommShiftFunctorSymmOfInverse {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [h : E.inverse.CommShift A] : E.symm.functor.CommShift A

Equations

• CategoryTheory.Equivalence.CommShift.instCommShiftFunctorSymmOfInverse E A = h

theorem CategoryTheory.Equivalence.CommShift.mk' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] (h : NatTrans.CommShift E.unitIso.hom A) : E.CommShift A

Constructor for Equivalence.CommShift.

instance CategoryTheory.Equivalence.CommShift.instCommShiftFunctorRefl {C : Type u_1} [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [HasShift C A] : refl.functor.CommShift A

The forward functor of the identity equivalence is compatible with shifts.

Equations

• CategoryTheory.Equivalence.CommShift.instCommShiftFunctorRefl A = id inferInstance

instance CategoryTheory.Equivalence.CommShift.instCommShiftInverseRefl {C : Type u_1} [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [HasShift C A] : refl.inverse.CommShift A

The inverse functor of the identity equivalence is compatible with shifts.

Equations

• CategoryTheory.Equivalence.CommShift.instCommShiftInverseRefl A = id inferInstance

instance CategoryTheory.Equivalence.CommShift.instRefl {C : Type u_1} [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [HasShift C A] : refl.CommShift A

The identity equivalence is compatible with shifts.

instance CategoryTheory.Equivalence.CommShift.instSymm {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] [E.CommShift A] : E.symm.CommShift A

If an equivalence E : C ≌ D is compatible with shifts, so is E.symm.

theorem CategoryTheory.Equivalence.CommShift.mk'' {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] (h : NatTrans.CommShift E.counitIso.hom A) : E.CommShift A

Constructor for Equivalence.CommShift.

instance CategoryTheory.Equivalence.CommShift.instCommShiftFunctorTrans {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] {F : Type u_4} [Category.{u_7, u_4} F] [HasShift F A] {E' : D ≌ F} [E'.functor.CommShift A] : (E.trans E').functor.CommShift A

If E : C ≌ D and E' : D ≌ F are equivalence whose forward functors are compatible with shifts, so is (E.trans E').functor.

Equations

• CategoryTheory.Equivalence.CommShift.instCommShiftFunctorTrans E A = id inferInstance

instance CategoryTheory.Equivalence.CommShift.instCommShiftInverseTrans {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.inverse.CommShift A] {F : Type u_4} [Category.{u_7, u_4} F] [HasShift F A] {E' : D ≌ F} [E'.inverse.CommShift A] : (E.trans E').inverse.CommShift A

If E : C ≌ D and E' : D ≌ F are equivalence whose inverse functors are compatible with shifts, so is (E.trans E').inverse.

Equations

• CategoryTheory.Equivalence.CommShift.instCommShiftInverseTrans E A = id inferInstance

instance CategoryTheory.Equivalence.CommShift.instTrans {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] (E : C ≌ D) (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] [E.inverse.CommShift A] {F : Type u_4} [Category.{u_6, u_4} F] [HasShift F A] {E' : D ≌ F} [E.CommShift A] [E'.functor.CommShift A] [E'.inverse.CommShift A] [E'.CommShift A] : (E.trans E').CommShift A

If equivalences E : C ≌ D and E' : D ≌ F are compatible with shifts, so is E.trans E'.

noncomputable def CategoryTheory.Equivalence.commShiftInverse {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] : E.inverse.CommShift A

If E : C ≌ D is an equivalence and we have a CommShift structure on E.functor, this constructs the unique compatible CommShift structure on E.inverse.

Equations

• E.commShiftInverse A = E.toAdjunction.rightAdjointCommShift A

theorem CategoryTheory.Equivalence.commShift_of_functor {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [E.functor.CommShift A] : E.CommShift A

noncomputable def CategoryTheory.Equivalence.commShiftFunctor {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (E : C ≌ D) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [E.inverse.CommShift A] : E.functor.CommShift A

If E : C ≌ D is an equivalence and we have a CommShift structure on E.inverse, this constructs the unique compatible CommShift structure on E.functor.

Equations

• E.commShiftFunctor A = E.symm.toAdjunction.rightAdjointCommShift A

theorem CategoryTheory.Equivalence.commShift_of_inverse {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (E : C ≌ D) (A : Type u_3) [AddGroup A] [HasShift C A] [HasShift D A] [E.inverse.CommShift A] : E.CommShift A