unop — Mathlib

English

Opposite of the LeftFractionRel maps back to RightFractionRel: if z1,z2 are related by RightFractionRel, then z1.unop,z2.unop are related by LeftFractionRel.

Русский

Обратное преобразование через unop возвращает к левому отношению: если z1,z2 связаны RightFractionRel, то z1.unop,z2.unop связаны LeftFractionRel.

LaTeX

$$$RightFractionRel(z_1,z_2) \Rightarrow LeftFractionRel(z_1^{unop}, z_2^{unop})$$$

Lean4

theorem unop {W : MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} {z₁ z₂ : W.LeftFraction X Y} (h : LeftFractionRel z₁ z₂) :
    RightFractionRel z₁.unop z₂.unop := by
  obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
  exact ⟨Opposite.unop Z, t₁.unop, t₂.unop, Quiver.Hom.op_inj hs, Quiver.Hom.op_inj hf, ht⟩

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