English
The pointwise star operation sends a subalgebra to another subalgebra; moreover, applying star twice yields the original subalgebra.
Русский
Пусть задана точечная операция звезды над подалгеброй; она даёт другую подалгебру, и повторное применение звезды возвращает исходную подалгебру.
LaTeX
$$$$\text{star}(S) \text{ is a subalgebra, and } \text{star}(\text{star}(S))=S.$$$$
Lean4
/-- The pointwise `star` of a subalgebra is a subalgebra. -/
instance involutiveStar : InvolutiveStar (Subalgebra R A)
where
star
S :=
{ carrier := star S.carrier
mul_mem' := fun {x y} hx hy =>
by
simp only [Set.mem_star, Subalgebra.mem_carrier] at *
exact (star_mul x y).symm ▸ mul_mem hy hx
one_mem' := Set.mem_star.mp ((star_one A).symm ▸ one_mem S : star (1 : A) ∈ S)
add_mem' := fun {x y} hx hy =>
by
simp only [Set.mem_star, Subalgebra.mem_carrier] at *
exact (star_add x y).symm ▸ add_mem hx hy
zero_mem' := Set.mem_star.mp ((star_zero A).symm ▸ zero_mem S : star (0 : A) ∈ S)
algebraMap_mem' := fun r => by
simpa only [Set.mem_star, Subalgebra.mem_carrier, ← algebraMap_star_comm] using S.algebraMap_mem (star r) }
star_involutive
S := Subalgebra.ext fun x => ⟨fun hx => star_star x ▸ hx, fun hx => ((star_star x).symm ▸ hx : star (star x) ∈ S)⟩
