main_pair_F_cosplit — Mathlib

English

There is a bijection between morphisms from (comparison adj).obj B to A and morphisms from B to comparisonRightAdjointObj adj A, natural in B.

Русский

Существует биекция между морфизмами ((comparison adj).obj B) → A и B → comparisonRightAdjointObj adj A, естественная по B.

LaTeX

$$$((\mathrm{comparison}\ adj).obj B \to A) \cong (B \to \mathrm{comparisonRightAdjointObj}\ adj A).$$$

Lean4

/-- 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⟩⟩

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