equiv — Mathlib

English

There is a canonical identification sending mk W f to L.map f under the localization equivalence.

Русский

Существует каноническое соответствие, отправляющее mk W f в L.map f через эквивалентность локализации.

LaTeX

$$$\text{equiv}(W,L)(\text{mk }W f) = L.map f$$$

Lean4

/-- The canonical bijection `SmallHom.{w} W X Y ≃ (L.obj X ⟶ L.obj Y)`
when `L` is a localization functor for `W : MorphismProperty C` and
that `HasSmallLocalizedHom.{w} W X Y` holds. -/
noncomputable def equiv (L : C ⥤ D) [L.IsLocalization W] {X Y : C} [HasSmallLocalizedHom.{w} W X Y] :
    SmallHom.{w} W X Y ≃ (L.obj X ⟶ L.obj Y) :=
  letI := small_of_hasSmallLocalizedHom.{w} W W.Q X Y
  (equivShrink _).symm.trans (homEquiv W W.Q L)

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