Documentation

Mathlib.Algebra.Star.StarRingHom

Morphisms of star rings #

This file defines a new type of morphism between (non-unital) rings A and B where both A and B are equipped with a star operation. This morphism, namely NonUnitalStarRingHom, is a direct extension of its non-starred counterpart with a field map_star which guarantees it preserves the star operation.

As with NonUnitalRingHom, the multiplications are not assumed to be associative or unital.

Main definitions #

Implementation #

This file is heavily inspired by Mathlib.Algebra.Star.StarAlgHom.

Tags #

non-unital, ring, morphism, star

Non-unital star ring homomorphisms #

structure NonUnitalStarRingHom (A : Type u_1) (B : Type u_2) [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] extends NonUnitalRingHom :
Type (max u_1 u_2)

A non-unital ⋆-ring homomorphism is a non-unital ring homomorphism between non-unital non-associative semirings A and B equipped with a star operation, and this homomorphism is also star-preserving.

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

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

Instances For
    theorem NonUnitalStarRingHom.map_star' {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (self : A →⋆ₙ+* B) (a : A) :
    self.toFun (star a) = star (self.toFun a)

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

    α →⋆ₙ+* β denotes the type of non-unital ring homomorphisms from α to β.

    Equations
    Instances For

      NonUnitalStarRingHomClass F A B states that F is a type of non-unital ⋆-ring homomorphisms. You should also extend this typeclass when you extend NonUnitalStarRingHom.

        Instances

          Turn an element of a type F satisfying NonUnitalStarRingHomClass F A B into an actual NonUnitalStarRingHom. This is declared as the default coercion from F to A →⋆ₙ+ B.

          Equations
          • f = let __src := f; { toNonUnitalRingHom := __src, map_star' := }
          Instances For
            Equations
            • NonUnitalStarRingHomClass.instCoeHeadNonUnitalStarRingHom = { coe := NonUnitalStarRingHomClass.toNonUnitalStarRingHom }
            Equations
            • NonUnitalStarRingHom.instFunLike = { coe := fun (f : A →⋆ₙ+* B) => f.toFun, coe_injective' := }

            See Note [custom simps projection]

            Equations
            Instances For
              @[simp]
              theorem NonUnitalStarRingHom.coe_coe {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] {F : Type u_5} [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass F A B] (f : F) :
              f = f
              @[simp]
              theorem NonUnitalStarRingHom.coe_toNonUnitalRingHom {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) :
              f.toNonUnitalRingHom = f
              theorem NonUnitalStarRingHom.ext {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] {f : A →⋆ₙ+* B} {g : A →⋆ₙ+* B} (h : ∀ (x : A), f x = g x) :
              f = g
              def NonUnitalStarRingHom.copy {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) (f' : AB) (h : f' = f) :

              Copy of a NonUnitalStarRingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

              Equations
              • f.copy f' h = { toFun := f', map_mul' := , map_zero' := , map_add' := , map_star' := }
              Instances For
                @[simp]
                theorem NonUnitalStarRingHom.coe_copy {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) (f' : AB) (h : f' = f) :
                (f.copy f' h) = f'
                theorem NonUnitalStarRingHom.copy_eq {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) (f' : AB) (h : f' = f) :
                f.copy f' h = f
                @[simp]
                theorem NonUnitalStarRingHom.coe_mk {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →ₙ+* B) (h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)) :
                { toNonUnitalRingHom := f, map_star' := h } = f
                @[simp]
                theorem NonUnitalStarRingHom.mk_coe {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) (h₁ : ∀ (x y : A), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) (h₄ : ∀ (a : A), { toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) = star ({ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)) :
                { toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } = f

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

                Equations
                Instances For

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

                  Equations
                  • f.comp g = let __src := f.comp g.toNonUnitalRingHom; { toNonUnitalRingHom := __src, map_star' := }
                  Instances For
                    @[simp]
                    theorem NonUnitalStarRingHom.coe_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [NonUnitalNonAssocSemiring C] [Star C] (f : B →⋆ₙ+* C) (g : A →⋆ₙ+* B) :
                    (f.comp g) = f g
                    @[simp]
                    theorem NonUnitalStarRingHom.comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [NonUnitalNonAssocSemiring C] [Star C] (f : B →⋆ₙ+* C) (g : A →⋆ₙ+* B) (a : A) :
                    (f.comp g) a = f (g a)
                    @[simp]
                    theorem NonUnitalStarRingHom.comp_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [NonUnitalNonAssocSemiring C] [Star C] [NonUnitalNonAssocSemiring D] [Star D] (f : C →⋆ₙ+* D) (g : B →⋆ₙ+* C) (h : A →⋆ₙ+* B) :
                    (f.comp g).comp h = f.comp (g.comp h)
                    Equations
                    • NonUnitalStarRingHom.instMonoid = Monoid.mk npowRec
                    @[simp]
                    Equations
                    • NonUnitalStarRingHom.instZero = { zero := let __src := 0; { toNonUnitalRingHom := __src, map_star' := } }
                    Equations
                    • NonUnitalStarRingHom.instInhabited = { default := 0 }
                    Equations

                    Star ring equivalences #

                    structure StarRingEquiv (A : Type u_1) (B : Type u_2) [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] extends RingEquiv :
                    Type (max u_1 u_2)

                    A ⋆-ring equivalence is an equivalence preserving addition, multiplication, and the star operation, which allows for considering both unital and non-unital equivalences with a single structure.

                    • 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 ⋆-ring equivalence preserves the star operation.

                    Instances For
                      theorem StarRingEquiv.map_star' {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (self : A ≃⋆+* B) (a : A) :
                      self.toFun (star a) = star (self.toFun a)

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

                      A ⋆-ring equivalence is an equivalence preserving addition, multiplication, and the star operation, which allows for considering both unital and non-unital equivalences with a single structure.

                      Equations
                      Instances For
                        class StarRingEquivClass (F : Type u_1) (A : outParam (Type u_2)) (B : outParam (Type u_3)) [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B] [EquivLike F A B] extends RingEquivClass :

                        StarRingEquivClass F A B asserts F is a type of bundled ⋆-ring equivalences between A and B. You should also extend this typeclass when you extend StarRingEquiv.

                        • map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b
                        • map_add : ∀ (f : F) (a b : A), f (a + b) = f a + f b
                        • map_star : ∀ (f : F) (a : A), f (star a) = star (f a)

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

                        Instances
                          theorem StarRingEquivClass.map_star {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B] [EquivLike F A B] [self : StarRingEquivClass F A B] (f : F) (a : A) :
                          f (star a) = star (f a)

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

                          @[instance 50]
                          instance StarRingEquivClass.instStarHomClass {F : Type u_1} {A : Type u_2} {B : Type u_3} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B] [EquivLike F A B] [hF : StarRingEquivClass F A B] :
                          Equations
                          • =
                          @[instance 100]
                          Equations
                          • =
                          def StarRingEquivClass.toStarRingEquiv {F : Type u_1} {A : Type u_2} {B : Type u_3} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B] [EquivLike F A B] [RingEquivClass F A B] [StarRingEquivClass F A B] (f : F) :

                          Turn an element of a type F satisfying StarRingEquivClass F A B into an actual StarRingEquiv. This is declared as the default coercion from F to A ≃⋆+* B.

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

                            Any type satisfying StarRingEquivClass can be cast into StarRingEquiv via StarRingEquivClass.toStarRingEquiv.

                            Equations
                            • StarRingEquivClass.instCoeHead = { coe := StarRingEquivClass.toStarRingEquiv }
                            instance StarRingEquiv.instEquivLike {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
                            Equations
                            • StarRingEquiv.instEquivLike = { coe := fun (f : A ≃⋆+* B) => f.toFun, inv := fun (f : A ≃⋆+* B) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                            instance StarRingEquiv.instRingEquivClass {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
                            Equations
                            • =
                            instance StarRingEquiv.instStarRingEquivClass {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
                            Equations
                            • =
                            instance StarRingEquiv.instFunLike {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
                            FunLike (A ≃⋆+* B) A B

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

                            Equations
                            • StarRingEquiv.instFunLike = { coe := fun (f : A ≃⋆+* B) => f.toFun, coe_injective' := }
                            @[simp]
                            theorem StarRingEquiv.toRingEquiv_eq_coe {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :
                            e.toRingEquiv = e
                            theorem StarRingEquiv.ext {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] {f : A ≃⋆+* B} {g : A ≃⋆+* B} (h : ∀ (a : A), f a = g a) :
                            f = g
                            theorem StarRingEquiv.ext_iff {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] {f : A ≃⋆+* B} {g : A ≃⋆+* B} :
                            f = g ∀ (a : A), f a = g a
                            def StarRingEquiv.refl {A : Type u_1} [Add A] [Mul A] [Star A] :

                            The identity map as a star ring isomorphism.

                            Equations
                            • StarRingEquiv.refl = let __src := RingEquiv.refl A; { toRingEquiv := __src, map_star' := }
                            Instances For
                              instance StarRingEquiv.instInhabited {A : Type u_1} [Add A] [Mul A] [Star A] :
                              Equations
                              • StarRingEquiv.instInhabited = { default := StarRingEquiv.refl }
                              @[simp]
                              theorem StarRingEquiv.coe_refl {A : Type u_1} [Add A] [Mul A] [Star A] :
                              StarRingEquiv.refl = id
                              def StarRingEquiv.symm {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :

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

                              Equations
                              • e.symm = let __src := e.symm; { toRingEquiv := __src, map_star' := }
                              Instances For
                                def StarRingEquiv.Simps.apply {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :
                                AB

                                See Note [custom simps projection]

                                Equations
                                Instances For
                                  def StarRingEquiv.Simps.symm_apply {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :
                                  BA

                                  See Note [custom simps projection]

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem StarRingEquiv.invFun_eq_symm {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] {e : A ≃⋆+* B} :
                                    EquivLike.inv e = e.symm
                                    @[simp]
                                    theorem StarRingEquiv.symm_symm {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :
                                    e.symm.symm = e
                                    theorem StarRingEquiv.symm_bijective {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
                                    Function.Bijective StarRingEquiv.symm
                                    theorem StarRingEquiv.coe_mk {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃+* B) (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)) :
                                    { toRingEquiv := e, map_star' := h₁ } = e
                                    @[simp]
                                    theorem StarRingEquiv.mk_coe {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* 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)) :
                                    { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ } = e
                                    def StarRingEquiv.symm_mk.aux {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul 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)) :

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

                                    Equations
                                    • StarRingEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ }.symm
                                    Instances For
                                      @[simp]
                                      theorem StarRingEquiv.symm_mk {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul 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)) :
                                      { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ }.symm = let __src := StarRingEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅; { toFun := f', invFun := f, left_inv := , right_inv := , map_mul' := , map_add' := , map_star' := }
                                      @[simp]
                                      theorem StarRingEquiv.refl_symm {A : Type u_1} [Add A] [Mul A] [Star A] :
                                      StarRingEquiv.refl.symm = StarRingEquiv.refl
                                      def StarRingEquiv.trans {A : Type u_1} {B : Type u_2} {C : Type u_3} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] [Add C] [Mul C] [Star C] (e₁ : A ≃⋆+* B) (e₂ : B ≃⋆+* C) :

                                      Transitivity of StarRingEquiv.

                                      Equations
                                      • e₁.trans e₂ = let __src := e₁.trans e₂.toRingEquiv; { toRingEquiv := __src, map_star' := }
                                      Instances For
                                        @[simp]
                                        theorem StarRingEquiv.apply_symm_apply {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) (x : B) :
                                        e (e.symm x) = x
                                        @[simp]
                                        theorem StarRingEquiv.symm_apply_apply {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) (x : A) :
                                        e.symm (e x) = x
                                        @[simp]
                                        theorem StarRingEquiv.symm_trans_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] [Add C] [Mul C] [Star C] (e₁ : A ≃⋆+* B) (e₂ : B ≃⋆+* C) (x : C) :
                                        (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
                                        @[simp]
                                        theorem StarRingEquiv.coe_trans {A : Type u_1} {B : Type u_2} {C : Type u_3} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] [Add C] [Mul C] [Star C] (e₁ : A ≃⋆+* B) (e₂ : B ≃⋆+* C) :
                                        (e₁.trans e₂) = e₂ e₁
                                        @[simp]
                                        theorem StarRingEquiv.trans_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] [Add C] [Mul C] [Star C] (e₁ : A ≃⋆+* B) (e₂ : B ≃⋆+* C) (x : A) :
                                        (e₁.trans e₂) x = e₂ (e₁ x)
                                        theorem StarRingEquiv.leftInverse_symm {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :
                                        Function.LeftInverse e.symm e
                                        theorem StarRingEquiv.rightInverse_symm {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆+* B) :
                                        Function.RightInverse e.symm e
                                        @[simp]
                                        theorem StarRingEquiv.ofStarRingHom_symm_apply {F : Type u_1} {G : Type u_2} {A : Type u_3} {B : Type u_4} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass 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) :
                                        (StarRingEquiv.ofStarRingHom f g h₁ h₂).symm a = g a
                                        @[simp]
                                        theorem StarRingEquiv.ofStarRingHom_apply {F : Type u_1} {G : Type u_2} {A : Type u_3} {B : Type u_4} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass 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) :
                                        (StarRingEquiv.ofStarRingHom f g h₁ h₂) a = f a
                                        def StarRingEquiv.ofStarRingHom {F : Type u_1} {G : Type u_2} {A : Type u_3} {B : Type u_4} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass 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 ring morphism has an inverse, it is an isomorphism of star rings.

                                        Equations
                                        • StarRingEquiv.ofStarRingHom f g h₁ h₂ = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂, map_mul' := , map_add' := , map_star' := }
                                        Instances For
                                          noncomputable def StarRingEquiv.ofBijective {F : Type u_1} {A : Type u_3} {B : Type u_4} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass F A B] (f : F) (hf : Function.Bijective f) :

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

                                          Equations
                                          Instances For
                                            @[simp]