Lean4
/-- To show `F` is a comonadic left adjoint, we can show it preserves and reflects `F`-split
equalizers, and `C` has them.
-/
def comonadicOfHasPreservesReflectsFSplitEqualizers [HasEqualizerOfIsCosplitPair F] [PreservesLimitOfIsCosplitPair F]
[ReflectsLimitOfIsCosplitPair F] : ComonadicLeftAdjoint F
where
R := G
adj := adj
eqv :=
by
have : ∀ (X : Coalgebra adj.toComonad), IsIso ((comparisonAdjunction adj).counit.app X) :=
by
intro X
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
· change IsIso ((comparisonAdjunction adj).counit.app X).f
rw [comparisonAdjunction_counit_f]
change IsIso (IsLimit.conePointUniqueUpToIso (beckEqualizer X) (counitLimitOfPreservesEqualizer X)).inv
exact (IsLimit.conePointUniqueUpToIso _ _).isIso_inv
have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) :=
by
intro Y
rw [comparisonAdjunction_unit_app]
change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
infer_instance
apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
letI _ : F.IsCosplitPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) :=
ComonadicityInternal.main_pair_F_cosplit _ ((comparison adj).obj Y)
infer_instance
exact (comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse
