Fermat's Last Theorem Blueprint

11. Miniproject: Fujisaki's Lemma🔗

In fact there is even a noncommutative version of this statement. In John Voight's book (Voight, 2021) this is Main Theorem 27.6.14(a) and Voight calls it Fujisaki's lemma. I know nothing of the history but I'm happy to adopt this name. In the quaternion algebra miniproject we will use this compactness result to prove finite-dimensionality of a space of quaternionic modular forms.

The compact quotient theorem for a division algebra is meant to be the noncommutative analogue of the classical compactness of K \backslash \mathbf{A}_K.

The TeX chapter uses this analogy repeatedly. The quotient K \backslash \mathbf{A}_K is the model case: a global field embedded discretely in its adeles with compact quotient. Fujisaki's lemma asks for the same style of compactness after replacing the commutative additive group by the norm-one units in an adelic division algebra.

11.1. Initial definitions🔗

Let K be a field. A central simple K-algebra is a K-algebra B not necessarily commutative with centre K such that B has exactly two two-sided ideals, namely {0} and B. We will be concerned only with central simple K-algebras which are finite-dimensional as K-vector spaces, and when K is clear we will just refer to them as central simple algebras. We remark that a 4-dimensional central simple algebra is called a quaternion algebra; we will have more to say about these later on.

Matrix algebras M_n(K) are examples of finite-dimensional central simple K-algebras. If K = ℂ or more generally if K is algebraically closed, then matrix algebras are the only finite-dimensional examples up to isomorphism.

There are other examples over the reals: for example Hamilton's quaternions ℍ := ℝ ⊕ ℝ i ⊕ ℝ j ⊕ ℝ k with the usual rules i^2 = j^2 = k^2 = -1, ij = -ji = k and so on are an example of a central simple ℝ-algebra, and matrix algebras over ℍ are other central simple ℝ-algebras. For a general field K one can make an analogue of Hamilton's quaternions K ⊕ Ki ⊕ Kj ⊕ Kk with the same multiplication rules to describe the multiplication, and if the characteristic of K is not 2 then this is a quaternion algebra which may or may not be isomorphic to M_2(K).

Some central simple algebras B are division algebras, meaning that they are division rings, or equivalently that every nonzero b\in B has a two-sided inverse. For example Hamilton's quaternions are a division algebra over \R, because (x+yi+zj+tk)(x-yi-zj-tk)=x^2+y^2+z^2+t^2, so the inverse of a nonzero x+yi+zj+tk is (x-yi-zj-tk)/(x^2+y^2+z^2+t^2).

However 2\times 2 matrices over a field K, whilst being a central simple algebra over K, are never a division algebra, because a nonzero matrix with determinant zero such as \begin{pmatrix}1&0\\0&0\end{pmatrix} has no inverse.

11.2. Enter the adeles🔗

Let K be a number field and let D/K be a finite-dimensional central simple K-algebra (later on D will be a division algebra, hence the name, but we do not need this yet). Then D_{\A}:=D\otimes_K\A_K is an \A_K-algebra which is free of finite rank, and if we give D_{\A} the \A_K-module topology then it is a topological ring. Furthermore D_{\A} is free of finite rank over the locally compact topological ring \A_K and is thus also locally compact. So by the theory of Haar characters (see [??]) there is a canonical character \delta_{D_{\A}}:D_{\A}^\times\to\R_{>0} measuring how left multiplication by an element of D_{\A}^\times changes the additive Haar measure on D_{\A}. Let D_{\A}^{(1)} denote the kernel of \delta_{D_{\A}}, and give it the subspace topology coming from D_{\A}^\times.

One can furthermore check that if R is a finite K-algebra then the \A_K-module topologies and \A_{\Q}-module topologies on R_{\A} coincide. Indeed, the topology on \A_K is the \A_{\Q}-module topology, as \A_K=\A_{\Q}\otimes_{\Q}K as topological \A_{\Q}-algebras, where the right hand side has the \A_{\Q}-module topology by definition.

