data.equiv.ring

# (Semi)ring equivs

In this file we define extension of equiv called ring_equiv, which is a datatype representing an isomorphism of semirings, rings, division_rings, or fields. We also introduce the corresponding group of automorphisms ring_aut.

## Notations

The extended equiv have coercions to functions, and the coercion is the canonical notation when treating the isomorphism as maps.

## Implementation notes

The fields for ring_equiv now avoid the unbundled is_mul_hom and is_add_hom, as these are deprecated.

Definition of multiplication in the groups of automorphisms agrees with function composition, multiplication in equiv.perm, and multiplication in category_theory.End, not with category_theory.comp.

## Tags

structure ring_equiv (R : Type u_4) (S : Type u_5) [has_mul R] [has_add R] [has_mul S] [has_add S] :
Type (max u_4 u_5)

An equivalence between two (semi)rings that preserves the algebraic structure.

def ring_equiv.to_mul_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :
R ≃+* SR ≃* S

The equivalence of multiplicative monoids underlying an equivalence of (semi)rings.

def ring_equiv.to_add_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :
R ≃+* SR ≃+ S

The equivalence of additive monoids underlying an equivalence of (semi)rings.

def ring_equiv.to_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :
R ≃+* SR S

The "plain" equivalence of types underlying an equivalence of (semi)rings.

@[instance]
def ring_equiv.has_coe_to_fun {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] :

Equations
@[simp]
theorem ring_equiv.to_fun_eq_coe_fun {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

@[ext]
theorem ring_equiv.ext {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] {f g : R ≃+* S} :
(∀ (x : R), f x = g x)f = g

Two ring isomorphisms agree if they are defined by the same underlying function.

@[instance]
def ring_equiv.has_coe_to_mul_equiv {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] :
has_coe (R ≃+* S) (R ≃* S)

Equations
@[instance]
def ring_equiv.has_coe_to_add_equiv {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] :
has_coe (R ≃+* S) (R ≃+ S)

Equations
theorem ring_equiv.coe_mul_equiv {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) (a : R) :
f a = f a

theorem ring_equiv.coe_add_equiv {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) (a : R) :
f a = f a

def ring_equiv.refl (R : Type u_1) [has_mul R] [has_add R] :
R ≃+* R

The identity map is a ring isomorphism.

Equations
@[simp]
theorem ring_equiv.refl_apply (R : Type u_1) [has_mul R] [has_add R] (x : R) :
x = x

@[simp]

@[simp]
theorem ring_equiv.coe_mul_equiv_refl (R : Type u_1) [has_mul R] [has_add R] :

@[instance]
def ring_equiv.inhabited (R : Type u_1) [has_mul R] [has_add R] :

Equations
def ring_equiv.symm {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] :
R ≃+* SS ≃+* R

The inverse of a ring isomorphism is a ring isomorphism.

Equations
def ring_equiv.trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] :
R ≃+* SS ≃+* S'R ≃+* S'

Transitivity of ring_equiv.

Equations
@[simp]
theorem ring_equiv.trans_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [semiring A] [semiring B] [semiring C] (e : A ≃+* B) (f : B ≃+* C) (a : A) :
(e.trans f) a = f (e a)

theorem ring_equiv.bijective {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :

theorem ring_equiv.injective {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :

theorem ring_equiv.surjective {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :

@[simp]
theorem ring_equiv.apply_symm_apply {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x : S) :
e ((e.symm) x) = x

@[simp]
theorem ring_equiv.symm_apply_apply {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x : R) :
(e.symm) (e x) = x

theorem ring_equiv.image_eq_preimage {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (s : set R) :
e '' s = (e.symm) ⁻¹' s

def ring_equiv.to_opposite (R : Type u_1)  :

A commutative ring is isomorphic to its opposite.

Equations
@[simp]
theorem ring_equiv.to_opposite_apply (R : Type u_1) (r : R) :

@[simp]
theorem ring_equiv.to_opposite_symm_apply (R : Type u_1) (r : Rᵒᵖ) :
.symm) r =

@[simp]
theorem ring_equiv.map_mul {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) (x y : R) :
f (x * y) = (f x) * f y

A ring isomorphism preserves multiplication.

@[simp]
theorem ring_equiv.map_one {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
f 1 = 1

A ring isomorphism sends one to one.

@[simp]
theorem ring_equiv.map_add {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) (x y : R) :
f (x + y) = f x + f y

@[simp]
theorem ring_equiv.map_zero {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
f 0 = 0

A ring isomorphism sends zero to zero.

@[simp]
theorem ring_equiv.map_eq_one_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) {x : R} :
f x = 1 x = 1

@[simp]
theorem ring_equiv.map_eq_zero_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) {x : R} :
f x = 0 x = 0

theorem ring_equiv.map_ne_one_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) {x : R} :
f x 1 x 1

theorem ring_equiv.map_ne_zero_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) {x : R} :
f x 0 x 0

def ring_equiv.of_bijective {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) :
R ≃+* S

Produce a ring isomorphism from a bijective ring homomorphism.

Equations
@[simp]
theorem ring_equiv.map_neg {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R ≃+* S) (x : R) :
f (-x) = -f x

@[simp]
theorem ring_equiv.map_sub {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R ≃+* S) (x y : R) :
f (x - y) = f x - f y

@[simp]
theorem ring_equiv.map_neg_one {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R ≃+* S) :
f (-1) = -1

def ring_equiv.to_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] :
R ≃+* SR →+* S

