# 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ᵐᵒᵖ`.

source
def RingCon.op {R : Type u_1} [Add R] [Mul R] (c : RingCon R) :
RingCon R ᵐᵒᵖ

If `c` is a `RingCon R`, then `(a, b) ↦ c b.unop a.unop` is a `RingCon Rᵐᵒᵖ`.

Equations

- c.op = { toSetoid := c.op.toSetoid, mul' := ⋯, add' := ⋯ }

Instances For

source
theorem RingCon.op_iff {R : Type u_1} [Add R] [Mul R] {c : RingCon R} {x y : R ᵐᵒᵖ} :
c.op x y ↔ c (MulOpposite.unop y) (MulOpposite.unop x)
source
def RingCon.unop {R : Type u_1} [Add R] [Mul R] (c : RingCon R ᵐᵒᵖ) :
RingCon R

If `c` is a `RingCon Rᵐᵒᵖ`, then `(a, b) ↦ c b.op a.op` is a `RingCon R`.

Equations

- c.unop = { toSetoid := c.unop.toSetoid, mul' := ⋯, add' := ⋯ }

Instances For

source
theorem RingCon.unop_iff {R : Type u_1} [Add R] [Mul R] {c : RingCon R ᵐᵒᵖ} {x y : R} :
c.unop x y ↔ c (MulOpposite.op y) (MulOpposite.op x)
source
def RingCon.opOrderIso {R : Type u_1} [Add R] [Mul R] :
RingCon R ≃o RingCon R ᵐᵒᵖ

The congruences of a ring `R` biject to the congruences of the opposite ring `Rᵐᵒᵖ`.

Equations

- RingCon.opOrderIso = { toFun := RingCon.op, invFun := RingCon.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem RingCon.opOrderIso_symm_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon R ᵐᵒᵖ) :
(RelIso.symm opOrderIso) c = c.unop
source
@[simp]
theorem RingCon.opOrderIso_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon R) :
opOrderIso c = c.op