mathlib documentation

algebra.star.subalgebra

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) :

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

A *-subalgebra is a subalgebra of a *-algebra which is closed under *.

Instances for star_subalgebra
@[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] :
Equations
@[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] :
Equations
@[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] :
Equations
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 shas_star.star a s) :

The centralizer, or commutant, of a *-closed set as star subalgebra.

Equations
@[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 shas_star.star a s) :
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 shas_star.star a s} {z : A} :
z star_subalgebra.centralizer R s w ∀ (g : A), g sg * z = z * g
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 shas_star.star a s) (wt : ∀ (a : A), a thas_star.star a t) (h : s t) :