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 :
  • carrier : Set A
  • mul_mem' : ∀ {a b : A}, a s.carrierb s.carriera * b s.carrier
  • one_mem' : 1 s.carrier
  • add_mem' : ∀ {a b : A}, a s.carrierb s.carriera + b s.carrier
  • zero_mem' : 0 s.carrier
  • algebraMap_mem' : ∀ (r : R), ↑(algebraMap R A) r s.carrier
  • star_mem' : ∀ {a : A}, a s.carrierstar a s.carrier

    The carrier is closed under the star operation.

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

Instances For
    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 => S.carrier, coe_injective' := (_ : ∀ (p q : StarSubalgebra R A), (fun S => S.carrier) p = (fun S => S.carrier) qp = q) }
    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) :
    StarRing { x // x s }
    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 { x // x 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
    • One or more equations did not get rendered due to their size.
    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) :
      ↑(StarSubalgebra.copy S 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) :
      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) :
      RingHom.rangeS (algebraMap R A) 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) :
      { x // x S } →⋆ₐ[R] A

      Embedding of a subalgebra into the algebra.

      Equations
      • One or more equations did not get rendered due to their size.
      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) :
        ↑(StarSubalgebra.subtype S) = 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 : { x // x S }) :
        @[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) :
        Subalgebra.val S.toSubalgebra = (StarSubalgebra.subtype S).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 : { x // x 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₂) :
        { x // x S₁ } →⋆ₐ[R] { x // x S₂ }

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

        Equations
        • One or more equations did not get rendered due to their size.
        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₂) :
          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
          • One or more equations did not get rendered due to their size.
          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 x, x S 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
            • One or more equations did not get rendered due to their size.
            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
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                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 ∀ (g : A), g sg * 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) :
                ↑(Subalgebra.starClosure S) = ⋂ (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
                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) :
                  (Subalgebra.starClosure S).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) :
                  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} :
                  Subalgebra.starClosure S₁ S₂ S₁ S₂.toSubalgebra

                  The star subalgebra generated by a set #

                  @[simp]
                  theorem StarSubalgebra.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) :
                  ↑(StarSubalgebra.adjoin R s) = ⋂ (t : Subsemiring A) (_ : Set.range ↑(algebraMap R A) t s t star s t), t
                  def StarSubalgebra.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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem StarSubalgebra.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) :
                    (StarSubalgebra.adjoin R s).toSubalgebra = Algebra.adjoin R (s star s)
                    theorem StarSubalgebra.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 StarSubalgebra.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 StarSubalgebra.gc {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] :
                    def StarSubalgebra.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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem StarSubalgebra.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 StarSubalgebra.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 StarSubalgebra.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 StarSubalgebra.adjoin R s) (Hs : (x : A) → x sp x) (Halg : (r : R) → p (↑(algebraMap R A) r)) (Hadd : (x y : A) → p xp yp (x + y)) (Hmul : (x y : A) → p xp yp (x * y)) (Hstar : (x : A) → p xp (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 StarSubalgebra.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 StarSubalgebra.adjoin R s) (hb : b StarSubalgebra.adjoin R s) (Hs : (x : A) → x s(y : A) → y sp x y) (Halg : (r₁ r₂ : R) → p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂)) (Halg_left : (r : R) → (x : A) → x sp (↑(algebraMap R A) r) x) (Halg_right : (r : R) → (x : A) → x sp 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 StarSubalgebra.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 : { x // x StarSubalgebra.adjoin R s }Prop} (a : { x // x StarSubalgebra.adjoin R s }) (Hs : (x : A) → (h : x s) → p { val := x, property := (_ : x ↑(StarSubalgebra.adjoin R s)) }) (Halg : (r : R) → p (↑(algebraMap R { x // x StarSubalgebra.adjoin R s }) r)) (Hadd : (x y : { x // x StarSubalgebra.adjoin R s }) → p xp yp (x + y)) (Hmul : (x y : { x // x StarSubalgebra.adjoin R s }) → p xp yp (x * y)) (Hstar : (x : { x // x StarSubalgebra.adjoin R s }) → p xp (star x)) :
                      p a

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

                      @[reducible]
                      def StarSubalgebra.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 : ∀ (a : A), a s∀ (b : A), b sa * b = b * a) (hcomm_star : ∀ (a : A), a s∀ (b : A), b sa * 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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible]
                        def StarSubalgebra.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 : ∀ (a : A), a s∀ (b : A), b sa * b = b * a) (hcomm_star : ∀ (a : A), a s∀ (b : A), b sa * 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
                        • One or more equations did not get rendered due to their size.
                        Instances For

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          instance StarSubalgebra.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
                          • One or more equations did not get rendered due to their size.

                          Complete lattice structure #

                          Equations
                          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) = ⋂ (s : StarSubalgebra R A) (_ : s S), 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 ∀ (p : StarSubalgebra R A), p Sx 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] [hF : 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] [hF : StarAlgHomClass F R A B] (f : F) (g : F) (x : A) :
                            x StarAlgHom.equalizer f g f x = g x
                            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] [hF : 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] [hF : StarAlgHomClass F R A B] {s : Set A} (h : StarSubalgebra.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} [StarAlgHomClass F R { x // x StarSubalgebra.adjoin R s } B] {f : F} {g : F} (h : ∀ (x : { x // x StarSubalgebra.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} [StarAlgHomClass F R { x // x StarSubalgebra.adjoin R {a} } B] {f : F} {g : F} (h : f { val := a, property := (_ : a StarSubalgebra.adjoin R {a}) } = g { val := a, property := (_ : a StarSubalgebra.adjoin R {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
                            • One or more equations did not get rendered due to their size.
                            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] { x // x S }

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              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) :
                                ↑(↑(StarAlgHom.codRestrict f 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) :
                                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) :
                                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) :

                                Restriction of the codomain of a StarAlgHom to its range.

                                Equations
                                Instances For
                                  @[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 : { x // x AlgHom.range f }), ↑(StarAlgEquiv.symm (StarAlgEquiv.ofInjective f hf)) a = Equiv.invFun (AlgEquiv.ofInjective (f) hf).toEquiv a
                                  @[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) :
                                  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) :

                                  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_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.symm (StarAlgEquiv.restrictScalars R f)) a = Equiv.invFun f.toEquiv a
                                      @[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) :
                                      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