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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
:
G.Additive
theorem
CategoryTheory.Adjunction.left_adjoint_additive
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[G.Additive]
:
F.Additive
def
CategoryTheory.Adjunction.homAddEquiv
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
:
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
- adj.homAddEquiv X Y = { toEquiv := adj.homEquiv X Y, map_add' := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.homAddEquiv_apply
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
(f f' : F.obj X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Adjunction.homAddEquiv_sub
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
(f f' : F.obj X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Adjunction.homAddEquiv_neg
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
(f : F.obj X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_zero
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
(f f' : X ⟶ G.obj Y)
:
@[simp]
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_sub
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
(f f' : X ⟶ G.obj Y)
:
@[simp]
theorem
CategoryTheory.Adjunction.homAddEquiv_symm_neg
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : C)
(Y : D)
(f : X ⟶ G.obj Y)
:
def
CategoryTheory.Adjunction.compPreadditiveYonedaIso
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
:
G.comp
(CategoryTheory.preadditiveYoneda.comp
((CategoryTheory.whiskeringRight Cᵒᵖ AddCommGrp AddCommGrp).obj AddCommGrp.uliftFunctor)) ≅ CategoryTheory.preadditiveYoneda.comp
(((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrp).obj F.op).comp
((CategoryTheory.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.
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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : Cᵒᵖ)
(Y : D)
(a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y))
:
((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₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Additive]
(X : Cᵒᵖ)
(Y : D)
(a : ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y))
:
((adj.compPreadditiveYonedaIso.inv.app Y).app X) a = { down := (adj.homEquiv (Opposite.unop X) Y) (AddEquiv.ulift a) }