Documentation

Mathlib.RingTheory.RingInvo

Ring involutions #

This file defines a ring involution as a structure extending R ≃+* Rᵐᵒᵖ≃+* Rᵐᵒᵖ, with the additional fact f.involution : (f (f x).unop).unop = x.

Notations #

We provide a coercion to a function R → Rᵐᵒᵖ→ Rᵐᵒᵖ.

References #

Tags #

Ring involution

structure RingInvo (R : Type u_1) [inst : Semiring R] extends RingEquiv :
Type u_1
  • The requirement that the ring homomorphism is its own inverse

    involution' : ∀ (x : R), (Equiv.toFun toRingEquiv.toEquiv (Equiv.toFun toRingEquiv.toEquiv x).unop).unop = x

A ring involution

Instances For
    class RingInvoClass (F : Type u_1) (R : outParam (Type u_2)) [inst : Semiring R] extends RingEquivClass :
    Type (maxu_1u_2)
    • Every ring involution must be its own inverse

      involution : ∀ (f : F) (x : R), (f (f x).unop).unop = x

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

    Instances
      def RingInvoClass.toRingInvo {F : Type u_1} {R : Type u_2} [inst : Semiring R] [inst : 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
      • One or more equations did not get rendered due to their size.
      instance RingInvo.instCoeTCRingInvo {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst : RingInvoClass F R] :

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

      Equations
      • RingInvo.instCoeTCRingInvo = { coe := RingInvoClass.toRingInvo }
      Equations
      def RingInvo.mk' {R : Type u_1} [inst : Semiring R] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), (f (f r).unop).unop = 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} [inst : Semiring R] (f : RingInvo R) (x : R) :
      (f (f x).unop).unop = x
      theorem RingInvo.coe_ringEquiv {R : Type u_1} [inst : Semiring R] (f : RingInvo R) (a : R) :
      f a = f a
      theorem RingInvo.map_eq_zero_iff {R : Type u_1} [inst : Semiring R] (f : RingInvo R) {x : R} :
      f x = 0 x = 0
      def RingInvo.id (R : Type u_1) [inst : CommRing R] :

      The identity function of a CommRing is a ring involution.

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