Class `IsZlattice`

Stream: mathlib4

[Xavier Roblot]

Is it a good idea to define the class IsZlattice in Mathlib/Algebra/Module/Zlattice.lean, say something like:

class IsZlattice (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E]
  (L : AddSubgroup E) [DiscreteTopology L] : Prop where
  /-- `L` spans the full space `E` over `K`. -/
  span_top : span K (L : Set E) = ⊤

That would make things a bit cleaner since, at the moment , we need to pass directly the hypothesis:(hs : span K (L : Set E) = ⊤) to the different lemmas about ℤ-lattices. Unfortunately, Lean cannot infer directly from this class that a ℤ-lattice is a finite module or free module because of synthesization order...

See #11356 to see what it would look like.

[Riccardo Brasca]

What about assuming the existence of L rather than giving it?

[Xavier Roblot]

I am not sure I understand what you mean

[Eric Rodriguez]

span_top would instead read Exists L,...

[Riccardo Brasca]

Maybe I am confused and I need a coffee, but I mean something like

class IsZlattice (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] : Prop where
  /-- `L` spans the full space `E` over `K`. -/
  span_top : ∃ (L : AddSubgroup E), DiscreteTopology L ∧ Submodule.span K (L : Set E) = ⊤

(this would not solve the synthesization order of course, it is a general remark)

[Xavier Roblot]

But the class is about L. It is there to characterise L when used as an argument in lemmas. Right now, the hypothesis (hs : span K (L : Set E) = ⊤) as to be provided to these lemmas and I thought using a class instead was a more elegant way to do it.

[Riccardo Brasca]

Ah yes, the lattice is L, sorry for the noise.

[Riccardo Brasca]

Does it make sense to define it as a discrete module over a blabla ring such that the tensorization with the field of fraction is finite dimensional?

[Riccardo Brasca]

No, ok, I need a coffee

[Riccardo Brasca]

It needs the whole space of course

[Xavier Roblot]

I mean we could say that the tensorization by K (which you can think of as being ℝ) is equal to E. That would be another way to spell span_top.

[Riccardo Brasca]

instance {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ProperSpace E]
  (L : AddSubgroup E) [DiscreteTopology L] [IsZlattice ℝ L] : Module.Finite ℤ L := sorry

is OK, right? So even if we don't have the general instance we can have the relevant ones.

[Xavier Roblot]

I am not in front of a computer so I cannot make sure it works but I think you are right: this should work and it is actually what we need.

[Riccardo Brasca]

Another possibility is to define the type of lattices

[Xavier Roblot]

Defining the instances as you suggested above works great. Lean can infer now in NumberField.Units that the unitLattice is a finite and free module automatically from the fact that it is a Zlattice, see #11356

[Filippo A. E. Nuccio]

But why the preference for $\mathbb{Z}$? In @Xavier Roblot 's first version we would have that $\mathcal{O}_K$ is a $\mathbb{Z}_p$-lattice for a finite $K/\mathbb{Q}_p$, and we certainly do not want to duplicate this class in all possible cases.

[Xavier Roblot]

The results in Mathlib.Algebra.Module.Zlattice.lean are proved for ℤ-lattices and the class is there to make it easier to use these results. Now, there will probably be the need to define a more general class of lattices over other rings as suggested by @Filippo A. E. Nuccio eventually and which point we should replace the class IsZlattice by a more general class or as a special case of the more general class. But that would belong to another file (and another project), I guess.