Documentation

Mathlib.Algebra.Star.Subalgebra

Star subalgebras #

A *-subalgebra is a subalgebra of a *-algebra which is closed under *.

The centralizer of a *-closed set is a *-subalgebra.

structure StarSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] extends Subalgebra :

A *-subalgebra is a subalgebra of a *-algebra which is closed under *.

  • carrier : Set A
  • mul_mem' : ∀ {a b : A}, a self.carrierb self.carriera * b self.carrier
  • one_mem' : 1 self.carrier
  • add_mem' : ∀ {a b : A}, a self.carrierb self.carriera + b self.carrier
  • zero_mem' : 0 self.carrier
  • algebraMap_mem' : ∀ (r : R), (algebraMap R A) r self.carrier
  • star_mem' : ∀ {a : A}, a self.carrierstar a self.carrier

    The carrier is closed under the star operation.

Instances For
    theorem StarSubalgebra.star_mem' {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (self : StarSubalgebra R A) {a : A} :
    a self.carrierstar a self.carrier

    The carrier is closed under the star operation.

    instance StarSubalgebra.setLike {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] :
    Equations
    • StarSubalgebra.setLike = { coe := fun (S : StarSubalgebra R A) => S.carrier, coe_injective' := }
    instance StarSubalgebra.starMemClass {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] :
    Equations
    • =
    Equations
    • =
    instance StarSubalgebra.smulMemClass {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] :
    Equations
    • =
    instance StarSubalgebra.subringClass {R : Type u_6} {A : Type u_7} [CommRing R] [StarRing R] [Ring A] [StarRing A] [Algebra R A] [StarModule R A] :
    Equations
    • =
    instance StarSubalgebra.starRing {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : StarSubalgebra R A) :
    Equations
    instance StarSubalgebra.algebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : StarSubalgebra R A) :
    Algebra R s
    Equations
    • s.algebra = s.algebra'
    instance StarSubalgebra.starModule {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : StarSubalgebra R A) :
    StarModule R s
    Equations
    • =
    @[simp]
    theorem StarSubalgebra.mem_carrier {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {s : StarSubalgebra R A} {x : A} :
    x s.carrier x s
    theorem StarSubalgebra.ext {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} {T : StarSubalgebra R A} (h : ∀ (x : A), x S x T) :
    S = T
    @[simp]
    theorem StarSubalgebra.coe_mk {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : Subalgebra R A) (h : ∀ {a : A}, a S.carrierstar a S.carrier) :
    { toSubalgebra := S, star_mem' := h } = S
    @[simp]
    theorem StarSubalgebra.mem_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} {x : A} :
    x S.toSubalgebra x S
    @[simp]
    theorem StarSubalgebra.coe_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
    S.toSubalgebra = S
    theorem StarSubalgebra.toSubalgebra_injective {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] :
    Function.Injective StarSubalgebra.toSubalgebra
    theorem StarSubalgebra.toSubalgebra_inj {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} {U : StarSubalgebra R A} :
    S.toSubalgebra = U.toSubalgebra S = U
    theorem StarSubalgebra.toSubalgebra_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} :
    S₁.toSubalgebra S₂.toSubalgebra S₁ S₂
    def StarSubalgebra.copy {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (s : Set A) (hs : s = S) :

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

    Equations
    • S.copy s hs = { toSubalgebra := S.copy s hs, star_mem' := }
    Instances For
      @[simp]
      theorem StarSubalgebra.coe_copy {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (s : Set A) (hs : s = S) :
      (S.copy s hs) = s
      theorem StarSubalgebra.copy_eq {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (s : Set A) (hs : s = S) :
      S.copy s hs = S
      theorem StarSubalgebra.algebraMap_mem {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (r : R) :
      (algebraMap R A) r S
      theorem StarSubalgebra.rangeS_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
      (algebraMap R A).rangeS S.toSubsemiring
      theorem StarSubalgebra.range_subset {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
      Set.range (algebraMap R A) S
      theorem StarSubalgebra.range_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
      Set.range (algebraMap R A) S
      theorem StarSubalgebra.smul_mem {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) {x : A} (hx : x S) (r : R) :
      r x S
      def StarSubalgebra.subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
      S →⋆ₐ[R] A

      Embedding of a subalgebra into the algebra.

      Equations
      • S.subtype = { toFun := Subtype.val, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := , map_star' := }
      Instances For
        @[simp]
        theorem StarSubalgebra.coe_subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
        S.subtype = Subtype.val
        theorem StarSubalgebra.subtype_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) (x : S) :
        S.subtype x = x
        @[simp]
        theorem StarSubalgebra.toSubalgebra_subtype {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
        S.val = S.subtype.toAlgHom
        @[simp]
        theorem StarSubalgebra.inclusion_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ S₂) :
        ∀ (a : S₁), (StarSubalgebra.inclusion h) a = Subtype.map id h a
        def StarSubalgebra.inclusion {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ S₂) :
        S₁ →⋆ₐ[R] S₂

        The inclusion map between StarSubalgebras given by Subtype.map id as a StarAlgHom.

        Equations
        Instances For
          theorem StarSubalgebra.inclusion_injective {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ S₂) :
          @[simp]
          theorem StarSubalgebra.subtype_comp_inclusion {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ S₂) :
          S₂.subtype.comp (StarSubalgebra.inclusion h) = S₁.subtype
          def StarSubalgebra.map {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R A) :

          Transport a star subalgebra via a star algebra homomorphism.

          Equations
          Instances For
            theorem StarSubalgebra.map_mono {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} {f : A →⋆ₐ[R] B} :
            S₁ S₂StarSubalgebra.map f S₁ StarSubalgebra.map f S₂
            @[simp]
            theorem StarSubalgebra.map_id {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
            theorem StarSubalgebra.map_map {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] (S : StarSubalgebra R A) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
            @[simp]
            theorem StarSubalgebra.mem_map {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {y : B} :
            y StarSubalgebra.map f S xS, f x = y
            theorem StarSubalgebra.map_toSubalgebra {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} :
            (StarSubalgebra.map f S).toSubalgebra = Subalgebra.map f.toAlgHom S.toSubalgebra
            @[simp]
            theorem StarSubalgebra.coe_map {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (S : StarSubalgebra R A) (f : A →⋆ₐ[R] B) :
            (StarSubalgebra.map f S) = f '' S
            def StarSubalgebra.comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) :

            Preimage of a star subalgebra under a star algebra homomorphism.

            Equations
            Instances For
              theorem StarSubalgebra.map_le_iff_le_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {U : StarSubalgebra R B} :
              theorem StarSubalgebra.comap_mono {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] {S₁ : StarSubalgebra R B} {S₂ : StarSubalgebra R B} {f : A →⋆ₐ[R] B} :
              S₁ S₂StarSubalgebra.comap f S₁ StarSubalgebra.comap f S₂
              @[simp]
              theorem StarSubalgebra.comap_id {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
              theorem StarSubalgebra.comap_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] (S : StarSubalgebra R C) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
              @[simp]
              theorem StarSubalgebra.mem_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (S : StarSubalgebra R B) (f : A →⋆ₐ[R] B) (x : A) :
              @[simp]
              theorem StarSubalgebra.coe_comap {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (S : StarSubalgebra R B) (f : A →⋆ₐ[R] B) :
              (StarSubalgebra.comap f S) = f ⁻¹' S
              def StarSubalgebra.centralizer (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :

              The centralizer, or commutant, of the star-closure of a set as a star subalgebra.

              Equations
              Instances For
                @[simp]
                theorem StarSubalgebra.coe_centralizer (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) :
                (StarSubalgebra.centralizer R s) = (s star s).centralizer
                theorem StarSubalgebra.mem_centralizer_iff (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {s : Set A} {z : A} :
                z StarSubalgebra.centralizer R s gs, g * z = z * g star g * z = z * star g

                The star closure of a subalgebra #

                instance Subalgebra.involutiveStar {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :

                The pointwise star of a subalgebra is a subalgebra.

                Equations
                @[simp]
                theorem Subalgebra.mem_star_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) (x : A) :
                x star S star x S
                theorem Subalgebra.star_mem_star_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) (x : A) :
                star x star S x S
                @[simp]
                theorem Subalgebra.coe_star {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
                (star S) = star S
                theorem Subalgebra.star_mono {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                theorem Subalgebra.star_adjoin_comm (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :

                The star operation on Subalgebra commutes with Algebra.adjoin.

                @[simp]
                theorem Subalgebra.starClosure_carrier {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
                S.starClosure = ⋂ (t : Subsemiring A), ⋂ (_ : Set.range (algebraMap R A) t S t star S t), t
                def Subalgebra.starClosure {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :

                The StarSubalgebra obtained from S : Subalgebra R A by taking the smallest subalgebra containing both S and star S.

                Equations
                • S.starClosure = { toSubalgebra := S star S, star_mem' := }
                Instances For
                  theorem Subalgebra.starClosure_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
                  S.starClosure.toSubalgebra = S star S
                  theorem Subalgebra.starClosure_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ S₂.toSubalgebra) :
                  S₁.starClosure S₂
                  theorem Subalgebra.starClosure_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} :
                  S₁.starClosure S₂ S₁ S₂.toSubalgebra

                  The star subalgebra generated by a set #

                  @[simp]
                  theorem StarAlgebra.adjoin_carrier (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
                  (StarAlgebra.adjoin R s) = ⋂ (t : Subsemiring A), ⋂ (_ : Set.range (algebraMap R A) t s t star s t), t
                  def StarAlgebra.adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :

                  The minimal star subalgebra that contains s.

                  Equations
                  Instances For
                    theorem StarAlgebra.adjoin_eq_starClosure_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
                    StarAlgebra.adjoin R s = (Algebra.adjoin R s).starClosure
                    theorem StarAlgebra.adjoin_toSubalgebra (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
                    (StarAlgebra.adjoin R s).toSubalgebra = Algebra.adjoin R (s star s)
                    theorem StarAlgebra.subset_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
                    theorem StarAlgebra.star_subset_adjoin (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
                    theorem StarAlgebra.gc {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                    def StarAlgebra.gi {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :

                    Galois insertion between adjoin and coe.

                    Equations
                    Instances For
                      theorem StarAlgebra.adjoin_le {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {s : Set A} (hs : s S) :
                      theorem StarAlgebra.adjoin_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {s : Set A} :
                      theorem StarAlgebra.adjoin_eq {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : StarSubalgebra R A) :
                      theorem StarAlgebra.adjoin_eq_span {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (s : Set A) :
                      Subalgebra.toSubmodule (StarAlgebra.adjoin R s).toSubalgebra = Submodule.span R (Submonoid.closure (s star s))
                      theorem Subalgebra.starClosure_eq_adjoin {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Subalgebra R A) :
                      S.starClosure = StarAlgebra.adjoin R S
                      theorem StarAlgebra.adjoin_induction {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : AProp} {a : A} (h : a StarAlgebra.adjoin R s) (mem : xs, p x) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r)) (add : ∀ (x y : A), p xp yp (x + y)) (mul : ∀ (x y : A), p xp yp (x * y)) (star : ∀ (x : A), p xp (Star.star x)) :
                      p a

                      If some predicate holds for all x ∈ (s : Set A) and this predicate is closed under the algebraMap, addition, multiplication and star operations, then it holds for a ∈ adjoin R s.

                      theorem StarAlgebra.adjoin_induction₂ {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : AAProp} {a : A} {b : A} (ha : a StarAlgebra.adjoin R s) (hb : b StarAlgebra.adjoin R s) (Hs : xs, ys, p x y) (Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)) (Halg_left : ∀ (r : R), xs, p ((algebraMap R A) r) x) (Halg_right : ∀ (r : R), xs, p x ((algebraMap R A) r)) (Hadd_left : ∀ (x₁ x₂ y : A), p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : A), p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : A), p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : A), p x y₁p x y₂p x (y₁ * y₂)) (Hstar : ∀ (x y : A), p x yp (star x) (star y)) (Hstar_left : ∀ (x y : A), p x yp (star x) y) (Hstar_right : ∀ (x y : A), p x yp x (star y)) :
                      p a b
                      theorem StarAlgebra.adjoin_induction' {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : (StarAlgebra.adjoin R s)Prop} (a : (StarAlgebra.adjoin R s)) (mem : ∀ (x : A) (h : x s), p x, ) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R (StarAlgebra.adjoin R s)) r)) (add : ∀ (x y : (StarAlgebra.adjoin R s)), p xp yp (x + y)) (mul : ∀ (x y : (StarAlgebra.adjoin R s)), p xp yp (x * y)) (star : ∀ (x : (StarAlgebra.adjoin R s)), p xp (Star.star x)) :
                      p a

                      The difference with StarSubalgebra.adjoin_induction is that this acts on the subtype.

                      @[reducible, inline]
                      abbrev StarAlgebra.adjoinCommSemiringOfComm (R : Type u_2) {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing 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 also commute pairwise with elements of star s, then StarSubalgebra.adjoin R s is commutative. See note [reducible non-instances].

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev StarAlgebra.adjoinCommRingOfComm (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A] [StarRing 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 also commute pairwise with elements of star s, then StarSubalgebra.adjoin R s is commutative. See note [reducible non-instances].

                        Equations
                        Instances For

                          The star subalgebra StarSubalgebra.adjoin R {x} generated by a single x : A is commutative if x is normal.

                          Equations
                          instance StarAlgebra.adjoinCommRingOfIsStarNormal (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A] [StarRing A] [StarModule R A] (x : A) [IsStarNormal x] :

                          The star subalgebra StarSubalgebra.adjoin R {x} generated by a single x : A is commutative if x is normal.

                          Equations

                          Complete lattice structure #

                          Equations
                          • StarSubalgebra.completeLattice = let __spread.0 := StarAlgebra.gi.liftCompleteLattice; CompleteLattice.mk
                          instance StarSubalgebra.inhabited {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                          Equations
                          • StarSubalgebra.inhabited = { default := }
                          @[simp]
                          theorem StarSubalgebra.coe_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                          = Set.univ
                          @[simp]
                          theorem StarSubalgebra.mem_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {x : A} :
                          @[simp]
                          theorem StarSubalgebra.top_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                          .toSubalgebra =
                          @[simp]
                          theorem StarSubalgebra.toSubalgebra_eq_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} :
                          S.toSubalgebra = S =
                          theorem StarSubalgebra.mem_sup_left {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} :
                          x Sx S T
                          theorem StarSubalgebra.mem_sup_right {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} :
                          x Tx S T
                          theorem StarSubalgebra.mul_mem_sup {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} {y : A} (hx : x S) (hy : y T) :
                          x * y S T
                          theorem StarSubalgebra.map_sup {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R A) (T : StarSubalgebra R A) :
                          @[simp]
                          theorem StarSubalgebra.coe_inf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : StarSubalgebra R A) (T : StarSubalgebra R A) :
                          (S T) = S T
                          @[simp]
                          theorem StarSubalgebra.mem_inf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} {T : StarSubalgebra R A} {x : A} :
                          x S T x S x T
                          @[simp]
                          theorem StarSubalgebra.inf_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : StarSubalgebra R A) (T : StarSubalgebra R A) :
                          (S T).toSubalgebra = S.toSubalgebra T.toSubalgebra
                          @[simp]
                          theorem StarSubalgebra.coe_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Set (StarSubalgebra R A)) :
                          (sInf S) = sS, s
                          theorem StarSubalgebra.mem_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : Set (StarSubalgebra R A)} {x : A} :
                          x sInf S pS, x p
                          @[simp]
                          theorem StarSubalgebra.sInf_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] (S : Set (StarSubalgebra R A)) :
                          (sInf S).toSubalgebra = sInf (StarSubalgebra.toSubalgebra '' S)
                          @[simp]
                          theorem StarSubalgebra.coe_iInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {ι : Sort u_5} {S : ιStarSubalgebra R A} :
                          (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                          theorem StarSubalgebra.mem_iInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {ι : Sort u_5} {S : ιStarSubalgebra R A} {x : A} :
                          x ⨅ (i : ι), S i ∀ (i : ι), x S i
                          @[simp]
                          theorem StarSubalgebra.iInf_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {ι : Sort u_5} (S : ιStarSubalgebra R A) :
                          (⨅ (i : ι), S i).toSubalgebra = ⨅ (i : ι), (S i).toSubalgebra
                          theorem StarSubalgebra.bot_toSubalgebra {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                          .toSubalgebra =
                          theorem StarSubalgebra.mem_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {x : A} :
                          @[simp]
                          theorem StarSubalgebra.coe_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                          theorem StarSubalgebra.eq_top_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} :
                          S = ∀ (x : A), x S
                          def StarAlgHom.equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f : F) (g : F) :

                          The equalizer of two star R-algebra homomorphisms.

                          Equations
                          Instances For
                            @[simp]
                            theorem StarAlgHom.mem_equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f : F) (g : F) (x : A) :
                            theorem StarAlgHom.adjoin_le_equalizer {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f : F) (g : F) {s : Set A} (h : Set.EqOn (f) (g) s) :
                            theorem StarAlgHom.ext_of_adjoin_eq_top {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] {s : Set A} (h : StarAlgebra.adjoin R s = ) ⦃f : F ⦃g : F (hs : Set.EqOn (f) (g) s) :
                            f = g
                            theorem StarAlgHom.map_adjoin {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (s : Set A) :
                            theorem StarAlgHom.ext_adjoin {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] {s : Set A} [FunLike F ((StarAlgebra.adjoin R s)) B] [AlgHomClass F R ((StarAlgebra.adjoin R s)) B] [StarAlgHomClass F R ((StarAlgebra.adjoin R s)) B] {f : F} {g : F} (h : ∀ (x : (StarAlgebra.adjoin R s)), x sf x = g x) :
                            f = g
                            theorem StarAlgHom.ext_adjoin_singleton {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] {a : A} [FunLike F ((StarAlgebra.adjoin R {a})) B] [AlgHomClass F R ((StarAlgebra.adjoin R {a})) B] [StarAlgHomClass F R ((StarAlgebra.adjoin R {a})) B] {f : F} {g : F} (h : f a, = g a, ) :
                            f = g
                            def StarAlgHom.range {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (φ : A →⋆ₐ[R] B) :

                            Range of a StarAlgHom as a star subalgebra.

                            Equations
                            • φ.range = { toSubalgebra := φ.range, star_mem' := }
                            Instances For
                              theorem StarAlgHom.range_eq_map_top {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (φ : A →⋆ₐ[R] B) :
                              def StarAlgHom.codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) :
                              A →⋆ₐ[R] S

                              Restriction of the codomain of a StarAlgHom to a star subalgebra containing the range.

                              Equations
                              • f.codRestrict S hf = { toAlgHom := f.codRestrict S.toSubalgebra hf, map_star' := }
                              Instances For
                                @[simp]
                                theorem StarAlgHom.coe_codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) (x : A) :
                                ((f.codRestrict S hf) x) = f x
                                @[simp]
                                theorem StarAlgHom.subtype_comp_codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) :
                                S.subtype.comp (f.codRestrict S hf) = f
                                theorem StarAlgHom.injective_codRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x S) :
                                Function.Injective (f.codRestrict S hf) Function.Injective f
                                def StarAlgHom.rangeRestrict {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) :
                                A →⋆ₐ[R] f.range

                                Restriction of the codomain of a StarAlgHom to its range.

                                Equations
                                • f.rangeRestrict = f.codRestrict f.range
                                Instances For
                                  @[simp]
                                  theorem StarAlgEquiv.ofInjective_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (a : A) :
                                  (StarAlgEquiv.ofInjective f hf) a = f.rangeRestrict a
                                  @[simp]
                                  theorem StarAlgEquiv.ofInjective_symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) :
                                  ∀ (a : (f).range), (StarAlgEquiv.ofInjective f hf).symm a = (AlgEquiv.ofInjective (f) hf).invFun a
                                  noncomputable def StarAlgEquiv.ofInjective {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) :
                                  A ≃⋆ₐ[R] f.range

                                  The StarAlgEquiv onto the range corresponding to an injective StarAlgHom.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem StarAlgHom.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A →⋆ₐ[S] B) :
                                    ∀ (a : A), (StarAlgHom.restrictScalars R f) a = f a
                                    def StarAlgHom.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A →⋆ₐ[S] B) :
                                    Equations
                                    Instances For
                                      theorem StarAlgHom.restrictScalars_injective (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] :
                                      @[simp]
                                      theorem StarAlgEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) (a : A) :
                                      @[simp]
                                      theorem StarAlgEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) :
                                      ∀ (a : B), (StarAlgEquiv.restrictScalars R f).symm a = f.invFun a
                                      def StarAlgEquiv.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For