feat: progress on computing modular characters in concrete types

FLT/FLT_files.lean

@@ -8,16 +8,32 @@ import FLT.EllipticCurve.Torsion
 import FLT.ForMathlib.ActionTopology
 import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
+import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.ForMathlib.MiscLemmas
+import FLT.ForMathlib.Topology.Algebra.Algebra
 import FLT.FromMathlib.Algebra
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.flatness
+import FLT.HaarMeasure.ConcreteCharCalculations
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Hard.Results
-import FLT.HIMExperiments.flatness
+import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import FLT.Mathlib.Algebra.Group.Subgroup.Defs
+import FLT.Mathlib.Algebra.Group.Units.Hom
+import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Data.Complex.Basic
+import FLT.Mathlib.Data.ENNReal.Inv
+import FLT.Mathlib.GroupTheory.Complement
+import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.RingTheory.Norm.Defs
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct

FLT/ForMathlib/MeasurableSpacePadics.lean

@@ -0,0 +1,50 @@
+import Mathlib.MeasureTheory.Measure.Haar.Basic
+import Mathlib.NumberTheory.Padics.ProperSpace
+
+open Topology TopologicalSpace MeasureTheory Measure
+
+variable {p : ℕ} [Fact p.Prime]
+
+instance : MeasurableSpace ℚ_[p] := borel _
+instance : BorelSpace ℚ_[p] := ⟨rfl⟩
+
+instance : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
+instance : BorelSpace ℤ_[p] := Subtype.borelSpace _
+
+lemma PadicInt.isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
+  refine IsOpen.isOpenEmbedding_subtypeVal (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1})
+  simpa only [Metric.closedBall, dist_eq_norm_sub, sub_zero] using
+    IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero
+
+lemma PadicInt.isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
+  convert PadicInt.isOpenEmbedding_coe.measurableEmbedding
+  exact inferInstanceAs (BorelSpace ℤ_[p])
+
+noncomputable instance : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩
+
+instance : IsAddHaarMeasure (volume : Measure ℤ_[p]) := isAddHaarMeasure_addHaarMeasure _
+
+lemma PadicInt.volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self
+
+-- should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
+private def Padic.unitBall_positiveCompact : PositiveCompacts ℚ_[p] where
+  carrier := {y | ‖y‖ ≤ 1}
+  isCompact' := by simpa only [Metric.closedBall, dist_zero_right] using
+    isCompact_closedBall (0 : ℚ_[p]) 1
+  interior_nonempty' := by
+    rw [IsOpen.interior_eq]
+    · exact ⟨0, by simp⟩
+    · simpa only [Metric.closedBall, dist_zero_right] using
+        IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero
+
+noncomputable instance : MeasureSpace ℚ_[p] := ⟨addHaarMeasure Padic.unitBall_positiveCompact⟩
+
+instance : IsAddHaarMeasure (volume : Measure ℚ_[p]) := isAddHaarMeasure_addHaarMeasure _
+
+lemma Padic.volume_closedBall : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self
+
+lemma PadicInt.volume_addSubgroupClosure (x : ℤ_[p]ˣ) :
+    volume (AddSubgroup.closure {x.1} : Set ℤ_[p]) = ‖x.1‖₊⁻¹ := sorry
+
+lemma Padic.volume_smul (x : ℚ_[p]ˣ) : volume (AddSubgroup.closure {x.1} : Set ℚ_[p]) = ‖x.1‖₊⁻¹ :=
+  sorry

FLT/HaarMeasure/ConcreteCharCalculations.lean

