random fixes

FLT/FLT_files.lean

@@ -21,6 +21,7 @@ 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.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
 import FLT.Mathlib.Analysis.Complex.Basic

FLT/HaarMeasure/ConcreteCharCalculations.lean

@@ -1,77 +1,81 @@
 import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.Analysis.Normed.Group.Ultra
 import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import Mathlib.RingTheory.Complex
-import Mathlib.RingTheory.Localization.NumDen
-import Mathlib.Analysis.Normed.Group.Ultra
-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.NumberTheory.Padics.MeasurableSpacePadics
 import FLT.Mathlib.RingTheory.Norm.Defs
+import FLT.HaarMeasure.DistribHaarChar
 
-open Real Complex Padic MeasureTheory Measure NNReal Set TopologicalSpace
+open Real Complex Padic MeasureTheory Measure NNReal Set  IsUltrametricDist Metric
 open scoped Pointwise ENNReal Localization
 
-lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)‖₊ ^ (-2 : ℤ) := by
+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
+  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 ℝ)
+    (f := (LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ)
   simp [key] at this
-  convert this _ using 2
+  convert this _ _ using 2
   · symm
-    exact Set.preimage_smul z _
-  · simp [← Real.ennnorm_eq_ofReal_abs, ← Complex.norm_eq_abs, zpow_ofNat]
+    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
+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 : nonZeroDivisors ℤ_[p]) :
+    ((closedBall_openAddSubgroup ℚ_[p] zero_lt_one).addSubgroupOf
+      ((x : ℚ_[p]) • (closedBall_openAddSubgroup _ zero_lt_one).toAddSubgroup)).FiniteIndex := sorry
+
+private lemma relindex_smul (x : nonZeroDivisors ℤ_[p]) :
+    (closedBall_openAddSubgroup ℚ_[p] zero_lt_one).toAddSubgroup.relindex
+      ((x : ℚ_[p]) • (closedBall_openAddSubgroup _ zero_lt_one).toAddSubgroup) = ‖(x : ℚ_[p])‖₊ :=
+  sorry
+
 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
+    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 `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)])
-    ?_
+  -- 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]
-  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]ˣ)
+  change volume (H : Set ℚ_[p]) = _
+  have : (Z.addSubgroupOf H).FiniteIndex := finiteIndex_smul _
+  rw [← index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup (μ := volume) (H := Z)]
+  · congr 1
+    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
+lemma distribHaarChar_padic (x : ℚ_[p]ˣ) : distribHaarChar ℚ_[p] x = ‖(x : ℚ_[p])‖₊ := by
   let g : ℚ_[p]ˣ →* ℝ≥0 := {
-    toFun := fun x => ‖(x : ℚ_[p])‖₊⁻¹
+    toFun := fun x => ‖(x : ℚ_[p])‖₊
     map_one' := by simp
-    map_mul' := by simp [mul_comm]
+    map_mul' := by simp
   }
   revert x
   suffices distribHaarChar ℚ_[p] = g by simp [this, g]
-  refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDiviorsZp_eq_unitsQp (p := p)) ?_
+  refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDivisorsZp_eq_unitsQp (p := p)) ?_
   simp
   ext x
   simp [g]

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/NumberTheory/Padics/PadicIntegers.lean

@@ -4,7 +4,8 @@ import FLT.Mathlib.Algebra.Group.Units.Hom
 /-!
 # TODO
 
-Make `PadicInt.valuation` `ℕ`-valued
+* Make `PadicInt.valuation` `ℕ`-valued
+* Rename `Coe.ringHom` to `coeRingHom`
 -/
 
 -- This is cool notation. Should mathlib have it?
@@ -43,14 +44,13 @@ lemma index_ideal_ppown (n : ℕ) :
   rw [AddSubgroup.index_eq_card]
   sorry
 
-def nonZeroDivisors_eq_units (G₀ : Type*) [GroupWithZero G₀] : nonZeroDivisors G₀ ≃* G₀ˣ := by sorry
-
-noncomputable instance  : Coe (nonZeroDivisors ℤ_[p]) ℚ_[p]ˣ where
+-- (Yaël): Do we really want this as a coercion?
+noncomputable instance : Coe (nonZeroDivisors ℤ_[p]) ℚ_[p]ˣ where
   coe x := .mk0 x.1 (map_ne_zero_of_mem_nonZeroDivisors (M := ℤ_[p])
     PadicInt.Coe.ringHom PadicInt.coe_injective x.2)
 
-lemma closure_nonZeroDiviorsZp_eq_unitsQp :
-  Subgroup.closure (Set.range ((↑) : (nonZeroDivisors ℤ_[p]) → ℚ_[p]ˣ)) = ⊤ :=
+lemma closure_nonZeroDivisorsZp_eq_unitsQp :
+    Subgroup.closure (Set.range ((↑) : (nonZeroDivisors ℤ_[p]) → ℚ_[p]ˣ)) = ⊤ :=
   sorry
 
 end PadicInt