comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms

Lean4

/-- An alternate version of Beck's comonadicity theorem. If `F` reflects isomorphisms, preserves
equalizers of `F`-cosplit pairs and `C` has equalizers of `F`-cosplit pairs, then it is comonadic.
-/
def comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms [F.ReflectsIsomorphisms]
    [HasEqualizerOfIsCosplitPair F] [PreservesLimitOfIsCosplitPair F] : ComonadicLeftAdjoint F :=
  by
  have : ReflectsLimitOfIsCosplitPair F :=
    ⟨fun f g _ => by
      have := HasEqualizerOfIsCosplitPair.out F f g
      apply reflectsLimit_of_reflectsIsomorphisms⟩
  apply comonadicOfHasPreservesReflectsFSplitEqualizers adj

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