Opposite rings

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-04-22.
Last modified on 2025-10-31.

module ring-theory.opposite-rings where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import ring-theory.rings

Idea

The opposite of a ring R is a ring with the same underlying abelian group, but with multiplication given by x·y := yx.

Definition

module _
  {l : Level} (R : Ring l)
  where

  op-Ring : Ring l
  pr1 op-Ring = ab-Ring R
  pr1 (pr1 (pr2 op-Ring)) = mul-Ring' R
  pr2 (pr1 (pr2 op-Ring)) x y z = inv (associative-mul-Ring R z y x)
  pr1 (pr1 (pr2 (pr2 op-Ring))) = one-Ring R
  pr1 (pr2 (pr1 (pr2 (pr2 op-Ring)))) = right-unit-law-mul-Ring R
  pr2 (pr2 (pr1 (pr2 (pr2 op-Ring)))) = left-unit-law-mul-Ring R
  pr1 (pr2 (pr2 (pr2 op-Ring))) x y z = right-distributive-mul-add-Ring R y z x
  pr2 (pr2 (pr2 (pr2 op-Ring))) x y z = left-distributive-mul-add-Ring R z x y

Recent changes