English
Let R be a commutative semiring with involution and A a semiring carrying an R-algebra structure, with star operations on R and A. If S is a subalgebra of A over R, then its star-closure is the smallest star-subalgebra of A containing S. Equivalently, the star-closure is the subalgebra generated by S together with its star S.
Русский
Пусть R—коммутативная полугруппа с инволюцией, A — полугруппа с структурой R-алгебры, и задано звёздное умножение. Пусть S — подалгебра A над R. Тогда звёздное замыкание S есть наименьшая звёздная подалгебра A, содержащая S; эквивалентно подалгебре, сгенерированной S ∪ S^*.
LaTeX
$$$\operatorname{StarClosure}(S) = S \lor S^{*}$, i.e. the star-closure of $S$ is the smallest star-subalgebra of $A$ containing $S$ and $S^{*}$.$$
Lean4
/-- The `StarSubalgebra` obtained from `S : Subalgebra R A` by taking the smallest subalgebra
containing both `S` and `star S`. -/
def starClosure (S : Subalgebra R A) : StarSubalgebra R A
where
toSubalgebra := S ⊔ star S
star_mem' := fun {a} ha =>
by
simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *
rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]
simpa using ha
