mathlib documentation

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 #

equiv, mul_equiv, add_equiv, ring_equiv, mul_aut, add_aut, ring_aut

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

source
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

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

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

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

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

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

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
source
@[simp]
theorem ring_equiv.to_fun_eq_coe {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
@[simp]
theorem ring_equiv.map_mul {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x y : R) :
⇑e (x * y) = (⇑e x) * ⇑e y

A ring isomorphism preserves multiplication.

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

A ring isomorphism preserves addition.

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
@[simp]
theorem ring_equiv.coe_mk {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R → S) (e' : S → R) (h₁ : function.left_inverse e' e) (h₂ : function.right_inverse e' e) (h₃ : ∀ (x y : R), e (x * y) = (e x) * e y) (h₄ : ∀ (x y : R), e (x + y) = e x + e y) :
⇑{to_fun := e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄} = e
source
@[simp]
theorem ring_equiv.mk_coe {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (e' : S → R) (h₁ : function.left_inverse e' ⇑e) (h₂ : function.right_inverse e' ⇑e) (h₃ : ∀ (x y : R), ⇑e (x * y) = (⇑e x) * ⇑e y) (h₄ : ∀ (x y : R), ⇑e (x + y) = ⇑e x + ⇑e y) :
{to_fun := ⇑e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄} = e
source
theorem ring_equiv.congr_arg {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] {f : R ≃+* S} {x x' : R} :
x = x' → ⇑f x = ⇑f x'
source
theorem ring_equiv.congr_fun {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 : f = g) (x : R) :
⇑f x = ⇑g x
source
theorem ring_equiv.ext_iff {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] {f g : R ≃+* S} :
f = g ↔ ∀ (x : R), ⇑f x = ⇑g x
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
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
source
theorem ring_equiv.to_add_equiv_eq_coe {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_add_equiv = ↑f
source
theorem ring_equiv.to_mul_equiv_eq_coe {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_mul_equiv = ↑f
source
@[simp]
theorem ring_equiv.coe_to_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) :
⇑↑f = ⇑f
source
@[simp]
theorem ring_equiv.coe_to_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) :
⇑↑f = ⇑f
source
def ring_equiv.ring_equiv_of_unique_of_unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_mul M] [has_add N] [has_mul N] :
M ≃+* N

The ring_equiv between two semirings with a unique element.

Equations
source
@[instance]
def ring_equiv.unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_mul M] [has_add N] [has_mul N] :
unique (M ≃+* N)
Equations
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
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
@[instance]
def ring_equiv.inhabited (R : Type u_1) [has_mul R] [has_add R] :
inhabited (R ≃+* R)
Equations
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
source
def ring_equiv.simps.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) :
S → R

See Note [custom simps projection]

Equations
source
@[simp]
theorem ring_equiv.symm_symm {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
e.symm.symm = e
source
theorem ring_equiv.symm_bijective {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] :
function.bijective ring_equiv.symm
source
@[simp]
theorem ring_equiv.mk_coe' {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (f : S → R) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e f) (h₃ : ∀ (x y : S), f (x * y) = (f x) * f y) (h₄ : ∀ (x y : S), f (x + y) = f x + f y) :
{to_fun := f, inv_fun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄} = e.symm
source
@[simp]
theorem ring_equiv.symm_mk {R : Type u_1} {S : Type u_2} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R → S) (g : S → R) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : R), f (x * y) = (f x) * f y) (h₄ : ∀ (x y : R), f (x + y) = f x + f y) :
{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄}.symm = {to_fun := g, inv_fun := f, 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
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
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_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_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
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
source
theorem ring_equiv.to_ring_hom_injective {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] :
function.injective ring_equiv.to_ring_hom
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
source
theorem ring_equiv.to_ring_hom_eq_coe {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
f.to_ring_hom = ↑f
source
@[simp]
theorem ring_equiv.coe_to_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
⇑↑f = ⇑f
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
theorem ring_equiv.to_add_monoid_hom_commutes {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
↑f.to_add_monoid_hom = ↑f.to_add_monoid_hom

The two paths coercion can take to an add_monoid_hom are equivalent

source
theorem ring_equiv.to_monoid_hom_commutes {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
↑f.to_monoid_hom = ↑f.to_monoid_hom

The two paths coercion can take to an monoid_hom are equivalent

source
theorem ring_equiv.to_equiv_commutes {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R ≃+* S) :
↑f.to_equiv = ↑f.to_equiv

The two paths coercion can take to an equiv are equivalent

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
@[simp]
theorem ring_equiv.to_ring_hom_comp_symm_to_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) :
e.to_ring_hom.comp e.symm.to_ring_hom = ring_hom.id S
source
@[simp]
theorem ring_equiv.symm_to_ring_hom_comp_to_ring_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (e : R ≃+* S) :
e.symm.to_ring_hom.comp e.to_ring_hom = ring_hom.id R
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
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
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
source
def equiv.units_equiv_ne_zero (K : Type u_4) [division_ring K] :
units K ≃ ↥{a : K | a ≠ 0}

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

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