subsingleton_to_ring — Mathlib

English

There is at most one hom from any bialgebra A to its base ring R; the hom-set is a singleton.

Русский

Множество гомоморфизмов биалгебры A в базовое кольцо R является синглетоном (не более одного элемента).

LaTeX

$$Subsingleton (BialgHom R A R)$$

Lean4

instance subsingleton_to_ring : Subsingleton (A →ₐc[R] R) :=
  ⟨fun _ _ => BialgHom.coe_coalgHom_injective (Subsingleton.elim _ _)⟩

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