English
Equality of cfc_nHom and its cfc_nHom_of_cfcHom variant under a special congruence.
Русский
Равенство функций cfc_nHom и cfc_nHom_of_cfcHom в особом случае.
LaTeX
$$$$ cfc\\!_nHom ha = cfc\\!_nHom\\_of\\_cfcHom R ha $$$$
Lean4
theorem cfcₙHom_of_cfcHom_map_quasispectrum {a : A} (ha : p a) :
∀ f : C(σₙ R a, R)₀, σₙ R (cfcₙHom_of_cfcHom R ha f) = range f :=
by
intro f
simp only [cfcₙHom_of_cfcHom]
rw [quasispectrum_eq_spectrum_union_zero]
simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe]
rw [cfcHom_map_spectrum ha]
ext x
constructor
· rintro (⟨x, rfl⟩ | rfl)
· exact ⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, rfl⟩
· exact ⟨0, map_zero f⟩
· rintro ⟨x, rfl⟩
have hx := x.2
simp_rw [quasispectrum_eq_spectrum_union_zero R a] at hx
obtain (hx | hx) := hx
· exact Or.inl ⟨⟨x.1, hx⟩, rfl⟩
· apply Or.inr
simp only [Set.mem_singleton_iff] at hx ⊢
rw [show x = 0 from Subtype.val_injective hx, map_zero]
