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

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

    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) :

      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.

      Instances For
        instance RingInvo.instCoeTCRingInvo {R : Type u_1} {F : Type u_2} [Semiring R] [RingInvoClass F R] :

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

        def' {R : Type u_1} [Semiring R] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), MulOpposite.unop (f (MulOpposite.unop (f r))) = r) :

        Construct a ring involution from a ring homomorphism.

        Instances For
          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 (R : Type u_1) [CommRing R] :

          The identity function of a CommRing is a ring involution.

          Instances For