monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms

Lean4

/-- An alternate version of **Beck's monadicity theorem**: if `G` reflects isomorphisms, preserves
coequalizers of `G`-split pairs and `C` has coequalizers of `G`-split pairs, then it is monadic.
-/
def monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms [G.ReflectsIsomorphisms]
    [HasCoequalizerOfIsSplitPair G] [PreservesColimitOfIsSplitPair G] : MonadicRightAdjoint G :=
  by
  have : ReflectsColimitOfIsSplitPair G :=
    ⟨fun f g _ => by
      have := HasCoequalizerOfIsSplitPair.out G f g
      apply reflectsColimit_of_reflectsIsomorphisms⟩
  apply monadicOfHasPreservesReflectsGSplitCoequalizers adj

Похожие утверждения