Commit 2023-04-19 15:24 823fd99b

View on Github →

Feat: Port CategoryTheory.Monad.Algebra (#3525)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monad/Algebra.lean

added def CategoryTheory.Comonad.Coalgebra.Hom.comp

added theorem CategoryTheory.Comonad.Coalgebra.Hom.ext'

added def CategoryTheory.Comonad.Coalgebra.Hom.id

added structure CategoryTheory.Comonad.Coalgebra.Hom

added theorem CategoryTheory.Comonad.Coalgebra.comp_eq_comp

added theorem CategoryTheory.Comonad.Coalgebra.comp_f

added theorem CategoryTheory.Comonad.Coalgebra.id_eq_id

added theorem CategoryTheory.Comonad.Coalgebra.id_f

added def CategoryTheory.Comonad.Coalgebra.isoMk

added structure CategoryTheory.Comonad.Coalgebra

added def CategoryTheory.Comonad.adj

added theorem CategoryTheory.Comonad.algebra_epi_of_epi

added theorem CategoryTheory.Comonad.algebra_mono_of_mono

added theorem CategoryTheory.Comonad.coalgebra_iso_of_iso

added def CategoryTheory.Comonad.cofree

added def CategoryTheory.Comonad.forget

added theorem CategoryTheory.Comonad.ofLeftAdjoint_forget

added theorem CategoryTheory.Comonad.rightAdjoint_forget

added def CategoryTheory.Monad.Algebra.Hom.comp

added theorem CategoryTheory.Monad.Algebra.Hom.ext'

added def CategoryTheory.Monad.Algebra.Hom.id

added structure CategoryTheory.Monad.Algebra.Hom

added theorem CategoryTheory.Monad.Algebra.comp_eq_comp

added theorem CategoryTheory.Monad.Algebra.comp_f

added theorem CategoryTheory.Monad.Algebra.id_eq_id

added theorem CategoryTheory.Monad.Algebra.id_f

added def CategoryTheory.Monad.Algebra.isoMk

added structure CategoryTheory.Monad.Algebra

added def CategoryTheory.Monad.adj

added def CategoryTheory.Monad.algebraEquivOfIsoMonads

added def CategoryTheory.Monad.algebraFunctorOfMonadHom

added def CategoryTheory.Monad.algebraFunctorOfMonadHomComp

added def CategoryTheory.Monad.algebraFunctorOfMonadHomEq

added def CategoryTheory.Monad.algebraFunctorOfMonadHomId

added theorem CategoryTheory.Monad.algebra_epi_of_epi

added theorem CategoryTheory.Monad.algebra_equiv_of_iso_monads_comp_forget

added theorem CategoryTheory.Monad.algebra_iso_of_iso

added theorem CategoryTheory.Monad.algebra_mono_of_mono

added def CategoryTheory.Monad.forget

added def CategoryTheory.Monad.free

added theorem CategoryTheory.Monad.leftAdjoint_forget

added theorem CategoryTheory.Monad.ofRightAdjoint_forget