starAlgHom_id — Mathlib

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

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