main_pair_reflexive — Mathlib

English

For every A in adj.toMonad.Algebra, there exists a coequalizer of F.map A.a and adj.counit.app(F.obj A.A).

Русский

Для каждого A из adj.toMonad.Algebra существует коэквализатор F.map A.a и adj.counit.app(F.obj A.A).

LaTeX

$$$\\forall A, \\operatorname{HasCoequalizer}\\bigl(F\\map A.a, \\; \\mathrm{adj.counit.app}(F.obj A.A)\\bigr).$$$

Lean4

/-- The "main pair" for an algebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a
reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it
is an equivalence.
-/
instance main_pair_reflexive (A : adj.toMonad.Algebra) : IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A)) :=
  by
  apply IsReflexivePair.mk' (F.map (adj.unit.app _)) _ _
  · rw [← F.map_comp, ← F.map_id]
    exact congr_arg F.map A.unit
  · rw [adj.left_triangle_components]
    rfl

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