shiftLocalizerMorphism

Mathlib.CategoryTheory.Shift.Localization

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

Lean4

/-- The morphism of localizer from `W` to `W` given by the functor `shiftFunctor C a`
when `a : A` and `W` is compatible with the shift by `A`. -/
abbrev shiftLocalizerMorphism (a : A) : LocalizerMorphism W W
    where
  functor := shiftFunctor C a
  map := by rw [MorphismProperty.IsCompatibleWithShift.condition]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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