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_1) [Semiring R] extends RingEquiv : Type u_1

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

  The requirement that the ring homomorphism is its own inverse

A ring involution

class RingInvoClass (F : Type u_2) (R : outParam (Type u_3)) [Semiring R] extends RingEquivClass : Type (max u_2 u_3)

• coe : F → R → Rᵐᵒᵖ
• inv : F → Rᵐᵒᵖ → R
• left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
• right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
• coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.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), MulOpposite.unop (↑f (MulOpposite.unop (↑f x))) = x

  Every ring involution must be its own inverse

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

def RingInvoClass.toRingInvo {F : Type u_2} {R : Type u_3} [Semiring 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.

instance RingInvo.instCoeTCRingInvo {R : Type u_1} {F : Type u_2} [Semiring R] [RingInvoClass F R] : CoeTC F (RingInvo R)

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

instance RingInvo.instRingInvoClassRingInvo {R : Type u_1} [Semiring R] : RingInvoClass (RingInvo R) R

def RingInvo.mk' {R : Type u_1} [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.

@[simp]

theorem RingInvo.involution {R : Type u_1} [Semiring R] (f : RingInvo R) (x : R) : MulOpposite.unop (↑f (MulOpposite.unop (↑f x))) = x

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

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

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

The identity function of a CommRing is a ring involution.

instance instInhabitedRingInvoToSemiringToCommSemiring (R : Type u_1) [CommRing R] : Inhabited (RingInvo R)