algebra.ring.equiv - mathlib docs

structure ring_equiv (R : Type u_7) (S : Type u_8) [has_mul R] [has_add R] [has_mul S] [has_add S] :

Type (max u_7 u_8)

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

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

def ring_equiv.to_mul_equiv {R : Type u_7} {S : Type u_8} [has_mul R] [has_add R] [has_mul S] [has_add S] (self : 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_7} {S : Type u_8} [has_mul R] [has_add R] [has_mul S] [has_add S] (self : R ≃+* S) :

R ≃+ S

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

source

def ring_equiv.to_equiv {R : Type u_7} {S : Type u_8} [has_mul R] [has_add R] [has_mul S] [has_add S] (self : R ≃+* S) :

R ≃ S

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

source

@[class]

structure ring_equiv_class (F : Type u_7) (R : out_param (Type u_8)) (S : out_param (Type u_9)) [has_mul R] [has_add R] [has_mul S] [has_add S] :

Type (max u_7 u_8 u_9)

coe : F → R → S
inv : F → S → R
left_inv : ∀ (e : F), function.left_inverse (ring_equiv_class.inv e) (ring_equiv_class.coe e)
right_inv : ∀ (e : F), function.right_inverse (ring_equiv_class.inv e) (ring_equiv_class.coe e)
coe_injective' : ∀ (e g : F), ring_equiv_class.coe e = ring_equiv_class.coe g → ring_equiv_class.inv e = ring_equiv_class.inv g → e = g
map_mul : ∀ (f : F) (a b : R), ⇑f (a * b) = (⇑f a) * ⇑f b
map_add : ∀ (f : F) (a b : R), ⇑f (a + b) = ⇑f a + ⇑f b

ring_equiv_class F R S states that F is a type of ring structure preserving equivalences. You should extend this class when you extend ring_equiv.

Instances

source

@[instance]

def ring_equiv_class.to_mul_equiv_class (F : Type u_7) (R : out_param (Type u_8)) (S : out_param (Type u_9)) [has_mul R] [has_add R] [has_mul S] [has_add S] [self : ring_equiv_class F R S] :

mul_equiv_class F R S

source

@[protected, instance]

def ring_equiv_class.to_add_equiv_class (F : Type u_1) (R : Type u_2) (S : Type u_3) [has_mul R] [has_add R] [has_mul S] [has_add S] [h : ring_equiv_class F R S] :

add_equiv_class F R S

Equations

ring_equiv_class.to_add_equiv_class F R S = {coe := coe_fn fun_like.has_coe_to_fun, inv := ring_equiv_class.inv h, left_inv := _, right_inv := _, coe_injective' := _, map_add := _}

source

@[protected, instance]

def ring_equiv_class.to_ring_hom_class (F : Type u_1) (R : Type u_2) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [h : ring_equiv_class F R S] :

ring_hom_class F R S

Equations

ring_equiv_class.to_ring_hom_class F R S = {coe := coe_fn fun_like.has_coe_to_fun, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _}

source

@[protected, instance]

def ring_equiv.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_mul β] [has_add β] [ring_equiv_class F α β] :

has_coe_t F (α ≃+* β)

Equations

ring_equiv.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, inv_fun := equiv_like.inv f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}}

source

@[protected, instance]