11.3. The proof🔗

Lemma11.3.1
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Definition 11.3.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1markupTeX✓L∃∀N

There's a compact subset E of D_A with the property that for all x\in D_A^{(1)}, the obvious map xE\to D\backslash D_A is not injective.

Lean code for Lemma11.3.1●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.existsE.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D] :
  ∃ E,
    IsCompact E ∧
      ∀
        (φ :
          TensorProduct K D
              (NumberField.AdeleRing (NumberField.RingOfIntegers K)
                K) ≃ₜ+
            TensorProduct K D
              (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
        MeasureTheory.addEquivAddHaarChar φ = 1 →
          ∃ e₁ ∈ E,
            ∃ e₂ ∈ E,
              e₁ ≠ e₂ ∧
                φ e₁ - φ e₂ ∈
                  Set.range ⇑Algebra.TensorProduct.includeLeft
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.existsE.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  ∃ E,
    IsCompact E ∧
      ∀
        (φ :
          TensorProduct K D
              (NumberField.AdeleRing
                (NumberField.RingOfIntegers
                  K)
                K) ≃ₜ+
            TensorProduct K D
              (NumberField.AdeleRing
                (NumberField.RingOfIntegers
                  K)
                K)),
        MeasureTheory.addEquivAddHaarChar
              φ =
            1 →
          ∃ e₁ ∈ E,
            ∃ e₂ ∈ E,
              e₁ ≠ e₂ ∧
                φ e₁ - φ e₂ ∈
                  Set.range
                    ⇑Algebra.TensorProduct.includeLeft
Proof for Lemma 11.3.1
uses 0

We know that if we pick a \Q-basis for D of size d then this identifies D with \Q^d, D_{\A} with \A_{\Q}^d, and D\backslash D_{\A} with (\Q\backslash\A_{\Q})^d. Now \Q is discrete in \A_{\Q} by theorem Theorem 9.5.3, and the quotient \Q\backslash \A_{\Q} is compact by theorem Theorem 9.5.4. Hence D is discrete in D_{\A} and the quotient D\backslash D_{\A} is compact.

Fix a Haar measure \mu on D_{\A} and push it forward to D\backslash D_{\A}; by compactness this quotient has finite and positive measure, say m\in\R_{>0}. Choose any compact E\subseteq D_{\A} with measure >m (for example, choose a \Z-lattice L\cong\Z^d in D\cong\Q^d, define E_f:=\prod_p L_p\in D\otimes_{\Q}\A_{\Q}^\infty, and define E_{\infty}\subseteq D\otimes_{\Q}\R\cong\R^n to be a huge closed ball, large enough to ensure the measure of E:=E_f\times E_{\infty} is bigger than m). Then \mu(xE)=\mu(E)>m so the map can't be injective.

Definition11.3.2
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 4
Reverse dependency previews
Preview
Definition 11.3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
markupTeX✓L∃∀N

We let E denote any compact set satisfying the hypothesis of the previous lemma.

Lean code for Definition11.3.2●1 definition
  • defdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    def NumberField.AdeleRing.DivisionAlgebra.Aux.E.{u_1, u_2} (K : Type u_1)
  [Field K] [NumberField K] (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
      (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))
    def NumberField.AdeleRing.DivisionAlgebra.Aux.E.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers K) K))
    An auxiliary set E used in the proof of Fujisaki's lemma.
Definition11.3.3
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 5
Reverse dependency previews
Preview
Definition 11.3.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
markupTeX✓L∃∀N

Define X:=E-E:=\{e-f:e,f\in E\}\subseteq D_{\A}.

Lean code for Definition11.3.3●1 definition
  • defdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    def NumberField.AdeleRing.DivisionAlgebra.Aux.X.{u_1, u_2} (K : Type u_1)
  [Field K] [NumberField K] (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
      (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))
    def NumberField.AdeleRing.DivisionAlgebra.Aux.X.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers K) K))
    An auxiliary set X used in the proof of Fukisaki's lemma. Defined as E - E.
Definition11.3.4
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 11.3.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
markupTeX✓L∃∀N

Define Y:=X.X:=\{xy:x,y\in X\}\subseteq D_{\A}.

Lean code for Definition11.3.4●1 definition
  • defdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    def NumberField.AdeleRing.DivisionAlgebra.Aux.Y.{u_1, u_2} (K : Type u_1)
  [Field K] [NumberField K] (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
      (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))
    def NumberField.AdeleRing.DivisionAlgebra.Aux.Y.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers K) K))
    An auxiliary set Y used in the proof of Fukisaki's lemma. Defined as X * X.
Lemma11.3.5
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1markupTeX✓L∃∀N

X is a compact subset of D_{\A}.

Lean code for Lemma11.3.5●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D] :
  IsCompact (NumberField.AdeleRing.DivisionAlgebra.Aux.X K D)
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  IsCompact
    (NumberField.AdeleRing.DivisionAlgebra.Aux.X
      K D)
Proof for Lemma 11.3.5
uses 0

It's the continuous image of the compact set E\times E.

Lemma11.3.6
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1markupTeX✓L∃∀N

Y is a compact subset of D_{\A}.

Lean code for Lemma11.3.6●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D] :
  IsCompact (NumberField.AdeleRing.DivisionAlgebra.Aux.Y K D)
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  IsCompact
    (NumberField.AdeleRing.DivisionAlgebra.Aux.Y
      K D)
Proof for Lemma 11.3.6
uses 0

It's the continuous image of the compact set X\times X.

Lemma11.3.7
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 11.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1markupTeX✓L∃∀N

If \beta\in D_{\A}^{(1)} then \beta X\cap D^\times\not=\emptyset.

Lean code for Lemma11.3.7●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D]
  {β :
    (TensorProduct K D
        (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ}
  (hβ :
    β ∈
      MeasureTheory.ringHaarCharKer
        (TensorProduct K D
          (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))) :
  ∃ x ∈ NumberField.AdeleRing.DivisionAlgebra.Aux.X K D,
    ∃
      d ∈
        Set.range ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl K D),
      ↑β * x = ↑d
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D]
  {β :
    (TensorProduct K D
        (NumberField.AdeleRing
          (NumberField.RingOfIntegers K)
          K))ˣ}
  (hβ :
    β ∈
      MeasureTheory.ringHaarCharKer
        (TensorProduct K D
          (NumberField.AdeleRing
            (NumberField.RingOfIntegers K)
            K))) :
  ∃
    x ∈
      NumberField.AdeleRing.DivisionAlgebra.Aux.X
        K D,
    ∃
      d ∈
        Set.range
          ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl
              K D),
      ↑β * x = ↑d
Proof for Lemma 11.3.7
uses 0

Indeed by the previous lemma Lemma 11.3.1, the map \beta E\to D\backslash D_{\A} is not injective, so there are distinct \beta e_1,\beta e_2\in \beta E with e_i\in E and \beta e_1-\beta e_2=b\in D. Now b\not=0 and D is a division algebra, so b\in D^\times. And e_1-e_2\in X so b=\beta(e_1-e_2)\in \beta X, so we are done.

Lemma11.3.8
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1markupTeX✓L∃∀N

Similarly, if \beta\in D_{\A}^{(1)} then X\beta^{-1}\cap D^\times\not=\emptyset.

Lean code for Lemma11.3.8●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D]
  {β :
    (TensorProduct K D
        (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ}
  (hβ :
    β ∈
      MeasureTheory.ringHaarCharKer
        (TensorProduct K D
          (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))) :
  ∃ x ∈ NumberField.AdeleRing.DivisionAlgebra.Aux.X K D,
    ∃
      d ∈
        Set.range ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl K D),
      x * ↑β⁻¹ = ↑d
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D]
  {β :
    (TensorProduct K D
        (NumberField.AdeleRing
          (NumberField.RingOfIntegers K)
          K))ˣ}
  (hβ :
    β ∈
      MeasureTheory.ringHaarCharKer
        (TensorProduct K D
          (NumberField.AdeleRing
            (NumberField.RingOfIntegers K)
            K))) :
  ∃
    x ∈
      NumberField.AdeleRing.DivisionAlgebra.Aux.X
        K D,
    ∃
      d ∈
        Set.range
          ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl
              K D),
      x * ↑β⁻¹ = ↑d
