Why `finrank` require `AddCommGroup`

Stream: general

[Jz Pan]

In Module.rank it's [Semiring R] [AddCommMonoid M], but in FiniteDimensional.finrank it's [Semiring R] [AddCommGroup M]. Are there design considerations in it?

[Anne Baanen]

I expect this is just a leftover from when findim was defined only for vector spaces. I suggest we can generalize this nothing will break.

[Andrew Yang]

I think the discussion near the end of https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20.60E.2FL.2FF.60.20and.20.60K.2FL'.2FF.60.20isomorphic.20.3D.3E.20.60.5BE.3AL.5D.3D.5BK.3AL'.5D.60 suggests that we shouldn't bother ourselves with generalising before making sure we are using the correct definition for semimodules.

[Jz Pan]

I remembered that there was a discussion that whether LinearIndependent should use the kernel of Finsupp.total being zero (i.e. the preimage of zero is zero) or Finsupp.total being injective. The latter is stronger than the former.
The former is equivalent to say any non-zero linear combination is not zero, and the latter is equivalent to say if two linear combinations are equal, then their coefficients are equal, or you can say formal subtraction is allowed (i.e. Grothendieck group). For rings, these two are equivalent.

[Jz Pan]

My opinion is that let's keep the prerequisites of Module.rank and FiniteDimensional.finrank the same.

[Antoine Chambert-Loir]

One could add the dual notion of “type”, the minimal cardinality of a generating set. That would be closer to what one wants to say.

[Jz Pan]

Antoine Chambert-Loir said:

One could add the dual notion of “type”, the minimal cardinality of a generating set. That would be closer to what one wants to say.

And then if these two definitions coincide, then I think that the module in question is very close to a free module.