hasSmallLocalizedShiftedHom_iff_source

English

If a morphism f: X → X' is W-equivalent and X' is related by a shift, then HasSmallLocalizedShiftedHom W M X Y is equivalent to HasSmallLocalizedShiftedHom W M X' Y.

Русский

Если f: X → X' эквивалентен по W и X' связан с X сдвигом, то HasSmallLocalizedShiftedHom W M X Y эквивалентно HasSmallLocalizedShiftedHom W M X' Y.

LaTeX

$$$ HasSmallLocalizedShiftedHom^{w} W M X Y \iff HasSmallLocalizedShiftedHom^{w} W M X' Y $$$

Lean4

theorem hasSmallLocalizedShiftedHom_iff_source [W.IsCompatibleWithShift M] {X' : C} (f : X ⟶ X') (hf : W f) (Y : C) :
    HasSmallLocalizedShiftedHom.{w} W M X Y ↔ HasSmallLocalizedShiftedHom.{w} W M X' Y :=
  forall_congr' (fun a ↦ forall_congr' (fun b ↦ hasSmallLocalizedHom_iff_source W (f⟦a⟧') (W.shift hf a) (Y⟦b⟧)))

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