Mathlib.RingTheory.Congruence.Opposite

Module docstring

{"# Congruences on the opposite ring

This file defines the order isomorphism between the congruences on a ring R and the congruences on the opposite ring Rᵐᵒᵖ.

RingCon.op definition

(c : RingCon R) : RingCon Rᵐᵒᵖ

Full source

/--
If `c` is a `RingCon R`, then `(a, b) ↦ c b.unop a.unop` is a `RingCon Rᵐᵒᵖ`.
-/
def op (c : RingCon R) : RingCon Rᵐᵒᵖ where
  __ := c.toCon.op
  mul' h1 h2 := c.toCon.op.mul h1 h2
  add' h1 h2 := c.add h1 h2

Ring congruence relation on the opposite ring

Informal description

Given a ring congruence relation $c$ on a ring $R$, the function $\text{RingCon.op}$ constructs a ring congruence relation on the opposite ring $R^\text{op}$ by defining $a \sim b$ if and only if $b^\text{op} \sim a^\text{op}$ under $c$. This relation preserves both addition and multiplication.

RingCon.op_iff theorem

{c : RingCon R} {x y : Rᵐᵒᵖ} : c.op x y ↔ c y.unop x.unop

Full source

lemma op_iff {c : RingCon R} {x y : Rᵐᵒᵖ} : c.op x y ↔ c y.unop x.unop := Iff.rfl

Characterization of Congruence Relation on Opposite Ring

Informal description

For any ring congruence relation $c$ on a ring $R$ and elements $x, y$ in the opposite ring $R^\text{op}$, the relation $c^\text{op}(x, y)$ holds if and only if $c(y^\text{op}, x^\text{op})$ holds in the original ring $R$.

RingCon.unop definition

(c : RingCon Rᵐᵒᵖ) : RingCon R

Full source

/--
If `c` is a `RingCon Rᵐᵒᵖ`, then `(a, b) ↦ c b.op a.op` is a `RingCon R`.
-/
def unop (c : RingCon Rᵐᵒᵖ) : RingCon R where
  __ := c.toCon.unop
  mul' h1 h2 := c.toCon.unop.mul h1 h2
  add' h1 h2 := c.add h1 h2

Ring congruence relation on the original ring from its opposite

Informal description

Given a ring congruence relation $c$ on the opposite ring $R^\text{op}$, the function $\text{RingCon.unop}$ constructs a ring congruence relation on $R$ by defining $a \sim b$ if and only if $b^\text{op} \sim a^\text{op}$ under $c$. This relation preserves both addition and multiplication.

RingCon.unop_iff theorem

{c : RingCon Rᵐᵒᵖ} {x y : R} : c.unop x y ↔ c (.op y) (.op x)

Full source

lemma unop_iff {c : RingCon Rᵐᵒᵖ} {x y : R} : c.unop x y ↔ c (.op y) (.op x) := Iff.rfl

Characterization of Unopposed Ring Congruence via Opposite Elements

Informal description

For any ring congruence relation $c$ on the opposite ring $R^\text{op}$ and any elements $x, y \in R$, the relation $c.\text{unop}(x, y)$ holds if and only if $c(y^\text{op}, x^\text{op})$ holds in $R^\text{op}$.

RingCon.opOrderIso definition

: RingCon R ≃o RingCon Rᵐᵒᵖ

Full source

/--
The congruences of a ring `R` biject to the congruences of the opposite ring `Rᵐᵒᵖ`.
-/
@[simps]
def opOrderIso : RingConRingCon R ≃o RingCon Rᵐᵒᵖ where
  toFun := op
  invFun := unop
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' {c d} := by rw [le_def, le_def]; constructor <;> intro h _ _ h' <;> exact h h'

Order isomorphism between ring congruences and opposite ring congruences

Informal description

The order isomorphism between the set of ring congruence relations on a ring $R$ and the set of ring congruence relations on its opposite ring $R^\text{op}$. Specifically, it maps a congruence relation $c$ on $R$ to the congruence relation on $R^\text{op}$ defined by $a \sim b$ if and only if $b^\text{op} \sim a^\text{op}$ under $c$, and vice versa. This bijection preserves the order structure of the congruence relations.