toBialgHom_id — Mathlib

English

Let R be a commutative ring and M an object of HopfAlgCat R. The underlying bialgebra hom corresponding to the identity morphism on M is the identity bialgebra homomorphism on M. In other words, applying the forgetful construction to the identity yields the identity in the category of bialgebras.

Русский

Пусть R является коммутативным кольцом, и M — объект HopfAlgCat R. Соответствующий гомоморфизм-билогбы для тождества на M равен тождественному биалгебрному гомоморфизму на M.

LaTeX

$$$\\operatorname{Hom}^{\\text{HopfAlgCat}}_{R}(\\mathrm{id}_M) = \\mathrm{BialgHom.id}_{R, M}.$$$

Lean4

@[simp]
theorem toBialgHom_id {M : HopfAlgCat.{v} R} : Hom.toBialgHom (𝟙 M) = BialgHom.id _ _ :=
  rfl

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