shift

Mathlib.CategoryTheory.Shift.Localization

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.shift

English

Shifting preserves invertedness: W f implies W of the shifted morphism f⟦a⟧′ for any a.

Русский

Сдвиг сохраняет инвертируемость: если W f, то W (f⟦a⟧′) для любого a.

LaTeX

$$$ \forall f, hf:\, W f \Rightarrow W (f\langle a\rangle') $$$

Lean4

theorem shift {X Y : C} {f : X ⟶ Y} (hf : W f) (a : A) : W (f⟦a⟧') := by
  simpa only [IsCompatibleWithShift.iff W f a] using hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru