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
- to_ring_equiv : R ≃+* Rᵐᵒᵖ
- involution' : ∀ (x : R), mul_opposite.unop (self.to_ring_equiv.to_fun (mul_opposite.unop (self.to_ring_equiv.to_fun x))) = x
A ring involution
Instances for ring_invo
- ring_invo.has_sizeof_inst
- ring_invo.has_coe_to_fun
- ring_invo.has_coe_to_ring_equiv
- ring_invo.inhabited
def
ring_invo.mk'
{R : Type u_1}
[semiring R]
(f : R →+* Rᵐᵒᵖ)
(involution : ∀ (r : R), mul_opposite.unop (⇑f (mul_opposite.unop (⇑f r))) = r) :
Construct a ring involution from a ring homomorphism.
Equations
- ring_invo.mk' f involution = {to_ring_equiv := {to_fun := f.to_fun, inv_fun := λ (r : Rᵐᵒᵖ), mul_opposite.unop (⇑f (mul_opposite.unop r)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, involution' := involution}
@[protected, instance]
def
ring_invo.has_coe_to_fun
{R : Type u_1}
[semiring R] :
has_coe_to_fun (ring_invo R) (λ (_x : ring_invo R), R → Rᵐᵒᵖ)
Equations
- ring_invo.has_coe_to_fun = {coe := λ (f : ring_invo R), f.to_ring_equiv.to_fun}
@[simp]
theorem
ring_invo.to_fun_eq_coe
{R : Type u_1}
[semiring R]
(f : ring_invo R) :
f.to_ring_equiv.to_fun = ⇑f
@[simp]
theorem
ring_invo.involution
{R : Type u_1}
[semiring R]
(f : ring_invo R)
(x : R) :
mul_opposite.unop (⇑f (mul_opposite.unop (⇑f x))) = x
@[protected, instance]
Equations
- ring_invo.has_coe_to_ring_equiv = {coe := ring_invo.to_ring_equiv _inst_1}
@[protected]
The identity function of a comm_ring
is a ring involution.
Equations
- ring_invo.id R = {to_ring_equiv := {to_fun := (ring_equiv.to_opposite R).to_fun, inv_fun := (ring_equiv.to_opposite R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, involution' := _}
@[protected, instance]
Equations
- ring_invo.inhabited R = {default := ring_invo.id R _inst_1}