feat(Module/ZLattice): define the pullback of a ZLattice (#16822)

Define the pullback of a ZLattice `L` by a linear map `f`. The following results are also included:

- If `f` is a continuous linear equiv, then the pullback is also a ZLattice (added as an instance).
- If `f` is a linear equiv, define the corresponding basis of the pullback obtained from a basis of `L` 
- If `f` is a continuous linear equiv and volume preserving, prove that `L` and its pullback have the same volume. 

This PR is part of the proof of the Analytic Class Number Formula.



Co-authored-by: Xavier Roblot <[email protected]>

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -24,14 +24,17 @@ A `ℤ`-lattice `L` can be defined in two ways:
 Results about the first point of view are in the `ZSpan` namespace and results about the second
 point of view are in the `ZLattice` namespace.
 
-## Main results
+## Main results and definitions
 
 * `ZSpan.isAddFundamentalDomain`: for a ℤ-lattice `Submodule.span ℤ (Set.range b)`, proves that
 the set defined by `ZSpan.fundamentalDomain` is a fundamental domain.
 * `ZLattice.module_free`: a `ℤ`-submodule of `E` that is discrete and spans `E` over `K` is a free
 `ℤ`-module
 * `ZLattice.rank`: a `ℤ`-submodule of `E` that is discrete and spans `E` over `K` is free
 of `ℤ`-rank equal to the `K`-rank of `E`
+* `ZLattice.comap`: for `e : E → F` a linear map and `L : Submodule ℤ E`, define the pullback of
+`L` by `e`. If `L` is a `IsZLattice` and `e` is a continuous linear equiv, then it is also a
+`IsZLattice`, see `instIsZLatticeComap`.
 
 ## Implementation Notes
 
@@ -58,6 +61,11 @@ variable (b : Basis ι K E)
 
 theorem span_top : span K (span ℤ (Set.range b) : Set E) = ⊤ := by simp [span_span_of_tower]
 
+
+theorem map {F : Type*} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) :
+    Submodule.map (f.restrictScalars ℤ) (span ℤ (Set.range b)) = span ℤ (Set.range (b.map f)) := by
+  simp_rw [Submodule.map_span, LinearEquiv.restrictScalars_apply, Basis.coe_map, Set.range_comp]
+
 /-- 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}
