Documentation

Mathlib.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.

structure StarSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] extends Subalgebra R A :

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

instance StarSubalgebra.setLike {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] :
Equations
instance StarSubalgebra.subringClass {R : Type u_6} {A : Type u_7} [CommRing R] [StarRing R] [Ring A] [StarRing A] [Algebra R A] [StarModule R A] :
instance StarSubalgebra.starRing {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : StarSubalgebra R A) :
Equations
instance StarSubalgebra.algebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : StarSubalgebra R A) :
Algebra R s
Equations
  • s.algebra = s.algebra'
instance StarSubalgebra.starModule {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : StarSubalgebra R A) :
StarModule R s

Turn a StarSubalgebra into a NonUnitalStarSubalgebra by forgetting that it contains 1.

Equations
  • S.toNonUnitalStarSubalgebra = { carrier := S.carrier, add_mem' := , zero_mem' := , mul_mem' := , smul_mem' := , star_mem' := }
theorem StarSubalgebra.one_mem_toNonUnitalStarSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
1 S.toNonUnitalStarSubalgebra
theorem StarSubalgebra.mem_carrier {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {s : StarSubalgebra R A} {x : A} :
x s.carrier x s
theorem StarSubalgebra.ext {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S T : StarSubalgebra R A} (h : ∀ (x : A), x S x T) :
S = T
@[simp]
theorem StarSubalgebra.coe_mk {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : Subalgebra R A) (h : ∀ {a : A}, a S.carrierstar a S.carrier) :
{ toSubalgebra := S, star_mem' := h } = S
@[simp]
theorem StarSubalgebra.mem_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} {x : A} :
x S.toSubalgebra x S
@[simp]
theorem StarSubalgebra.coe_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
S.toSubalgebra = S
theorem StarSubalgebra.toSubalgebra_inj {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S U : StarSubalgebra R A} :
S.toSubalgebra = U.toSubalgebra S = U
theorem StarSubalgebra.toSubalgebra_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} :
S₁.toSubalgebra S₂.toSubalgebra S₁ S₂
def StarSubalgebra.copy {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (s : Set A) (hs : s = S) :

Copy of a star subalgebra with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
  • S.copy s hs = { toSubalgebra := S.copy s hs, star_mem' := }
@[simp]
theorem StarSubalgebra.coe_copy {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (s : Set A) (hs : s = S) :
(S.copy s hs) = s
theorem StarSubalgebra.copy_eq {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (s : Set A) (hs : s = S) :
S.copy s hs = S
theorem StarSubalgebra.algebraMap_mem {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (r : R) :
(algebraMap R A) r S
theorem StarSubalgebra.rangeS_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
(algebraMap R A).rangeS S.toSubsemiring
theorem StarSubalgebra.range_subset {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
Set.range (algebraMap R A) S
theorem StarSubalgebra.range_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
Set.range (algebraMap R A) S
theorem StarSubalgebra.smul_mem {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) {x : A} (hx : x S) (r : R) :
r x S
def StarSubalgebra.subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
S →⋆ₐ[R] A

Embedding of a subalgebra into the algebra.

Equations
  • S.subtype = { toFun := Subtype.val, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := , map_star' := }
@[simp]
theorem StarSubalgebra.coe_subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
S.subtype = Subtype.val
theorem StarSubalgebra.subtype_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (x : S) :
S.subtype x = x
@[simp]
theorem StarSubalgebra.toSubalgebra_subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
S.val = S.subtype.toAlgHom
def StarSubalgebra.inclusion {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ S₂) :
S₁ →⋆ₐ[R] S₂

The inclusion map between StarSubalgebras given by Subtype.map id as a StarAlgHom.

Equations
@[simp]
theorem StarSubalgebra.inclusion_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ S₂) (a✝ : S₁) :
(inclusion h) a✝ = Subtype.map id h a✝
theorem StarSubalgebra.inclusion_injective {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ S₂) :
@[simp]
theorem StarSubalgebra.subtype_comp_inclusion {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ S₂) :
S₂.subtype.comp (inclusion h) = S₁.subtype
def StarSubalgebra.map {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R A) :

Transport a star subalgebra via a star algebra homomorphism.

Equations
theorem StarSubalgebra.map_mono {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S₁ S₂ : StarSubalgebra R A} {f : A →⋆ₐ[R] B} :
S₁ S₂map f S₁ map f S₂
theorem StarSubalgebra.map_injective {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {f : A →⋆ₐ[R] B} (hf : Function.Injective f) :
@[simp]
theorem StarSubalgebra.map_id {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
map (StarAlgHom.id R A) S = S
theorem StarSubalgebra.map_map {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] (S : StarSubalgebra R A) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
map g (map f S) = map (g.comp f) S
@[simp]
theorem StarSubalgebra.mem_map {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {y : B} :
y map f S xS, f x = y
theorem StarSubalgebra.map_toSubalgebra {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} :
(map f S).toSubalgebra = Subalgebra.map f.toAlgHom S.toSubalgebra
@[simp]
theorem StarSubalgebra.coe_map {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (S : StarSubalgebra R A) (f : A →⋆ₐ[R] B) :
(map f S) = f '' S
def StarSubalgebra.comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) :

Preimage of a star subalgebra under a star algebra homomorphism.

Equations
theorem StarSubalgebra.map_le_iff_le_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {U : StarSubalgebra R B} :
map f S U S comap f U
theorem StarSubalgebra.gc_map_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) :
theorem StarSubalgebra.comap_mono {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S₁ S₂ : StarSubalgebra R B} {f : A →⋆ₐ[R] B} :
S₁ S₂comap f S₁ comap f S₂
theorem StarSubalgebra.comap_injective {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {f : A →⋆ₐ[R] B} (hf : Function.Surjective f) :
@[simp]
theorem StarSubalgebra.comap_id {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
theorem StarSubalgebra.comap_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] (S : StarSubalgebra R C) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
comap f (comap g S) = comap (g.comp f) S
@[simp]
theorem StarSubalgebra.mem_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (S : StarSubalgebra R B) (f : A →⋆ₐ[R] B) (x : A) :
x comap f S f x S
@[simp]
theorem StarSubalgebra.coe_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (S : StarSubalgebra R B) (f : A →⋆ₐ[R] B) :
(comap f S) = f ⁻¹' S
def StarSubalgebra.centralizer (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :

The centralizer, or commutant, of the star-closure of a set as a star subalgebra.

Equations
@[simp]
theorem StarSubalgebra.coe_centralizer (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :
(centralizer R s) = (s star s).centralizer
theorem StarSubalgebra.mem_centralizer_iff (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {s : Set A} {z : A} :
z centralizer R s gs, g * z = z * g star g * z = z * star g
theorem StarSubalgebra.centralizer_le (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s t : Set A) (h : s t) :
theorem StarSubalgebra.centralizer_toSubalgebra (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :
(centralizer R s).toSubalgebra = Subalgebra.centralizer R (s star s)
theorem StarSubalgebra.coe_centralizer_centralizer (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :
(centralizer R (centralizer R s)) = (s star s).centralizer.centralizer

The star closure of a subalgebra #

instance Subalgebra.involutiveStar {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :

The pointwise star of a subalgebra is a subalgebra.

Equations
@[simp]
theorem Subalgebra.mem_star_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) (x : A) :
x star S star x S
theorem Subalgebra.star_mem_star_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) (x : A) :
star x star S x S
@[simp]
theorem Subalgebra.coe_star {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
(star S) = star S
theorem Subalgebra.star_mono {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
theorem Subalgebra.star_adjoin_comm (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :

The star operation on Subalgebra commutes with Algebra.adjoin.

def Subalgebra.starClosure {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :

The StarSubalgebra obtained from S : Subalgebra R A by taking the smallest subalgebra containing both S and star S.

Equations
  • S.starClosure = { toSubalgebra := S star S, star_mem' := }
@[simp]
theorem Subalgebra.starClosure_carrier {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
S.starClosure = ⋂ (t : Subsemiring A), ⋂ (_ : Set.range (algebraMap R A) t S t star S t), t
theorem Subalgebra.starClosure_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
S.starClosure.toSubalgebra = S star S
theorem Subalgebra.starClosure_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ S₂.toSubalgebra) :
S₁.starClosure S₂
theorem Subalgebra.starClosure_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} :
S₁.starClosure S₂ S₁ S₂.toSubalgebra

The star subalgebra generated by a set #

def StarAlgebra.adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :

The minimal star subalgebra that contains s.

Equations
@[simp]
theorem StarAlgebra.adjoin_carrier (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
(adjoin R s) = ⋂ (t : Subsemiring A), ⋂ (_ : Set.range (algebraMap R A) t s t star s t), t
theorem StarAlgebra.adjoin_eq_starClosure_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
adjoin R s = (Algebra.adjoin R s).starClosure
theorem StarAlgebra.adjoin_toSubalgebra (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
(adjoin R s).toSubalgebra = Algebra.adjoin R (s star s)
theorem StarAlgebra.subset_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
s (adjoin R s)
theorem StarAlgebra.star_subset_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
star s (adjoin R s)
theorem StarAlgebra.self_mem_adjoin_singleton (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (x : A) :
x adjoin R {x}
theorem StarAlgebra.star_self_mem_adjoin_singleton (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (x : A) :
star x adjoin R {x}

Galois insertion between adjoin and coe.

Equations
theorem StarAlgebra.adjoin_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {s : Set A} (hs : s S) :
adjoin R s S
theorem StarAlgebra.adjoin_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {s : Set A} :
adjoin R s S s S
theorem StarAlgebra.adjoin_eq {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : StarSubalgebra R A) :
adjoin R S = S
theorem StarAlgebra.adjoin_eq_span {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
Subalgebra.toSubmodule (adjoin R s).toSubalgebra = Submodule.span R (Submonoid.closure (s star s))
theorem StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : NonUnitalStarSubalgebra R A) :
Subalgebra.toSubmodule (adjoin R s).toSubalgebra = Submodule.span R {1} s.toSubmodule
theorem Subalgebra.starClosure_eq_adjoin {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
S.starClosure = StarAlgebra.adjoin R S
theorem StarAlgebra.adjoin_induction {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : (x : A) → x adjoin R sProp} (mem : ∀ (x : A) (h : x s), p x ) (algebraMap : ∀ (r : R), p ((algebraMap R A) r) ) (add : ∀ (x y : A) (hx : x adjoin R s) (hy : y adjoin R s), p x hxp y hyp (x + y) ) (mul : ∀ (x y : A) (hx : x adjoin R s) (hy : y adjoin R s), p x hxp y hyp (x * y) ) (star : ∀ (x : A) (hx : x adjoin R s), p x hxp (star x) ) {a : A} (ha : a adjoin R s) :
p a ha

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.

theorem StarAlgebra.adjoin_induction₂ {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : (x y : A) → x adjoin R sy adjoin R sProp} (mem_mem : ∀ (x y : A) (hx : x s) (hy : y s), p x y ) (algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ) (algebraMap_left : ∀ (r : R) (x : A) (hx : x s), p ((algebraMap R A) r) x ) (algebraMap_right : ∀ (r : R) (x : A) (hx : x s), p x ((algebraMap R A) r) ) (add_left : ∀ (x y z : A) (hx : x adjoin R s) (hy : y adjoin R s) (hz : z adjoin R s), p x z hx hzp y z hy hzp (x + y) z hz) (add_right : ∀ (x y z : A) (hx : x adjoin R s) (hy : y adjoin R s) (hz : z adjoin R s), p x y hx hyp x z hx hzp x (y + z) hx ) (mul_left : ∀ (x y z : A) (hx : x adjoin R s) (hy : y adjoin R s) (hz : z adjoin R s), p x z hx hzp y z hy hzp (x * y) z hz) (mul_right : ∀ (x y z : A) (hx : x adjoin R s) (hy : y adjoin R s) (hz : z adjoin R s), p x y hx hyp x z hx hzp x (y * z) hx ) (star_left : ∀ (x y : A) (hx : x adjoin R s) (hy : y adjoin R s), p x y hx hyp (star x) y hy) (star_right : ∀ (x y : A) (hx : x adjoin R s) (hy : y adjoin R s), p x y hx hyp x (star y) hx ) {a b : A} (ha : a adjoin R s) (hb : b adjoin R s) :
p a b ha hb
theorem StarAlgebra.adjoin_induction_subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : (adjoin R s)Prop} (a : (adjoin R s)) (mem : ∀ (x : A) (h : x s), p x, ) (algebraMap : ∀ (r : R), p ((algebraMap R (adjoin R s)) r)) (add : ∀ (x y : (adjoin R s)), p xp yp (x + y)) (mul : ∀ (x y : (adjoin R s)), p xp yp (x * y)) (star : ∀ (x : (adjoin R s)), p xp (star x)) :
p a

The difference with StarSubalgebra.adjoin_induction is that this acts on the subtype.

@[reducible, inline]
abbrev StarAlgebra.adjoinCommSemiringOfComm (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} (hcomm : as, bs, a * b = b * a) (hcomm_star : as, bs, a * star b = star b * a) :

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].

Equations
@[reducible, inline]
abbrev StarAlgebra.adjoinCommRingOfComm (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} (hcomm : as, bs, a * b = b * a) (hcomm_star : as, bs, a * star b = star b * a) :
CommRing (adjoin R s)

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].

Equations
instance StarAlgebra.adjoinCommSemiringOfIsStarNormal (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (x : A) [IsStarNormal x] :
CommSemiring (adjoin R {x})

The star subalgebra StarSubalgebra.adjoin R {x} generated by a single x : A is commutative if x is normal.

Equations
instance StarAlgebra.adjoinCommRingOfIsStarNormal (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A] [StarRing A] [StarModule R A] (x : A) [IsStarNormal x] :
CommRing (adjoin R {x})

The star subalgebra StarSubalgebra.adjoin R {x} generated by a single x : A is commutative if x is normal.

Equations

Complete lattice structure #

instance StarSubalgebra.inhabited {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
Equations
@[simp]
theorem StarSubalgebra.coe_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
@[simp]
theorem StarSubalgebra.mem_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {x : A} :
@[simp]
theorem StarSubalgebra.top_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
.toSubalgebra =
@[simp]
theorem StarSubalgebra.toSubalgebra_eq_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} :
S.toSubalgebra = S =
theorem StarSubalgebra.mem_sup_left {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S T : StarSubalgebra R A} {x : A} :
x Sx S T
theorem StarSubalgebra.mem_sup_right {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S T : StarSubalgebra R A} {x : A} :
x Tx S T
theorem StarSubalgebra.mul_mem_sup {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S T : StarSubalgebra R A} {x y : A} (hx : x S) (hy : y T) :
x * y S T
theorem StarSubalgebra.map_sup {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S T : StarSubalgebra R A) :
map f (S T) = map f S map f T
theorem StarSubalgebra.map_inf {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (S T : StarSubalgebra R A) :
map f (S T) = map f S map f T
@[simp]
theorem StarSubalgebra.coe_inf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S T : StarSubalgebra R A) :
(S T) = S T
@[simp]
theorem StarSubalgebra.mem_inf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S T : StarSubalgebra R A} {x : A} :
x S T x S x T
@[simp]
theorem StarSubalgebra.inf_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S T : StarSubalgebra R A) :
(S T).toSubalgebra = S.toSubalgebra T.toSubalgebra
@[simp]
theorem StarSubalgebra.coe_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Set (StarSubalgebra R A)) :
(sInf S) = sS, s
theorem StarSubalgebra.mem_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : Set (StarSubalgebra R A)} {x : A} :
x sInf S pS, x p
@[simp]
theorem StarSubalgebra.sInf_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Set (StarSubalgebra R A)) :
(sInf S).toSubalgebra = sInf (toSubalgebra '' S)
@[simp]
theorem StarSubalgebra.coe_iInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {ι : Sort u_5} {S : ιStarSubalgebra R A} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
theorem StarSubalgebra.mem_iInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {ι : Sort u_5} {S : ιStarSubalgebra R A} {x : A} :
x ⨅ (i : ι), S i ∀ (i : ι), x S i
theorem StarSubalgebra.map_iInf {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] {ι : Sort u_5} [Nonempty ι] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (s : ιStarSubalgebra R A) :
map f (iInf s) = ⨅ (i : ι), map f (s i)
@[simp]
theorem StarSubalgebra.iInf_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {ι : Sort u_5} (S : ιStarSubalgebra R A) :
(⨅ (i : ι), S i).toSubalgebra = ⨅ (i : ι), (S i).toSubalgebra
theorem StarSubalgebra.bot_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
.toSubalgebra =
theorem StarSubalgebra.mem_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {x : A} :
@[simp]
theorem StarSubalgebra.coe_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
theorem StarSubalgebra.eq_top_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} :
S = ∀ (x : A), x S
theorem StarAlgHom.ext_adjoin {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] {s : Set A} [FunLike F (↥(StarAlgebra.adjoin R s)) B] [AlgHomClass F R (↥(StarAlgebra.adjoin R s)) B] [StarHomClass F (↥(StarAlgebra.adjoin R s)) B] {f g : F} (h : ∀ (x : (StarAlgebra.adjoin R s)), x sf x = g x) :
f = g
theorem StarAlgHom.ext_adjoin_singleton {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] {a : A} [FunLike F (↥(StarAlgebra.adjoin R {a})) B] [AlgHomClass F R (↥(StarAlgebra.adjoin R {a})) B] [StarHomClass F (↥(StarAlgebra.adjoin R {a})) B] {f g : F} (h : f a, = g a, ) :
f = g
def StarAlgHom.equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [FunLike F A B] [AlgHomClass F R A B] [StarHomClass F A B] (f g : F) :

The equalizer of two star R-algebra homomorphisms.

Equations
@[simp]
theorem StarAlgHom.mem_equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [FunLike F A B] [AlgHomClass F R A B] [StarHomClass F A B] (f g : F) (x : A) :
x equalizer f g f x = g x
theorem StarAlgHom.adjoin_le_equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [FunLike F A B] [AlgHomClass F R A B] [StarHomClass F A B] (f g : F) {s : Set A} (h : Set.EqOn (⇑f) (⇑g) s) :
theorem StarAlgHom.ext_of_adjoin_eq_top {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [FunLike F A B] [AlgHomClass F R A B] [StarHomClass F A B] {s : Set A} (h : StarAlgebra.adjoin R s = ) ⦃f g : F (hs : Set.EqOn (⇑f) (⇑g) s) :
f = g
theorem StarAlgHom.map_adjoin {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [StarModule R B] (f : A →⋆ₐ[R] B) (s : Set A) :
def StarAlgHom.range {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (φ : A →⋆ₐ[R] B) :

Range of a StarAlgHom as a star subalgebra.

Equations
  • φ.range = { toSubalgebra := φ.range, star_mem' := }
theorem StarAlgHom.range_eq_map_top {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [StarModule R B] (φ : A →⋆ₐ[R] B) :
def StarAlgHom.codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) :
A →⋆ₐ[R] S

Restriction of the codomain of a StarAlgHom to a star subalgebra containing the range.

Equations
  • f.codRestrict S hf = { toAlgHom := f.codRestrict S.toSubalgebra hf, map_star' := }
@[simp]
theorem StarAlgHom.coe_codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) (x : A) :
((f.codRestrict S hf) x) = f x
@[simp]
theorem StarAlgHom.subtype_comp_codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) :
S.subtype.comp (f.codRestrict S hf) = f
theorem StarAlgHom.injective_codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) :
Function.Injective (f.codRestrict S hf) Function.Injective f
def StarAlgHom.rangeRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) :
A →⋆ₐ[R] f.range

Restriction of the codomain of a StarAlgHom to its range.

Equations
  • f.rangeRestrict = f.codRestrict f.range
noncomputable def StarAlgEquiv.ofInjective {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) :
A ≃⋆ₐ[R] f.range

The StarAlgEquiv onto the range corresponding to an injective StarAlgHom.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem StarAlgEquiv.ofInjective_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (a : A) :
(ofInjective f hf) a = f.rangeRestrict a
@[simp]
theorem StarAlgEquiv.ofInjective_symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (a✝ : (↑f).range) :
(ofInjective f hf).symm a✝ = (AlgEquiv.ofInjective (↑f) hf).invFun a✝
def StarAlgHom.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A →⋆ₐ[S] B) :
Equations
@[simp]
theorem StarAlgHom.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A →⋆ₐ[S] B) (a✝ : A) :
(restrictScalars R f) a✝ = f a✝
theorem StarAlgHom.restrictScalars_injective (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] :
def StarAlgEquiv.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) :
Equations
  • StarAlgEquiv.restrictScalars R f = { toFun := f, invFun := f.invFun, left_inv := , right_inv := , map_mul' := , map_add' := , map_star' := , map_smul' := }
@[simp]
theorem StarAlgEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) (a✝ : B) :
(restrictScalars R f).symm a✝ = f.invFun a✝
@[simp]
theorem StarAlgEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) (a : A) :
(restrictScalars R f) a = f a
theorem StarAlgEquiv.restrictScalars_injective (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] :

Turn a non-unital star subalgebra containing 1 into a StarSubalgebra.

Equations
  • S.toStarSubalgebra h1 = { carrier := S.carrier, mul_mem' := , one_mem' := h1, add_mem' := , zero_mem' := , algebraMap_mem' := , star_mem' := }
theorem StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
S.toNonUnitalStarSubalgebra.toStarSubalgebra = S
theorem NonUnitalStarSubalgebra.toStarSubalgebra_toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : NonUnitalStarSubalgebra R A) (h1 : 1 S) :
(S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S
theorem NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :
adjoin R s (StarAlgebra.adjoin R s).toNonUnitalStarSubalgebra