opFunctor

Mathlib.CategoryTheory.Square

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Square.opFunctor

Lean4

/-- The functor `(Square C)ᵒᵖ ⥤ Square Cᵒᵖ`. -/
@[simps]
def opFunctor : (Square C)ᵒᵖ ⥤ Square Cᵒᵖ where
  obj sq := sq.unop.op
  map
    φ :=
    { τ₁ := φ.unop.τ₄.op
      τ₂ := φ.unop.τ₂.op
      τ₃ := φ.unop.τ₃.op
      τ₄ := φ.unop.τ₁.op
      comm₁₂ := Quiver.Hom.unop_inj (by simp)
      comm₁₃ := Quiver.Hom.unop_inj (by simp)
      comm₂₄ := Quiver.Hom.unop_inj (by simp)
      comm₃₄ := Quiver.Hom.unop_inj (by simp) }

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

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

Разделы

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

Аффилиация

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