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

theorem AddCon.op.proof_1 {M : Type u_1} [Add M] (c : AddCon M) : Equivalence fun (a b : Mᵃᵒᵖ) => c (AddOpposite.unop b) (AddOpposite.unop a)

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ᵃᵒᵖ

Equations

• c.op = { r := fun (a b : Mᵃᵒᵖ) => c (AddOpposite.unop b) (AddOpposite.unop a), iseqv := ⋯, add' := ⋯ }

theorem AddCon.op.proof_2 {M : Type u_1} [Add M] (c : AddCon M) : ∀ {w x y z : Mᵃᵒᵖ}, { r := fun (a b : Mᵃᵒᵖ) => c (AddOpposite.unop b) (AddOpposite.unop a), iseqv := ⋯ } w x → { r := fun (a b : Mᵃᵒᵖ) => c (AddOpposite.unop b) (AddOpposite.unop a), iseqv := ⋯ } y z → c (AddOpposite.unop z + AddOpposite.unop x) (AddOpposite.unop y + AddOpposite.unop w)

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

Equations

• c.op = { r := fun (a b : Mᵐᵒᵖ) => c (MulOpposite.unop b) (MulOpposite.unop a), iseqv := ⋯, mul' := ⋯ }

theorem AddCon.unop.proof_1 {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) : Equivalence fun (a b : M) => c (AddOpposite.op b) (AddOpposite.op a)

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

Equations

• c.unop = { r := fun (a b : M) => c (AddOpposite.op b) (AddOpposite.op a), iseqv := ⋯, add' := ⋯ }

theorem AddCon.unop.proof_2 {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) : ∀ {w x y z : M}, { r := fun (a b : M) => c (AddOpposite.op b) (AddOpposite.op a), iseqv := ⋯ } w x → { r := fun (a b : M) => c (AddOpposite.op b) (AddOpposite.op a), iseqv := ⋯ } y z → c ({ unop' := z } + { unop' := x }) ({ unop' := y } + { unop' := w })

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

Equations

• c.unop = { r := fun (a b : M) => c (MulOpposite.op b) (MulOpposite.op a), iseqv := ⋯, mul' := ⋯ }

theorem AddCon.orderIsoOp.proof_3 {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} : { toFun := AddCon.op, invFun := AddCon.unop, left_inv := ⋯, right_inv := ⋯ } c ≤ { toFun := AddCon.op, invFun := AddCon.unop, left_inv := ⋯, right_inv := ⋯ } d ↔ c ≤ d

theorem AddCon.orderIsoOp.proof_2 {M : Type u_1} [Add M] : ∀ (x : AddCon Mᵃᵒᵖ), x.unop.op = x.unop.op

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ᵃᵒᵖ

Equations

• AddCon.orderIsoOp = { toFun := AddCon.op, invFun := AddCon.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem AddCon.orderIsoOp.proof_1 {M : Type u_1} [Add M] : ∀ (x : AddCon M), x.op.unop = x.op.unop

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• Con.orderIsoOp = { toFun := Con.op, invFun := Con.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }