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 :

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.

Instances For

source

theorem StarSubalgebra.star_mem' {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (self : StarSubalgebra R A) {a : A} :

a ∈ self.carrier → star a ∈ self.carrier

The carrier is closed under the star operation.

source

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

Equations

StarSubalgebra.setLike = { coe := fun (S : StarSubalgebra R A) => S.carrier, coe_injective' := ⋯ }

source

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

Equations

⋯ = ⋯

source

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

Equations

⋯ = ⋯

source

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

Equations

⋯ = ⋯

source

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

Equations

⋯ = ⋯

source

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 { x : A // x ∈ s }

Equations

s.starRing = StarRing.mk ⋯

source

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 { x : A // x ∈ s }

Equations

s.algebra = s.algebra'

source

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 { x : A // x ∈ s }

Equations

⋯ = ⋯

source

@[simp]

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

source

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 : StarSubalgebra R A} {T : StarSubalgebra R A} :

S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T

source

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 : StarSubalgebra R A} {T : StarSubalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) :

S = T

source

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

source

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

source

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

source

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 StarSubalgebra.toSubalgebra

source

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 : StarSubalgebra R A} {U : StarSubalgebra R A} :

S.toSubalgebra = U.toSubalgebra ↔ S = U

source

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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} :

S₁.toSubalgebra ≤ S₂.toSubalgebra ↔ S₁ ≤ S₂

source

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.

Equations

S.copy s hs = { toSubalgebra := S.copy s hs, star_mem' := ⋯ }

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

{ x : A // x ∈ S } →⋆ₐ[R] A

Embedding of a subalgebra into the algebra.

Equations

S.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

source

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

source

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 : { x : A // x ∈ S }) :

S.subtype x = ↑x

source

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

source

@[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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) :

∀ (a : { x : A // x ∈ S₁ }), (StarSubalgebra.inclusion h) a = Subtype.map id h a

source

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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) :

{ x : A // x ∈ S₁ } →⋆ₐ[R] { x : A // x ∈ S₂ }

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

Equations

StarSubalgebra.inclusion h = { toFun := Subtype.map id h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

source

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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) :

Function.Injective ⇑(StarSubalgebra.inclusion h)

source

@[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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) :

S₂.subtype.comp (StarSubalgebra.inclusion h) = S₁.subtype

source

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.

Equations

StarSubalgebra.map f S = { toSubalgebra := Subalgebra.map f.toAlgHom S.toSubalgebra, star_mem' := ⋯ }

source

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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} {f : A →⋆ₐ[R] B} :

S₁ ≤ S₂ → StarSubalgebra.map f S₁ ≤ StarSubalgebra.map f S₂

source

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 (StarSubalgebra.map f)

source

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

StarSubalgebra.map (StarAlgHom.id R A) S = S

source

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

StarSubalgebra.map g (StarSubalgebra.map f S) = StarSubalgebra.map (g.comp f) S

source

@[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 ∈ StarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y

source

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

(StarSubalgebra.map f S).toSubalgebra = Subalgebra.map f.toAlgHom S.toSubalgebra

source

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

↑(StarSubalgebra.map f S) = ⇑f '' ↑S

source

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.

Equations

StarSubalgebra.comap f S = { toSubalgebra := Subalgebra.comap f.toAlgHom S.toSubalgebra, star_mem' := ⋯ }

source

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

StarSubalgebra.map f S ≤ U ↔ S ≤ StarSubalgebra.comap f U

source

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 (StarSubalgebra.map f) (StarSubalgebra.comap f)

source

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₁ : StarSubalgebra R B} {S₂ : StarSubalgebra R B} {f : A →⋆ₐ[R] B} :

S₁ ≤ S₂ → StarSubalgebra.comap f S₁ ≤ StarSubalgebra.comap f S₂

source

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 (StarSubalgebra.comap f)

source

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

StarSubalgebra.comap (StarAlgHom.id R A) S = S

source

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

StarSubalgebra.comap f (StarSubalgebra.comap g S) = StarSubalgebra.comap (g.comp f) S

source

@[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 ∈ StarSubalgebra.comap f S ↔ f x ∈ S

source

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

↑(StarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S

source

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.

Equations

StarSubalgebra.centralizer R s = { toSubalgebra := Subalgebra.centralizer R (s ∪ star s), star_mem' := ⋯ }

source

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

↑(StarSubalgebra.centralizer R s) = (s ∪ star s).centralizer

source

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 ∈ StarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

source

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 : Set A) (t : Set A) (h : s ⊆ t) :

StarSubalgebra.centralizer R t ≤ StarSubalgebra.centralizer R s

The star closure of a subalgebra #

source

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.

Equations

Subalgebra.involutiveStar = InvolutiveStar.mk ⋯

source

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

source

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

source

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

source

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

source

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.

source

@[simp]

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

↑S.starClosure = ⋂ (t : Subsemiring A), ⋂ (_ : Set.range ⇑(algebraMap R A) ⊆ ↑t ∧ ↑S ⊆ ↑t ∧ star ↑S ⊆ ↑t), ↑t

source

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.

Equations

S.starClosure = { toSubalgebra := S ⊔ star S, star_mem' := ⋯ }

source

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

source

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₂

source

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 #

source

@[simp]

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

↑(StarAlgebra.adjoin R s) = ⋂ (t : Subsemiring A), ⋂ (_ : Set.range ⇑(algebraMap R A) ⊆ ↑t ∧ s ⊆ ↑t ∧ star s ⊆ ↑t), ↑t

source

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.

Equations

StarAlgebra.adjoin R s = { toSubalgebra := Algebra.adjoin R (s ∪ star s), star_mem' := ⋯ }

source

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

StarAlgebra.adjoin R s = (Algebra.adjoin R s).starClosure

source

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

(StarAlgebra.adjoin R s).toSubalgebra = Algebra.adjoin R (s ∪ star s)

source

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 ⊆ ↑(StarAlgebra.adjoin R s)

source

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 ⊆ ↑(StarAlgebra.adjoin R s)

source

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 ∈ StarAlgebra.adjoin R {x}

source

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 ∈ StarAlgebra.adjoin R {x}

source

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 (StarAlgebra.adjoin R) SetLike.coe

source

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 (StarAlgebra.adjoin R) SetLike.coe

Galois insertion between adjoin and coe.

Equations

StarAlgebra.gi = { choice := fun (s : Set A) (hs : ↑(StarAlgebra.adjoin R s) ≤ s) => (StarAlgebra.adjoin R s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

source

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

StarAlgebra.adjoin R s ≤ S

source

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

StarAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S

source

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

StarAlgebra.adjoin R ↑S = S

source

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 (StarAlgebra.adjoin R s).toSubalgebra = Submodule.span R ↑(Submonoid.closure (s ∪ star s))

source

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

source

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 : A → Prop} {a : A} (h : a ∈ StarAlgebra.adjoin R s) (mem : ∀ x ∈ s, p x) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r)) (add : ∀ (x y : A), p x → p y → p (x + y)) (mul : ∀ (x y : A), p x → p y → p (x * y)) (star : ∀ (x : A), p x → p (Star.star x)) :

p a

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.

source

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 : A → A → Prop} {a : A} {b : A} (ha : a ∈ StarAlgebra.adjoin R s) (hb : b ∈ StarAlgebra.adjoin R s) (Hs : ∀ x ∈ s, ∀ y ∈ s, p x y) (Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)) (Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x) (Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap 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 (star x) (star y)) (Hstar_left : ∀ (x y : A), p x y → p (star x) y) (Hstar_right : ∀ (x y : A), p x y → p x (star y)) :

p a b

source

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 ∈ StarAlgebra.adjoin R s } → Prop} (a : { x : A // x ∈ StarAlgebra.adjoin R s }) (mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R { x : A // x ∈ StarAlgebra.adjoin R s }) r)) (add : ∀ (x y : { x : A // x ∈ StarAlgebra.adjoin R s }), p x → p y → p (x + y)) (mul : ∀ (x y : { x : A // x ∈ StarAlgebra.adjoin R s }), p x → p y → p (x * y)) (star : ∀ (x : { x : A // x ∈ StarAlgebra.adjoin R s }), p x → p (Star.star x)) :

p a

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

source

@[reducible, inline]

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

CommSemiring { x : A // x ∈ StarAlgebra.adjoin R s }

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

Equations

StarAlgebra.adjoinCommSemiringOfComm R hcomm hcomm_star = CommSemiring.mk ⋯

source

@[reducible, inline]

abbrev StarAlgebra.adjoinCommRingOfComm (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) :

CommRing { x : A // x ∈ StarAlgebra.adjoin R s }

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

Equations

StarAlgebra.adjoinCommRingOfComm R hcomm hcomm_star = CommRing.mk ⋯

source

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 { x_1 : A // x_1 ∈ StarAlgebra.adjoin R {x} }

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

Equations

StarAlgebra.adjoinCommSemiringOfIsStarNormal R x = StarAlgebra.adjoinCommSemiringOfComm R ⋯ ⋯

source

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 { x_1 : A // x_1 ∈ StarAlgebra.adjoin R {x} }

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

Equations

StarAlgebra.adjoinCommRingOfIsStarNormal R x = CommRing.mk ⋯

Complete lattice structure #

source

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)

Equations

StarSubalgebra.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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)

Equations

StarSubalgebra.inhabited = { default := ⊤ }

source

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

source

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

source

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

source

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

source

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 : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} :

x ∈ S → x ∈ S ⊔ T

source

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 : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} :

x ∈ T → x ∈ S ⊔ T

source

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 : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} {y : A} (hx : x ∈ S) (hy : y ∈ T) :

x * y ∈ S ⊔ T

source

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

StarSubalgebra.map f (S ⊔ T) = StarSubalgebra.map f S ⊔ StarSubalgebra.map f T

source

@[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 : StarSubalgebra R A) (T : StarSubalgebra R A) :

↑(S ⊓ T) = ↑S ∩ ↑T

source

@[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 : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} :

x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

source

@[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 : StarSubalgebra R A) (T : StarSubalgebra R A) :

(S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

source

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

source

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

source

@[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 (StarSubalgebra.toSubalgebra '' S)

source

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

source

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

source

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

source

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 = ⊥

source

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)

source

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

source

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

source

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 { x : A // x ∈ StarAlgebra.adjoin R s } B] [AlgHomClass F R { x : A // x ∈ StarAlgebra.adjoin R s } B] [StarHomClass F { x : A // x ∈ StarAlgebra.adjoin R s } B] {f : F} {g : F} (h : ∀ (x : { x : A // x ∈ StarAlgebra.adjoin R s }), ↑x ∈ s → f x = g x) :

f = g

source

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 { x : A // x ∈ StarAlgebra.adjoin R {a} } B] [AlgHomClass F R { x : A // x ∈ StarAlgebra.adjoin R {a} } B] [StarHomClass F { x : A // x ∈ StarAlgebra.adjoin R {a} } B] {f : F} {g : F} (h : f ⟨a, ⋯⟩ = g ⟨a, ⋯⟩) :

f = g

source

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 : F) (g : F) :

StarSubalgebra R A

The equalizer of two star R-algebra homomorphisms.

Equations

StarAlgHom.equalizer f g = { toSubalgebra := AlgHom.equalizer ↑f ↑g, star_mem' := ⋯ }

source

@[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 : F) (g : F) (x : A) :

x ∈ StarAlgHom.equalizer f g ↔ f x = g x

source

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 : F) (g : F) {s : Set A} (h : Set.EqOn (⇑f) (⇑g) s) :

StarAlgebra.adjoin R s ≤ StarAlgHom.equalizer f g

source

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 : F⦄ ⦃g : F⦄ (hs : Set.EqOn (⇑f) (⇑g) s) :

f = g

source

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)

source

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.

Equations

φ.range = { toSubalgebra := φ.range, star_mem' := ⋯ }

source

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 φ ⊤

source

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] { x : B // x ∈ S }

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

Equations

f.codRestrict S hf = { toAlgHom := f.codRestrict S.toSubalgebra hf, map_star' := ⋯ }

source

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

source

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

source

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

source

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] { x : B // x ∈ f.range }

Restriction of the codomain of a StarAlgHom to its range.

Equations

f.rangeRestrict = f.codRestrict f.range ⋯

source

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

(StarAlgEquiv.ofInjective f hf) a = f.rangeRestrict a

source

@[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 : { x : B // x ∈ (↑f).range }), (StarAlgEquiv.ofInjective f hf).symm a = (AlgEquiv.ofInjective (↑f) hf).invFun a

source

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] { x : B // x ∈ f.range }

The StarAlgEquiv onto the range corresponding to an injective StarAlgHom.

Equations

One or more equations did not get rendered due to their size.

source

@[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), (StarAlgHom.restrictScalars R f) a = f a

source

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

Equations

StarAlgHom.restrictScalars R f = { toAlgHom := AlgHom.restrictScalars R f.toAlgHom, map_star' := ⋯ }

source

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 (StarAlgHom.restrictScalars R)

source

@[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), (StarAlgEquiv.restrictScalars R f).symm a = f.invFun a

source

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

(StarAlgEquiv.restrictScalars R f) a = f a

source

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

Equations

StarAlgEquiv.restrictScalars R f = { toFun := ⇑f, invFun := f.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }

source

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 (StarAlgEquiv.restrictScalars R)

Documentation

Mathlib.Algebra.Star.Subalgebra

Star subalgebras #

The star closure of a subalgebra #

The star subalgebra generated by a set #

Complete lattice structure #