Learning by starting at the end: Writing a Proof in Lean
5 points by iamwil
5 points by iamwil
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.
I think the thing they’re working with is just the set of functions from the set of objects to the natural numbers (or integers) in a trench coat, in which case the claimed property is trivial. (Moduli it not being true, as you note, unless we allow bags that contain negative quantities.)
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.