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

Tags

Ring isomorphism, automorphism, antihomomorphism, antiisomorphism, antiautomorphism, involution

@[class]
structure is_ring_anti_hom {R : Type u_1} {F : Type u_2} [ring R] [ring F] :
(R → F) → Prop
  • map_one : f 1 = 1
  • map_mul : ∀ {x y : R}, f (x * y) = f y * f x
  • map_add : ∀ {x y : R}, f (x + y) = f x + f y

Instances
@[instance]
def is_ring_anti_hom.is_add_group_hom {R : Type u_1} {F : Type u_2} [ring R] [ring F] (f : R → F) [is_ring_anti_hom f] :

Equations
theorem is_ring_anti_hom.map_zero {R : Type u_1} {F : Type u_2} [ring R] [ring F] (f : R → F) [is_ring_anti_hom f] :
f 0 = 0

theorem is_ring_anti_hom.map_neg {R : Type u_1} {F : Type u_2} [ring R] [ring F] (f : R → F) [is_ring_anti_hom f] {x : R} :
f (-x) = -f x

theorem is_ring_anti_hom.map_sub {R : Type u_1} {F : Type u_2} [ring R] [ring F] (f : R → F) [is_ring_anti_hom f] {x y : R} :
f (x - y) = f x - f y

theorem ring_equiv.bijective {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : R ≃+* F) :

theorem ring_equiv.map_zero_iff {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : R ≃+* F) {x : R} :
Hs x = 0 x = 0

structure ring_anti_equiv (R : Type u_1) (F : Type u_2) [ring R] [ring F] :
Type (max u_1 u_2)

A ring antiisomorphism

@[instance]
def ring_anti_equiv.has_coe_to_fun {R : Type u_1} {F : Type u_2} [ring R] [ring F] :

Equations
@[instance]
def ring_anti_equiv.is_ring_anti_hom {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) :

Equations
  • _ = _
theorem ring_anti_equiv.map_add {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) (x y : R) :
Hs (x + y) = Hs x + Hs y

theorem ring_anti_equiv.map_zero {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) :
Hs 0 = 0

theorem ring_anti_equiv.map_neg {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) (x : R) :
Hs (-x) = -Hs x

theorem ring_anti_equiv.map_sub {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) (x y : R) :
Hs (x - y) = Hs x - Hs y

theorem ring_anti_equiv.map_mul {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) (x y : R) :
Hs (x * y) = Hs y * Hs x

theorem ring_anti_equiv.map_one {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) :
Hs 1 = 1

theorem ring_anti_equiv.map_neg_one {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) :
Hs (-1) = -1

theorem ring_anti_equiv.bijective {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) :

theorem ring_anti_equiv.map_zero_iff {R : Type u_1} {F : Type u_2} [ring R] [ring F] (Hs : ring_anti_equiv R F) {x : R} :
Hs x = 0 x = 0

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

A ring involution

@[instance]

Equations
@[instance]
def ring_invo.is_ring_anti_hom {R : Type u_1} [ring R] (Hi : ring_invo R) :

Equations
  • _ = _
theorem ring_invo.map_add {R : Type u_1} [ring R] (Hi : ring_invo R) (x y : R) :
Hi (x + y) = Hi x + Hi y

theorem ring_invo.map_zero {R : Type u_1} [ring R] (Hi : ring_invo R) :
Hi 0 = 0

theorem ring_invo.map_neg {R : Type u_1} [ring R] (Hi : ring_invo R) (x : R) :
Hi (-x) = -Hi x

theorem ring_invo.map_sub {R : Type u_1} [ring R] (Hi : ring_invo R) (x y : R) :
Hi (x - y) = Hi x - Hi y

theorem ring_invo.map_mul {R : Type u_1} [ring R] (Hi : ring_invo R) (x y : R) :
Hi (x * y) = Hi y * Hi x

theorem ring_invo.map_one {R : Type u_1} [ring R] (Hi : ring_invo R) :
Hi 1 = 1

theorem ring_invo.map_neg_one {R : Type u_1} [ring R] (Hi : ring_invo R) :
Hi (-1) = -1

theorem ring_invo.bijective {R : Type u_1} [ring R] (Hi : ring_invo R) :

theorem ring_invo.map_zero_iff {R : Type u_1} [ring R] (Hi : ring_invo R) {x : R} :
Hi x = 0 x = 0

def ring_invo.id (R : Type u_1) [comm_ring R] :

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

Equations
theorem comm_ring.hom_to_anti_hom {R : Type u_1} {F : Type u_2} [comm_ring R] [comm_ring F] (f : R → F) [is_ring_hom f] :

theorem comm_ring.anti_hom_to_hom {R : Type u_1} {F : Type u_2} [comm_ring R] [comm_ring F] (f : R → F) [is_ring_anti_hom f] :