equiv_chgUniv — Mathlib

English

For a localization functor L and an equivalence e, the equiv before and after changing universes coincides: equiv(W,L)(chgUniv^{w''}(e)) = equiv(W,L)(e).

Русский

Для локализационной функтора L и эквивалентности e равенство сохраняется при смене универсум: equiv_W,L(chgUniv^{w''}(e)) = equiv_W,L(e).

LaTeX

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

Lean4

theorem equiv_chgUniv (L : C ⥤ D) [L.IsLocalization W] {X Y : C} [HasSmallLocalizedHom.{w} W X Y]
    [HasSmallLocalizedHom.{w''} W X Y] (e : SmallHom.{w} W X Y) : equiv W L (chgUniv.{w''} e) = equiv W L e :=
  by
  obtain ⟨f, rfl⟩ := (equiv W W.Q).symm.surjective e
  dsimp [chgUniv]
  simp only [Equiv.apply_symm_apply, equiv_equiv_symm W _ _ _ (Localization.compUniqFunctor W.Q L W)]

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