additive

Stream: general

[Kevin Buzzard]

From group_theory.free_abelian_group.

def free_abelian_group : Type u :=
additive $ abelianization $ free_group α

The additive type alias means "treat this multiplicative group as an additive group". We also have

/-- Reinterpret `x : α` as an element of `additive α`. -/
def additive.of_mul (x : α) : additive α := x

Now in the free abelian group file, we have these:

def of (x : α) : free_abelian_group α :=
abelianization.of $ free_group.of x

This says "I will construct an element of the additive group by giving you an element of the multiplicative group and letting the unifier do the work" (abelianization.of spits out a term of type abelianization X).

Here is a proposed alternative definition:

def of (x : α) : free_abelian_group α :=
additive.of_mul $ abelianization.of $ free_group.of x

For me this is a better definition because it keeps up the pretence. But some people who understand Lean's internals far better than I do have gone with the original definition. Is my definition better in any way at all? I'd like to think that it could help e.g. the simplifier.

[Scott Morrison]

My gut feeling, in which I don't have so much confidence, is that your change is an improvement, and it's basically always better to not make defeq work hard.

[Kevin Buzzard]

I ended up having a long conversation with Chris about this during which he convinced me that the entire file should be thrown away and replaced with a finsupp version :-/ I ended up doing nothing ::-/ Sorry I've been so unproductive so far

[Scott Morrison]

No worries.

[Scott Morrison]

Chris' suggestion sounds pretty good.

[Kevin Buzzard]

I figured it might be for another PR though