5. An Example Of An Automorphic Form🔗

5.1. Introduction🔗

The key ingredient in Wiles' proof of Fermat's Last Theorem is a modularity lifting theorem, sometimes called an R=T theorem. For Wiles, the R came from elliptic curves, the T came from classical modular forms, and the fact that they're equal is basically the Shimura--Taniyama--Weil conjecture, now known as the Breuil--Conrad--Diamond--Taylor modularity theorem: any elliptic curve over the rationals is modular.

At the heart of the proof we shall formalise is also an R=T theorem, however the T which we shall use will be associated not to classical modular forms, but to spaces of more general automorphic forms called quaternionic modular forms. Those of you who know something about classical modular forms might well know that the groups \SL_2(\R) and \SL_2(\Z) are intimately involved; these are the norm 1 units in the matrix rings M_2(\R) and M_2(\Z). In the theory of quaternionic modular forms, the analogous groups are the norm 1 units in rings such as Hamilton's quaternions \R\oplus\R i\oplus\R j\oplus\R k, and subrings such as \Z\oplus\Z i\oplus\Z j\oplus\Z k.

One of the main goals of the FLT project at the time of writing this sentence, is formalising the statement of the modularity lifting theorem which we shall use. So we are going to need to develop the theory of quaternionic modular forms, which is rather different to the theory of classical modular forms (for example, in the cases we need, the definition is completely algebraic; there are no holomorphic functions in sight, and the analogue of the upper half plane in the quaternionic theory is a finite set of points).

We could just launch into the general theory over totally real fields, which will be the generality which we'll need. But when I was a PhD student, I learnt about these objects by playing with explicit examples. So, whilst not logically necessary for the proof, I thought it would be fun, and perhaps also instructional, to compute a concrete example of a space of quaternionic modular forms. The process of constructing the example might even inform what kind of machinery we should be developing in general. Let's begin by discussing the quaternion algebra we shall use.

5.2. A quaternion algebra🔗

Let's define D to be the quaternion algebra \Q\oplus\Q i\oplus\Q j\oplus\Q k. As a vector space, D is 4-dimensional over \Q with [1,i,j,k] giving a basis. It has a (non-commutative) ring structure, with multiplication satisfying the usual quaternion algebra relations i^2=j^2=k^2=ijk=-1. You can think of D as an analogue of 2 × 2 matrices with rational coefficients, hence its units D^\times are an analogue of the group \GL_2(\Q).

We will also need an analogue of the group \GL_2(\Z), which will come from an integral structure on D. We choose the Hurwitz order, namely the subring \calO:=\Z\oplus\Z i\oplus\Z j\oplus\Z \omega, where \omega=\frac{-1+(i+j+k)}{2}, a cube root of unity, as (i+j+k)^2=-3. The simplest way to understand \calO is that it's quaternions a+bi+cj+dk where either a,b,c,d are all integers or are all in \frac{1}{2}+\Z.

Note that \calO is a maximal order and a Euclidean domain, which is why we prefer it over the more obvious sublattice \Z\oplus\Z i\oplus\Z j\oplus\Z k.

In this chapter, we are going to compute a complex vector space which could be called something like the "weight 2 level 2 modular forms for D^\times". The main result will be that this space is 1-dimensional.

Note that mathlib has modular forms, but it doesn't have enough complex analysis to deduce that the space of modular forms of a given weight and level is finite-dimensional. If all the sorrys in this chapter are completed before mathlib gets the necessary complex analysis, then the first nonzero space of modular forms to be proved finite-dimensional in Lean will be a space of quaternionic modular forms.

We will use a modern "adelic" definition of our modular forms, so the first thing we need to do is to talk about profinite completions.

5.3. Zhat🔗

Definition5.1

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Lemma 5.2

Blueprint label

«ZHat.commRing»

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 3

Hover a use site to preview it.

Preview

Lemma 5.2

Blueprint label

«ZHat.commRing»

Uses target in

statement

The profinite completion \Zhat of \Z is the set of all compatible collections c=(c_N)_N of elements of \Z/N\Z indexed by \N^+ := \{1,2,3,\ldots\}. A collection is said to be compatible if for all positive integers D \mid N, we have c_N mod D equals c_D.

Code for Definition5.1●1 definition

def ZHat : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

def ZHat : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

We define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

complete

Classically automorphic forms were defined as functions on symmetric spaces (like the upper half plane) which transformed well under the action of certain discrete groups (for example \SL_2(\Z)). However such definitions became combinatorially problematic when generalised to number fields with nontrivial class group, because the classical theory needed a number p to define the Hecke operator T_p, and in the case where p was a non-principal prime ideal in a number field, there was no appropriate number. One fix is to take disjoint unions of symmetric spaces indexed by the ideal class group of the field in question, but it is easier to work adelically, which is morally what we shall do. However we are able to avoid introducing the adeles explicitly; we can work instead with the conceptually simpler object \Zhat, the profinite completion of \Z. So what is \Zhat? We offer a low-level definition of this object.

Lemma5.2

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 11

Hover a use site to preview it.

Preview

Lemma 5.3

Blueprint label

«ZHat.nontrivial»

Uses target in

statement

Definition 5.1 \Zhat is a subring of \prod_{N\geq1}(Z/N\Z) and in particular is a ring.

Code for Lemma5.2●1 definition

def ZHat.commRing : CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

def ZHat.commRing : CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

complete

Proof

Follow your nose.

Lemma5.3

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Lemma 5.2 0\not=1 in \Zhat.

Code for Lemma5.3●1 theorem

theorem ZHat.nontrivial : NontrivialNontrivial.{u_3} (α : Type u_3) : PropPredicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension.  ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

theorem ZHat.nontrivial : NontrivialNontrivial.{u_3} (α : Type u_3) : PropPredicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension.  ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

complete

Proof

Recall that you can evaluate an element of \Zhat at a positive integer. Evaluating 0 at 2 gives 0, and evaluating 1 at 2 gives 1, and these are distinct elements of \Z/2\Z, so 0\not=1 in \Zhat.

Lemma5.4

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

The map from the naturals into \Zhat sending n to n is injective.

Code for Lemma5.4●1 theorem

theorem ZHat.charZero : CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

theorem ZHat.charZero : CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

complete

Proof

Generalise the above idea. Feel free to write up a LaTeX proof and PR it.

Note that it follows easily that that the map from the integers to \Zhat is injective.

But \Zhat is much larger than \Z; it has the same cardinality as the reals in fact. Let's write down an explicit example of an element of \Zhat which isn't obviously in \Z.

Definition5.5

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Lemma 5.6

