Documentation

Mathlib.Algebra.Star.StarAlgHom

Morphisms of star algebras #

This file defines morphisms between R-algebras (unital or non-unital) A and B where both A and B are equipped with a star operation. These morphisms, namely StarAlgHom and NonUnitalStarAlgHom are direct extensions of their non-starred counterparts with a field map_star which guarantees they preserve the star operation. We keep the type classes as generic as possible, in keeping with the definition of NonUnitalAlgHom in the non-unital case. In this file, we only assume Star unless we want to talk about the zero map as a NonUnitalStarAlgHom, in which case we need StarAddMonoid. Note that the scalar ring R is not required to have a star operation, nor do we need StarRing or StarModule structures on A and B.

As with NonUnitalAlgHom, in the non-unital case the multiplications are not assumed to be associative or unital, or even to be compatible with the scalar actions. In a typical application, the operations will satisfy compatibility conditions making them into algebras (albeit possibly non-associative and/or non-unital) but such conditions are not required here for the definitions.

The primary impetus for defining these types is that they constitute the morphisms in the categories of unital C⋆-algebras (with StarAlgHoms) and of C⋆-algebras (with NonUnitalStarAlgHoms).

Main definitions #

Tags #

non-unital, algebra, morphism, star

Non-unital star algebra homomorphisms #

structure NonUnitalStarAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] extends NonUnitalAlgHom :
Type (max u_2 u_3)

A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between non-unital R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

  • toFun : AB
  • map_smul' : ∀ (m : R) (x : A), self.toFun (m x) = m self.toFun x
  • map_zero' : self.toFun 0 = 0
  • map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
  • map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
  • map_star' : ∀ (a : A), self.toFun (star a) = star (self.toFun a)

    By definition, a non-unital ⋆-algebra homomorphism preserves the star operation.

