comparisonAdjunction_counit_f — Mathlib

English

The counit component equals the lift from the Beck equalizer to the counit fork, highlighting the Beck construction.

Русский

Компонента сопряжения равна подъемy из эквалайзера Бека к ветвиCounit, отражая конструкцию Бека.

LaTeX

$$$((\mathrm{comparisonAdjunction}\ adj).\mathrm{counit}.app A).f = (\mathrm{beckEqualizer} A).lift (\mathrm{counitFork} A).$$$

Lean4

theorem comparisonAdjunction_counit_f
    [∀ 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 = (beckEqualizer A).lift (counitFork A) := by
  simp [Adjunction.homEquiv_counit]

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