adjunction — Mathlib

Lean4
/-- The adjunction `adj`, seen as an adjunction between `OppositeShift.functor G`
and `OppositeShift.functor F`.
-/
@[simps -isSimp]
def adjunction {F} {G : D ⥤ C} (adj : F ⊣ G) : OppositeShift.functor A G ⊣ OppositeShift.functor A F
    where
  unit :=
    (NatTrans.OppositeShift.natIsoId D A).hom ≫
      OppositeShift.natTrans A adj.counit ≫ (NatTrans.OppositeShift.natIsoComp A G F).hom
  counit :=
    (NatTrans.OppositeShift.natIsoComp A F G).inv ≫
      OppositeShift.natTrans A adj.unit ≫ (NatTrans.OppositeShift.natIsoId C A).inv
  left_triangle_components
    _ :=
    by
    dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp, NatTrans.OppositeShift.natIsoId,
      OppositeShift.functor]
    simp only [comp_id, id_comp, Quiver.Hom.unop_op]
    rw [← op_comp, adj.right_triangle_components]
    rfl
  right_triangle_components
    _ :=
    by
    dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp, NatTrans.OppositeShift.natIsoId,
      OppositeShift.functor]
    simp only [comp_id, id_comp, Quiver.Hom.unop_op]
    rw [← op_comp, adj.left_triangle_components]
    rfl
Похожие утверждения