hasSmallLocalizedHom_iff_source — Mathlib

English

There is a canonical equivalence between SmallHom W X Y and the corresponding Hom after localization, natural in X and Y.

Русский

Существует каноническая эквивалентность между SmallHom W X Y и соответствующим гомоморфизмом после локализации, естественная по X и Y.

LaTeX

$$$\text{SmallHom}(W,X,Y) \simeq \mathrm{Hom}(L_X, L_Y).$$$

Lean4

theorem hasSmallLocalizedHom_iff_source {X' : C} (f : X ⟶ X') (hf : W f) (Y : C) :
    HasSmallLocalizedHom.{w} W X Y ↔ HasSmallLocalizedHom.{w} W X' Y :=
  by
  simp only [hasSmallLocalizedHom_iff W W.Q]
  exact small_congr (Iso.homCongr (Localization.isoOfHom W.Q W f hf) (Iso.refl _))

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