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.homEquivlifts to an additive equivalenceAdjunction.homAddEquiv. - We also give a version of this additive equivalence as an isomorphism of
preadditiveYonedafunctors (analogous toAdjunction.compYonedaIso), inAdjunction.compPreadditiveYonedaIso.
theorem
CategoryTheory.Adjunction.right_adjoint_additive
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
:
G.Additive
theorem
CategoryTheory.Adjunction.left_adjoint_additive
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[G.Additive]
:
F.Additive
def
CategoryTheory.Adjunction.homAddEquiv
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
:
AddEquiv (Quiver.Hom (F.obj X) Y) (Quiver.Hom 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.
Equations
- Eq (adj.homAddEquiv X Y) { toEquiv := adj.homEquiv X Y, map_add' := ⋯ }
Instances For
theorem
CategoryTheory.Adjunction.homAddEquiv_apply
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f : Quiver.Hom (F.obj X) Y)
:
Eq (DFunLike.coe (adj.homAddEquiv X Y) f) (DFunLike.coe (adj.homEquiv X Y) f)
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_apply
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f : Quiver.Hom X (G.obj Y))
:
Eq (DFunLike.coe (adj.homAddEquiv X Y).symm f) (DFunLike.coe (adj.homEquiv X Y).symm f)
theorem
CategoryTheory.Adjunction.homAddEquiv_zero
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
:
Eq (DFunLike.coe (adj.homEquiv X Y) 0) 0
theorem
CategoryTheory.Adjunction.homAddEquiv_add
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f f' : Quiver.Hom (F.obj X) Y)
:
Eq (DFunLike.coe (adj.homEquiv X Y) (HAdd.hAdd f f'))
(HAdd.hAdd (DFunLike.coe (adj.homEquiv X Y) f) (DFunLike.coe (adj.homEquiv X Y) f'))
theorem
CategoryTheory.Adjunction.homAddEquiv_sub
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f f' : Quiver.Hom (F.obj X) Y)
:
Eq (DFunLike.coe (adj.homEquiv X Y) (HSub.hSub f f'))
(HSub.hSub (DFunLike.coe (adj.homEquiv X Y) f) (DFunLike.coe (adj.homEquiv X Y) f'))
theorem
CategoryTheory.Adjunction.homAddEquiv_neg
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f : Quiver.Hom (F.obj X) Y)
:
Eq (DFunLike.coe (adj.homEquiv X Y) (Neg.neg f)) (Neg.neg (DFunLike.coe (adj.homEquiv X Y) f))
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_zero
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
:
Eq (DFunLike.coe (adj.homEquiv X Y).symm 0) 0
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_add
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f f' : Quiver.Hom X (G.obj Y))
:
Eq (DFunLike.coe (adj.homEquiv X Y).symm (HAdd.hAdd f f'))
(HAdd.hAdd (DFunLike.coe (adj.homEquiv X Y).symm f) (DFunLike.coe (adj.homEquiv X Y).symm f'))
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_sub
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f f' : Quiver.Hom X (G.obj Y))
:
Eq (DFunLike.coe (adj.homEquiv X Y).symm (HSub.hSub f f'))
(HSub.hSub (DFunLike.coe (adj.homEquiv X Y).symm f) (DFunLike.coe (adj.homEquiv X Y).symm f'))
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_neg
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : C)
(Y : D)
(f : Quiver.Hom X (G.obj Y))
:
Eq (DFunLike.coe (adj.homEquiv X Y).symm (Neg.neg f)) (Neg.neg (DFunLike.coe (adj.homEquiv X Y).symm f))
def
CategoryTheory.Adjunction.compPreadditiveYonedaIso
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
:
Iso (G.comp (preadditiveYoneda.comp ((whiskeringRight (Opposite C) AddCommGrp AddCommGrp).obj AddCommGrp.uliftFunctor)))
(preadditiveYoneda.comp
(((whiskeringLeft (Opposite C) (Opposite D) AddCommGrp).obj F.op).comp
((whiskeringRight (Opposite 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : Opposite C)
(Y : D)
(a : ULift (Quiver.Hom (Opposite.unop X) (G.obj Y)))
:
Eq (DFunLike.coe (ConcreteCategory.hom ((adj.compPreadditiveYonedaIso.hom.app Y).app X)) a)
{ down := DFunLike.coe (adj.homEquiv (Opposite.unop X) Y).symm (DFunLike.coe AddEquiv.ulift a) }
theorem
CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply
{C : Type u₁}
{D : Type u₂}
[Category C]
[Category D]
[Preadditive C]
[Preadditive D]
{F : Functor C D}
{G : Functor D C}
(adj : Adjunction F G)
[F.Additive]
(X : Opposite C)
(Y : D)
(a : ULift (Quiver.Hom (F.obj (Opposite.unop X)) Y))
:
Eq (DFunLike.coe (ConcreteCategory.hom ((adj.compPreadditiveYonedaIso.inv.app Y).app X)) a)
{ down := DFunLike.coe (adj.homEquiv (Opposite.unop X) Y) (DFunLike.coe AddEquiv.ulift a) }