4th isomorphism theorem

Stream: Is there code for X?

[Adam Topaz]

I am teaching introductory group theory this term, and we just covered the various isomorphism theorems. I wanted to mention to some of my students the statement of the 4th isomorphism theorem (lattice theorem) in lean, but I can't seem to find it. I assume it's stated in some general form using Galois connections. Can someone point me to the right file?

[Johan Commelin]

cc @Thomas Browning @Chris Hughes

[Thomas Browning]

If it's not in quotient_group.lean, then we might not have it.

[Chris Hughes]

I think we basically have it, but maybe not labelled 4th ismorphism theorem. map_comap_eq_self_of_surjective and comap_map_eq_self is basically it I think for groups.

[Patrick Massot]

We could easily package this as an ordered types isomorphism

[Adam Topaz]

Thanks! Yes, that's what I was looking for.

[Adam Topaz]

I was indeed looking around mostly at quotient_group.lean (which has the first three iso thms)