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

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

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 { x // x ∈ 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.

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 { x // x ∈ 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.

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 { x // x ∈ 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.

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 { x // x ∈ 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.

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

{ x // x ∈ s } →⋆ₙₐ[R] A

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

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

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

A non-unital star subalgebra is a non-unital subalgebra which 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

source

instance NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star 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

source

instance NonUnitalStarSubalgebra.instStarMemClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star 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

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.

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.

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

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

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

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

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

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

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' { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ S }

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 { x // x ∈ S } { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ S } { x // x ∈ 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 { x // x ∈ 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 : { x // x ∈ S }) (y : { x // x ∈ 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 : { x // x ∈ S }) (y : { x // x ∈ 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 : { x // 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 : { x // x ∈ S }) (y : { x // x ∈ 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 : { x // 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 : { x // 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] [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.

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] [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] [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] [NonUnitalStarAlgHomClass F R A B] {S : NonUnitalStarSubalgebra R A} {f : F} {y : B} :

y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x, 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] [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] [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] [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.

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] [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] [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] [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] [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 { x // x ∈ 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 : A), x ∈ s → star x ∈ s) :

NonUnitalStarSubalgebra R A

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

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 : A), 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 : A), 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 : A), 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 : A), 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] [NonUnitalStarAlgHomClass F R A B] (φ : F) :

NonUnitalStarSubalgebra R B

Range of an NonUnitalAlgHom as a NonUnitalStarSubalgebra.

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] [NonUnitalStarAlgHomClass F R A B] (φ : F) {y : B} :

y ∈ NonUnitalStarAlgHom.range φ ↔ ∃ x, ↑φ 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] [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] [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] [NonUnitalStarAlgHomClass F R A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), ↑f x ∈ S) :

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

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

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] [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] [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] [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] [NonUnitalStarAlgHomClass F R A B] (f : F) :

A →⋆ₙₐ[R] { x // x ∈ 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.

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] [NonUnitalStarAlgHomClass F R A B] (ϕ : F) (ψ : F) :

NonUnitalStarSubalgebra R A

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

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] [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] [hF : NonUnitalStarAlgHomClass F R A B] {g : B → A} {f : F} (h : Function.LeftInverse g ↑f) :

A ≃⋆ₐ[R] { x // x ∈ 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.

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] [hF : 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] [hF : NonUnitalStarAlgHomClass F R A B] {g : B → A} {f : F} (h : Function.LeftInverse g ↑f) (x : { x // 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] [hF : NonUnitalStarAlgHomClass F R A B] (f : F) (hf : Function.Injective ↑f) :

A ≃⋆ₐ[R] { x // x ∈ NonUnitalStarAlgHom.range f }

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

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] [hF : 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.

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.

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.

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.

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)

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] [hF : 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 : NonUnitalStarSubalgebra R A) (_ : 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 : NonUnitalStarSubalgebra R A), 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)

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] [hF : 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] [hF : 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] [hF : 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] [hF : 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] { x // x ∈ ⊤ }

NonUnitalStarAlgHom to ⊤ : NonUnitalStarSubalgebra R A.

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)

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)

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

{ x // x ∈ S } →⋆ₙₐ[R] { x // x ∈ 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.ofLe, or NonUnitalSubalgebra.inclusion

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 { x // x ∈ 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 := h x hx }

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 : { x // 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 : { x // 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 : { x // x ∈ 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.

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.fst ∈ S ∧ x.snd ∈ 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 => 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 => x ≤ x_1) K) (f : (i : ι) → { x // x ∈ 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) :

{ x // x ∈ 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 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ 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 : { x // 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 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ 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 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ 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 : { x // 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 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ 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 : { x // 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.

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 { x // x ∈ NonUnitalStarSubalgebra.center R A }

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 { x // x ∈ NonUnitalStarSubalgebra.center R A }

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.

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