unopFunctor

Mathlib.CategoryTheory.Localization.Resolution

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

Lean4

/-- The functor `(Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop`. -/
@[simps]
def unopFunctor (X₂ : C₂ᵒᵖ) : (Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop
    where
  obj R := R.unop.unop
  map
    φ :=
    { f := φ.unop.f.unop
      comm := Quiver.Hom.op_inj φ.unop.comm }

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

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

Разделы

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

Аффилиация

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