Lean4
/-- Coreflexive (crude) comonadicity theorem. If `F` has a right adjoint, `C` has and `F` preserves
coreflexive equalizers and `F` reflects isomorphisms, then `F` is comonadic.
-/
def comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms : ComonadicLeftAdjoint F
where
R := G
adj := adj
eqv :=
by
have : ∀ (X : adj.toComonad.Coalgebra), 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]
exact (IsLimit.conePointUniqueUpToIso (beckEqualizer X) (counitLimitOfPreservesEqualizer X)).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
have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) :=
by
apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
· rw [← G.map_comp, ← G.map_id]
exact congr_arg G.map (adj.left_triangle_components Y)
· rw [← G.map_id]
simp
apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
apply reflectsLimit_of_reflectsIsomorphisms
exact (comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse
