Ring involutions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_fun : R → Rᵐᵒᵖ
inv_fun : Rᵐᵒᵖ → 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
involution' : ∀ (x : R), mul_opposite.unop (self.to_fun (mul_opposite.unop (self.to_fun x))) = x

A ring involution

Instances for ring_invo

source

def ring_invo.to_ring_equiv {R : Type u_1} [semiring R] (self : ring_invo R) :

R ≃+* Rᵐᵒᵖ

The equivalence of rings underlying a ring involution.

source

@[instance]

def ring_invo_class.to_ring_equiv_class (F : Type u_2) (R : out_param (Type u_3)) [semiring R] [self : ring_invo_class F R] :

ring_equiv_class F R Rᵐᵒᵖ

source

@[class]

structure ring_invo_class (F : Type u_2) (R : out_param (Type u_3)) [semiring R] :

Type (max u_2 u_3)

coe : F → R → Rᵐᵒᵖ
inv : F → Rᵐᵒᵖ → R
left_inv : ∀ (e : F), function.left_inverse (ring_invo_class.inv e) (ring_invo_class.coe e)
right_inv : ∀ (e : F), function.right_inverse (ring_invo_class.inv e) (ring_invo_class.coe e)
coe_injective' : ∀ (e g : F), ring_invo_class.coe e = ring_invo_class.coe g → ring_invo_class.inv e = ring_invo_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
involution : ∀ (f : F) (x : R), mul_opposite.unop (⇑f (mul_opposite.unop (⇑f x))) = x

ring_invo_class F R S states that F is a type of ring involutions. You should extend this class when you extend ring_invo.

Instances of this typeclass

ring_invo.ring_invo_class

Instances of other typeclasses for ring_invo_class

ring_invo_class.has_sizeof_inst

source

@[protected, instance]

def ring_invo.ring_invo_class (R : Type u_1) [semiring R] :

ring_invo_class (ring_invo R) R

Equations

ring_invo.ring_invo_class R = {coe := ring_invo.to_fun _inst_2, inv := ring_invo.inv_fun _inst_2, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _, map_add := _, involution := _}

source

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

ring_invo R

Construct a ring involution from a ring homomorphism.

Equations

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

source

@[protected, instance]

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

has_coe_to_fun (ring_invo R) (λ (_x : ring_invo R), R → Rᵐᵒᵖ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

ring_invo.has_coe_to_fun = {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_fun = ⇑f

source

@[simp]

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

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

source

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

@[norm_cast]

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

@[protected]

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

ring_invo R

The identity function of a comm_ring is a ring involution.

Equations

ring_invo.id R = {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

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