map_eq_iff — Mathlib

English

If φ1,map under L1 equals φ2,map under L1, then φ1.map under L2 equals φ2.map under L2.

Русский

Если φ1.map под L1 равен φ2.map под L1, то φ1.map под L2 равен φ2.map под L2.

LaTeX

$$$\forall {W} {X Y} (φ_1 φ_2 : W.LeftFraction X Y) {E} [Category E] (L_1 : C \to D) (L_2 : C \to E) [L_1.IsLocalization W] [L_2.IsLocalization W] (h : φ_1.map L_1 (Localization.inverts L_1 W) = φ_2.map L_1 (Localization.inverts L_1 W)) : φ_1.map L_2 (Localization.inverts L_2 W) = φ_2.map L_2 (Localization.inverts L_2 W)$$$

Lean4

theorem map_eq_iff {X Y : C} (φ ψ : W.LeftFraction X Y) :
    φ.map L (Localization.inverts _ _) = ψ.map L (Localization.inverts _ _) ↔ LeftFractionRel φ ψ :=
  by
  constructor
  · intro h
    rw [← MorphismProperty.LeftFraction.Localization.map_eq_iff]
    apply map_eq_of_map_eq _ _ _ _ h
  · intro h
    simp only [← Localization.Hom.map_mk _ L (Localization.inverts _ _)]
    congr 1
    exact Quot.sound h

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