## Stream: new members

### Topic: Finite-rank free modules

#### Oliver Nash (Oct 28 2019 at 20:54):

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 (Oct 28 2019 at 20:55):

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,
neg          := sorry,
add_comm     := sorry }


?

#### Oliver Nash (Oct 28 2019 at 20:58):

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 (Oct 28 2019 at 21:00):

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 (Oct 28 2019 at 21:00):

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

#### Johan Commelin (Oct 29 2019 at 04:37):

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 (Oct 29 2019 at 04:38):

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

#### Johan Commelin (Oct 29 2019 at 04:38):

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 (Oct 29 2019 at 04:39):

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

#### Kevin Buzzard (Oct 29 2019 at 07:29):

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 (Oct 29 2019 at 19:40):

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.

Last updated: May 17 2021 at 21:12 UTC