Fermat's Last Theorem Blueprint

12. Miniproject: Quaternion algebras🔗

12.1. The goal🔗

At the time of writing, mathlib still does not have a proof that the space of classical modular forms of a fixed weight, level and character is finite-dimensional. The main result in this miniproject is to prove that certain spaces of quaternionic modular forms are finite-dimensional. We need finiteness results like this in order to control the Hecke algebras which act on these spaces; these Hecke algebras are the Ts which are isomorphic to the Rs in the R = T theorem which is the big first target for the FLT project.

12.2. Initial definitions🔗

Our first goal in this miniproject is the definition of these spaces of quaternionic modular forms. We start with some preliminary work towards this.

Let K be a field. Recall that a quaternion algebra over K is a central simple K-algebra of K-dimension 4.

A fundamental fact about central simple algebras is that if D/K is a central simple K-algebra and L/K is an extension of fields, then D \otimes_K L is a central simple L-algebra. In particular, if D is a quaternion algebra over K then D \otimes_K L is a quaternion algebra over L. Some Imperial undergraduate students have established this fact in ongoing project work.

A totally real field is a number field F such that the image of every ring homomorphism F \to \bbC is a subset of \R. We fix once and for all a totally real field F and a quaternion algebra D over F. We furthermore assume that D is totally definite, that is, that for all field embeddings \tau : F \to \R we have D \otimes_{F,\tau} \R \cong \bbH. Because F has at least one real place, the totally definite hypothesis is enough to show that D is not a matrix algebra and thus must be a division algebra. Thus Fujisaki's theorem from the Fujisaki miniproject applies, and we know that D^\times\backslash (D\otimes_F\A_F)^{(1)} is compact.

The high-falutin' explanation of what is about to happen is that the units D^\times of D can be regarded as a connected reductive algebraic group over F, and we are going to define certain spaces of automorphic forms for this algebraic group. For a general connected reductive algebraic group, part of the definition of an automorphic form is that it is satisfies some differential equations (for example modular forms are automorphic forms for the algebraic group GL_2 over Q, and the definition of a modular form involves holomorphic functions, which are solutions to the Cauchy-Riemann equations). However under the assumption that F is totally real and D/F is totally definite, the "associated symmetric space is a 0-dimensional manifold", meaning in practice that the part of the definition of an automorphic form involving differential equations is vacuously satisfied in this setting.

As a consequence, the definitions we are about to give have a far more algebraic flavour. Crucially, the fact that we do not need to talk about differential equations at all means that one does not need to assume that our automorphic forms are ℂ-valued; our definition makes sense for forms valued in an arbitrary additive commutative group. In particular, it is possible to talk about mod p^n and p-adic automorphic forms in this setting without doing any complicated algebraic geometry.

12.3. Brief introduction to automorphic forms in this setting🔗

Having made assumptions on D which make the theory of automorphic forms over D^\times far less technical, we will now make it a little more technical by using the modern adelic approach to the theory. Note that many results about the adeles of a number field are proved in the adele miniproject. Our automorphic forms will be certain functions on the units of the ring D_{\A^\infty} := D \otimes_F \A_F^\infty \cong D \otimes_{\Q} \A_{\Q}^\infty.

To prove Fermat's Last Theorem it suffices to work in weight 2 and trivial character, and for simplicity we shall, at least for now, bake these assumptions into our definitions, even though they would be easy to remove. We remark again that there is no analogue of the holomorphicity condition that one sees in the classical theory, because the symmetric space is a finite set of points rather than the upper half plane. Also there is no analogue of the cuspidality condition because there are no cusps in this setting. Other than the number field F and the quaternion algebra D, the other variable we will see in our situation will be the level of the forms. The main result in this miniproject will be that the space of weight 2 automorphic forms of level U is finite-dimensional.

12.4. Definition of spaces of automorphic forms🔗

Let us now give some precise definitions. Recall that by \A_F^\infty we mean the finite adeles of the totally real number field F.

