English
Let f be a nonunital star-algebra homomorphism A →⋆ₙₐ[R] B together with witnesses h1, h2, h3, h4, h5 that certify its structure. Then the canonical constructor that rebuilds the same homomorphism from f and the witnesses yields the original map; i.e., the constructed object equals f.
Русский
Пусть имеется ненулевой ⋆-алгоморфизм A →⋆ₙₐ[R] B с данными h1, h2, h3, h4, h5, удостоверяющими структуру. Тогда канонический конструктор, собирающий тот же гомоморфизм, возвращает исходную функцию; т. е. полученная структура равна f.
LaTeX
$$$\bigl\langle\langle\langle\langle f, h_1 \rangle, h_2\rangle, h_3\rangle, h_4\rangle, h_5\rangle = f$$$
Lean4
@[simp]
theorem mk_coe (f : A →⋆ₙₐ[R] B) (h₁ h₂ h₃ h₄ h₅) : (⟨⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩, h₅⟩ : A →⋆ₙₐ[R] B) = f :=
by
ext
rfl
