Documentation

Mathlib.RingTheory.RingInvo

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

A ring involution

Instances For
    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 :

    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

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

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

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

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

        Equations
        • RingInvo.instCoeTCOfRingInvoClass = { coe := RingInvoClass.toRingInvo }
        Equations
        • RingInvo.instEquivLikeMulOpposite = { coe := fun (f : RingInvo R) => f.toFun, inv := fun (f : RingInvo R) => f.invFun, left_inv := , right_inv := , coe_injective' := }
        Equations
        • =
        def RingInvo.mk' {R : Type u_2} [Semiring R] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), MulOpposite.unop (f (MulOpposite.unop (f r))) = r) :

        Construct a ring involution from a ring homomorphism.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem RingInvo.involution {R : Type u_2} [Semiring R] (f : RingInvo R) (x : R) :
          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] :

          The identity function of a CommRing is a ring involution.

          Equations
          Instances For
            Equations