Lean4
/-- Reflexive (crude) monadicity theorem. If `G` has a right adjoint, `D` has and `G` preserves
reflexive coequalizers and `G` reflects isomorphisms, then `G` is monadic.
-/
def monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms : MonadicRightAdjoint G
where
L := F
adj := adj
eqv :=
by
have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) :=
by
intro X
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
· change IsIso ((comparisonAdjunction adj).unit.app X).f
rw [comparisonAdjunction_unit_f]
exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).isIso_hom
have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) :=
by
intro Y
rw [comparisonAdjunction_counit_app]
-- Porting note: passing instances through
change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
infer_instance
-- Porting note: passing instances through
apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_
apply reflectsColimit_of_reflectsIsomorphisms
exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse
