Non-unital Star Subalgebras #

In this file we define NonUnitalStarSubalgebras and the usual operations on them (map, comap).

TODO #

once we have scalar actions by semigroups (as opposed to monoids), implement the action of a non-unital subalgebra on the larger algebra.

instance StarMemClass.instInvolutiveStar {S : Type u_1} {R : Type u_2} [InvolutiveStar R] [SetLike S R] [StarMemClass S R] (s : S) :

InvolutiveStar ↥s

If a type carries an involutive star, then any star-closed subset does too.

Equations

StarMemClass.instInvolutiveStar s = InvolutiveStar.mk (_ : ∀ (r : ↥s), star (star r) = r)

source

instance StarMemClass.instStarMul {S : Type u_1} {R : Type u_2} [Mul R] [StarMul R] [SetLike S R] [MulMemClass S R] [StarMemClass S R] (s : S) :

StarMul ↥s

In a star magma (i.e., a multiplication with an antimultiplicative involutive star operation), any star-closed subset which is also closed under multiplication is itself a star magma.

Equations

StarMemClass.instStarMul s = StarMul.mk (_ : ∀ (x x_1 : ↥s), star (x * x_1) = star x_1 * star x)

source

instance StarMemClass.instStarAddMonoid {S : Type u_1} {R : Type u_2} [AddMonoid R] [StarAddMonoid R] [SetLike S R] [AddSubmonoidClass S R] [StarMemClass S R] (s : S) :

StarAddMonoid ↥s

In a StarAddMonoid (i.e., an additive monoid with an additive involutive star operation), any star-closed subset which is also closed under addition and contains zero is itself a StarAddMonoid.

Equations

StarMemClass.instStarAddMonoid s = StarAddMonoid.mk (_ : ∀ (x x_1 : ↥s), star (x + x_1) = star x + star x_1)

source

instance StarMemClass.instStarRing {S : Type u_1} {R : Type u_2} [NonUnitalNonAssocSemiring R] [StarRing R] [SetLike S R] [NonUnitalSubsemiringClass S R] [StarMemClass S R] (s : S) :

StarRing ↥s

In a star ring (i.e., a non-unital, non-associative, semiring with an additive, antimultiplicative, involutive star operation), a star-closed non-unital subsemiring is itself a star ring.

Equations

StarMemClass.instStarRing s = let src := StarMemClass.instStarMul s; let src_1 := StarMemClass.instStarAddMonoid s; StarRing.mk (_ : ∀ (r s_1 : ↥s), star (r + s_1) = star r + star s_1)

source

instance StarMemClass.instStarModule {S : Type u_1} (R : Type u_2) {M : Type u_3} [Star R] [Star M] [SMul R M] [StarModule R M] [SetLike S M] [SMulMemClass S R M] [StarMemClass S M] (s : S) :

StarModule R ↥s

In a star R-module (i.e., star (r • m) = (star r) • m) any star-closed subset which is also closed under the scalar action by R is itself a star R-module.

Equations

(_ : StarModule R ↥s) = (_ : StarModule R ↥s)

source

def NonUnitalStarSubalgebraClass.subtype {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Star A] [Module R A] {S : Type w''} [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] [StarMemClass S A] (s : S) :

↥s →⋆ₙₐ[R] A

Embedding of a non-unital star subalgebra into the non-unital star algebra.

Equations

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

Instances For

source

@[simp]

theorem NonUnitalStarSubalgebraClass.coeSubtype {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Star A] [Module R A] {S : Type w''} [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] [StarMemClass S A] (s : S) :

⇑(NonUnitalStarSubalgebraClass.subtype s) = Subtype.val

source

structure NonUnitalStarSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] extends NonUnitalSubalgebra :

Type v

A non-unital star subalgebra is a non-unital subalgebra which is closed under the star operation.

carrier : Set A
add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
zero_mem' : 0 ∈ self.carrier
mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
smul_mem' : ∀ (c : R) {x : A}, x ∈ self.carrier → c • x ∈ self.carrier
star_mem' : ∀ {a : A}, a ∈ self.carrier → star a ∈ self.carrier
The carrier of a NonUnitalStarSubalgebra is closed under the star operation.

Instances For

source

