unopFunctor

Mathlib.CategoryTheory.Square

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

Lean4

/-- The functor `(Square Cᵒᵖ)ᵒᵖ ⥤ Square Cᵒᵖ`. -/
def unopFunctor : (Square Cᵒᵖ)ᵒᵖ ⥤ Square C where
  obj sq := sq.unop.unop
  map
    φ :=
    { τ₁ := φ.unop.τ₄.unop
      τ₂ := φ.unop.τ₂.unop
      τ₃ := φ.unop.τ₃.unop
      τ₄ := φ.unop.τ₁.unop
      comm₁₂ := Quiver.Hom.op_inj (by simp)
      comm₁₃ := Quiver.Hom.op_inj (by simp)
      comm₂₄ := Quiver.Hom.op_inj (by simp)
      comm₃₄ := Quiver.Hom.op_inj (by simp) }

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

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

Разделы

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

Аффилиация

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