mathlib documentation

ring_theory.ring_invo

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

structure ring_invo (R : Type u_1) [semiring R] :
Type u_1

A ring involution

def ring_invo.mk' {R : Type u_1} [semiring R] (f : R →+* Rᵒᵖ) (involution : ∀ (r : R), opposite.unop (f (opposite.unop (f r))) = r) :

Construct a ring involution from a ring homomorphism.

Equations
@[instance]
Equations
@[simp]
theorem ring_invo.to_fun_eq_coe {R : Type u_1} [semiring R] (f : ring_invo R) :
@[simp]
theorem ring_invo.involution {R : Type u_1} [semiring R] (f : ring_invo R) (x : R) :
theorem ring_invo.coe_ring_equiv {R : Type u_1} [semiring R] (f : ring_invo R) (a : R) :
f a = f a
@[simp]
theorem ring_invo.map_eq_zero_iff {R : Type u_1} [semiring R] (f : ring_invo R) {x : R} :
f x = 0 x = 0
def ring_invo.id (R : Type u_1) [comm_ring R] :

The identity function of a comm_ring is a ring involution.

Equations
@[instance]
def ring_invo.inhabited (R : Type u_1) [comm_ring R] :
Equations