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
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)
:
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.
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 }
instance
RingInvo.instRingInvoClassRingInvo
{R : Type u_1}
[inst : Semiring R]
:
RingInvoClass (RingInvo R) R
Equations
- RingInvo.instRingInvoClassRingInvo = RingInvoClass.mk (_ : ∀ (f : RingInvo R) (x : R), (Equiv.toFun f.toRingEquiv.toEquiv (Equiv.toFun f.toRingEquiv.toEquiv x).unop).unop = x)
Equations
- instInhabitedRingInvoToSemiringToRing R = { default := RingInvo.id R }