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

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

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

      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

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

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

          Equations
            Instances For
              @[simp]
              theorem NonUnitalStarSubalgebraClass.subtype_apply {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 : s) :
              (subtype s) x = x
              @[simp]
              @[deprecated NonUnitalStarSubalgebraClass.coe_subtype (since := "2025-02-18")]

              Alias of NonUnitalStarSubalgebraClass.coe_subtype.

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

              Instances For

                The actual NonUnitalStarSubalgebra obtained from an element of a type satisfying NonUnitalSubsemiringClass, SMulMemClass and StarMemClass.

                Equations
                  Instances For
                    @[simp]
                    theorem NonUnitalStarSubalgebra.ofClass_carrier {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [SetLike S A] [NonUnitalSubsemiringClass S A] [SMulMemClass S R A] [StarMemClass S A] (s : S) :
                    (ofClass s) = s
                    @[instance 100]
                    instance NonUnitalStarSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] :
                    CanLift (Set A) (NonUnitalStarSubalgebra R A) SetLike.coe fun (s : Set A) => 0 s (∀ {x y : A}, x sy sx + y s) (∀ {x y : A}, x sy sx * y s) (∀ (r : R) {x : A}, x sr x s) ∀ {x : A}, x sstar 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
                    theorem NonUnitalStarSubalgebra.ext_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {S T : NonUnitalStarSubalgebra R A} :
                    S = T ∀ (x : A), x S x T

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

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

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

                        Equations
                          Instances For

                            NonUnitalStarSubalgebras inherit structure from their NonUnitalSubsemiringClass and NonUnitalSubringClass instances.

                            Equations

                              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
                                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
                                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_neg {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing 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] [NonUnitalNonAssocRing 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) [SMul R' R] [SMul 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

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

                                Equations
                                  Instances For
                                    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₂map f S₁ map f 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) :
                                    map g (map f S) = 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 map f S xS, f x = y
                                    @[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) :
                                    (map f S) = f '' S

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

                                    Equations
                                      Instances For
                                        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} :
                                        map f S U S comap f U
                                        @[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 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) :
                                        (comap f S) = f ⁻¹' S

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

                                        Equations
                                          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 : xs, star 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 : xs, star x s) :
                                            (s.toNonUnitalStarSubalgebra h_star) = 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) :

                                            Range of an NonUnitalAlgHom as a NonUnitalStarSubalgebra.

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

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

                                                Equations
                                                  Instances For
                                                    @[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) :
                                                    @[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) :
                                                    ((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) :
                                                    @[reducible, inline]

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

                                                    This is the bundled version of Set.rangeFactorization.

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

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

                                                        Equations
                                                          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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ ψ : F) (x : A) :
                                                            x 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 : 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.

                                                            Equations
                                                              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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {g : BA} {f : F} (h : Function.LeftInverse g f) (x : A) :
                                                                ((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 : BA} {f : F} (h : Function.LeftInverse g f) (x : (NonUnitalStarAlgHom.range f)) :
                                                                (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) :

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

                                                                Equations
                                                                  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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (hf : Function.Injective f) (x : A) :
                                                                    ((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.

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

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

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

                                                                          The minimal non-unital subalgebra that includes s.

                                                                          Equations
                                                                            Instances For
                                                                              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 (adjoin R s)
                                                                              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 adjoin R sProp} (mem : ∀ (x : A) (hx : x s), p x ) (add : ∀ (x y : A) (hx : x adjoin R s) (hy : y adjoin R s), p x hxp y hyp (x + y) ) (zero : p 0 ) (mul : ∀ (x y : A) (hx : x adjoin R s) (hy : y adjoin R s), p x hxp y hyp (x * y) ) (smul : ∀ (r : R) (x : A) (hx : x adjoin R s), p x hxp (r x) ) (star : ∀ (x : A) (hx : x adjoin R s), p x hxp (star x) ) {a : A} (ha : a adjoin R s) :
                                                                              p a ha

                                                                              Galois insertion between adjoin and Subtype.val.

                                                                              Equations
                                                                                Instances For
                                                                                  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) :
                                                                                  adjoin R s S
                                                                                  @[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} :
                                                                                  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 Sx ST
                                                                                  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 Tx ST
                                                                                  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 ST
                                                                                  @[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) :
                                                                                  (ST) = 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 ST x S x T
                                                                                  @[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) = sS, 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 pS, x p
                                                                                  @[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
                                                                                  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
                                                                                  @[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.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) :
                                                                                  @[simp]
                                                                                  @[deprecated NonUnitalStarAlgebra.range_eq_top (since := "2024-11-11")]

                                                                                  Alias of NonUnitalStarAlgebra.range_eq_top.

                                                                                  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
                                                                                    Instances For
                                                                                      @[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) :
                                                                                      (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) :
                                                                                      (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) :
                                                                                      (inclusion htu) ((inclusion hst) x) = (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) :
                                                                                      ((inclusion h) s) = s

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

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[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₁
                                                                                          @[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₁
                                                                                          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 TS₁ 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₁ = (ST).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 (inclusion h)) (T : NonUnitalStarSubalgebra R A) (hT : T = iSup K) :

                                                                                          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
                                                                                            Instances For
                                                                                              @[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 (inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : (K i)) (h : K i T) :
                                                                                              (iSupLift K dir f hf T hT) ((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 (inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i T) :
                                                                                              (iSupLift K dir f hf T hT).comp (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 (inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : (K i)) (hx : x T) :
                                                                                              (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 (inclusion h)} {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : T) (hx : x K i) :
                                                                                              (iSupLift K dir f hf T hT) x = (f i) x, 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.

                                                                                              Equations
                                                                                                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 center R A ∀ (b : A), b * a = a * b

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

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      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 centralizer R s gs, g * z = z * g star g * z = z * star g
                                                                                                      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 adjoin R s) (h : bs, Commute a b) (h_star : bs, Commute a (star 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 adjoin R {b}) (h : Commute a b) (h_star : Commute a (star 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 : as, bs, a * b = b * a) (hcomm_star : as, bs, a * star b = star b * a) :

                                                                                                      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
                                                                                                        Instances For
                                                                                                          @[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 : as, bs, a * b = b * a) (hcomm_star : as, bs, a * star b = star b * a) :

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