A level is a compact open subgroup U of (D \otimes_F \A_F^\infty)^\times. These are plentiful. The ring D_f := D \otimes_F \A_F^\infty is a topological ring, and hence the units D_f^\times of this ring are a topological group. This group is locally profinite, and hence has many compact open subgroups; we will see explicit examples later on.

We regard \A_F^\infty as a subring of D_{\A^\infty} := D \otimes_F \A_F^\infty, which is possible because F is a subring of D. More precisely, we embed \A_F^\infty into D \otimes_F \A_F^\infty via the map sending g to 1 \otimes g. Because F is in the centre of D, we have that \A_F^\infty is in the centre of D_{\A^\infty}. As a consequence we can identify (\A_F^\infty)^\times as a subgroup of (D \otimes_F \A_F^\infty)^\times. We may also regard D as a subring of D \otimes_F \A_F^\infty via the map d \mapsto d \otimes 1, and hence we can think of D^\times as a subgroup of (D \otimes_F \A_F^\infty)^\times.

Let R be an additive commutative group. Later on R will be a commutative ring but we will not need this for the definition.

Let us now give some precise definitions. Recall that by \A_F^\infty we mean the finite adeles of the totally real number field F.

A level is a compact open subgroup U of (D\otimes_F\A_F^\infty)^\times. These are plentiful. The ring D_f:=D\otimes_F\A_F^\infty is a topological ring, and hence the units D_f^\times of this ring are a topological group. This group is locally profinite, and hence has many compact open subgroups; we will see explicit examples later on.

We regard \A_F^\infty as a subring of D_{\A^\infty}:=D\otimes_F\A_F^\infty, which is possible because F is a subring of D. More precisely, we embed \A_F^\infty into D\otimes_F\A_F^\infty via the map sending g to 1\otimes g. Because F is in the centre of D, we have that \A_F^\infty is in the centre of D_{\A^\infty}. As a consequence we can identify (\A_F^\infty)^\times as a subgroup of (D\otimes_F\A_F^\infty)^\times. We may also regard D as a subring of D\otimes_F\A_F^\infty via the map d\mapsto d\otimes 1, and hence we can think of D^\times as a subgroup of (D\otimes_F\A_F^\infty)^\times.

Let R be an additive commutative group. Later on R will be a commutative ring but we will not need this for the definition.

Definition12.1
Group: Miniproject: Quaternion algebras. (5)
Hover another entry in this group to preview it.
Preview
Definition 12.2
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup»
Group
  • Miniproject: Quaternion algebras.
✓L∃∀N
Used by 4
Hover a use site to preview it.
Preview
Definition 12.2
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup»
Uses target in
  • statement

The space of R-valued automorphic forms for D^\times is the set of functions f:D_{\A^\infty}^\times\to R satisfying the following axioms:

  • f(dg)=f(g) for all d\in D^\times and g\in D_{\A^\infty}^\times.

  • f(gz)=f(g) for all g\in D_{\A^\infty}^\times.

  • There exists a compact open subgroup U\subseteq (D_{\A^f}^\times) such that f(gu)=f(g) for all g\in D_{\A^\infty}^\times and u\in U.

