Covolume of a Z-lattice

Stream: maths

[Xavier Roblot]

I'd like to define the covolume of a Z-lattice. However, all the definitions I can find rely on the choice of a basis of the lattice or of a fundamental domain of the lattice. Of course, it is easy to prove that any basis / fundamental domain give the same covolume (see #11327 for what I have so far). But I wonder if there is a way to do it more "canonically".

[Johan Commelin]

If you take volume and push it forward to the quotient V/L that should give you a Haar measure on the quotient group, I think? Can't you take the measure of that full quotient group?

[Sébastien Gouëzel]

Is that related to #7506?

[Sébastien Gouëzel]

Pushing volume to the quotient will give you an infinite measure downstairs, which is not what you want.

[Johan Commelin]

Aah, ignore what I said

[Johan Commelin]

#7506 seems quite related yes!

[Xavier Roblot]

Yes, that does seem related indeed. I guess I should wait for this PR then...

[Sébastien Gouëzel]

The PR has already taken some time, in part because @Alex Kontorovich is maybe more involved with PNT currently. @Alex Kontorovich , I can help fixing the PR if you like, just tell me!

[Alex Kontorovich]

Thanks Sebastien; I'm hoping Heather and I can fix it when we meet on Fri. But if not, I'll circle back around and ask you for help!...

[Kevin Buzzard]

I'd like to define the dimension of a finite-dimensional real vector space. However, all the definitions I can find rely on the choice of a basis of the vector space. Of course, it is easy to prove that any basis gives the same dimension (see any linear algebra textbook). But I wonder if there is a way to do it more "canonically".

[Richard Copley]

docs#FiniteDimensional.finrank ?

[Kevin Buzzard]

Yes I know it's there already :-) I'm just saying that sometimes you really do have to break the symmetry -- there is no "canonical" way to do it. Perhaps I should add that the last time I brought this up a lot of people suggested various tricks to make it "canonical" and nothing worked.

[Alex Kontorovich]

Ooh interesting. Measure the volume change when a lattice grows by a factor of 2....

[Kevin Buzzard]

yeah but now you have to choose a basis for the lattice, as Xavier just pointed out :-) Oh I've just realised that the argument with the "quotient measure" claims to not have to do this?

[Antoine Chambert-Loir]

Kevin Buzzard said:

I'd like to define the dimension of a finite-dimensional real vector space. However, all the definitions I can find rely on the choice of a basis of the vector space. Of course, it is easy to prove that any basis gives the same dimension (see any linear algebra textbook). But I wonder if there is a way to do it more "canonically".

This year, I wanted to avoid the classical definition because of the same ambiguity.
One possibility was the supremum of the cardinalities of free subsets (which docs#FiniteDimensional.finrank is, but is bizarre in a general module because there are nonzero modules of zero rank), and I preferred to take the infimum of the cardinalities of generating subsets.
Then the theorems follow cleanly: 1) all free subsets have cardinality <= dim (V); 2) all generating subsets have cardinality >= dim(V) (this is the definition of dim); 3) there are bases and they all have cardinality dim(V).

[Kevin Buzzard]

Maybe next year you can define it to be the log of the multiplicative scaling factor on additive haar measure :-)

[Kevin Buzzard]

Oh but then you have to choose a Haar measure :-)

[Antoine Chambert-Loir]

No you don't. Endomorphisms of a 1-dimensional vector spaces are homotheties.
(It's the same for determinants : n-linear alternate forms on V constitute a 1-dim vector space, and any endomorphism u of V gives an endomorphism of that line, which is multiplication by det(u)).

[Junyan Xu]

there are bases and they all have cardinality dim(V).

I've been thinking about proving the analogue for semisimple modules: every isotypic component decomposes into a direct sum of copies of a simple module, and the number of summands (possibly infinite) is an invariant. I think this is necessary if you want to prove the uniqueness in Artin--Wedderburn. The proof is basically the same as in the vector space case (the simple modules over a field are one-dimensional), and I wonder whether we should develop some matroid API to prove it ... and that might also be used to prove the invariance of the transcendence degree.

[Kevin Buzzard]

The difficulty with using n'th wedge powers is that we're trying to find n

[Antoine Chambert-Loir]

If $M=\bigoplus_{i\in I} S_i$ is a direct sum of simple modules, then for any simple module $S$, you have $\mathop{\rm Hom}_R(S,M)=\bigoplus_{i\in I}\mathop{\rm Hom}_R(S,S_i)$, which you understand by the theory of vector spaces, because only remain the $i$ such that $S\simeq S_i$. There is, in fact, a canonical way of understanding such direct sums of isomorphic simple modules as $S\otimes_R V$ where $D$ is the field $\mathop{\rm End}(S)^\circ$ and $V$ is a $D$-vector space. The multiplicity of $S$ is the dimension of $V$.

[Junyan Xu]

That's a great idea! We have a Module.End R S action on S commuting with the R-action and therefore a (Module.End R S)ᵈᵐᵃ action on S →ₗ[R] M. I think you meant to write $S\otimes_D V$ though.

It's interesting to note that in mathlib invariance of dimension (over a division ring) is apparently from docs#IsNoetherianRing.strongRankCondition (mathlib#7711).

[Alex Kontorovich]

Sébastien Gouëzel said:

The PR has already taken some time, in part because Alex Kontorovich is maybe more involved with PNT currently. Alex Kontorovich , I can help fixing the PR if you like, just tell me!

#7506 is now ready for more comments/suggestions. Thanks!