Module docstring
{"# 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ᵒᵖ.
"}
Con.op
definition
(c : Con M) : Con Mᵐᵒᵖ
Full source
/-- If `c` is a multiplicative congruence on `M`, then `(a, b) ↦ c b.unop a.unop` is a
multiplicative congruence on `Mᵐᵒᵖ`. -/
@[to_additive "If `c` is an additive congruence on `M`, then `(a, b) ↦ c b.unop a.unop` is an
additive congruence on `Mᵃᵒᵖ`"]
def op (c : Con M) : Con Mᵐᵒᵖ where
r a b := c b.unop a.unop
iseqv :=
{ refl := fun a ↦ c.refl a.unop
symm := c.symm
trans := fun h1 h2 ↦ c.trans h2 h1 }
mul' h1 h2 := c.mul h2 h1Informal description
Given a multiplicative congruence relation $c$ on a multiplicative structure $M$, the function $\text{Con.op}$ constructs a multiplicative congruence relation on the opposite structure $M^\text{op}$ by defining $a \sim b$ if and only if $b^\text{op} \sim a^\text{op}$ under $c$. This relation is reflexive, symmetric, transitive, and preserves multiplication.
Con.unop
definition
(c : Con Mᵐᵒᵖ) : Con M
Full source
/-- If `c` is a multiplicative congruence on `Mᵐᵒᵖ`, then `(a, b) ↦ c bᵒᵖ aᵒᵖ` is a multiplicative
congruence on `M`. -/
@[to_additive "If `c` is an additive congruence on `Mᵃᵒᵖ`, then `(a, b) ↦ c bᵒᵖ aᵒᵖ` is an additive
congruence on `M`"]
def unop (c : Con Mᵐᵒᵖ) : Con M where
r a b := c (.op b) (.op a)
iseqv :=
{ refl := fun a ↦ c.refl (.op a)
symm := c.symm
trans := fun h1 h2 ↦ c.trans h2 h1 }
mul' h1 h2 := c.mul h2 h1Informal description
Given a multiplicative congruence relation $c$ on the opposite group $M^\text{op}$, the function $\text{Con.unop}$ constructs a multiplicative congruence relation on $M$ by defining $a \sim b$ if and only if $b^\text{op} \sim a^\text{op}$ under $c$. This relation is reflexive, symmetric, transitive, and preserves multiplication.
Con.orderIsoOp
definition
: Con M ≃o Con Mᵐᵒᵖ
Full source
/--
The multiplicative congruences on `M` bijects to the multiplicative congruences on `Mᵐᵒᵖ`
-/
@[to_additive (attr := simps) "The additive congruences on `M` bijects to the additive congruences
on `Mᵃᵒᵖ`"]
def orderIsoOp : ConCon M ≃o Con Mᵐᵒᵖ where
toFun := op
invFun := unop
left_inv _ := rfl
right_inv _ := rfl
map_rel_iff' {c d} := by rw [le_def, le_def]; constructor <;> intro h _ _ h' <;> exact h h'Informal description
The order isomorphism between the set of congruence relations on a multiplicative structure $M$ and the set of congruence relations on its opposite structure $M^\text{op}$. The isomorphism maps a congruence relation $c$ on $M$ to its opposite version $\text{op}(c)$ on $M^\text{op}$, and vice versa via $\text{unop}$. This bijection preserves the partial order structure, meaning $c \leq d$ if and only if $\text{op}(c) \leq \text{op}(d)$ for any two congruence relations $c$ and $d$ on $M$.