Documentation

Mathlib.RingTheory.Congruence.Opposite

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) :

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
    theorem RingCon.op_iff {R : Type u_1} [Add R] [Mul R] {c : RingCon R} {x : Rᵐᵒᵖ} {y : Rᵐᵒᵖ} :
    def RingCon.unop {R : Type u_1} [Add R] [Mul R] (c : 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
      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)
      @[simp]
      theorem RingCon.opOrderIso_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon R) :
      RingCon.opOrderIso c = c.op
      @[simp]
      theorem RingCon.opOrderIso_symm_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon Rᵐᵒᵖ) :
      (RelIso.symm RingCon.opOrderIso) c = c.unop

      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