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

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

A ring involution

• toFun : R → Rᵐᵒᵖ
• invFun : Rᵐᵒᵖ → R
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
• map_add' : ∀ (x y : R), self.toFun (x + y) = self.toFun x + self.toFun y
• involution' : ∀ (x : R), MulOpposite.unop (self.toFun (MulOpposite.unop (self.toFun x))) = x

  The requirement that the ring homomorphism is its own inverse

theorem RingInvo.involution' {R : Type u_2} [Semiring R] (self : RingInvo R) (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) [Semiring R] [EquivLike F R Rᵐᵒᵖ] extends RingEquivClass : Prop

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

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

Every ring involution must be its own inverse

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

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' := ⋯ }

instance RingInvo.instCoeTCOfRingInvoClass {F : Type u_1} {R : Type u_2} [Semiring R] [EquivLike F R Rᵐᵒᵖ] [RingInvoClass F R] : CoeTC F (RingInvo R)

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

Equations

• RingInvo.instCoeTCOfRingInvoClass = { coe := RingInvoClass.toRingInvo }

instance RingInvo.instEquivLikeMulOpposite {R : Type u_2} [Semiring R] : EquivLike (RingInvo R) R Rᵐᵒᵖ

Equations

• RingInvo.instEquivLikeMulOpposite = { coe := fun (f : RingInvo R) => f.toFun, inv := fun (f : RingInvo R) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance RingInvo.instRingInvoClass {R : Type u_2} [Semiring R] : RingInvoClass (RingInvo R) R

Equations

• ⋯ = ⋯

def RingInvo.mk' {R : Type u_2} [Semiring R] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), MulOpposite.unop (f (MulOpposite.unop (f r))) = r) : RingInvo 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_2} [Semiring R] (f : RingInvo R) (x : R) : MulOpposite.unop (f (MulOpposite.unop (f x))) = x

theorem RingInvo.coe_ringEquiv {R : Type u_2} [Semiring R] (f : RingInvo R) (a : R) : ↑f a = f a

theorem RingInvo.map_eq_zero_iff {R : Type u_2} [Semiring R] (f : RingInvo R) {x : R} : f x = 0 ↔ x = 0

def RingInvo.id (R : Type u_2) [CommRing R] : RingInvo R

The identity function of a CommRing is a ring involution.

Equations

• RingInvo.id R = let __src := RingEquiv.toOpposite R; { toRingEquiv := __src, involution' := ⋯ }

instance instInhabitedRingInvo (R : Type u_2) [CommRing R] : Inhabited (RingInvo R)

Equations

• instInhabitedRingInvo R = { default := RingInvo.id R }