English
For a LocalizerMorphism Φ between morphism properties, there is a canonical map from the left resolution of X₂ to the right resolution of Opposite(X₂) in the opposite localized context. On data, if L is a left resolution with components X₁, w, hw, then op(L) has X₁ in opposite form and w, hw reversed accordingly.
Русский
Для локализатора Φ между свойствами морфизмов существует канонич. переход от левого разрешения X₂ к правому разрешению Opposite(X₂) в противоположном контексте локализации. В данных L, если L состоит из X₁, w, hw, то op(L) имеет X₁ в противоположной форме и преобразования w, hw соответственно.
LaTeX
$$$\operatorname{op}: \Phi.LeftResolution(X_2) \to \Phi.op.RightResolution(\operatorname{Opposite}(X_2))$,\quad \operatorname{op}(L) = (\operatorname{Opposite}(L.X_1),\ L.w^{op},\ L.hw).$$
Lean4
/-- The canonical map `Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂)`. -/
@[simps]
def op {X₂ : C₂} (L : Φ.LeftResolution X₂) : Φ.op.RightResolution (Opposite.op X₂)
where
X₁ := Opposite.op L.X₁
w := L.w.op
hw := L.hw
