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) = (MonoidHom.id R) 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
    theorem NonUnitalStarAlgHom.map_star' {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 →⋆ₙₐ[R] B) (a : A) :
    self.toFun (star a) = star (self.toFun a)

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

    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
            Instances For
              Equations
              • NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHom = { coe := NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom }
              Equations
              • NonUnitalStarAlgHom.instFunLike = { 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
                • f.copy f' h = { toFun := f', map_smul' := , map_zero' := , map_add' := , map_mul' := , map_star' := }
                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) :
                  (f.copy f' h) = 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) :
                  f.copy f' 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 : AB) (h₁ : ∀ (m : R) (x : A), f (m x) = (MonoidHom.id R) 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), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) (h₅ : ∀ (a : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) = star ({ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)) :
                  { 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) = (MonoidHom.id R) 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), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) (h₅ : ∀ (a : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) = star ({ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)) :
                  { 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
                    • f.comp g = let __src := f.comp g.toNonUnitalAlgHom; { toNonUnitalAlgHom := __src, map_star' := }
                    Instances For
                      @[simp]
                      theorem NonUnitalStarAlgHom.coe_comp {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 : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) :
                      (f.comp g) = f g
                      @[simp]
                      theorem NonUnitalStarAlgHom.comp_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 : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) (a : A) :
                      (f.comp g) a = f (g a)
                      @[simp]
                      theorem NonUnitalStarAlgHom.comp_assoc {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] [NonUnitalNonAssocSemiring D] [DistribMulAction R D] [Star D] (f : C →⋆ₙₐ[R] D) (g : B →⋆ₙₐ[R] C) (h : A →⋆ₙₐ[R] B) :
                      (f.comp g).comp h = f.comp (g.comp h)
                      Equations
                      • NonUnitalStarAlgHom.instMonoid = 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.instZero = { zero := let __src := 0; { toNonUnitalAlgHom := __src, map_star' := } }
                      Equations
                      • NonUnitalStarAlgHom.instInhabited = { default := 0 }
                      Equations

                      If a monoid R acts on another monoid S, then a non-unital star algebra homomorphism over S can be viewed as a non-unital star algebra homomorphism over R.

                      Equations
                      Instances For

                        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.toRingHom).toFun 1 = 1
                        • map_mul' : ∀ (x y : A), (self.toRingHom).toFun (x * y) = (self.toRingHom).toFun x * (self.toRingHom).toFun y
                        • map_zero' : (self.toRingHom).toFun 0 = 0
                        • map_add' : ∀ (x y : A), (self.toRingHom).toFun (x + y) = (self.toRingHom).toFun x + (self.toRingHom).toFun y
                        • commutes' : ∀ (r : R), (self.toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r
                        • map_star' : ∀ (x : A), (self.toRingHom).toFun (star x) = star ((self.toRingHom).toFun x)

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

                        Instances For
                          theorem StarAlgHom.map_star' {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 →⋆ₐ[R] B) (x : A) :
                          (self.toRingHom).toFun (star x) = star ((self.toRingHom).toFun x)

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

                          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 100]
                                  instance StarAlgHomClass.toNonUnitalStarAlgHomClass (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
                                  • =
                                  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.instFunLike {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.instFunLike = { coe := fun (f : A →⋆ₐ[R] B) => (f.toRingHom).toFun, coe_injective' := }
                                    instance StarAlgHom.instAlgHomClass {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
                                    • =
                                    instance StarAlgHom.instStarAlgHomClass {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
                                      • f.copy f' h = { toFun := f', map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := , map_star' := }
                                      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) :
                                        (f.copy 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) :
                                        f.copy f' 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 : 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₃ : ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), ({ 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), ({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun (star x) = star (({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun x)) :
                                        { 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.toRingHom).toFun (star x) = star ((f.toRingHom).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₃ : ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), ({ 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), ({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun (star x) = star (({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun x)) :
                                        { 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
                                          • StarAlgHom.ofId R A = let __src := Algebra.ofId R A; { toFun := (algebraMap R A), map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := , map_star' := }
                                          Instances For
                                            instance StarAlgHom.instInhabited {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
                                            • f.comp g = let __src := f.comp g.toAlgHom; { toAlgHom := __src, map_star' := }
                                            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) :
                                              (f.comp 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) :
                                              (f.comp 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) :
                                              (f.comp g).comp h = f.comp (g.comp h)
                                              @[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) :
                                              (StarAlgHom.id R B).comp f = f
                                              @[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) :
                                              f.comp (StarAlgHom.id R A) = f
                                              instance StarAlgHom.instMonoid {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :
                                              Equations
                                              • StarAlgHom.instMonoid = 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
                                              • f.toNonUnitalStarAlgHom = { toFun := (f.toRingHom).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := , map_star' := }
                                              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) :
                                                f.toNonUnitalStarAlgHom = f

                                                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) :
                                                    (f.prod g) i = (f i, g i)

                                                    The Pi.prod of two morphisms is a morphism.

                                                    Equations
                                                    • f.prod g = let __src := f.prod g.toNonUnitalAlgHom; { toNonUnitalAlgHom := __src, map_star' := }
                                                    Instances For
                                                      theorem NonUnitalStarAlgHom.coe_prod {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) :
                                                      (f.prod g) = Pi.prod f g
                                                      @[simp]
                                                      theorem NonUnitalStarAlgHom.fst_prod {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) :
                                                      (NonUnitalStarAlgHom.fst R B C).comp (f.prod g) = f
                                                      @[simp]
                                                      theorem NonUnitalStarAlgHom.snd_prod {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) :
                                                      (NonUnitalStarAlgHom.snd R B C).comp (f.prod g) = g
                                                      @[simp]
                                                      theorem NonUnitalStarAlgHom.prodEquiv_symm_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 × C) :
                                                      NonUnitalStarAlgHom.prodEquiv.symm f = ((NonUnitalStarAlgHom.fst R B C).comp f, (NonUnitalStarAlgHom.snd R B C).comp f)
                                                      @[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 = f.1.prod 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) :
                                                                (f.prod 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
                                                                • f.prod g = let __src := f.prod g.toAlgHom; { toAlgHom := __src, map_star' := }
                                                                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) :
                                                                  (f.prod 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) :
                                                                  (StarAlgHom.fst R B C).comp (f.prod g) = f
                                                                  @[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) :
                                                                  (StarAlgHom.snd R B C).comp (f.prod g) = g
                                                                  @[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] :
                                                                  (StarAlgHom.fst R A B).prod (StarAlgHom.snd R A B) = 1
                                                                  @[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 = f.1.prod f.2
                                                                  @[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.fst R B C).comp f, (StarAlgHom.snd R B C).comp f)
                                                                  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
                                                                      theorem StarAlgEquiv.map_star' {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] (self : A ≃⋆ₐ[R] B) (a : A) :
                                                                      self.toFun (star a) = star (self.toFun a)

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

                                                                      theorem StarAlgEquiv.map_smul' {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] (self : A ≃⋆ₐ[R] B) (r : R) (a : A) :
                                                                      self.toFun (r a) = r self.toFun a

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

                                                                      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 , MulActionSemiHomClass :

                                                                          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
                                                                                theorem StarAlgEquivClass.map_star {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] [self : StarAlgEquivClass F R A B] (f : F) (a : A) :
                                                                                f (star a) = star (f a)

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

                                                                                @[instance 50]
                                                                                instance StarAlgEquivClass.instStarHomClass {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] [hF : StarAlgEquivClass F R A B] :
                                                                                Equations
                                                                                • =
                                                                                @[instance 100]
                                                                                Equations
                                                                                • =
                                                                                @[instance 100]
                                                                                instance StarAlgEquivClass.instAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] :
                                                                                Equations
                                                                                • =
                                                                                @[instance 100]
                                                                                instance StarAlgEquivClass.instStarAlgHomClass (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] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarAlgEquivClass 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.instEquivLike {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.instEquivLike = { coe := fun (f : A ≃⋆ₐ[R] B) => f.toFun, inv := fun (f : A ≃⋆ₐ[R] B) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                                                                                  instance StarAlgEquiv.instNonUnitalAlgEquivClass {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.instStarAlgEquivClass {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.instFunLike {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.instFunLike = { 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] :

                                                                                  The identity map is a star algebra isomorphism.

                                                                                  Equations
                                                                                  • StarAlgEquiv.refl = let __src := RingEquiv.refl A; { toRingEquiv := __src, map_star' := , map_smul' := }
                                                                                  Instances For
                                                                                    instance StarAlgEquiv.instInhabited {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :
                                                                                    Equations
                                                                                    • StarAlgEquiv.instInhabited = { 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) :

                                                                                    The inverse of a star algebra isomorphism is a star algebra isomorphism.

                                                                                    Equations
                                                                                    • e.symm = let __src := e.symm; { toRingEquiv := __src, map_star' := , map_smul' := }
                                                                                    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} :
                                                                                          EquivLike.inv e = e.symm
                                                                                          @[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) :
                                                                                          e.symm.symm = e
                                                                                          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.coe_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] (e : A ≃+* B) (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)) (h₂ : ∀ (r : R) (a : A), e.toFun (r a) = r e.toFun a) :
                                                                                          { toRingEquiv := e, map_star' := h₁, map_smul' := h₂ } = e
                                                                                          @[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) (e' : BA) (h₁ : Function.LeftInverse e' e) (h₂ : Function.RightInverse e' e) (h₃ : ∀ (x y : A), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (a : A), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : A), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r a) = r { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a) :
                                                                                          { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ } = e
                                                                                          def StarAlgEquiv.symm_mk.aux {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), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r a) = r { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a) :

                                                                                          Auxilliary definition to avoid looping in dsimp with StarAlgEquiv.symm_mk.

                                                                                          Equations
                                                                                          • StarAlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ h₆ = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ }.symm
                                                                                          Instances For
                                                                                            @[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), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r a) = r { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a) :
                                                                                            { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ }.symm = let __src := StarAlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ h₆; { 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.refl.symm = 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) :
                                                                                            (f).symm = f.symm
                                                                                            @[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) :
                                                                                            e.symm = (e).symm
                                                                                            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) :

                                                                                            Transitivity of StarAlgEquiv.

                                                                                            Equations
                                                                                            • e₁.trans e₂ = let __src := e₁.trans e₂.toRingEquiv; { toRingEquiv := __src, map_star' := , map_smul' := }
                                                                                            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 (e.symm 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) :
                                                                                              e.symm (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) :
                                                                                              (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
                                                                                              @[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) :
                                                                                              (e₁.trans 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) :
                                                                                              (e₁.trans 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) :
                                                                                              Function.LeftInverse e.symm e
                                                                                              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) :
                                                                                              Function.RightInverse e.symm e
                                                                                              @[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) :
                                                                                              (StarAlgEquiv.ofStarAlgHom f g h₁ h₂).symm a = g a
                                                                                              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
                                                                                              • StarAlgEquiv.ofStarAlgHom f g h₁ h₂ = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂, map_mul' := , map_add' := , map_star' := , map_smul' := }
                                                                                              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) :