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

source
ink
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
    source
    ink
    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
      source
      ink
      def RingInvoClass.toRingInvo {F : Type u_1} {R : Type u_2} [inst : Semiring R] [inst : 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
      • One or more equations did not get rendered due to their size.
      source
      ink
      instance RingInvo.instCoeTCRingInvo {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst : 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 }
      source
      ink
      instance RingInvo.instRingInvoClassRingInvo {R : Type u_1} [inst : Semiring R] :
      RingInvoClass (RingInvo R) R
      Equations
      source
      ink
      def RingInvo.mk' {R : Type u_1} [inst : Semiring R] (f : R →+* Rᵐᵒᵖ) (involution : ∀ (r : R), (↑f (↑f r).unop).unop = r) :
      RingInvo R

      Construct a ring involution from a ring homomorphism.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      @[simp]
      theorem RingInvo.involution {R : Type u_1} [inst : Semiring R] (f : RingInvo R) (x : R) :
      (↑f (↑f x).unop).unop = x
      source
      ink
      theorem RingInvo.coe_ringEquiv {R : Type u_1} [inst : Semiring R] (f : RingInvo R) (a : R) :
      ↑↑f a = ↑f a
      source
      ink
      theorem RingInvo.map_eq_zero_iff {R : Type u_1} [inst : Semiring R] (f : RingInvo R) {x : R} :
      ↑f x = 0 ↔ x = 0
      source
      ink
      def RingInvo.id (R : Type u_1) [inst : 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.
      source
      ink
      instance instInhabitedRingInvoToSemiringToRing (R : Type u_1) [inst : CommRing R] :
      Inhabited (RingInvo R)
      Equations