Documentation

Mathlib.CategoryTheory.Shift.Adjunction

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:

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)) :

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.
Instances For
    @[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)) :

    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.
    Instances For
      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₁.

      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ā‚‚) :

      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] :

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

      Instances
        @[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) :
        @[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) :
        @[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) :
        @[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) :
        @[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) :
        @[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) :
        @[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) :
        @[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) :
        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.

        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) :
        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) :
        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) :
        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) :
        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] :

        Auxiliary definition for iso.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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] :

          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
          Instances For
            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) :
            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) :
            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āœ))))

            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] :

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

            Equations
            Instances For
              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] :

              Auxiliary definition for iso.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                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] :

                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
                Instances For
                  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) :
                  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) :

                  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] :

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

                  Equations
                  Instances For
                    @[simp]
                    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]

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

                    Equations
                    Instances For

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

                      Equations

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

                      Equations

                      The identity equivalence is compatible with shifts.

                      If an equivalence E : C ā‰Œ D is compatible with shifts, so is E.symm.

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

                      Equations

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

                      Equations

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

                      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
                      Instances For

                        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
                        Instances For