@@ -0,0 +1,79 @@
+import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+import Mathlib.RingTheory.Complex
+import Mathlib.RingTheory.Localization.NumDen
+import Mathlib.Analysis.Normed.Group.Ultra
+import FLT.ForMathlib.MeasurableSpacePadics
+import FLT.HaarMeasure.DistribHaarChar
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Data.Complex.Basic
+import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.RingTheory.Norm.Defs
+
+open Real Complex Padic MeasureTheory Measure NNReal Set TopologicalSpace
+open scoped Pointwise ENNReal Localization
+
+lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)‖₊ ^ (-2 : ℤ) := by
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1 ×ℂ Icc 0 1) (μ := volume)
+    (measure_pos_of_nonempty_interior _ <| by simp [interior_reProdIm]).ne'
+    (isCompact_Icc.reProdIm isCompact_Icc).measure_ne_top ?_
+  have key : ((LinearMap.mul ℂ ℂ z).restrictScalars ℝ).det = ‖z.val‖₊ ^ 2 := by
+    refine Complex.ofReal_injective ?_
+    rw [LinearMap.det_restrictScalars]
+    simp [Algebra.norm_complex_apply, normSq_eq_norm_sq, zpow_ofNat]
+  have := addHaar_preimage_linearMap (E := ℂ) volume
+    (f := (LinearMap.mul ℂ ℂ z).restrictScalars ℝ)
+  simp [key] at this
+  convert this _ using 2
+  · symm
+    exact Set.preimage_smul z _
+  · simp [← Real.ennnorm_eq_ofReal_abs, ← Complex.norm_eq_abs, zpow_ofNat]
+
+lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊⁻¹ := by
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1) (μ := volume)
+    (measure_pos_of_nonempty_interior _ <| by simp).ne' isCompact_Icc.measure_ne_top ?_
+  rw [Units.smul_def, Measure.addHaar_smul]
+  simp [Real.ennnorm_eq_ofReal_abs, abs_inv, ENNReal.ofReal_inv_of_pos]
+
+variable {p : ℕ} [Fact p.Prime]
+
+private lemma distribHaarChar_padic_integral (x : nonZeroDivisors ℤ_[p]) :
+  distribHaarChar ℚ_[p] (x : ℚ_[p]ˣ) = ‖(x : ℚ_[p])‖₊⁻¹ := by
+  let K : AddSubgroup ℚ_[p] :=
+    (IsUltrametricDist.closedBall_openAddSubgroup _ (zero_lt_one)).toAddSubgroup
+  -- have : K = ℤ_[p] := rfl
+  -- TODO: See `FLT.Mathlib.Analysis.Normed.Group.Ultra`. This would make `K = ℤ_[p]` definitionally
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := K) (μ := volume) (G := ℚ_[p]ˣ)
+    (by simp [K, IsUltrametricDist.closedBall_openAddSubgroup, Metric.closedBall, Padic.volume_closedBall (p := p)])
+    (by simp [K, IsUltrametricDist.closedBall_openAddSubgroup, Metric.closedBall, Padic.volume_closedBall (p := p)])
+    ?_
+  rw [Units.smul_def]
+  simp
+  let H := (x : ℚ_[p])⁻¹ • K
+  rw [← ENNReal.mul_eq_mul_left (a := H.relindex K) (by sorry) (by sorry)]
+  let h : (H.addSubgroupOf K).FiniteIndex := sorry
+  change _ * volume (H : Set ℚ_[p]) = _
+  rw [index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup (μ := volume) (K := K)]
+  -- volume (K) = 1 via this line
+  -- simp [K, IsUltrametricDist.closedBall_openAddSubgroup, Metric.closedBall, Padic.volume_closedBall]
+  sorry
+  sorry
+  · exact measurableSet_closedBall.const_smul (x⁻¹ : ℚ_[p]ˣ)
+  · exact measurableSet_closedBall
+
+lemma distribHaarChar_padic (x : ℚ_[p]ˣ) : distribHaarChar ℚ_[p] x = ‖(x : ℚ_[p])‖₊⁻¹ := by
+  let g : ℚ_[p]ˣ →* ℝ≥0 := {
+    toFun := fun x => ‖(x : ℚ_[p])‖₊⁻¹
+    map_one' := by simp
+    map_mul' := by simp [mul_comm]
+  }
+  revert x
+  suffices distribHaarChar ℚ_[p] = g by simp [this, g]
+  refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDiviorsZp_eq_unitsQp (p := p)) ?_
+  simp
+  ext x
+  simp [g]
+  rw [distribHaarChar_padic_integral]
+  rfl

FLT/HaarMeasure/DistribHaarChar.lean

@@ -78,3 +78,8 @@ lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ
 lemma distribHaarChar_eq_div (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (g : G) :
     distribHaarChar A g = μ (g⁻¹ • s) / μ s := by
   rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right hs₀ hs]
