English
There is a functor from the opposite of Φ.LeftResolution(X₂) to Φ.op.RightResolution(Opposite(X₂)), sending objects L to L.unop.op and morphisms φ to φ.unop.f.op with reversed commutativity data.
Русский
Существует функтор от противоположного Φ.LeftResolution(X₂) к Φ.op.RightResolution(Opposite(X₂)), отправляющий объекты L в L.unop.op и морфизмы φ в φ.unop.f.op с обращением условий совместности.
LaTeX
$$$(\Phi.LeftResolution(X_2))^{op} \to \Phi.op.RightResolution(X_2^{op})$,\quad
obj:\; L \mapsto L.unop.op,\quad map:\; φ \mapsto { f := φ.unop.f.op, \; comm := \text{(unop-comms)}}$$
Lean4
/-- The functor `(Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂)`. -/
@[simps]
def opFunctor (X₂ : C₂) : (Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂)
where
obj L := L.unop.op
map
φ :=
{ f := φ.unop.f.op
comm := Quiver.Hom.unop_inj φ.unop.comm }
