From 2235a09e1e7ecb7b34190edaa53368a0c43d907a Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 10 Dec 2024 05:24:06 +0100
Subject: [PATCH 1/4] add lattice def

---
 Mathlib.lean                        |   1 +
 Mathlib/Algebra/Module/Lattice.lean | 218 ++++++++++++++++++++++++++++
 2 files changed, 219 insertions(+)
 create mode 100644 Mathlib/Algebra/Module/Lattice.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index e1579076cc334..bfe416cd6fe96 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -530,6 +530,7 @@ import Mathlib.Algebra.Module.FreeLocus
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
+import Mathlib.Algebra.Module.Lattice
 import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Algebra.Module.LinearMap.End
diff --git a/Mathlib/Algebra/Module/Lattice.lean b/Mathlib/Algebra/Module/Lattice.lean
new file mode 100644
index 0000000000000..4c4453934fd38
--- /dev/null
+++ b/Mathlib/Algebra/Module/Lattice.lean
@@ -0,0 +1,218 @@
+/-
+Copyright (c) 2024 Judith Ludwig, Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Judith Ludwig, Christian Merten
+-/
+import Mathlib.LinearAlgebra.Dimension.Localization
+import Mathlib.LinearAlgebra.FiniteDimensional
+import Mathlib.LinearAlgebra.FreeModule.PID
+import Mathlib.Algebra.NoZeroSMulDivisors.Pi
+
+/-!
+# Lattices
+
+Let `A` be an `R`-algebra and `V` an `A`-module. Then an `R`-submodule `M` of `V` is a lattice,
+if `M` is finitely generated and spans `V` as an `A`-module.
+
+The typical use case is `A = K` is the fraction field of `R` and `V = ι → K` for some finite `ι`.
+In this case there is a natural action of `GL ι K` on the type of lattices, whose stabilizer
+at the standard lattice is `GL ι R`.
+
+By taking the quotient of the type of `R`-lattices in `ι → K` by the homothety relation,
+one obtains the vertices of what is called the Bruhat-Tits tree of `GL 2 K` when `ι = Fin 2`.
+
+## Main definitions
+
+- `Submodule.IsLattice`: An `R`-submodule `M` of `V` is a lattice, if it is finitely generated
+  and its `A`-span is `V`.
+
+-/
+
+/-- If `M` is `A`-torsion free and `algebraMap R A` is injective, `M` is also `R`-torsion free. -/
+lemma NoZeroSMulDivisors.of_algebraMap_injective' {R A M : Type*} [CommSemiring R] [Semiring A]
+    [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
+    [NoZeroSMulDivisors A M]
+    (h : Function.Injective (algebraMap R A)) :
+    NoZeroSMulDivisors R M where
+  eq_zero_or_eq_zero_of_smul_eq_zero hx := by
+    rw [← algebraMap_smul (A := A)] at hx
+    obtain (hc|hx) := eq_zero_or_eq_zero_of_smul_eq_zero hx
+    · exact Or.inl <| (map_eq_zero_iff _ h).mp hc
+    · exact Or.inr hx
+
+variable {R : Type*} [CommRing R]
+--variable {V : Type*} [AddCommMonoid V] [Module R V] [Module A V] [IsScalarTower R A V]
+
+open Pointwise
+
+namespace Submodule
+
+/--
+An `R`-submodule `M` of `V` is a lattice if it is finitely generated
+and spans `V` as an `A`-module.
+
+Note: `A` is marked as an `outParam` here. In practice this should not cause issues, since
+`R` and `A` are fixed, where typically `A` is the fraction field of `R`. -/
+class IsLattice (A : outParam Type*) [CommRing A] [Algebra R A]
+    {V : Type*} [AddCommMonoid V] [Module R V] [Module A V] [IsScalarTower R A V]
+    [Algebra R A] [IsScalarTower R A V] (M : Submodule R V) : Prop where
+  fg : M.FG
+  span_eq_top : Submodule.span A (M : Set V) = ⊤
+
+namespace IsLattice
+
+section
+
+variable (A : Type*) [CommRing A] [Algebra R A]
+variable {V : Type*} [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V]
+variable (M : Submodule R V)
+
+/-- Any `R`-lattice is finite. -/
+instance finite [IsLattice A M] : Module.Finite R M := by
+  rw [Module.Finite.iff_fg]
+  exact IsLattice.fg
+
+/-- The action of `Aˣ` on `R`-submodules of `V` preserves `IsLattice`. -/
+instance smul [IsLattice A M] (a : Aˣ) : IsLattice A (a • M : Submodule R V) where
+  fg := by
+    obtain ⟨s, rfl⟩ := IsLattice.fg (M := M)
+    rw [Submodule.smul_span]
+    have : Finite (a • (s : Set V) : Set V) := Finite.Set.finite_image _ _
+    exact Submodule.fg_span (Set.toFinite (a • (s : Set V)))
+  span_eq_top := by
+    rw [Submodule.coe_pointwise_smul, ← Submodule.smul_span, IsLattice.span_eq_top]
+    ext x
+    refine ⟨fun _ ↦ trivial, fun _ ↦ ?_⟩
+    rw [show x = a • a⁻¹ • x by simp]
+    exact Submodule.smul_mem_pointwise_smul _ _ _ (by trivial)
+
+lemma span_basis_eq_top {κ : Type*} [Fintype κ]
+    {M : Submodule R V} (b : Basis κ R M)
+    [IsLattice A M] : Submodule.span A (Set.range fun i ↦ (b i).val) = ⊤ := by
+  rw [eq_top_iff]
+  rintro x -
+  have hx : x ∈ Submodule.span A (M : Set V) := by
+    rw [IsLattice.span_eq_top]
+    trivial
+  induction' hx using Submodule.span_induction with x hx x y _ _ hx hy a x _ hx
+  · have hv : ⟨x, hx⟩ ∈ Submodule.span R (Set.range b) := Basis.mem_span b ⟨x, hx⟩
+    obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun _).mp hv
+    simp only [Subtype.ext_iff, AddSubmonoidClass.coe_finset_sum, SetLike.val_smul] at hc
+    rw [← hc]
+    refine Submodule.sum_mem _ (fun i _ ↦ ?_)
+    rw [← algebraMap_smul (A := A)]
+    exact Submodule.smul_mem _ _ <| Submodule.subset_span (Set.mem_range_self i)
+  · simp
+  · exact Submodule.add_mem _ hx hy
+  · exact Submodule.smul_mem _ _ hx
+
+
+end
+
+section
+
+/-!
+## Lattices are free
+
+In this section we prove that every lattice is a free `R`-module of rank `2` and
+every such `R`-module is a lattice.
+-/
+
+variable (K : Type*) [Field K] [Algebra R K]
+variable [IsDomain R] [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K]
+variable {V : Type*} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V]
+
+/-- Any lattice over a PID is a free `R`-module. -/
+instance free (M : Submodule R V) [IsLattice K M] : Module.Free R M := by
+  haveI : NoZeroSMulDivisors R V := by
+    apply NoZeroSMulDivisors.of_algebraMap_injective' (A := K)
+    exact NoZeroSMulDivisors.algebraMap_injective R K
+  /- torsion free, finite module over a PID -/
+  infer_instance
+
+/-- Any lattice has `R`-rank equal to the `K`-rank of `V`. -/
+theorem rank' [IsFractionRing R K] (M : Submodule R V) [IsLattice K M] :
+    Module.rank R M = Module.rank K V := by
+  let b := Module.Free.chooseBasis R M
+  have hli : LinearIndependent K (fun i ↦ (b i).val) := by
+    rw [← LinearIndependent.iff_fractionRing (R := R), linearIndependent_iff']
+    intro s g hs
+    simp_rw [← Submodule.coe_smul_of_tower, ← Submodule.coe_sum, Submodule.coe_eq_zero] at hs
+    exact linearIndependent_iff'.mp b.linearIndependent s g hs
+  have hsp : ⊤ ≤ Submodule.span K (Set.range <| fun i ↦ (b i).val) := by
+    rw [span_basis_eq_top]
+  let b' := Basis.mk hli hsp
+  rw [rank_eq_card_basis b, ← rank_eq_card_basis b']
+
+/-- Any `R`-lattice has rank `k` as an `R`-module. -/
+lemma rank [IsFractionRing R K] {k : ℕ} (M : Submodule R (Fin k → K)) [IsLattice K M] :
+    Module.rank R M = k := by
+  rw [IsLattice.rank' K M]
+  simp
+
+/-- `Module.finrank` version of `IsLattice.rank`. -/
+lemma finrank [IsFractionRing R K] {k : ℕ} (M : Submodule R (Fin k → K)) [IsLattice K M] :
+    Module.finrank R M = k :=
+  Module.finrank_eq_of_rank_eq (IsLattice.rank K M)
+
+/-- The supremum of two lattices is a lattice. -/
+instance sup (M N : Submodule R V) [IsLattice K M] [IsLattice K N] :
+    IsLattice K (M ⊔ N) where
+  fg := Submodule.FG.sup IsLattice.fg IsLattice.fg
+  span_eq_top := by
+    rw [_root_.eq_top_iff]
+    trans
+    · show ⊤ ≤ Submodule.span K M
+      rw [IsLattice.span_eq_top (M := M)]
+    · apply Submodule.span_mono
+      simp
+
+omit [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K] in
+lemma span_eq_top_of_rank [Module.Finite K V] [IsFractionRing R K]
+    {M : Submodule R V} (h : Module.rank R M = Module.rank K V) :
+    Submodule.span K (M : Set V) = ⊤ := by
+  obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M
+  replace hli := hli.map' M.subtype (Submodule.ker_subtype M)
+  rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli
+  rw [h, ← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
+  obtain ⟨hfin, hcard⟩ := hs
+  have hsubset : Set.range (fun x : s ↦ x.val.val) ⊆ M := by
+    rintro x ⟨a, rfl⟩
+    simp
+  have hcard : Fintype.card ↑s = Module.finrank K V := by simpa
+  rw [_root_.eq_top_iff]
+  rw [← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]
+  exact Submodule.span_mono hsubset
+
+omit [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K] in
+/-- A finitely-generated `R`-submodule of `V` that has rank the `K`-rank of `V` is
+a lattice. -/
+lemma of_rank [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
+    (hfg : M.FG) (hr : Module.rank R M = Module.rank K V) : IsLattice K M where
+  fg := hfg
+  span_eq_top := span_eq_top_of_rank K hr
+
+/-- The intersection of two lattices is a lattice. -/
+theorem inf [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V)
+    [IsLattice K M] [IsLattice K N] :
+    IsLattice K (M ⊓ N) where
+  fg := by
+    have aux : M.FG := IsLattice.fg
+    have : IsNoetherian R M := isNoetherian_of_fg_of_noetherian M aux
+    have g : (M ⊓ N) ≤ M := inf_le_left
+    have : IsNoetherian R ↥(M ⊓ N) := isNoetherian_of_le g
+    have h : Module.Finite R ↥(M ⊓ N):= Module.IsNoetherian.finite R ↥(M ⊓ N)
+    apply Module.Finite.iff_fg.mp
+    exact h
+  span_eq_top := by
+    apply span_eq_top_of_rank
+    have h := Submodule.rank_sup_add_rank_inf_eq M N
+    rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h
+    apply Cardinal.eq_of_add_eq_add_left h
+    exact Module.rank_lt_aleph0 K V
+
+end
+
+end IsLattice
+
+end Submodule

From ed5151e222cf56f2f70eda81c8a028f4afa7f690 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 10 Dec 2024 13:24:00 +0100
Subject: [PATCH 2/4] cleanup

---
 Mathlib/Algebra/Algebra/Basic.lean  |  23 ++--
 Mathlib/Algebra/Module/Lattice.lean | 203 +++++++++++++---------------
 2 files changed, 104 insertions(+), 122 deletions(-)

diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
index 98aab66f635a1..773b0b6060ecd 100644
--- a/Mathlib/Algebra/Algebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Basic.lean
@@ -334,18 +334,21 @@ theorem algebra_compatible_smul (r : R) (m : M) : r • m = (algebraMap R A) r 
 theorem algebraMap_smul (r : R) (m : M) : (algebraMap R A) r • m = r • m :=
   (algebra_compatible_smul A r m).symm
 
+/-- If `M` is `A`-torsion free and `algebraMap R A` is injective, `M` is also `R`-torsion free. -/
+lemma NoZeroSMulDivisors.of_algebraMap_injective' {R A M : Type*} [CommSemiring R] [Semiring A]
+    [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
+    [NoZeroSMulDivisors A M] (h : Function.Injective (algebraMap R A)) :
+    NoZeroSMulDivisors R M where
+  eq_zero_or_eq_zero_of_smul_eq_zero hx := by
+    rw [← algebraMap_smul (A := A)] at hx
+    obtain (hc|hx) := eq_zero_or_eq_zero_of_smul_eq_zero hx
+    · exact Or.inl <| (map_eq_zero_iff _ h).mp hc
+    · exact Or.inr hx
+
 theorem NoZeroSMulDivisors.trans (R A M : Type*) [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
     [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors R A]
-    [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M := by
-  refine ⟨fun {r m} h => ?_⟩
-  rw [algebra_compatible_smul A r m] at h
-  rcases smul_eq_zero.1 h with H | H
-  · have : Function.Injective (algebraMap R A) :=
-      NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance
-    left
-    exact (injective_iff_map_eq_zero _).1 this _ H
-  · right
-    exact H
+    [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M :=
+  of_algebraMap_injective' (A := A) (NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance)
 
 variable {A}
 
diff --git a/Mathlib/Algebra/Module/Lattice.lean b/Mathlib/Algebra/Module/Lattice.lean
index 4c4453934fd38..820481c7dc758 100644
--- a/Mathlib/Algebra/Module/Lattice.lean
+++ b/Mathlib/Algebra/Module/Lattice.lean
@@ -6,7 +6,6 @@ Authors: Judith Ludwig, Christian Merten
 import Mathlib.LinearAlgebra.Dimension.Localization
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.LinearAlgebra.FreeModule.PID
-import Mathlib.Algebra.NoZeroSMulDivisors.Pi
 
 /-!
 # Lattices
@@ -26,22 +25,20 @@ one obtains the vertices of what is called the Bruhat-Tits tree of `GL 2 K` when
 - `Submodule.IsLattice`: An `R`-submodule `M` of `V` is a lattice, if it is finitely generated
   and its `A`-span is `V`.
 
+## Main properties
+
+Let `R` be a PID and `A = K` its field of fractions.
+
+- `Submodule.IsLattice.free`: Every lattice in `V` is `R`-free.
+- `Basis.extendOfIsLattice`: Any `R`-basis of a lattice `M` in `V` defines a `K`-basis of `V`.
+- `Submodule.IsLattice.rank`: The `R`-rank of a lattice in `V` equals to the `K`-rank of `V`.
+- `Submodule.IsLattice.inf`: The intersection of two lattices is a lattice.
+
 -/
 
-/-- If `M` is `A`-torsion free and `algebraMap R A` is injective, `M` is also `R`-torsion free. -/
-lemma NoZeroSMulDivisors.of_algebraMap_injective' {R A M : Type*} [CommSemiring R] [Semiring A]
-    [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
-    [NoZeroSMulDivisors A M]
-    (h : Function.Injective (algebraMap R A)) :
-    NoZeroSMulDivisors R M where
-  eq_zero_or_eq_zero_of_smul_eq_zero hx := by
-    rw [← algebraMap_smul (A := A)] at hx
-    obtain (hc|hx) := eq_zero_or_eq_zero_of_smul_eq_zero hx
-    · exact Or.inl <| (map_eq_zero_iff _ h).mp hc
-    · exact Or.inr hx
+universe u
 
 variable {R : Type*} [CommRing R]
---variable {V : Type*} [AddCommMonoid V] [Module R V] [Module A V] [IsScalarTower R A V]
 
 open Pointwise
 
@@ -86,44 +83,76 @@ instance smul [IsLattice A M] (a : Aˣ) : IsLattice A (a • M : Submodule R V)
     rw [show x = a • a⁻¹ • x by simp]
     exact Submodule.smul_mem_pointwise_smul _ _ _ (by trivial)
 
-lemma span_basis_eq_top {κ : Type*} [Fintype κ]
-    {M : Submodule R V} (b : Basis κ R M)
-    [IsLattice A M] : Submodule.span A (Set.range fun i ↦ (b i).val) = ⊤ := by
-  rw [eq_top_iff]
-  rintro x -
-  have hx : x ∈ Submodule.span A (M : Set V) := by
-    rw [IsLattice.span_eq_top]
-    trivial
-  induction' hx using Submodule.span_induction with x hx x y _ _ hx hy a x _ hx
-  · have hv : ⟨x, hx⟩ ∈ Submodule.span R (Set.range b) := Basis.mem_span b ⟨x, hx⟩
-    obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun _).mp hv
-    simp only [Subtype.ext_iff, AddSubmonoidClass.coe_finset_sum, SetLike.val_smul] at hc
-    rw [← hc]
-    refine Submodule.sum_mem _ (fun i _ ↦ ?_)
-    rw [← algebraMap_smul (A := A)]
-    exact Submodule.smul_mem _ _ <| Submodule.subset_span (Set.mem_range_self i)
-  · simp
-  · exact Submodule.add_mem _ hx hy
-  · exact Submodule.smul_mem _ _ hx
+end
 
+section Field
 
-end
+variable {K : Type*} [Field K] [Algebra R K]
 
-section
+lemma _root_.Submodule.span_range_eq_top_of_injective_of_rank {M N : Type u} [IsDomain R]
+    [IsFractionRing R K] [AddCommGroup M] [Module R M]
+    [AddCommGroup N] [Module R N] [Module K N] [IsScalarTower R K N] [Module.Finite K N]
+    {f : M →ₗ[R] N} (hf : Function.Injective f)
+    (h : Module.rank R M = Module.rank K N) :
+    Submodule.span K (LinearMap.range f : Set N) = ⊤ := by
+  obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M
+  replace hli := hli.map' f (LinearMap.ker_eq_bot.mpr hf)
+  rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli
+  rw [h, ← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
+  obtain ⟨hfin, hcard⟩ := hs
+  have hsubset : Set.range (fun x : s ↦ f x.val) ⊆ (LinearMap.range f : Set N) := by
+    rintro x ⟨a, rfl⟩
+    simp
+  have hcard : Fintype.card ↑s = Module.finrank K N := by simpa
+  rw [eq_top_iff, ← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]
+  exact Submodule.span_mono hsubset
 
-/-!
-## Lattices are free
+variable (K) {V : Type*} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V]
 
-In this section we prove that every lattice is a free `R`-module of rank `2` and
-every such `R`-module is a lattice.
--/
+/-- Any basis of an `R`-lattice in `V` defines a `K`-basis of `V`. -/
+noncomputable def _root_.Basis.extendOfIsLattice [IsFractionRing R K] {κ : Type*}
+    {M : Submodule R V} [IsLattice K M] (b : Basis κ R M) :
+    Basis κ K V :=
+  have hli : LinearIndependent K (fun i ↦ (b i).val) := by
+    rw [← LinearIndependent.iff_fractionRing (R := R), linearIndependent_iff']
+    intro s g hs
+    simp_rw [← Submodule.coe_smul_of_tower, ← Submodule.coe_sum, Submodule.coe_eq_zero] at hs
+    exact linearIndependent_iff'.mp b.linearIndependent s g hs
+  have hsp : ⊤ ≤ span K (Set.range fun i ↦ (M.subtype ∘ b) i) := by
+    rw [← Submodule.span_span_of_tower R, Set.range_comp, ← Submodule.map_span]
+    simp [b.span_eq, Submodule.map_top, span_eq_top]
+  Basis.mk hli hsp
 
-variable (K : Type*) [Field K] [Algebra R K]
-variable [IsDomain R] [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K]
-variable {V : Type*} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V]
+@[simp]
+lemma _root_.Basis.extendOfIsLattice_apply [IsFractionRing R K] {κ : Type*}
+    {M : Submodule R V} [IsLattice K M] (b : Basis κ R M) (k : κ) :
+    b.extendOfIsLattice K k = (b k).val := by
+  simp [Basis.extendOfIsLattice]
 
-/-- Any lattice over a PID is a free `R`-module. -/
-instance free (M : Submodule R V) [IsLattice K M] : Module.Free R M := by
+variable [IsDomain R]
+
+/-- A finitely-generated `R`-submodule of `V` that has rank the `K`-rank of `V` is
+a lattice. -/
+lemma of_rank [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
+    (hfg : M.FG) (hr : Module.rank R M = Module.rank K V) : IsLattice K M where
+  fg := hfg
+  span_eq_top := by
+    simpa using Submodule.span_range_eq_top_of_injective_of_rank M.injective_subtype hr
+
+/-- The supremum of two lattices is a lattice. -/
+instance sup (M N : Submodule R V) [IsLattice K M] [IsLattice K N] :
+    IsLattice K (M ⊔ N) where
+  fg := Submodule.FG.sup IsLattice.fg IsLattice.fg
+  span_eq_top := by
+    rw [eq_top_iff]
+    exact le_trans (b := span K M) (by rw [IsLattice.span_eq_top]) (Submodule.span_mono (by simp))
+
+variable [IsPrincipalIdealRing R]
+
+/-- Any lattice over a PID is a free `R`-module.
+Note that under our conditions, `NoZeroSMulDivisors R K` simply says that `algebraMap R K` is
+injective. -/
+instance free [NoZeroSMulDivisors R K] (M : Submodule R V) [IsLattice K M] : Module.Free R M := by
   haveI : NoZeroSMulDivisors R V := by
     apply NoZeroSMulDivisors.of_algebraMap_injective' (A := K)
     exact NoZeroSMulDivisors.algebraMap_injective R K
@@ -131,87 +160,37 @@ instance free (M : Submodule R V) [IsLattice K M] : Module.Free R M := by
   infer_instance
 
 /-- Any lattice has `R`-rank equal to the `K`-rank of `V`. -/
-theorem rank' [IsFractionRing R K] (M : Submodule R V) [IsLattice K M] :
+lemma rank' [IsFractionRing R K] (M : Submodule R V) [IsLattice K M] :
     Module.rank R M = Module.rank K V := by
   let b := Module.Free.chooseBasis R M
-  have hli : LinearIndependent K (fun i ↦ (b i).val) := by
-    rw [← LinearIndependent.iff_fractionRing (R := R), linearIndependent_iff']
-    intro s g hs
-    simp_rw [← Submodule.coe_smul_of_tower, ← Submodule.coe_sum, Submodule.coe_eq_zero] at hs
-    exact linearIndependent_iff'.mp b.linearIndependent s g hs
-  have hsp : ⊤ ≤ Submodule.span K (Set.range <| fun i ↦ (b i).val) := by
-    rw [span_basis_eq_top]
-  let b' := Basis.mk hli hsp
-  rw [rank_eq_card_basis b, ← rank_eq_card_basis b']
-
-/-- Any `R`-lattice has rank `k` as an `R`-module. -/
-lemma rank [IsFractionRing R K] {k : ℕ} (M : Submodule R (Fin k → K)) [IsLattice K M] :
-    Module.rank R M = k := by
+  rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]
+
+/-- Any `R`-lattice in `ι → K` has `#ι` as `R`-rank. -/
+lemma rank_of_pi {ι : Type*} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K))
+    [IsLattice K M] : Module.rank R M = Fintype.card ι := by
   rw [IsLattice.rank' K M]
   simp
 
 /-- `Module.finrank` version of `IsLattice.rank`. -/
-lemma finrank [IsFractionRing R K] {k : ℕ} (M : Submodule R (Fin k → K)) [IsLattice K M] :
-    Module.finrank R M = k :=
-  Module.finrank_eq_of_rank_eq (IsLattice.rank K M)
-
-/-- The supremum of two lattices is a lattice. -/
-instance sup (M N : Submodule R V) [IsLattice K M] [IsLattice K N] :
-    IsLattice K (M ⊔ N) where
-  fg := Submodule.FG.sup IsLattice.fg IsLattice.fg
-  span_eq_top := by
-    rw [_root_.eq_top_iff]
-    trans
-    · show ⊤ ≤ Submodule.span K M
-      rw [IsLattice.span_eq_top (M := M)]
-    · apply Submodule.span_mono
-      simp
-
-omit [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K] in
-lemma span_eq_top_of_rank [Module.Finite K V] [IsFractionRing R K]
-    {M : Submodule R V} (h : Module.rank R M = Module.rank K V) :
-    Submodule.span K (M : Set V) = ⊤ := by
-  obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M
-  replace hli := hli.map' M.subtype (Submodule.ker_subtype M)
-  rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli
-  rw [h, ← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
-  obtain ⟨hfin, hcard⟩ := hs
-  have hsubset : Set.range (fun x : s ↦ x.val.val) ⊆ M := by
-    rintro x ⟨a, rfl⟩
-    simp
-  have hcard : Fintype.card ↑s = Module.finrank K V := by simpa
-  rw [_root_.eq_top_iff]
-  rw [← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]
-  exact Submodule.span_mono hsubset
-
-omit [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K] in
-/-- A finitely-generated `R`-submodule of `V` that has rank the `K`-rank of `V` is
-a lattice. -/
-lemma of_rank [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
-    (hfg : M.FG) (hr : Module.rank R M = Module.rank K V) : IsLattice K M where
-  fg := hfg
-  span_eq_top := span_eq_top_of_rank K hr
+lemma finrank_of_pi {ι : Type*} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K))
+    [IsLattice K M] : Module.finrank R M = Fintype.card ι :=
+  Module.finrank_eq_of_rank_eq (IsLattice.rank_of_pi K M)
 
 /-- The intersection of two lattices is a lattice. -/
-theorem inf [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V)
-    [IsLattice K M] [IsLattice K N] :
-    IsLattice K (M ⊓ N) where
+instance inf [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V)
+    [IsLattice K M] [IsLattice K N] : IsLattice K (M ⊓ N) where
   fg := by
-    have aux : M.FG := IsLattice.fg
-    have : IsNoetherian R M := isNoetherian_of_fg_of_noetherian M aux
-    have g : (M ⊓ N) ≤ M := inf_le_left
-    have : IsNoetherian R ↥(M ⊓ N) := isNoetherian_of_le g
-    have h : Module.Finite R ↥(M ⊓ N):= Module.IsNoetherian.finite R ↥(M ⊓ N)
-    apply Module.Finite.iff_fg.mp
-    exact h
+    have : IsNoetherian R ↥(M ⊓ N) := isNoetherian_of_le inf_le_left
+    rw [← Module.Finite.iff_fg]
+    infer_instance
   span_eq_top := by
-    apply span_eq_top_of_rank
+    rw [← range_subtype (M ⊓ N)]
+    apply Submodule.span_range_eq_top_of_injective_of_rank (M ⊓ N).injective_subtype
     have h := Submodule.rank_sup_add_rank_inf_eq M N
     rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h
-    apply Cardinal.eq_of_add_eq_add_left h
-    exact Module.rank_lt_aleph0 K V
+    exact Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)
 
-end
+end Field
 
 end IsLattice
 

From 257930a5740bf30a600750ab9af0aa0296f2ea36 Mon Sep 17 00:00:00 2001
From: judithludwig <judith.ludwig@iwr.uni-heidelberg.de>
Date: Wed, 11 Dec 2024 11:29:26 +0100
Subject: [PATCH 3/4] improved docu

---
 Mathlib/Algebra/Module/Lattice.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Module/Lattice.lean b/Mathlib/Algebra/Module/Lattice.lean
index 820481c7dc758..0edaac04aeb7e 100644
--- a/Mathlib/Algebra/Module/Lattice.lean
+++ b/Mathlib/Algebra/Module/Lattice.lean
@@ -13,12 +13,13 @@ import Mathlib.LinearAlgebra.FreeModule.PID
 Let `A` be an `R`-algebra and `V` an `A`-module. Then an `R`-submodule `M` of `V` is a lattice,
 if `M` is finitely generated and spans `V` as an `A`-module.
 
-The typical use case is `A = K` is the fraction field of `R` and `V = ι → K` for some finite `ι`.
-In this case there is a natural action of `GL ι K` on the type of lattices, whose stabilizer
-at the standard lattice is `GL ι R`.
+The typical use case is `A = K` is the fraction field of an integral domain `R` and `V = ι → K`
+for some finite `ι`. The scalar multiple a lattice by a unit in `K` is again a lattice. This gives
+rise to a homothety relation.
 
-By taking the quotient of the type of `R`-lattices in `ι → K` by the homothety relation,
-one obtains the vertices of what is called the Bruhat-Tits tree of `GL 2 K` when `ι = Fin 2`.
+When `R` is a DVR and `ι = Fin 2`, then by taking the quotient of the type of `R`-lattices in
+`ι → K` by the homothety relation, one obtains the vertices of what is called the Bruhat-Tits tree
+of `GL 2 K`.
 
 ## Main definitions
 
@@ -31,7 +32,7 @@ Let `R` be a PID and `A = K` its field of fractions.
 
 - `Submodule.IsLattice.free`: Every lattice in `V` is `R`-free.
 - `Basis.extendOfIsLattice`: Any `R`-basis of a lattice `M` in `V` defines a `K`-basis of `V`.
-- `Submodule.IsLattice.rank`: The `R`-rank of a lattice in `V` equals to the `K`-rank of `V`.
+- `Submodule.IsLattice.rank`: The `R`-rank of a lattice in `V` is equal to the `K`-rank of `V`.
 - `Submodule.IsLattice.inf`: The intersection of two lattices is a lattice.
 
 -/

From 1bcff7c20d130f30d4b8cda069b4bc2d768d2fb3 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 12 Dec 2024 14:06:02 +0100
Subject: [PATCH 4/4] review suggestions

---
 Mathlib/Algebra/Module/Lattice.lean | 42 +++++++++++++++--------------
 1 file changed, 22 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Algebra/Module/Lattice.lean b/Mathlib/Algebra/Module/Lattice.lean
index 820481c7dc758..8492540cd1288 100644
--- a/Mathlib/Algebra/Module/Lattice.lean
+++ b/Mathlib/Algebra/Module/Lattice.lean
@@ -83,27 +83,37 @@ instance smul [IsLattice A M] (a : Aˣ) : IsLattice A (a • M : Submodule R V)
     rw [show x = a • a⁻¹ • x by simp]
     exact Submodule.smul_mem_pointwise_smul _ _ _ (by trivial)
 
+lemma of_le_of_isLattice_of_fg {M N : Submodule R V} (hle : M ≤ N) [IsLattice A M]
+    (hfg : N.FG) : IsLattice A N :=
+  ⟨hfg, eq_top_iff.mpr <|
+    le_trans (b := span A M) (by rw [IsLattice.span_eq_top]) (Submodule.span_mono hle)⟩
+
+/-- The supremum of two lattices is a lattice. -/
+instance sup (M N : Submodule R V) [IsLattice A M] [IsLattice A N] :
+    IsLattice A (M ⊔ N) :=
+  of_le_of_isLattice_of_fg A le_sup_left (Submodule.FG.sup IsLattice.fg IsLattice.fg)
+
 end
 
 section Field
 
 variable {K : Type*} [Field K] [Algebra R K]
 
-lemma _root_.Submodule.span_range_eq_top_of_injective_of_rank {M N : Type u} [IsDomain R]
+lemma _root_.Submodule.span_range_eq_top_of_injective_of_rank_le {M N : Type u} [IsDomain R]
     [IsFractionRing R K] [AddCommGroup M] [Module R M]
     [AddCommGroup N] [Module R N] [Module K N] [IsScalarTower R K N] [Module.Finite K N]
-    {f : M →ₗ[R] N} (hf : Function.Injective f)
-    (h : Module.rank R M = Module.rank K N) :
+    {f : M →ₗ[R] N} (hf : Function.Injective f) (h : Module.rank K N ≤ Module.rank R M) :
     Submodule.span K (LinearMap.range f : Set N) = ⊤ := by
   obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M
   replace hli := hli.map' f (LinearMap.ker_eq_bot.mpr hf)
   rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli
-  rw [h, ← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
+  replace hs : Cardinal.mk s = Module.rank K N :=
+    le_antisymm (LinearIndependent.cardinal_le_rank hli) (hs ▸ h)
+  rw [← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
   obtain ⟨hfin, hcard⟩ := hs
   have hsubset : Set.range (fun x : s ↦ f x.val) ⊆ (LinearMap.range f : Set N) := by
     rintro x ⟨a, rfl⟩
     simp
-  have hcard : Fintype.card ↑s = Module.finrank K N := by simpa
   rw [eq_top_iff, ← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]
   exact Submodule.span_mono hsubset
 
@@ -131,21 +141,13 @@ lemma _root_.Basis.extendOfIsLattice_apply [IsFractionRing R K] {κ : Type*}
 
 variable [IsDomain R]
 
-/-- A finitely-generated `R`-submodule of `V` that has rank the `K`-rank of `V` is
-a lattice. -/
-lemma of_rank [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
-    (hfg : M.FG) (hr : Module.rank R M = Module.rank K V) : IsLattice K M where
+/-- A finitely-generated `R`-submodule of `V` of rank at least the `K`-rank of `V`
+is a lattice. -/
+lemma of_rank_le [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
+    (hfg : M.FG) (hr : Module.rank K V ≤ Module.rank R M) : IsLattice K M where
   fg := hfg
   span_eq_top := by
-    simpa using Submodule.span_range_eq_top_of_injective_of_rank M.injective_subtype hr
-
-/-- The supremum of two lattices is a lattice. -/
-instance sup (M N : Submodule R V) [IsLattice K M] [IsLattice K N] :
-    IsLattice K (M ⊔ N) where
-  fg := Submodule.FG.sup IsLattice.fg IsLattice.fg
-  span_eq_top := by
-    rw [eq_top_iff]
-    exact le_trans (b := span K M) (by rw [IsLattice.span_eq_top]) (Submodule.span_mono (by simp))
+    simpa using Submodule.span_range_eq_top_of_injective_of_rank_le M.injective_subtype hr
 
 variable [IsPrincipalIdealRing R]
 
@@ -185,10 +187,10 @@ instance inf [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V)
     infer_instance
   span_eq_top := by
     rw [← range_subtype (M ⊓ N)]
-    apply Submodule.span_range_eq_top_of_injective_of_rank (M ⊓ N).injective_subtype
+    apply Submodule.span_range_eq_top_of_injective_of_rank_le (M ⊓ N).injective_subtype
     have h := Submodule.rank_sup_add_rank_inf_eq M N
     rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h
-    exact Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)
+    rw [Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)]
 
 end Field