Instances For

    A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between non-unital R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

    Equations
    Instances For

      A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between non-unital R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

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

        NonUnitalStarAlgHomClass F R A B asserts F is a type of bundled non-unital ⋆-algebra homomorphisms from A to B.

          Instances

            Turn an element of a type F satisfying NonUnitalStarAlgHomClass F R A B into an actual NonUnitalStarAlgHom. This is declared as the default coercion from F to A →⋆ₙₐ[R] B.

            Equations
            • f = let __src := f; { toNonUnitalAlgHom := __src, map_star' := }
            Instances For
              Equations
              • NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHom = { coe := NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom }
              Equations
              • NonUnitalStarAlgHom.instFunLikeNonUnitalStarAlgHom = { coe := fun (f : A →⋆ₙₐ[R] B) => f.toFun, coe_injective' := }

              See Note [custom simps projection]

              Equations
              Instances For
                @[simp]
                theorem NonUnitalStarAlgHom.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {F : Type u_6} [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) :
                f = f
                @[simp]
                theorem NonUnitalStarAlgHom.coe_toNonUnitalAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {f : A →⋆ₙₐ[R] B} :
                f.toNonUnitalAlgHom = f
                theorem NonUnitalStarAlgHom.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {f : A →⋆ₙₐ[R] B} {g : A →⋆ₙₐ[R] B} (h : ∀ (x : A), f x = g x) :
                f = g
                def NonUnitalStarAlgHom.copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (f' : AB) (h : f' = f) :

                Copy of a NonUnitalStarAlgHom with a new toFun 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 NonUnitalStarAlgHom.coe_copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (f' : AB) (h : f' = f) :
                  theorem NonUnitalStarAlgHom.copy_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (f' : AB) (h : f' = f) :
                  @[simp]
                  theorem NonUnitalStarAlgHom.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : AB) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun x * { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun y) (h₅ : ∀ (a : A), { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toFun (star a) = star ({ toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toFun a)) :
                  { toNonUnitalAlgHom := { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }, map_star' := h₅ } = f
                  @[simp]
                  theorem NonUnitalStarAlgHom.coe_mk' {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →ₙₐ[R] B) (h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)) :
                  { toNonUnitalAlgHom := f, map_star' := h } = f
                  @[simp]
                  theorem NonUnitalStarAlgHom.mk_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun x * { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun y) (h₅ : ∀ (a : A), { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toFun (star a) = star ({ toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toFun a)) :
                  { toNonUnitalAlgHom := { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }, map_star' := h₅ } = f

                  The identity as a non-unital ⋆-algebra homomorphism.

                  Equations
                  Instances For

                    The composition of non-unital ⋆-algebra homomorphisms, as a non-unital ⋆-algebra homomorphism.

                    Equations
                    Instances For
                      @[simp]
                      Equations
                      • NonUnitalStarAlgHom.instMonoidNonUnitalStarAlgHom = Monoid.mk npowRec
                      @[simp]
                      theorem NonUnitalStarAlgHom.coe_one {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] :
                      1 = id
                      theorem NonUnitalStarAlgHom.one_apply {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] (a : A) :
                      1 a = a
                      Equations
                      • NonUnitalStarAlgHom.instInhabitedNonUnitalStarAlgHomToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarToInvolutiveStarToAddMonoidToAddCommMonoid = { default := 0 }

                      Unital star algebra homomorphisms #

                      structure StarAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] extends AlgHom :
                      Type (max u_2 u_3)

                      A ⋆-algebra homomorphism is an algebra homomorphism between R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

                      • toFun : AB
                      • map_one' : self.toFun 1 = 1
                      • map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
                      • map_zero' : self.toFun 0 = 0
                      • map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
                      • commutes' : ∀ (r : R), self.toFun ((algebraMap R A) r) = (algebraMap R B) r
                      • map_star' : ∀ (x : A), self.toFun (star x) = star (self.toFun x)

                        By definition, a ⋆-algebra homomorphism preserves the star operation.

                      Instances For

                        A ⋆-algebra homomorphism is an algebra homomorphism between R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

                        Equations
                        Instances For

                          A ⋆-algebra homomorphism is an algebra homomorphism between R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            class StarAlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [FunLike F A B] [AlgHomClass F R A B] extends StarHomClass :

                            StarAlgHomClass F R A B states that F is a type of ⋆-algebra homomorphisms.

                            You should also extend this typeclass when you extend StarAlgHom.

                              Instances
                                instance StarAlgHomClass.toNonUnitalStarAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) :
                                ∀ {x : CommSemiring R} {x_1 : Semiring A} [inst : Algebra R A] [inst_1 : Star A] {x_2 : Semiring B} [inst_2 : Algebra R B] [inst_3 : Star B] [inst_4 : FunLike F A B] [inst_5 : AlgHomClass F R A B] [inst_6 : StarAlgHomClass F R A B], NonUnitalStarAlgHomClass F R A B
                                Equations
                                • =
                                def StarAlgHomClass.toStarAlgHom {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f : F) :

                                Turn an element of a type F satisfying StarAlgHomClass F R A B into an actual StarAlgHom. This is declared as the default coercion from F to A →⋆ₐ[R] B.

                                Equations
                                • f = let __src := f; { toAlgHom := __src, map_star' := }
                                Instances For
                                  instance StarAlgHomClass.instCoeTCStarAlgHom (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] :
                                  Equations
                                  instance StarAlgHom.instFunLikeStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] :
                                  FunLike (A →⋆ₐ[R] B) A B
                                  Equations
                                  • StarAlgHom.instFunLikeStarAlgHom = { coe := fun (f : A →⋆ₐ[R] B) => f.toFun, coe_injective' := }
                                  instance StarAlgHom.instAlgHomClassStarAlgHomInstFunLikeStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] :
                                  Equations
                                  • =
                                  @[simp]
                                  theorem StarAlgHom.coe_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] {F : Type u_7} [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f : F) :
                                  f = f
                                  def StarAlgHom.Simps.apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) :
                                  AB

                                  See Note [custom simps projection]

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem StarAlgHom.coe_toAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] {f : A →⋆ₐ[R] B} :
                                    f.toAlgHom = f
                                    theorem StarAlgHom.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] {f : A →⋆ₐ[R] B} {g : A →⋆ₐ[R] B} (h : ∀ (x : A), f x = g x) :
                                    f = g
                                    def StarAlgHom.copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (f' : AB) (h : f' = f) :

                                    Copy of a StarAlgHom with a new toFun 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 StarAlgHom.coe_copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (f' : AB) (h : f' = f) :
                                      (StarAlgHom.copy f f' h) = f'
                                      theorem StarAlgHom.copy_eq {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (f' : AB) (h : f' = f) :
                                      @[simp]
                                      theorem StarAlgHom.coe_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : AB) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun 0 = 0) (h₄ : ∀ (x y : A), { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun (x + y) = { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun x + { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun y) (h₅ : ∀ (r : R), { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }.toFun ((algebraMap R A) r) = (algebraMap R B) r) (h₆ : ∀ (x : A), { toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }.toFun (star x) = star ({ toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }.toFun x)) :
                                      { toAlgHom := { toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }, map_star' := h₆ } = f
                                      @[simp]
                                      theorem StarAlgHom.coe_mk' {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →ₐ[R] B) (h : ∀ (x : A), f.toFun (star x) = star (f.toFun x)) :
                                      { toAlgHom := f, map_star' := h } = f
                                      @[simp]
                                      theorem StarAlgHom.mk_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun 0 = 0) (h₄ : ∀ (x y : A), { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun (x + y) = { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun x + { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }.toFun y) (h₅ : ∀ (r : R), { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }.toFun ((algebraMap R A) r) = (algebraMap R B) r) (h₆ : ∀ (x : A), { toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }.toFun (star x) = star ({ toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }.toFun x)) :
                                      { toAlgHom := { toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }, map_star' := h₆ } = f
                                      def StarAlgHom.id (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :

                                      The identity as a StarAlgHom.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem StarAlgHom.coe_id (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :
                                        (StarAlgHom.id R A) = id
                                        @[simp]
                                        theorem StarAlgHom.ofId_apply (R : Type u_7) (A : Type u_8) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] (a : R) :
                                        (StarAlgHom.ofId R A) a = (algebraMap R A) a
                                        def StarAlgHom.ofId (R : Type u_7) (A : Type u_8) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] :

                                        algebraMap R A as a StarAlgHom when A is a star algebra over R.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          instance StarAlgHom.instInhabitedStarAlgHom {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :
                                          Equations
                                          def StarAlgHom.comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) :

                                          The composition of ⋆-algebra homomorphisms, as a ⋆-algebra homomorphism.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem StarAlgHom.coe_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) :
                                            (StarAlgHom.comp f g) = f g
                                            @[simp]
                                            theorem StarAlgHom.comp_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) (a : A) :
                                            (StarAlgHom.comp f g) a = f (g a)
                                            @[simp]
                                            theorem StarAlgHom.comp_assoc {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] [Semiring D] [Algebra R D] [Star D] (f : C →⋆ₐ[R] D) (g : B →⋆ₐ[R] C) (h : A →⋆ₐ[R] B) :
                                            @[simp]
                                            theorem StarAlgHom.id_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) :
                                            @[simp]
                                            theorem StarAlgHom.comp_id {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) :
                                            instance StarAlgHom.instMonoidStarAlgHom {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :
                                            Equations
                                            • StarAlgHom.instMonoidStarAlgHom = Monoid.mk npowRec
                                            def StarAlgHom.toNonUnitalStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) :

                                            A unital morphism of ⋆-algebras is a NonUnitalStarAlgHom.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem StarAlgHom.coe_toNonUnitalStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) :

                                              Operations on the product type #

                                              Note that this is copied from Algebra.Hom.NonUnitalAlg.

                                              @[simp]
                                              theorem NonUnitalStarAlgHom.fst_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (self : A × B) :
                                              (NonUnitalStarAlgHom.fst R A B) self = self.1

                                              The first projection of a product is a non-unital ⋆-algebra homomorphism.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem NonUnitalStarAlgHom.snd_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (self : A × B) :
                                                (NonUnitalStarAlgHom.snd R A B) self = self.2

                                                The second projection of a product is a non-unital ⋆-algebra homomorphism.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem NonUnitalStarAlgHom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) (i : A) :
                                                  (NonUnitalStarAlgHom.prod f g) i = (f i, g i)

                                                  The Pi.prod of two morphisms is a morphism.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem NonUnitalStarAlgHom.prodEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)) :
                                                    NonUnitalStarAlgHom.prodEquiv f = NonUnitalStarAlgHom.prod f.1 f.2

                                                    Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

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

                                                      The left injection into a product is a non-unital algebra homomorphism.

                                                      Equations
                                                      Instances For

                                                        The right injection into a product is a non-unital algebra homomorphism.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          @[simp]
                                                          theorem StarAlgHom.fst_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (self : A × B) :
                                                          (StarAlgHom.fst R A B) self = self.1
                                                          def StarAlgHom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] :

                                                          The first projection of a product is a ⋆-algebra homomorphism.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem StarAlgHom.snd_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (self : A × B) :
                                                            (StarAlgHom.snd R A B) self = self.2
                                                            def StarAlgHom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] :

                                                            The second projection of a product is a ⋆-algebra homomorphism.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem StarAlgHom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) (x : A) :
                                                              (StarAlgHom.prod f g) x = (f x, g x)
                                                              def StarAlgHom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :

                                                              The Pi.prod of two morphisms is a morphism.

                                                              Equations
                                                              Instances For
                                                                theorem StarAlgHom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :
                                                                (StarAlgHom.prod f g) = Pi.prod f g
                                                                @[simp]
                                                                theorem StarAlgHom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :
                                                                @[simp]
                                                                theorem StarAlgHom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :
                                                                @[simp]
                                                                theorem StarAlgHom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] :
                                                                @[simp]
                                                                theorem StarAlgHom.prodEquiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B × C) :
                                                                StarAlgHom.prodEquiv.symm f = (StarAlgHom.comp (StarAlgHom.fst R B C) f, StarAlgHom.comp (StarAlgHom.snd R B C) f)
                                                                @[simp]
                                                                theorem StarAlgHom.prodEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)) :
                                                                StarAlgHom.prodEquiv f = StarAlgHom.prod f.1 f.2
                                                                def StarAlgHom.prodEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] :
                                                                (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C) (A →⋆ₐ[R] B × C)

                                                                Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

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

                                                                  Star algebra equivalences #

                                                                  structure StarAlgEquiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] extends RingEquiv :
                                                                  Type (max u_2 u_3)

                                                                  A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar multiplication and the star operation, which allows for considering both unital and non-unital equivalences with a single structure. Currently, AlgEquiv requires unital algebras, which is why this structure does not extend it.

                                                                  • toFun : AB
                                                                  • invFun : BA
                                                                  • left_inv : Function.LeftInverse self.invFun self.toFun
                                                                  • right_inv : Function.RightInverse self.invFun self.toFun
                                                                  • map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
                                                                  • map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
                                                                  • map_star' : ∀ (a : A), self.toFun (star a) = star (self.toFun a)

                                                                    By definition, a ⋆-algebra equivalence preserves the star operation.

                                                                  • map_smul' : ∀ (r : R) (a : A), self.toFun (r a) = r self.toFun a

                                                                    By definition, a ⋆-algebra equivalence commutes with the action of scalars.

                                                                  Instances For

                                                                    A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar multiplication and the star operation, which allows for considering both unital and non-unital equivalences with a single structure. Currently, AlgEquiv requires unital algebras, which is why this structure does not extend it.

                                                                    Equations
                                                                    Instances For

                                                                      A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar multiplication and the star operation, which allows for considering both unital and non-unital equivalences with a single structure. Currently, AlgEquiv requires unital algebras, which is why this structure does not extend it.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        class NonUnitalAlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Add A] [Mul A] [SMul R A] [Add B] [Mul B] [SMul R B] [EquivLike F A B] extends RingEquivClass , SMulHomClass :

                                                                        The class that directly extends RingEquivClass and SMulHomClass.

                                                                        Mostly an implementation detail for StarAlgEquivClass.

                                                                          Instances
                                                                            class StarAlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] :

                                                                            StarAlgEquivClass F R A B asserts F is a type of bundled ⋆-algebra equivalences between A and B.

                                                                            You should also extend this typeclass when you extend StarAlgEquiv.

                                                                            • map_star : ∀ (f : F) (a : A), f (star a) = star (f a)

                                                                              By definition, a ⋆-algebra equivalence preserves the star operation.

                                                                            Instances
                                                                              instance StarAlgEquivClass.instStarHomClassToFunLike {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} :
                                                                              ∀ {x : Add A} {x_1 : Mul A} [inst : SMul R A] {x_2 : Star A} {x_3 : Add B} {x_4 : Mul B} [inst_1 : SMul R B] {x_5 : Star B} [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B] [hF : StarAlgEquivClass F R A B], StarHomClass F A B
                                                                              Equations
                                                                              • =
                                                                              instance StarAlgEquivClass.instNonUnitalAlgHomClassToFunLike {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} :
                                                                              ∀ {x : Monoid R} {x_1 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A] {x_2 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction R B] [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B], NonUnitalAlgHomClass F R A B
                                                                              Equations
                                                                              • =
                                                                              instance StarAlgEquivClass.instNonUnitalStarAlgHomClassToFunLikeInstNonUnitalAlgHomClassToFunLike {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} :
                                                                              ∀ {x : Monoid R} {x_1 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A] {x_2 : Star A} {x_3 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction R B] {x_4 : Star B} [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B] [inst_4 : StarAlgEquivClass F R A B], NonUnitalStarAlgHomClass F R A B
                                                                              Equations
                                                                              • =
                                                                              instance StarAlgEquivClass.instAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) :
                                                                              ∀ {x : CommSemiring R} {x_1 : Semiring A} [inst : Algebra R A] {x_2 : Semiring B} [inst_1 : Algebra R B] [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B], AlgEquivClass F R A B
                                                                              Equations
                                                                              • =
                                                                              instance StarAlgEquivClass.instStarAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) :
                                                                              ∀ {x : CommSemiring R} {x_1 : Semiring A} [inst : Algebra R A] {x_2 : Star A} {x_3 : Semiring B} [inst_1 : Algebra R B] {x_4 : Star B} [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B] [inst_4 : StarAlgEquivClass F R A B], StarAlgHomClass F R A B
                                                                              Equations
                                                                              • =
                                                                              def StarAlgEquivClass.toStarAlgEquiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarAlgEquivClass F R A B] (f : F) :

                                                                              Turn an element of a type F satisfying StarAlgEquivClass F R A B into an actual StarAlgEquiv. This is declared as the default coercion from F to A ≃⋆ₐ[R] B.

                                                                              Equations
                                                                              • f = let __src := f; { toRingEquiv := __src, map_star' := , map_smul' := }
                                                                              Instances For
                                                                                instance StarAlgEquivClass.instCoeHead {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarAlgEquivClass F R A B] :

                                                                                Any type satisfying StarAlgEquivClass can be cast into StarAlgEquiv via StarAlgEquivClass.toStarAlgEquiv.

                                                                                Equations
                                                                                • StarAlgEquivClass.instCoeHead = { coe := StarAlgEquivClass.toStarAlgEquiv }
                                                                                instance StarAlgEquiv.instEquivLikeStarAlgEquiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] :
                                                                                Equations
                                                                                • StarAlgEquiv.instEquivLikeStarAlgEquiv = { coe := fun (f : A ≃⋆ₐ[R] B) => f.toFun, inv := fun (f : A ≃⋆ₐ[R] B) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                                                                                instance StarAlgEquiv.instNonUnitalAlgEquivClassStarAlgEquivInstEquivLikeStarAlgEquiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] :
                                                                                Equations
                                                                                • =
                                                                                instance StarAlgEquiv.instFunLikeStarAlgEquiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] :
                                                                                FunLike (A ≃⋆ₐ[R] B) A B

                                                                                Helper instance for cases where the inference via EquivLike is too hard.

                                                                                Equations
                                                                                • StarAlgEquiv.instFunLikeStarAlgEquiv = { coe := fun (f : A ≃⋆ₐ[R] B) => f.toFun, coe_injective' := }
                                                                                @[simp]
                                                                                theorem StarAlgEquiv.toRingEquiv_eq_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                e.toRingEquiv = e
                                                                                theorem StarAlgEquiv.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] {f : A ≃⋆ₐ[R] B} {g : A ≃⋆ₐ[R] B} (h : ∀ (a : A), f a = g a) :
                                                                                f = g
                                                                                theorem StarAlgEquiv.ext_iff {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] {f : A ≃⋆ₐ[R] B} {g : A ≃⋆ₐ[R] B} :
                                                                                f = g ∀ (a : A), f a = g a
                                                                                def StarAlgEquiv.refl {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :

                                                                                Star algebra equivalences are reflexive.

                                                                                Equations
                                                                                • StarAlgEquiv.refl = let __src := RingEquiv.refl A; { toRingEquiv := __src, map_star' := , map_smul' := }
                                                                                Instances For
                                                                                  instance StarAlgEquiv.instInhabitedStarAlgEquiv {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :
                                                                                  Equations
                                                                                  • StarAlgEquiv.instInhabitedStarAlgEquiv = { default := StarAlgEquiv.refl }
                                                                                  @[simp]
                                                                                  theorem StarAlgEquiv.coe_refl {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :
                                                                                  StarAlgEquiv.refl = id
                                                                                  def StarAlgEquiv.symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :

                                                                                  Star algebra equivalences are symmetric.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def StarAlgEquiv.Simps.apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                    AB

                                                                                    See Note [custom simps projection]

                                                                                    Equations
                                                                                    Instances For
                                                                                      def StarAlgEquiv.Simps.symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                      BA

                                                                                      See Note [custom simps projection]

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem StarAlgEquiv.invFun_eq_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] {e : A ≃⋆ₐ[R] B} :
                                                                                        @[simp]
                                                                                        theorem StarAlgEquiv.symm_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                        theorem StarAlgEquiv.symm_bijective {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] :
                                                                                        Function.Bijective StarAlgEquiv.symm
                                                                                        @[simp]
                                                                                        theorem StarAlgEquiv.mk_coe' {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) (f : BA) (h₁ : Function.LeftInverse (e) f) (h₂ : Function.RightInverse (e) f) (h₃ : ∀ (x y : B), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : B), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (a : B), { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : B), { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun (r a) = r { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun a) :
                                                                                        { toRingEquiv := { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }, map_star' := h₅, map_smul' := h₆ } = StarAlgEquiv.symm e
                                                                                        @[simp]
                                                                                        theorem StarAlgEquiv.symm_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (f : AB) (f' : BA) (h₁ : Function.LeftInverse f' f) (h₂ : Function.RightInverse f' f) (h₃ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (a : A), { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : A), { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun (r a) = r { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toFun a) :
                                                                                        StarAlgEquiv.symm { toRingEquiv := { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }, map_star' := h₅, map_smul' := h₆ } = let __src := StarAlgEquiv.symm { toRingEquiv := { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }, map_star' := h₅, map_smul' := h₆ }; { toRingEquiv := { toEquiv := { toFun := f', invFun := f, left_inv := , right_inv := }, map_mul' := , map_add' := }, map_star' := , map_smul' := }
                                                                                        @[simp]
                                                                                        theorem StarAlgEquiv.refl_symm {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :
                                                                                        StarAlgEquiv.symm StarAlgEquiv.refl = StarAlgEquiv.refl
                                                                                        theorem StarAlgEquiv.to_ringEquiv_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) :
                                                                                        @[simp]
                                                                                        theorem StarAlgEquiv.symm_to_ringEquiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                        def StarAlgEquiv.trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) :

                                                                                        Star algebra equivalences are transitive.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.apply_symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) (x : B) :
                                                                                          e ((StarAlgEquiv.symm e) x) = x
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.symm_apply_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) (x : A) :
                                                                                          (StarAlgEquiv.symm e) (e x) = x
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.symm_trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : C) :
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.coe_trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) :
                                                                                          (StarAlgEquiv.trans e₁ e₂) = e₂ e₁
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : A) :
                                                                                          (StarAlgEquiv.trans e₁ e₂) x = e₂ (e₁ x)
                                                                                          theorem StarAlgEquiv.leftInverse_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                          theorem StarAlgEquiv.rightInverse_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) :
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.ofStarAlgHom_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] [FunLike G B A] (f : F) (g : G) (h₁ : ∀ (x : A), g (f x) = x) (h₂ : ∀ (x : B), f (g x) = x) (a : A) :
                                                                                          (StarAlgEquiv.ofStarAlgHom f g h₁ h₂) a = f a
                                                                                          @[simp]
                                                                                          theorem StarAlgEquiv.ofStarAlgHom_symm_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] [FunLike G B A] (f : F) (g : G) (h₁ : ∀ (x : A), g (f x) = x) (h₂ : ∀ (x : B), f (g x) = x) (a : B) :
                                                                                          def StarAlgEquiv.ofStarAlgHom {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] [FunLike G B A] (f : F) (g : G) (h₁ : ∀ (x : A), g (f x) = x) (h₂ : ∀ (x : B), f (g x) = x) :

                                                                                          If a (unital or non-unital) star algebra morphism has an inverse, it is an isomorphism of star algebras.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            noncomputable def StarAlgEquiv.ofBijective {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] (f : F) (hf : Function.Bijective f) :

                                                                                            Promote a bijective star algebra homomorphism to a star algebra equivalence.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem StarAlgEquiv.coe_ofBijective {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {f : F} (hf : Function.Bijective f) :
                                                                                              theorem StarAlgEquiv.ofBijective_apply {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {f : F} (hf : Function.Bijective f) (a : A) :