Generalized Isomorphism Theorem

Stream: Is there code for X?

[Erika Su]

Is there Isomorphism thoerem in term of universal algebra perspective?

[Adam Topaz]

What sort of statement are you looking for?

[Anne Baanen]

Somewhat related topic: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Universal.20Algebra

[Adam Topaz]

Well, I was asking because the naive generalization of the first isomorphism theorem (for groups, say) doesn't hold in general.

[Adam Topaz]

And the generalization that does hold in general seems to be essentially a tautology.

[Adam Topaz]

But anyway, I do think we should have some more universal algebra in mathlib!

[Adam Topaz]

Ha! I just noticed that the original post had a link to the target theorem! Sorry for my confusion! Yes, this is the statement that I think is more-or-less a tautology.

[Adam Topaz]

I guess the main interesting thing is to define what it means for a relation to be a congruence and to show that the relation obtained from a morphism is indeed such a congruence.

[Eric Wieser]

Ha! I just noticed that the original post had a link to the target theorem!

it was edited in