+
+lemma distribHaarChar_eq_of_measure_smul_eq_mul (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) {r : ℝ≥0}
+    (hμgs : μ (g⁻¹ • s) = r * μ s) : distribHaarChar A g = r := by
+  refine ENNReal.coe_injective ?_
+  rw [distribHaarChar_eq_div hs₀ hs, hμgs, ENNReal.mul_div_cancel_right hs₀ hs]

FLT/Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -0,0 +1,6 @@
+import Mathlib.Algebra.Group.Subgroup.Defs
+
+namespace Subgroup
+
+-- TODO: Rename in mathlib
+@[to_additive] alias coe_subtype := coeSubtype

FLT/Mathlib/Algebra/Group/Units/Hom.lean

@@ -0,0 +1,8 @@
+import Mathlib.Algebra.Group.Units.Hom
+
+variable {M N : Type*} [Monoid M] [Monoid N]
+
+@[to_additive (attr := simp)]
+lemma Units.map_mk (f : M →* N) (val inv : M) (val_inv inv_val) :
+    map f (mk val inv val_inv inv_val) = mk (f val) (f inv)
+      (by rw [← f.map_mul, val_inv, f.map_one]) (by rw [← f.map_mul, inv_val, f.map_one]) := rfl

FLT/Mathlib/Analysis/Complex/Basic.lean

@@ -0,0 +1,9 @@
+
+import Mathlib.Analysis.Complex.Basic
+
+open Complex
+
+variable {s t : Set ℝ}
+
+lemma IsCompact.reProdIm (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ℂ t) :=
+  equivRealProdCLM.toHomeomorph.isCompact_preimage.2 (hs.prod ht)

FLT/Mathlib/Analysis/Normed/Group/Ultra.lean

@@ -0,0 +1,5 @@
+/-!
+# TODO
+
+Change the definition of `closedBall_openSubgroup` from `{x | dist 0 x} ≤ 1` to `{x | ‖x‖ ≤ 1}`.
+-/

FLT/Mathlib/Data/Complex/Basic.lean

