subsingleton — Mathlib

English

If the subalgebra is subsingleton, then there is at most one NonUnitalStarAlgHom A B; any two such homomorphisms are equal.

Русский

Если подалгебра является одиночной, то гомоморфизм NonUnitalStarAlgHom A B уникален; любые два такие гомоморфизма совпадают.

LaTeX

$$$\\mathrm{Subsingleton}\\,(A \\to⋆ₙₐ[R] B)$$$

Lean4

instance _root_.NonUnitalStarAlgHom.subsingleton [Subsingleton (NonUnitalStarSubalgebra R A)] :
    Subsingleton (A →⋆ₙₐ[R] B) :=
  ⟨fun f g =>
    NonUnitalStarAlgHom.ext fun a =>
      have : a ∈ (⊥ : NonUnitalStarSubalgebra R A) := Subsingleton.elim (⊤ : NonUnitalStarSubalgebra R A) ⊥ ▸ mem_top
      (mem_bot.mp this).symm ▸ (map_zero f).trans (map_zero g).symm⟩

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