comparisonAdjunction_unit_f — Mathlib

English

The f-component of the unit is equal to the Beck coequalizer descent map.

Русский

f-компонента единицы равна отображению спуска по Beck-коэквалайзеру.

LaTeX

$$$((\\mathrm{comparisonAdjunction}\\ adj).\\mathrm{unit}.\\mathrm{app} A)^{-} = (\\mathrm{beckCoequalizer} A).\\mathrm{desc}(\\mathrm{unitCofork} A).$$$

Lean4

theorem comparisonAdjunction_unit_f [∀ 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 = (beckCoequalizer A).desc (unitCofork A) :=
  by
  apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A)
  rw [Cofork.IsColimit.π_desc]
  dsimp only [beckCofork_π, unitCofork_π]
  rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition,
    adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc]
  apply adj.right_triangle_components_assoc

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