feat: progress on computing modular characters in concrete types

FLT/FLT_files.lean

@@ -12,15 +12,33 @@ 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.HaarMeasure.MeasurableSpacePadics
 import FLT.Hard.Results
-import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
 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.GroupWithZero.NonZeroDivisors
+import FLT.Mathlib.Algebra.Module.End
+import FLT.Mathlib.Algebra.Module.NatInt
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Analysis.Normed.Group.Ultra
+import FLT.Mathlib.Data.Complex.Basic
 import FLT.Mathlib.Data.ENNReal.Inv
+import FLT.Mathlib.GroupTheory.Complement
+import FLT.Mathlib.GroupTheory.Index
+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.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct
@@ -30,9 +48,6 @@ import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
-import FLT.Mathlib.RingTheory.Norm.Defs
-import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
-import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal

FLT/HaarMeasure/ConcreteCharCalculations.lean

@@ -0,0 +1,84 @@
+import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.Analysis.Normed.Group.Ultra
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+import Mathlib.RingTheory.Complex
+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.RingTheory.Norm.Defs
+import FLT.HaarMeasure.DistribHaarChar
+import FLT.HaarMeasure.MeasurableSpacePadics
+
+open Real Complex Padic MeasureTheory Measure NNReal Set  IsUltrametricDist Metric
+open scoped Pointwise ENNReal Localization nonZeroDivisors
+
+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
+    simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def]
+      using Set.preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1)
+  · simp [ofReal_norm_eq_coe_nnnorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]
+  · simp [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 finiteIndex_smul (x : ℤ_[p]⁰) :
+    (((x : ℚ_[p]) • (closedBall_openAddSubgroup ℚ_[p] zero_lt_one).toAddSubgroup).addSubgroupOf
+      (closedBall_openAddSubgroup ℚ_[p] zero_lt_one)).FiniteIndex := sorry
+
+private lemma relindex_smul (x : ℤ_[p]⁰) :
+    ((x : ℚ_[p]) • (closedBall_openAddSubgroup ℚ_[p] zero_lt_one).toAddSubgroup).relindex
+      (closedBall_openAddSubgroup ℚ_[p] zero_lt_one) = ‖(x : ℚ_[p])‖₊ :=
+  sorry
+
+private lemma distribHaarChar_padic_integral (x : ℤ_[p]⁰) :
+    distribHaarChar ℚ_[p] (x : ℚ_[p]ˣ) = ‖(x : ℚ_[p])‖₊ := by
+  let Z : AddSubgroup ℚ_[p] := (closedBall_openAddSubgroup _ zero_lt_one).toAddSubgroup
+  -- have : K = ℤ_[p] := rfl
+  -- TODO: See `FLT.Mathlib.Analysis.Normed.Group.Ultra`. This would make `Z = ℤ_[p]` definitionally
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := Z) (μ := volume) (G := ℚ_[p]ˣ)
+    (by simp [Z, closedBall_openAddSubgroup, Metric.closedBall, Padic.volume_closedBall])
+    (by simp [Z, closedBall_openAddSubgroup, Metric.closedBall, Padic.volume_closedBall]) ?_
+  let H := (x : ℚ_[p]) • Z
+  rw [Units.smul_def]
+  change volume (H : Set ℚ_[p]) = _
+  have : (H.addSubgroupOf Z).FiniteIndex := finiteIndex_smul _
+  rw [← index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup (μ := volume) (H := H) (K := Z)]
+  · congr 1
+    rw [relindex_smul]
+    exact mod_cast relindex_smul x
+  · sorry
+  · exact measurableSet_closedBall
+  · exact measurableSet_closedBall.const_smul (x : ℚ_[p]ˣ)
+
+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
+  }
+  revert x
+  suffices distribHaarChar ℚ_[p] = g by simp [this, g]
+  refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDivisors_padicInt (p := p)) ?_
+  simp
+  ext x
+  simp [g]
+  rw [distribHaarChar_padic_integral]
+  rfl

FLT/HaarMeasure/DistribHaarChar.lean

@@ -66,16 +66,19 @@ lemma addHaarScalarFactor_smul_eq_distribHaarChar_inv (g : G) :
 lemma distribHaarChar_pos : 0 < distribHaarChar A g :=
   pos_iff_ne_zero.mpr ((Group.isUnit g).map (distribHaarChar A)).ne_zero
 
-variable [IsFiniteMeasureOnCompacts μ] [Regular μ] {s : Set A}
+variable [Regular μ] {s : Set A}
 
 variable (μ) in
-omit [IsFiniteMeasureOnCompacts μ] in
 lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ (g • s) := by
   have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [dma_smul_apply]
   rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
     ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
 
