mathlib docs: data.equiv.ring

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)

to_fun : R → S
inv_fun : S → R
left_inv : function.left_inverse c.inv_fun c.to_fun
right_inv : function.right_inverse c.inv_fun c.to_fun
map_mul' : ∀ (x y : R), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
map_add' : ∀ (x y : R), c.to_fun (x + y) = c.to_fun x + c.to_fun y

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] (s : R ≃+* S) :

R ≃* S

source

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] (s : R ≃+* S) :

R ≃+ S

source

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] (s : R ≃+* S) :

R ≃ S

source

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

has_coe_to_fun (R ≃+* S)

Equations

ring_equiv.has_coe_to_fun = {F := λ (x : R ≃+* S), R → S, coe := ring_equiv.to_fun _inst_4}

source

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

f.to_fun = ⇑f

source

@[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} (h : ∀ (x : R), ⇑f x = ⇑g x) :

f = g

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

source

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

ring_equiv.has_coe_to_mul_equiv = {coe := ring_equiv.to_mul_equiv _inst_4}

source

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

ring_equiv.has_coe_to_add_equiv = {coe := ring_equiv.to_add_equiv _inst_4}

source

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

source

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

source

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

R ≃+* R

The identity map is a ring isomorphism.

Equations

ring_equiv.refl R = {to_fun := (mul_equiv.refl R).to_fun, inv_fun := (mul_equiv.refl R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem ring_equiv.refl_apply (R : Type u_1) [has_mul R] [has_add R] (x : R) :

⇑(ring_equiv.refl R) x = x

source

@[simp]

theorem ring_equiv.coe_add_equiv_refl (R : Type u_1) [has_mul R] [has_add R] :

↑(ring_equiv.refl R) = add_equiv.refl R

source

@[simp]

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

↑(ring_equiv.refl R) = mul_equiv.refl R

source

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

S ≃+* R

The inverse of a ring isomorphism is a ring isomorphism.

Equations

e.symm = {to_fun := e.to_mul_equiv.symm.to_fun, inv_fun := e.to_mul_equiv.symm.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

R ≃+* S'

Transitivity of ring_equiv.

Equations

e₁.trans e₂ = {to_fun := (e₁.to_mul_equiv.trans e₂.to_mul_equiv).to_fun, inv_fun := (e₁.to_mul_equiv.trans e₂.to_mul_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

source

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

function.bijective ⇑e

source

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

function.injective ⇑e

source

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

function.surjective ⇑e

source

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

source

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

source

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

source

def ring_equiv.to_opposite (R : Type u_1) [comm_semiring R] :

R ≃+* Rᵒᵖ

A commutative ring is isomorphic to its opposite.

Equations

ring_equiv.to_opposite R = {to_fun := opposite.equiv_to_opposite.to_fun, inv_fun := opposite.equiv_to_opposite.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem ring_equiv.to_opposite_apply (R : Type u_1) [comm_semiring R] (r : R) :

⇑(ring_equiv.to_opposite R) r = opposite.op r

source

@[simp]

theorem ring_equiv.to_opposite_symm_apply (R : Type u_1) [comm_semiring R] (r : Rᵒᵖ) :

⇑((ring_equiv.to_opposite R).symm) r = opposite.unop r

source

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

source

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

source

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

A ring isomorphism preserves addition.

source

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

source

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

source

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

source

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

source

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

source

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

R ≃+* S

Produce a ring isomorphism from a bijective ring homomorphism.

Equations

ring_equiv.of_bijective f hf = {to_fun := (equiv.of_bijective ⇑f hf).to_fun, inv_fun := (equiv.of_bijective ⇑f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

source

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

source

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

source

def ring_equiv.to_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) :

R →+* S

Reinterpret a ring equivalence as a ring homomorphism.

Equations

e.to_ring_hom = {to_fun := e.to_mul_equiv.to_monoid_hom.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

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

ring_equiv.has_coe_to_ring_hom = {coe := ring_equiv.to_ring_hom _inst_2}

source

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

source

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

source

def ring_equiv.to_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) :

R →* S

Reinterpret a ring equivalence as a monoid homomorphism.

source

def ring_equiv.to_add_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) :

R →+ S

Reinterpret a ring equivalence as an add_monoid homomorphism.

source

@[simp]

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

(ring_equiv.refl R).to_ring_hom = ring_hom.id R

source

@[simp]

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

(ring_equiv.refl R).to_monoid_hom = monoid_hom.id R

source

@[simp]

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

(ring_equiv.refl R).to_add_monoid_hom = add_monoid_hom.id R

source

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

⇑(e.to_ring_hom) (⇑(e.symm.to_ring_hom) y) = y

source

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

⇑(e.symm.to_ring_hom) (⇑(e.to_ring_hom) x) = x

source

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

(e₁.trans e₂).to_ring_hom = e₂.to_ring_hom.comp e₁.to_ring_hom

source

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

R ≃+* S

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

Equations

ring_equiv.of_hom_inv hom inv hom_inv_id inv_hom_id = {to_fun := hom.to_fun, inv_fun := ⇑inv, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[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 = ring_hom.id R) (inv_hom_id : hom.comp inv = ring_hom.id S) (r : R) :

⇑(ring_equiv.of_hom_inv hom inv hom_inv_id inv_hom_id) r = ⇑hom r

source

@[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 = ring_hom.id R) (inv_hom_id : hom.comp inv = ring_hom.id S) (s : S) :

⇑((ring_equiv.of_hom_inv hom inv hom_inv_id inv_hom_id).symm) s = ⇑inv s

source

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) (H : ∀ (x y : R), ⇑h (x + y) = ⇑h x + ⇑h y) :

R ≃+* S

Gives a ring_equiv from a mul_equiv preserving addition.

Equations

h.to_ring_equiv H = {to_fun := h.to_equiv.to_fun, inv_fun := h.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[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 = ring_equiv.refl R

source

@[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 = ring_equiv.refl S

source

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

is_integral_domain A

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

source

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

integral_domain A

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

Equations

ring_equiv.integral_domain B e = {add := ring.add _inst_5, add_assoc := _, zero := ring.zero _inst_5, zero_add := _, add_zero := _, neg := ring.neg _inst_5, add_left_neg := _, add_comm := _, mul := ring.mul _inst_5, mul_assoc := _, one := ring.one _inst_5, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

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

Type u_1

The group of ring automorphisms.

Equations

ring_aut R = (R ≃+* R)

source

@[instance]

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

group (ring_aut 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