# Documentation

Mathlib.RingTheory.RingInvo

# Ring involutions #

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

## Notations #

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

## Tags #

Ring involution

structure RingInvo (R : Type u_1) [inst : ] extends :
Type u_1
• The requirement that the ring homomorphism is its own inverse

involution' : ∀ (x : R), (Equiv.toFun toRingEquiv.toEquiv (Equiv.toFun toRingEquiv.toEquiv x).unop).unop = x

A ring involution

Instances For
class RingInvoClass (F : Type u_1) (R : outParam (Type u_2)) [inst : ] extends :
Type (maxu_1u_2)
• Every ring involution must be its own inverse

involution : ∀ (f : F) (x : R), (f (f x).unop).unop = x

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

Instances
def RingInvoClass.toRingInvo {F : Type u_1} {R : Type u_2} [inst : ] [inst : ] (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
• One or more equations did not get rendered due to their size.
instance RingInvo.instCoeTCRingInvo {R : Type u_1} {F : Type u_2} [inst : ] [inst : ] :
CoeTC F ()

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

Equations
• RingInvo.instCoeTCRingInvo = { coe := RingInvoClass.toRingInvo }
instance RingInvo.instRingInvoClassRingInvo {R : Type u_1} [inst : ] :
Equations
def RingInvo.mk' {R : Type u_1} [inst : ] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), (f (f r).unop).unop = r) :

Construct a ring involution from a ring homomorphism.

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

The identity function of a CommRing is a ring involution.

Equations
• One or more equations did not get rendered due to their size.
instance instInhabitedRingInvoToSemiringToRing (R : Type u_1) [inst : ] :
Equations
• = { default := }