undefined | Better HN

0 pointsJweb_Guru4y ago0 comments

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.

0 comments

Ericson23144y ago

Your 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_GuruOP4y ago

Nope, 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).

j / k navigate · click thread line to collapse

0 pointsJweb_Guru4y ago0 comments

0 comments

Ericson23144y ago

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_GuruOP4y ago

j / k navigate · click thread line to collapse