Blueprint label

«ZHat.e_def»

Uses target in

statement

Lemma 5.2 The infinite sum 0!+1!+2!+3!+4!+5!+\cdots looks like it makes no sense at all; it is the sum of an infinite series of larger and larger positive numbers. However, the sum is finite modulo N for every positive integer N, because all the terms from N! onwards are multiples of N and thus are zero in \Z/N\Z. Thus it makes sense to define e_N to be the value of the finite sum modulo N. Explicitly, e_N=0!+1!+\cdots+(N-1)! modulo N.

Code for Definition5.5●1 definition

def ZHat.e : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

def ZHat.e : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type.

A nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`.
It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.

complete

Lemma5.6

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.5 The collection (e_N)_N is an element of \Zhat.

Code for Lemma5.6●1 theorem

theorem ZHat.e_def (nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) : ZHat.eZHat.e : ZHatA nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`.
It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.  nℕ+ =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`. ∑ iℕ ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.  ↑nℕ+, ↑iℕ.factorialNat.factorial : ℕ → ℕ`Nat.factorial n` is the factorial of `n`.

theorem ZHat.e_def (nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) :
  ZHat.eZHat.e : ZHatA nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`.
It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.  nℕ+ =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`.
    ∑ iℕ ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.  ↑nℕ+, ↑iℕ.factorialNat.factorial : ℕ → ℕ`Nat.factorial n` is the factorial of `n`.

complete

Proof

This boils down to checking that D!+(D+1)!+\cdots+(N-1)! is a multiple of D.

Lemma5.7

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.5 The element (e_N)_N of \Zhat is not in \Z.

Code for Lemma5.7●1 theorem

theorem ZHat.e_not_in_Int (aℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
) : ZHat.eZHat.e : ZHatA nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`.
It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.  ≠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`. ↑aℤ

theorem ZHat.e_not_in_Int (aℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
) : ZHat.eZHat.e : ZHatA nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`.
It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.  ≠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`. ↑aℤ

Nonarchimedean $e$ is not an integer.

complete

Proof

First imagine that e=n with n\in\Z and 0\leq n. In this case, choose j such that 0!+1!+2!+\cdots+j!>n and check also that the sum is less than (j+1)!. Now set N=(j+1)! and let's compare e_N and n_N=n. The trick is that e_N must be 0!+1!+\cdots+j! mod N, because all the terms beyond this are multiples not just of (j+1) but of (j+1)!=N. Thus mod N we have 0\leq n<e_N<N so n\not=e.

Now we deal with n=-t<0; choose j large such that (j+1)!-(0!+1!+\cdots+j!)>t (possible because the sum is at most 2\times j!) and then set N=(j+1)! and we have 0 < e_N<N-t<N so we cannot have e_N=-t in \Z/N\Z, so again e\not=n.

Lemma5.8

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Lemma 5.2 Lemma 5.4 If 0<N is an integer then multiplication by N is injective on \Zhat.

Code for Lemma5.8●1 theorem

theorem ZHat.torsionfree (Nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) : Function.InjectiveFunction.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called injective if `f x = f y` implies `x = y`.  fun zZHat ↦ ↑↑Nℕ+ *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`. zZHat

theorem ZHat.torsionfree (Nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) :
  Function.InjectiveFunction.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called injective if `f x = f y` implies `x = y`.  fun zZHat ↦ ↑↑Nℕ+ *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`. zZHat

complete

Proof

Suppose that (z_i)_i\in\Zhat and Nz=0. This means that Nz_i=0\in\Z/i\Z for all i. Let us fix an arbitrary positive integer~j; we need to prove that z_j=0\in\Z/j\Z. Consider the element z_{Nj}\in\Z/Nj\Z. By assumption, we have Nz_{Nj}=0, meaning that if we lift z_{Nj} to an integer, we have Nj\mid Nz_{Nj}, and thus j\mid z_{Nj}. Thus by the compatibility assumption on the z_i we have that z_j\in\Z/j\Z is the mod~j reduction of z_{Nj} and hence is zero.

Lemma5.9

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Lemma 5.2 The multiples of~N in \Zhat are precisely the compatible collections (z_i)_i\in\Zhat with z_N=0.

Code for Lemma5.9●1 theorem

theorem ZHat.multiples (Nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) (zZHat : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type. ) : (∃ yZHat, ↑↑Nℕ+ *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`. yZHat =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`. zZHat) ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). zZHat Nℕ+ =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`. 0

