Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 09:33 40fdf72d

View on Github →

feat(category_theory/endofunctor/algebra): Define coalgebras over an endofunctor and prove an equivalence (#14834) This PR dualises the definition of an algebra over an endofunctor to that of a coalgebra over an endofunctor. Furthermore, it proves that if an endofunctor F is left adjoint to an endofunctor G, then the category of algebras over F is equivalent to the category of coalgebras over G.

Estimated changes