comparisonAdjunction_counit_app — Mathlib

English

The counit at B is the colimit_desc of a specific parallel pair with a counit cofork.

Русский

Коути единицы в B является описанием колимита по коллапсу параллельной пары с кофорком к counit.

LaTeX

$$$(\\mathrm{comparisonAdjunction}\\ adj).\\mathrm{counit}.\\mathrm{app} B = \\operatorname{colimit.desc}\\bigl(\\operatorname{parallelPair}(F.map (G.map (\\mathrm{adj.counit.app} B)), \\mathrm{adj.counit.app}(F.obj (G.obj B)))\\bigr)(\\mathrm{counitCofork}\\ adj B).$$$

Lean4

theorem comparisonAdjunction_counit_app
    [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) :
    (comparisonAdjunction adj).counit.app B = colimit.desc _ (counitCofork adj B) :=
  by
  apply coequalizer.hom_ext
  change
    coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ = coequalizer.π _ _ ≫ coequalizer.desc _ _
  simp [Adjunction.homEquiv_counit]

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