theorem ZHat.multiples (Nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) (zZHat : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type. ) :
  (∃ yZHat, ↑↑Nℕ+ *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`. yZHat =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`. zZHat) ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). zZHat Nℕ+ =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`. 0

complete

Proof

Clearly z_N=0 is a necessary condition to be a multiple of~N. To see it is sufficient, take a general (z_i)\in\Zhat such that z_N=0, and now define a new element (y_j)_j of \Zhat by y_j=z_{Nj}/N. Just to clarify what this means: z_{Nj}\in\Z/Nj\Z reduces mod~N to z_N=0 by the compatibility assumption, so it is in the subgroup N\Z/Nj\Z of \Z/Nj\Z, which is isomorphic (via "division by N") to the group \Z/j\Z; this is how we construct y_j. It is easily checked that the y_j are compatible and that Ny=z.

5.4. More Advanced Remarks On Zhat Versus Q🔗

This section can be skipped on first reading.

People who have seen some more advanced algebra might recognise this construction of \Zhat as being the profinite completion of the additive abelian group \Z, so it is a fundamental object of mathematics in some sense. But usually, when building mathematics, after \Z we go to \Q, a multiplicative localisation of \Z, and only complete after that (to get \R). The process of "completing before localising" gives us a far more arithmetic completion of \Z.

Even though \Q is a divisible abelian group and hence its profinite completion vanishes, we can still attempt to "locally profinitely complete it" by defining \Qhat:=\Q\otimes_{\Z}\Zhat. This object is more commonly known as the finite adeles of \Q. More generally if F is any number field then F\otimes_{\Z}\Zhat is the ring of finite adeles of F. To get to the full ring of adeles of a number field F you need to take the product with the ring of infinite adeles of F, which is F\otimes_{\Q}\R: some kind of universal archimedean completion of F. I don't know a reference which develops the theory of adeles in this way, so this is what we shall do here.

5.5. Qhat and tensor products.🔗

The definition of \Qhat is easy if you know about tensor products of additive abelian groups.

Definition5.10

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 8

Hover a use site to preview it.

Preview

Lemma 5.11

Blueprint label

«QHat.canonicalForm»

Uses target in

statement

Definition 5.1 The profinite completion \Qhat of \Q is the tensor product \Q\otimes_{\Z}\Zhat, or \Qhat=\Q\otimes\Zhat for short.

Code for Definition5.10●1 definition

def QHat : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

def QHat : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

The "profinite completion" of ℚ is defined to be `ℚ ⊗ ZHat`, with `ZHat` the profinite
completion of `ℤ`.

complete

5.6. A crash course in tensor products🔗

We've defined \Qhat to be \Q\otimes\Zhat. Whatever does this mean? Well just to orient yourself, if A and B are additive abelian groups, then A\otimes B is also an abelian group. And if A and B are commutative rings (as they are in our case), then A\otimes B is also a commutative ring.

Even if A and B are completely concrete commutative rings, their tensor product A\otimes B might be incomprehensible. For example \bbC\otimes\bbC is completely incomprehensible (note that we are tensoring over the integers). It is not like the product of groups or the disjoint union of two sets, where you have a completely explicit unambiguous formula for each element.

In this sense, the theory of tensor products is a bit like the theory of continuous functions. Humanity started off studying concrete polynomial equations such as x^2+1 and then moved on to concrete analytic functions such as \log(x) and \sin(x), but eventually the abstract concept of a continuous function from the reals to the reals was born. There is no "formula" for a general continuous function, and continuous functions such as e^{-1/x^2} or |x| have no power series. Even if there were a formula for a specific continuous function of interest, it is not clear in general how to make sense of the claim that it's the "best" formula. In other words, there is no "canonical form" for a general continuous function, and yet we prove things about them anyway. We shall adopt the same attitude for elements of A\otimes B.

The first thing to know about the tensor product A\otimes B of two abelian groups A and B is a "constructor" for the type. In other words, how can we make elements A\otimes B? Well, it turns out that given elements a\in A and b\in B, we can form the element a\otimes_t b\in A\otimes B.

Recall that the sum of all the factorials is an element e\in\Zhat, and 22/7 is certainly a rational number, so we can make the element \frac{22}{7}\otimes_te\in\Qhat.

This example is in the Lean code.

Elements of the form a\otimes_t b\in A\otimes B are known as pure tensors. In the literature, pure tensors are often written a\otimes b, but we shall follow mathlib's convention in reserving the \otimes symbol for groups like A \otimes B, and adorning it with a t when using it on elements of the groups (or, as Lean calls them, terms, which explains the notation).

Addition of pure tensors obeys the "distributivity" rules a\otimes_t b_1+a\otimes_t b_2=a\otimes_t(b_1+b_2) and a_1\otimes_t b+a_2\otimes_t b=(a_1+a_2)\otimes_t b, but there is no rule which simplifies a general sum a\otimes_t b + c\otimes_t d into a pure tensor. Indeed, in general it is not the case that every element of a tensor product A\otimes B is of the form a\otimes_t b; there can be tensors which aren't pure. However every element of A\otimes B is a finite sum of pure tensors, with the result that one can attempt to define additive maps from A\otimes B by saying what they do on pure tensors, and then extending linearly.

Another thing worth understanding is that just like how rational numbers can be written as quotients of integers in several ways (for example 1/2=2/4=3/6=\cdots), a general pure tensor in A\otimes B can be represented as a\otimes_t b in many ways. For example, in \Qhat we have 1\otimes_t 2=2\otimes_t 1. A general rule for equality of pure tensors is that if a\in A and b\in B and z\in\Z, then za\otimes_tb=a\otimes_tzb; integers can move over the tensor symbol. But equality is hard: in general there may not be an algorithm to decide whether two pure tensors a\otimes_t b and c\otimes_t d are equal in A\otimes B.

A summary of the situation: if A and B are abelian groups, then every element of A\otimes B can be written in the form \sum_{i=1}^Na_i\otimes_tb_i. It's just that this representation is highly nonunique, and furthermore given explicit elements a_1,a_2\in A and b_1,b_2\in B it might be a hard problem to figure out if a_1\otimes_t b_1=a_2\otimes_t b_2.

For example, it turns out that (\Z/2\Z)\otimes(\Z/3\Z)=0 and so in this tensor product all the a\otimes_t b are equal to each other and to 0\otimes 0.

Having said all of that, one nice property of \Qhat is that every tensor is pure; let's prove this now.

Lemma5.11

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Lemma 5.17

Blueprint label

«QHat.rat_join_zHat»

Uses target in

proof

Definition 5.10 Lemma 5.2 Every element of \Qhat:=\Q\otimes\Zhat can be written as q\otimes_t z with q\in\Q and z\in\Zhat. Furthermore one can even assume that q=\frac{1}{N} for some positive integer N.

Code for Lemma5.11●1 theorem

theorem QHat.canonicalForm (zQHat : QHatQHat : TypeThe "profinite completion" of ℚ is defined to be `ℚ ⊗ ZHat`, with `ZHat` the profinite
completion of `ℤ`. ) : ∃ Nℕ+ z'ZHat, zQHat =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`. (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑Nℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  z'ZHat

theorem QHat.canonicalForm (zQHat : QHatQHat : TypeThe "profinite completion" of ℚ is defined to be `ℚ ⊗ ZHat`, with `ZHat` the profinite
completion of `ℤ`. ) :
  ∃ Nℕ+ z'ZHat, zQHat =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`. (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑Nℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  z'ZHat

complete

Proof

A proof I would write on the board would look like the following. Take a general element of \Qhat; we know it can be expressed as a finite sum \sum_i q_i\otimes_t z_i with q_i\in\Q and z_i\in\Zhat. Now choose a large positive integer N, the lowest common multiple of all the denominators showing up in the q_i, and then rewrite \sum_i q_i\otimes_t z_i as \sum_i \frac{n_i}{N}\otimes z_i with n_i\in\Z. Now using the fundamental fact that na\otimes_t b=a\otimes_t nb for n\in\Z, we can rewrite the sum as \sum_i \frac{1}{N}\otimes_t n_i z_i which is equal to the pure tensor \frac{1}{N}\otimes(\sum_i n_i z_i).

In Lean I would prove this using TensorProduct.induction_on, which quickly reduces us to the claim that the sum of two pure tensors is pure, which we can prove using the above technique whilst avoiding the general theory of finite sums.

Be careful though: just because every element of \Qhat can be written as q\otimes z, this representation may not be unique. For example 2\otimes 1=1\otimes 2. However, writing \frac{1}{N}\otimes_t z as z/N does tempt us into the following definition.

Definition5.12

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Lemma 5.2 If N\in\N^+ and z\in\Zhat then we say that N and z are coprime if z_N\in(\Z/N\Z)^\times. We write z/N as notation for the element \frac{1}{N}\otimes_tz.

Code for Definition5.12●1 definition

def QHat.IsCoprime (Nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) (zZHat : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.

def QHat.IsCoprime (Nℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) (zZHat : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.

complete

Lemma5.13

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 2

Hover a use site to preview it.

Preview

Lemma 5.16

Blueprint label

«QHat.rat_meet_zHat»

Uses target in

proof

Definition 5.12 Every element of \Qhat can be uniquely written as z/N with z\in\Zhat, N\in\N^+, and with N and z coprime.

Code for Lemma5.13●1 theorem

theorem QHat.lowestTerms (xQHat : QHatQHat : TypeThe "profinite completion" of ℚ is defined to be `ℚ ⊗ ZHat`, with `ZHat` the profinite
completion of `ℤ`. ) :
  (∃ Nℕ+ zZHat, QHat.IsCoprimeQHat.IsCoprime (N : ℕ+) (z : ZHat) : Prop Nℕ+ zZHat ∧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 `/\`). xQHat =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`. (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑Nℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  zZHat) ∧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 `/\`).
    ∀ (N₁ℕ+ N₂ℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) (z₁ZHat z₂ZHat : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type. ),
      QHat.IsCoprimeQHat.IsCoprime (N : ℕ+) (z : ZHat) : Prop N₁ℕ+ z₁ZHat ∧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 `/\`).
          QHat.IsCoprimeQHat.IsCoprime (N : ℕ+) (z : ZHat) : Prop N₂ℕ+ z₂ZHat ∧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 `/\`).
            (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑N₁ℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  z₁ZHat =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`. (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑N₂ℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  z₂ZHat →
        N₁ℕ+ =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`. N₂ℕ+ ∧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 `/\`). z₁ZHat =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`. z₂ZHat

theorem QHat.lowestTerms (xQHat : QHatQHat : TypeThe "profinite completion" of ℚ is defined to be `ℚ ⊗ ZHat`, with `ZHat` the profinite
completion of `ℤ`. ) :
  (∃ Nℕ+ zZHat,
      QHat.IsCoprimeQHat.IsCoprime (N : ℕ+) (z : ZHat) : Prop Nℕ+ zZHat ∧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 `/\`).
        xQHat =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`. (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑Nℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  zZHat) ∧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 `/\`).
    ∀ (N₁ℕ+ N₂ℕ+ : ℕ+PNat : Type`ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored. ) (z₁ZHat z₂ZHat : ZHatZHat : TypeWe define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for
all positive integers `N`. We declare it as a subring of `∏_{N ≥ 1} (ℤ/Nℤ)`, and then promote it
to a type. ),
      QHat.IsCoprimeQHat.IsCoprime (N : ℕ+) (z : ZHat) : Prop N₁ℕ+ z₁ZHat ∧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 `/\`).
          QHat.IsCoprimeQHat.IsCoprime (N : ℕ+) (z : ZHat) : Prop N₂ℕ+ z₂ZHat ∧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 `/\`).
            (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑N₁ℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  z₁ZHat =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`.
              (HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑↑N₂ℕ+)HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  z₂ZHat →
        N₁ℕ+ =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`. N₂ℕ+ ∧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 `/\`). z₁ZHat =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`. z₂ZHat

complete

Proof

Existence: by the previous lemma, an arbitrary element can be written as z/N; let D be the greatest common divisor of N and z_N (lifted to a natural). If D=1 then the fraction is by definition in lowest terms. However if 1<D\mid N then z_D is the reduction of z_N and is hence 0. By lemma ZHat.multiples we deduce that z=Dy is a multiple of D, and hence z/N=\frac{1}{N}\otimes_tDy=\frac{1}{E}\otimes y, where E=N/D. Now if a natural divided both y_E and E then this natural would divide both z_N/D and N/D, contradicting the fact that D is the greatest common divisor.

Uniqueness: if z/N=w/M, we deduce 1\otimes_t Mz=1\otimes_t Nw, and by injectivity of \Zhat\to\Qhat we deduce that Mz=Nw=y. In particular, if L is the lowest common multiple of M and N then y_L is a multiple of both M and N and is hence zero, so y=Lx is a multiple of L by ZHat.multiples, and we deduce from torsionfreeness that z=(L/M)x and w=(L/N)x. If some prime divided L/M then it would have to divide N which means that z is not in lowest terms; similarly if some prime divided L/N then w/M would not be in lowest terms. We deduce that L=M=N and hence z=w by torsionfreeness.

If A and B are additive abelian groups then A\otimes B is also an additive abelian group. However if A and B are commutative rings, then A\otimes B also inherits the structure of a commutative ring, with 0=0\otimes_t 0 and 1=1\otimes_t 1. Pure tensors multiply in the obvious way: the product of a_1\otimes_t b_1 and a_2\otimes_t b_2 is a_1a_2\otimes_t b_1b_2. There are ring homomorphisms A\to A\otimes B and B\to A\otimes B sending a to a\otimes_t 1 and b to 1\otimes_t b. In general such maps are not injective, but in the case of \Qhat=\Q\otimes\Zhat both maps from \Q and \Zhat are inclusions.

Lemma5.14

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.10 Lemma 5.2 The ring homomorphism \Q\to\Qhat sending q to q\otimes_t 1 is injective.

Code for Lemma5.14●1 theorem

theorem QHat.injective_rat : Function.InjectiveFunction.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called injective if `f x = f y` implies `x = y`.  ⇑QHat.i₁QHat.i₁ : ℚ →ₐ[ℤ] QHat

theorem QHat.injective_rat :
  Function.InjectiveFunction.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called injective if `f x = f y` implies `x = y`.  ⇑QHat.i₁QHat.i₁ : ℚ →ₐ[ℤ] QHat

complete

Proof

We have seen that the map from \Z to \Zhat is injective. Now \Q is a flat \Z-module, because it's torsion-free, so tensoring up we deduce that the map from \Q=\Q\otimes\Z to \Qhat=\Q\otimes\Zhat is also injective. There is no doubt a more elementary proof of this fact.

Lemma5.15

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.10 Lemma 5.8 The ring homomorphism \Zhat\to\Qhat sending z to 1\otimes_t z is injective.

Code for Lemma5.15●1 theorem

theorem QHat.injective_zHat : Function.InjectiveFunction.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called injective if `f x = f y` implies `x = y`.  ⇑QHat.i₂QHat.i₂ : ZHat →ₐ[ℤ] QHat

theorem QHat.injective_zHat :
  Function.InjectiveFunction.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called injective if `f x = f y` implies `x = y`.  ⇑QHat.i₂QHat.i₂ : ZHat →ₐ[ℤ] QHat

complete

Proof

The map from \Z to \Q is injective, and we have seen that \Zhat is a torsion-free and thus flat \Z-module, so the map from \Zhat to \Qhat is also injective.

5.7. Additive structure of Qhat.🔗

Here we forget the ring structure on everything, and analyse \Qhat as an additive abelian group, and in particular how the subgroups \Z, \Q and \Zhat sit within it.

The two results we prove in this section are that \Q\cap\Zhat=\Z and that \Q+\Zhat=\Qhat. Using lattice-theoretic notation we could write these results as \Q\sqcap\Zhat=\Z and \Q\sqcup\Zhat=\Qhat.

Lemma5.16

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Definition 5.10 Lemma 5.2 The intersection of \Q and \Zhat in \Qhat is \Z.

Code for Lemma5.16●1 theorem

theorem QHat.rat_meet_zHat : QHat.ratsubQHat.ratsub : AddSubgroup QHat ⊓ QHat.zHatsubQHat.zHatsub : AddSubgroup QHat =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`. QHat.zsubQHat.zsub : AddSubgroup QHat

theorem QHat.rat_meet_zHat :
  QHat.ratsubQHat.ratsub : AddSubgroup QHat ⊓ QHat.zHatsubQHat.zHatsub : AddSubgroup QHat =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`. QHat.zsubQHat.zsub : AddSubgroup QHat

complete

Proof

Lemma 5.13 Clearly \Z\subseteq\Q\cap\Zhat. Now suppose that x\in\Q\cap\Zhat. Because x is rational we can write it as \frac{A}{B}\otimes_t1 for some fraction A/B in lowest terms, and hence x=A/B where now we regard A\in\Zhat and note that A/B is still in lowest terms. However x\in\Zhat implies that x=x/1 is in lowest terms, so we deduce that B=1 and thus x=A\in\Z.

Lemma5.17

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.10 Lemma 5.2 The sum of \Q and \Zhat in \Qhat is \Qhat. More precisely, every element of \Qhat can be written as q+z with q\in\Q and z\in\Zhat, or more precisely as q\otimes_t 1+1\otimes_t z.

Code for Lemma5.17●1 theorem

theorem QHat.rat_join_zHat : QHat.ratsubQHat.ratsub : AddSubgroup QHat ⊔ QHat.zHatsubQHat.zHatsub : AddSubgroup QHat =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`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.

theorem QHat.rat_join_zHat :
  QHat.ratsubQHat.ratsub : AddSubgroup QHat ⊔ QHat.zHatsubQHat.zHatsub : AddSubgroup QHat =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`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.

complete

Proof

Lemma 5.11 Write x\in\Qhat as x=z/N in lowest terms. Lift z_N to an integer t and observe that (z-t)_N=0, hence z-t=Ny for some y\in\Zhat. Now x=t/N+y\in\Q+\Zhat.

5.8. Multiplicative structure of the units of Qhat.🔗

We now forget the additive structure on the commutative ring \Qhat and consider the multiplicative structure of its group of units \Qhat^\times (which I couldn't get into the section title). We have the obvious subgroups \Q^\times, \Z^\times and \Zhat^\times.

Lemma5.18

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.10 Lemma 5.2 The intersection of \Q^\times and \Zhat^\times in \Qhat^\times is \Z^\times.

Code for Lemma5.18●1 theorem

theorem QHat.unitsrat_meet_unitszHat :
  QHat.unitsratsubQHat.unitsratsub : Subgroup QHatˣ ⊓ QHat.unitszHatsubQHat.unitszHatsub : Subgroup QHatˣ =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`. QHat.unitszsubQHat.unitszsub : Subgroup QHatˣ

theorem QHat.unitsrat_meet_unitszHat :
  QHat.unitsratsubQHat.unitsratsub : Subgroup QHatˣ ⊓ QHat.unitszHatsubQHat.unitszHatsub : Subgroup QHatˣ =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`.
    QHat.unitszsubQHat.unitszsub : Subgroup QHatˣ

complete

Proof

Lemma 5.13 Lemma 5.16 Clearly the intersection is contained within \Q\cap\Zhat=\Z. If n\in\Z is in \Zhat^\times then n\not=0 and its inverse 1/n=\pm1/|n| is in lowest terms but also in \Zhat, and hence |n|=1 by uniqueness of lowest term representation.

Note that by the previous lemma, this representation will be unique up to sign.

Lemma5.19

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.10 Lemma 5.2 The product of \Q^\times and \Zhat^\times in \Qhat^\times is all of \Qhat^\times. More precisely, every element of \Qhat^\times can be written as qz with q\in\Q^\times and z\in\Zhat^\times.

Code for Lemma5.19●1 theorem

theorem QHat.unitsrat_join_unitszHat : QHat.unitsratsubQHat.unitsratsub : Subgroup QHatˣ ⊔ QHat.unitszHatsubQHat.unitszHatsub : Subgroup QHatˣ =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`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.

theorem QHat.unitsrat_join_unitszHat :
  QHat.unitsratsubQHat.unitsratsub : Subgroup QHatˣ ⊔ QHat.unitszHatsubQHat.unitszHatsub : Subgroup QHatˣ =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`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.

complete

Proof

Lemma 5.9 [??] Lemma 5.11 We already know that a general element of \Qhat^\times can be written as x/N with N positive, so this reduces us to proving that a general element x\in\Zhat which is invertible in \Qhat^\times can be written as qz with q\in\Q^\times and z\in\Zhat^\times.

We know 1/x can be written in lowest terms as y/M, and multiplying up we deduce that xy=M, and hence x divides a positive integer. If i:\Z\to\Zhat denotes the inclusion, then we've just seen that the preimage of the principal ideal (x), namely, J:=i^{-1}(x\Zhat) is nonzero, as it contains M. Let g\in J be the smallest positive integer; it's well-known that J=(g).

I claim that it suffices to show that x\Zhat=g\Zhat. Because knowing g=yx and x=gz for some y,z\in\Zhat tells us that g(1-yz)=0, and we know that multiplication by g is injective, hence yz=1, so z is a unit and we have written x=gz with g\in\Q^\times and z\in\Zhat^\times.

It remains to prove the claim. By definition g\in J\subseteq x\Zhat so this is one inclusion. For the other, it suffices to prove that x_g=0. However if 0<x_g<g lifts x_g to the naturals then I claim that x_g\in J, for x_g-x is a multiple of g and hence of x, and this contradicts minimality of g.

5.9. The Hurwitz quaternions🔗

Definition5.20

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 4

Hover a use site to preview it.

Preview

Lemma 5.21

Blueprint label

«Hurwitz.ring»

Uses target in

statement

The Hurwitz quaternions are the set \calO := \Z\oplus\Z \omega\oplus\Z i\oplus\Z i\omega (as an abstract abelian group or as a subgroup of the usual quaternions). Here \omega=\frac{-1+(i+j+k)}{2} and note that (i+j+k)^2=-3. We have \overline{\omega}=\omega^2=-(\omega+1). A general quaternion a+bi+cj+dk is a Hurwitz quaternion if either a,b,c,d\in\Z or a,b,c,d\in\Z+\frac{1}{2}.

Code for Definition5.20●1 definition

structure Hurwitz : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

structure Hurwitz : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

Constructor

Hurwitz.mk (reℤ im_oℤ im_iℤ im_oiℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
) : 𝓞Hurwitz : Type

Fields

reℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

im_oℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

im_iℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

im_oiℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

complete

Lemma5.21

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Definition 5.20 The Hurwitz quaternions form a ring.

Code for Lemma5.21●1 definition

def Hurwitz.ring : RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  𝓞Hurwitz : Type

def Hurwitz.ring : RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  𝓞Hurwitz : Type

complete

Proof

Follow your nose.

This ring is isomorphic to \Z^4 as an additive group, and \calO\otimes_{\Z}\R=\R\oplus \R i\oplus \R j\oplus\R \omega is the usual Hamilton quaternions.

Definition5.22

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Lemma 5.21 There's a conjugation map (which we'll call "star") from the Hurwitz quaternions to themselves, sending integers to themselves and purely imaginary elements like 2\omega+1 to minus themselves. It satisfies (x^*)^*=x, (xy)^*=y^*x^* and (x+y)^*=x^*+y^*. In particular, the Hurwitz quaternions are a "star ring" in the sense of mathlib.

Code for Definition5.22●1 definition

def Hurwitz.starRing : StarRingStarRing.{u} (R : Type u) [NonUnitalNonAssocSemiring R] : Type uA `*`-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation
which is additive which makes `R` with its multiplicative structure into a `*`-multiplication
(i.e. `star (r * s) = star s * star r`).  𝓞Hurwitz : Type

def Hurwitz.starRing : StarRingStarRing.{u} (R : Type u) [NonUnitalNonAssocSemiring R] : Type uA `*`-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation
which is additive which makes `R` with its multiplicative structure into a `*`-multiplication
(i.e. `star (r * s) = star s * star r`).  𝓞Hurwitz : Type

Conjugate; sends $a+bi+cj+dk$ to $a-bi-cj-dk$.

complete

Definition5.23

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀N

Used by 9

Hover a use site to preview it.

Preview

Lemma 5.24

Blueprint label

«Hurwitz.norm_eq_mul_conj»

Uses target in

proof

Definition 5.20 The Hurwitz quaternions come equipped with an integer-valued norm, which is a^2+b^2+c^2+d^2 on a+bi+cj+dk but needs to be modified a bit to deal with \omega.

Code for Definition5.23●1 definition

def Hurwitz.norm (z𝓞 : 𝓞Hurwitz : Type) : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

def Hurwitz.norm (z𝓞 : 𝓞Hurwitz : Type) : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

complete

Lemma5.24

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

We have N(x)=x\overline{x}.

Code for Lemma5.24●1 theorem

theorem Hurwitz.norm_eq_mul_conj (z𝓞 : 𝓞Hurwitz : Type) : ↑z𝓞.normHurwitz.norm (z : 𝓞) : ℤ =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`. z𝓞 *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`. starStar.star.{u} {R : Type u} [self : Star R] : R → RA star operation (e.g. complex conjugate).
 z𝓞

theorem Hurwitz.norm_eq_mul_conj (z𝓞 : 𝓞Hurwitz : Type) :
  ↑z𝓞.normHurwitz.norm (z : 𝓞) : ℤ =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`. z𝓞 *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`. starStar.star.{u} {R : Type u} [self : Star R] : R → RA star operation (e.g. complex conjugate).
 z𝓞

complete

Proof

Definition 5.23 Definition 5.22 Easy calculation.

Lemma5.25

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.23 The norm of 0 is 0.

Code for Lemma5.25●1 theorem

theorem Hurwitz.norm_zero : Hurwitz.normHurwitz.norm (z : 𝓞) : ℤ 0 =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`. 0

theorem Hurwitz.norm_zero : Hurwitz.normHurwitz.norm (z : 𝓞) : ℤ 0 =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`. 0

complete

Proof

A calculation.

Lemma5.26

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.23 The norm of 1 is 1.

Code for Lemma5.26●1 theorem

theorem Hurwitz.norm_one : Hurwitz.normHurwitz.norm (z : 𝓞) : ℤ 1 =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

theorem Hurwitz.norm_one : Hurwitz.normHurwitz.norm (z : 𝓞) : ℤ 1 =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

complete

Proof

A calculation.

Lemma5.27

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.23 The norm of a product is the product of the norms.

Code for Lemma5.27●1 theorem

theorem Hurwitz.norm_mul (x𝓞 y𝓞 : 𝓞Hurwitz : Type) : (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`.x𝓞 *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`. y𝓞)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`..normHurwitz.norm (z : 𝓞) : ℤ =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`. x𝓞.normHurwitz.norm (z : 𝓞) : ℤ *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`. y𝓞.normHurwitz.norm (z : 𝓞) : ℤ

theorem Hurwitz.norm_mul (x𝓞 y𝓞 : 𝓞Hurwitz : Type) :
  (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`.x𝓞 *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`. y𝓞)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`..normHurwitz.norm (z : 𝓞) : ℤ =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`. x𝓞.normHurwitz.norm (z : 𝓞) : ℤ *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`. y𝓞.normHurwitz.norm (z : 𝓞) : ℤ

complete

Proof

A calculation.

Lemma5.28

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.23 The norm of an element is nonnegative.

Code for Lemma5.28●1 theorem

theorem Hurwitz.norm_nonneg (x𝓞 : 𝓞Hurwitz : Type) : 0 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). x𝓞.normHurwitz.norm (z : 𝓞) : ℤ

theorem Hurwitz.norm_nonneg (x𝓞 : 𝓞Hurwitz : Type) : 0 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). x𝓞.normHurwitz.norm (z : 𝓞) : ℤ

complete

Proof

It's a sum of rational squares.

Lemma5.29

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.23 The norm of an element is zero if and only if the element is zero.

Code for Lemma5.29●1 theorem

theorem Hurwitz.norm_eq_zero (x𝓞 : 𝓞Hurwitz : Type) : x𝓞.normHurwitz.norm (z : 𝓞) : ℤ =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`. 0 ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). x𝓞 =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`. 0

theorem Hurwitz.norm_eq_zero (x𝓞 : 𝓞Hurwitz : Type) :
  x𝓞.normHurwitz.norm (z : 𝓞) : ℤ =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`. 0 ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). x𝓞 =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`. 0

complete

Proof

It's a sum of rational squares.

Lemma5.30

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Definition 5.23 Given a "usual" quaternion a=x+yi+zj+wk with x,y,z,w\in\R, there exists a Hurwitz quaternion q such that N(a-q)<1.

Code for Lemma5.30●1 theorem

theorem Hurwitz.exists_near (aQuaternion ℝ : QuaternionQuaternion.{u_1} (R : Type u_1) [Zero R] [One R] [Neg R] : Type u_1Space of quaternions over a type, denoted as `ℍ[R]`.
Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : ∃ q𝓞, distDist.dist.{u_3} {α : Type u_3} [self : Dist α] : α → α → ℝDistance between two points  aQuaternion ℝ q𝓞.toQuaternionHurwitz.toQuaternion (z : 𝓞) : Quaternion ℝ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. 1

theorem Hurwitz.exists_near (aQuaternion ℝ : QuaternionQuaternion.{u_1} (R : Type u_1) [Zero R] [One R] [Neg R] : Type u_1Space of quaternions over a type, denoted as `ℍ[R]`.
Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  ∃ q𝓞, distDist.dist.{u_3} {α : Type u_3} [self : Dist α] : α → α → ℝDistance between two points  aQuaternion ℝ q𝓞.toQuaternionHurwitz.toQuaternion (z : 𝓞) : Quaternion ℝ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. 1

complete

Proof

If [r] denotes the nearest integer to the real number r, then |r-[r]|\leq \frac{1}{2}. Hence if q=[x]+[y]i+[z]j+[w]k then N(a-q)=|x-[x]|^2+\cdots \leq \frac{1}{4}+\frac{1}{4}+\frac{1}{4}+\frac{1}{4}\leq 1, with strict inequality unless |x-[x]|=|y-[y]|=|z-[z]|=|w-[w]|=\frac{1}{2}, in which case a\in\mathcal{O} because a-\omega has integer coordinates.

Lemma5.31

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 1

Definition 5.23 Lemma 5.30 Given two Hurwitz quaternions a and b with b nonzero, there exists q and r such that a=qb+r and N(r)<N(b).

Code for Lemma5.31●1 theorem

theorem Hurwitz.quot_rem (a𝓞 b𝓞 : 𝓞Hurwitz : Type) (hbb ≠ 0 : b𝓞 ≠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`. 0) :
  ∃ q𝓞 r𝓞, a𝓞 =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`. q𝓞 *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`. b𝓞 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. r𝓞 ∧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 `/\`). r𝓞.normHurwitz.norm (z : 𝓞) : ℤ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. b𝓞.normHurwitz.norm (z : 𝓞) : ℤ

theorem Hurwitz.quot_rem (a𝓞 b𝓞 : 𝓞Hurwitz : Type) (hbb ≠ 0 : b𝓞 ≠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`. 0) :
  ∃ q𝓞 r𝓞, a𝓞 =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`. q𝓞 *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`. b𝓞 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. r𝓞 ∧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 `/\`). r𝓞.normHurwitz.norm (z : 𝓞) : ℤ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. b𝓞.normHurwitz.norm (z : 𝓞) : ℤ

complete

Proof

Let q be the Hurwitz quaternion obtained by applying lemma Hurwitz.exists_near to a/b := ab^{-1}; then N(a/b-q)<1 and now everything follows after multiplying up.

Corollary5.32

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

✓L∃∀Nused by 0

Definition 5.23 All left ideals of \calO are principal.

Code for Corollary5.32●1 theorem

theorem Hurwitz.left_ideal_princ (ISubmodule 𝓞 𝓞 : SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  𝓞Hurwitz : Type 𝓞Hurwitz : Type) : ∃ a𝓞, ISubmodule 𝓞 𝓞 =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`. 𝓞Hurwitz : Type ∙Submodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
  Submodule R MThe span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.  a𝓞

theorem Hurwitz.left_ideal_princ
  (ISubmodule 𝓞 𝓞 : SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  𝓞Hurwitz : Type 𝓞Hurwitz : Type) : ∃ a𝓞, ISubmodule 𝓞 𝓞 =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`. 𝓞Hurwitz : Type ∙Submodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
  Submodule R MThe span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.  a𝓞

complete

Proof

Lemma 5.31 If the ideal is 0, use 0. Otherwise, choose a nonzero element of smallest norm.

All right ideals are principal too, because there's another version of Euclid saying a=bq+r.

5.10. Profinite completion of the Hurwitz quaternions🔗

We define \calOhat to be \calO\otimes\Zhat, so it's elements a+bi+cj+d\omega with a,b,c,d\in\Zhat. The basic thing we need is this:

Theorem5.33

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

XL∃∀Nused by 0

Definition 5.20 If N is a positive natural then the obvious map \calO\to\calOhat/N\calOhat is surjective.

Proof

This is just four copies of the surjection \Z\to\Zhat/N\Zhat. Note that this latter map is surjective because \Z\to\Z/N\Z is surjective, hence given z\in\Zhat you can subtract an integer w such that (z-w)_N=0, so z-w is a multiple of N.

We define D:=\Q\otimes\calO=\Q\oplus\Q i\oplus\Q j\oplus\Q\omega=\Q\oplus\Q i\oplus\Q j\oplus\Q k. Finally, we define \widehat{D}:=D\otimes\Zhat. Just as with \Qhat we have

Lemma5.34

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

⚠L∃∀Nused by 1

Definition 5.10 Definition 5.1 Definition 5.20 Every element of \widehat{D} can be written as z/N with z\in\calOhat and N\in\N^+.

Code for Lemma5.34●1 theorem, incomplete

theorem HurwitzRatHat.canonicalForm (zHurwitzRatHat : HurwitzRatHatHurwitzRatHat : TypeThe "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module
generated by 1, i, j, and (1+i+j+k)/2. ) :
  ∃ Nℕ+ z'HurwitzHat, zHurwitzRatHat =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`. HurwitzRatHat.j₁HurwitzRatHat.j₁ : HurwitzRat →ₐ[ℤ] HurwitzRatHatThe inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ.  (TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. (↑↑Nℕ+)⁻¹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`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  1)TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  *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`. HurwitzRatHat.j₂HurwitzRatHat.j₂ : HurwitzHat →ₐ[ℤ] HurwitzRatHatThe inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k,
with 𝔸 the finite adeles of ℚ.  z'HurwitzHat

theorem HurwitzRatHat.canonicalForm
  (zHurwitzRatHat : HurwitzRatHatHurwitzRatHat : TypeThe "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module
generated by 1, i, j, and (1+i+j+k)/2. ) :
  ∃ Nℕ+ z'HurwitzHat,
    zHurwitzRatHat =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`.
      HurwitzRatHat.j₁HurwitzRatHat.j₁ : HurwitzRat →ₐ[ℤ] HurwitzRatHatThe inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ.  (TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. (↑↑Nℕ+)⁻¹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`. ⊗ₜ[TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
]TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  1)TensorProduct.tmul.{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] (m : M) (n : N) : TensorProduct R M NThe canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  *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`.
        HurwitzRatHat.j₂HurwitzRatHat.j₂ : HurwitzHat →ₐ[ℤ] HurwitzRatHatThe inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k,
with 𝔸 the finite adeles of ℚ.  z'HurwitzHat

contains sorry in proof

Proof

Same as the proof for \Qhat.

It is not hard to check that \widehat{D} contains \widehat{\calO} and D as subrings, and that as additive abelian groups we have \widehat{\calO}\cap D=\calO and \widehat{\calO}+D=\widehat{D}. This is because \calO is just four copies of \Z and we've proved the analogous result for \Z.

However the multiplicative structure is more interesting, especially as D is not commutative. For a general quaternion algebra it is not true that (\widehat{D})^\times=D^\times(\widehat{\calO})^\times, because there are "class group obstructions". The double coset space is some kind of non-commutative analogue of a class group. However for our particular choice of D and \calO the result is true.

Theorem5.35

Group: The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (34)

Hover another entry in this group to preview it.

Preview

Definition 5.1

Blueprint label

ZHat

Group

The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.

⚠L∃∀Nused by 0

Lemma 5.34 The group of units of \widehat{D} is D^\times\calOhat^\times. More precisely, every element of \widehat{D}^\times can be written as a product \delta u with \delta\in D^\times and u\in\calOhat^\times.

Code for Theorem5.35●1 theorem, incomplete

theorem HurwitzRatHat.completed_units (zHurwitzRatHatˣ : HurwitzRatHatHurwitzRatHat : TypeThe "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module
generated by 1, i, j, and (1+i+j+k)/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`. ) :
  ∃ uHurwitzRatˣ vHurwitzHatˣ, ↑zHurwitzRatHatˣ =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`. HurwitzRatHat.j₁HurwitzRatHat.j₁ : HurwitzRat →ₐ[ℤ] HurwitzRatHatThe inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ.  ↑uHurwitzRatˣ *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`. HurwitzRatHat.j₂HurwitzRatHat.j₂ : HurwitzHat →ₐ[ℤ] HurwitzRatHatThe inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k,
with 𝔸 the finite adeles of ℚ.  ↑vHurwitzHatˣ

theorem HurwitzRatHat.completed_units
  (zHurwitzRatHatˣ : HurwitzRatHatHurwitzRatHat : TypeThe "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module
generated by 1, i, j, and (1+i+j+k)/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`. ) :
  ∃ uHurwitzRatˣ vHurwitzHatˣ,
    ↑zHurwitzRatHatˣ =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`.
      HurwitzRatHat.j₁HurwitzRatHat.j₁ : HurwitzRat →ₐ[ℤ] HurwitzRatHatThe inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ.  ↑uHurwitzRatˣ *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`.
        HurwitzRatHat.j₂HurwitzRatHat.j₂ : HurwitzHat →ₐ[ℤ] HurwitzRatHatThe inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k,
with 𝔸 the finite adeles of ℚ.  ↑vHurwitzHatˣ

contains sorry in proof

Proof

Given an element x of \widehat{D}^\times, we can use lemma HurwitzRatHat.canonicalForm to write it as z/N with N a positive integer and z\in\widehat{\calO}. Note that N is central and in D^\times. Similarly, we can write x^{-1} as y/M with M a positive integer and y\in\widehat{\calO}. Then 1=xx^{-1}=zy/NM and so zy=NM=MN, and 1=x^{-1}x=yz/MN so yz=MN too. In particular y both left and right divides a positive integer.

Now consider the left ideal \widehat{\calO}y generated by y. We've just seen that this ideal has nontrivial intersection with \calO, because it contains MN>0. Hence its intersection with \calO is a nonzero left ideal of \calO, which is hence principal by corollary Hurwitz.left_ideal_princ. Write it as \calO\alpha with 0\not=\alpha\in\calO.

It suffices to show that \calOhat\alpha=\calOhat y. For this would imply that u\alpha=y and vy=\alpha for some u,v\in\calOhat, and thus (vu-1)\alpha=0 and (uv-1)y=0, and both \alpha and y are left divisors of positive integers (the norm of \alpha, and MN respectively), so now using the fact that \calOhat is \Z-torsion-free (is the tensor product of torsion-free abelian groups torsion-free? That would be a cheap way of doing it. Otherwise use \calO=\Z^4) we deduce that u and v are units, and thus x^{-1}=\frac{1}{M}u\alpha so x=(M\alpha^{-1})v\in D^\times\calOhat^\times.

What remains is this. We have y\in\calOhat which left and right divides some positive integer. We've defined 0\not=\alpha\in\calO such that \calO\alpha is the pullback of the abelian group \calOhat y along the map \calO\to\calOhat. We need to show that when we push this ideal \calO\alpha forwards to \calOhat we get \calOhat y again. The fact that \calOhat\alpha\subseteq\calOhat y is easy, because \alpha\in\calOhat y by definition. So it remains to show that y\in\calOhat\alpha.

Let's define T to be a positive integer which is both a left and right multiple of both y and \alpha (for example T=MN\alpha\overline{\alpha} will do). Now note that we have an isomorphism \calO/T\calO=\calOhat/T\calOhat, so we can choose some \beta\in\calO such that \beta-y\in T\calOhat is a multiple of T. Next note that \beta\in y+\calOhat T\subset \calOhat y is in \calOhat y\cap\calO=\calO\alpha, meaning \beta=\gamma\alpha for some \gamma\in\calO. Hence y\in\beta+\calOhat T\subseteq\calOhat\alpha.