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

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_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def star_subalgebra.algebra {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (s : star_subalgebra R A) :
Equations
@[protected, instance]
def star_subalgebra.star_module {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (s : star_subalgebra R A) :
@[simp]
theorem star_subalgebra.mem_carrier {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {s : star_subalgebra R A} {x : A} :
x s.carrier x s
@[ext]
theorem star_subalgebra.ext {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {S T : star_subalgebra R A} (h : (x : A), x S x T) :
S = T
@[simp]
theorem star_subalgebra.mem_to_subalgebra {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {S : star_subalgebra R A} {x : A} :
@[simp]
theorem star_subalgebra.to_subalgebra_le_iff {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {S₁ S₂ : star_subalgebra R A} :
S₁.to_subalgebra S₂.to_subalgebra S₁ S₂
@[protected]
def star_subalgebra.copy {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra 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
@[simp]
theorem star_subalgebra.coe_copy {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) (s : set A) (hs : s = S) :
(S.copy s hs) = s
theorem star_subalgebra.copy_eq {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) (s : set A) (hs : s = S) :
S.copy s hs = S
theorem star_subalgebra.algebra_map_mem {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) (r : R) :
@[protected]
theorem star_subalgebra.smul_mem {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) {x : A} (hx : x S) (r : R) :
r x S
def star_subalgebra.subtype {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) :

Embedding of a subalgebra into the algebra.

Equations
@[simp]
theorem star_subalgebra.coe_subtype {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) :
theorem star_subalgebra.subtype_apply {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) (x : S) :
@[simp]
theorem star_subalgebra.inclusion_apply {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {S₁ S₂ : star_subalgebra R A} (h : S₁ S₂) (ᾰ : {x // x S₁}) :
def star_subalgebra.inclusion {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {S₁ S₂ : star_subalgebra R A} (h : S₁ S₂) :

The inclusion map between star_subalgebras given by subtype.map id as a star_alg_hom.

Equations
@[simp]
theorem star_subalgebra.subtype_comp_inclusion {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] {S₁ S₂ : star_subalgebra R A} (h : S₁ S₂) :
def star_subalgebra.map {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] (f : A →⋆ₐ[R] B) (S : star_subalgebra R A) :

Transport a star subalgebra via a star algebra homomorphism.

Equations
theorem star_subalgebra.map_mono {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] {S₁ S₂ : star_subalgebra R A} {f : A →⋆ₐ[R] B} :
@[simp]
theorem star_subalgebra.map_id {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) :
theorem star_subalgebra.map_map {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] [semiring C] [star_ring C] [algebra R C] [star_module R C] (S : star_subalgebra R A) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
theorem star_subalgebra.mem_map {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] {S : star_subalgebra R A} {f : A →⋆ₐ[R] B} {y : B} :
y star_subalgebra.map f S (x : A) (H : x S), f x = y
@[simp]
theorem star_subalgebra.coe_map {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] (S : star_subalgebra R A) (f : A →⋆ₐ[R] B) :
def star_subalgebra.comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] (f : A →⋆ₐ[R] B) (S : star_subalgebra R B) :

Preimage of a star subalgebra under an star algebra homomorphism.

Equations
theorem star_subalgebra.comap_mono {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] {S₁ S₂ : star_subalgebra R B} {f : A →⋆ₐ[R] B} :
@[simp]
theorem star_subalgebra.comap_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] [semiring C] [star_ring C] [algebra R C] [star_module R C] (S : star_subalgebra R C) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
@[simp]
theorem star_subalgebra.mem_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] (S : star_subalgebra R B) (f : A →⋆ₐ[R] B) (x : A) :
@[simp, norm_cast]
theorem star_subalgebra.coe_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_module R A] [semiring B] [star_ring B] [algebra R B] [star_module R B] (S : star_subalgebra R B) (f : A →⋆ₐ[R] B) :
theorem set.star_mem_centralizer {A : Type u_3} [semiring A] [star_ring A] {a : A} {s : set A} (h : (a : A), a s has_star.star a s) (ha : a s.centralizer) :
def star_subalgebra.centralizer (R : Type u_2) {A : Type u_3} [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) :

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

Equations
@[simp]
theorem star_subalgebra.coe_centralizer (R : Type u_2) {A : Type u_3} [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) :
theorem star_subalgebra.mem_centralizer_iff (R : Type u_2) {A : Type u_3} [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} :
z star_subalgebra.centralizer R s w (g : A), g s g * z = z * g
theorem star_subalgebra.centralizer_le (R : Type u_2) {A : Type u_3} [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) :

The star closure of a subalgebra #

@[protected, instance]

The pointwise star of a subalgebra is a subalgebra.

Equations
@[simp]
theorem subalgebra.mem_star_iff {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (S : subalgebra R A) (x : A) :
@[simp]
theorem subalgebra.star_mem_star_iff {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (S : subalgebra R A) (x : A) :
@[simp]
theorem subalgebra.coe_star {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (S : subalgebra R A) :

The star operation on subalgebra commutes with algebra.adjoin.

def subalgebra.star_closure {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (S : subalgebra R A) :

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

Equations
theorem subalgebra.star_closure_le {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S₁ : subalgebra R A} {S₂ : star_subalgebra R A} (h : S₁ S₂.to_subalgebra) :
S₁.star_closure S₂
theorem subalgebra.star_closure_le_iff {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S₁ : subalgebra R A} {S₂ : star_subalgebra R A} :
S₁.star_closure S₂ S₁ S₂.to_subalgebra

The star subalgebra generated by a set #

def star_subalgebra.adjoin (R : Type u_2) {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (s : set A) :

The minimal star subalgebra that contains s.

Equations
Instances for star_subalgebra.adjoin
theorem star_subalgebra.subset_adjoin (R : Type u_2) {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (s : set A) :
@[protected]
@[protected]

Galois insertion between adjoin and coe.

Equations
theorem star_subalgebra.adjoin_le {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S : star_subalgebra R A} {s : set A} (hs : s S) :
theorem star_subalgebra.adjoin_le_iff {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S : star_subalgebra R A} {s : set A} :
theorem star_subalgebra.adjoin_induction {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {s : set A} {p : A Prop} {a : A} (h : a star_subalgebra.adjoin R s) (Hs : (x : A), x s p x) (Halg : (r : R), p ((algebra_map R A) r)) (Hadd : (x y : A), p x p y p (x + y)) (Hmul : (x y : A), p x p y p (x * y)) (Hstar : (x : A), p x p (has_star.star x)) :
p a

If some predicate holds for all x ∈ (s : set A) and this predicate is closed under the algebra_map, addition, multiplication and star operations, then it holds for a ∈ adjoin R s.

theorem star_subalgebra.adjoin_induction₂ {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {s : set A} {p : A A Prop} {a b : A} (ha : a star_subalgebra.adjoin R s) (hb : b star_subalgebra.adjoin R s) (Hs : (x : A), x s (y : A), y s p x y) (Halg : (r₁ r₂ : R), p ((algebra_map R A) r₁) ((algebra_map R A) r₂)) (Halg_left : (r : R) (x : A), x s p ((algebra_map R A) r) x) (Halg_right : (r : R) (x : A), x s p x ((algebra_map R A) r)) (Hadd_left : (x₁ x₂ y : A), p x₁ y p x₂ y p (x₁ + x₂) y) (Hadd_right : (x y₁ y₂ : A), p x y₁ p x y₂ p x (y₁ + y₂)) (Hmul_left : (x₁ x₂ y : A), p x₁ y p x₂ y p (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : A), p x y₁ p x y₂ p x (y₁ * y₂)) (Hstar : (x y : A), p x y p (has_star.star x) (has_star.star y)) (Hstar_left : (x y : A), p x y p (has_star.star x) y) (Hstar_right : (x y : A), p x y p x (has_star.star y)) :
p a b
theorem star_subalgebra.adjoin_induction' {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {s : set A} {p : (star_subalgebra.adjoin R s) Prop} (a : (star_subalgebra.adjoin R s)) (Hs : (x : A) (h : x s), p x, _⟩) (Halg : (r : R), p ((algebra_map R (star_subalgebra.adjoin R s)) r)) (Hadd : (x y : (star_subalgebra.adjoin R s)), p x p y p (x + y)) (Hmul : (x y : (star_subalgebra.adjoin R s)), p x p y p (x * y)) (Hstar : (x : (star_subalgebra.adjoin R s)), p x p (has_star.star x)) :
p a

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

@[reducible]
def star_subalgebra.adjoin_comm_semiring_of_comm (R : Type u_2) {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {s : set A} (hcomm : (a : A), a s (b : A), b s a * b = b * a) (hcomm_star : (a : A), a s (b : A), b s a * has_star.star b = has_star.star b * a) :

If all elements of s : set A commute pairwise and also commute pairwise with elements of star s, then star_subalgebra.adjoin R s is commutative. See note [reducible non-instances].

Equations
@[reducible]
def star_subalgebra.adjoin_comm_ring_of_comm (R : Type u) {A : Type v} [comm_ring R] [star_ring R] [ring A] [algebra R A] [star_ring A] [star_module R A] {s : set A} (hcomm : (a : A), a s (b : A), b s a * b = b * a) (hcomm_star : (a : A), a s (b : A), b s a * has_star.star b = has_star.star b * a) :

If all elements of s : set A commute pairwise and also commute pairwise with elements of star s, then star_subalgebra.adjoin R s is commutative. See note [reducible non-instances].

Equations
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations

Complete lattice structure #

@[protected, instance]
Equations
@[simp]
theorem star_subalgebra.coe_top {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] :
@[simp]
theorem star_subalgebra.mem_top {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {x : A} :
@[simp]
theorem star_subalgebra.mem_sup_left {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S T : star_subalgebra R A} {x : A} :
x S x S T
theorem star_subalgebra.mem_sup_right {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S T : star_subalgebra R A} {x : A} :
x T x S T
theorem star_subalgebra.mul_mem_sup {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S T : star_subalgebra R A} {x y : A} (hx : x S) (hy : y T) :
x * y S T
theorem star_subalgebra.map_sup {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] [star_module R B] (f : A →⋆ₐ[R] B) (S T : star_subalgebra R A) :
@[simp, norm_cast]
theorem star_subalgebra.coe_inf {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (S T : star_subalgebra R A) :
(S T) = S T
@[simp]
theorem star_subalgebra.mem_inf {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S T : star_subalgebra R A} {x : A} :
x S T x S x T
@[simp, norm_cast]
theorem star_subalgebra.coe_Inf {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] (S : set (star_subalgebra R A)) :
(has_Inf.Inf S) = (s : star_subalgebra R A) (H : s S), s
theorem star_subalgebra.mem_Inf {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S : set (star_subalgebra R A)} {x : A} :
x has_Inf.Inf S (p : star_subalgebra R A), p S x p
@[simp, norm_cast]
theorem star_subalgebra.coe_infi {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {ι : Sort u_1} {S : ι star_subalgebra R A} :
( (i : ι), S i) = (i : ι), (S i)
theorem star_subalgebra.mem_infi {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {ι : Sort u_1} {S : ι star_subalgebra R A} {x : A} :
(x (i : ι), S i) (i : ι), x S i
@[simp]
theorem star_subalgebra.infi_to_subalgebra {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {ι : Sort u_1} (S : ι star_subalgebra R A) :
( (i : ι), S i).to_subalgebra = (i : ι), (S i).to_subalgebra
theorem star_subalgebra.mem_bot {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {x : A} :
@[simp]
theorem star_subalgebra.coe_bot {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] :
theorem star_subalgebra.eq_top_iff {R : Type u_2} {A : Type u_3} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S : star_subalgebra R A} :
S = (x : A), x S
def star_alg_hom.equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] [hF : star_alg_hom_class F R A B] (f g : F) :

The equalizer of two star R-algebra homomorphisms.

Equations
@[simp]
theorem star_alg_hom.mem_equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] [hF : star_alg_hom_class F R A B] (f g : F) (x : A) :
theorem star_alg_hom.adjoin_le_equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] [hF : star_alg_hom_class F R A B] (f g : F) {s : set A} (h : set.eq_on f g s) :
theorem star_alg_hom.ext_of_adjoin_eq_top {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] [hF : star_alg_hom_class F R A B] {s : set A} (h : star_subalgebra.adjoin R s = ) ⦃f g : F⦄ (hs : set.eq_on f g s) :
f = g
theorem star_alg_hom.map_adjoin {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] [star_module R B] (f : A →⋆ₐ[R] B) (s : set A) :
theorem star_alg_hom.ext_adjoin {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] {s : set A} [star_alg_hom_class F R (star_subalgebra.adjoin R s) B] {f g : F} (h : (x : (star_subalgebra.adjoin R s)), x s f x = g x) :
f = g
theorem star_alg_hom.ext_adjoin_singleton {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [star_ring R] [semiring A] [algebra R A] [star_ring A] [star_module R A] [semiring B] [algebra R B] [star_ring B] {a : A} [star_alg_hom_class F R (star_subalgebra.adjoin R {a}) B] {f g : F} (h : f a, _⟩ = g a, _⟩) :
f = g