Congruences on the opposite of a group

This file defines the order isomorphism between the congruences on a group G and the congruences on the opposite group Gᵒᵖ.

def Con.op {M : Type u_1} [Mul M] (c : Con M) : Con Mᵐᵒᵖ

If c is a multiplicative congruence on M, then (a, b) ↦ c b.unop a.unop is a multiplicative congruence on Mᵐᵒᵖ.

def AddCon.op {M : Type u_1} [Add M] (c : AddCon M) : AddCon Mᵃᵒᵖ

If c is an additive congruence on M, then (a, b) ↦ c b.unop a.unop is an additive congruence on Mᵃᵒᵖ

def Con.unop {M : Type u_1} [Mul M] (c : Con Mᵐᵒᵖ) : Con M

If c is a multiplicative congruence on Mᵐᵒᵖ, then (a, b) ↦ c bᵒᵖ aᵒᵖ is a multiplicative congruence on M.

def AddCon.unop {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) : AddCon M

If c is an additive congruence on Mᵃᵒᵖ, then (a, b) ↦ c bᵒᵖ aᵒᵖ is an additive congruence on M.

def Con.orderIsoOp {M : Type u_1} [Mul M] : Con M ≃o Con Mᵐᵒᵖ

The multiplicative congruences on M bijects to the multiplicative congruences on Mᵐᵒᵖ

def AddCon.orderIsoOp {M : Type u_1} [Add M] : AddCon M ≃o AddCon Mᵃᵒᵖ

The additive congruences on M bijects to the additive congruences on Mᵃᵒᵖ

@[simp]

theorem AddCon.orderIsoOp_symm_apply {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) : (RelIso.symm orderIsoOp) c = c.unop

@[simp]

theorem Con.orderIsoOp_symm_apply {M : Type u_1} [Mul M] (c : Con Mᵐᵒᵖ) : (RelIso.symm orderIsoOp) c = c.unop

@[simp]

theorem AddCon.orderIsoOp_apply {M : Type u_1} [Add M] (c : AddCon M) : orderIsoOp c = c.op

@[simp]

theorem Con.orderIsoOp_apply {M : Type u_1} [Mul M] (c : Con M) : orderIsoOp c = c.op