[Merged by Bors] - feat(Algebra.Module.Zlattice): add Zlattice.module_free and Zlattice.rank#5728
[Merged by Bors] - feat(Algebra.Module.Zlattice): add Zlattice.module_free and Zlattice.rank#5728
Conversation
|
Please remember to add the label |
Mathlib/Algebra/Module/Zlattice.lean
Outdated
| -- `0 → span ℤ s → L → L / span ℤ s → 0` with `span ℤ s` and `L / span ℤ s` finitely generated. | ||
| refine fg_of_fg_map_of_fg_inf_ker (span ℤ s).mkQ ?_ ?_ | ||
| · -- Let `b` be the `K`-basis of `E` formed by the vectors in `s`. The elements of | ||
| -- `L / span ℤ s = L /span ℤ b` are in bijection with elements of `L ∩ fundamentalDomain b` |
There was a problem hiding this comment.
| -- `L / span ℤ s = L /span ℤ b` are in bijection with elements of `L ∩ fundamentalDomain b` | |
| -- `L / span ℤ s = L / span ℤ b` are in bijection with elements of `L ∩ fundamentalDomain b` |
There was a problem hiding this comment.
| -- `L / span ℤ s = L /span ℤ b` are in bijection with elements of `L ∩ fundamentalDomain b` | |
| -- `L ⧸ span ℤ s = L ⧸ span ℤ b` are in bijection with elements of `L ∩ fundamentalDomain b` |
|
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
|
This is not really a suggestion but just a point I wanted to raise: it would be nice to frame this as part of the general theory of lattices in topological groups. I don't know much about this theory but I expect for example that I was guessing the definition should be about a compact quotient but my reading of wikipedia suggests it should be something like: import Mathlib.MeasureTheory.Group.Measure
open MeasureTheory MeasureTheory.Measure
class IsLattice {G : Type*} [Group G] [TopologicalSpace G] [MeasurableSpace G]
(Γ : Subgroup G) [DiscreteTopology Γ] : Prop :=
exists_smulInv_finite : ∃ (μ : Measure (G ⧸ Γ)), SMulInvariantMeasure G _ μ ∧ IsFiniteMeasure μ(possibly also including In addition to permitting generalisation I think such a definition (or similar) would help organise the very nice results in this PR a little. |
|
I agree that the notion of ℤ-lattice developed in this PR should generalise to the setting of topological groups. However, I am far from an expert on the subject and I wouldn't know what the right setting/definition is. Maybe what you can do is to open an issue of that topic so that more experts people can weight in eventually. |
|
bors r+ |
…rank (#5728) We prove the main characterisation of $\mathbb{Z}$-lattices: a subgroup $L$ of $\mathbb{R}^n$ that is discrete and that spans $\mathbb{R}^n$ is a free $\mathbb{Z}$-module of rank $n$ (in a slightly more general setting).
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
We prove the main characterisation of$\mathbb{Z}$ -lattices: a subgroup $L$ of $\mathbb{R}^n$ that is discrete and that spans $\mathbb{R}^n$ is a free $\mathbb{Z}$ -module of rank $n$ (in a slightly more general setting).