# 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ᵐᵒᵖ.

## Tags #

Ring involution

structure RingInvo (R : Type u_2) [] extends :
Type u_2

A ring involution

Instances For
theorem RingInvo.involution' {R : Type u_2} [] (self : ) (x : R) :
MulOpposite.unop (self.toFun (MulOpposite.unop (self.toFun x))) = x

The requirement that the ring homomorphism is its own inverse

class RingInvoClass (F : Type u_3) (R : Type u_4) [] [EquivLike F R Rᵐᵒᵖ] extends :

RingInvoClass F R states that F is a type of ring involutions. You should extend this class when you extend RingInvo.

• 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), MulOpposite.unop (f (MulOpposite.unop (f x))) = x

Every ring involution must be its own inverse

Instances
theorem RingInvoClass.involution {F : Type u_3} {R : Type u_4} [] [EquivLike F R Rᵐᵒᵖ] [self : ] (f : F) (x : R) :

Every ring involution must be its own inverse

def RingInvoClass.toRingInvo {F : Type u_1} {R : Type u_3} [] [EquivLike F R Rᵐᵒᵖ] [] (f : F) :

Turn an element of a type F satisfying RingInvoClass F R into an actual RingInvo. This is declared as the default coercion from F to RingInvo R.

Equations
• f = let __src := f; { toRingEquiv := __src, involution' := }
Instances For
instance RingInvo.instCoeTCOfRingInvoClass {F : Type u_1} {R : Type u_2} [] [EquivLike F R Rᵐᵒᵖ] [] :
CoeTC F ()

Any type satisfying RingInvoClass can be cast into RingInvo via RingInvoClass.toRingInvo.

Equations
• RingInvo.instCoeTCOfRingInvoClass = { coe := RingInvoClass.toRingInvo }
Equations
• RingInvo.instEquivLikeMulOpposite = { coe := fun (f : ) => f.toFun, inv := fun (f : ) => f.invFun, left_inv := , right_inv := , coe_injective' := }
instance RingInvo.instRingInvoClass {R : Type u_2} [] :
Equations
• =
def RingInvo.mk' {R : Type u_2} [] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), MulOpposite.unop (f (MulOpposite.unop (f r))) = r) :

Construct a ring involution from a ring homomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem RingInvo.involution {R : Type u_2} [] (f : ) (x : R) :
theorem RingInvo.coe_ringEquiv {R : Type u_2} [] (f : ) (a : R) :
f a = f a
theorem RingInvo.map_eq_zero_iff {R : Type u_2} [] (f : ) {x : R} :
f x = 0 x = 0
def RingInvo.id (R : Type u_2) [] :

The identity function of a CommRing is a ring involution.

Equations
• = let __src := ; { toRingEquiv := __src, involution' := }
Instances For
instance instInhabitedRingInvo (R : Type u_2) [] :
Equations
• = { default := }