instFaithfulAlgebraToMonadComparison

English

If R is faithful, then the comparison functor from L ⊣ R to the corresponding monad comparison is faithful; more precisely, it injects morphisms on algebra maps.

Русский

Если R верно сохраняет различение морфизмов, то сопоставляющее отображение монадного сопоставления является инъективным на морфизмах алгебр.

LaTeX

$$$$\\text{Faithful}(\\mathrm{Monad.comparison}(L\\!\\!\\!R))$$ given $R$ faithful and $L\\dashv R$.$$

Lean4

instance [R.Faithful] (h : L ⊣ R) : (Monad.comparison h).Faithful where
  map_injective {_ _} _ _ w := R.map_injective (congr_arg Monad.Algebra.Hom.f w :)

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