map_eq_iff — Mathlib

English

For X,Y and LeftFraction z1,z2, equality of their images under a localization functor L is equivalent to LeftFractionRel z1 z2.

Русский

Для x,y и левых дробей z1,z2 равенство их изображений под локализационным функтором L эквивалентно LeftFractionRel z1 z2.

LaTeX

$$$\forall {C} {D} [\text{Category } C] [\text{Category } D] {W} {X Y} (z_1 z_2 : W.LeftFraction X Y) (L : C \to D) [L.IsLocalization W], \; homMk z_1 = homMk z_2 \;\Leftrightarrow\; LeftFractionRel z_1 z_2$$$

Lean4

theorem map_eq_iff {X Y : C} (f g : LeftFraction W X Y) :
    f.map (LeftFraction.Localization.Q W) (Localization.inverts _ _) =
        g.map (LeftFraction.Localization.Q W) (Localization.inverts _ _) ↔
      LeftFractionRel f g :=
  by
  simp only [← Hom.map_mk _ (Q W)]
  constructor
  · intro h
    rw [← homMk_eq_iff_leftFractionRel, homMk_eq, homMk_eq]
    exact h
  · intro h
    congr 1
    exact Quot.sound h

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