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 ⋯

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 ⋯

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 ⋯

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 = StarRing.mk ⋯

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.

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

• NonUnitalStarSubalgebraClass.subtype s = { toFun := Subtype.val, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

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

structure NonUnitalStarSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] extends NonUnitalSubalgebra R A : 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} (_ha : a ∈ self.carrier) : star a ∈ self.carrier

  The carrier of a NonUnitalStarSubalgebra is closed under the star operation.

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

Equations

• NonUnitalStarSubalgebra.instSetLike = { coe := fun {s : NonUnitalStarSubalgebra R A} => s.carrier, coe_injective' := ⋯ }

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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) : ↑(S.copy s hs) = s

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) : S.copy s hs = S

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

• S.toNonUnitalSubring = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, neg_mem' := ⋯ }

@[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 ∈ S.toNonUnitalSubring ↔ x ∈ S

@[simp]

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

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

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

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

• S.instInhabited = { default := 0 }

NonUnitalStarSubalgebras inherit structure from their NonUnitalSubsemiringClass and NonUnitalSubringClass instances.

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

• S.toNonUnitalSemiring = inferInstance

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

• S.toNonUnitalCommSemiring = inferInstance

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

• S.toNonUnitalRing = inferInstance

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

• S.toNonUnitalCommRing = inferInstance

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

• NonUnitalStarSubalgebra.toNonUnitalSubalgebra' = { toFun := fun (S : NonUnitalStarSubalgebra R A) => S.toNonUnitalSubalgebra, inj' := ⋯, map_rel_iff' := ⋯ }

NonUnitalStarSubalgebras inherit structure from their Submodule coercions.

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

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

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

• S.instModule = S.module'

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

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

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

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

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

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

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

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

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

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

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

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

@[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 = NonUnitalAlgHomClass.toNonUnitalAlgHom (NonUnitalStarSubalgebraClass.subtype S)

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

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] [StarHomClass F 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

• NonUnitalStarSubalgebra.map f S = { toNonUnitalSubalgebra := NonUnitalSubalgebra.map (NonUnitalAlgHomClass.toNonUnitalAlgHom f) S.toNonUnitalSubalgebra, star_mem' := ⋯ }

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] [StarHomClass F A B] {S₁ S₂ : NonUnitalStarSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalStarSubalgebra.map f S₁ ≤ NonUnitalStarSubalgebra.map f S₂

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] [StarHomClass F A B] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (NonUnitalStarSubalgebra.map f)

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

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 (g.comp f) S

@[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] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} {y : B} : y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y

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] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} : (NonUnitalStarSubalgebra.map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra

@[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] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R A) (f : F) : ↑(NonUnitalStarSubalgebra.map f S) = ⇑f '' ↑S

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] [StarHomClass F 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' := ⋯ }

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] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} {U : NonUnitalStarSubalgebra R B} : NonUnitalStarSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalStarSubalgebra.comap f U

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] [StarHomClass F A B] (f : F) : GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)

@[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] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R B) (f : F) (x : A) : x ∈ NonUnitalStarSubalgebra.comap f S ↔ f x ∈ S