-omit [IsFiniteMeasureOnCompacts μ] in
 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/HaarMeasure/MeasurableSpacePadics.lean

@@ -0,0 +1,61 @@
+import Mathlib.MeasureTheory.Measure.Haar.Basic
+import Mathlib.NumberTheory.Padics.ProperSpace
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+
+open Topology TopologicalSpace MeasureTheory Measure
+open scoped Pointwise nonZeroDivisors
+
+variable {p : ℕ} [Fact p.Prime]
+
+namespace Padic
+
+instance : MeasurableSpace ℚ_[p] := borel _
+instance : BorelSpace ℚ_[p] := ⟨rfl⟩
+
+-- should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
+private def 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 volume_closedBall : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self
+
+end Padic
+
+namespace PadicInt
+
+instance : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
+instance : BorelSpace ℤ_[p] := Subtype.borelSpace _
+
+lemma 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 isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
+  convert isOpenEmbedding_coe.measurableEmbedding
+  exact inferInstanceAs (BorelSpace ℤ_[p])
+
+noncomputable instance : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩
+
+instance : IsAddHaarMeasure (volume : Measure ℤ_[p]) := isAddHaarMeasure_addHaarMeasure _
+
+@[simp] lemma volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self
+
+lemma volume_smul (x : ℤ_[p]⁰) : volume (x • ⊤ : Set ℤ_[p]) = ‖x.1‖₊⁻¹ := by
+  rw [← index_smul_top]
+
+end PadicInt
+
+lemma Padic.volume_smul {x : ℚ_[p]} (hx : x ≠ 0) : volume (x • {y : ℚ_[p] | ‖y‖ ≤ 1}) = ‖x‖₊⁻¹ :=
+  sorry

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/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -0,0 +1,13 @@
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
+
+open scoped nonZeroDivisors
+
+variable {G₀ : Type*} [GroupWithZero G₀]
+
+@[simps]
+noncomputable def nonZeroDivisorsEquivUnits : G₀⁰ ≃* G₀ˣ where
+  toFun u := .mk0 _ <| mem_nonZeroDivisors_iff_ne_zero.1 u.2
+  invFun u := ⟨u, u.isUnit.mem_nonZeroDivisors⟩
+  left_inv u := rfl
+  right_inv u := by simp
+  map_mul' u v := by simp

FLT/Mathlib/Algebra/Module/End.lean

@@ -0,0 +1,3 @@
+import Mathlib.Algebra.Module.End
+
+attribute [norm_cast] Int.cast_smul_eq_zsmul

FLT/Mathlib/Algebra/Module/NatInt.lean

@@ -0,0 +1,3 @@
+import Mathlib.Algebra.Module.NatInt
+
+attribute [norm_cast] Nat.cast_smul_eq_nsmul

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,54 @@
+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 IsComplement.pairwiseDisjoint_smul (hst : IsComplement s t) :
+    s.PairwiseDisjoint (· • t) := fun a ha b hb hab ↦ disjoint_iff_forall_ne.2 <| by
+  rintro _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩
+  exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂:= (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])
+
+@[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/GroupTheory/Index.lean

@@ -0,0 +1,22 @@
+import Mathlib.GroupTheory.Index
+
+open Function
+open scoped Pointwise
+
+namespace Subgroup
+variable {G H : Type*} [Group G] [Group H] {f : G →* H}
+
+@[to_additive]
+lemma index_map_of_bijective (S : Subgroup G) (hf : Bijective f) : (S.map f).index = S.index :=
+  index_map_eq _ hf.2 (by rw [f.ker_eq_bot_iff.2 hf.1]; exact bot_le)
+
+end Subgroup
+
+namespace AddSubgroup
+variable {G A : Type*} [Group G] [AddGroup A] [DistribMulAction G A]
+
+-- TODO: Why does making this lemma simp make `NumberTheory.Padic.PadicIntegers` time out?
+lemma index_smul (a : G) (S : AddSubgroup A) : (a • S).index = S.index :=
+  index_map_of_bijective _ (MulAction.bijective _)
+
+end AddSubgroup

FLT/Mathlib/LinearAlgebra/Determinant.lean

@@ -0,0 +1,11 @@
+import Mathlib.LinearAlgebra.Determinant
+
+namespace LinearMap
+variable {R : Type*} [CommRing R]
+
+@[simp] lemma det_mul (a : R) : (mul R R a).det = a := by
+  classical
+  rw [det_eq_det_toMatrix_of_finset (s := {1}) ⟨(Finsupp.LinearEquiv.finsuppUnique R R _).symm⟩,
+    Matrix.det_unique]
+  change a * _ = a
+  simp