Proof for Lemma 11.3.8
Proof uses 2
Proof dependency previews
Preview
Theorem 10.9.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Indeed, \beta^{-1}\in D_{\A}^{(1)}, and so left multiplication by \beta^{-1} does not change Haar measure on D_{\A}, so neither does right multiplication (by theorem NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul). So the same argument works: E\beta^{-1}\to D\backslash D_{\A} is not injective so choose e_1\beta^{-1}\not=e_2\beta^{-1} with difference b\in D and then (e_1-e_2)\beta^{-1}\in D-\{0\}=D^\times.

Definition11.3.9
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 11.3.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
markupTeX✓L∃∀N

Let T = Y \cap D^\times.

Lean code for Definition11.3.9●1 definition
  • defdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    def NumberField.AdeleRing.DivisionAlgebra.Aux.T.{u_1, u_2} (K : Type u_1)
  [Field K] [NumberField K] (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
        (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ
    def NumberField.AdeleRing.DivisionAlgebra.Aux.T.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
        (NumberField.AdeleRing
          (NumberField.RingOfIntegers K)
          K))ˣ
    An auxiliary set T used in the proof of Fukisaki's lemma. Defined as Y ∩ Dˣ.
Lemma11.3.10
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1markupTeX✓L∃∀N

T is finite.

Lean code for Lemma11.3.10●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D] :
  (NumberField.AdeleRing.DivisionAlgebra.Aux.T K D).Finite
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  (NumberField.AdeleRing.DivisionAlgebra.Aux.T
      K D).Finite
Proof for Lemma 11.3.10
uses 1

It suffices to prove that Y\cap D is finite. But D\subseteq D_{\A} is a discrete additive subgroup, and hence closed. And Y\subseteq D_{\A} is compact. So D\cap Y is compact and discrete, so finite.

Definition11.3.11
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 11.3.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 11.3.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
markupTeX✓L∃∀N

Define C := (T^{-1}.X)\times X\subset D_{\A}\times D_{\A}.

Lean code for Definition11.3.11●1 definition
  • defdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    def NumberField.AdeleRing.DivisionAlgebra.Aux.C.{u_1, u_2} (K : Type u_1)
  [Field K] [NumberField K] (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
        (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ×
      TensorProduct K D
        (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))
    def NumberField.AdeleRing.DivisionAlgebra.Aux.C.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  Set
    (TensorProduct K D
        (NumberField.AdeleRing
          (NumberField.RingOfIntegers K)
          K) ×
      TensorProduct K D
        (NumberField.AdeleRing
          (NumberField.RingOfIntegers K)
          K))
    An auxiliary set C used in the proof of Fukisaki's lemma. Defined as T⁻¹X × X.
Lemma11.3.12
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Lemma 11.3.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1markupTeX✓L∃∀N

C is compact.

Lean code for Lemma11.3.12●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D] :
  IsCompact (NumberField.AdeleRing.DivisionAlgebra.Aux.C K D)
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D] :
  IsCompact
    (NumberField.AdeleRing.DivisionAlgebra.Aux.C
      K D)
Proof for Lemma 11.3.12
uses 0

X is compact and T is finite.

Lemma11.3.13
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1markupTeX✓L∃∀N

For every \beta \in D_A^{(1)}, there exist b \in D^\times and \nu \in D_A^{(1)} such that \beta = b\nu and (\nu, \nu^{-1}) \in C.

