op — Mathlib · SciLib

English

There is a canonical map from the right resolution of X₂ to the left resolution of Opposite(X₂) in the opposite localized context. It sends data X₁ to Opposite(X₁), and w, hw are opposites accordingly.

Русский

Существуют каноничный гомоморфизм правого разрешения X₂ к левому разрешению Opposite(X₂) в противоположной локализации; данные X₁, w, hw переводятся аналогично через Opposite.

LaTeX

$$$\operatorname{op}: \Phi.RightResolution(X_2) \to \Phi.op.LeftResolution(\operatorname{Opposite}(X_2))$,\quad \operatorname{op}(R) = (\operatorname{Opposite}(R.X_1),\ R.w^{op},\ R.hw).$$

Lean4

/-- The canonical map `Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂)`. -/
@[simps]
def op {X₂ : C₂} (L : Φ.RightResolution X₂) : Φ.op.LeftResolution (Opposite.op X₂)
    where
  X₁ := Opposite.op L.X₁
  w := L.w.op
  hw := L.hw

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