instance NonUnitalStarSubalgebra.instSetLike {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :

SetLike (NonUnitalStarSubalgebra R A) A

Equations

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

source

instance NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :

NonUnitalSubsemiringClass (NonUnitalStarSubalgebra R A) A

Equations

(_ : NonUnitalSubsemiringClass (NonUnitalStarSubalgebra R A) A) = (_ : NonUnitalSubsemiringClass (NonUnitalStarSubalgebra R A) A)

source

instance NonUnitalStarSubalgebra.instSMulMemClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :

SMulMemClass (NonUnitalStarSubalgebra R A) R A

Equations

(_ : SMulMemClass (NonUnitalStarSubalgebra R A) R A) = (_ : SMulMemClass (NonUnitalStarSubalgebra R A) R A)

source

instance NonUnitalStarSubalgebra.instStarMemClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :

StarMemClass (NonUnitalStarSubalgebra R A) A

Equations

(_ : StarMemClass (NonUnitalStarSubalgebra R A) A) = (_ : StarMemClass (NonUnitalStarSubalgebra R A) A)

source

instance NonUnitalStarSubalgebra.instNonUnitalSubringClass {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [Star A] :

NonUnitalSubringClass (NonUnitalStarSubalgebra R A) A

Equations

(_ : NonUnitalSubringClass (NonUnitalStarSubalgebra R A) A) = (_ : NonUnitalSubringClass (NonUnitalStarSubalgebra R A) A)

source

theorem NonUnitalStarSubalgebra.mem_carrier {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {s : NonUnitalStarSubalgebra R A} {x : A} :

x ∈ s.carrier ↔ x ∈ s

source

theorem NonUnitalStarSubalgebra.ext {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) :

S = T

source

@[simp]

theorem NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} {x : A} :

x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

↑S.toNonUnitalSubalgebra = ↑S

source

theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :

Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubalgebra

source

theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} {U : NonUnitalStarSubalgebra R A} :

S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U

source

theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {S₁ : NonUnitalStarSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} :

S₁.toNonUnitalSubalgebra ≤ S₂.toNonUnitalSubalgebra ↔ S₁ ≤ S₂

source

def NonUnitalStarSubalgebra.copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S) :

NonUnitalStarSubalgebra R A

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

Equations

NonUnitalStarSubalgebra.copy S s hs = let src := NonUnitalSubalgebra.copy S.toNonUnitalSubalgebra s hs; { toNonUnitalSubalgebra := src, star_mem' := (_ : ∀ x ∈ s, star x ∈ s) }

Instances For

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S) :

↑(NonUnitalStarSubalgebra.copy S s hs) = s

source

theorem NonUnitalStarSubalgebra.copy_eq {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S) :

NonUnitalStarSubalgebra.copy S s hs = S

source

def NonUnitalStarSubalgebra.toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalSubring A

A non-unital star subalgebra over a ring is also a Subring.

Equations

NonUnitalStarSubalgebra.toNonUnitalSubring S = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, neg_mem' := (_ : ∀ {x : A}, x ∈ S → -x ∈ S) }

Instances For

source

@[simp]

theorem NonUnitalStarSubalgebra.mem_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} {x : A} :

x ∈ NonUnitalStarSubalgebra.toNonUnitalSubring S ↔ x ∈ S

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

↑(NonUnitalStarSubalgebra.toNonUnitalSubring S) = ↑S

source

theorem NonUnitalStarSubalgebra.toNonUnitalSubring_injective {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] :

Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubring

source

theorem NonUnitalStarSubalgebra.toNonUnitalSubring_inj {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} {U : NonUnitalStarSubalgebra R A} :

NonUnitalStarSubalgebra.toNonUnitalSubring S = NonUnitalStarSubalgebra.toNonUnitalSubring U ↔ S = U

source

instance NonUnitalStarSubalgebra.instInhabited {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

Inhabited ↥S

Equations

NonUnitalStarSubalgebra.instInhabited S = { default := 0 }

NonUnitalStarSubalgebras inherit structure from their NonUnitalSubsemiringClass and NonUnitalSubringClass instances.

source

instance NonUnitalStarSubalgebra.toNonUnitalSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalSemiring ↥S

Equations

NonUnitalStarSubalgebra.toNonUnitalSemiring S = inferInstance

source

instance NonUnitalStarSubalgebra.toNonUnitalCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalCommSemiring ↥S

Equations

NonUnitalStarSubalgebra.toNonUnitalCommSemiring S = inferInstance

source

instance NonUnitalStarSubalgebra.toNonUnitalRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalRing ↥S

Equations

NonUnitalStarSubalgebra.toNonUnitalRing S = inferInstance

source

instance NonUnitalStarSubalgebra.toNonUnitalCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalCommRing A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalCommRing ↥S

Equations

NonUnitalStarSubalgebra.toNonUnitalCommRing S = inferInstance

source

def NonUnitalStarSubalgebra.toNonUnitalSubalgebra' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :

NonUnitalStarSubalgebra R A ↪o NonUnitalSubalgebra R A

The forgetful map from NonUnitalStarSubalgebra to NonUnitalSubalgebra as an OrderEmbedding

Equations

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

Instances For

NonUnitalStarSubalgebras inherit structure from their Submodule coercions.

source

instance NonUnitalStarSubalgebra.module' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :

Module R' ↥S

Equations

NonUnitalStarSubalgebra.module' S = SMulMemClass.toModule' (NonUnitalStarSubalgebra R A) R' R A S

source

instance NonUnitalStarSubalgebra.instModule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

Module R ↥S

Equations

NonUnitalStarSubalgebra.instModule S = NonUnitalStarSubalgebra.module' S

source

instance NonUnitalStarSubalgebra.instIsScalarTower' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :

IsScalarTower R' R ↥S

Equations

(_ : IsScalarTower R' R ↥S) = (_ : IsScalarTower R' R ↥S.toNonUnitalSubalgebra)

source

instance NonUnitalStarSubalgebra.instIsScalarTower {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [IsScalarTower R A A] :

IsScalarTower R ↥S ↥S

Equations

(_ : IsScalarTower R ↥S ↥S) = (_ : IsScalarTower R ↥S ↥S)

source

instance NonUnitalStarSubalgebra.instSMulCommClass' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SMulCommClass R' R A] :

SMulCommClass R' R ↥S

Equations

(_ : SMulCommClass R' R ↥S) = (_ : SMulCommClass R' R ↥S)

source

instance NonUnitalStarSubalgebra.instSMulCommClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [SMulCommClass R A A] :

SMulCommClass R ↥S ↥S

Equations

(_ : SMulCommClass R ↥S ↥S) = (_ : SMulCommClass R ↥S ↥S)

source

instance NonUnitalStarSubalgebra.noZeroSMulDivisors_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [NoZeroSMulDivisors R A] :

NoZeroSMulDivisors R ↥S

Equations

(_ : NoZeroSMulDivisors R ↥S) = (_ : NoZeroSMulDivisors R ↥S)

source

theorem NonUnitalStarSubalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) (x : ↥S) (y : ↥S) :

