Learning by starting at the end: Writing a Proof in Lean

5 points by iamwil


hwayne

Z-set: Sets are a bag of unique elements. Z-sets are bags that can contain multiple instances of the same element.

I was waiting for the punchline that these don't from an abelian group because multisets over merge don't have an inverse. I recognize it works because Z-sets can have "negative instances", but this analogy originally gave me the wrong intuition.

Corbin

There is a more direct intuition: since integers are Abelian, any mapping into the integers can also be made Abelian by pointwise lifting. In the special case of sets, the set of mappings from a chosen set to the integers S → Z is actually the free Abelian group on S; quoting Wikipedia, "Free abelian groups have properties which make them similar to vector spaces, and may equivalently be called free Z-modules, the free modules over the integers." This is what the LLM was trying to regurgitate for you.

For a better intuition, understand the slogan: the integers are the initial Abelian group.