Fundamental domains

Stream: FLT

[Kevin Buzzard]

So we're close to a sorry-free TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional and I hope to get this over the line before Christmas (I have plenty of time to work on this myself).

Annoyingly, my vision for how one proof would go has been punctured slightly. We need this basic fact that if $X$ is a locally compact additive abelian group (think $\mathbb{R}^n$) and $\Gamma$ is a countable discrete group of $X$ (think $\mathbb{Z}^n$) such that $X/\Gamma$ is compact, then for $U\subseteq X$ of sufficiently large (Haar) measure, the composite $U\to X\to X/\Gamma$ can't be injective. I had assumed that this would be somewhere in mathlib (and I don't even know a precise statement; maybe what I'm claiming is too general), but the best I can find is docs#MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd which, instead of using quotients, is using docs#IsAddFundamentalDomain and I can't find any magic way of constructing fundamental domains for discrete actions so I'm wondering if the easiest thing is simply to construct the fundamental domain in our situation. This will involve doing measure theory, which is definitely not my strong point. We actually need an adelic version, but only over $\mathbb{Q}$. Here is an example of what would be helpful to us (if we do everything for the adeles of $\mathbb{Q}$ then we can deduce everything in general, because $\mathbb{A}_K=\mathbb{A}_{\mathbb{Q}}\otimes_{\mathbb{Q}}K$).

import Mathlib

open NumberField Metric Measure MeasureTheory IsDedekindDomain

notation:101 "𝔸" K => AdeleRing (𝓞 K) K

instance : MeasurableSpace (𝔸 ℚ) := borel _
instance : BorelSpace (𝔸 ℚ) := ⟨rfl⟩

instance : LocallyCompactSpace (𝔸 ℚ) := sorry

-- is this how you make a VAdd from an Algebra?
noncomputable instance : VAdd ℚ (AdeleRing (𝓞 ℚ) ℚ) where
  vadd q a := algebraMap ℚ (𝔸 ℚ) q + a

def F : Set (𝔸 ℚ) := (Set.univ.pi fun _ => closedBall 0 0.5).prod
      (Set.range <| RestrictedProduct.structureMap _ _ _)

example : IsAddFundamentalDomain ℚ F Measure.addHaar := by
  sorry

