English
There is a star-hom class structure on WeakDual.Complex, compatible with the complex algebraic setup, enabling star-preserving maps from F to A → ℂ.
Русский
У WeakDual.Complex существует структура класса звездных гомоморфизмов, совместимая с конфигурацией комплексного алгебраического окружения, задающая звездоподобные отображения из F в A → ℂ.
LaTeX
$$$\text{There exists a }\mathrm{StarHomClass}\, F\, A\, \mathbb{C}$$$
Lean4
/-- This instance is provided instead of `StarHomClass` to avoid type class inference loops.
See note [lower instance priority] -/
noncomputable instance (priority := 100) instStarHomClass : StarHomClass F A ℂ where
map_star φ
a :=
by
suffices hsa : ∀ s : selfAdjoint A, (φ s)⋆ = φ s
by
rw [← realPart_add_I_smul_imaginaryPart a]
simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]
intro s
have := AlgHom.apply_mem_spectrum φ (s : A)
rw [selfAdjoint.val_re_map_spectrum s] at this
rcases this with ⟨⟨_, _⟩, _, heq⟩
simp only [Function.comp_apply] at heq
rw [← heq, RCLike.star_def]
exact RCLike.conj_ofReal _
