opEquivalence — Mathlib

English

There is an equivalence of categories between (Φ.LeftResolution X₂)^{op} and Φ.op.RightResolution(Opposite(X₂)).

Русский

Существует эквивалентность категорий между (Φ.LeftResolution X₂)^{op} и Φ.op.RightResolution(Opposite(X₂)).

LaTeX

$$$(\Phi.LeftResolution X_2)^{op} \simeq \Phi.op.RightResolution(X_2^{op}).$$$

Lean4

/-- The equivalence of categories
`(Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂)`. -/
@[simps]
def opEquivalence (X₂ : C₂) : (Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂)
    where
  functor := LeftResolution.opFunctor Φ X₂
  inverse := (RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp
  unitIso := Iso.refl _
  counitIso := Iso.refl _

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