@@ -399,6 +407,8 @@ theorem _root_.ZSpan.isZLattice {E ι : Type*} [NormedAddCommGroup E] [NormedSpa
     IsZLattice ℝ (span ℤ (Set.range b)) where
   span_top := ZSpan.span_top b
 
+section NormedLinearOrderedField
+
 variable (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
 variable [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology L]
@@ -607,4 +617,81 @@ instance instCountable_of_discrete_submodule {E : Type*} [NormedAddCommGroup E]
   simp_rw [← (Module.Free.chooseBasis ℤ L).ofZLatticeBasis_span ℝ]
   infer_instance
 
+end NormedLinearOrderedField
+
+section comap
+
+variable (K : Type*) [NormedField K] {E F : Type*} [NormedAddCommGroup E] [NormedSpace K E]
+    [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E)
+
+/-- Let `e : E → F` a linear map, the map that sends a `L : Submodule ℤ E` to the
+`Submodule ℤ F` that is the pullback of `L` by `e`. If `IsZLattice L` and `e` is a continuous
+linear equiv, then it is a `IsZLattice` of `E`, see `instIsZLatticeComap`. -/
+protected def ZLattice.comap (e : F →ₗ[K] E) := L.comap (e.restrictScalars ℤ)
+
+@[simp]
+theorem ZLattice.coe_comap (e : F →ₗ[K] E) :
+    (ZLattice.comap K L e : Set F) = e⁻¹' L := rfl
+
+theorem ZLattice.comap_refl :
+    ZLattice.comap K L (1 : E →ₗ[K] E)= L := Submodule.comap_id L
+
+theorem ZLattice.comap_discreteTopology [hL : DiscreteTopology L] {e : F →ₗ[K] E}
+    (he₁ : Continuous e) (he₂ : Function.Injective e) :
+    DiscreteTopology (ZLattice.comap K L e) := by
+  exact DiscreteTopology.preimage_of_continuous_injective L he₁ he₂
+
+instance [DiscreteTopology L] (e : F ≃L[K] E) :
+    DiscreteTopology (ZLattice.comap K L e.toLinearMap) :=
+  ZLattice.comap_discreteTopology K L e.continuous e.injective
+
+theorem ZLattice.comap_span_top (hL : span K (L : Set E) = ⊤) {e : F →ₗ[K] E}
+    (he : (L : Set E) ⊆ LinearMap.range e) :
+    span K (ZLattice.comap K L e : Set F) = ⊤ := by
+  rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]
+
+instance instIsZLatticeComap [DiscreteTopology L] [IsZLattice K L] (e : F ≃L[K] E) :
+    IsZLattice K (ZLattice.comap K L e.toLinearMap) where
+  span_top := by
+    rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
+      ← Submodule.map_span, IsZLattice.span_top, Submodule.map_top, LinearEquivClass.range]
+
+theorem ZLattice.comap_comp {G : Type*} [NormedAddCommGroup G] [NormedSpace K G]
+    (e : F →ₗ[K] E) (e' : G →ₗ[K] F) :
+    (ZLattice.comap K (ZLattice.comap K L e) e') = ZLattice.comap K L (e ∘ₗ e') :=
+  (Submodule.comap_comp _ _ L).symm
+
+/-- If `e` is a linear equivalence, it induces a `ℤ`-linear equivalence between
+`L` and `ZLattice.comap K L e`. -/
+def ZLattice.comap_equiv (e : F ≃ₗ[K] E) :
+    L ≃ₗ[ℤ] (ZLattice.comap K L e.toLinearMap) :=
+  LinearEquiv.ofBijective
+    ((e.symm.toLinearMap.restrictScalars ℤ).restrict
+      (fun _ h ↦ by simpa [← SetLike.mem_coe] using h))
+    ⟨fun _ _ h ↦ Subtype.ext_iff_val.mpr (e.symm.injective (congr_arg Subtype.val h)),
+    fun ⟨x, hx⟩ ↦ ⟨⟨e x, by rwa [← SetLike.mem_coe, ZLattice.coe_comap] at hx⟩,
+      by simp [Subtype.ext_iff_val]⟩⟩
+
+@[simp]
+theorem ZLattice.comap_equiv_apply (e : F ≃ₗ[K] E) (x : L) :
+    ZLattice.comap_equiv K L e x = e.symm x := rfl
+
+/-- The basis of `ZLattice.comap K L e` given by the image of a basis `b` of `L` by `e.symm`. -/
+def Basis.ofZLatticeComap (e : F ≃ₗ[K] E) {ι : Type*}
+    (b : Basis ι ℤ L) :
+    Basis ι ℤ (ZLattice.comap K L e.toLinearMap) := b.map (ZLattice.comap_equiv K L e)
+
+@[simp]
+theorem Basis.ofZLatticeComap_apply (e : F ≃ₗ[K] E) {ι : Type*}
+    (b : Basis ι ℤ L) (i : ι) :
+    b.ofZLatticeComap K L e i = e.symm (b i) := by simp [Basis.ofZLatticeComap]
+
+@[simp]
+theorem Basis.ofZLatticeComap_repr_apply (e : F ≃ₗ[K] E) {ι : Type*} (b : Basis ι ℤ L) (x : L)
+    (i : ι) :
+    (b.ofZLatticeComap K L e).repr (ZLattice.comap_equiv K L e x) i = b.repr x i := by
+  simp [Basis.ofZLatticeComap]
+
+end comap
+
 end ZLattice

Mathlib/Algebra/Module/ZLattice/Covolume.lean

@@ -8,7 +8,7 @@ import Mathlib.Algebra.Module.ZLattice.Basic
 /-!
 # Covolume of ℤ-lattices
 
-Let `E` be a finite dimensional real vector space with an inner product.
+Let `E` be a finite dimensional real vector space.
 
 Let `L` be a `ℤ`-lattice `L` defined as a discrete `ℤ`-submodule of `E` that spans `E` over `ℝ`.
 
@@ -29,7 +29,7 @@ noncomputable section
 
 namespace ZLattice
 
-open Submodule MeasureTheory Module MeasureTheory Module
+open Submodule MeasureTheory Module MeasureTheory Module ZSpan
 
 section General
 
@@ -61,18 +61,30 @@ theorem covolume_eq_measure_fundamentalDomain {F : Set E} (h : IsAddFundamentalD
 theorem covolume_ne_zero : covolume L μ ≠ 0 := by
   rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
     ENNReal.toReal_ne_zero]
-  refine ⟨ZSpan.measure_fundamentalDomain_ne_zero _, ne_of_lt ?_⟩
-  exact Bornology.IsBounded.measure_lt_top (ZSpan.fundamentalDomain_isBounded _)
+  refine ⟨measure_fundamentalDomain_ne_zero _, ne_of_lt ?_⟩
+  exact Bornology.IsBounded.measure_lt_top (fundamentalDomain_isBounded _)
 
 theorem covolume_pos : 0 < covolume L μ :=
   lt_of_le_of_ne ENNReal.toReal_nonneg (covolume_ne_zero L μ).symm
 
+theorem covolume_comap {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
+    [MeasurableSpace F] [BorelSpace F] (ν : Measure F := by volume_tac) [Measure.IsAddHaarMeasure ν]
+    {e : F ≃L[ℝ] E} (he : MeasurePreserving e ν μ) :
+    covolume (ZLattice.comap ℝ L e.toLinearMap) ν = covolume L μ := by
+  rw [covolume_eq_measure_fundamentalDomain _ _ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
+    covolume_eq_measure_fundamentalDomain _ _ ((isAddFundamentalDomain
+    ((Free.chooseBasis ℤ L).ofZLatticeComap ℝ L e.toLinearEquiv) ν)), ← he.measure_preimage
+    (fundamentalDomain_measurableSet _).nullMeasurableSet, ← e.image_symm_eq_preimage,
+    ← e.symm.coe_toLinearEquiv, map_fundamentalDomain]
+  congr!
+  ext; simp
+
 theorem covolume_eq_det_mul_measure {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ L)
     (b₀ : Basis ι ℝ E) :
-    covolume L μ = |b₀.det ((↑) ∘ b)| * (μ (ZSpan.fundamentalDomain b₀)).toReal := by
+    covolume L μ = |b₀.det ((↑) ∘ b)| * (μ (fundamentalDomain b₀)).toReal := by
   rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),
-    ZSpan.measure_fundamentalDomain _ _ b₀,
-    measure_congr (ZSpan.fundamentalDomain_ae_parallelepiped b₀ μ), ENNReal.toReal_mul,
+    measure_fundamentalDomain _ _ b₀,
+    measure_congr (fundamentalDomain_ae_parallelepiped b₀ μ), ENNReal.toReal_mul,
     ENNReal.toReal_ofReal (by positivity)]
   congr
   ext
@@ -82,7 +94,7 @@ theorem covolume_eq_det {ι : Type*} [Fintype ι] [DecidableEq ι] (L : Submodul
     [DiscreteTopology L] [IsZLattice ℝ L] (b : Basis ι ℤ L) :
     covolume L = |(Matrix.of ((↑) ∘ b)).det| := by
   rw [covolume_eq_measure_fundamentalDomain L volume (isAddFundamentalDomain b volume),
-    ZSpan.volume_fundamentalDomain, ENNReal.toReal_ofReal (by positivity)]
+    volume_fundamentalDomain, ENNReal.toReal_ofReal (by positivity)]
   congr
   ext1
   exact b.ofZLatticeBasis_apply ℝ L _