Adjunctions between additive functors.

This provides some results and constructions for adjunctions between functors on preadditive categories:

• If one of the adjoint functors is additive, so is the other.
• If one of the adjoint functors is additive, the equivalence Adjunction.homEquiv lifts to an additive equivalence Adjunction.homAddEquiv.
• We also give a version of this additive equivalence as an isomorphism of preadditiveYoneda functors (analogous to Adjunction.compYonedaIso), in Adjunction.compPreadditiveYonedaIso.

theorem CategoryTheory.Adjunction.right_adjoint_additive {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] : G.Additive

theorem CategoryTheory.Adjunction.left_adjoint_additive {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.Additive] : F.Additive

def CategoryTheory.Adjunction.homAddEquiv {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) : (F.obj X ⟶ Y) ≃+ (X ⟶ G.obj Y)

If we have an adjunction adj : F ⊣ G of functors between preadditive categories, and if F is additive, then the hom set equivalence upgrades to an AddEquiv. Note that F is additive if and only if G is, by Adjunction.right_adjoint_additive and Adjunction.left_adjoint_additive.

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_apply {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f : F.obj X ⟶ Y) : (adj.homAddEquiv X Y) f = (adj.homEquiv X Y) f

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_symm_apply {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f : X ⟶ G.obj Y) : (adj.homAddEquiv X Y).symm f = (adj.homEquiv X Y).symm f

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_zero {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) : (adj.homEquiv X Y) 0 = 0

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_add {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : F.obj X ⟶ Y) : (adj.homEquiv X Y) (f + f') = (adj.homEquiv X Y) f + (adj.homEquiv X Y) f'

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_sub {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : F.obj X ⟶ Y) : (adj.homEquiv X Y) (f - f') = (adj.homEquiv X Y) f - (adj.homEquiv X Y) f'

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_neg {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f : F.obj X ⟶ Y) : (adj.homEquiv X Y) (-f) = -(adj.homEquiv X Y) f

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_symm_zero {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) : (adj.homEquiv X Y).symm 0 = 0

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_symm_add {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : X ⟶ G.obj Y) : (adj.homEquiv X Y).symm (f + f') = (adj.homEquiv X Y).symm f + (adj.homEquiv X Y).symm f'

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_symm_sub {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : X ⟶ G.obj Y) : (adj.homEquiv X Y).symm (f - f') = (adj.homEquiv X Y).symm f - (adj.homEquiv X Y).symm f'

@[simp]

theorem CategoryTheory.Adjunction.homAddEquiv_symm_neg {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f : X ⟶ G.obj Y) : (adj.homEquiv X Y).symm (-f) = -(adj.homEquiv X Y).symm f

def CategoryTheory.Adjunction.compPreadditiveYonedaIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] : G.comp (preadditiveYoneda.comp ((Functor.whiskeringRight Cᵒᵖ AddCommGrp AddCommGrp).obj AddCommGrp.uliftFunctor)) ≅ preadditiveYoneda.comp (((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrp).obj F.op).comp ((Functor.whiskeringRight Cᵒᵖ AddCommGrp AddCommGrp).obj AddCommGrp.uliftFunctor))

If we have an adjunction adj : F ⊣ G of functors between preadditive categories, and if F is additive, then the hom set equivalence upgrades to an isomorphism between G ⋙ preadditiveYoneda and preadditiveYoneda ⋙ F, once we throw in the necessary universe lifting functors. Note that F is additive if and only if G is, by Adjunction.right_adjoint_additive and Adjunction.left_adjoint_additive.

theorem CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : Cᵒᵖ) (Y : D) (a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y)) : (ConcreteCategory.hom ((adj.compPreadditiveYonedaIso.hom.app Y).app X)) a = { down := (adj.homEquiv (Opposite.unop X) Y).symm (AddEquiv.ulift a) }

theorem CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Additive] (X : Cᵒᵖ) (Y : D) (a : ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y)) : (ConcreteCategory.hom ((adj.compPreadditiveYonedaIso.inv.app Y).app X)) a = { down := (adj.homEquiv (Opposite.unop X) Y) (AddEquiv.ulift a) }