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 A →ₙₐ[R] B :
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.

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

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

            Equations
              Instances For

                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] [StarHomClass F A B] (f : F) :
                    f = 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 g : A →⋆ₙₐ[R] B} (h : ∀ (x : A), f x = g x) :
                    f = g
                    theorem NonUnitalStarAlgHom.ext_iff {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 g : A →⋆ₙₐ[R] B} :
                    f = g ∀ (x : A), f x = g x
                    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
                      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
                              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]
                                @[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

                                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
                                    @[simp]

                                    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 A →ₐ[R] B :
                                    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.

                                    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
                                            Instances For
                                              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] [StarHomClass F A B] (f : F) :

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

                                              Equations
                                                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] [StarHomClass F 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
                                                      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] :
                                                      instance StarAlgHom.instStarHomClass {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] :
                                                      @[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] [StarHomClass F 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 g : A →⋆ₐ[R] B} (h : ∀ (x : A), f x = g x) :
                                                          f = g
                                                          theorem StarAlgHom.ext_iff {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 g : A →⋆ₐ[R] B} :
                                                          f = g ∀ (x : A), f x = g x
                                                          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
                                                            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
                                                                  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
                                                                    Instances For
                                                                      @[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) :
                                                                      (ofId R A) a = (algebraMap R A) a
                                                                      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
                                                                          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
                                                                              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
                                                                                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.

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

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[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) :
                                                                                      (fst R A B) self = self.1

                                                                                      The second 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) :
                                                                                          (snd R A B) self = self.2

                                                                                          The Pi.prod of two morphisms is a morphism.

                                                                                          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)
                                                                                              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) :
                                                                                              (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) :
                                                                                              (snd R B C).comp (f.prod g) = g
                                                                                              @[simp]
                                                                                              theorem NonUnitalStarAlgHom.prod_fst_snd {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] :
                                                                                              (fst R A B).prod (snd R A B) = 1

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

                                                                                              Equations
                                                                                                Instances For
                                                                                                  def Pi.evalNonUnitalStarAlgHom {ι : Type u_1} (R : Type u_2) (A : ιType u_3) (j : ι) [Monoid R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → DistribMulAction R (A i)] [(i : ι) → Star (A i)] :
                                                                                                  ((i : ι) → A i) →⋆ₙₐ[R] A j

                                                                                                  Function.eval as a NonUnitalStarAlgHom.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem Pi.evalNonUnitalStarAlgHom_apply {ι : Type u_1} (R : Type u_2) (A : ιType u_3) (j : ι) [Monoid R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → DistribMulAction R (A i)] [(i : ι) → Star (A i)] (a✝ : (i : ι) → A i) :
                                                                                                      (evalNonUnitalStarAlgHom R A j) a✝ = (evalMulHom A j).toFun a✝
                                                                                                      def Pi.evalStarAlgHom {ι : Type u_1} (R : Type u_2) (A : ιType u_3) (j : ι) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → Star (A i)] :
                                                                                                      ((i : ι) → A i) →⋆ₐ[R] A j

                                                                                                      Function.eval as a StarAlgHom.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem Pi.evalStarAlgHom_apply {ι : Type u_1} (R : Type u_2) (A : ιType u_3) (j : ι) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → Star (A i)] (a✝ : (i : ι) → A i) :
                                                                                                          (evalStarAlgHom R A j) a✝ = (evalNonUnitalStarAlgHom R A j).toFun a✝

                                                                                                          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]
                                                                                                                  theorem NonUnitalStarAlgHom.coe_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] :
                                                                                                                  (inl R A B) = fun (x : A) => (x, 0)
                                                                                                                  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.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) :
                                                                                                                      (fst R A B) self = self.1
                                                                                                                      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.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) :
                                                                                                                          (snd R A B) self = self.2
                                                                                                                          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
                                                                                                                              @[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)
                                                                                                                              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) :
                                                                                                                              (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) :
                                                                                                                              (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] :
                                                                                                                              (fst R A B).prod (snd R A B) = 1
                                                                                                                              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
                                                                                                                                Instances For
                                                                                                                                  @[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)) :
                                                                                                                                  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) :
                                                                                                                                  prodEquiv.symm f = ((fst R B C).comp f, (snd R B C).comp f)

                                                                                                                                  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 A ≃+* B :
                                                                                                                                  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.

                                                                                                                                  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
                                                                                                                                          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 F A B, MulActionSemiHomClass F id A B :

                                                                                                                                            The class that directly extends RingEquivClass and SMulHomClass.

                                                                                                                                            Mostly an implementation detail for StarAlgEquivClass.

                                                                                                                                            Instances
                                                                                                                                              @[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] :
                                                                                                                                              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] [StarHomClass F A B] (f : F) :

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

                                                                                                                                              Equations
                                                                                                                                                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] [StarHomClass F A B] :

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

                                                                                                                                                  Equations
                                                                                                                                                    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
                                                                                                                                                      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] :
                                                                                                                                                      instance StarAlgEquiv.instStarHomClass {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] :
                                                                                                                                                      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
                                                                                                                                                        @[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 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 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
                                                                                                                                                          Instances For
                                                                                                                                                            instance StarAlgEquiv.instInhabited {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :
                                                                                                                                                            Equations
                                                                                                                                                              @[simp]
                                                                                                                                                              theorem StarAlgEquiv.coe_refl {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :
                                                                                                                                                              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
                                                                                                                                                                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) :
                                                                                                                                                                          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] :
                                                                                                                                                                          @[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) :

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

                                                                                                                                                                          Equations
                                                                                                                                                                            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 := 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] :
                                                                                                                                                                              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
                                                                                                                                                                                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) :
                                                                                                                                                                                  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) :
                                                                                                                                                                                  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] [StarHomClass F 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
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[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] [StarHomClass F 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) :
                                                                                                                                                                                      (ofStarAlgHom f g h₁ h₂).symm a = g a
                                                                                                                                                                                      @[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] [StarHomClass F 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) :
                                                                                                                                                                                      (ofStarAlgHom f g h₁ h₂) a = f a
                                                                                                                                                                                      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] [StarHomClass F A B] (f : F) (hf : Function.Bijective f) :

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

                                                                                                                                                                                      Equations
                                                                                                                                                                                        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] [StarHomClass F A B] {f : F} (hf : Function.Bijective f) :
                                                                                                                                                                                          (ofBijective f hf) = 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] [StarHomClass F A B] {f : F} (hf : Function.Bijective f) (a : A) :
                                                                                                                                                                                          (ofBijective f hf) a = f a