↑(x + y) = ↑x + ↑y

source

theorem NonUnitalStarSubalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) (x : ↥S) (y : ↥S) :

↑(x * y) = ↑x * ↑y

source

theorem NonUnitalStarSubalgebra.coe_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

↑0 = 0

source

theorem NonUnitalStarSubalgebra.coe_neg {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} (x : ↥S) :

↑(-x) = -↑x

source

theorem NonUnitalStarSubalgebra.coe_sub {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] {S : NonUnitalStarSubalgebra R A} (x : ↥S) (y : ↥S) :

↑(x - y) = ↑x - ↑y

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : ↥S) :

↑(r • x) = r • ↑x

source

theorem NonUnitalStarSubalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) {x : ↥S} :

↑x = 0 ↔ x = 0

source

@[simp]

theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalSubalgebraClass.subtype S = ↑(NonUnitalStarSubalgebraClass.subtype S)

source

@[simp]

theorem NonUnitalStarSubalgebra.toSubring_subtype {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalSubringClass.subtype S = ↑(NonUnitalStarSubalgebraClass.subtype S)

source

def NonUnitalStarSubalgebra.map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R A) :

NonUnitalStarSubalgebra R B

Transport a non-unital star subalgebra via a non-unital star algebra homomorphism.

Equations

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

Instances For

source

