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 #

source
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 : A → B
  • 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
source
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.

source
def «term_→⋆ₙ+*_» :
Lean.TrailingParserDescr

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

Equations
source
class NonUnitalStarRingHomClass (F : Type u_1) (A : outParam (Type u_2)) (B : outParam (Type u_3)) [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] extends StarHomClass :
Prop

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
    source
    def NonUnitalStarRingHomClass.toNonUnitalStarRingHom {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass F A B] (f : F) :
    A →⋆ₙ+* B

    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 = { toNonUnitalRingHom := ↑f, map_star' := ⋯ }
    source
    instance NonUnitalStarRingHomClass.instCoeHeadNonUnitalStarRingHom {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [FunLike F A B] [NonUnitalRingHomClass F A B] [NonUnitalStarRingHomClass F A B] :
    CoeHead F (A →⋆ₙ+* B)
    Equations
    • NonUnitalStarRingHomClass.instCoeHeadNonUnitalStarRingHom = { coe := NonUnitalStarRingHomClass.toNonUnitalStarRingHom }
    source
    instance NonUnitalStarRingHom.instFunLike {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] :
    FunLike (A →⋆ₙ+* B) A B
    Equations
    • NonUnitalStarRingHom.instFunLike = { coe := fun (f : A →⋆ₙ+* B) => f.toFun, coe_injective' := ⋯ }
    source
    instance NonUnitalStarRingHom.instNonUnitalRingHomClass {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] :
    NonUnitalRingHomClass (A →⋆ₙ+* B) A B
    Equations
    • ⋯ = ⋯
    source
    instance NonUnitalStarRingHom.instNonUnitalStarRingHomClass {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] :
    NonUnitalStarRingHomClass (A →⋆ₙ+* B) A B
    Equations
    • ⋯ = ⋯
    source
    def NonUnitalStarRingHom.Simps.apply {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) :
    A → B

    See Note [custom simps projection]

    Equations
    source
    @[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
    source
    @[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
    source
    theorem NonUnitalStarRingHom.ext_iff {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] {f : A →⋆ₙ+* B} {g : A →⋆ₙ+* B} :
    f = g ↔ ∀ (x : A), f x = g x
    source
    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
    source
    def NonUnitalStarRingHom.copy {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) (f' : A → B) (h : f' = ⇑f) :
    A →⋆ₙ+* B

    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' := ⋯ }
    source
    @[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' : A → B) (h : f' = ⇑f) :
    ⇑(f.copy f' h) = f'
    source
    theorem NonUnitalStarRingHom.copy_eq {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) (f' : A → B) (h : f' = ⇑f) :
    f.copy f' h = f
    source
    @[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
    source
    @[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
    source
    def NonUnitalStarRingHom.id (A : Type u_1) [NonUnitalNonAssocSemiring A] [Star A] :
    A →⋆ₙ+* A

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

    Equations
    source
    @[simp]
    theorem NonUnitalStarRingHom.coe_id (A : Type u_1) [NonUnitalNonAssocSemiring A] [Star A] :
    ⇑(NonUnitalStarRingHom.id A) = id
    source
    def NonUnitalStarRingHom.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) :
    A →⋆ₙ+* C

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

    Equations
    • f.comp g = { toNonUnitalRingHom := f.comp g.toNonUnitalRingHom, map_star' := ⋯ }
    source
    @[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
    source
    @[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)
    source
    @[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)
    source
    @[simp]
    theorem NonUnitalStarRingHom.id_comp {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) :
    (NonUnitalStarRingHom.id B).comp f = f
    source
    @[simp]
    theorem NonUnitalStarRingHom.comp_id {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) :
    f.comp (NonUnitalStarRingHom.id A) = f
    source
    instance NonUnitalStarRingHom.instMonoid {A : Type u_1} [NonUnitalNonAssocSemiring A] [Star A] :
    Monoid (A →⋆ₙ+* A)
    Equations
    • NonUnitalStarRingHom.instMonoid = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯
    source
    @[simp]
    theorem NonUnitalStarRingHom.coe_one {A : Type u_1} [NonUnitalNonAssocSemiring A] [Star A] :
    ⇑1 = id
    source
    theorem NonUnitalStarRingHom.one_apply {A : Type u_1} [NonUnitalNonAssocSemiring A] [Star A] (a : A) :
    1 a = a
    source
    instance NonUnitalStarRingHom.instZero {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [StarAddMonoid B] :
    Zero (A →⋆ₙ+* B)
    Equations
    • NonUnitalStarRingHom.instZero = { zero := let __src := 0; { toNonUnitalRingHom := __src, map_star' := ⋯ } }
    source
    instance NonUnitalStarRingHom.instInhabited {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [StarAddMonoid B] :
    Inhabited (A →⋆ₙ+* B)
    Equations
    • NonUnitalStarRingHom.instInhabited = { default := 0 }
    source
    instance NonUnitalStarRingHom.instMonoidWithZero {A : Type u_1} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] :
    MonoidWithZero (A →⋆ₙ+* A)
    Equations
    source
    @[simp]
    theorem NonUnitalStarRingHom.coe_zero {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [StarAddMonoid B] :
    ⇑0 = 0
    source
    theorem NonUnitalStarRingHom.zero_apply {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [StarAddMonoid B] (a : A) :
    0 a = 0

    Star ring equivalences #

    source
    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 : A → B
    • invFun : B → A
    • 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
    source
    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.

    source
    def «term_≃⋆+*_» :
    Lean.TrailingParserDescr

    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
    source
    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 :
    Prop

    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
    source
    theorem StarRingEquivClass.map_star {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} :
    ∀ {inst : Add A} {inst_1 : Mul A} {inst_2 : Star A} {inst_3 : Add B} {inst_4 : Mul B} {inst_5 : Star B} {inst_6 : 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.

    source
    @[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] :
    StarHomClass F A B
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance StarRingEquivClass.instNonUnitalStarRingHomClass {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] [EquivLike F A B] [RingEquivClass F A B] [StarRingEquivClass F A B] :
    NonUnitalStarRingHomClass F A B
    Equations
    • ⋯ = ⋯
    source
    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) :
    A ≃⋆+* B

    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 = { toRingEquiv := ↑f, map_star' := ⋯ }
    source
    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] :
    CoeHead F (A ≃⋆+* B)

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

    Equations
    • StarRingEquivClass.instCoeHead = { coe := StarRingEquivClass.toStarRingEquiv }
    source
    instance StarRingEquiv.instEquivLike {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
    EquivLike (A ≃⋆+* B) A B
    Equations
    • StarRingEquiv.instEquivLike = { coe := fun (f : A ≃⋆+* B) => f.toFun, inv := fun (f : A ≃⋆+* B) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
    source
    instance StarRingEquiv.instRingEquivClass {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
    RingEquivClass (A ≃⋆+* B) A B
    Equations
    • ⋯ = ⋯
    source
    instance StarRingEquiv.instStarRingEquivClass {A : Type u_1} {B : Type u_2} [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] :
    StarRingEquivClass (A ≃⋆+* B) A B
    Equations
    • ⋯ = ⋯
    source
    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' := ⋯ }
    source
    @[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
    source
    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
    source
    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
    source
    def StarRingEquiv.refl {A : Type u_1} [Add A] [Mul A] [Star A] :
    A ≃⋆+* A

    The identity map as a star ring isomorphism.

    Equations
    source
    instance StarRingEquiv.instInhabited {A : Type u_1} [Add A] [Mul A] [Star A] :
    Inhabited (A ≃⋆+* A)
    Equations
    • StarRingEquiv.instInhabited = { default := StarRingEquiv.refl }
    source
    @[simp]
    theorem StarRingEquiv.coe_refl {A : Type u_1} [Add A] [Mul A] [Star A] :
    ⇑StarRingEquiv.refl = id
    source
    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) :
    B ≃⋆+* A

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

    Equations
    • e.symm = { toRingEquiv := e.symm, map_star' := ⋯ }
    source
    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) :
    A → B

    See Note [custom simps projection]

    Equations
    source
    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) :
    B → A

    See Note [custom simps projection]

    Equations
    source
    @[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
    source
    @[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
    source
    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
    source
    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
    source
    @[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' : B → A) (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
    source
    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 : A → B) (f' : B → A) (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)) :
    B ≃⋆+* A

    Auxiliary 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
    source
    @[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 : A → B) (f' : B → A) (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' := ⋯ }
    source
    @[simp]
    theorem StarRingEquiv.refl_symm {A : Type u_1} [Add A] [Mul A] [Star A] :
    StarRingEquiv.refl.symm = StarRingEquiv.refl
    source
    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) :
    A ≃⋆+* C

    Transitivity of StarRingEquiv.

    Equations
    • e₁.trans e₂ = { toRingEquiv := e₁.trans e₂.toRingEquiv, map_star' := ⋯ }
    source
    @[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
    source
    @[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
    source
    @[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)
    source
    @[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₁
    source
    @[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)
    source
    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
    source
    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
    source
    @[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
    source
    @[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
    source
    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) :
    A ≃⋆+* B

    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' := ⋯ }
    source
    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) :
    A ≃⋆+* B

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

    Equations
    source
    @[simp]
    theorem StarRingEquiv.coe_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) :
    ⇑(StarRingEquiv.ofBijective f hf) = ⇑f
    source
    theorem StarRingEquiv.ofBijective_apply {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) (a : A) :
    (StarRingEquiv.ofBijective f hf) a = f a