Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-15 10:30 8041945f

View on Github →

feat(category_theory/monad): monadicity theorems (#5137) This is a proof of the reflexive (or crude) monadicity theorem along with a complete proof of Beck's monadicity theorem. Also renames the prefix for special monad coequalizers to free_coequalizer rather than coequalizer, to avoid name-clashes when both monad and limits are imported.

Estimated changes

Modified src/category_theory/monad/adjunction.lean

Modified src/category_theory/monad/coequalizer.lean

modified def category_theory.monad.beck_algebra_cofork

deleted def category_theory.monad.coequalizer.bottom_map

deleted theorem category_theory.monad.coequalizer.condition

deleted def category_theory.monad.coequalizer.top_map

deleted def category_theory.monad.coequalizer.π

added def category_theory.monad.free_coequalizer.bottom_map

added theorem category_theory.monad.free_coequalizer.condition

added def category_theory.monad.free_coequalizer.top_map

added def category_theory.monad.free_coequalizer.π

Created src/category_theory/monad/monadicity.lean

added def category_theory.monad.creates_G_split_coequalizers_of_monadic

added def category_theory.monad.monadic_of_creates_G_split_coequalizers

added def category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms

added def category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers

added def category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms

added def category_theory.monad.monadicity_internal.comparison_adjunction

added theorem category_theory.monad.monadicity_internal.comparison_adjunction_counit_app

added theorem category_theory.monad.monadicity_internal.comparison_adjunction_unit_f

added theorem category_theory.monad.monadicity_internal.comparison_adjunction_unit_f_aux

added def category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv

added def category_theory.monad.monadicity_internal.comparison_left_adjoint_obj

added def category_theory.monad.monadicity_internal.counit_coequalizer_of_reflects_coequalizer

added def category_theory.monad.monadicity_internal.counit_cofork

added def category_theory.monad.monadicity_internal.left_adjoint_comparison

added def category_theory.monad.monadicity_internal.unit_cofork

added def category_theory.monad.monadicity_internal.unit_colimit_of_preserves_coequalizer