@[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] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R B) (f : F) : ↑(NonUnitalStarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S

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

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

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

@[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 ∈ s.toNonUnitalStarSubalgebra h_star ↔ x ∈ s

@[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) : ↑(s.toNonUnitalStarSubalgebra h_star) = ↑s

@[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) : (s.toNonUnitalStarSubalgebra h_star).toNonUnitalSubalgebra = s

@[simp]

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

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

Range of an NonUnitalAlgHom as a NonUnitalStarSubalgebra.

Equations

• NonUnitalStarAlgHom.range φ = { toNonUnitalSubalgebra := NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ), star_mem' := ⋯ }

@[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] [StarHomClass F A B] (φ : F) {y : B} : y ∈ NonUnitalStarAlgHom.range φ ↔ ∃ (x : A), φ x = y

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] [StarHomClass F A B] (φ : F) (x : A) : φ x ∈ NonUnitalStarAlgHom.range φ

@[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] [StarHomClass F A B] (φ : F) : ↑(NonUnitalStarAlgHom.range φ) = Set.range ⇑φ

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 (g.comp f) = NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f)

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 (g.comp f) ≤ NonUnitalStarAlgHom.range g

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] [StarHomClass F 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

• NonUnitalStarAlgHom.codRestrict f S hf = { toNonUnitalAlgHom := NonUnitalAlgHom.codRestrict f S.toNonUnitalSubalgebra hf, map_star' := ⋯ }

@[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] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : (NonUnitalStarSubalgebraClass.subtype S).comp (NonUnitalStarAlgHom.codRestrict f S hf) = ↑f

@[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] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A) : ↑((NonUnitalStarAlgHom.codRestrict f S hf) x) = f x

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] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : Function.Injective ⇑(NonUnitalStarAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f

@[reducible, inline]

abbrev 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] [StarHomClass F 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) ⋯

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

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

Equations

• NonUnitalStarAlgHom.equalizer ϕ ψ = { toNonUnitalSubalgebra := NonUnitalAlgHom.equalizer ϕ ψ, star_mem' := ⋯ }

@[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] [StarHomClass F A B] (φ ψ : F) (x : A) : x ∈ NonUnitalStarAlgHom.equalizer φ ψ ↔ φ x = ψ x

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] [StarHomClass F 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.

@[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] [StarHomClass F A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) (x : A) : ↑((StarAlgEquiv.ofLeftInverse' h) x) = f x

@[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] [StarHomClass F A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) (x : ↥(NonUnitalStarAlgHom.range f)) : (StarAlgEquiv.ofLeftInverse' h).symm x = g ↑x

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] [StarHomClass F 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' ⋯

@[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] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) (x : A) : ↑((StarAlgEquiv.ofInjective' f hf) x) = f x

The star closure of a subalgebra

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 ⋯

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

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

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

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

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

The star operation on NonUnitalSubalgebra commutes with NonUnitalAlgebra.adjoin.

def NonUnitalSubalgebra.starClosure {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A 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

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

@[simp]

theorem NonUnitalSubalgebra.starClosure_carrier {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) : ↑S.starClosure = ⋂ (s : Submodule R A), ⋂ (_ : ↑(NonUnitalSubsemiring.closure (↑S ∪ star ↑S)) ⊆ ↑s), ↑s

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

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

@[simp]

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

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

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

• NonUnitalStarAlgebra.adjoin R s = { toNonUnitalSubalgebra := NonUnitalAlgebra.adjoin R (s ∪ star s), star_mem' := ⋯ }

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 = (NonUnitalAlgebra.adjoin R s).starClosure

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)

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)

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)

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}

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}

theorem NonUnitalStarAlgebra.adjoin_induction (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} {p : (x : A) → x ∈ NonUnitalStarAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (r • x) ⋯) (star : ∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (star x) ⋯) {a : A} (ha : a ∈ NonUnitalStarAlgebra.adjoin R s) : p a ha

@[deprecated NonUnitalStarAlgebra.adjoin_induction (since := "2024-10-10")]

theorem NonUnitalStarAlgebra.adjoin_induction' (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} {p : (x : A) → x ∈ NonUnitalStarAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (r • x) ⋯) (star : ∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (star x) ⋯) {a : A} (ha : a ∈ NonUnitalStarAlgebra.adjoin R s) : p a ha

Alias of NonUnitalStarAlgebra.adjoin_induction.

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

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.

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

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

theorem NonUnitalStarAlgebra.adjoin_eq {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) : NonUnitalStarAlgebra.adjoin R ↑s = s

theorem NonUnitalStarAlgebra.adjoin_eq_span {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).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))

@[simp]

