rightOp_eq — Mathlib

English

The right operation of a right adjoint in the opposite category is given by the inverse op-op equivalence composed with the opposite functor.

Русский

Правая операция правого сопряжения в противоположной категории задаётся через обратную операцию эквивалентности и противоположный функтор.

LaTeX

$$$F.rightOp = (\\mathrm{opOpEquivalence} D).symm.toAdjunction \\circ F.op$$$

Lean4

theorem rightOp_eq {F : Cᵒᵖ ⥤ D} {G : Dᵒᵖ ⥤ C} (a : F.rightOp ⊣ G) :
    a.rightOp = (opOpEquivalence D).symm.toAdjunction.comp a.op := by ext X; simp [Equivalence.unit]

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