mk' — Mathlib

English

Two compatible strict universal properties yield an isLocalization structure by mk'.

Русский

Две совместимые строгие универсальные свойства образуют структуру локализации через mk'.

LaTeX

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

Lean4

theorem mk' (h₁ : Localization.StrictUniversalPropertyFixedTarget L W D)
    (h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization) : IsLocalization L W :=
  { inverts := h₁.inverts
    isEquivalence :=
      IsEquivalence.mk' (h₂.lift W.Q W.Q_inverts)
        (eqToIso
          (Localization.Construction.uniq _ _
            (by simp only [← Functor.assoc, Localization.Construction.fac, h₂.fac, Functor.comp_id])))
        (eqToIso
          (h₁.uniq _ _ (by simp only [← Functor.assoc, h₂.fac, Localization.Construction.fac, Functor.comp_id]))) }

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