counit_surjective — Mathlib

English

In a bialgebra over R, the counit map ε: A → R is surjective; every r ∈ R has a preimage under ε, for instance ε(η(r)) = r where η is the structure map.

Русский

В биалгебре над R отображение counit: A → R является сюръективным; для каждого элемента r ∈ R существует элемент в A с образом ε(η(r)) = r, где η — каноническое отображение.

LaTeX

$$$\\operatorname{Surjective}(\\mathrm{Coalgebra.counit}: A \\to_R R)$$$

Lean4

theorem counit_surjective : Surjective (Coalgebra.counit : A →ₗ[R] R) :=
  RightInverse.surjective counit_algebraMap

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