Q

Mathlib.CategoryTheory.Localization.Construction

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

Lean4

/-- The obvious functor `C ⥤ W.Localization` -/
def Q : C ⥤ W.Localization where
  obj X := (Quotient.functor _).obj ((Paths.of _).obj ⟨X⟩)
  map f := (Quotient.functor _).map (ψ₁ W f)
  map_id X := Quotient.sound _ (relations.id X)
  map_comp f g := Quotient.sound _ (relations.comp f g)

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

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

Разделы

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

Аффилиация

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