Idempotent.lean

import Mathlib.CategoryTheory.Adjunction.Basic
import Mathlib.CategoryTheory.Monad.Algebra
import Mathlib.CategoryTheory.Conj
import Mathlib.Tactic.TFAE

namespace CategoryTheory

variable {C : Type*} [Category C] {D : Type*} [Category D] {F : C ⥤ D} {G : D ⥤ C}
  {E : Type*} [Category E] {H : D ⥤ E} {K : E ⥤ D}

namespace Monad

variable (T : Monad C)

@[mk_iff]
structure IsIdempotent : Prop where
  out : ∀ c, T.η.app (T.obj c) = T.map (T.η.app c)

lemma IsIdempotent.tfae (T : Monad C) :
    [T.IsIdempotent
    , IsIso T.μ
    , ∀ c, Mono (T.μ.app c)
    , whiskerLeft T.toFunctor T.η = whiskerRight T.η T.toFunctor -- should insert unitors
    , ∀ A : Algebra T, IsIso A.a
    , ∀ (A B : Algebra T), (T.forget.map : (A ⟶ B) → (A.A ⟶ B.A)).Bijective
    ].TFAE := by
  rw [isIdempotent_iff]
  tfae_have 1 ↔ 4
  · exact Iff.symm <| Iff.trans (NatTrans.ext_iff _ _) Function.funext_iff
  tfae_have 2 → 3
  · intros; exact StrongMono.mono
  tfae_have 3 → 1
  · intro h c
    erw [← cancel_mono (T.μ.app c), T.left_unit, T.right_unit]
  tfae_have 1 → 5
  · intro h A
    refine ⟨⟨T.η.app A.A, ?_, A.unit⟩⟩
    convert congrArg T.map A.unit using 1
    · exact Eq.trans (T.η.naturality A.a) <| Eq.trans (congrArg (· ≫ _) (h A.A)) (T.map_comp _ _).symm
    · exact Eq.symm (T.map_id A.A)
  tfae_have 5 → 2
  · intro h
    haveI : ∀ c, IsIso (T.μ.app c) := fun c => h (T.free.obj c)
    exact NatIso.isIso_of_isIso_app (μ T)
  tfae_have 5 → 6
  · intro h A B
    -- obtain ⟨ ⟩
    refine ⟨Faithful.map_injective, ?_⟩
    admit
  admit
    -- erw [T.η.naturality, h, ← T.map_comp, A.unit, T.map_id]
    -- admit

end Monad

namespace Comonad

@[mk_iff]
structure IsIdempotent (T : Comonad C) : Prop where
  h : IsIso T.δ

end Comonad

namespace Adjunction

@[mk_iff]
structure IsIdempotent (adj : F ⊣ G) : Prop where
  h : IsIso (whiskerRight adj.unit F)
  -- whiskerUnitComm : whiskerLeft (F ⋙ G) adj.unit = whiskerRight adj.unit (F ⋙ G)

lemma IsIdempotent.tfae (adj : F ⊣ G) :
    [adj.IsIdempotent
    , IsIso (whiskerRight adj.unit F)
    , IsIso (whiskerLeft F adj.counit)
    , 
    ].TFAE := sorry

end Adjunction

end CategoryTheory