English
For objects X,Y in C and arrows f1,f2: X → Y, L.map f1 = L.map f2 if and only if there exists Z and s such that f1 ≫ s = f2 ≫ s with s ∈ W.
Русский
Для стрелок f1,f2: X → Y в C выполняется: L.map f1 = L.map f2 тогда и только тогда, существует Z и s: Y → Z с f1 ≫ s = f2 ≫ s и s ∈ W.
LaTeX
$$$\forall {C} {D} [\text{Category } C] [\text{Category } D] {W} {X Y} (f_1 f_2 : X \to Y),
L.map f_1 = L.map f_2 \Leftrightarrow ∃ Z \; (s : Y \to Z) (hs : W s), f_1 \circ s = f_2 \circ s$$$
Lean4
theorem map_eq_iff_postcomp {X Y : C} (f₁ f₂ : X ⟶ Y) :
L.map f₁ = L.map f₂ ↔ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s :=
by
constructor
· intro h
rw [← LeftFraction.map_ofHom W _ L (Localization.inverts _ _), ←
LeftFraction.map_ofHom W _ L (Localization.inverts _ _), LeftFraction.map_eq_iff] at h
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
dsimp at t₁ t₂ hst hft ht
grind
· rintro ⟨Z, s, hs, fac⟩
simp only [← cancel_mono (Localization.isoOfHom L W s hs).hom, Localization.isoOfHom_hom, ← L.map_comp, fac]
