equiv_chgUniv — Mathlib

English

Let L be a localization functor and e a SmallShiftedHom in universe w; changing the universe via chgUniv to w'' yields the same value of the equiv map after applying L and W, i.e., equiv_W^L(chgUniv^{w''}(e)) = equiv_W^L(e).

Русский

Пусть L — локализационный функтор, e — SmallShiftedHom в вселенной w; переход к вселенной через chgUniv в w'' не меняет значение отображения эквив, т.е. equiv_W^L(chgUniv^{w''}(e)) = equiv_W^L(e).

LaTeX

$$$\mathrm{equiv}_{W,L}(\mathrm{chgUniv}^{w''}(e)) = \mathrm{equiv}_{W,L}(e)$$$

Lean4

theorem equiv_chgUniv (L : C ⥤ D) [L.IsLocalization W] [L.CommShift M] {X Y : C} {m : M}
    [HasSmallLocalizedShiftedHom.{w} W M X Y] [HasSmallLocalizedShiftedHom.{w''} W M X Y]
    (e : SmallShiftedHom.{w} W X Y m) : equiv W L (chgUniv.{w''} e) = equiv W L e :=
  by
  dsimp [equiv]
  congr
  apply SmallHom.equiv_chgUniv

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