equiv_mkInv — Mathlib

English

In a localization setting, for a morphism f: Y → X with hf in W, the equivalence image of mkInv f hf equals the inverse of the localization iso corresponding to f.

Русский

В локализации для морфизма f: Y → X с hf ∈ W, образ эквивалентности от mkInv f hf совпадает с обратной стороной изоморфизма локализации, соответствующего f.

LaTeX

$$$\operatorname{equiv}_W L (\mathrm{mkInv} \\ f \\ hf) = (\mathrm{Localization.isoOfHom} L W f hf)^{-1}$$$

Lean4

@[simp]
theorem equiv_mkInv (L : C ⥤ D) [L.IsLocalization W] {X Y : C} (f : Y ⟶ X) (hf : W f) [HasSmallLocalizedHom.{w} W X Y] :
    equiv.{w} W L (mkInv f hf) = (Localization.isoOfHom L W f hf).inv := by
  simp only [equiv, mkInv, Equiv.symm_trans_apply, Equiv.symm_symm, homEquiv_symm_apply, Equiv.trans_apply,
    Equiv.symm_apply_apply, homEquiv_isoOfHom_inv]

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