Code for Definition12.1●1 definition
  • structure TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2,
    u_3}
  (FType 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`.  FType 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 ℚ.  FType u_1] (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] (RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  RType u_3] : Type (max (max u_1 u_2) u_3)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    structure TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1,
    u_2, u_3}
  (FType 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`.  FType 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 ℚ.  FType u_1]
  (DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] (RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  RType u_3] :
  Type (max (max u_1 u_2) u_3)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.

    Constructor

    TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1] {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  RType u_3]
  (toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R :
    TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
        FType u_1 DType u_2 →
      RType u_3)
  (left_invt∀ (δ : Dˣ) (g : TotallyDefiniteQuaternionAlgebra.Dfx F D),
  toFun ((TotallyDefiniteQuaternionAlgebra.incl₁ F D) δ * g) = toFun g :
    ∀ (δDˣ : DType u_2ˣ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`. )
      (gTotallyDefiniteQuaternionAlgebra.Dfx F D :
        TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
          FType u_1 DType u_2),
      toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R
          (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`.(TotallyDefiniteQuaternionAlgebra.incl₁TotallyDefiniteQuaternionAlgebra.incl₁.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Dˣ →* TotallyDefiniteQuaternionAlgebra.Dfx F Dincl₁ is an abbreviation for the inclusion
$D^\times\to(D\otimes_F\mathbb{A}_F^\infty)^\times.$ Remark: I wrote the `incl₁`
docstring in LaTeX and the `incl₂` one in unicode. Which is better? 
                FType u_1 DType u_2)
              δDˣ *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`.
            gTotallyDefiniteQuaternionAlgebra.Dfx F D)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`. =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`.
        toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R gTotallyDefiniteQuaternionAlgebra.Dfx F D)
  (right_invt∃ U, IsOpen ↑U ∧ ∀ (g u : TotallyDefiniteQuaternionAlgebra.Dfx F D), u ∈ U → toFun (g * u) = toFun g :
    ∃ USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D),
      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 (TotallyDefiniteQuaternionAlgebra.Dfx F D) ∧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 `/\`).
        ∀
          (gTotallyDefiniteQuaternionAlgebra.Dfx F D uTotallyDefiniteQuaternionAlgebra.Dfx F D :
            TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
              FType u_1 DType u_2),
          uTotallyDefiniteQuaternionAlgebra.Dfx F D ∈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`. USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D) →
            toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R (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`.gTotallyDefiniteQuaternionAlgebra.Dfx F D *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`. uTotallyDefiniteQuaternionAlgebra.Dfx F D)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`. =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`. toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R gTotallyDefiniteQuaternionAlgebra.Dfx F D)
  (trivial_central_char∀ (z : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ)
  (g : TotallyDefiniteQuaternionAlgebra.Dfx F D), toFun (g * (TotallyDefiniteQuaternionAlgebra.incl₂ F D) z) = toFun g :
    ∀
      (z(IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ :
        (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.

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

              FType u_1)
            FType 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`. )
      (gTotallyDefiniteQuaternionAlgebra.Dfx F D :
        TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
          FType u_1 DType u_2),
      toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R
          (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`.gTotallyDefiniteQuaternionAlgebra.Dfx F D *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`.
            (TotallyDefiniteQuaternionAlgebra.incl₂TotallyDefiniteQuaternionAlgebra.incl₂.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] :
  (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* TotallyDefiniteQuaternionAlgebra.Dfx F D`incl₂` is he inclusion `𝔸_F^∞ˣ → (D ⊗ 𝔸_F^∞ˣ)`. Remark: I wrote the `incl₁`
docstring in LaTeX and the `incl₂` one in unicode. Which is better? 
                FType u_1 DType u_2)
              z(IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ)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`. =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`.
        toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → R gTotallyDefiniteQuaternionAlgebra.Dfx F D) :
  TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.

    FType u_1 DType u_2 RType u_3

    Fields

    toFunTotallyDefiniteQuaternionAlgebra.Dfx F D → RThe function underlying an automorphic form.  : TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType u_1 DType u_2 → RType u_3
    The function underlying an automorphic form. 
    left_invt∀ (δ : Dˣ) (g : TotallyDefiniteQuaternionAlgebra.Dfx F D),
  ↑self ((TotallyDefiniteQuaternionAlgebra.incl₁ F D) δ * g) = ↑self g : ∀ (δDˣ : DType u_2ˣ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`. ) (gTotallyDefiniteQuaternionAlgebra.Dfx F D : TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType u_1 DType u_2),
  ↑selfTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm F D R (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`.(TotallyDefiniteQuaternionAlgebra.incl₁TotallyDefiniteQuaternionAlgebra.incl₁.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Dˣ →* TotallyDefiniteQuaternionAlgebra.Dfx F Dincl₁ is an abbreviation for the inclusion
$D^\times\to(D\otimes_F\mathbb{A}_F^\infty)^\times.$ Remark: I wrote the `incl₁`
docstring in LaTeX and the `incl₂` one in unicode. Which is better?  FType u_1 DType u_2) δDˣ *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`. gTotallyDefiniteQuaternionAlgebra.Dfx F D)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`. =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`. ↑selfTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm F D R gTotallyDefiniteQuaternionAlgebra.Dfx F D
    right_invt∃ U, IsOpen ↑U ∧ ∀ (g u : TotallyDefiniteQuaternionAlgebra.Dfx F D), u ∈ U → ↑self (g * u) = ↑self g : ∃ USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D), 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 (TotallyDefiniteQuaternionAlgebra.Dfx F D) ∧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 `/\`). ∀ (gTotallyDefiniteQuaternionAlgebra.Dfx F D uTotallyDefiniteQuaternionAlgebra.Dfx F D : TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType u_1 DType u_2), uTotallyDefiniteQuaternionAlgebra.Dfx F D ∈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`. USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D) → ↑selfTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm F D R (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`.gTotallyDefiniteQuaternionAlgebra.Dfx F D *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`. uTotallyDefiniteQuaternionAlgebra.Dfx F D)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`. =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`. ↑selfTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm F D R gTotallyDefiniteQuaternionAlgebra.Dfx F D
    trivial_central_char∀ (z : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ)
  (g : TotallyDefiniteQuaternionAlgebra.Dfx F D), ↑self (g * (TotallyDefiniteQuaternionAlgebra.incl₂ F D) z) = ↑self g : ∀ (z(IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ : (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.
 (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.
 FType u_1) FType 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`. )
  (gTotallyDefiniteQuaternionAlgebra.Dfx F D : TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType u_1 DType u_2), ↑selfTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm F D R (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`.gTotallyDefiniteQuaternionAlgebra.Dfx F D *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`. (TotallyDefiniteQuaternionAlgebra.incl₂TotallyDefiniteQuaternionAlgebra.incl₂.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] :
  (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* TotallyDefiniteQuaternionAlgebra.Dfx F D`incl₂` is he inclusion `𝔸_F^∞ˣ → (D ⊗ 𝔸_F^∞ˣ)`. Remark: I wrote the `incl₁`
docstring in LaTeX and the `incl₂` one in unicode. Which is better?  FType u_1 DType u_2) z(IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ)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`. =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`. ↑selfTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm F D R gTotallyDefiniteQuaternionAlgebra.Dfx F D
    complete

Let S^D(R) denote the set of automorphic forms for D^\times. The space S^D(R) is sometimes referred to as a space of "quaternionic modular forms" over R. Three basic observations about S^D(R) are as follows.

Definition12.2
Group: Miniproject: Quaternion algebras. (5)
Hover another entry in this group to preview it.
Preview
Definition 12.1
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm»
Group
  • Miniproject: Quaternion algebras.
✓L∃∀N
Used by 3
Hover a use site to preview it.
Preview
Definition 12.3
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.module»
Uses target in
  • statement

Pointwise addition (f_1 + f_2)(g) := f_1(g) + f_2(g) makes S^D(R) into an additive abelian group. This depends on Definition 12.1.

Code for Definition12.2●1 definition
  • def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1] {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  RType u_3] :
  AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`. 
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.
 FType u_1 DType u_2 RType u_3)
    def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1]
  {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  RType u_3] :
  AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`. 
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.

      FType u_1 DType u_2 RType u_3)
    complete
Definition12.3
Group: Miniproject: Quaternion algebras. (5)
Hover another entry in this group to preview it.
Preview
Definition 12.1
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm»
Group
  • Miniproject: Quaternion algebras.
✓L∃∀N
Used by 3
Hover a use site to preview it.
Preview
Definition 12.4
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.distribMulAction»
Uses target in
  • statement

If R is a commutative ring then pointwise scalar multiplication (r \cdot f)(g) := r \cdot f(g) makes S^D(R) into an R-module. This depends on Definition 12.1 and Definition 12.2.

Code for Definition12.3●1 definition
  • def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.module.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1] {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_3] :
  ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u_3
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.
 FType u_1 DType u_2 RType u_3)
    def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.module.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1]
  {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_3] :
  ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u_3
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.

      FType u_1 DType u_2 RType u_3)
    complete
Definition12.4
Group: Miniproject: Quaternion algebras. (5)
Hover another entry in this group to preview it.
Preview
Definition 12.1
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm»
Group
  • Miniproject: Quaternion algebras.
✓L∃∀Nused by 1

The group D_{\A^\infty}^\times acts on the additive abelian group S^D(R) by (g \cdot f)(x) = f(xg). This depends on Definition 12.1, Definition 12.2, and Definition 12.3.

Code for Definition12.4●1 definition
  • def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.distribMulAction.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1] {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  RType u_3] :
  DistribMulActionDistribMulAction.{u_12, u_13} (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] : Type (max u_12 u_13)Typeclass for multiplicative actions on additive structures.

For example, if `G` is a group (with group law written as multiplication) and `A` is an
abelian group (with group law written as addition), then to give `A` a `G`-module
structure (for example, to use the theory of group cohomology) is to say `[DistribMulAction G A]`.
Note in that we do not use the `Module` typeclass for `G`-modules, as the `Module` typeclass
is for modules over a ring rather than a group.

Mathematically, `DistribMulAction G A` is equivalent to giving `A` the structure of
a `ℤ[G]`-module.
 (TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType u_1 DType u_2)
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.
 FType u_1 DType u_2 RType u_3)
    def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.distribMulAction.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1]
  {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2] {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  RType u_3] :
  DistribMulActionDistribMulAction.{u_12, u_13} (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] : Type (max u_12 u_13)Typeclass for multiplicative actions on additive structures.

For example, if `G` is a group (with group law written as multiplication) and `A` is an
abelian group (with group law written as addition), then to give `A` a `G`-module
structure (for example, to use the theory of group cohomology) is to say `[DistribMulAction G A]`.
Note in that we do not use the `Module` typeclass for `G`-modules, as the `Module` typeclass
is for modules over a ring rather than a group.

Mathematically, `DistribMulAction G A` is equivalent to giving `A` the structure of
a `ℤ[G]`-module.

    (TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
      FType u_1 DType u_2)
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.{u_1, u_2, u_3} (F : Type u_1) [Field F] [NumberField F]
  (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] (R : Type u_3) [AddCommMonoid R] :
  Type (max (max u_1 u_2) u_3)This definition is made in mathlib-generality but is *not* the definition of a
weight 2 automorphic form unless `Dˣ` is compact mod centre at infinity.
This hypothesis will be true if `D` is a totally definite quaternion algebra
over a totally real field.

      FType u_1 DType u_2 RType u_3)
    complete

If R is a commutative ring then the action of D_{\A^\infty}^\times commutes with the R-action.

Now let U be a level, that is, a compact open subgroup of D_{\A^\infty}^\times.

Definition12.5
Group: Miniproject: Quaternion algebras. (5)
Hover another entry in this group to preview it.
Preview
Definition 12.1
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm»
Group
  • Miniproject: Quaternion algebras.
✓L∃∀Nused by 0

The quaternionic modular forms of level U, with notation S^D(U;R), are the U-invariants for the D_{\A^\infty}^\times-action on S^D(R). This depends on Definition 12.1, Definition 12.2, Definition 12.4, and Definition 12.3.

Code for Definition12.5●1 definition
  • def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1] {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2]
  (USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F 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.  (TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType u_1 DType u_2))
  (RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_3] : Type (max (max u_3 u_2) u_1)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType u_1]
  {DType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  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.
 FType 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.  FType u_1 DType u_2]
  (USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F 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. 
      (TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
        FType u_1 DType u_2))
  (RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_3] :
  Type (max (max u_3 u_2) u_1)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    `WeightTwoAutomorphicFormOfLevel U R` is the `R`-valued weight 2 automorphic forms of a fixed
level `U` for a totally definite quaternion algebra over a totally real field.
    complete

The Hecke algebras involved in the main modularity lifting theorems needed in the FLT project will be endomorphisms of these spaces S^D(U;R).

12.5. The main result🔗

The point of this miniproject is the finite-dimensionality result below. This is an analogue of the result that classical modular forms of a fixed level, weight and character are finite-dimensional. In fact, by delicate results of Jacquet and Langlands this result, in the case k = \bbC, implies many cases of that classical claim, although of course the Jacquet--Langlands theorem is much harder to prove than the classical proof of finite-dimensionality.

Theorem12.6
Group: Miniproject: Quaternion algebras. (5)
Hover another entry in this group to preview it.
Preview
Definition 12.1
Blueprint label
  • «TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm»
Group
  • Miniproject: Quaternion algebras.
✓L∃∀Nused by 0

Let k be a field. Then the space S^D(U;k) is a finite-dimensional k-vector space. This depends on Definition 12.3.

Code for Theorem12.6●1 theorem
  • theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType 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.
 FType u_1 DType u_2] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  FType 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`.
 FType u_1 DType u_2] (KType u_3 : Type u_3A 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_3]
  {USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F 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.  (TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$  FType 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 (TotallyDefiniteQuaternionAlgebra.Dfx F D)) :
  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_3
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevelTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.{u_1, u_2, u_3} {F : Type u_1} [Field F]
  [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D]
  (U : Subgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D)) (R : Type u_3) [CommRing R] : Type (max (max u_3 u_2) u_1)`WeightTwoAutomorphicFormOfLevel U R` is the `R`-valued weight 2 automorphic forms of a fixed