theorem NonUnitalStarSubalgebra.map_mono {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {S₁ : NonUnitalStarSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} {f : F} :

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

source

theorem NonUnitalStarSubalgebra.map_injective {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {f : F} (hf : Function.Injective ⇑f) :

Function.Injective (NonUnitalStarSubalgebra.map f)

source

@[simp]

theorem NonUnitalStarSubalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalStarSubalgebra.map (NonUnitalStarAlgHom.id R A) S = S

source

theorem NonUnitalStarSubalgebra.map_map {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [NonUnitalNonAssocSemiring C] [Module R C] [Star C] (S : NonUnitalStarSubalgebra R A) (g : B →⋆ₙₐ[R] C) (f : A →⋆ₙₐ[R] B) :

NonUnitalStarSubalgebra.map g (NonUnitalStarSubalgebra.map f S) = NonUnitalStarSubalgebra.map (NonUnitalStarAlgHom.comp g f) S

source

@[simp]

theorem NonUnitalStarSubalgebra.mem_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {S : NonUnitalStarSubalgebra R A} {f : F} {y : B} :

y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y

source

theorem NonUnitalStarSubalgebra.map_toNonUnitalSubalgebra {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {S : NonUnitalStarSubalgebra R A} {f : F} :

(NonUnitalStarSubalgebra.map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (S : NonUnitalStarSubalgebra R A) (f : F) :

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

source

def NonUnitalStarSubalgebra.comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R B) :

NonUnitalStarSubalgebra R A

Preimage of a non-unital star subalgebra under a non-unital star algebra homomorphism.

Equations

NonUnitalStarSubalgebra.comap f S = { toNonUnitalSubalgebra := NonUnitalSubalgebra.comap f S.toNonUnitalSubalgebra, star_mem' := (_ : ∀ (a : A), f a ∈ S → f (star a) ∈ S) }

Instances For

source

theorem NonUnitalStarSubalgebra.map_le {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {S : NonUnitalStarSubalgebra R A} {f : F} {U : NonUnitalStarSubalgebra R B} :

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

source

theorem NonUnitalStarSubalgebra.gc_map_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :

GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)

source

@[simp]

theorem NonUnitalStarSubalgebra.mem_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (S : NonUnitalStarSubalgebra R B) (f : F) (x : A) :

x ∈ NonUnitalStarSubalgebra.comap f S ↔ f x ∈ S

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (S : NonUnitalStarSubalgebra R B) (f : F) :

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

source

instance NonUnitalStarSubalgebra.instNoZeroDivisors {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NoZeroDivisors ↥S

Equations

(_ : NoZeroDivisors ↥S) = (_ : NoZeroDivisors ↥S)

source

def NonUnitalSubalgebra.toNonUnitalStarSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s) :

NonUnitalStarSubalgebra R A

A non-unital subalgebra closed under star is a non-unital star subalgebra.

Equations

NonUnitalSubalgebra.toNonUnitalStarSubalgebra s h_star = { toNonUnitalSubalgebra := s, star_mem' := h_star }

Instances For

source

@[simp]

theorem NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] {s : NonUnitalSubalgebra R A} {h_star : ∀ x ∈ s, star x ∈ s} {x : A} :

x ∈ NonUnitalSubalgebra.toNonUnitalStarSubalgebra s h_star ↔ x ∈ s

source

@[simp]

theorem NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s) :

↑(NonUnitalSubalgebra.toNonUnitalStarSubalgebra s h_star) = ↑s

source

@[simp]

theorem NonUnitalSubalgebra.toNonUnitalStarSubalgebra_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s) :

(NonUnitalSubalgebra.toNonUnitalStarSubalgebra s h_star).toNonUnitalSubalgebra = s

source

@[simp]

theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalSubalgebra.toNonUnitalStarSubalgebra S.toNonUnitalSubalgebra (_ : ∀ x ∈ S, star x ∈ S) = S

source

def NonUnitalStarAlgHom.range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (φ : F) :

NonUnitalStarSubalgebra R B

Range of an NonUnitalAlgHom as a NonUnitalStarSubalgebra.

Equations

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

Instances For

source

@[simp]

theorem NonUnitalStarAlgHom.mem_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (φ : F) {y : B} :

y ∈ NonUnitalStarAlgHom.range φ ↔ ∃ (x : A), φ x = y

source

theorem NonUnitalStarAlgHom.mem_range_self {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (φ : F) (x : A) :

φ x ∈ NonUnitalStarAlgHom.range φ

source

@[simp]

theorem NonUnitalStarAlgHom.coe_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (φ : F) :

↑(NonUnitalStarAlgHom.range φ) = Set.range ⇑φ

source

theorem NonUnitalStarAlgHom.range_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [NonUnitalNonAssocSemiring C] [Module R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] C) :

NonUnitalStarAlgHom.range (NonUnitalStarAlgHom.comp g f) = NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f)

source

theorem NonUnitalStarAlgHom.range_comp_le_range {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [NonUnitalNonAssocSemiring C] [Module R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] C) :

NonUnitalStarAlgHom.range (NonUnitalStarAlgHom.comp g f) ≤ NonUnitalStarAlgHom.range g

source

def NonUnitalStarAlgHom.codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) :

A →⋆ₙₐ[R] ↥S

Restrict the codomain of a non-unital star algebra homomorphism.

Equations

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

Instances For

source

@[simp]

theorem NonUnitalStarAlgHom.subtype_comp_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) :

NonUnitalStarAlgHom.comp (NonUnitalStarSubalgebraClass.subtype S) (NonUnitalStarAlgHom.codRestrict f S hf) = ↑f

source

@[simp]

theorem NonUnitalStarAlgHom.coe_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A) :

↑((NonUnitalStarAlgHom.codRestrict f S hf) x) = f x

source

theorem NonUnitalStarAlgHom.injective_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) :

Function.Injective ⇑(NonUnitalStarAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f

source

@[reducible]

def NonUnitalStarAlgHom.rangeRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :

A →⋆ₙₐ[R] ↥(NonUnitalStarAlgHom.range f)

Restrict the codomain of a non-unital star algebra homomorphism f to f.range.

This is the bundled version of Set.rangeFactorization.

Equations

NonUnitalStarAlgHom.rangeRestrict f = NonUnitalStarAlgHom.codRestrict f (NonUnitalStarAlgHom.range f) (_ : ∀ (x : A), f x ∈ NonUnitalStarAlgHom.range f)

Instances For

source

def NonUnitalStarAlgHom.equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (ϕ : F) (ψ : F) :

NonUnitalStarSubalgebra R A

The equalizer of two non-unital star R-algebra homomorphisms

Equations

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

Instances For

source

@[simp]

theorem NonUnitalStarAlgHom.mem_equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (φ : F) (ψ : F) (x : A) :

x ∈ NonUnitalStarAlgHom.equalizer φ ψ ↔ φ x = ψ x

source

def StarAlgEquiv.ofLeftInverse' {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) :

A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range f)

Restrict a non-unital star algebra homomorphism with a left inverse to an algebra isomorphism to its range.

This is a computable alternative to StarAlgEquiv.ofInjective.

Equations

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

Instances For

source

@[simp]

theorem StarAlgEquiv.ofLeftInverse'_apply {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) (x : A) :

