English
The main pair for a coalgebra (A, α) given by the adjunction is always a G-cosplit pair, i.e., the pair (G.map A.a, η_GA) is cosplit with respect to F.
Русский
Основная пара для коалгебры (A, α), образованная при помощи сопоставления, всегда кослитна по отношению к F, то есть (G.map A.a, η_GA) образуют кослитную пару.
LaTeX
$$$\text{The main pair } (G.map A.a, \eta_{G A}) \text{ is a } F\text{-cosplit pair.}$$$
Lean4
/-- The "main pair" for a coalgebra `(A, α)` is the pair of morphisms `(G α, η_GA)`. It is always a
coreflexive pair, and will be used to construct the left adjoint to the comparison functor and show
it is an equivalence.
-/
instance main_pair_coreflexive (A : adj.toComonad.Coalgebra) :
IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A)) :=
by
apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
· rw [← G.map_comp, ← G.map_id]
exact congr_arg G.map A.counit
· rw [adj.right_triangle_components]
rfl
