Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A)) := by

Mathlib declaration: CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit
Held-out module: Mathlib.CategoryTheory.Monad.Comonadicity
Banned modules (itself + downstream): 3
Reference proof premises (reachable / held-out): 0 / 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

No configuration has attempted this theorem yet.

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- The "main pair" for a coalgebra `(A, α)` is the pair of morphisms `(G α, η_GA)`. It is always a
`G`-cosplit pair, and will be used to construct the right adjoint to the comparison functor and show
it is an equivalence.
-/
instance main_pair_F_cosplit (A : adj.toComonad.Coalgebra) :
    F.IsCosplitPair (G.map A.a)
      (adj.unit.app (G.obj A.A)) where
  splittable := ⟨_, _, ⟨beckSplitEqualizer A⟩⟩