Commit 2023-07-12 03:49 1e93cf2e

View on Github →

feat: port CategoryTheory.Monad.Monadicity (#5088)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monad/Monadicity.lean

added def CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction

added theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app

added theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f

added theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux

added def CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv

added def CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj

added def CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer

added def CategoryTheory.Monad.MonadicityInternal.counitCofork

added def CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison

added def CategoryTheory.Monad.MonadicityInternal.unitCofork

added theorem CategoryTheory.Monad.MonadicityInternal.unitCofork_π

added def CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer

added def CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic

added def CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers

added def CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms

added def CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers

added def CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms