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

Modified src/category_theory/endofunctor/algebra.lean

added def category_theory.endofunctor.adjunction.alg_coalg_equiv.counit_iso

added def category_theory.endofunctor.adjunction.alg_coalg_equiv.unit_iso

added theorem category_theory.endofunctor.adjunction.algebra.hom_equiv_naturality_str

added def category_theory.endofunctor.adjunction.algebra.to_coalgebra_of

added def category_theory.endofunctor.adjunction.algebra_coalgebra_equiv

added theorem category_theory.endofunctor.adjunction.coalgebra.hom_equiv_naturality_str_symm

added def category_theory.endofunctor.adjunction.coalgebra.to_algebra_of

added theorem category_theory.endofunctor.coalgebra.comp_eq_comp

added theorem category_theory.endofunctor.coalgebra.comp_f

added def category_theory.endofunctor.coalgebra.equiv_of_nat_iso

added def category_theory.endofunctor.coalgebra.forget

added def category_theory.endofunctor.coalgebra.functor_of_nat_trans

added def category_theory.endofunctor.coalgebra.functor_of_nat_trans_comp

added def category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq

added def category_theory.endofunctor.coalgebra.functor_of_nat_trans_id

added def category_theory.endofunctor.coalgebra.hom.comp

added def category_theory.endofunctor.coalgebra.hom.id

added structure category_theory.endofunctor.coalgebra.hom

added theorem category_theory.endofunctor.coalgebra.id_eq_id

added theorem category_theory.endofunctor.coalgebra.id_f

added def category_theory.endofunctor.coalgebra.iso_mk

added theorem category_theory.endofunctor.coalgebra.iso_of_iso

added structure category_theory.endofunctor.coalgebra