areEqualizedByLocalization_iff — Mathlib

English

If h: AreEqualizedByLocalization W f g, then for any L: C ⥤ D with L.IsLocalization W, L.map f = L.map g.

Русский

Если h: AreEqualizedByLocalization W f g, то для любого L: C ⥤ D, локализация сохраняет равенство: L.map f = L.map g.

LaTeX

$$$\\text{AreEqualizedByLocalization } W f g \\Rightarrow (\\forall L\\; [L.IsLocalization W], L.map f = L.map g)$$$

Lean4

theorem areEqualizedByLocalization_iff [L.IsLocalization W] : AreEqualizedByLocalization W f g ↔ L.map f = L.map g :=
  by
  dsimp [AreEqualizedByLocalization]
  constructor
  · intro h
    let e := Localization.compUniqFunctor W.Q L W
    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
    dsimp
    rw [h]
  · intro h
    let e := Localization.compUniqFunctor L W.Q W
    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
    dsimp
    rw [h]

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