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 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.1

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Definition 11.2

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.E»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

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.

Code for Lemma11.1●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.existsE.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  ∃ ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
    IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`.  ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
      ∀
        (φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) :
          TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
              (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
                KType u_1) ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous. 
            TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
              (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1)),
        MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1 →
          ∃ e₁TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈ ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
            ∃ e₂TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈ ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
              e₁TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. e₂TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) e₁TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) e₂TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
                  Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  ⇑Algebra.TensorProduct.includeLeftAlgebra.TensorProduct.includeLeft.{uR, uS, uA, uB} {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB}
  [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A]
  [SMulCommClass R S A] : A →ₐ[S] TensorProduct R A BThe `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.existsE.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  ∃ ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
    IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`.  ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
      ∀
        (φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) :
          TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
              (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

                (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.

                  KType u_1)
                KType u_1) ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous. 
            TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
              (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

                (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.

                  KType u_1)
                KType u_1)),
        MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`. 
              φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
            1 →
          ∃ e₁TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈ ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
            ∃ e₂TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈ ESet (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)),
              e₁TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. e₂TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) e₁TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). φTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃ₜ+
  TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) e₂TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
                  Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort. 
                    ⇑Algebra.TensorProduct.includeLeftAlgebra.TensorProduct.includeLeft.{uR, uS, uA, uB} {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB}
  [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A]
  [SMulCommClass R S A] : A →ₐ[S] TensorProduct R A BThe `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`.

complete

Proof

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 NumberField.AdeleRing.discrete, and the quotient \Q\backslash \A_{\Q} is compact by theorem Rat.AdeleRing.cocompact. 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.2

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀N

Used by 4

Hover a use site to preview it.

Preview

Definition 11.3

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.X»

Uses target in

statement

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

Code for Definition11.2●1 definition

def NumberField.AdeleRing.DivisionAlgebra.Aux.E.{u_1, u_2} (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
      (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))

def NumberField.AdeleRing.DivisionAlgebra.Aux.E.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
      (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

        (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))

An auxiliary set E used in the proof of Fujisaki's lemma.

complete

Definition11.3

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀N

Used by 5

Hover a use site to preview it.

Preview

Definition 11.4

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.Y»

Uses target in

statement

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

Code for Definition11.3●1 definition

def NumberField.AdeleRing.DivisionAlgebra.Aux.X.{u_1, u_2} (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
      (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))

def NumberField.AdeleRing.DivisionAlgebra.Aux.X.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
      (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

        (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))

An auxiliary set X used in the proof of Fukisaki's lemma. Defined as E - E.

complete

Definition11.4

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Lemma 11.6

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact»

Uses target in

statement

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

Code for Definition11.4●1 definition

def NumberField.AdeleRing.DivisionAlgebra.Aux.Y.{u_1, u_2} (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
      (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))

def NumberField.AdeleRing.DivisionAlgebra.Aux.Y.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
      (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

        (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))

An auxiliary set Y used in the proof of Fukisaki's lemma. Defined as X * X.

complete

Lemma11.5

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

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

Code for Lemma11.5●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`.  (NumberField.AdeleRing.DivisionAlgebra.Aux.XNumberField.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.  KType u_1 DType u_2)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. 
    (NumberField.AdeleRing.DivisionAlgebra.Aux.XNumberField.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. 
      KType u_1 DType u_2)

complete

Proof

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

Lemma11.6

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

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

Code for Lemma11.6●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`.  (NumberField.AdeleRing.DivisionAlgebra.Aux.YNumberField.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.  KType u_1 DType u_2)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. 
    (NumberField.AdeleRing.DivisionAlgebra.Aux.YNumberField.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. 
      KType u_1 DType u_2)

complete

Proof

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

Lemma11.7

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

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

Code for Lemma11.7●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  {β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ :
    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. }
  (hββ ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) :
    β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
      MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

        (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
          (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))) :
  ∃ xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈ NumberField.AdeleRing.DivisionAlgebra.Aux.XNumberField.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.  KType u_1 DType u_2,
    ∃
      d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
        Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism.  KType u_1 DType u_2),
      ↑β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ↑d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  {β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ :
    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

          (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
          KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. }
  (hββ ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) :
    β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
      MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

        (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
          (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

            (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
            KType u_1))) :
  ∃
    xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈
      NumberField.AdeleRing.DivisionAlgebra.Aux.XNumberField.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. 
        KType u_1 DType u_2,
    ∃
      d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
        Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort. 
          ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism. 
              KType u_1 DType u_2),
      ↑β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ↑d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ

