diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean index ee8017b8..bd08d006 100644 --- a/FLT/FLT_files.lean +++ b/FLT/FLT_files.lean @@ -12,15 +12,34 @@ import FLT.GaloisRepresentation.HardlyRamified import FLT.GlobalLanglandsConjectures.GLnDefs import FLT.GlobalLanglandsConjectures.GLzero import FLT.GroupScheme.FiniteFlat -import FLT.HaarMeasure.DistribHaarChar -import FLT.Hard.Results import FLT.HIMExperiments.flatness +import FLT.HaarMeasure.DistribHaarChar.Basic +import FLT.HaarMeasure.DistribHaarChar.Padic +import FLT.HaarMeasure.DistribHaarChar.RealComplex +import FLT.HaarMeasure.MeasurableSpacePadics +import FLT.Hard.Results 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.Subgroup.Pointwise +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.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 +49,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 diff --git a/FLT/HaarMeasure/DistribHaarChar.lean b/FLT/HaarMeasure/DistribHaarChar/Basic.lean similarity index 89% rename from FLT/HaarMeasure/DistribHaarChar.lean rename to FLT/HaarMeasure/DistribHaarChar/Basic.lean index bb6bfe67..05027b90 100644 --- a/FLT/HaarMeasure/DistribHaarChar.lean +++ b/FLT/HaarMeasure/DistribHaarChar/Basic.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] + rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right] <;> simp [*] + +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] <;> simp [*] diff --git a/FLT/HaarMeasure/DistribHaarChar/Padic.lean b/FLT/HaarMeasure/DistribHaarChar/Padic.lean new file mode 100644 index 00000000..f1807508 --- /dev/null +++ b/FLT/HaarMeasure/DistribHaarChar/Padic.lean @@ -0,0 +1,106 @@ +/- +Copyright (c) 2024 Yaël Dillies, Javier Lopez-Contreras. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yaël Dillies, Javier Lopez-Contreras +-/ +import FLT.Mathlib.MeasureTheory.Group.Action +import FLT.HaarMeasure.DistribHaarChar.Basic +import FLT.HaarMeasure.MeasurableSpacePadics + +/-! +# The distributive Haar characters of the p-adics + +This file computes `distribHaarChar` in the case of the actions of `ℤ_[p]ˣ` on `ℤ_[p]` and of +`ℚ_[p]ˣ` on `ℚ_[p]`. + +This lets us know what `volume (x • s)` is in terms of `‖x‖` and `volume s`, when `x` is a +p-adic/p-adic integer and `s` is a set of p-adics/p-adic integers. + +## Main declarations + +* `distribHaarChar_padic`: `distribHaarChar ℚ_[p]` is the usual p-adic norm on `ℚ_[p]`. +* `distribHaarChar_padicInt`: `distribHaarChar ℤ_[p]` is the usual p-adic norm on `ℤ_[p]`. +* `Padic.volume_padic_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℚ_[p]` and + `s : Set ℚ_[p]`. +* `PadicInt.volume_padicInt_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℤ_[p]` and + `s : Set ℤ_[p]`. +-/ + +open Padic MeasureTheory Measure Metric Set +open scoped Pointwise ENNReal NNReal nonZeroDivisors + +variable {p : ℕ} [Fact p.Prime] + +private lemma distribHaarChar_padic_padicInt (x : ℤ_[p]⁰) : + distribHaarChar ℚ_[p] (x : ℚ_[p]ˣ) = ‖(x : ℚ_[p])‖₊ := by + -- Let `K` be the copy of `ℤ_[p]` inside `ℚ_[p]` and `H` be `xK`. + let K : AddSubgroup ℚ_[p] := (Submodule.span ℤ_[p] 1).toAddSubgroup + let H := (x : ℚ_[p]) • K + -- We compute that `volume H = ‖x‖₊ * volume K`. + refine distribHaarChar_eq_of_measure_smul_eq_mul (s := K) (μ := volume) (G := ℚ_[p]ˣ) + (by simp [K, Padic.submoduleSpan_padicInt_one, closedBall, Padic.volume_closedBall_one]) + (by simp [K, Padic.submoduleSpan_padicInt_one, closedBall, Padic.volume_closedBall_one]) ?_ + change volume (H : Set ℚ_[p]) = ‖(x : ℚ_[p])‖₊ * volume (K : Set ℚ_[p]) + -- This is true because `H` is a `‖x‖₊⁻¹`-index subgroup of `K`. + have hHK : H ≤ K := by + simpa [H, K, -Submodule.smul_le_self_of_tower] + using (.span _ 1 : Submodule ℤ_[p] ℚ_[p]).smul_le_self_of_tower (x : ℤ_[p]) + have : H.FiniteRelIndex K := + PadicInt.smul_submoduleSpan_finiteRelIndex_submoduleSpan (p := p) + (mem_nonZeroDivisors_iff_ne_zero.1 x.2) {1} + have H_relindex_Z : (H.relindex K : ℝ≥0∞) = ‖(x : ℚ_[p])‖₊⁻¹ := + congr(ENNReal.ofNNReal $(PadicInt.smul_submoduleSpan_relindex_submoduleSpan (p := p) x {1})) + rw [← index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup hHK, H_relindex_Z, ENNReal.coe_inv, + ENNReal.mul_inv_cancel_left] + · simp + · simp + · simp + · simpa [H, K, Padic.submoduleSpan_padicInt_one] + using measurableSet_closedBall.const_smul (x : ℚ_[p]ˣ) + · simpa [K, Padic.submoduleSpan_padicInt_one] using measurableSet_closedBall + +/-- The distributive Haar character of the action of `ℚ_[p]ˣ` on `ℚ_[p]` is the usual p-adic norm. + +This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℚ_[p]` and `s : Set ℚ_[p]`. +See `Padic.volume_padic_smul` -/ +lemma distribHaarChar_padic (x : ℚ_[p]ˣ) : distribHaarChar ℚ_[p] x = ‖(x : ℚ_[p])‖₊ := by + -- Write the RHS as the application of a monoid hom `g`. + 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] + -- By density of `ℤ_[p]⁰` inside `ℚ_[p]ˣ`, it's enough to check that `distribHaarChar ℚ_[p]` and + -- `g` agree on `ℤ_[p]⁰`. + refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDivisors_padicInt (p := p)) ?_ + -- But this is what we proved in `distribHaarChar_padic_padicInt`. + simp + ext x + simp [g] + rw [distribHaarChar_padic_padicInt] + rfl + +@[simp] +lemma Padic.volume_padic_smul (x : ℚ_[p]) (s : Set ℚ_[p]) : volume (x • s) = ‖x‖₊ * volume s := by + obtain rfl | hx := eq_or_ne x 0 + · simp [(finite_zero.subset s.zero_smul_set_subset).measure_zero] + · lift x to ℚ_[p]ˣ using hx.isUnit + rw [← distribHaarChar_padic, distribHaarChar_mul, Units.smul_def] + +@[simp] lemma Padic.volume_padicInt_smul (x : ℤ_[p]) (s : Set ℚ_[p]) : + volume (x • s) = ‖x‖₊ * volume s := by simpa [-volume_padic_smul] using volume_padic_smul x s + +@[simp] lemma PadicInt.volume_padicInt_smul (x : ℤ_[p]) (s : Set ℤ_[p]) : + volume (x • s) = ‖x‖₊ * volume s := by + simpa [-volume_padicInt_smul, ← image_coe_smul_set] using Padic.volume_padicInt_smul x ((↑) '' s) + +/-- The distributive Haar character of the action of `ℤ_[p]ˣ` on `ℤ_[p]` is the usual p-adic norm. + +This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℤ_[p]` and `s : Set ℤ_[p]`. +See `PadicInt.volume_padicInt_smul` -/ +lemma distribHaarChar_padicInt (x : ℤ_[p]ˣ) : distribHaarChar ℤ_[p] x = ‖(x : ℤ_[p])‖₊ := + -- We compute `distribHaarChar ℤ_[p]` by lifting everything to `ℚ_[p]`. + distribHaarChar_eq_of_measure_smul_eq_mul (s := univ) (μ := volume) (by simp) (measure_ne_top _ _) + (PadicInt.volume_padicInt_smul ..) diff --git a/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean b/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean new file mode 100644 index 00000000..2a8af85a --- /dev/null +++ b/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2024 Yaël Dillies, Javier Lopez-Contreras. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yaël Dillies, Javier Lopez-Contreras +-/ +import Mathlib.Analysis.Complex.ReImTopology +import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar +import Mathlib.RingTheory.Complex +import FLT.HaarMeasure.DistribHaarChar.Basic +import FLT.Mathlib.Analysis.Complex.Basic +import FLT.Mathlib.Data.Complex.Basic +import FLT.Mathlib.LinearAlgebra.Determinant +import FLT.Mathlib.RingTheory.Norm.Defs + +/-! +# The distributive Haar characters of `ℝ` and `ℂ` + +This file computes `distribHaarChar` in the case of the actions of `ℝˣ` on `ℝ` and of `ℂˣ` on `ℂ`. + +This lets us know what `volume (x • s)` is in terms of `‖x‖` and `volume s`, when `x` is a +real/complex number and `s` is a set of reals/complex numbers. + +## Main declarations + +* `distribHaarChar_real`: `distribHaarChar ℝ` is the usual norm on `ℝ`. +* `distribHaarChar_complex`: `distribHaarChar ℂ` is the usual norm on `ℂ` squared. +* `Real.volume_real_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℝ` and `s : Set ℝ`. +* `Complex.volume_complex_smul`: `volume (z • s) = ‖z‖₊ ^ 2 * volume s` for all `z : ℂ` and + `s : Set ℂ`. +-/ + +open Real Complex MeasureTheory Measure Set +open scoped Pointwise + +lemma Real.volume_real_smul (x : ℝ) (s : Set ℝ) : volume (x • s) = ‖x‖₊ * volume s := by + simp [← ennnorm_eq_ofReal_abs] + +/-- The distributive Haar character of the action of `ℝˣ` on `ℝ` is the usual norm. + +This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℝ` and `s : Set ℝ`. +See `Real.volume_real_smul`. -/ +lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊ := + -- We compute that `volume (x • [0, 1]) = ‖x‖₊ * volume [0, 1]`. + 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 + (Real.volume_real_smul ..) + +/-- The distributive Haar character of the action of `ℂˣ` on `ℂ` is the usual norm squared. + +This means that `volume (z • s) = ‖z‖ ^ 2 * volume s` for all `z : ℂ` and `s : Set ℂ`. +See `Complex.volume_complex_smul`. -/ +lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)‖₊ ^ 2 := by + -- We compute that `volume (x • ([0, 1] × [0, 1])) = ‖x‖₊ ^ 2 * volume ([0, 1] × [0, 1])`. + 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 ?_ + -- The determinant of left multiplication by `z⁻¹` as a `ℝ`-linear map is `‖z‖₊ ^ (-2)`. + 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] + -- Massaging, we find the result. + 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 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 Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : volume (z • s) = ‖z‖₊ ^ 2 * volume s := by + obtain rfl | hz := eq_or_ne z 0 + · simp [(finite_zero.subset s.zero_smul_set_subset).measure_zero] + · lift z to ℂˣ using hz.isUnit + rw [← ENNReal.coe_pow, ← distribHaarChar_complex, distribHaarChar_mul, Units.smul_def] diff --git a/FLT/HaarMeasure/MeasurableSpacePadics.lean b/FLT/HaarMeasure/MeasurableSpacePadics.lean new file mode 100644 index 00000000..a62fa025 --- /dev/null +++ b/FLT/HaarMeasure/MeasurableSpacePadics.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2024 Yaël Dillies, David Loeffler. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yaël Dillies, David Loeffler +-/ +import Mathlib.MeasureTheory.Measure.Haar.Basic +import Mathlib.NumberTheory.Padics.ProperSpace +import FLT.Mathlib.NumberTheory.Padics.PadicIntegers + +/-! +# Measurability and measures on the p-adics + +This file endows `ℤ_[p]` and `ℚ_[p]` with their Borel sigma-algebra and their Haar measure that +makes `ℤ_[p]` (or the copy of `ℤ_[p]` inside `ℚ_[p]`) have norm `1`. +-/ + +open MeasureTheory Measure TopologicalSpace Topology + +variable {p : ℕ} [Fact p.Prime] + +namespace Padic + +instance instMeasurableSpace : MeasurableSpace ℚ_[p] := borel _ +instance instBorelSpace : 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 instMeasureSpace : MeasureSpace ℚ_[p] := + ⟨addHaarMeasure unitBall_positiveCompact⟩ + +instance instIsAddHaarMeasure : IsAddHaarMeasure (volume : Measure ℚ_[p]) := + isAddHaarMeasure_addHaarMeasure _ + +lemma volume_closedBall_one : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self + +end Padic + +namespace PadicInt + +instance instMeasurableSpace : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace +instance instBorelSpace : BorelSpace ℤ_[p] := Subtype.borelSpace _ + +lemma isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by + convert isOpenEmbedding_coe.measurableEmbedding + exact inferInstanceAs (BorelSpace ℤ_[p]) + +noncomputable instance instMeasureSpace : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩ + +instance instIsAddHaarMeasure : IsAddHaarMeasure (volume : Measure ℤ_[p]) := + isAddHaarMeasure_addHaarMeasure _ + +@[simp] lemma volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self + +instance instIsFiniteMeasure : IsFiniteMeasure (volume : Measure ℤ_[p]) where + measure_univ_lt_top := by simp + +-- https://github.com/ImperialCollegeLondon/FLT/issues/278 +@[simp] lemma volume_coe (s : Set ℤ_[p]) : volume ((↑) '' s : Set ℚ_[p]) = volume s := sorry + +end PadicInt diff --git a/FLT/Mathlib/Algebra/Group/Subgroup/Defs.lean b/FLT/Mathlib/Algebra/Group/Subgroup/Defs.lean new file mode 100644 index 00000000..fe6fbe35 --- /dev/null +++ b/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 diff --git a/FLT/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/FLT/Mathlib/Algebra/Group/Subgroup/Pointwise.lean new file mode 100644 index 00000000..bfee8106 --- /dev/null +++ b/FLT/Mathlib/Algebra/Group/Subgroup/Pointwise.lean @@ -0,0 +1,12 @@ +import Mathlib.Algebra.Group.Subgroup.Pointwise +import Mathlib.Algebra.Module.End + +open scoped Pointwise + +namespace AddSubgroup +variable {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M] + +@[simp] protected lemma smul_zero (s : AddSubgroup M) : (0 : R) • s = ⊥ := + show s.map (Module.toAddMonoidEnd _ _ 0) = ⊥ by simp + +end AddSubgroup diff --git a/FLT/Mathlib/Algebra/Group/Units/Hom.lean b/FLT/Mathlib/Algebra/Group/Units/Hom.lean new file mode 100644 index 00000000..7776f8fc --- /dev/null +++ b/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 diff --git a/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean b/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean new file mode 100644 index 00000000..4bb16e91 --- /dev/null +++ b/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean @@ -0,0 +1,15 @@ +import Mathlib.Algebra.GroupWithZero.NonZeroDivisors + +open scoped nonZeroDivisors + +variable {G₀ : Type*} [GroupWithZero G₀] + +attribute [simp] mem_nonZeroDivisors_iff_ne_zero + +@[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 diff --git a/FLT/Mathlib/Algebra/Module/End.lean b/FLT/Mathlib/Algebra/Module/End.lean new file mode 100644 index 00000000..3c9d217c --- /dev/null +++ b/FLT/Mathlib/Algebra/Module/End.lean @@ -0,0 +1,3 @@ +import Mathlib.Algebra.Module.End + +attribute [norm_cast] Int.cast_smul_eq_zsmul diff --git a/FLT/Mathlib/Algebra/Module/NatInt.lean b/FLT/Mathlib/Algebra/Module/NatInt.lean new file mode 100644 index 00000000..2ddfee7f --- /dev/null +++ b/FLT/Mathlib/Algebra/Module/NatInt.lean @@ -0,0 +1,3 @@ +import Mathlib.Algebra.Module.NatInt + +attribute [norm_cast] Nat.cast_smul_eq_nsmul diff --git a/FLT/Mathlib/Analysis/Complex/Basic.lean b/FLT/Mathlib/Analysis/Complex/Basic.lean new file mode 100644 index 00000000..0b2204f9 --- /dev/null +++ b/FLT/Mathlib/Analysis/Complex/Basic.lean @@ -0,0 +1,8 @@ +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) diff --git a/FLT/Mathlib/Data/Complex/Basic.lean b/FLT/Mathlib/Data/Complex/Basic.lean new file mode 100644 index 00000000..540cd127 --- /dev/null +++ b/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 diff --git a/FLT/Mathlib/Data/ENNReal/Inv.lean b/FLT/Mathlib/Data/ENNReal/Inv.lean index 797d6c80..dba25307 100644 --- a/FLT/Mathlib/Data/ENNReal/Inv.lean +++ b/FLT/Mathlib/Data/ENNReal/Inv.lean @@ -1,8 +1,41 @@ import Mathlib.Data.ENNReal.Inv namespace ENNReal +variable {a b : ℝ≥0∞} -protected lemma mul_div_cancel_right {b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb : b ≠ ∞) (a : ℝ≥0∞) : - a * b / b = a := by rw [ENNReal.mul_div_right_comm, ENNReal.div_mul_cancel hb₀ hb] +protected lemma inv_mul_cancel_left (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : + a⁻¹ * (a * b) = b := by + obtain rfl | ha₀ := eq_or_ne a 0 + · simp_all + obtain rfl | ha := eq_or_ne a ⊤ + · simp_all + · simp [← mul_assoc, ENNReal.inv_mul_cancel, *] + +protected lemma mul_inv_cancel_left (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : + a * (a⁻¹ * b) = b := by + obtain rfl | ha₀ := eq_or_ne a 0 + · simp_all + obtain rfl | ha := eq_or_ne a ⊤ + · simp_all + · simp [← mul_assoc, ENNReal.mul_inv_cancel, *] + +protected lemma mul_inv_cancel_right (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : + a * b * b⁻¹ = a := by + obtain rfl | hb₀ := eq_or_ne b 0 + · simp_all + obtain rfl | hb := eq_or_ne b ⊤ + · simp_all + · simp [mul_assoc, ENNReal.mul_inv_cancel, *] + +protected lemma inv_mul_cancel_right (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : + a * b⁻¹ * b = a := by + obtain rfl | hb₀ := eq_or_ne b 0 + · simp_all + obtain rfl | hb := eq_or_ne b ⊤ + · simp_all + · simp [mul_assoc, ENNReal.inv_mul_cancel, *] + +protected lemma mul_div_cancel_right (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : + a * b / b = a := ENNReal.mul_inv_cancel_right hb₀ hb end ENNReal diff --git a/FLT/Mathlib/GroupTheory/Complement.lean b/FLT/Mathlib/GroupTheory/Complement.lean new file mode 100644 index 00000000..0b1af2a8 --- /dev/null +++ b/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 diff --git a/FLT/Mathlib/GroupTheory/Index.lean b/FLT/Mathlib/GroupTheory/Index.lean new file mode 100644 index 00000000..9ee7b2da --- /dev/null +++ b/FLT/Mathlib/GroupTheory/Index.lean @@ -0,0 +1,46 @@ +import Mathlib.GroupTheory.Index + +/-! +# TODO + +* Rename `relindex` to `relIndex` +* Rename `FiniteIndex.finiteIndex` to `FiniteIndex.index_ne_zero` +-/ + +open Function +open scoped Pointwise + +-- This is cool notation. Should mathlib have it? And what should the `relindex` version be? +scoped[GroupTheory] notation "[" G ":" H "]" => @AddSubgroup.index G _ H + +namespace Subgroup +variable {G G' : Type*} [Group G] [Group G'] {f : G →* G'} {H K : Subgroup G} + +class _root_.AddSubgroup.FiniteRelIndex {G : Type*} [AddGroup G] (H K : AddSubgroup G) : Prop where + protected relIndex_ne_zero : H.relindex K ≠ 0 + +@[to_additive] class FiniteRelIndex (H K : Subgroup G) : Prop where + protected relIndex_ne_zero : H.relindex K ≠ 0 + +@[to_additive] +lemma relIndex_ne_zero [H.FiniteRelIndex K] : H.relindex K ≠ 0 := FiniteRelIndex.relIndex_ne_zero + +@[to_additive] +instance FiniteRelIndex.to_finiteIndex_subgroupOf [H.FiniteRelIndex K] : + (H.subgroupOf K).FiniteIndex where + finiteIndex := relIndex_ne_zero + +@[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 diff --git a/FLT/Mathlib/LinearAlgebra/Determinant.lean b/FLT/Mathlib/LinearAlgebra/Determinant.lean new file mode 100644 index 00000000..c653ef50 --- /dev/null +++ b/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 diff --git a/FLT/Mathlib/MeasureTheory/Group/Action.lean b/FLT/Mathlib/MeasureTheory/Group/Action.lean new file mode 100644 index 00000000..6e59c68d --- /dev/null +++ b/FLT/Mathlib/MeasureTheory/Group/Action.lean @@ -0,0 +1,66 @@ +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 +import FLT.Mathlib.GroupTheory.Index + +/-! +# 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 := by measurability + measurable_const_mul c := sorry -- https://github.com/ImperialCollegeLondon/FLT/issues/276 + +@[to_additive] +instance (μ : Measure G) [μ.IsMulLeftInvariant] : + (μ.comap Subtype.val : Measure H).IsMulLeftInvariant where + map_mul_left_eq_self g := sorry -- https://github.com/ImperialCollegeLondon/FLT/issues/276 + +@[to_additive] +instance (μ : Measure G) [μ.IsMulRightInvariant] : + (μ.comap Subtype.val : Measure H).IsMulRightInvariant where + map_mul_right_eq_self g := sorry -- https://github.com/ImperialCollegeLondon/FLT/issues/276 + +@[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] + · exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab) + +@[to_additive index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup] +lemma index_mul_haar_subgroup_eq_haar_subgroup [H.FiniteRelIndex K] (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 + rwa [coe_comap, coe_subtype, Set.image_preimage_eq_of_subset (by simpa)] at this + exact .subtype_coe hK + exact .subtype_coe hK + +end MeasureTheory diff --git a/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean new file mode 100644 index 00000000..9bda429f --- /dev/null +++ b/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -0,0 +1,110 @@ +import Mathlib.Algebra.CharZero.Infinite +import Mathlib.NumberTheory.Padics.PadicIntegers +import FLT.Mathlib.Algebra.Group.Subgroup.Pointwise +import FLT.Mathlib.Algebra.Group.Units.Hom +import FLT.Mathlib.Algebra.GroupWithZero.NonZeroDivisors +import FLT.Mathlib.GroupTheory.Index + +/-! +# TODO + +* Make `PadicInt.valuation` `ℕ`-valued +* Rename `Coe.ringHom` to `coeRingHom` +* Protect `PadicInt.norm_mul`, `PadicInt.norm_units`, `PadicInt.norm_pow` +-/ + +open Function Topology Subgroup +open scoped NNReal nonZeroDivisors Pointwise + +variable {p : ℕ} [Fact p.Prime] + +namespace PadicInt +variable {x : ℤ_[p]} + +attribute [simp] coe_eq_zero + +@[simp, norm_cast] lemma coe_coeRingHom : ⇑(Coe.ringHom (p := p)) = (↑) := rfl + +lemma coe_injective : Injective ((↑) : ℤ_[p] → ℚ_[p]) := Subtype.val_injective + +@[simp] lemma coe_inj {x y : ℤ_[p]} : (x : ℚ_[p]) = (y : ℚ_[p]) ↔ x = y := coe_injective.eq_iff + +instance : Infinite ℤ_[p] := CharZero.infinite _ + +@[simp] +protected lemma nnnorm_mul (x y : ℤ_[p]) : ‖x * y‖₊ = ‖x‖₊ * ‖y‖₊ := by simp [nnnorm, NNReal] + +@[simp] +protected lemma nnnorm_pow (x : ℤ_[p]) (n : ℕ) : ‖x ^ n‖₊ = ‖x‖₊ ^ n := by simp [nnnorm, NNReal] + +@[simp] lemma nnnorm_p : ‖(p : ℤ_[p])‖₊ = (p : ℝ≥0)⁻¹ := by simp [nnnorm]; rfl + +@[simp] protected lemma nnnorm_units (u : ℤ_[p]ˣ) : ‖(u : ℤ_[p])‖₊ = 1 := by simp [nnnorm, NNReal] + +-- TODO: Replace `valuation` +noncomputable def valuation' (a : ℤ_[p]) : ℕ := a.valuation.toNat + +lemma exists_unit_mul_p_pow_eq (hx : x ≠ 0) : ∃ (u : ℤ_[p]ˣ) (n : ℕ), (u : ℤ_[p]) * p ^ n = x := + ⟨_, _, (unitCoeff_spec hx).symm⟩ + +lemma isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by + refine (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1}).isOpenEmbedding_subtypeVal + simpa only [Metric.closedBall, dist_eq_norm_sub, sub_zero] using + IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero + +@[simp] lemma image_coe_smul_set (x : ℤ_[p]) (s : Set ℤ_[p]) : + ((↑) '' (x • s) : Set ℚ_[p]) = x • (↑) '' s := Set.image_comm fun _ ↦ rfl + +-- Yaël: Do we really want this as a coercion? +noncomputable instance : Coe ℤ_[p]ˣ ℚ_[p]ˣ where coe := Units.map Coe.ringHom.toMonoidHom + +/-- `x • sℤ_[p]` has index `‖x‖⁻¹` in `sℤ_[p]`. + +Note that `sℤ_[p]` is the form `yℤ_[p]` for some `y : ℚ_[p]`, but this is syntactically less +general. -/ +lemma smul_submoduleSpan_relindex_submoduleSpan (x : ℤ_[p]) (s : Set ℚ_[p]) : + (x • (Submodule.span ℤ_[p] s).toAddSubgroup).relindex (Submodule.span ℤ_[p] s).toAddSubgroup + = ‖x‖₊⁻¹ := + -- https://github.com/ImperialCollegeLondon/FLT/issues/279 + -- Note: You might need to prove `smul_submoduleSpan_finiteRelIndex_submoduleSpan` first + sorry + +/-- `x • sℤ_[p]` has finite index in `sℤ_[p]` if `x ≠ 0`. + +Note that `sℤ_[p]` is the form `yℤ_[p]` for some `y : ℚ_[p]`, but this is syntactically less +general. -/ +lemma smul_submoduleSpan_finiteRelIndex_submoduleSpan (hx : x ≠ 0) (s : Set ℚ_[p]) : + (x • (Submodule.span ℤ_[p] s).toAddSubgroup).FiniteRelIndex + (Submodule.span ℤ_[p] s).toAddSubgroup where + relIndex_ne_zero := by + simpa [← Nat.cast_ne_zero (R := ℝ≥0), smul_submoduleSpan_relindex_submoduleSpan] + +-- Yaël: Do we really want this as a coercion? +noncomputable instance : Coe ℤ_[p]⁰ ℚ_[p]ˣ where + coe x := .mk0 x.1 <| map_ne_zero_of_mem_nonZeroDivisors (M := ℤ_[p]) Coe.ringHom coe_injective x.2 + +/-- Non-zero p-adic integers generate non-zero p-adic numbers as a group. -/ +lemma closure_nonZeroDivisors_padicInt : + Subgroup.closure (Set.range ((↑) : ℤ_[p]⁰ → ℚ_[p]ˣ)) = ⊤ := by + set H := Subgroup.closure (Set.range ((↑) : ℤ_[p]⁰ → ℚ_[p]ˣ)) + rw [eq_top_iff'] + intro x + obtain ⟨y, z, hz, hyzx⟩ := IsFractionRing.div_surjective (A := ℤ_[p]) x.val + have hy : y ∈ ℤ_[p]⁰ := by simp; rintro rfl; simp [eq_comm] at hyzx + convert div_mem (H := H) (subset_closure <| Set.mem_range_self ⟨y, hy⟩) + (subset_closure <| Set.mem_range_self ⟨z, hz⟩) using 1 + ext + simpa using hyzx.symm + +end PadicInt + +namespace Padic + +lemma submoduleSpan_padicInt_one : + Submodule.span ℤ_[p] (1 : Set ℚ_[p]) = Metric.closedBall (0 : ℚ_[p]) 1 := by + rw [← Submodule.one_eq_span_one_set] + ext x + simp + simp [PadicInt] + +end Padic