Non-unital Star Subalgebras #
- once we have scalar actions by semigroups (as opposed to monoids), implement the action of a non-unital subalgebra on the larger algebra.
In a star magma (i.e., a multiplication with an antimultiplicative involutive star operation), any star-closed subset which is also closed under multiplication is itself a star magma.
In a star ring (i.e., a non-unital, non-associative, semiring with an additive, antimultiplicative, involutive star operation), a star-closed non-unital subsemiring is itself a star ring.
In a star
star (r • m) = (star r) • m) any star-closed subset which is also
closed under the scalar action by
R is itself a star
Embedding of a non-unital star subalgebra into the non-unital star algebra.
- carrier : Set A
- zero_mem' : 0 ∈ s.carrier
NonUnitalStarSubalgebrais closed under the
A non-unital star subalgebra is a non-unital subalgebra which is closed under the
Copy of a non-unital star subalgebra with a new
carrier equal to the old one.
Useful to fix definitional equalities.
Transport a non-unital star subalgebra via a non-unital star algebra homomorphism.
Preimage of a non-unital star subalgebra under a non-unital star algebra homomorphism.
A non-unital subalgebra closed under
star is a non-unital star subalgebra.
Restrict the codomain of a non-unital star algebra homomorphism.
Restrict the codomain of a non-unital star algebra homomorphism
This is the bundled version of
The equalizer of two non-unital star
Restrict a non-unital star algebra homomorphism with a left inverse to an algebra isomorphism to its range.
This is a computable alternative to
Restrict an injective non-unital star algebra homomorphism to a star algebra isomorphism
The star closure of a subalgebra #
The minimal non-unital subalgebra that includes
S → T when
S is a non-unital star subalgebra contained in the non-unital star
The product of two non-unital star subalgebras is a non-unital star subalgebra.
Define a non-unital star algebra homomorphism on a directed supremum of non-unital star subalgebras by defining it on each non-unital star subalgebra, and proving that it agrees on the intersection of non-unital star subalgebras.
The center of a non-unital star algebra is the set of elements which commute with every element. They form a non-unital star subalgebra.
The centralizer of the star-closure of a set as a non-unital star subalgebra.