complete

Proof

Indeed by the previous lemma, 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.8

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

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

Code for Lemma11.8●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2]
  {β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ :
    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. }
  (hββ ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) :
    β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
      MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

        (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
          (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))) :
  ∃ xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈ NumberField.AdeleRing.DivisionAlgebra.Aux.XNumberField.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.  KType u_1 DType u_2,
    ∃
      d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
        Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism.  KType u_1 DType u_2),
      xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ↑β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ↑d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2]
  {β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ :
    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

          (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
          KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. }
  (hββ ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) :
    β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
      MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

        (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
          (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

            (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
            KType u_1))) :
  ∃
    xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ∈
      NumberField.AdeleRing.DivisionAlgebra.Aux.XNumberField.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. 
        KType u_1 DType u_2,
    ∃
      d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
        Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort. 
          ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism. 
              KType u_1 DType u_2),
      xTensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ↑β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ↑d(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ

complete

Proof

Definition 11.2 Theorem 10.31 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.9

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Lemma 11.10

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite»

Uses target in

statement

Definition 11.4 Let T = Y \cap D^\times.

Code for Definition11.9●1 definition

def NumberField.AdeleRing.DivisionAlgebra.Aux.T.{u_1, u_2} (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`.

def NumberField.AdeleRing.DivisionAlgebra.Aux.T.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

          (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
          KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`.

An auxiliary set T used in the proof of Fukisaki's lemma. Defined as Y ∩ Dˣ.

complete

Lemma11.10

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

Definition 11.9 The set T is finite.

Code for Lemma11.10●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  (NumberField.AdeleRing.DivisionAlgebra.Aux.TNumberField.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ˣ.  KType u_1 DType u_2).FiniteSet.Finite.{u} {α : Type u} (s : Set α) : PropA set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  (NumberField.AdeleRing.DivisionAlgebra.Aux.TNumberField.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ˣ. 
      KType u_1 DType u_2).FiniteSet.Finite.{u} {α : Type u} (s : Set α) : PropA set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`.

complete

Proof

Lemma 11.6 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.11

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Lemma 11.12

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact»

Uses target in

statement

Definition 11.9 Definition 11.3 Define the compact constraint set C = (T^{-1} X) \times X \subseteq D_A \times D_A.

Code for Definition11.11●1 definition

def NumberField.AdeleRing.DivisionAlgebra.Aux.C.{u_1, u_2} (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1) ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
      TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.

def NumberField.AdeleRing.DivisionAlgebra.Aux.C.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.

    (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

          (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
          KType u_1) ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
      TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

          (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
          KType u_1))Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.

An auxiliary set C used in the proof of Fukisaki's lemma. Defined as T⁻¹X × X.

complete

Lemma11.12

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

Definition 11.11 The set C is compact. Lemma 11.10 Lemma 11.5

Code for Lemma11.12●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`.  (NumberField.AdeleRing.DivisionAlgebra.Aux.CNumberField.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.  KType u_1 DType u_2)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2] :
  IsCompactIsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : PropA set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. 
    (NumberField.AdeleRing.DivisionAlgebra.Aux.CNumberField.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. 
      KType u_1 DType u_2)

complete

Proof

X is compact and T is finite.

Lemma11.13

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

Definition 11.11 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.

Code for Lemma11.13●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2]
  {β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ :
    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. }
  (hββ ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) :
    β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
      MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

        (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
          (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1))) :
  ∃ b(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈ Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism.  KType u_1 DType u_2),
    ∃
      ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
        MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

          (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
            (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1) KType u_1)),
      β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. b(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
        (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.↑ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ,Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ↑ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. NumberField.AdeleRing.DivisionAlgebra.Aux.CNumberField.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.  KType u_1 DType u_2

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2]
  {β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ :
    (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
        (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

          (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
          KType u_1))ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. }
  (hββ ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) :
    β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
      MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

        (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
          (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

            (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
            KType u_1))) :
  ∃
    b(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
      Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort. 
        ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism. 
            KType u_1 DType u_2),
    ∃
      ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∈
        MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

          (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
            (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

              (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.

                KType u_1)
              KType u_1)),
      β(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. b(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
        (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.↑ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ,Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ↑ν(TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣ⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
          NumberField.AdeleRing.DivisionAlgebra.Aux.CNumberField.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. 
            KType u_1 DType u_2

complete

Proof

Definition 11.11 Definition 11.2 Lemma 11.7 Lemma 11.8

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 NumberField.AdeleRing.units_mem_ringHaarCharacter_ker, 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.14

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

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.

Code for Theorem11.14●1 theorem

theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2] :
  CompactSpaceCompactSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : PropType class for compact spaces. Separation is sometimes included in the definition, especially
in the French literature, but we do not include it here. 
    (QuotientQuotient.{u} {α : Sort u} (s : Setoid α) : Sort uQuotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.

Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.

The key quotient operators are:
 * `Quotient.mk` places elements of the underlying type `α` into the quotient.
 * `Quotient.lift` allows the definition of functions from the quotient to some other type.
 * `Quotient.sound` asserts the equality of elements related by `r`
 * `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
   constructed with `Quotient.mk`.

`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.

      (QuotientGroup.rightRelQuotientGroup.rightRel.{u_1} {α : Type u_1} [Group α] (s : Subgroup α) : Setoid αThe equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. 
        (Subgroup.comapSubgroup.comap.{u_1, u_7} {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup GThe preimage of a subgroup along a monoid homomorphism is a subgroup. 
          (MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

              (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
                (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 KType u_1)
                  KType u_1))).subtypeSubgroup.subtype.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : ↥H →* GThe natural group hom from a subgroup of group `G` to `G`. 
          (NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism.  KType u_1 DType u_2).rangeMonoidHom.range.{u_1, u_5} {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup NThe range of a monoid homomorphism from a group is a subgroup. )))

theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2] :
  CompactSpaceCompactSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : PropType class for compact spaces. Separation is sometimes included in the definition, especially
in the French literature, but we do not include it here. 
    (QuotientQuotient.{u} {α : Sort u} (s : Setoid α) : Sort uQuotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.

Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.

The key quotient operators are:
 * `Quotient.mk` places elements of the underlying type `α` into the quotient.
 * `Quotient.lift` allows the definition of functions from the quotient to some other type.
 * `Quotient.sound` asserts the equality of elements related by `r`
 * `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
   constructed with `Quotient.mk`.

`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.

      (QuotientGroup.rightRelQuotientGroup.rightRel.{u_1} {α : Type u_1} [Group α] (s : Subgroup α) : Setoid αThe equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. 
        (Subgroup.comapSubgroup.comap.{u_1, u_7} {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup GThe preimage of a subgroup along a monoid homomorphism is a subgroup. 
          (MeasureTheory.ringHaarChar_kerMeasureTheory.ringHaarChar_ker.{u_1} (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup RˣThe kernel of the `ringHaarChar : Rˣ → ℝ≥0`, namely the units
of a locally compact topological ring such that left multiplication
by them does not change additive Haar measure.

              (TensorProductTensorProduct.{u_1, u_7, u_8} (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M]
  [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  KType u_1 DType u_2
                (NumberField.AdeleRingNumberField.AdeleRing.{u_1, u_2} (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] : Type (max u_2 u_2 u_1)`AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.

                  (NumberField.RingOfIntegersNumberField.RingOfIntegers.{u_1} (K : Type u_1) [Field K] : Type u_1The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.

                    KType u_1)
                  KType u_1))).subtypeSubgroup.subtype.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : ↥H →* GThe natural group hom from a subgroup of group `G` to `G`. 
          (NumberField.AdeleRing.DivisionAlgebra.Aux.inclNumberField.AdeleRing.DivisionAlgebra.Aux.incl.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))ˣThe inclusion Dˣ → D_𝔸ˣ as a group homomorphism. 
              KType u_1 DType u_2).rangeMonoidHom.range.{u_1, u_5} {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup NThe range of a monoid homomorphism from a group is a subgroup. )))

Dˣ \ D_𝔸^{(1)} is compact.

complete

Proof

Lemma 11.12 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.15, 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.13 shows that M surjects onto D^\times \backslash D_A^{(1)} which is thus also compact.

We note here some useful consequences.

Theorem11.16

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Theorem 11.17

Blueprint label

«NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset»

Uses target in

statement

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

Code for Theorem11.16●1 theorem

theorem NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2] :
  CompactSpaceCompactSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : PropType class for compact spaces. Separation is sometimes included in the definition, especially
in the French literature, but we do not include it here. 
    (QuotientQuotient.{u} {α : Sort u} (s : Setoid α) : Sort uQuotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.

Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.

The key quotient operators are:
 * `Quotient.mk` places elements of the underlying type `α` into the quotient.
 * `Quotient.lift` allows the definition of functions from the quotient to some other type.
 * `Quotient.sound` asserts the equality of elements related by `r`
 * `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
   constructed with `Quotient.mk`.

`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.

      (QuotientGroup.rightRelQuotientGroup.rightRel.{u_1} {α : Type u_1} [Group α] (s : Subgroup α) : Setoid αThe equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. 
        (NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K DThe inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism.  KType u_1 DType u_2).rangeMonoidHom.range.{u_1, u_5} {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup NThe range of a monoid homomorphism from a group is a subgroup. ))

theorem NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2] :
  CompactSpaceCompactSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : PropType class for compact spaces. Separation is sometimes included in the definition, especially
in the French literature, but we do not include it here. 
    (QuotientQuotient.{u} {α : Sort u} (s : Setoid α) : Sort uQuotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.

Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.

The key quotient operators are:
 * `Quotient.mk` places elements of the underlying type `α` into the quotient.
 * `Quotient.lift` allows the definition of functions from the quotient to some other type.
 * `Quotient.sound` asserts the equality of elements related by `r`
 * `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
   constructed with `Quotient.mk`.

`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.

      (QuotientGroup.rightRelQuotientGroup.rightRel.{u_1} {α : Type u_1} [Group α] (s : Subgroup α) : Setoid αThe equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. 
        (NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K DThe inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism. 
            KType u_1 DType u_2).rangeMonoidHom.range.{u_1, u_5} {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup NThe range of a monoid homomorphism from a group is a subgroup. ))

Dˣ \ D_𝔸^fˣ is compact.

complete

Proof

Theorem 11.14 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.17

Group: Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (15)

Hover another entry in this group to preview it.

Preview

Lemma 11.1

Blueprint label

«NumberField.AdeleRing.DivisionAlgebra.Aux.existsE»

Group

Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.

✓L∃∀Nused by 1

Theorem 11.16 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.

Code for Theorem11.17●1 theorem

theorem NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset.{u_1, u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2]
  {USubgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D) : SubgroupSubgroup.{u_3} (G : Type u_3) [Group G] : Type u_3A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.  (NumberField.AdeleRing.DivisionAlgebra.Aux.DfxNumberField.AdeleRing.DivisionAlgebra.Aux.Dfx.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Type (max u_2 u_1)Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ.  KType u_1 DType u_2)}
  (hUIsOpen ↑U : IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  ↑USubgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D)) :
  FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.

    (DoubleCoset.QuotientDoubleCoset.Quotient.{u_1} {G : Type u_1} [Group G] (H K : Set G) : Type u_1Quotient of `G` by the double coset relation, i.e. `H \ G / K` 
      (Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K DThe inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism.  KType u_1 DType u_2))
      ↑USubgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D))

theorem NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset.{u_1,
    u_2}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_1] [NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  KType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [DivisionRingDivisionRing.{u_2} (K : Type u_2) : Type u_2A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  DType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_1 DType u_2] [FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  KType u_1 DType u_2]
  [Algebra.IsCentralAlgebra.IsCentral.{u, v} (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : PropFor a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 KType u_1 DType u_2]
  {USubgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D) :
    SubgroupSubgroup.{u_3} (G : Type u_3) [Group G] : Type u_3A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse. 
      (NumberField.AdeleRing.DivisionAlgebra.Aux.DfxNumberField.AdeleRing.DivisionAlgebra.Aux.Dfx.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Type (max u_2 u_1)Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ. 
        KType u_1 DType u_2)}
  (hUIsOpen ↑U : IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  ↑USubgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D)) :
  FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.

    (DoubleCoset.QuotientDoubleCoset.Quotient.{u_1} {G : Type u_1} [Group G] (H K : Set G) : Type u_1Quotient of `G` by the double coset relation, i.e. `H \ G / K` 
      (Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort. 
        ⇑(NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁.{u_1, u_2} (K : Type u_1) [Field K] [NumberField K] (D : Type u_2)
  [DivisionRing D] [Algebra K D] : Dˣ →* NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K DThe inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism. 
            KType u_1 DType u_2))
      ↑USubgroup (NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx K D))

complete

Proof

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 NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.