map_eq — 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: C\\to D)\;[W\\text{ inverted}]\\Rightarrow F.map f = F.map g$$$

Lean4

theorem map_eq (h : AreEqualizedByLocalization W f g) (L : C ⥤ D) [L.IsLocalization W] : L.map f = L.map g :=
  (areEqualizedByLocalization_iff L W f g).1 h

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