def ring_equiv.ring_equiv_class {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :

ring_equiv_class (R ≃+* S) R S

Equations

ring_equiv.ring_equiv_class = {coe := ring_equiv.to_fun _inst_4, inv := ring_equiv.inv_fun _inst_4, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _, map_add := _}

source

@[protected, instance]

def ring_equiv.has_coe_to_fun {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :

has_coe_to_fun (R ≃+* S) (λ (_x : R ≃+* S), R → S)

Equations

ring_equiv.has_coe_to_fun = {coe := ring_equiv.to_fun _inst_4}

source

@[simp]

theorem ring_equiv.to_equiv_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

f.to_equiv = ↑f

source

@[simp]

theorem ring_equiv.to_fun_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

f.to_fun = ⇑f

source

@[simp]

theorem ring_equiv.coe_to_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

⇑↑f = ⇑f

source

@[protected]

theorem ring_equiv.map_mul {R : Type u_4} {S : Type u_5} [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

@[protected]

theorem ring_equiv.map_add {R : Type u_4} {S : Type u_5} [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_4} {S : Type u_5} [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_4} {S : Type u_5} [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_4} {S : Type u_5} [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

@[protected]

theorem ring_equiv.congr_arg {R : Type u_4} {S : Type u_5} [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

@[protected]

theorem ring_equiv.congr_fun {R : Type u_4} {S : Type u_5} [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

@[protected]

theorem ring_equiv.ext_iff {R : Type u_4} {S : Type u_5} [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

@[simp]

theorem ring_equiv.to_add_equiv_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

f.to_add_equiv = ↑f

source

@[simp]

theorem ring_equiv.to_mul_equiv_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

f.to_mul_equiv = ↑f

source

@[simp, norm_cast]

theorem ring_equiv.coe_to_mul_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

⇑↑f = ⇑f

source

@[simp, norm_cast]

theorem ring_equiv.coe_to_add_equiv {R : Type u_4} {S : Type u_5} [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

ring_equiv.ring_equiv_of_unique_of_unique = {to_fun := add_equiv.add_equiv_of_unique_of_unique.to_fun, inv_fun := add_equiv.add_equiv_of_unique_of_unique.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

ring_equiv.unique = {to_inhabited := {default := ring_equiv.ring_equiv_of_unique_of_unique _inst_12}, uniq := _}

source

@[protected]

def ring_equiv.refl (R : Type u_4) [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_4) [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_4) [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_4) [has_mul R] [has_add R] :

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

source

@[protected, instance]

def ring_equiv.inhabited (R : Type u_4) [has_mul R] [has_add R] :

inhabited (R ≃+* R)

Equations

ring_equiv.inhabited R = {default := ring_equiv.refl R _inst_2}

source

@[protected]

def ring_equiv.symm {R : Type u_4} {S : Type u_5} [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.simps.symm_apply {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :

S → R

See Note [custom simps projection]

Equations

ring_equiv.simps.symm_apply e = ⇑(e.symm)

source

@[simp]

theorem ring_equiv.inv_fun_eq_symm {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :

f.inv_fun = ⇑(f.symm)

source

@[simp]

theorem ring_equiv.symm_symm {R : Type u_4} {S : Type u_5} [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_4} {S : Type u_5} [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_4} {S : Type u_5} [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_4} {S : Type u_5} [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

@[protected]

def ring_equiv.trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [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 {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) :

⇑(e₁.trans e₂) a = ⇑e₂ (⇑e₁ a)

source

@[protected]

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

function.bijective ⇑e

source

@[protected]

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

function.injective ⇑e

source

@[protected]

theorem ring_equiv.surjective {R : Type u_4} {S : Type u_5} [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_4} {S : Type u_5} [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_4} {S : Type u_5} [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_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (s : set R) :

⇑e '' s = ⇑(e.symm) ⁻¹' s

source

@[simp]

theorem ring_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) (ᾰ : β) :

⇑((⇑(ring_equiv.op.symm) f).symm) ᾰ = (⇑(add_equiv.mul_op.symm) f.to_add_equiv).inv_fun ᾰ

source

@[simp]

theorem ring_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) (ᾰ : α) :

⇑(⇑(ring_equiv.op.symm) f) ᾰ = (⇑(add_equiv.mul_op.symm) f.to_add_equiv).to_fun ᾰ

source

@[simp]

theorem ring_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : α ≃+* β) (ᾰ : βᵐᵒᵖ) :

⇑((⇑ring_equiv.op f).symm) ᾰ = (⇑add_equiv.mul_op f.to_add_equiv).inv_fun ᾰ

source

@[protected]

def ring_equiv.op {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] :

α ≃+* β ≃ (αᵐᵒᵖ ≃+* βᵐᵒᵖ)

A ring iso α ≃+* β can equivalently be viewed as a ring iso αᵐᵒᵖ ≃+* βᵐᵒᵖ.

Equations

ring_equiv.op = {to_fun := λ (f : α ≃+* β), {to_fun := (⇑add_equiv.mul_op f.to_add_equiv).to_fun, inv_fun := (⇑add_equiv.mul_op f.to_add_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, inv_fun := λ (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ), {to_fun := (⇑(add_equiv.mul_op.symm) f.to_add_equiv).to_fun, inv_fun := (⇑(add_equiv.mul_op.symm) f.to_add_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem ring_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : α ≃+* β) (ᾰ : αᵐᵒᵖ) :

⇑(⇑ring_equiv.op f) ᾰ = (⇑add_equiv.mul_op f.to_add_equiv).to_fun ᾰ

source

@[protected, simp]

def ring_equiv.unop {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] :

αᵐᵒᵖ ≃+* βᵐᵒᵖ ≃ (α ≃+* β)

The 'unopposite' of a ring iso αᵐᵒᵖ ≃+* βᵐᵒᵖ. Inverse to ring_equiv.op.

Equations

ring_equiv.unop = ring_equiv.op.symm

source

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

R ≃+* Rᵐᵒᵖ

A commutative ring is isomorphic to its opposite.

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[protected]

theorem ring_equiv.map_zero {R : Type u_4} {S : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (f : R ≃+* S) :

⇑f 0 = 0

A ring isomorphism sends zero to zero.

source

@[protected]

theorem ring_equiv.map_eq_zero_iff {R : Type u_4} {S : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (f : R ≃+* S) {x : R} :

⇑f x = 0 ↔ x = 0

source

theorem ring_equiv.map_ne_zero_iff {R : Type u_4} {S : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (f : R ≃+* S) {x : R} :

⇑f x ≠ 0 ↔ x ≠ 0

source

@[protected]

theorem ring_equiv.map_one {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) :

⇑f 1 = 1

A ring isomorphism sends one to one.

source

@[protected]

theorem ring_equiv.map_eq_one_iff {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) {x : R} :

⇑f x = 1 ↔ x = 1

source

theorem ring_equiv.map_ne_one_iff {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) {x : R} :

⇑f x ≠ 1 ↔ x ≠ 1

source

noncomputable def ring_equiv.of_bijective {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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.coe_of_bijective {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) (hf : function.bijective ⇑f) :

⇑(ring_equiv.of_bijective f hf) = ⇑f

source

theorem ring_equiv.of_bijective_apply {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) (hf : function.bijective ⇑f) (x : R) :

⇑(ring_equiv.of_bijective f hf) x = ⇑f x

source

@[simp]

theorem ring_equiv.Pi_congr_right_apply {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [Π (i : ι), semiring (R i)] [Π (i : ι), semiring (S i)] (e : Π (i : ι), R i ≃+* S i) (x : Π (i : ι), R i) (j : ι) :

⇑(ring_equiv.Pi_congr_right e) x j = ⇑(e j) (x j)

source

def ring_equiv.Pi_congr_right {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [Π (i : ι), semiring (R i)] [Π (i : ι), semiring (S i)] (e : Π (i : ι), R i ≃+* S i) :

(Π (i : ι), R i) ≃+* Π (i : ι), S i

A family of ring isomorphisms Π j, (R j ≃+* S j) generates a ring isomorphisms between Π j, R j and Π j, S j.

This is the ring_equiv version of equiv.Pi_congr_right, and the dependent version of ring_equiv.arrow_congr.

Equations

ring_equiv.Pi_congr_right e = {to_fun := λ (x : Π (i : ι), R i) (j : ι), ⇑(e j) (x j), inv_fun := λ (x : Π (i : ι), S i) (j : ι), ⇑((e j).symm) (x j), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem ring_equiv.Pi_congr_right_refl {ι : Type u_1} {R : ι → Type u_2} [Π (i : ι), semiring (R i)] :

ring_equiv.Pi_congr_right (λ (i : ι), ring_equiv.refl (R i)) = ring_equiv.refl (Π (i : ι), R i)

source

@[simp]

theorem ring_equiv.Pi_congr_right_symm {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [Π (i : ι), semiring (R i)] [Π (i : ι), semiring (S i)] (e : Π (i : ι), R i ≃+* S i) :

(ring_equiv.Pi_congr_right e).symm = ring_equiv.Pi_congr_right (λ (i : ι), (e i).symm)

source

@[simp]

theorem ring_equiv.Pi_congr_right_trans {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} {T : ι → Type u_4} [Π (i : ι), semiring (R i)] [Π (i : ι), semiring (S i)] [Π (i : ι), semiring (T i)] (e : Π (i : ι), R i ≃+* S i) (f : Π (i : ι), S i ≃+* T i) :

(ring_equiv.Pi_congr_right e).trans (ring_equiv.Pi_congr_right f) = ring_equiv.Pi_congr_right (λ (i : ι), (e i).trans (f i))

source

@[protected]

theorem ring_equiv.map_neg {R : Type u_4} {S : Type u_5} [non_assoc_ring R] [non_assoc_ring S] (f : R ≃+* S) (x : R) :

⇑f (-x) = -⇑f x

source

@[protected]

theorem ring_equiv.map_sub {R : Type u_4} {S : Type u_5} [non_assoc_ring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_ring R] [non_assoc_ring S] (f : R ≃+* S) :

⇑f (-1) = -1

source

def ring_equiv.to_ring_hom {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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

theorem ring_equiv.to_ring_hom_injective {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :

function.injective ring_equiv.to_ring_hom

source

@[protected, instance]

def ring_equiv.has_coe_to_ring_hom {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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.to_ring_hom_eq_coe {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) :

f.to_ring_hom = ↑f

source

@[simp, norm_cast]

theorem ring_equiv.coe_to_ring_hom {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) :

⇑↑f = ⇑f

source

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

f = g ↔ ↑f = ↑g

source

def ring_equiv.to_monoid_hom {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} [non_assoc_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_4} [non_assoc_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_4} [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} {S' : Type u_6} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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

theorem ring_equiv.map_list_prod {R : Type u_4} {S : Type u_5} [semiring R] [semiring S] (f : R ≃+* S) (l : list R) :

⇑f l.prod = (list.map ⇑f l).prod

source

theorem ring_equiv.map_list_sum {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) (l : list R) :

⇑f l.sum = (list.map ⇑f l).sum

source

theorem ring_equiv.unop_map_list_prod {R : Type u_4} {S : Type u_5} [semiring R] [semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : list R) :

mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod

An isomorphism into the opposite ring acts on the product by acting on the reversed elements

source

theorem ring_equiv.map_multiset_prod {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (f : R ≃+* S) (s : multiset R) :

⇑f s.prod = (multiset.map ⇑f s).prod

source

theorem ring_equiv.map_multiset_sum {R : Type u_4} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) (s : multiset R) :

⇑f s.sum = (multiset.map ⇑f s).sum

source

theorem ring_equiv.map_prod {R : Type u_4} {S : Type u_5} {α : Type u_1} [comm_semiring R] [comm_semiring S] (g : R ≃+* S) (f : α → R) (s : finset α) :

⇑g (∏ (x : α) in s, f x) = ∏ (x : α) in s, ⇑g (f x)

source

theorem ring_equiv.map_sum {R : Type u_4} {S : Type u_5} {α : Type u_1} [non_assoc_semiring R] [non_assoc_semiring S] (g : R ≃+* S) (f : α → R) (s : finset α) :

⇑g (∑ (x : α) in s, f x) = ∑ (x : α) in s, ⇑g (f x)

source

theorem ring_equiv.map_inv {K : Type u_7} {K' : Type u_8} [division_ring K] [division_ring K'] (g : K ≃+* K') (x : K) :

⇑g x⁻¹ = (⇑g x)⁻¹

source

theorem ring_equiv.map_div {K : Type u_7} {K' : Type u_8} [division_ring K] [division_ring K'] (g : K ≃+* K') (x y : K) :

⇑g (x / y) = ⇑g x / ⇑g y

source

@[protected]

theorem ring_equiv.map_pow {R : Type u_4} {S : Type u_5} [semiring R] [semiring S] (f : R ≃+* S) (a : R) (n : ℕ) :

⇑f (a ^ n) = ⇑f a ^ n

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