level `U` for a totally definite quaternion algebra over a totally real field.
 USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D)
      KType u_3)
    theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional.{u_1,
    u_2, u_3}
  {FType 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`.  FType 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 ℚ.  FType 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.
 FType u_1 DType u_2] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  FType 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`.
 FType u_1 DType u_2] (KType u_3 : Type u_3A 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_3]
  {USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F 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. 
      (TotallyDefiniteQuaternionAlgebra.DfxTotallyDefiniteQuaternionAlgebra.Dfx.{u_1, u_2} (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D]
  [Algebra F D] : Type (max u_1 u_2)`Dfx` is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ 
        FType 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 (TotallyDefiniteQuaternionAlgebra.Dfx F D)) :
  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_3
    (TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevelTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.{u_1, u_2, u_3} {F : Type u_1} [Field F]
  [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D]
  (U : Subgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D)) (R : Type u_3) [CommRing R] : Type (max (max u_3 u_2) u_1)`WeightTwoAutomorphicFormOfLevel U R` is the `R`-valued weight 2 automorphic forms of a fixed
level `U` for a totally definite quaternion algebra over a totally real field.

      USubgroup (TotallyDefiniteQuaternionAlgebra.Dfx F D) KType u_3)
    Let `D/F` be a totally definite quaterion algebra over a totally real