Reinterpret a ring equivalence as a ring homomorphism.

Equations
theorem ring_equiv.to_ring_hom_injective {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] :

@[instance]
def ring_equiv.has_coe_to_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] :
has_coe (R ≃+* S) (R →+* S)

Equations
theorem ring_equiv.coe_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) (a : R) :
f a = f a

theorem ring_equiv.coe_ring_hom_inj_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f g : R ≃+* S) :
f = g f = g

def ring_equiv.to_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] :
R ≃+* SR →* S

Reinterpret a ring equivalence as a monoid homomorphism.

def ring_equiv.to_add_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] :
R ≃+* SR →+ S

Reinterpret a ring equivalence as an add_monoid homomorphism.

@[simp]
theorem ring_equiv.to_ring_hom_refl {R : Type u_1} [semiring R] :

@[simp]
theorem ring_equiv.to_monoid_hom_refl {R : Type u_1} [semiring R] :

@[simp]
theorem ring_equiv.to_add_monoid_hom_refl {R : Type u_1} [semiring R] :

@[simp]
theorem ring_equiv.to_ring_hom_apply_symm_to_ring_hom_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) (y : S) :

@[simp]
theorem ring_equiv.symm_to_ring_hom_apply_to_ring_hom_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) (x : R) :

@[simp]
theorem ring_equiv.to_ring_hom_trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [semiring R] [semiring S] [semiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

def ring_equiv.of_hom_inv {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (hom : R →+* S) (inv : S →+* R) :
inv.comp hom = hom.comp inv = R ≃+* S

Construct an equivalence of rings from homomorphisms in both directions, which are inverses.

Equations
@[simp]
theorem ring_equiv.of_hom_inv_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (hom : R →+* S) (inv : S →+* R) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) (r : R) :
inv hom_inv_id inv_hom_id) r = hom r

@[simp]
theorem ring_equiv.of_hom_inv_symm_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (hom : R →+* S) (inv : S →+* R) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) (s : S) :
inv hom_inv_id inv_hom_id).symm) s = inv s

def mul_equiv.to_ring_equiv {R : Type u_1} {S : Type u_2} [has_add R] [has_add S] [has_mul R] [has_mul S] (h : R ≃* S) :
(∀ (x y : R), h (x + y) = h x + h y)R ≃+* S

Gives a ring_equiv from a mul_equiv preserving addition.

Equations
@[simp]
theorem ring_equiv.trans_symm {R : Type u_1} {S : Type u_2} [has_add R] [has_add S] [has_mul R] [has_mul S] (e : R ≃+* S) :
e.trans e.symm =

@[simp]
theorem ring_equiv.symm_trans {R : Type u_1} {S : Type u_2} [has_add R] [has_add S] [has_mul R] [has_mul S] (e : R ≃+* S) :
e.symm.trans e =

theorem ring_equiv.is_integral_domain {A : Type u_1} (B : Type u_2) [ring A] [ring B] :
A ≃+* B

If two rings are isomorphic, and the second is an integral domain, then so is the first.

def ring_equiv.integral_domain {A : Type u_1} (B : Type u_2) [ring A]  :
A ≃+* B

If two rings are isomorphic, and the second is an integral domain, then so is the first.

Equations
def ring_aut (R : Type u_1) [has_mul R] [has_add R] :
Type u_1

The group of ring automorphisms.

Equations
@[instance]
def ring_aut.group (R : Type u_1) [has_mul R] [has_add R] :

The group operation on automorphisms of a ring is defined by λ g h, ring_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x) .

Equations
@[instance]
def ring_aut.inhabited (R : Type u_1) [has_mul R] [has_add R] :

Equations

Monoid homomorphism from ring automorphisms to additive automorphisms.

Equations
def ring_aut.to_mul_aut (R : Type u_1) [has_mul R] [has_add R] :

Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

Equations
def ring_aut.to_perm (R : Type u_1) [has_mul R] [has_add R] :

Monoid homomorphism from ring automorphisms to permutations.

Equations
def equiv.units_equiv_ne_zero (K : Type u_4)  :
{a : K | a 0}

In a division ring K, the unit group units K is equivalent to the subtype of nonzero elements.

Equations
@[simp]
theorem equiv.coe_units_equiv_ne_zero {K : Type u_4} (a : units K) :
a) = a