Lean code for Lemma11.3.13●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D]
  {β :
    (TensorProduct K D
        (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ}
  (hβ :
    β ∈
      MeasureTheory.ringHaarCharKer
        (TensorProduct K D
          (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))) :
  ∃ b ∈ Set.range ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl K D),
    ∃
      ν ∈
        MeasureTheory.ringHaarCharKer
          (TensorProduct K D
            (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
      β = b * ν ∧
        (↑ν, ↑ν⁻¹) ∈ NumberField.AdeleRing.DivisionAlgebra.Aux.C K D
    theorem NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D]
  {β :
    (TensorProduct K D
        (NumberField.AdeleRing
          (NumberField.RingOfIntegers K)
          K))ˣ}
  (hβ :
    β ∈
      MeasureTheory.ringHaarCharKer
        (TensorProduct K D
          (NumberField.AdeleRing
            (NumberField.RingOfIntegers K)
            K))) :
  ∃
    b ∈
      Set.range
        ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl
            K D),
    ∃
      ν ∈
        MeasureTheory.ringHaarCharKer
          (TensorProduct K D
            (NumberField.AdeleRing
              (NumberField.RingOfIntegers
                K)
              K)),
      β = b * ν ∧
        (↑ν, ↑ν⁻¹) ∈
          NumberField.AdeleRing.DivisionAlgebra.Aux.C
            K D
Proof for Lemma 11.3.13
Proof uses 4
Proof dependency previews
Preview
Definition 11.3.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

By lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel, \beta X\cap D^\times\not=\emptyset, and lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel', X\beta^{-1}\cap D^\times\not=\emptyset, so we can write \beta x_1=b_1 and x_2\beta^{-1}=b_2 with b_i\in D^\times and x_i\in X. Note that \beta\in D_{\A}^{(1)} and b_i\in D^{\times}\subseteq D_{\A}^{(1)} by corollary Corollary 10.9.6, so x_i\in D_{\A}^{(1)} as well. In particular x_i\in D_{\A}^\times so x_1^{-1} makes sense.

Multiplying the equations defining the x_i and b_i we deduce that x_2x_1=b_2b_1\in Y\cap D^\times=T (recall that Y=X.X and T=Y\cap D^\times is finite); call this element t. Then x_1^{-1}=t^{-1}x_2\in T^{-1}.X, and x_1\in X, so if we set \nu=x_1^{-1}\in D_{\A}^{(1)} and b=b_1\in D^\times then we have \beta=b\nu and (\nu,\nu^{-1})\in C := (T^{-1}.X)\times X. We are done!

Theorem11.3.14
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

If D is a division algebra then the quotient D^\times\backslash D_{\A}^{(1)} with its quotient topology coming from D_{\A}^{(1)} is compact.

Lean code for Theorem11.3.14●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D] :
  CompactSpace
    (Quotient
      (QuotientGroup.rightRel
        (Subgroup.comap
          (MeasureTheory.ringHaarCharKer
              (TensorProduct K D
                (NumberField.AdeleRing (NumberField.RingOfIntegers K)
                  K))).subtype
          (NumberField.AdeleRing.DivisionAlgebra.Aux.incl K D).range)))
    theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D] :
  CompactSpace
    (Quotient
      (QuotientGroup.rightRel
        (Subgroup.comap
          (MeasureTheory.ringHaarCharKer
              (TensorProduct K D
                (NumberField.AdeleRing
                  (NumberField.RingOfIntegers
                    K)
                  K))).subtype
          (NumberField.AdeleRing.DivisionAlgebra.Aux.incl
              K D).range)))
    Dˣ \ D_𝔸^{(1)} is compact.
Proof for Theorem 11.3.14
Proof uses 3
Proof dependency previews
Preview
Corollary 10.3.1.4
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Indeed, if M is the preimage of C under the inclusion D_A^{(1)} \to D_A \times D_A sending \nu to (\nu, \nu^{-1}), then M is a closed subspace of a compact space so it's compact (note that \delta_{D_A} is continuous, by Corollary 10.3.1.4, so D_A^{(1)} is a closed subset of D_A^\times which is itself a closed subset of D_A \times D_A).

