toCoalgebraOf

Mathlib.CategoryTheory.Endofunctor.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf

Lean4

/-- Given an adjunction `F ⊣ G`, the functor that associates to an algebra over `F` a
coalgebra over `G` defined via adjunction applied to the structure map. -/
@[simps!]
def toCoalgebraOf (adj : F ⊣ G) : Algebra F ⥤ Coalgebra G
    where
  obj
    A :=
    { V := A.1
      str := (adj.homEquiv A.1 A.1).toFun A.2 }
  map
    f :=
    { f := f.1
      h := Algebra.homEquiv_naturality_str adj _ _ f }

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

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

Разделы

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

Аффилиация

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