Documentation

Mathlib.Algebra.Star.NonUnitalSubalgebra

Non-unital Star Subalgebras #

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

TODO #

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.

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.

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.

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.

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.

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
    @[simp]
    • carrier : Set A
    • add_mem' : ∀ {a b : A}, a s.carrierb s.carriera + b s.carrier
    • zero_mem' : 0 s.carrier
    • mul_mem' : ∀ {a b : A}, a s.carrierb s.carriera * b s.carrier
    • smul_mem' : ∀ (c : R) {x : A}, x s.carrierc x s.carrier
    • star_mem' : ∀ {a : A}, a s.carrierstar 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
      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 : NonUnitalStarSubalgebra R A} {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 : NonUnitalStarSubalgebra R A} {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₁ : NonUnitalStarSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} :
      S₁.toNonUnitalSubalgebra S₂.toNonUnitalSubalgebra S₁ S₂

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

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

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

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

          NonUnitalStarSubalgebras inherit structure from their NonUnitalSubsemiringClass and NonUnitalSubringClass instances.

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

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

          Instances For
            @[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
            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
            @[simp]

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

            Instances For
              @[simp]
              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 sstar x s) :

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

              Instances For
                @[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 sstar x s} {x : A} :
                @[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 sstar x 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 : A), x sstar x s) :
                (NonUnitalSubalgebra.toNonUnitalStarSubalgebra s h_star).toNonUnitalSubalgebra = s
                @[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
                @[simp]
                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
                  @[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
                  @[reducible]

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

                  This is the bundled version of Set.rangeFactorization.

                  Instances For

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

                    Instances For
                      @[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
                      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 : BA} {f : F} (h : Function.LeftInverse g 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
                        @[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 : BA} {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] [hF : NonUnitalStarAlgHomClass F R A B] {g : BA} {f : F} (h : Function.LeftInverse g f) (x : { x // x NonUnitalStarAlgHom.range f }) :
                        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) :

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

                        Instances For
                          @[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 #

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

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

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

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

                            The minimal non-unital subalgebra that includes s.

                            Instances For

                              Galois insertion between adjoin and Subtype.val.

                              Instances For
                                @[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} :
                                @[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 : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {x : A} :
                                x Sx 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 : NonUnitalStarSubalgebra R A} {T : NonUnitalStarSubalgebra R A} {x : A} {y : A} (hx : x S) (hy : y T) :
                                x * y S 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 : NonUnitalStarSubalgebra R A) (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 : NonUnitalStarSubalgebra R A} {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 : NonUnitalStarSubalgebra R A) (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 : NonUnitalStarSubalgebra R A) (_ : 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 : NonUnitalStarSubalgebra R A), p Sx 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
                                @[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
                                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]
                                @[simp]
                                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
                                  @[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 }
                                  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
                                  @[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 }) :

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

                                  Instances For
                                    @[simp]
                                    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
                                    @[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₁
                                    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)
                                    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
                                      @[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
                                      @[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) :
                                      @[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
                                      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 }

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

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

                                        Instances For
                                          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 sg * z = z * g star g * z = z * star g