↑((StarAlgEquiv.ofLeftInverse' h) x) = f x

source

@[simp]

theorem StarAlgEquiv.ofLeftInverse'_symm_apply {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) (x : ↥(NonUnitalStarAlgHom.range f)) :

(StarAlgEquiv.symm (StarAlgEquiv.ofLeftInverse' h)) x = g ↑x

source

noncomputable def StarAlgEquiv.ofInjective' {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (hf : Function.Injective ⇑f) :

A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range f)

Restrict an injective non-unital star algebra homomorphism to a star algebra isomorphism

Equations

StarAlgEquiv.ofInjective' f hf = StarAlgEquiv.ofLeftInverse' (_ : Function.LeftInverse (Classical.choose (_ : Function.HasLeftInverse ⇑f)) ⇑f)

Instances For

source

@[simp]

theorem StarAlgEquiv.ofInjective'_apply {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (hf : Function.Injective ⇑f) (x : A) :

↑((StarAlgEquiv.ofInjective' f hf) x) = f x

The star closure of a subalgebra #

source

instance NonUnitalSubalgebra.instInvolutiveStar {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] :

InvolutiveStar (NonUnitalSubalgebra R A)

The pointwise star of a non-unital subalgebra is a non-unital subalgebra.

Equations

NonUnitalSubalgebra.instInvolutiveStar = InvolutiveStar.mk (_ : ∀ (S : NonUnitalSubalgebra R A), star (star S) = S)

source

@[simp]

theorem NonUnitalSubalgebra.mem_star_iff {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] (S : NonUnitalSubalgebra R A) (x : A) :

x ∈ star S ↔ star x ∈ S

source

theorem NonUnitalSubalgebra.star_mem_star_iff {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] (S : NonUnitalSubalgebra R A) (x : A) :

star x ∈ star S ↔ x ∈ S

source

@[simp]

theorem NonUnitalSubalgebra.coe_star {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] (S : NonUnitalSubalgebra R A) :

↑(star S) = star ↑S

source

theorem NonUnitalSubalgebra.star_mono {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

Monotone star

source

theorem NonUnitalSubalgebra.star_adjoin_comm (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) :

star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s)

The star operation on NonUnitalSubalgebra commutes with NonUnitalAlgebra.adjoin.

source

@[simp]

theorem NonUnitalSubalgebra.starClosure_carrier {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : NonUnitalSubalgebra R A) :

↑(NonUnitalSubalgebra.starClosure S) = ⋂ (s : Submodule R A), ⋂ (_ : ↑(NonUnitalSubsemiring.closure (↑S ∪ star ↑S)) ⊆ ↑s), ↑s

source

def NonUnitalSubalgebra.starClosure {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : NonUnitalSubalgebra R A) :

NonUnitalStarSubalgebra R A

The NonUnitalStarSubalgebra obtained from S : NonUnitalSubalgebra R A by taking the smallest non-unital subalgebra containing both S and star S.

Equations

NonUnitalSubalgebra.starClosure S = { toNonUnitalSubalgebra := S ⊔ star S, star_mem' := (_ : ∀ a ∈ S ⊔ star S, star a ∈ S ⊔ star S) }

Instances For

source

theorem NonUnitalSubalgebra.starClosure_le {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} (h : S₁ ≤ S₂.toNonUnitalSubalgebra) :

NonUnitalSubalgebra.starClosure S₁ ≤ S₂

source

theorem NonUnitalSubalgebra.starClosure_le_iff {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} :

NonUnitalSubalgebra.starClosure S₁ ≤ S₂ ↔ S₁ ≤ S₂.toNonUnitalSubalgebra

source

@[simp]

theorem NonUnitalSubalgebra.starClosure_toNonunitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalSubalgebra R A} :

(NonUnitalSubalgebra.starClosure S).toNonUnitalSubalgebra = S ⊔ star S

source

theorem NonUnitalSubalgebra.starClosure_mono {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

Monotone NonUnitalSubalgebra.starClosure

source

def NonUnitalStarAlgebra.adjoin (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) :

NonUnitalStarSubalgebra R A

The minimal non-unital subalgebra that includes s.

Equations

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

Instances For

source

theorem NonUnitalStarAlgebra.adjoin_eq_starClosure_adjoin (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) :

NonUnitalStarAlgebra.adjoin R s = NonUnitalSubalgebra.starClosure (NonUnitalAlgebra.adjoin R s)

source

theorem NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) :

(NonUnitalStarAlgebra.adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s)

source

theorem NonUnitalStarAlgebra.subset_adjoin (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) :

s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)

source

theorem NonUnitalStarAlgebra.star_subset_adjoin (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) :

star s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)

source

theorem NonUnitalStarAlgebra.self_mem_adjoin_singleton (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (x : A) :

x ∈ NonUnitalStarAlgebra.adjoin R {x}

source

theorem NonUnitalStarAlgebra.star_self_mem_adjoin_singleton (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (x : A) :

star x ∈ NonUnitalStarAlgebra.adjoin R {x}

source

theorem NonUnitalStarAlgebra.gc {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

GaloisConnection (NonUnitalStarAlgebra.adjoin R) SetLike.coe

source

def NonUnitalStarAlgebra.gi {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

GaloisInsertion (NonUnitalStarAlgebra.adjoin R) SetLike.coe

Galois insertion between adjoin and Subtype.val.

Equations

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

Instances For

source

theorem NonUnitalStarAlgebra.adjoin_le {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {s : Set A} (hs : s ⊆ ↑S) :

NonUnitalStarAlgebra.adjoin R s ≤ S

source

theorem NonUnitalStarAlgebra.adjoin_le_iff {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {s : Set A} :

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

source

theorem NonUnitalSubalgebra.starClosure_eq_adjoin {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : NonUnitalSubalgebra R A) :

NonUnitalSubalgebra.starClosure S = NonUnitalStarAlgebra.adjoin R ↑S

source

instance NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebraToNonUnitalNonAssocSemiringToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarAddMonoid {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

CompleteLattice (NonUnitalStarSubalgebra R A)

Equations

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

source

@[simp]

theorem NonUnitalStarAlgebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

↑⊤ = Set.univ

source

@[simp]

theorem NonUnitalStarAlgebra.mem_top {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {x : A} :

x ∈ ⊤

source

@[simp]

theorem NonUnitalStarAlgebra.top_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

⊤.toNonUnitalSubalgebra = ⊤

source

@[simp]

theorem NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} :

S.toNonUnitalSubalgebra = ⊤ ↔ S = ⊤

source

theorem NonUnitalStarAlgebra.mem_sup_left {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {x : A} :

x ∈ S → x ∈ S ⊔ T

source

theorem NonUnitalStarAlgebra.mem_sup_right {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {x : A} :

x ∈ T → x ∈ S ⊔ T

source

theorem NonUnitalStarAlgebra.mul_mem_sup {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {x : A} {y : A} (hx : x ∈ S) (hy : y ∈ T) :

x * y ∈ S ⊔ T

source

theorem NonUnitalStarAlgebra.map_sup {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R A) (T : NonUnitalStarSubalgebra R A) :

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

source

@[simp]

theorem NonUnitalStarAlgebra.coe_inf {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : NonUnitalStarSubalgebra R A) (T : NonUnitalStarSubalgebra R A) :

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

source

@[simp]

theorem NonUnitalStarAlgebra.mem_inf {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {x : A} :

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

source

@[simp]

theorem NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : NonUnitalStarSubalgebra R A) (T : NonUnitalStarSubalgebra R A) :

(S ⊓ T).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra ⊓ T.toNonUnitalSubalgebra

source

@[simp]

theorem NonUnitalStarAlgebra.coe_sInf {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)) :

↑(sInf S) = ⋂ s ∈ S, ↑s

source

theorem NonUnitalStarAlgebra.mem_sInf {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : Set (NonUnitalStarSubalgebra R A)} {x : A} :

x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

source

@[simp]

theorem NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)) :

(sInf S).toNonUnitalSubalgebra = sInf (NonUnitalStarSubalgebra.toNonUnitalSubalgebra '' S)

source

@[simp]

theorem NonUnitalStarAlgebra.coe_iInf {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} {S : ι → NonUnitalStarSubalgebra R A} :

↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

source

theorem NonUnitalStarAlgebra.mem_iInf {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} {S : ι → NonUnitalStarSubalgebra R A} {x : A} :

x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

source

@[simp]

theorem NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} (S : ι → NonUnitalStarSubalgebra R A) :

(⨅ (i : ι), S i).toNonUnitalSubalgebra = ⨅ (i : ι), (S i).toNonUnitalSubalgebra

source

instance NonUnitalStarAlgebra.instInhabitedNonUnitalStarSubalgebraToNonUnitalNonAssocSemiringToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarAddMonoid {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

Inhabited (NonUnitalStarSubalgebra R A)

Equations

NonUnitalStarAlgebra.instInhabitedNonUnitalStarSubalgebraToNonUnitalNonAssocSemiringToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarAddMonoid = { default := ⊥ }

source

theorem NonUnitalStarAlgebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {x : A} :

x ∈ ⊥ ↔ x = 0

source

theorem NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

⊥.toNonUnitalSubalgebra = ⊥

source

@[simp]

theorem NonUnitalStarAlgebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

↑⊥ = {0}

source

theorem NonUnitalStarAlgebra.eq_top_iff {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} :

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

source

theorem NonUnitalStarAlgebra.range_top_iff_surjective {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :

NonUnitalStarAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f

source

@[simp]

theorem NonUnitalStarAlgebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

NonUnitalStarAlgHom.range (NonUnitalStarAlgHom.id R A) = ⊤

source

@[simp]

theorem NonUnitalStarAlgebra.map_top {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :

NonUnitalStarSubalgebra.map f ⊤ = NonUnitalStarAlgHom.range f

source

@[simp]

theorem NonUnitalStarAlgebra.map_bot {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :

NonUnitalStarSubalgebra.map f ⊥ = ⊥

source

@[simp]

theorem NonUnitalStarAlgebra.comap_top {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :

NonUnitalStarSubalgebra.comap f ⊤ = ⊤

source

def NonUnitalStarAlgebra.toTop {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

A →⋆ₙₐ[R] ↥⊤

NonUnitalStarAlgHom to ⊤ : NonUnitalStarSubalgebra R A.

Equations

NonUnitalStarAlgebra.toTop = NonUnitalStarAlgHom.codRestrict (NonUnitalStarAlgHom.id R A) ⊤ (_ : ∀ (x : A), (NonUnitalStarAlgHom.id R A) x ∈ ⊤)

Instances For

source

instance NonUnitalStarSubalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [Subsingleton A] :

Subsingleton (NonUnitalStarSubalgebra R A)

Equations

(_ : Subsingleton (NonUnitalStarSubalgebra R A)) = (_ : Subsingleton (NonUnitalStarSubalgebra R A))

source

instance NonUnitalStarAlgHom.subsingleton {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [Subsingleton (NonUnitalStarSubalgebra R A)] :

Subsingleton (A →⋆ₙₐ[R] B)

Equations

(_ : Subsingleton (A →⋆ₙₐ[R] B)) = (_ : Subsingleton (A →⋆ₙₐ[R] B))

source

theorem NonUnitalStarSubalgebra.range_val {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] (S : NonUnitalStarSubalgebra R A) :

NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype S) = S

source

def NonUnitalStarSubalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} (h : S ≤ T) :

↥S →⋆ₙₐ[R] ↥T

The map S → T when S is a non-unital star subalgebra contained in the non-unital star algebra T.

This is the non-unital star subalgebra version of Submodule.inclusion, or NonUnitalSubalgebra.inclusion

Equations

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

Instances For

source

theorem NonUnitalStarSubalgebra.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} (h : S ≤ T) :

Function.Injective ⇑(NonUnitalStarSubalgebra.inclusion h)

source

@[simp]

theorem NonUnitalStarSubalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} :

↑(NonUnitalStarSubalgebra.inclusion (_ : S ≤ S)) = NonUnitalAlgHom.id R ↥S

source

@[simp]

theorem NonUnitalStarSubalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) :

(NonUnitalStarSubalgebra.inclusion h) { val := x, property := hx } = { val := x, property := (_ : x ∈ T) }

source

theorem NonUnitalStarSubalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S) :

(NonUnitalStarSubalgebra.inclusion h) { val := ↑x, property := m } = x

source

@[simp]

theorem NonUnitalStarSubalgebra.inclusion_inclusion {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {U : NonUnitalStarSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S) :

(NonUnitalStarSubalgebra.inclusion htu) ((NonUnitalStarSubalgebra.inclusion hst) x) = (NonUnitalStarSubalgebra.inclusion (_ : S ≤ U)) x

source

@[simp]

theorem NonUnitalStarSubalgebra.val_inclusion {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (s : ↥S) :

↑((NonUnitalStarSubalgebra.inclusion h) s) = ↑s

source

def NonUnitalStarSubalgebra.prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B) :

NonUnitalStarSubalgebra R (A × B)

The product of two non-unital star subalgebras is a non-unital star subalgebra.

Equations

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

Instances For

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B) :

↑(NonUnitalStarSubalgebra.prod S S₁) = ↑S ×ˢ ↑S₁

source

theorem NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B) :

(NonUnitalStarSubalgebra.prod S S₁).toNonUnitalSubalgebra = NonUnitalSubalgebra.prod S.toNonUnitalSubalgebra S₁.toNonUnitalSubalgebra

source

@[simp]

theorem NonUnitalStarSubalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {S : NonUnitalStarSubalgebra R A} {S₁ : NonUnitalStarSubalgebra R B} {x : A × B} :

x ∈ NonUnitalStarSubalgebra.prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

source

@[simp]

theorem NonUnitalStarSubalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] :

NonUnitalStarSubalgebra.prod ⊤ ⊤ = ⊤

source

theorem NonUnitalStarSubalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {S₁ : NonUnitalStarSubalgebra R B} {T₁ : NonUnitalStarSubalgebra R B} :

S ≤ T → S₁ ≤ T₁ → NonUnitalStarSubalgebra.prod S S₁ ≤ NonUnitalStarSubalgebra.prod T T₁

source

@[simp]

theorem NonUnitalStarSubalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] {S : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {S₁ : NonUnitalStarSubalgebra R B} {T₁ : NonUnitalStarSubalgebra R B} :

NonUnitalStarSubalgebra.prod S S₁ ⊓ NonUnitalStarSubalgebra.prod T T₁ = NonUnitalStarSubalgebra.prod (S ⊓ T) (S₁ ⊓ T₁)

source

theorem NonUnitalStarSubalgebra.coe_iSup_of_directed {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Type u_1} [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A} (dir : Directed (fun (x x_1 : NonUnitalStarSubalgebra R A) => x ≤ x_1) S) :

↑(iSup S) = ⋃ (i : ι), ↑(S i)

source

noncomputable def NonUnitalStarSubalgebra.iSupLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {ι : Type u_1} [Nonempty ι] (K : ι → NonUnitalStarSubalgebra R A) (dir : Directed (fun (x x_1 : NonUnitalStarSubalgebra R A) => x ≤ x_1) K) (f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalStarAlgHom.comp (f j) (NonUnitalStarSubalgebra.inclusion h)) (T : NonUnitalStarSubalgebra R A) (hT : T = iSup K) :

↥T →⋆ₙₐ[R] B

Define a non-unital star algebra homomorphism on a directed supremum of non-unital star subalgebras by defining it on each non-unital star subalgebra, and proving that it agrees on the intersection of non-unital star subalgebras.

Instances For

source

@[simp]

theorem NonUnitalStarSubalgebra.iSupLift_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalStarSubalgebra R A) => x ≤ x_1) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalStarAlgHom.comp (f j) (NonUnitalStarSubalgebra.inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (h : K i ≤ T) :

(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalStarSubalgebra.inclusion h) x) = (f i) x

source

@[simp]

theorem NonUnitalStarSubalgebra.iSupLift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalStarSubalgebra R A) => x ≤ x_1) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalStarAlgHom.comp (f j) (NonUnitalStarSubalgebra.inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) :

NonUnitalStarAlgHom.comp (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) (NonUnitalStarSubalgebra.inclusion h) = f i

source

@[simp]

theorem NonUnitalStarSubalgebra.iSupLift_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalStarSubalgebra R A) => x ≤ x_1) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalStarAlgHom.comp (f j) (NonUnitalStarSubalgebra.inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T) :

(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) { val := ↑x, property := hx } = (f i) x

source

theorem NonUnitalStarSubalgebra.iSupLift_of_mem {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalStarSubalgebra R A) => x ≤ x_1) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalStarAlgHom.comp (f j) (NonUnitalStarSubalgebra.inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i) :

(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) x = (f i) { val := ↑x, property := hx }

source

def NonUnitalStarSubalgebra.center (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :

NonUnitalStarSubalgebra R A

The center of a non-unital star algebra is the set of elements which commute with every element. They form a non-unital star subalgebra.

Equations

NonUnitalStarSubalgebra.center R A = { toNonUnitalSubalgebra := NonUnitalSubalgebra.center R A, star_mem' := (_ : ∀ {a : A}, a ∈ Set.center A → star a ∈ Set.center A) }

Instances For

source

theorem NonUnitalStarSubalgebra.coe_center (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :

↑(NonUnitalStarSubalgebra.center R A) = Set.center A

source

@[simp]

theorem NonUnitalStarSubalgebra.center_toNonUnitalSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :

(NonUnitalStarSubalgebra.center R A).toNonUnitalSubalgebra = NonUnitalSubalgebra.center R A

source

@[simp]

theorem NonUnitalStarSubalgebra.center_eq_top (R : Type u) [CommSemiring R] [StarRing R] (A : Type u_1) [NonUnitalCommSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] :

NonUnitalStarSubalgebra.center R A = ⊤

source

instance NonUnitalStarSubalgebra.instNonUnitalCommSemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :

NonUnitalCommSemiring ↥(NonUnitalStarSubalgebra.center R A)

Equations

NonUnitalStarSubalgebra.instNonUnitalCommSemiring = NonUnitalSubalgebra.center.instNonUnitalCommSemiring

source

instance NonUnitalStarSubalgebra.instNonUnitalCommRing {R : Type u} [CommSemiring R] {A : Type u_1} [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :

NonUnitalCommRing ↥(NonUnitalStarSubalgebra.center R A)

Equations

NonUnitalStarSubalgebra.instNonUnitalCommRing = NonUnitalSubalgebra.center.instNonUnitalCommRing

source

theorem NonUnitalStarSubalgebra.mem_center_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} :

a ∈ NonUnitalStarSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b

source

def NonUnitalStarSubalgebra.centralizer (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) :

NonUnitalStarSubalgebra R A

The centralizer of the star-closure of a set as a non-unital star subalgebra.

Equations

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

Instances For

source

@[simp]

theorem NonUnitalStarSubalgebra.coe_centralizer (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) :

↑(NonUnitalStarSubalgebra.centralizer R s) = Set.centralizer (s ∪ star s)

source

theorem NonUnitalStarSubalgebra.mem_centralizer_iff (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {z : A} :

z ∈ NonUnitalStarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

source

theorem NonUnitalStarSubalgebra.centralizer_le (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) (t : Set A) (h : s ⊆ t) :

NonUnitalStarSubalgebra.centralizer R t ≤ NonUnitalStarSubalgebra.centralizer R s

source

@[simp]

theorem NonUnitalStarSubalgebra.centralizer_univ (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :

NonUnitalStarSubalgebra.centralizer R Set.univ = NonUnitalStarSubalgebra.center R A

Documentation

Mathlib.Algebra.Star.NonUnitalSubalgebra

Non-unital Star Subalgebras #

TODO #

The star closure of a subalgebra #