Star subalgebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
The centralizer of a *-closed set is a *-subalgebra.
def
star_subalgebra.to_subalgebra
{R : Type u}
{A : Type v}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A]
(self : star_subalgebra R A) :
subalgebra R A
Forgetting that a *-subalgebra is closed under *.
structure
star_subalgebra
(R : Type u)
(A : Type v)
[comm_semiring R]
[star_ring R]
[semiring A]
[star_ring A]
[algebra R A]
[star_module R A] :
Type v
- carrier : set A
- mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ self.carrier
- star_mem' : ∀ {a : A}, a ∈ self.carrier → has_star.star a ∈ self.carrier
A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
Instances for star_subalgebra
@[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] :
set_like (star_subalgebra R A) A
Equations
- star_subalgebra.set_like = {coe := star_subalgebra.carrier _inst_6, coe_injective' := _}
@[protected, instance]
def
star_subalgebra.star_mem_class
{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] :
star_mem_class (star_subalgebra R A) A
Equations
@[protected, instance]
def
star_subalgebra.subsemiring_class
{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] :
subsemiring_class (star_subalgebra R A) A
@[protected, instance]
def
star_subalgebra.subring_class
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[star_ring R]
[ring A]
[star_ring A]
[algebra R A]
[star_module R A] :
subring_class (star_subalgebra R A) A
@[protected, instance]
def
star_subalgebra.star_ring
{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
- s.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := has_star.star (star_mem_class.has_star s)}, star_involutive := _}, star_mul := _}, star_add := _}
@[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) :
star_module R ↥s
@[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} :
@[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} :
x ∈ S.to_subalgebra ↔ x ∈ S
@[simp]
theorem
star_subalgebra.coe_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) :
↑(S.to_subalgebra) = ↑S
theorem
star_subalgebra.to_subalgebra_injective
{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] :
theorem
star_subalgebra.to_subalgebra_inj
{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 U : star_subalgebra R A} :
S.to_subalgebra = U.to_subalgebra ↔ S = U
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) :
star_subalgebra R A
Copy of a star subalgebra with a new carrier equal to the old one. Useful to fix definitional
equalities.
@[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) :
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) :
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) :
⇑(algebra_map R A) r ∈ S
theorem
star_subalgebra.srange_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 : star_subalgebra R A) :
(algebra_map R A).srange ≤ S.to_subalgebra.to_subsemiring
theorem
star_subalgebra.range_subset
{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) :
set.range ⇑(algebra_map R A) ⊆ ↑S
theorem
star_subalgebra.range_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 : star_subalgebra R A) :
set.range ⇑(algebra_map R A) ≤ ↑S
@[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) :
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.
@[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.to_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) :
@[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₁}) :
⇑(star_subalgebra.inclusion h) ᾰ = subtype.map id h ᾰ
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.
theorem
star_subalgebra.inclusion_injective
{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₂) :
@[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₂) :
S₂.subtype.comp (star_subalgebra.inclusion h) = S₁.subtype
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) :
star_subalgebra R B
Transport a star subalgebra via a star algebra homomorphism.
Equations
- star_subalgebra.map f S = {carrier := (subalgebra.map f.to_alg_hom S.to_subalgebra).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _}
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} :
S₁ ≤ S₂ → star_subalgebra.map f S₁ ≤ star_subalgebra.map f S₂
theorem
star_subalgebra.map_injective
{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}
(hf : function.injective ⇑f) :
@[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) :
star_subalgebra.map (star_alg_hom.id R A) S = S
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) :
star_subalgebra.map g (star_subalgebra.map f S) = star_subalgebra.map (g.comp f) S
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} :
theorem
star_subalgebra.map_to_subalgebra
{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} :
@[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) :
star_subalgebra R A
Preimage of a star subalgebra under an star algebra homomorphism.
Equations
- star_subalgebra.comap f S = {carrier := (subalgebra.comap f.to_alg_hom S.to_subalgebra).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _}
theorem
star_subalgebra.map_le_iff_le_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 A}
{f : A →⋆ₐ[R] B}
{U : star_subalgebra R B} :
star_subalgebra.map f S ≤ U ↔ S ≤ star_subalgebra.comap f U
theorem
star_subalgebra.gc_map_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) :
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} :
S₁ ≤ S₂ → star_subalgebra.comap f S₁ ≤ star_subalgebra.comap f S₂
theorem
star_subalgebra.comap_injective
{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}
(hf : function.surjective ⇑f) :
@[simp]
theorem
star_subalgebra.comap_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) :
star_subalgebra.comap (star_alg_hom.id R A) S = S
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) :
star_subalgebra.comap f (star_subalgebra.comap g S) = star_subalgebra.comap (g.comp f) S
@[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) :
x ∈ star_subalgebra.comap f S ↔ ⇑f x ∈ S
@[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) :
star_subalgebra R A
The centralizer, or commutant, of a *-closed set as star subalgebra.
Equations
- star_subalgebra.centralizer R s w = {carrier := (subalgebra.centralizer R s).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _}
@[simp]
theorem
star_subalgebra.coe_centralizer
(R : Type u_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) :
↑(star_subalgebra.centralizer R s w) = s.centralizer
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} :
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) :
star_subalgebra.centralizer R t wt ≤ star_subalgebra.centralizer R s ws
The star closure of a subalgebra #
@[protected, instance]
def
subalgebra.has_involutive_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] :
The pointwise star of a subalgebra is a subalgebra.
Equations
- subalgebra.has_involutive_star = {to_has_star := {star := λ (S : subalgebra R A), {carrier := has_star.star S.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}}, star_involutive := _}
@[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) :
x ∈ has_star.star S ↔ has_star.star x ∈ S
@[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) :
has_star.star x ∈ has_star.star S ↔ x ∈ S
@[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) :
↑(has_star.star S) = has_star.star ↑S
theorem
subalgebra.star_mono
{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
subalgebra.star_adjoin_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) :
has_star.star (algebra.adjoin R s) = algebra.adjoin R (has_star.star s)
The star operation on subalgebra commutes with algebra.adjoin.
@[simp]
theorem
subalgebra.star_closure_carrier
{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_closure.carrier = (S ⊔ has_star.star S).carrier
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) :
star_subalgebra R A
The star_subalgebra obtained from S : subalgebra R A by taking the smallest subalgebra
containing both S and star S.
Equations
- S.star_closure = {carrier := (S ⊔ has_star.star S).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _}
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) :
star_subalgebra R A
The minimal star subalgebra that contains s.
Equations
- star_subalgebra.adjoin R s = {carrier := (algebra.adjoin R (s ∪ has_star.star s)).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _}
Instances for ↥star_subalgebra.adjoin
@[simp]
theorem
star_subalgebra.adjoin_carrier
(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) :
(star_subalgebra.adjoin R s).carrier = (algebra.adjoin R (s ∪ has_star.star s)).carrier
theorem
star_subalgebra.adjoin_eq_star_closure_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) :
star_subalgebra.adjoin R s = (algebra.adjoin R s).star_closure
theorem
star_subalgebra.adjoin_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]
(s : set A) :
(star_subalgebra.adjoin R s).to_subalgebra = algebra.adjoin R (s ∪ has_star.star s)
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) :
s ⊆ ↑(star_subalgebra.adjoin R s)
theorem
star_subalgebra.star_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) :
has_star.star s ⊆ ↑(star_subalgebra.adjoin R s)
theorem
star_subalgebra.self_mem_adjoin_singleton
(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) :
x ∈ star_subalgebra.adjoin R {x}
theorem
star_subalgebra.star_self_mem_adjoin_singleton
(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) :
has_star.star x ∈ star_subalgebra.adjoin R {x}
@[protected]
theorem
star_subalgebra.gc
{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] :
@[protected]
def
star_subalgebra.gi
{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] :
Galois insertion between adjoin and coe.
Equations
- star_subalgebra.gi = {choice := λ (s : set A) (hs : ↑(star_subalgebra.adjoin R s) ≤ s), (star_subalgebra.adjoin R s).copy s _, gc := _, le_l_u := _, choice_eq := _}
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) :
star_subalgebra.adjoin R 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} :
star_subalgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
theorem
subalgebra.star_closure_eq_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 : subalgebra R 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
- star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star = {add := semiring.add (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, add_assoc := _, zero := semiring.zero (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (star_subalgebra.adjoin R s).to_subalgebra.to_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[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
- star_subalgebra.adjoin_comm_ring_of_comm R hcomm hcomm_star = {add := comm_semiring.add (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), add_assoc := _, zero := comm_semiring.zero (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (star_subalgebra.adjoin R s).to_subalgebra.to_ring, sub := ring.sub (star_subalgebra.adjoin R s).to_subalgebra.to_ring, sub_eq_add_neg := _, zsmul := ring.zsmul (star_subalgebra.adjoin R s).to_subalgebra.to_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (star_subalgebra.adjoin R s).to_subalgebra.to_ring, nat_cast := comm_semiring.nat_cast (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), one := comm_semiring.one (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_semiring.mul (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), mul_assoc := _, one_mul := _, mul_one := _, npow := comm_semiring.npow (star_subalgebra.adjoin_comm_semiring_of_comm R hcomm hcomm_star), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[protected, instance]
def
star_subalgebra.adjoin_comm_semiring_of_is_star_normal
(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)
[is_star_normal x] :
comm_semiring ↥(star_subalgebra.adjoin R {x})
The star subalgebra star_subalgebra.adjoin R {x} generated by a single x : A is commutative
if x is normal.
@[protected, instance]
def
star_subalgebra.adjoin_comm_ring_of_is_star_normal
(R : Type u)
{A : Type v}
[comm_ring R]
[star_ring R]
[ring A]
[algebra R A]
[star_ring A]
[star_module R A]
(x : A)
[is_star_normal x] :
comm_ring ↥(star_subalgebra.adjoin R {x})
The star subalgebra star_subalgebra.adjoin R {x} generated by a single x : A is commutative
if x is normal.
Equations
- star_subalgebra.adjoin_comm_ring_of_is_star_normal R x = {add := ring.add (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, add_assoc := _, zero := ring.zero (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, sub := ring.sub (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, sub_eq_add_neg := _, zsmul := ring.zsmul (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, nat_cast := ring.nat_cast (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, one := ring.one (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (star_subalgebra.adjoin R {x}).to_subalgebra.to_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Complete lattice structure #
@[protected, instance]
def
star_subalgebra.complete_lattice
{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] :
@[protected, instance]
def
star_subalgebra.inhabited
{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] :
inhabited (star_subalgebra R A)
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.top_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] :
@[simp]
theorem
star_subalgebra.to_subalgebra_eq_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]
{S : star_subalgebra R A} :
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} :
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} :
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) :
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) :
star_subalgebra.map f (S ⊔ T) = star_subalgebra.map f S ⊔ star_subalgebra.map f 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 T : star_subalgebra R A) :
@[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} :
@[simp]
theorem
star_subalgebra.inf_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]
(S T : star_subalgebra R A) :
(S ⊓ T).to_subalgebra = S.to_subalgebra ⊓ T.to_subalgebra
@[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]
theorem
star_subalgebra.Inf_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]
(S : set (star_subalgebra R A)) :
@[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} :
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} :
@[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.bot_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] :
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} :
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) :
star_subalgebra R A
The equalizer of two star R-algebra homomorphisms.
@[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) :
star_subalgebra.map f (star_subalgebra.adjoin R s) = star_subalgebra.adjoin R (⇑f '' s)
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