@@ -0,0 +1,19 @@
+import Mathlib.Data.Complex.Basic
+
+open Set
+
+namespace Complex
+variable {s t : Set ℝ}
+
+open Set
+
+lemma «forall» {p : ℂ → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ := by aesop
+lemma «exists» {p : ℂ → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ := by aesop
+
+@[simp] lemma reProdIm_nonempty : (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
+  simp [Set.Nonempty, reProdIm, Complex.exists]
+
+@[simp] lemma reProdIm_eq_empty : s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
+  simp [← not_nonempty_iff_eq_empty, reProdIm_nonempty, -not_and, not_and_or]
+
+end Complex

FLT/Mathlib/GroupTheory/Complement.lean

@@ -0,0 +1,49 @@
+import Mathlib.GroupTheory.Complement
+
+open Set
+open scoped Pointwise
+
+namespace Subgroup
+variable {G : Type*} [Group G] {s t : Set G}
+
+@[to_additive (attr := simp)]
+lemma not_isComplement_empty_left : ¬ IsComplement ∅ t :=
+  fun h ↦ by simpa [eq_comm (a := ∅)] using h.mul_eq
+
+@[to_additive (attr := simp)]
+lemma not_isComplement_empty_right : ¬ IsComplement s ∅ :=
+  fun h ↦ by simpa [eq_comm (a := ∅)] using h.mul_eq
+
+@[to_additive]
+lemma IsComplement.nonempty_of_left (hst : IsComplement s t) : s.Nonempty := by
+  contrapose! hst; simp [hst]
+
+@[to_additive]
+lemma IsComplement.nonempty_of_right (hst : IsComplement s t) : t.Nonempty := by
+  contrapose! hst; simp [hst]
+
+@[to_additive]
+lemma not_empty_mem_leftTransversals : ∅ ∉ leftTransversals s := not_isComplement_empty_left
+
+@[to_additive]
+lemma not_empty_mem_rightTransversals : ∅ ∉ rightTransversals s := not_isComplement_empty_right
+
+@[to_additive]
+lemma nonempty_of_mem_leftTransversals (hst : s ∈ leftTransversals t) : s.Nonempty :=
+  hst.nonempty_of_left
+
+@[to_additive]
+lemma nonempty_of_mem_rightTransversals (hst : s ∈ rightTransversals t) : s.Nonempty :=
+  hst.nonempty_of_right
+
+variable {H : Subgroup G} [H.FiniteIndex]
+
+@[to_additive]
+lemma finite_of_mem_leftTransversals (hs : s ∈ leftTransversals H) : s.Finite :=
+  Nat.finite_of_card_ne_zero <| by rw [card_left_transversal hs]; exact FiniteIndex.finiteIndex
+
+@[to_additive]
+lemma finite_of_mem_rightTransversals (hs : s ∈ rightTransversals H) : s.Finite :=
+  Nat.finite_of_card_ne_zero <| by rw [card_right_transversal hs]; exact FiniteIndex.finiteIndex
+
+end Subgroup

FLT/Mathlib/LinearAlgebra/Determinant.lean

@@ -0,0 +1,8 @@
+import Mathlib.LinearAlgebra.Determinant
+
+namespace LinearMap
+variable {R : Type*} [CommRing R]
+
+variable (R) in
+@[simp] lemma det_mul (a : R) : (mul R R a).det = a := by
+  sorry

FLT/Mathlib/MeasureTheory/Group/Action.lean

@@ -0,0 +1,67 @@
+import Mathlib.MeasureTheory.Group.Action
+import Mathlib.MeasureTheory.Group.Pointwise
+import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
+import FLT.Mathlib.Algebra.Group.Subgroup.Defs
+import FLT.Mathlib.GroupTheory.Complement
+
+/-!
+# TODO
+
+* Make `α` implicit in `SMulInvariantMeasure`
+* Rename `SMulInvariantMeasure` to `Measure.IsSMulInvariant`
+-/
+
+open Subgroup Set
+open scoped Pointwise
+
+namespace MeasureTheory
+variable {G α : Type*} [Group G] [MeasurableSpace G] [MeasurableMul G] [MeasurableSpace α]
+  {H K : Subgroup G}
+
+@[to_additive]
+instance : MeasurableMul H where
+  measurable_mul_const c := have := measurable_mul_const (c : G); sorry
+  measurable_const_mul c := sorry
+
+@[to_additive]
+instance (μ : Measure G) [μ.IsMulLeftInvariant] :
+    (μ.comap Subtype.val : Measure H).IsMulLeftInvariant where
+  map_mul_left_eq_self g := sorry
+
+@[to_additive]
+instance (μ : Measure G) [μ.IsMulRightInvariant] :
+    (μ.comap Subtype.val : Measure H).IsMulRightInvariant where
+  map_mul_right_eq_self g := sorry
+
+@[to_additive index_mul_addHaar_addSubgroup]
+lemma index_mul_haar_subgroup [H.FiniteIndex] (hH : MeasurableSet (H : Set G)) (μ : Measure G)
+    [μ.IsMulLeftInvariant] : H.index * μ H = μ univ := by
+  obtain ⟨s, hs, -⟩ := H.exists_left_transversal 1
+  have hs' : Finite s := finite_of_mem_leftTransversals hs
+  calc
+    H.index * μ H = ∑' a : s, μ (a.val • H) := by
+      simp [measure_smul]
+      rw [← Set.Finite.cast_ncard_eq hs', ← Nat.card_coe_set_eq, card_left_transversal hs]
+      norm_cast
+    _ = μ univ := by
+      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
+      · simp [hs.mul_eq]
+      · sorry
+
+@[to_additive index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup]
+lemma index_mul_haar_subgroup_eq_haar_subgroup [(H.subgroupOf K).FiniteIndex] (hHK : H ≤ K)
+    (hH : MeasurableSet (H : Set G)) (hK : MeasurableSet (K : Set G)) (μ : Measure G)
+    [μ.IsMulLeftInvariant] : H.relindex K * μ H = μ K := by
+  have := index_mul_haar_subgroup (H := H.subgroupOf K) (measurable_subtype_coe hH)
+    (μ.comap Subtype.val)
+  simp at this
+  rw [MeasurableEmbedding.comap_apply, MeasurableEmbedding.comap_apply] at this
+  simp at this
+  unfold subgroupOf at this
+  rw [coe_comap, coe_subtype, Set.image_preimage_eq_of_subset] at this
+  exact this
+  simpa
+  exact .subtype_coe hK
+  exact .subtype_coe hK
+
+end MeasureTheory