feat(RingTheory/Congruence): interpret `RingCon` as two sided ideals

[jjaassoonn]

In this PR, we set up an instance SetLike (RingCon R) R for any NonUnitalNonAssocRing R. This enables us to interpret RingCon R as two-sided-ideals.

Co-authored-by: Eric Wieser <@eric-wieser>

---

• [x] depends on: #13610
• [x] depends on: #13730
• [x] depends on: #13902
• [ ] depends on: #14453

[jjaassoonn]

Thanks for the quick response!

[eric-wieser]

~~Defining RingCon.toIdeal might allow you to further golf some of the proofs / instances.~~ nevermind, that was a dumb suggestion

[jjaassoonn]

This is a pretty unusual use of SetLike, but I don't forsee it causing much trouble.

It might be good to get the connection to Ideal in this version; in particular that (I.con : Set R) = I or whatever the map from ideals to congruence relations is actually called.

I have added toIdeal and fromIdeal and proved that for any I : RingCon R, from I.toIdeal = I and for any J : Ideal R, J \le (fromIdeal J).toIdeal

[jjaassoonn]

If people like the idea of this PR but find it too big to review, I will split it up.

[jjaassoonn]

There are still a lot of missing lemmas like

lemma mem_inf {I J : RingCon R} {x} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J := by simp [mem_iff]

lemma mem_sup_left {I J : RingCon R} {x} : x ∈ I → x ∈ I ⊔ J := @le_sup_left _ _ I J x 0

lemma mem_sup_right {I J : RingCon R} {x} : x ∈ J → x ∈ I ⊔ J := @le_sup_right _ _ I J x 0

But I guess I will wait for another PR

[github-actions[bot]]

PR summary 40de468be2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.TwoSidedIdeal	799

---

Declarations diff

+ addCommGroup + add_mem + coeAddMonoidHom + coeOrderEmbedding + comap + fromIdeal + fromIdeal_toIdeal + instance : Add I where add x y := ⟨x.1 + y.1, I.add_mem x.2 y.2⟩ + instance : AddSubgroupClass (RingCon R) R + instance : Neg I where neg x := ⟨-x.1, I.neg_mem x.2⟩ + instance : SMul R I where smul r x := ⟨r • x.1, I.mul_mem_left _ _ x.2⟩ + instance : SMul Rᵐᵒᵖ I where smul r x := ⟨r • x.1, I.mul_mem_right _ _ x.2⟩ + instance : SMul ℕ I + instance : SMul ℤ I + instance : SMulCommClass R Rᵐᵒᵖ I + instance : SMulMemClass (RingCon R) R R + instance : SMulMemClass (RingCon R) Rᵐᵒᵖ R + instance : Sub I where sub x y := ⟨x.1 - y.1, I.sub_mem x.2 y.2⟩ + instance : Zero I where zero := ⟨0, I.zero_mem⟩ + le_iff + le_toIdeal_fromIdeal + leftModule + lt_iff + mem_comap + mem_iff + mem_span_iff + mem_toIdeal + mem_toIdealMop + mem_toIdealMop' + mul_mem_left + mul_mem_right + neg_mem + nsmul_mem + rel_iff + rightModule + setLike + span + sub_mem + subset_span + subtype + subtypeMop + toIdeal + toIdealMop + zero_mem + zsmul_mem

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[j-loreaux]

Is there any chance we can have an abbrev TwoSidedIdeal := RingCon? I really hate the current spelling (although I love the implementation! Thanks!)

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13610~~
• ~~leanprover-community/mathlib4#13730~~
• ~~leanprover-community/mathlib4#13902~~
• leanprover-community/mathlib4#14453 By Dependent Issues (🤖). Happy coding!

[jjaassoonn]

Superseded by https://github.com/leanprover-community/mathlib4/pull/14453