I can't find any magic constructors for docs#IsAddFundamentalDomain so I think we might simply have to check the axioms. nullMeasurableSet and ae_covers shouldn't be too bad but I am a bit nervous about aedisjoint : Pairwise <| (AEDisjoint μ on fun g : G => g +ᵥ s). Another approach would be to use $[0,1)$ at infinity rather than $[-0.5,0.5]$ and then one can really prove disjointness; the measure-theory issues go away because this really would be a fundamental domain in the strict sense (it meets every orbit once, rather than up to a measure zero error); maybe this is a better idea (but then we'd have to figure out how to say $[0,1)$ in Set v.Completion where v : InfinitePlace ℚ, which is probably something we should be able to do anyway...

We need this for NumberField.AdeleRing.DivisionAlgebra.Aux.existsE in FLT/DivisionAlgebra/Finiteness.lean.

[Kevin Buzzard]

Actually, typing this message has made me realise that the most sensible approach is simply to use $[0,1)$ which makes all measure-theoretic issues go away. I'm now working on a variant of the above sorry which will suffice.

[Kevin Buzzard]

A couple of random things I've skipped:

import Mathlib

lemma Int.eq_floor {a : ℝ} {b : ℤ} (h1 : 0 ≤ a - b) (h2 : a - b < 1) : b = ⌊a⌋ := by
  sorry

example (t : ℝ) (ht : t ∈ Set.Ico 0 1) : ‖t‖ ≤ 1 := by
  sorry

but things are going well. I have a set and have reduced the proof that it's a fundamental domain to statements which are not measure-theoretic but are completely algebraic, which means that I should be able to use Salvatore's work on the way K sits in A_K.

[Sébastien Gouëzel]

Didn't we already have this kind of discussion some time ago, e.g. in #Is there code for X? > descending measures to compact quotients @ 💬 ?

[Kevin Buzzard]

Yes! And you told me that I had to make a fundamental domain and that's what I've been doing all afternoon.

[Kevin Buzzard]

In particular you pointed out docs#MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd but this needs a fundamental domain. What I want is: "U in X with measure > Bound => map U -> X -> X/Gamma not injective" and I had assumed that compactness of X/Gamma would be enough but my understanding of the discussion you linked to was that we didn't have a way of magically constructing a fundamental domain by abstract nonsense (and the key lemma needs a fundamental domain) so I am just writing one down explicitly.

[Kevin Buzzard]

Oh sorry, let me be more precise: you did give me a method for constructing a fundamental domain by mostly pure thought but then Antoine said this #Is there code for X? > descending measures to compact quotients @ 💬 so I figured I would follow his idea instead.

[Kevin Buzzard]

(The point is that we did all the algebraic work already when proving compactness)

[Michael Stoll]

Kevin Buzzard said:

example (t : ℝ) (ht : t ∈ Set.Ico 0 1) : ‖t‖ ≤ 1 := by
  sorry

import Mathlib

example (t : ℝ) (ht : t ∈ Set.Ico 0 1) : ‖t‖ ≤ 1 := by
  grind [Real.norm_eq_abs]

[Thomas Browning]

The abstract way of doing this is to take the Haar measures on $\Gamma$ and $X/\Gamma$, show that they define a Haar measure on $X$ satisfying $\int_X=\int_{X/\Gamma}\int_\Gamma$ (or rather, $\int_X=\int_{X/\Gamma}\sum_\Gamma$ since $\Gamma$ is discrete). Then $U\to X\to X/\Gamma$ being injective implies that the inner sum is $\leq1$, so $\mu(U)\leq\mu(X/\Gamma$.

[Thomas Browning]

I can play around with this today and see if it's workable if you want (I'm not sure how easy this Haar measures on short exact sequences thing is).

[Kevin Buzzard]

Right -- this was the proof which I had expected to be formalising, but my impression was that the other thread was guiding me towards using fundamental domains instead.

[Michael Stoll]

import Mathlib

lemma Int.eq_floor {a : ℝ} {b : ℤ} (h1 : 0 ≤ a - b) (h2 : a - b < 1) : b = ⌊a⌋ := by
  rw [eq_comm, Int.floor_eq_iff]
  grind

just in case...

[Thomas Browning]

Thomas Browning said:

The abstract way of doing this is to take the Haar measures on $\Gamma$ and $X/\Gamma$, show that they define a Haar measure on $X$ satisfying $\int_X=\int_{X/\Gamma}\int_\Gamma$ (or rather, $\int_X=\int_{X/\Gamma}\sum_\Gamma$ since $\Gamma$ is discrete). Then $U\to X\to X/\Gamma$ being injective implies that the inner sum is $\leq1$, so $\mu(U)\leq\mu(X/\Gamma$.

I've got a proof here: #32672. It's not super pretty yet, but I'll work on cleaning it up over the next few days. Is there a specific sorry in the FLT repo that we're looking to close?

[Kevin Buzzard]

There's something called existsE but that's several things rolled into one. I have a draft PR which contains something closer but it contains a bunch of other stuff too. Today quite busy though

[Kevin Buzzard]

OK on branch kbuzzard-existsE-workingtowards there's not_injective_of_large_measure in FLT/DivisionAlgebra/Finiteness.lean which should be enough for the application. You can assume that $D\subset D_{\mathbb{A}}$ is countable, discrete and cocompact, and that $D_{\mathbb{A}}$ is locally compact; we either have these already or they're easy from what we have.

[Thomas Browning]

Looks like I don't even need cocompactness, just discreteness (although they are equivalent, I think).

[Kevin Buzzard]

You mean for your integral formula? I can believe it. I just need compactness to guarantee finite measure in the application. I checked today that the statement on the FLT branch is enough for me.

[Thomas Browning]

Ok, I'll clean up the PR a bit more and then look into hooking it up to not_injective_of_large_measure.

[Thomas Browning]

So looks like I will need compactness of the quotient after all. Is this known, or will I need to use an explicit compact set (e.g., a fundamental domain or something larger)?

[Thomas Browning]

Or maybe it follows from cocompactness of the adeles?

[Kevin Buzzard]

We already have compactness of the quotient. What we didn't have was the fundamental domain.

[Thomas Browning]

Yes, it's looking like this will go through just fine, I think.

[Thomas Browning]

A bit hacky, but FLT#798 now closes the sorry in not_injective_of_large_measure

[Kevin Buzzard]

It's ready for merge as far as I'm concerned, but it's failing CI because the mathlib PR part of it doesn't lint:

  /- The `defLemma` linter reports:
  INCORRECT DEF/LEMMA: -/
  -- FLT.Mathlib.MeasureTheory.Haar.Extension
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:56:1: error: @TopologicalGroup.IsSES.ofClosedSubgroup is a def, should be lemma/theorem
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:57:3: error: @TopologicalAddGroup.IsSES.ofClosedAddSubgroup is a def, should be lemma/theorem

  /- The `docBlame` linter reports:
  DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
  -- FLT.Mathlib.MeasureTheory.Haar.Extension
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:79:3: error: @TopologicalAddGroup.IsSES.pullback definition missing documentation string
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:113:3: error: @TopologicalAddGroup.IsSES.pushforward definition missing documentation string
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:224:3: error: @TopologicalAddGroup.IsSES.integrate definition missing documentation string
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:248:3: error: @TopologicalAddGroup.IsSES.inducedMeasure definition missing documentation string

and I didn't want to start fixing it because I didn't want it to diverge too much from the mathlib PR, however the mathlib PR seems shorter than the version in FLT so I didn't quite know what to do.

[Thomas Browning]

Ah, these were linting errors in the mathlib PR as well. I'll copy it over.

[Thomas Browning]

It's only longer because it has one extra theorem at the end, I think.

[Thomas Browning]

It should lint now, I think

[Kevin Buzzard]

Thanks! It's merged.

[Alex Kontorovich]

Just seeing this thread. Long ago, Heather and I constructed the classical fundamental domain for $SL(2,\Z)\backslash SL(2,\R)$, in case that API may be useful here...

[Kevin Buzzard]

That sounds much harder than what I did! It's a nonabelian setting. I was lucky enough to be in a situation where I could write down a set-theoretic fundamental domain so all the measure theory could be avoided.

[Alex Kontorovich]

Won't you eventually need $GL(2,{\mathbb Q})\backslash GL(2,{\mathbb A})$...?

[Kevin Buzzard]

One day I will, but this is certainly not a priority; we've just got compactness of $D^\times\backslash (D\otimes_F\mathbb{A}_F)^\times$ for a totally definite quaternion algebra over a totally real field (I literally hit merge under an hour ago) and this will do for now; Jacquet--Langlands is going to be assumed...