theorem NonUnitalStarAlgebra.span_eq_toSubmodule {A : Type v} [NonUnitalSemiring A] [StarRing A] {R : Type u_1} [CommSemiring R] [Module R A] (s : NonUnitalStarSubalgebra R A) : Submodule.span R ↑s = s.toSubmodule

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) : S.starClosure = NonUnitalStarAlgebra.adjoin R ↑S

instance NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra {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

• NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra = NonUnitalStarAlgebra.gi.liftCompleteLattice

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

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

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

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

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 T : NonUnitalStarSubalgebra R A} {x : A} : x ∈ S → x ∈ S ⊔ T

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 T : NonUnitalStarSubalgebra R A} {x : A} : x ∈ T → x ∈ S ⊔ T

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

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] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (S T : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (S ⊔ T) = NonUnitalStarSubalgebra.map f S ⊔ NonUnitalStarSubalgebra.map f T

theorem NonUnitalStarAlgebra.map_inf {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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (hf : Function.Injective ⇑f) (S T : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (S ⊓ T) = NonUnitalStarSubalgebra.map f S ⊓ NonUnitalStarSubalgebra.map f T

@[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 T : NonUnitalStarSubalgebra R A) : ↑(S ⊓ T) = ↑S ∩ ↑T

@[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 T : NonUnitalStarSubalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

@[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 T : NonUnitalStarSubalgebra R A) : (S ⊓ T).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra ⊓ T.toNonUnitalSubalgebra

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

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

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

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

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

theorem NonUnitalStarAlgebra.map_iInf {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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (hf : Function.Injective ⇑f) (S : ι → NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (⨅ (i : ι), S i) = ⨅ (i : ι), NonUnitalStarSubalgebra.map f (S i)

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

instance NonUnitalStarAlgebra.instInhabitedNonUnitalStarSubalgebra {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.instInhabitedNonUnitalStarSubalgebra = { default := ⊥ }

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

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

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

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

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

@[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] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarSubalgebra.map f ⊥ = ⊥

@[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] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarSubalgebra.comap f ⊤ = ⊤

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) ⊤ ⋯

theorem NonUnitalStarAlgebra.range_eq_top {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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f

@[deprecated NonUnitalStarAlgebra.range_eq_top (since := "2024-11-11")]

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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f

Alias of NonUnitalStarAlgebra.range_eq_top.

@[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] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (f : F) : NonUnitalStarSubalgebra.map f ⊤ = NonUnitalStarAlgHom.range f

theorem NonUnitalStarAlgHom.map_adjoin {F : Type v'} {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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (s : Set A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R s) = NonUnitalStarAlgebra.adjoin R (⇑f '' s)

@[simp]

theorem NonUnitalStarAlgHom.map_adjoin_singleton {F : Type v'} {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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (x : A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R {x}) = NonUnitalStarAlgebra.adjoin R {f x}

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)

instance NonUnitalStarAlgHom.subsingleton {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] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Subsingleton (NonUnitalStarSubalgebra R A)] : Subsingleton (A →⋆ₙₐ[R] B)

def NonUnitalStarSubalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S 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

• NonUnitalStarSubalgebra.inclusion h = { toNonUnitalAlgHom := NonUnitalSubalgebra.inclusion h, map_star' := ⋯ }

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

@[simp]

theorem NonUnitalStarSubalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} : NonUnitalAlgHomClass.toNonUnitalAlgHom (NonUnitalStarSubalgebra.inclusion ⋯) = NonUnitalAlgHom.id R ↥S

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

• S.prod S₁ = { carrier := ↑S ×ˢ ↑S₁, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯, star_mem' := ⋯ }

@[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) : ↑(S.prod S₁) = ↑S ×ˢ ↑S₁

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) : (S.prod S₁).toNonUnitalSubalgebra = S.prod S₁.toNonUnitalSubalgebra

@[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 ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

@[simp]

theorem NonUnitalStarSubalgebra.prod_top {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] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] : ⊤.prod ⊤ = ⊤

theorem NonUnitalStarSubalgebra.prod_mono {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] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] {S T : NonUnitalStarSubalgebra R A} {S₁ T₁ : NonUnitalStarSubalgebra R B} : S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

@[simp]

theorem NonUnitalStarSubalgebra.prod_inf_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] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] {S T : NonUnitalStarSubalgebra R A} {S₁ T₁ : NonUnitalStarSubalgebra R B} : S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

theorem NonUnitalStarSubalgebra.coe_iSup_of_directed {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A} (dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) => x1 ≤ x2) S) : ↑(iSup S) = ⋃ (i : ι), ↑(S i)

noncomputable def NonUnitalStarSubalgebra.iSupLift {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] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] (K : ι → NonUnitalStarSubalgebra R A) (dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) => x1 ≤ x2) K) (f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (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.

Equations

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

@[simp]

theorem NonUnitalStarSubalgebra.iSupLift_inclusion {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] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (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

@[simp]

theorem NonUnitalStarSubalgebra.iSupLift_comp_inclusion {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] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) : (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalStarSubalgebra.inclusion h) = f i

@[simp]

theorem NonUnitalStarSubalgebra.iSupLift_mk {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] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (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) ⟨↑x, hx⟩ = (f i) x

theorem NonUnitalStarSubalgebra.iSupLift_of_mem {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] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (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) ⟨↑x, hx⟩

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' := ⋯ }

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

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

@[simp]

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

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

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

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

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

• NonUnitalStarSubalgebra.centralizer R s = { toNonUnitalSubalgebra := NonUnitalSubalgebra.centralizer R (s ∪ star s), star_mem' := ⋯ }

@[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) = (s ∪ star s).centralizer

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

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

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

theorem NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra (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).toNonUnitalSubalgebra = NonUnitalSubalgebra.centralizer R (s ∪ star s)

theorem NonUnitalStarSubalgebra.coe_centralizer_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 ↑(NonUnitalStarSubalgebra.centralizer R s)) = (s ∪ star s).centralizer.centralizer

theorem NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer (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 ≤ NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)

theorem NonUnitalStarAlgebra.commute_of_mem_adjoin_of_forall_mem_commute {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 b : A} {s : Set A} (hb : b ∈ NonUnitalStarAlgebra.adjoin R s) (h : ∀ b ∈ s, Commute a b) (h_star : ∀ b ∈ s, Commute a (star b)) : Commute a b

theorem NonUnitalStarAlgebra.commute_of_mem_adjoin_singleton_of_commute {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 b c : A} (hc : c ∈ NonUnitalStarAlgebra.adjoin R {b}) (h : Commute a b) (h_star : Commute a (star b)) : Commute a c

theorem NonUnitalStarAlgebra.commute_of_mem_adjoin_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] {a b : A} [IsStarNormal a] (hb : b ∈ NonUnitalStarAlgebra.adjoin R {a}) : Commute a b

@[reducible, inline]

abbrev NonUnitalStarAlgebra.adjoinNonUnitalCommSemiringOfComm (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} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : NonUnitalCommSemiring ↥(NonUnitalStarAlgebra.adjoin R s)

If all elements of s : Set A commute pairwise and with elements of star s, then adjoin R s is a non-unital commutative semiring.

See note [reducible non-instances].

Equations

• NonUnitalStarAlgebra.adjoinNonUnitalCommSemiringOfComm R hcomm hcomm_star = NonUnitalCommSemiring.mk ⋯

@[reducible, inline]

abbrev NonUnitalStarAlgebra.adjoinNonUnitalCommRingOfComm (R : Type u_1) {A : Type u_2} [CommRing R] [StarRing R] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : NonUnitalCommRing ↥(NonUnitalStarAlgebra.adjoin R s)

If all elements of s : Set A commute pairwise and with elements of star s, then adjoin R s is a non-unital commutative ring.

See note [reducible non-instances].

Equations

• NonUnitalStarAlgebra.adjoinNonUnitalCommRingOfComm R hcomm hcomm_star = NonUnitalCommRing.mk ⋯