mathlib documentation

ring_theory.ring_invo

Ring involutions

This file defines a ring involution as a structure extending R ≃+* Rᵒᵖ, with the additional fact f.involution : (f (f x).unop).unop = x.

Notations

We provide a coercion to a function R → Rᵒᵖ.

References

https://en.wikipedia.org/wiki/Involution_(mathematics)#Ring_theory

Tags

Ring involution

source

structure ring_invo (R : Type u_1) [semiring R] :

Type u_1

to_ring_equiv : R ≃+* Rᵒᵖ
involution' : ∀ (x : R), opposite.unop (c.to_ring_equiv.to_fun (opposite.unop (c.to_ring_equiv.to_fun x))) = x

A ring involution

source

def ring_invo.mk' {R : Type u_1} [semiring R] (f : R →+* Rᵒᵖ) (involution : ∀ (r : R), opposite.unop (⇑f (opposite.unop (⇑f r))) = r) :

ring_invo R

Construct a ring involution from a ring homomorphism.

Equations

ring_invo.mk' f involution = {to_ring_equiv := {to_fun := f.to_fun, inv_fun := λ (r : Rᵒᵖ), opposite.unop (⇑f (opposite.unop r)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, involution' := involution}

source

@[instance]

def ring_invo.has_coe_to_fun {R : Type u_1} [semiring R] :

has_coe_to_fun (ring_invo R)

Equations

ring_invo.has_coe_to_fun = {F := λ (f : ring_invo R), R → Rᵒᵖ, coe := λ (f : ring_invo R), f.to_ring_equiv.to_fun}

source

@[simp]

theorem ring_invo.to_fun_eq_coe {R : Type u_1} [semiring R] (f : ring_invo R) :

f.to_ring_equiv.to_fun = ⇑f

source

@[simp]

theorem ring_invo.involution {R : Type u_1} [semiring R] (f : ring_invo R) (x : R) :

opposite.unop (⇑f (opposite.unop (⇑f x))) = x

source

@[instance]

def ring_invo.has_coe_to_ring_equiv {R : Type u_1} [semiring R] :

has_coe (ring_invo R) (R ≃+* Rᵒᵖ)

Equations

ring_invo.has_coe_to_ring_equiv = {coe := ring_invo.to_ring_equiv _inst_1}

source

theorem ring_invo.coe_ring_equiv {R : Type u_1} [semiring R] (f : ring_invo R) (a : R) :

⇑↑f a = ⇑f a

source

@[simp]

theorem ring_invo.map_eq_zero_iff {R : Type u_1} [semiring R] (f : ring_invo R) {x : R} :

⇑f x = 0 ↔ x = 0

source

def ring_invo.id (R : Type u_1) [comm_ring R] :

ring_invo R

Equations

ring_invo.id R = {to_ring_equiv := {to_fun := (ring_equiv.to_opposite R).to_fun, inv_fun := (ring_equiv.to_opposite R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, involution' := _}

source

@[instance]

def ring_invo.inhabited (R : Type u_1) [comm_ring R] :

inhabited (ring_invo R)

Equations

ring_invo.inhabited R = {default := ring_invo.id R _inst_1}