hasSmallLocalizedShiftedHom_iff — Mathlib

English

Under the localization L with a shift of M, HasSmallLocalizedShiftedHom W M X Y is equivalent to a family of small morphisms parameterized by M: all Hom spaces are small.

Русский

При локализации L с сдвигом M свойство HasSmallLocalizedShiftedHom эквивалентно семье малых морфизмов параметризованных по M: все пространства гомоморфизмов малые.

LaTeX

$$$ HasSmallLocalizedShiftedHom^{w} W M X Y \iff \forall a,b \in M, Small^w( (L.obj X)⟦a⟧ \to (L.obj Y)⟦b⟧) $$$

Lean4

theorem hasSmallLocalizedShiftedHom_iff (L : C ⥤ D) [L.IsLocalization W] [L.CommShift M] (X Y : C) :
    HasSmallLocalizedShiftedHom.{w} W M X Y ↔ ∀ (a b : M), Small.{w} ((L.obj X)⟦a⟧ ⟶ (L.obj Y)⟦b⟧) :=
  by
  dsimp [HasSmallLocalizedShiftedHom]
  have eq := fun (a b : M) ↦ small_congr.{w} (Iso.homCongr ((L.commShiftIso a).app X) ((L.commShiftIso b).app Y))
  dsimp at eq
  simp only [hasSmallLocalizedHom_iff _ L, eq]

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