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 #

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

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.

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 :

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

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 = let __src := ↑f; { toNonUnitalRingHom := __src, 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

Equations

⋯ = ⋯

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

⋯ = ⋯

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 : 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' : 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 = let __src := 1; { toNonUnitalRingHom := __src, 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 = let __src := f.comp g.toNonUnitalRingHom; { toNonUnitalRingHom := __src, 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 ⋯ ⋯ npowRec ⋯ ⋯

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

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.

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 :

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

StarRingEquiv.instStarRingEquivClass

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] :

StarHomClass F A B

Equations

⋯ = ⋯

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

⋯ = ⋯

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

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

Equations

⋯ = ⋯

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

⋯ = ⋯

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

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) :

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

Equations

e.symm = let __src := e.symm; { toRingEquiv := __src, 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)) :

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

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

Transitivity of StarRingEquiv.

Equations

e₁.trans e₂ = let __src := e₁.trans e₂.toRingEquiv; { toRingEquiv := __src, 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

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

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

StarRingEquiv.ofBijective f hf = let __src := RingEquiv.ofBijective f hf; { toFun := ⇑f, invFun := __src.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