unop — Mathlib

English

For W a MorphismProperty on C and z1,z2 in W.RightFraction X Y with X,Y in Cᵒᵖ, if z1 relates to z2 by RightFractionRel, then z1.unop relates to z2.unop by LeftFractionRel.

Русский

Для W — свойство морфизмов на Cᵒᵖ и для z1,z2 из W.RightFraction X Y, если z1 связано z2 RightFractionRel, то z1.unop связано z2.unop LeftFractionRel.

LaTeX

$$$\forall X,Y \; \forall z_1,z_2 \in W.RightFraction(X,Y):\; (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.RightFraction X Y} (h : RightFractionRel z₁ z₂) :
    LeftFractionRel 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⟩

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