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

Tags

Ring involution

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

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.toEquiv.toFun (x * y) = self.toEquiv.toFun x * self.toEquiv.toFun y
• map_add' : ∀ (x y : R), self.toEquiv.toFun (x + y) = self.toEquiv.toFun x + self.toEquiv.toFun y
• involution' : ∀ (x : R), MulOpposite.unop (self.toEquiv.toFun (MulOpposite.unop (self.toEquiv.toFun x))) = x

  The requirement that the ring homomorphism is its own inverse

class RingInvoClass (F : Type u_2) (R : Type u_3) [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

def RingInvoClass.toRingInvo {F : Type u_2} {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' := (_ : ∀ (x : R), MulOpposite.unop (f (MulOpposite.unop (f x))) = x) }

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : RingInvoClass (RingInvo R) 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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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