ZLattice: which fields do we care about?

Stream: mathlib4

[Yury G. Kudryashov]

@Xavier Roblot Are there any fields other than docs#Real you care about in the context of docs#IsZLattice ?

[Kevin Buzzard]

This concept is useful in complex analysis too (a complex abelian variety is the quotient of a f.d. complex vector space by a lattice). But no nontrivial examples exist over p-adic fields.

[Yury G. Kudryashov]

In case of complex abelian varieties, the field K is still Real.

[Yury G. Kudryashov]

In the sense that span Real L = \top, not just span Complex L = \top.

[Yury G. Kudryashov]

I think about refactoring this part of the library by switching to bundled structures, restricting to K = Real, and generalizing in 1 of 2 (or both) directions:

@[to_additive] -- Option 1: lattice in a topological group
structure MulLattice (G : Type*) [TopologicalSpace G] [Group G] extends Subgroup G where
  discrete : DiscreteSpace toSubgroup
  compact : CompactSpace (G ⧸ toSubgroup)

-- Option 2: don't depend on topology
structure ZLattice (E : Type*) [AddCommGroup E] [Module ℝ E] extends AddSubgroup E where
  exists_basis : ∃ s : Set E, LinearIndependent ℝ (Subtype.val : s → E) ∧ Submodule.span ℝ s = ⊤ ∧ toAddSubgroup = .closure s

[Yury G. Kudryashov]

Does it make sense?

[Kevin Buzzard]

I'd be the first to complain if there were some p-adic variant which isn't covered but I don't know of any examples not covered by this refactor. @Xavier Roblot do you have any comments on this change?

[Johan Commelin]

@Yury G. Kudryashov Can you please remind me why you want to fix the real ambient space?

Here is a different approach, and it's not clear what the pros and cons of either of the two are: https://github.com/erikvdplas/mathlib4/blob/7f418e1373b95b96afcd5ba6404906a138a89c1c/Mathlib/GroupTheory/IntegralLattice/Basic.lean

[Antoine Chambert-Loir]

These are euclidean lattice, which is a slightly different kind of beast but can be viewed as a lattice in a euclidean Space. Those also exist over number fields, and in the hermitian context.

There are also lattices in general (locally compact) topological groups (discrete, finite covolume) and for real vector spaces, they coincide with docs#IsZLattice

[Johan Commelin]

@Antoine Chambert-Loir Thanks. So we should distinguish these concepts using different names. Do you have some suggestions for how to call them in Lean?

[Antoine Chambert-Loir]

Submodule.IsLattice could say that the submodule is free over the subring and generates top over the larger ring. Should it be refined to Submodule.IsIntLatticeor Submodule.IsZLattice?

Subgroup.IsLattice would require the ambient group to be a locally compact topological group and say that the subgroup is discrete and has finite covolume.

[Xavier Roblot]

Yury G. Kudryashov said:

Xavier Roblot Are there any fields other than docs#Real you care about in the context of docs#IsZLattice ?

Yes, the lattices that I am interested in are over the real numbers. I stated some results in a more general setting because It was possible but I am not sure they have any use other than the real case.

[Xavier Roblot]

Yury G. Kudryashov said:

I think about refactoring this part of the library by switching to bundled structures, restricting to K = Real, and generalizing in 1 of 2 (or both) directions:

@[to_additive] -- Option 1: lattice in a topological group
structure MulLattice (G : Type*) [TopologicalSpace G] [Group G] extends Subgroup G where
  discrete : DiscreteSpace toSubgroup
  compact : CompactSpace (G ⧸ toSubgroup)

-- Option 2: don't depend on topology
structure ZLattice (E : Type*) [AddCommGroup E] [Module ℝ E] extends AddSubgroup E where
  exists_basis : ∃ s : Set E, LinearIndependent ℝ (Subtype.val : s → E) ∧ Submodule.span ℝ s = ⊤ ∧ toAddSubgroup = .closure s

I like option 2 slighter better since, for me, the important property of lattices is that they admit a ℤ-basis that is also a ℝ-basis of the full space. Also, note that I changed recently ZLattice from AddSubgroup to Submodule ℤ E as I was mostly computing with bases and it was easier that way. I guess it depends also on the application you have in mind.

[Johan Commelin]

@Antoine Chambert-Loir That makes sense. But then there is also the "absolute" notion, that doesn't talk about subthings of an ambient thing, but just requires a finitely generated free gadget with some sort of bilinear form.

And as I understand it, you say that should be yet another different concept, possibly also called some variant of "lattice"?

[Xavier Roblot]

In any case, the notion of ZLattice I developed in these files was specific to the applications I had in mind in the geometry of numbers and there are certainly ways to generalize these to a larger setting as mentioned by Antoine.

[Xavier Roblot]

Note also that have several PRs about ZLattice that are coming (for the proof of the Class Number Formula), see #16822 and #12488 for example, so it would be nice if any refactor does changes things too much :sweat_smile:

[Antoine Chambert-Loir]

@Johan Commelin AFAI, you can view euclidean lattices

• as $(L,q)$ where $L$ is a free $\mathbf Z$-module of finite rank and $q$ is a positive definite $\mathbf R$-valued bilinear form on $L$, but one needs to be cautious about what that means: it's definitely not sufficient that it be strictly positive on $L\setminus\{0\}$ (for example $(x-y\sqrt 2)^2$ on $\mathbf Z^2$ would not qualify);
• or as $(L,V,q)$ where $V$ is a finite dimensional real space, $q$ a positive definite bilinear form on $V$, and $L$ is a free $\mathbf Z$-submodule of $V$ of full rank.
  Since in the first definition, the definite positive condition on $q$ applies to its scalar extension to $L_{\mathbf R}$, I am tempted to believe that the second definition is more natural.

