chore: Define the class IsZlattice (#11356)

See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)

Author: xroblot

Mathlib/Algebra/Module/Zlattice.lean

@@ -55,6 +55,8 @@ variable [NormedAddCommGroup E] [NormedSpace K E]
 
 variable (b : Basis ι K E)
 
+theorem span_top : span K (span ℤ (Set.range b) : Set E) = ⊤ := by simp [span_span_of_tower]
+
 /-- The fundamental domain of the ℤ-lattice spanned by `b`. See `Zspan.isAddFundamentalDomain`
 for the proof that it is a fundamental domain. -/
 def fundamentalDomain : Set E := {m | ∀ i, b.repr m i ∈ Set.Ico (0 : K) 1}
@@ -310,6 +312,10 @@ instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)) := by
   · exact discreteTopology_pi_basisFun
   · refine Subtype.map_injective _ (Basis.equivFun b).injective
 
+instance [Fintype ι] : DiscreteTopology (span ℤ (Set.range b)).toAddSubgroup := by
+  change DiscreteTopology (span ℤ (Set.range b))
+  infer_instance
+
 @[measurability]
 theorem fundamentalDomain_measurableSet [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] :
     MeasurableSet (fundamentalDomain b) := by
@@ -367,14 +373,26 @@ end Zspan
 
 section Zlattice
 
