Ring antihomomorphisms, isomorphisms, antiisomorphisms and involutions
This file defines ring antihomomorphisms, antiisomorphism and involutions and proves basic properties of them.
Notations
All types defined in this file are given a coercion to the underlying function.
References
- https://en.wikipedia.org/wiki/Antihomomorphism
- https://en.wikipedia.org/wiki/Involution_(mathematics)#Ring_theory
Tags
Ring isomorphism, automorphism, antihomomorphism, antiisomorphism, antiautomorphism, involution
- to_ring_equiv : R ≃+* Rᵒᵖ
- involution' : ∀ (x : R), opposite.unop (c.to_ring_equiv.to_fun (opposite.unop (c.to_ring_equiv.to_fun x))) = x
A ring involution
def
ring_invo.mk'
{R : Type u_1}
[semiring R]
(f : R →+* Rᵒᵖ) :
(∀ (r : R), opposite.unop (⇑f (opposite.unop (⇑f r))) = r) → ring_invo 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ᵒᵖ), opposite.unop (⇑f (opposite.unop r)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}, involution' := involution}
@[instance]
Equations
- ring_invo.has_coe_to_fun = {F := λ (f : ring_invo R), R → Rᵒᵖ, 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
@[instance]
Equations
- ring_invo.has_coe_to_ring_equiv = {coe := ring_invo.to_ring_equiv _inst_1}
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' := _}
@[instance]
Equations
- ring_invo.inhabited R = {default := ring_invo.id R _inst_1}