3 ms·
That's a nice idea but it tends to fall flat when you can't actually construct an explicit function exhibiting the homomorphism in question (which does happen f
by Jweb_Guru 5y ago
That's a nice idea but it tends to fall flat when you can't actually construct an explicit function exhibiting the homomorphism in question (which does happen from time to time). A lot of equivalences in areas like group theory only hold classically.
- Ericson2314 5y agoYour concerns make sense in general, but I have hard time understanding them for would-be subgroups. I would think the "explicit function" would be the easy part. The hard pat is annoyance of finding a "syntactic" representation of the subgroup and proving it's a group (closed) in its own right. In any event, Lean's reputation is that it goes the extra mile for "regular" mathematicians. It probably has something nicer for this just like it does for quotiented types.
- Jweb_Guru 5y agoNope, proving something is a group doesn't usually run into foundational concerns (at least if you use setoid equality). But finding a function exhibiting a homomorphism can unless you use a functional relation instead (but then you lose most of the nice benefits of using this version of the definition in the first place).