Lattice/Correspondence/Fourth Isomorphism Theorem for Groups

Stream: mathlib4

[Johannes Choo]

Hi, I'd been trying some obvious keyword names, but I don't think I can find the https://en.wikipedia.org/wiki/Correspondence_theorem in Mathlib4 . If it's present, I'd like to add it to the glossary file; if it's not I'd like to try contributing!

[Daniel Weber]

@loogle Group, Subgroup.Normal, HasQuotient.Quotient

[loogle]

:search: QuotientGroup.Quotient.group, QuotientGroup.Quotient.group.eq_1, and 93 more

[Daniel Weber]

It doesn't seem to exist

[Johannes Choo]

Thanks! I'll be going about looking Mathlib for examples of galois connections to see how I might phrase this similarly, but if any examples or advice come to mind, please do let me know!

[Kevin Buzzard]

I'm pretty sure it's there somewhere but I'm not at a computer right now. Loogle let me down recently with another search for quotients so I might chase this up if I can reconstruct

[Daniel Weber]

There is docs#Subgroup.gc_map_comap, maybe you can use it with docs#QuotientGroup.mk'

[Junyan Xu]

For ideals, there are docs#Ideal.relIsoOfSurjective and docs#Ideal.orderEmbeddingOfSurjective, but I can't find the Subgroup version.

[Kevin Buzzard]

Yes I couldn't find it either, so I retract my claim that it's there somewhere. We have the three isomorphism theorems but apparently not this?

[Christian Merten]

We also have it for submodules docs#Submodule.comapMkQRelIso

[Matt Diamond]

Johannes Choo said:

Thanks! I'll be going about looking Mathlib for examples of galois connections to see how I might phrase this similarly, but if any examples or advice come to mind, please do let me know!

I assume this would be phrased as Subgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H }, right? Once you've defined the OrderIso, you get the GaloisConnection for free with docs#OrderIso.to_galoisConnection

[Kevin Buzzard]

An order isomorphism is a bit of a degenerate case of a Galois connection, right? I'm not sure what you gain by having the Galois connection here, the order iso gives you much stronger results.

[Johannes Choo]

Hi! I've opened a PR https://github.com/leanprover-community/mathlib4/pull/20007 for this, and it basically mirrors docs#Submodule.comapMkQRelIso. I'm running into an issue where the natural homomorphism to the quotient group is called mk', so that triggers a warning on lemmas added that end in ...mk', failing the CI. What's the preferred way to resolve this?