-open Submodule
+open Submodule FiniteDimensional
+
+-- TODO: generalize this class to other rings than `ℤ`
+/-- An `L : Addsubgroup E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if
+it is discrete and spans `E` over `K`. -/
+class IsZlattice (K : Type*) [NormedField K] {E : Type*} [NormedAddCommGroup E] [NormedSpace K E]
+    (L : AddSubgroup E) [DiscreteTopology L] : Prop where
+  /-- `L` spans the full space `E` over `K`. -/
+  span_top : span K (L : Set E) = ⊤
+
+theorem _root_.Zspan.isZlattice {E ι : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+    [Fintype ι] (b : Basis ι ℝ E) :
+    IsZlattice ℝ (span ℤ (Set.range b)).toAddSubgroup where
+  span_top := Zspan.span_top b
 
 variable (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
-variable [ProperSpace E] {L : AddSubgroup E} [DiscreteTopology L]
-variable (hs : span K (L : Set E) = ⊤)
+variable [ProperSpace E] (L : AddSubgroup E) [DiscreteTopology L]
 
-theorem Zlattice.FG : AddSubgroup.FG L := by
+theorem Zlattice.FG [hs : IsZlattice K L] : AddSubgroup.FG L := by
   suffices (AddSubgroup.toIntSubmodule L).FG by exact (fg_iff_add_subgroup_fg _).mp this
   obtain ⟨s, ⟨h_incl, ⟨h_span, h_lind⟩⟩⟩ := exists_linearIndependent K (L : Set E)
   -- Let `s` be a maximal `K`-linear independent family of elements of `L`. We show that
@@ -386,7 +404,7 @@ theorem Zlattice.FG : AddSubgroup.FG L := by
     -- so there are finitely many since `fundamentalDomain b` is bounded.
     refine fg_def.mpr ⟨map (span ℤ s).mkQ (AddSubgroup.toIntSubmodule L), ?_, span_eq _⟩
     let b := Basis.mk h_lind (by
-      rw [← hs, ← h_span]
+      rw [← hs.span_top, ← h_span]
       exact span_mono (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl]))
     rw [show span ℤ s = span ℤ (Set.range b) by simp [b, Basis.coe_mk, Subtype.range_coe_subtype]]
     have : Fintype s := h_lind.setFinite.fintype
@@ -409,24 +427,53 @@ theorem Zlattice.FG : AddSubgroup.FG L := by
     rw [ker_mkQ, inf_of_le_right (span_le.mpr h_incl)]
     exact fg_span (LinearIndependent.setFinite h_lind)
 
-theorem Zlattice.module_finite : Module.Finite ℤ L :=
-  Module.Finite.iff_addGroup_fg.mpr ((AddGroup.fg_iff_addSubgroup_fg L).mpr (FG K hs))
-
-theorem Zlattice.module_free : Module.Free ℤ L := by
-  have : Module.Finite ℤ L := module_finite K hs
+theorem Zlattice.module_finite [IsZlattice K L] : Module.Finite ℤ L :=
+  Module.Finite.iff_addGroup_fg.mpr ((AddGroup.fg_iff_addSubgroup_fg L).mpr (FG K L))
+
+instance instModuleFinite_of_discrete_addSubgroup {E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : AddSubgroup E) [DiscreteTopology L] :
+    Module.Finite ℤ L := by
+  let f := (span ℝ (L : Set E)).subtype
+  let L₀ := (AddSubgroup.toIntSubmodule L).comap (f.restrictScalars ℤ)
+  have h_img : f '' L₀ = L := by
+    rw [← LinearMap.coe_restrictScalars ℤ f, ← Submodule.map_coe (f.restrictScalars ℤ),
+      Submodule.map_comap_eq_self, AddSubgroup.coe_toIntSubmodule]
+    exact fun x hx ↦ LinearMap.mem_range.mpr ⟨⟨x, Submodule.subset_span hx⟩, rfl⟩
+  suffices Module.Finite ℤ L₀ by
+    have : L₀.map (f.restrictScalars ℤ) = (AddSubgroup.toIntSubmodule L) :=
+      SetLike.ext'_iff.mpr h_img
+    convert this ▸ Module.Finite.map L₀ (f.restrictScalars ℤ)
+  have : DiscreteTopology L₀.toAddSubgroup := by
+    refine DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)
+    exact LinearMap.continuous_of_finiteDimensional f
+  have : IsZlattice ℝ L₀.toAddSubgroup := ⟨by
+    rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
+      Submodule.map_top, range_subtype, coe_toAddSubgroup, h_img]⟩
+  exact Zlattice.module_finite ℝ L₀.toAddSubgroup
+
+theorem Zlattice.module_free [IsZlattice K L] : Module.Free ℤ L := by
+  have : Module.Finite ℤ L := module_finite K L
   have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
   have : NoZeroSMulDivisors ℤ E := RatModule.noZeroSMulDivisors
   have : NoZeroSMulDivisors ℤ L := by
     change NoZeroSMulDivisors ℤ (AddSubgroup.toIntSubmodule L)
     exact noZeroSMulDivisors _
   infer_instance
 
-open FiniteDimensional
+instance instModuleFree__of_discrete_addSubgroup {E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : AddSubgroup E) [DiscreteTopology L] :
+    Module.Free ℤ L := by
+  have : Module ℚ E := Module.compHom E (algebraMap ℚ ℝ)
+  have : NoZeroSMulDivisors ℤ E := RatModule.noZeroSMulDivisors
+  have : NoZeroSMulDivisors ℤ L := by
+    change NoZeroSMulDivisors ℤ (AddSubgroup.toIntSubmodule L)
+    exact noZeroSMulDivisors _
+  infer_instance
 
-theorem Zlattice.rank : finrank ℤ L = finrank K E := by
+theorem Zlattice.rank [hs : IsZlattice K L] : finrank ℤ L = finrank K E := by
   classical
-  have : Module.Finite ℤ L := module_finite K hs
-  have : Module.Free ℤ L := module_free K hs
+  have : Module.Finite ℤ L := module_finite K L
+  have : Module.Free ℤ L := module_free K L
   have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
   let b₀ := Module.Free.chooseBasis ℤ L
   -- Let `b` be a `ℤ`-basis of `L` formed of vectors of `E`
@@ -439,7 +486,9 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
     · rw [map_span, Set.range_comp]
       rfl
     · exact (map_subtype_top _).symm
-  have h_spanE : span K (Set.range b) = ⊤ := by rwa [← span_span_of_tower (R := ℤ), h_spanL]
+  have h_spanE : span K (Set.range b) = ⊤ := by
+    rw [← span_span_of_tower (R := ℤ), h_spanL]
+    exact hs.span_top
   have h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ L) =
       (Set.range b).toFinset.card := by
     rw [Set.toFinset_range, Finset.univ.card_image_of_injective]

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

@@ -1078,10 +1078,6 @@ theorem exists_ne_zero_mem_ideal_of_norm_le {B : ℝ}
   have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
     change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)): Set (E K))
     infer_instance
-  have : DiscreteTopology
-      (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
-    change DiscreteTopology (span ℤ (Set.range (fractionalIdealLatticeBasis K I)): Set (E K))
-    infer_instance
   obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure
       h_fund (fun _ ↦ convexBodySum_neg_mem K B) (convexBodySum_convex K B)
       (convexBodySum_compact K B) h

Mathlib/NumberTheory/NumberField/Units.lean

@@ -478,22 +478,18 @@ instance instDiscrete_unitLattice : DiscreteTopology (unitLattice K) := by
     rintro ⟨x, hx, rfl⟩
     exact ⟨Subtype.mem x, hx⟩
 
+instance instZlattice_unitLattice : IsZlattice ℝ (unitLattice K) where
+  span_top := unitLattice_span_eq_top K
+
 protected theorem finrank_eq_rank :
     finrank ℝ ({w : InfinitePlace K // w ≠ w₀} → ℝ) = Units.rank K := by
   simp only [finrank_fintype_fun_eq_card, Fintype.card_subtype_compl,
     Fintype.card_ofSubsingleton, rank]
 
-instance instModuleFree_unitLattice : Module.Free ℤ (unitLattice K) :=
-  Zlattice.module_free ℝ (unitLattice_span_eq_top K)
-
-instance instModuleFinite_unitLattice : Module.Finite ℤ (unitLattice K) :=
-  Zlattice.module_finite ℝ (unitLattice_span_eq_top K)
-
 @[simp]
 theorem unitLattice_rank :
     finrank ℤ (unitLattice K) = Units.rank K := by
-  rw [← Units.finrank_eq_rank]
-  exact Zlattice.rank ℝ (unitLattice_span_eq_top K)
+  rw [← Units.finrank_eq_rank, Zlattice.rank ℝ]
 
 /-- The linear equivalence between `unitLattice` and `(𝓞 K)ˣ ⧸ (torsion K)` as an additive
 `ℤ`-module. -/
@@ -514,7 +510,7 @@ def unitLatticeEquiv : (unitLattice K) ≃ₗ[ℤ] Additive ((𝓞 K)ˣ ⧸ (tor
     rfl
 
 instance : Module.Free ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
-  (instModuleFree_unitLattice K).of_equiv' (unitLatticeEquiv K)
+  Module.Free.of_equiv (unitLatticeEquiv K)
 
 instance : Module.Finite ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
   Module.Finite.equiv (unitLatticeEquiv K)

Mathlib/Topology/Constructions.lean

@@ -1209,6 +1209,14 @@ theorem DiscreteTopology.of_subset {X : Type*} [TopologicalSpace X] {s t : Set X
   (embedding_inclusion ts).discreteTopology
 #align discrete_topology.of_subset DiscreteTopology.of_subset
 
+/-- Let `s` be a discrete subset of a topological space. Then the preimage of `s` by
+a continuous injective map is also discrete. -/
+theorem DiscreteTopology.preimage_of_continuous_injective {X Y : Type*} [TopologicalSpace X]
+    [TopologicalSpace Y] (s : Set Y) [DiscreteTopology s] {f : X → Y} (hc : Continuous f)
+    (hinj : Function.Injective f) : DiscreteTopology (f ⁻¹' s) :=
+  DiscreteTopology.of_continuous_injective (β := s) (Continuous.restrict
+    (by exact fun _ x ↦ x) hc) ((Set.MapsTo.restrict_inj _).mpr <| Set.injOn_of_injective hinj _)
+
 end Subtype
 
 section Quotient