q_isLocalization — Mathlib

English

Given two strict universal properties for a localization, one can assemble them into a full localization structure.

Русский

Даны две строгие универсальные свойства локализации; их можно объединить в полную структуру локализации.

LaTeX

$$$IsLocalization.mk'\\ L\\ W\\ h1\\ h2$$$

Lean4

instance q_isLocalization : W.Q.IsLocalization W
    where
  inverts := W.Q_inverts
  isEquivalence :=
    by
    suffices Localization.Construction.lift W.Q W.Q_inverts = 𝟭 _
      by
      rw [this]
      infer_instance
    apply Localization.Construction.uniq
    simp only [Localization.Construction.fac]
    rfl

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