Hermitean variants replace $\mathbf Z$ by rings of integers in quadratic fields.

[Johan Commelin]

But there are also not-necessarily-euclidean-or-hermitian lattices, right? And then you just have $(L, q)$ without much conditions on $q$.

[Antoine Chambert-Loir]

Of course, you're right. (Signature $(p,q)$ lattices are even parameterized by $O_{p,q}(\mathbf R)/O_{p,q}(\mathbf Z)$, and Shimura varieties for $U(n,1)$ exist as well…)

[Johan Commelin]

So would you formalize those with an ambient vector space, or as absolute gadgets?

[Johan Commelin]

Or both?

[Antoine Chambert-Loir]

Good question. One way I would try to address it is by thinking about what groups act naturally on these newly created types.

[Yury G. Kudryashov]

Xavier Roblot said:

Yury G. Kudryashov said:

I think about refactoring this part of the library by switching to bundled structures, restricting to K = Real, and generalizing in 1 of 2 (or both) directions:

@[to_additive] -- Option 1: lattice in a topological group
structure MulLattice (G : Type*) [TopologicalSpace G] [Group G] extends Subgroup G where
  discrete : DiscreteSpace toSubgroup
  compact : CompactSpace (G ⧸ toSubgroup)

-- Option 2: don't depend on topology
structure ZLattice (E : Type*) [AddCommGroup E] [Module ℝ E] extends AddSubgroup E where
  exists_basis : ∃ s : Set E, LinearIndependent ℝ (Subtype.val : s → E) ∧ Submodule.span ℝ s = ⊤ ∧ toAddSubgroup = .closure s

I like option 2 slighter better since, for me, the important property of lattices is that they admit a ℤ-basis that is also a ℝ-basis of the full space. Also, note that I changed recently ZLattice from AddSubgroup to Submodule ℤ E as I was mostly computing with bases and it was easier that way. I guess it depends also on the application you have in mind.

For real vector spaces they are equivalent, so one can be a definition and another can be a constructor+theorem. The former version (not sure what's the right condition on the quotient space; can we way "finite covolume" without depending on Measure?) has other applications, e.g., to deal with nilmanifolds.

[Antoine Chambert-Loir]

I'm not sure how one can frame the “finite covolume condition” without mentioning Haar measures. (on the other hand, the condition could be: for all haar measures…)

[Yury G. Kudryashov]

What's the better condition: finite covolume or compact quotient?

[Antoine Chambert-Loir]

Discrete subgroups with compact quotient have finite covolume. On the other hand $SL(2,\mathbf Z)$ has finite covolume but is not compact.

[Yury G. Kudryashov]

Should we have names for both?

[Yury G. Kudryashov]

Or finite covolume is the most important case?

[Sébastien Gouëzel]

Both are very important, so both deserve names. Normally, they're called lattices and cocompact lattices.

[Antoine Chambert-Loir]

The question is whether cocompact is an adjective that applies to lattice, or whether the word is “cocompact_lattice”.

[Sébastien Gouëzel]

If you want typeclass inference to be able to infer the fact that the quotient is compact, it should probably be a single word cocompactLattice.

[Antoine Chambert-Loir]

Then the whole discussion will be easier to implement, than what the initial discussion suggested. Indeed, one can start by defining cocompactLatticeas discrete subgroup with compact quotient (or with the existence of a compact fundamental “domain”, that will avoid to introduce the quotient). When general lattices will be introduced (almost the same definition, with a fundamental “domain” of finite measure), it will suffice to observe that cocompactLattices are lattices, because compact sets have finite measure.

[Riccardo Brasca]

There is now #19902 about submodule lattice. Does anyone have a suggestion for the name?

[Judith Ludwig]

As @Riccardo Brasca mentioned above, with @Christian Merten we have opened the pull request #19902 on a general notion of $R$-lattices.
We are motivated by the kind of lattices that you need to construct the Bruhat-Tits tree. So for $R$ an integral domain say, with fraction field $K$, one would define these lattices as finitely generated $R$-submodules of $K$-vector spaces $V$ that generate $V$ over $K$. When $R$ is a PID, we show in the above mentioned PR that any lattice is free.
In practice (for us this means for the Bruhat-Tits tree), $R$ is a DVR, and $K$ is its fraction field.

As there is already a notion of $\mathbb{Z}$-lattices in mathlib, and there is this discussion here on the notion of lattices, I want to ask for suggestions on how we should proceed. What name should we give the Bruhat--Tits / submodule lattices? Also I'm happy to hear suggestions on what the definition of a "lattice" in mathlib should ultimately be.

[Kevin Buzzard]

There are so many meanings of the word "lattice" in mathematics that my instinct is that you should just pick something (e.g. Submodule.IsLattice, which you picked) and just get on with it. You could explain in the docstring of your IsLattice that if people are looking for ways of making complex tori or whatever then they might want to take a look at docs#IsZLattice, and you might even want to add a comment to the docstring of IsZLattice that if people are looking for things in $\mathbb{Q}$-vector spaces then they could try Submodule.IsLattice.

[Riccardo Brasca]

If there is a (at least partial) consensus I am happy to merge the PR (there are a few comments to take into account), but I agree we want a docstring.