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

• NonUnitalStarRingHom

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

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

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

Equations

• «term_→⋆ₙ+*_» = Lean.ParserDescr.trailingNode `«term_→⋆ₙ+*_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →⋆ₙ+* ") (Lean.ParserDescr.cat `term 25))

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 F A B : 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.

• map_star (f : F) (r : A) : f (star r) = star (f r)

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' := ⋯ }

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 }

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' := ⋯ }

instance NonUnitalStarRingHom.instNonUnitalRingHomClass {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] : NonUnitalRingHomClass (A →⋆ₙ+* B) A B

instance NonUnitalStarRingHom.instNonUnitalStarRingHomClass {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] : NonUnitalStarRingHomClass (A →⋆ₙ+* B) A B

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

• NonUnitalStarRingHom.Simps.apply f = ⇑f

@[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 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' : 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' := ⋯ }

@[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'

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

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

def NonUnitalStarRingHom.id (A : Type u_1) [NonUnitalNonAssocSemiring A] [Star A] : A →⋆ₙ+* A

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

Equations

• NonUnitalStarRingHom.id A = { toNonUnitalRingHom := 1, map_star' := ⋯ }

@[simp]

theorem NonUnitalStarRingHom.coe_id (A : Type u_1) [NonUnitalNonAssocSemiring A] [Star A] : ⇑(NonUnitalStarRingHom.id A) = id

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' := ⋯ }

@[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)

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

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

instance NonUnitalStarRingHom.instMonoid {A : Type u_1} [NonUnitalNonAssocSemiring A] [Star A] : Monoid (A →⋆ₙ+* A)

Equations

• NonUnitalStarRingHom.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

@[simp]

theorem NonUnitalStarRingHom.coe_one {A : Type u_1} [NonUnitalNonAssocSemiring A] [Star A] : ⇑1 = id

theorem NonUnitalStarRingHom.one_apply {A : Type u_1} [NonUnitalNonAssocSemiring A] [Star A] (a : A) : 1 a = a

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' := ⋯ } }

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 }

instance NonUnitalStarRingHom.instMonoidWithZero {A : Type u_1} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] : MonoidWithZero (A →⋆ₙ+* A)

Equations

• NonUnitalStarRingHom.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

@[simp]

theorem NonUnitalStarRingHom.coe_zero {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [StarAddMonoid B] : ⇑0 = 0

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

structure StarRingEquiv (A : Type u_1) (B : Type u_2) [Add A] [Add B] [Mul A] [Mul B] [Star A] [Star B] extends A ≃+* B : 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.

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

• «term_≃⋆+*_» = Lean.ParserDescr.trailingNode `«term_≃⋆+*_» 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃⋆+* ") (Lean.ParserDescr.cat `term 0))

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 F A B : 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.

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

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

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' := ⋯ }

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 }

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' := ⋯ }

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

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

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 g : A ≃⋆+* B} (h : ∀ (a : A), f a = g a) : f = g

def StarRingEquiv.refl {A : Type u_1} [Add A] [Mul A] [Star A] : A ≃⋆+* A

The identity map as a star ring isomorphism.

Equations

• StarRingEquiv.refl = { toRingEquiv := RingEquiv.refl A, map_star' := ⋯ }

instance StarRingEquiv.instInhabited {A : Type u_1} [Add A] [Mul A] [Star A] : Inhabited (A ≃⋆+* 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) : B ≃⋆+* A

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

Equations

• e.symm = { toRingEquiv := e.symm, map_star' := ⋯ }

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

• StarRingEquiv.Simps.apply e = ⇑e

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

• StarRingEquiv.Simps.symm_apply e = ⇑e.symm

@[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' : 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

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

@[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' := ⋯ }

@[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) : A ≃⋆+* C

Transitivity of StarRingEquiv.

Equations

• e₁.trans e₂ = { toRingEquiv := e₁.trans e₂.toRingEquiv, map_star' := ⋯ }

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

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' := ⋯ }

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

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

• StarRingEquiv.ofBijective f hf = { toFun := ⇑f, invFun := (RingEquiv.ofBijective f hf).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯ }

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

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