Lean4
/-- To show `G` is a monadic right adjoint, we can show it preserves and reflects `G`-split
coequalizers, and `D` has them.
-/
def monadicOfHasPreservesReflectsGSplitCoequalizers [HasCoequalizerOfIsSplitPair G] [PreservesColimitOfIsSplitPair G]
[ReflectsColimitOfIsSplitPair G] : 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]
change IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
exact (IsColimit.coconePointUniqueUpToIso _ _).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 _ _ _ _ _ _ _ _ ?_
letI _ : G.IsSplitPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))) :=
MonadicityInternal.main_pair_G_split _ ((comparison adj).obj Y)
infer_instance
exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse
