comparisonAdjunction_unit_f_aux — Mathlib

English

A technical auxiliary formula giving the f-component of the unit of the comparison adjunction in terms of a hom-equivalence and a coequalizer.

Русский

Техническая вспомогательная формула для f-части единицы сопряжения сравнения через гом-эквивалентность и коэквалайзеры.

LaTeX

$$$\\text{For all } A,\\ ((\\mathrm{comparisonAdjunction}\\ adj).\\mathrm{unit}.\\mathrm{app}\\;A)^{\\,f} = \\mathrm{adj.homEquiv}\\;A.A\\;\\_\\;\\bigl(\\mathrm{coequalizer}.\\pi( F.map A.a, \\mathrm{adj.counit.app}(F.obj A.A))\\bigr).$$$

Lean4

theorem comparisonAdjunction_unit_f_aux
    [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) :
    ((comparisonAdjunction adj).unit.app A).f =
      adj.homEquiv A.A _ (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) :=
  congr_arg (adj.homEquiv _ _) (Category.comp_id _)

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