Lemma 11.3.13 shows that M surjects onto D^\times \backslash D_A^{(1)} which is thus also compact.

We note here some useful consequences.

Theorem11.3.15
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 11.3.16
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
markupTeX✓L∃∀N

The quotient D^\times \backslash (D \otimes_K \mathbf{A}_K^\infty)^\times is compact.

Lean code for Theorem11.3.15●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D] :
  CompactSpace
    (Quotient
      (QuotientGroup.rightRel
        (NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁ K D).range))
    theorem NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D] :
  CompactSpace
    (Quotient
      (QuotientGroup.rightRel
        (NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁
            K D).range))
    Dˣ \ D_𝔸^fˣ is compact.
Proof for Theorem 11.3.15
uses 1

There's a natural map α from D^\times \backslash D_A^{(1)} to D^\times \backslash (D \otimes_K \mathbf{A}_K^\infty)^\times. We claim that it's surjective. Granted this claim, we are home, because if we put the quotient topology on D^\times \backslash (D \otimes_K \mathbf{A}_K^\infty)^\times coming from (D \otimes_K \mathbf{A}_K^\infty)^\times then it's readily verified that α is continuous, and the continuous image of a compact space is compact.

As for surjectivity: say x \in (D \otimes_K \mathbf{A}_K^\infty)^\times. We need to extend x to an element (x,y) \in (D \otimes_K \mathbf{A}_K^\infty)^\times \times (D \otimes_K K_\infty)^\times which is in the kernel of \delta_{D_A}. Because \delta_{D_A}(x,1) is some positive real number, it will suffice to show that if r is any positive real number then we can find y \in (D \otimes_K \mathbf{A}_K^\infty)^\times = (D \otimes_\mathbf{Q} \mathbf{R})^\times with \delta_{D_A}(1,y)=r, or equivalently, setting D_\mathbf{R} = D \otimes_\mathbf{Q} \mathbf{R}, that \delta_{D_\mathbf{R}}(y)=r. But D \ne 0 as it is a division algebra, and hence \mathbf{Q} \subseteq D, meaning \mathbf{R} \subseteq D_\mathbf{R}, and if x \in \mathbf{R}^\times \subseteq D_\mathbf{R}^\times then \delta(x)=|x|^d with d = \dim_\mathbf{Q}(D), as multiplication by x is just scaling by a factor of x on D_\mathbf{R}\cong\mathbf{R}^d. In particular we can set x=y^{1/d}.

Theorem11.3.16
Group: Fujisaki's lemma and adelic compactness. (15)
Group member previews
Preview
Lemma 11.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1markupTeX✓L∃∀N

If U is an open subgroup of (D \otimes_K \mathbf{A}_K^\infty)^\times, then the double coset space D^\times \backslash (D \otimes_K \mathbf{A}_K^\infty)^\times / U is finite.

Lean code for Theorem11.3.16●1 theorem
  • theoremdefined in FLT/DivisionAlgebra/Finiteness.lean
    complete
    theorem NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset.{u_1, u_2}
  (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D]
  {U : Subgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D)}
  (hU : IsOpen ↑U) :
  Finite
    (DoubleCoset.Quotient
      (Set.range ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁ K D))
      ↑U)
    theorem NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset.{u_1,
    u_2}
  (K : Type u_1) [Field K] [NumberField K]
  (D : Type u_2) [DivisionRing D]
  [Algebra K D] [FiniteDimensional K D]
  [Algebra.IsCentral K D]
  {U :
    Subgroup
      (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx
        K D)}
  (hU : IsOpen ↑U) :
  Finite
    (DoubleCoset.Quotient
      (Set.range
        ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁
            K D))
      ↑U)
Proof for Theorem 11.3.16
uses 0

The double cosets give a disjoint open cover of (D\otimes_K \A_K^\infty) which descends to a disjoint open cover of the quotient space D^\times\backslash(D\otimes_K \A_K^\infty)^\times. However this space is compact by theorem Theorem 11.3.15.