rightOp — Mathlib

English

The left operation of a left adjoint is obtained by transporting along the standard op-equivalence.

Русский

Левая операция левого сопряжения получается за счёт переноса по стандартному противоположному эквиваленту.

LaTeX

$$$a.leftOp = (\\mathrm{opOpEquivalence} D).symm.toAdjunction .\\circ a.op$$$

Lean4

instance rightOp {F : Cᵒᵖ ⥤ D} [F.IsRightAdjoint] : F.rightOp.IsLeftAdjoint :=
  ⟨F.leftAdjoint.leftOp, ⟨.rightOp <| .ofIsRightAdjoint _⟩⟩

Похожие утверждения