English
The star-closure of the range of charAlgHom forms a star-subalgebra of bounded complex-valued functions on V.
Русский
Замкнутое относительно операции звезда множество образов charAlgHom образует подалгебру с операцией звезда в пространстве ограниченных функций на V со значениями в ℂ.
LaTeX
$$$\\text{charPoly}(he,hL) \\text{ is a StarSubalgebra } \\mathbb{C}(V, \\mathbb{C})$.$$
Lean4
/-- The family of `ℂ`-linear combinations of `char he hL w, w : W`, is closed under `star`. -/
theorem star_mem_range_charAlgHom (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) {x : V →ᵇ ℂ}
(hx : x ∈ (charAlgHom he hL).range) : star x ∈ (charAlgHom he hL).range :=
by
simp only [AlgHom.mem_range] at hx ⊢
obtain ⟨y, rfl⟩ := hx
let z := Finsupp.mapRange star (star_zero _) y
let f : W ↪ W := ⟨fun x ↦ -x, (fun _ _ ↦ neg_inj.mp)⟩
refine ⟨z.embDomain f, ?_⟩
ext1 u
simp only [charAlgHom_apply, Finsupp.support_embDomain, Finset.sum_map, Finsupp.embDomain_apply, star_apply, star_sum,
star_mul', Circle.star_addChar]
rw [Finsupp.support_mapRange_of_injective (star_zero _) y star_injective]
simp [z, f]
