Star subalgebras #
A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
The centralizer of a *-closed set is a *-subalgebra.
- carrier : Set A
- one_mem' : 1 ∈ s.carrier
- zero_mem' : 0 ∈ s.carrier
- algebraMap_mem' : ∀ (r : R), ↑(algebraMap R A) r ∈ s.carrier
The
carrier
is closed under thestar
operation.
A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
Instances For
Copy of a star subalgebra with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Instances For
Embedding of a subalgebra into the algebra.
Instances For
The inclusion map between StarSubalgebra
s given by Subtype.map id
as a StarAlgHom
.
Instances For
Transport a star subalgebra via a star algebra homomorphism.
Instances For
Preimage of a star subalgebra under a star algebra homomorphism.
Instances For
The centralizer, or commutant, of the star-closure of a set as a star subalgebra.
Instances For
The star closure of a subalgebra #
The pointwise star
of a subalgebra is a subalgebra.
The star operation on Subalgebra
commutes with Algebra.adjoin
.
The StarSubalgebra
obtained from S : Subalgebra R A
by taking the smallest subalgebra
containing both S
and star S
.
Instances For
The star subalgebra generated by a set #
The minimal star subalgebra that contains s
.
Instances For
Galois insertion between adjoin
and coe
.
Instances For
If some predicate holds for all x ∈ (s : Set A)
and this predicate is closed under the
algebraMap
, addition, multiplication and star operations, then it holds for a ∈ adjoin R s
.
The difference with StarSubalgebra.adjoin_induction
is that this acts on the subtype.
If all elements of s : Set A
commute pairwise and also commute pairwise with elements of
star s
, then StarSubalgebra.adjoin R s
is commutative. See note [reducible non-instances].
Instances For
If all elements of s : Set A
commute pairwise and also commute pairwise with elements of
star s
, then StarSubalgebra.adjoin R s
is commutative. See note [reducible non-instances].
Instances For
The star subalgebra StarSubalgebra.adjoin R {x}
generated by a single x : A
is commutative
if x
is normal.
The star subalgebra StarSubalgebra.adjoin R {x}
generated by a single x : A
is commutative
if x
is normal.
Complete lattice structure #
The equalizer of two star R
-algebra homomorphisms.
Instances For
Range of a StarAlgHom
as a star subalgebra.
Instances For
Restriction of the codomain of a StarAlgHom
to a star subalgebra containing the range.
Instances For
Restriction of the codomain of a StarAlgHom
to its range.
Instances For
The StarAlgEquiv
onto the range corresponding to an injective StarAlgHom
.