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
- toFun : R → Rᵐᵒᵖ
- invFun : Rᵐᵒᵖ → R
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_mul' : ∀ (x y : R), Equiv.toFun s.toEquiv (x * y) = Equiv.toFun s.toEquiv x * Equiv.toFun s.toEquiv y
- map_add' : ∀ (x y : R), Equiv.toFun s.toEquiv (x + y) = Equiv.toFun s.toEquiv x + Equiv.toFun s.toEquiv y
- involution' : ∀ (x : R), MulOpposite.unop (Equiv.toFun s.toEquiv (MulOpposite.unop (Equiv.toFun s.toEquiv x))) = x
The requirement that the ring homomorphism is its own inverse
A ring involution
Instances For
- coe : F → R → Rᵐᵒᵖ
- inv : F → Rᵐᵒᵖ → R
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
- involution : ∀ (f : F) (x : R), MulOpposite.unop (↑f (MulOpposite.unop (↑f x))) = x
Every ring involution must be its own inverse
RingInvoClass F R
states that F
is a type of ring involutions.
You should extend this class when you extend RingInvo
.
Instances
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
Any type satisfying RingInvoClass
can be cast into RingInvo
via
RingInvoClass.toRingInvo
.
Construct a ring involution from a ring homomorphism.