toAlgebraOf

Mathlib.CategoryTheory.Endofunctor.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf

Lean4

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

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

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

Разделы

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

Аффилиация

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