map_eq_of_isInvertedBy — Mathlib

English

If h: AreEqualizedByLocalization W f g and F is inverted by W, then F.map f = F.map g.

Русский

Если h: AreEqualizedByLocalization W f g и F инвертируется W, то F.map f = F.map g.

LaTeX

$$$\\text{AreEqualizedByLocalization } W f g \\Rightarrow F.map f = F.map g$ for all F with W.IsInvertedBy$$

Lean4

theorem map_eq_of_isInvertedBy (h : AreEqualizedByLocalization W f g) (F : C ⥤ D) (hF : W.IsInvertedBy F) :
    F.map f = F.map g := by simp [← NatIso.naturality_1 (Localization.fac F hF W.Q), h.map_eq W.Q]

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