feat(Algebra/Module): definition of R-lattices

[chrisflav]

Given an integral domain R and its fraction field K, we define an R-lattice in a K-vector space V to be a finitely generated R-submodule of V that generates V over K. If R is a PID a lattice is always a free R-module of rank Module.rank K V.

The unit group of R naturally acts on the type of R-lattices in V. If V = Fin 2 → K and R is a discrete valuation ring, the quotient by this action are the vertices of the Bruhat-Tits tree of GL (Fin 2) K.

In this PR the predicate IsLattice on a submodule M is defined and some basic stability properties are shown.

From "Formalizing the Bruhat-Tits tree"

Co-authored by: Judith Ludwig [email protected]

---

[github-actions]

PR summary ff278854d1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Module.Lattice (new file)	1200

---

Declarations diff

+ IsLattice
+ NoZeroSMulDivisors.of_algebraMap_injective'
+ _root_.Basis.extendOfIsLattice
+ _root_.Basis.extendOfIsLattice_apply
+ _root_.Submodule.span_range_eq_top_of_injective_of_rank_le
+ finite
+ finrank_of_pi
+ free
+ inf
+ of_le_of_isLattice_of_fg
+ of_rank_le
+ rank'
+ rank_of_pi
+ smul
+ sup

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[acmepjz]

I think "the intersection of two lattices is a lattice" is also true for Dedekind domains (perhaps more general), but it needs a local-global argument. Do you have plan to formalize it?

[chrisflav]

I think "the intersection of two lattices is a lattice" is also true for Dedekind domains (perhaps more general), but it needs a local-global argument. Do you have plan to formalize it?

No, we don't have plans to generalize this.

[acmepjz]

I think "the intersection of two lattices is a lattice" is also true for Dedekind domains (perhaps more general), but it needs a local-global argument. Do you have plan to formalize it?

No, we don't have plans to generalize this.

I see. I think that is useful in algebraic number theory, e.g. to study the intersections of orders (i.e. subrings which are lattices) and ideals in a number field or a quaternion algebra over a number field, etc. etc.

[judithludwig]

I think "the intersection of two lattices is a lattice" is also true for Dedekind domains (perhaps more general), but it needs a local-global argument. Do you have plan to formalize it?

No, we don't have plans to generalize this.

I see. I think that is useful in algebraic number theory, e.g. to study the intersections of orders (i.e. subrings which are lattices) and ideals in a number field or a quaternion algebra over a number field, etc. etc.

Indeed, and we'd be happy to see lattices developed further. Our current project is on formalizing the Bruhat-Tits tree, and for that we work in the setting of a DVR, so our setting is local, not global. (Vertices in the Bruhat-Tits tree are defined as homothety classes of lattices.) This motivates this pull request.

[acmepjz]

Maybe I'll look at this when I finish currently planned PRs.