map_eq_iff — Mathlib

English

For W on Cᵒᵖ and X,Y in Cᵒᵖ, φ ∈ W.RightFraction X Y lifts to a right fraction after unop.

Русский

Для W на Cᵒᵖ и X,Y в Cᵒᵖ, φ ∈ W.RightFraction X Y соответствует правой дроби после unop.

LaTeX

$$$\forall {X Y : C^{op}}, \forall {z_1 z_2 : W.RightFraction X Y}, RightFractionRel(z_1,z_2) \Rightarrow LeftFractionRel(z_1^{unop}, z_2^{unop})$$

Lean4

theorem map_eq_iff {X Y : C} (φ ψ : W.RightFraction X Y) :
    φ.map L (Localization.inverts _ _) = ψ.map L (Localization.inverts _ _) ↔ RightFractionRel φ ψ :=
  by
  rw [← leftFractionRel_op_iff, ← LeftFraction.map_eq_iff L.op W.op φ.op ψ.op, ← φ.op_map L (Localization.inverts _ _),
    ← ψ.op_map L (Localization.inverts _ _)]
  constructor
  · apply Quiver.Hom.unop_inj
  · apply Quiver.Hom.op_inj

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