English
If two LeftFractions φ1, φ2 map to the same arrow under L1, then they map to the same arrow under L2, provided both L1,L2 are localizations of W.
Русский
Если два LeftFraction φ1, φ2 имеют одинаковое изображение под L1, то и под L2 они совпадают, если L1,L2 являются локализациями W.
LaTeX
$$$\forall {C D} {W} {X Y} (φ_1 φ_2 : W.LeftFraction X Y) (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_of_map_eq {W} {X Y : C} (φ₁ φ₂ : W.LeftFraction X Y) {E : Type*} [Category E] (L₁ : C ⥤ D) (L₂ : C ⥤ E)
[L₁.IsLocalization W] [L₂.IsLocalization W]
(h : φ₁.map L₁ (Localization.inverts L₁ W) = φ₂.map L₁ (Localization.inverts L₁ W)) :
φ₁.map L₂ (Localization.inverts L₂ W) = φ₂.map L₂ (Localization.inverts L₂ W) :=
by
apply (Localization.uniq L₂ L₁ W).functor.map_injective
rw [map_compatibility φ₁ L₂ L₁, map_compatibility φ₂ L₂ L₁, h]
