Lean4
/-- Given a congruence relation `c` on a type `M` with a multiplication, the order-preserving
bijection between the set of congruence relations containing `c` and the congruence relations
on the quotient of `M` by `c`. -/
@[to_additive /-- Given an additive congruence relation `c` on a type `M` with an addition,
the order-preserving bijection between the set of additive congruence relations containing `c` and
the additive congruence relations on the quotient of `M` by `c`. -/
]
def correspondence {c : Con M} : { d // c ≤ d } ≃o Con c.Quotient
where
toFun d := d.1.mapOfSurjective (mkMulHom c) (by rw [Con.ker_mkMulHom_eq]; exact d.2) <| Quotient.mk_surjective
invFun
d := ⟨comap ((↑) : M → c.Quotient) (fun _ _ => rfl) d, fun x y h => show d x y by rw [c.eq.2 h]; exact d.refl _⟩
left_inv
d :=
Subtype.ext_iff.2 <|
ext fun x y =>
⟨fun ⟨a, b, H, hx, hy⟩ => d.1.trans (d.1.symm <| d.2 <| c.eq.1 hx) <| d.1.trans H <| d.2 <| c.eq.1 hy, fun h =>
⟨_, _, h, rfl, rfl⟩⟩
right_inv
d := ext fun x y => ⟨fun ⟨_, _, H, hx, hy⟩ => hx ▸ hy ▸ H, Con.induction_on₂ x y fun w z h => ⟨w, z, h, rfl, rfl⟩⟩
map_rel_iff'
{s t} := by
constructor
· intro h x y hs
rcases h ⟨x, y, hs, rfl, rfl⟩ with ⟨a, b, ht, hx, hy⟩
exact t.1.trans (t.1.symm <| t.2 <| c.eq.1 hx) (t.1.trans ht (t.2 <| c.eq.1 hy))
· exact Relation.map_mono
