condition — Mathlib

English

For an object X in an algebra over a monad, the map top maps to the coequalizer agree with the bottom map after passing through the common projection π: the top and bottom maps commute with π.

Русский

Для объекта X над алгеброй монад, отображения верхнее и нижнее согласованы через общий проекция π: topMap(X)∘π_X = bottomMap(X)∘π_X.

LaTeX

$$$FreeCoequalizer.topMap X \;\gg\; FreeCoequalizer.\pi X = FreeCoequalizer.bottomMap X \;\gg\; FreeCoequalizer.\pi X.$$$

Lean4

theorem condition :
    FreeCoequalizer.topMap X ≫ FreeCoequalizer.π X = FreeCoequalizer.bottomMap X ≫ FreeCoequalizer.π X :=
  Algebra.Hom.ext X.assoc.symm

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