comparisonAdjunction_counit_f_aux

English

A simple auxiliary formula expresses the counit component under the adjunction via the equalizer morphism, relating to the hom-equivalence.

Русский

Простейшая вспомогательная формула выражает компоненты чинного сопряжения через эквалайзер и гомэквивалентность.

LaTeX

$$$((\mathrm{comparisonAdjunction}\ adj).\mathrm{counit}.app A).f = (\adj.homEquiv _ A.A)^{-1} (\operatorname{equalizer.ι}(G.map A.a)(\adj.unit.app (G.obj A.A))).$$$

Lean4

theorem comparisonAdjunction_counit_f_aux
    [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) :
    ((comparisonAdjunction adj).counit.app A).f =
      (adj.homEquiv _ A.A).symm (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) :=
  congr_arg (adj.homEquiv _ _).symm (Category.id_comp _)

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