Commit 2025-01-08 20:49 1e45d5cd
View on Github →feat(Algebra/Module): definition of R-lattices (#19902)
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 ludwig@mathi.uni-heidelberg.de