## Stream: maths

### Topic: Linear independence in torsion modules

#### Eric Wieser (Jan 02 2021 at 23:02):

Consider the int-module zmod 4 × int. Does mathlib consider the vectors a=(1, 1) and b=(0, 1) docs#linear_independent?

It shouldn't.

#### Eric Wieser (Jan 02 2021 at 23:05):

Obviously 4*a=4*b, so my impression is that it doesn't

#### Adam Topaz (Jan 02 2021 at 23:06):

They generate, so if they were independent you would have a free module

#### Eric Wieser (Jan 02 2021 at 23:07):

Are "free module" and "torsion-free module" synonyms?

#### Adam Topaz (Jan 02 2021 at 23:08):

No, but free implies torsion free

#### Adam Topaz (Jan 02 2021 at 23:09):

There's a weaker notion of independence. I don't know what it's called, but these satisfy that.

#### Eric Wieser (Jan 02 2021 at 23:09):

That weaker notion is what I'm seeking here, I think

#### Adam Topaz (Jan 02 2021 at 23:10):

I've called it quasi-independent in one of my old papers.

#### Adam Topaz (Jan 02 2021 at 23:10):

But again there might be a standard name

#### Eric Wieser (Jan 02 2021 at 23:11):

And this came up because the tfae statement made by wikipedia about docs#alternating_map appears to be untrue in this module

#### Adam Topaz (Jan 02 2021 at 23:12):

What's the statement?

#### Eric Wieser (Jan 02 2021 at 23:13):

https://en.m.wikipedia.org/wiki/Alternating_multilinear_map#Definition

#### Adam Topaz (Jan 02 2021 at 23:15):

Right. So in this case the wedge product of the module you mentioned with itself is isomorphic to zmod 4.

#### Eric Wieser (Jan 02 2021 at 23:16):

As far as I can tell, condition 2 does not imply 3 on that page

#### Adam Topaz (Jan 02 2021 at 23:16):

So two vectors a,b are quasi-independent if a \wedge b generates that module

#### Eric Wieser (Jan 02 2021 at 23:17):

I didn't understand your previous message but I understand at least the gist of that one

#### Adam Topaz (Jan 02 2021 at 23:18):

You can formulate quasi-independence in some way analogous to usual independence, but it's a bit tedious to write down (and I'm on mobile, so I'll have to do it later, if you're still interested)

#### Eric Wieser (Jan 02 2021 at 23:19):

I'm also on mobile, later is fine!

#### Kevin Buzzard (Jan 02 2021 at 23:34):

Free only implies torsion-free for integral domains, maybe? Or maybe there's a cleverer definition of torsion.

#### Kevin Buzzard (Jan 02 2021 at 23:35):

An example of a torsion-free module that isn't free is the rationals as a Z-module. It's not finitely-generated but any two elements are dependent!

#### Kevin Buzzard (Jan 02 2021 at 23:36):

Another example is the ideal generated by X and Y in k[X,Y] where k is a field.

#### Adam Topaz (Jan 02 2021 at 23:46):

Oh yeah, I was thinking explicitly of Z :)

#### Adam Topaz (Jan 02 2021 at 23:48):

I mean with the usual def of torsion free, Z/4 is not torsion free over itself. The definition of torsion free is kind of stupid imo

#### Adam Topaz (Jan 03 2021 at 00:13):

@Eric Wieser on second thought the wedge product thing is probably not good enough... E.g. (1,0) and (0,3) would satisfy that condition.

Last updated: May 12 2021 at 07:17 UTC