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

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' := ⋯ }

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

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' := ⋯ }

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

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' := ⋯ }

@[simp]

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

@[simp]

theorem RingCon.opOrderIso_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon R) : RingCon.opOrderIso c = c.op