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 : Type v

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

• 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
• algebraMap_mem' (r : R) : (algebraMap R A) r ∈ self.carrier
• star_mem' {a : A} : a ∈ self.carrier → star a ∈ self.carrier

  The carrier is closed under the star operation.

@[implicit_reducible]

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] : SetLike (StarSubalgebra R A) A

@[implicit_reducible]

instance StarSubalgebra.instPartialOrder {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : PartialOrder (StarSubalgebra R A)

def StarSubalgebra.ofClass {S : Type u_6} {R : Type u_7} {A : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A] [SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] [StarMemClass S A] (s : S) : StarSubalgebra R A

The actual StarSubalgebra obtained from an element of a type satisfying SubsemiringClass, SMulMemClass and StarMemClass.

@[simp]

theorem StarSubalgebra.ofClass_carrier {S : Type u_6} {R : Type u_7} {A : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A] [SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] [StarMemClass S A] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance StarSubalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : CanLift (Set A) (StarSubalgebra R A) SetLike.coe fun (s : Set A) => (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ (∀ (r : R), (algebraMap R A) r ∈ s) ∧ ∀ {x : A}, x ∈ s → star x ∈ s

instance StarSubalgebra.starMemClass {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : StarMemClass (StarSubalgebra R A) A

instance StarSubalgebra.subsemiringClass {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : SubsemiringClass (StarSubalgebra R A) A

instance StarSubalgebra.smulMemClass {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : SMulMemClass (StarSubalgebra R A) R A

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] : SubringClass (StarSubalgebra R A) A

@[implicit_reducible]

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) : StarRing ↥s

@[implicit_reducible]

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

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

@[reducible]

def StarSubalgebra.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) : NonUnitalStarSubalgebra R A

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

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

@[simp]

theorem StarSubalgebra.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} {x : A} : x ∈ S.toNonUnitalStarSubalgebra ↔ x ∈ S

theorem StarSubalgebra.toNonUnitalStarSubalgebra_injective {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : Function.Injective toNonUnitalStarSubalgebra

theorem StarSubalgebra.toNonUnitalStarSubalgebra_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.toNonUnitalStarSubalgebra = U.toNonUnitalStarSubalgebra ↔ S = U

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

theorem StarSubalgebra.ext_iff {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} : S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ 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.carrier → star 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_injective {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : Function.Injective toSubalgebra

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) : StarSubalgebra R A

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

@[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.

@[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.

@[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₂) : Function.Injective ⇑(inclusion h)

@[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) : StarSubalgebra R B

Transport a star subalgebra via a star algebra homomorphism.

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) : Function.Injective (map 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 ↔ ∃ x ∈ S, 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) : StarSubalgebra R A

Preimage of a star subalgebra under a star algebra homomorphism.

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) : GaloisConnection (map f) (comap f)

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) : Function.Injective (comap 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) : comap (StarAlgHom.id R A) S = S

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) : StarSubalgebra R A

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

@[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 ↔ ∀ g ∈ s, 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) : centralizer R t ≤ centralizer R s

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

@[implicit_reducible]

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] : InvolutiveStar (Subalgebra R A)

The pointwise star of a subalgebra is a subalgebra.

@[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] : Monotone star

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) : star (Algebra.adjoin R s) = Algebra.adjoin R (star s)

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) : StarSubalgebra R A

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

@[simp]

theorem Subalgebra.coe_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) : ↑S.starClosure = ↑(S ⊔ star S)

@[simp]

theorem Subalgebra.mem_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) {x : A} : x ∈ S.starClosure ↔ x ∈ S ⊔ star S

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) : StarSubalgebra R A

The minimal star subalgebra that contains s.

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)

@[simp]

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)

@[simp]

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.mem_adjoin_of_mem (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} {x : A} (hx : x ∈ s) : x ∈ adjoin R s

@[simp]

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}

theorem StarAlgebra.gc {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] : GaloisConnection (adjoin R) SetLike.coe

def StarAlgebra.gi {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] : GaloisInsertion (adjoin R) SetLike.coe

Galois insertion between adjoin and coe.

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

@[simp]

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_mono {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s t : Set A} (H : s ⊆ t) : adjoin R s ≤ adjoin R t

@[simp]

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 = 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 s → Prop} (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 hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯) (star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (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 s → y ∈ adjoin R s → Prop} (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 hz → p y z hy hz → p (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 hy → p x z hx hz → p 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 hz → p y z hy hz → p (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 hy → p x z hx hz → p x (y * z) hx ⋯) (star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy) (star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p 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 x → p y → p (x + y)) (mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)) (star : ∀ (x : ↥(adjoin R s)), p x → p (star x)) : p a

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

theorem StarAlgebra.adjoin_le_centralizer_centralizer (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 ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R s)

theorem StarAlgebra.isMulCommutative_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} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : IsMulCommutative ↥(adjoin R s)

If all elements of s : Set A commute pairwise and with elements of star s, then adjoin R s is commutative.

@[reducible, inline, deprecated StarAlgebra.isMulCommutative_adjoin (since := "2026-03-11")]

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 : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : CommSemiring ↥(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].

instance StarAlgebra.instIsMulCommutative_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : Type u_5} [SetLike S A] [MulMemClass S A] [StarMemClass S A] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(adjoin R ↑s)

@[reducible, inline, deprecated StarAlgebra.isMulCommutative_adjoin (since := "2026-03-11")]

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 : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, 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].

instance StarAlgebra.isMulCommutative_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) [IsStarNormal x] : IsMulCommutative ↥(adjoin R {x})

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

@[implicit_reducible, deprecated StarAlgebra.isMulCommutative_adjoin_singleton (since := "2026-03-11")]

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.

@[implicit_reducible, deprecated StarAlgebra.isMulCommutative_adjoin_singleton (since := "2026-03-11")]

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.

Complete lattice structure

@[implicit_reducible]

instance StarSubalgebra.completeLattice {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] : CompleteLattice (StarSubalgebra R A)

@[implicit_reducible]

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] : Inhabited (StarSubalgebra R A)

@[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] : ↑⊤ = Set.univ

@[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} : x ∈ ⊤

@[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 ∈ S → x ∈ 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 ∈ T → x ∈ 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) = ⋂ s ∈ S, ↑s

@[simp]

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 ↔ ∀ p ∈ S, 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)

@[simp]

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} : x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R 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] : ↑⊥ = Set.range ⇑(algebraMap 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 ∈ s → f 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) : StarSubalgebra R A

The equalizer of two star R-algebra homomorphisms.

@[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) : StarAlgebra.adjoin R s ≤ equalizer f g

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) : StarSubalgebra.map f (StarAlgebra.adjoin R s) = StarAlgebra.adjoin R (⇑f '' s)

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) : StarSubalgebra R B

Range of a StarAlgHom as a star subalgebra.

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) : φ.range = StarSubalgebra.map φ ⊤

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.

@[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.

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.

@[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✝

@[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

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) : A →⋆ₐ[R] B

@[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] : Function.Injective (restrictScalars R)

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) : A ≃⋆ₐ[R] B

@[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

@[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✝

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] : Function.Injective (restrictScalars R)

def NonUnitalStarSubalgebra.toStarSubalgebra {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) : StarSubalgebra R A

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

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

theorem StarAlgebra.adjoin_nonUnitalStarSubalgebra (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 ↑(NonUnitalStarAlgebra.adjoin R s) = adjoin R s