ofEq

Mathlib.CategoryTheory.Localization.LocalizerMorphism

URI: https://scilib.ai/kg/mathlib#CategoryTheory.LocalizerMorphism.ofEq

Lean4

/-- Constructor for localizer morphisms given by a functor `F : C₁ ⥤ C₂`
under the stronger assumption that the classes of morphisms `W₁` and `W₂`
satisfy `W₁ = W₂.inverseImage F`. -/
@[simps]
def ofEq {F : C₁ ⥤ C₂} (hW : W₁ = W₂.inverseImage F) : LocalizerMorphism W₁ W₂
    where
  functor := F
  map := by rw [hW]

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

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

Разделы

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

Аффилиация

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