Theorems · Theorem · category theory

CategoryTheory.Adjunction.CommShift.compatibilityCounit_of_compatibilityUnit

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂ →
    CategoryTheory.Adjunction.CommShift.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.

Defined in

Mathlib.CategoryTheory.Shift.Adjunction

Cited by

2 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShift