English
If SpectrumRestricts a f holds and φ maps the restricted id to a, then the descended star-algebra homomorphism maps the restricted id to a as well.
Русский
Если SpectrumRestricts a f выполняется и φ отправляет ограниченный идентичный элемент в a, то спусковое звездоалгебраическое отображение тоже отправляет ограниченный идентичный элемент в a.
LaTeX
$$$\\mathrm{h.starAlgHom}(\\phi)(\\mathrm{restrict} \\; \\mathrm{spectrum}(R,a)\\; \\mathrm{id}) = a.$$$
Lean4
theorem starAlgHom_id {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A} {f : C(S, R)} (h : SpectrumRestricts a f)
(h_id : φ (.restrict (spectrum S a) <| .id S) = a) : h.starAlgHom φ (.restrict (spectrum R a) <| .id R) = a :=
by
simp only [SpectrumRestricts.starAlgHom_apply]
convert h_id
ext x
exact h.rightInvOn x.2