Star subalgebras #
A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
The centralizer of a *-closed set is a *-subalgebra.
def
star_subalgebra.to_subalgebra
{R : Type u}
{A : Type v}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A]
(self : star_subalgebra R A) :
subalgebra R A
Forgetting that a *-subalgebra is closed under *.
structure
star_subalgebra
(R : Type u)
(A : Type v)
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A] :
Type v
- carrier : set A
- mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ self.carrier
- star_mem' : ∀ {a : A}, a ∈ self.carrier → has_star.star a ∈ self.carrier
A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
Instances for star_subalgebra
- star_subalgebra.has_sizeof_inst
- star_subalgebra.set_like
- star_subalgebra.has_top
- star_subalgebra.inhabited
@[protected, instance]
def
star_subalgebra.set_like
(R : Type u)
(A : Type v)
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A] :
set_like (star_subalgebra R A) A
Equations
- star_subalgebra.set_like R A = {coe := star_subalgebra.carrier _inst_6, coe_injective' := _}
@[protected, instance]
def
star_subalgebra.has_top
(R : Type u)
(A : Type v)
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A] :
has_top (star_subalgebra R A)
@[protected, instance]
def
star_subalgebra.inhabited
(R : Type u)
(A : Type v)
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A] :
inhabited (star_subalgebra R A)
Equations
- star_subalgebra.inhabited R A = {default := ⊤}
def
star_subalgebra.centralizer
(R : Type u)
{A : Type v}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A]
(s : set A)
(w : ∀ (a : A), a ∈ s → has_star.star a ∈ s) :
star_subalgebra R A
The centralizer, or commutant, of a *-closed set as star subalgebra.
Equations
- star_subalgebra.centralizer R s w = {carrier := (subalgebra.centralizer R s).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _}
@[simp]
theorem
star_subalgebra.coe_centralizer
(R : Type u)
{A : Type v}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A]
(s : set A)
(w : ∀ (a : A), a ∈ s → has_star.star a ∈ s) :
↑(star_subalgebra.centralizer R s w) = s.centralizer
theorem
star_subalgebra.mem_centralizer_iff
(R : Type u)
{A : Type v}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A]
{s : set A}
{w : ∀ (a : A), a ∈ s → has_star.star a ∈ s}
{z : A} :
theorem
star_subalgebra.centralizer_le
(R : Type u)
{A : Type v}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A]
(s t : set A)
(ws : ∀ (a : A), a ∈ s → has_star.star a ∈ s)
(wt : ∀ (a : A), a ∈ t → has_star.star a ∈ t)
(h : s ⊆ t) :
star_subalgebra.centralizer R t wt ≤ star_subalgebra.centralizer R s ws