Finite-rank free modules

Stream: new members

[Oliver Nash]

Given a ring R and a natural number n, I'd like to use the free module R^n? Does Mathlib contain a definition for this? So far I can't find it.

[Oliver Nash]

Poking around I see that there is dfinsupp.to_module, which I could obviously use to define R^n but this seems rather heavyweight, which brings me to my second question: is there a case to be made for creating the following:

instance (n : ℕ) (R : Type u) [ring R] : add_comm_group (vector R n) :=
  { zero         := sorry,
    add          := sorry,
    add_assoc    := sorry,
    zero_add     := sorry,
    add_zero     := sorry,
    neg          := sorry,
    add_left_neg := sorry,
    add_comm     := sorry }

?

[Oliver Nash]

Oops, that's just the commutative group structure. I mean also to have the scalar action so that we actually have an instance module R (vector R n)?

[Floris van Doorn]

The most convenient definition of R^n is (I claim) fin n -> R. This has a module structure using pi.module (hidden in algebra/pi_instances.lean).

[Oliver Nash]

Aha, thank you! I will chase that down :D

[Johan Commelin]

Similar to the free algebra (polynomials) discussed a while ago, we might need to introduce a type class free_module, and maybe it should carry a basis around with it. Because in practice you might also end up with finsupp (fin n) R or some inductively defined iterated product, or vector n R (admittedly, unlikely).

[Johan Commelin]

I think we've been working a lot with constructions, and have neglected to use a characteristic "predicate".

[Johan Commelin]

I don't have a feeling for whether we want an actual predicate, or whether we should carry the data of a basis around.

[Johan Commelin]

But introducing something that unifies all different n-dimensional free module constructions seems like a good move to me.

[Kevin Buzzard]

This is I guess because one will want to prove things about free modules (eg free modules are flat, free modules are projective) for one type and then hope to deduce it for all the other types. So we're supposed to prove 'if it satisfies these free module axioms then it is projective", right? That's the dependent type theory way of doing this I guess

[Oliver Nash]

Thank you both for these comments. For now I am unblocked by the advice to use fin n → R, but I will keep in mind these remarks and cook up a PR if something crystalises.