field. Then the space of `K`-valued weight 2 level `U` quaternionic automorphic forms
for `Dˣ` is finite-dimensional over `K`.
    complete
Proof

The finite-dimensionality theorem is in fact an easy consequence of Fujisaki's lemma, proved in the Fujisaki miniproject. Theorem 11.16, and Theorem 11.17. Write (D \otimes_F \A_F^\infty)^\times as a disjoint union of double cosets \coprod_i D^\times g_i U. This open cover descends to a disjoint open cover of D^\times \backslash (D \otimes_F \A_F^\infty)^\times, and this latter space is compact by Theorem 11.16. Hence the cover is finite; write the double coset representatives as g_1, g_2, \ldots, g_n.

We claim that the function S^D(U;k) \to k^n sending f to (f(g_1), f(g_2), \ldots, f(g_n)) is injective and k-linear, which suffices by finite-dimensionality of k^n. k-linearity is easy, so let us talk about injectivity.

Say f_1 and f_2 are two elements of S^D(U;k) which agree on each g_i. It suffices to prove that f_1(g) = f_2(g) for all g \in (D \otimes_F \A_F^\infty)^\times. So say g \in (D \otimes_F \A_F^\infty)^\times, and write g = \delta g_i u for \delta \in D^\times and u \in U. Then f_1(g) = f_1(\delta g_i u) = f_1(g_i) by the definition of S^D(U;k), and similarly f_2(g) = f_2(g_i). Because f_1(g_i) = f_2(g_i) by assumption, we deduce that f_1(g) = f_2(g) as required.