functor

Mathlib.CategoryTheory.Enriched.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.forgetEnrichmentOppositeEquivalence.functor

Lean4

/-- The functor going from the underlying category of the enriched category `Cᵒᵖ`
to the opposite of the underlying category of the enriched category `C`. -/
def functor : ForgetEnrichment V Cᵒᵖ ⥤ (ForgetEnrichment V C)ᵒᵖ
    where
  obj x := x
  map {x y} f := f.op
  map_comp {x y z} f
    g := by
    have : (f ≫ g) = homTo V (f ≫ g) := rfl
    rw [this, ForgetEnrichment.homTo_comp, Category.assoc, tensorHom_eComp_op_eq, leftUnitor_inv_braiding_assoc, ←
      unitors_inv_equal, ← Category.assoc]
    congr 1

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

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

Разделы

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

Аффилиация

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