9. Miniproject: Adeles🔗

9.1. Status🔗

This is an active miniproject.

9.2. Goals🔗

There are several goals to this miniproject.

Define the adeles \A_K of a number field K and give them the structure of a K-algebra.
Prove that \A_K is a locally compact topological ring.
Base change: show that if L/K is a finite extension of number fields then the natural map L\otimes_K\A_K\to\A_L is an isomorphism, both algebraic and topological.
Prove that K \subseteq \A_K is a discrete subgroup and the quotient is compact.
Get this stuff into mathlib.

We briefly go through the basic definitions. Let K be a number field. Let \Zhat=\projlim_{N\geq1}(\Z/N\Z) be the profinite completion of \Z, equipped with the projective limit topology.

A cheap definition of the finite adeles \A_K^\infty of K is K\otimes_{\Z}\Zhat, equipped with the \Zhat-module topology.

A cheap definition of the infinite adeles K_\infty is K\otimes_{\Q}\R with the \R-module topology. This is a finite-dimensional \R-vector space, so this is just the usual topology on \R^n.

A cheap definition of the adeles of K is \A_K^\infty\times K_\infty with the product topology. This is a commutative topological ring.

However in the literature (and in mathlib) we see different definitions. The finite adeles of K are usually defined in the books as the so-called restricted product \prod'_{\mathfrak{p}}K_{\mathfrak{p}} over the completions K_{\mathfrak{p}} of K at all maximal ideals \mathfrak{p}\subseteq\mathcal{O}_K of the integers of K. Here the restricted product is the subset of \prod_{\mathfrak{p}}K_{\mathfrak{p}} consisting of elements which are in the integers \mathcal{O}_{K,\mathfrak{p}} of K_{\mathfrak{p}} for all but finitely many \mathfrak{p}. This is the definition given in mathlib. Mathlib also has the proof that they are a topological ring; furthermore the construction of the finite adeles in mathlib works for any Dedekind domain. The adeles are an arithmetic object, but the finite adeles are an algebraic object.

Similarly the infinite adeles of a number field K are usually defined as \prod_v K_v, the product running over the archimedean completions of K, and this is the mathlib definition.

The adeles of a number field K are the product of the finite and infinite adeles, and mathlib knows that they are a K-algebra and a topological ring.

9.3. Local compactness🔗

As mentioned above, Salvatore Mercuri was the first to give a complete formalization of the proof that the adele ring is locally compact as a topological space. His work proved the result using the ad hoc topology on the adeles which we initially had. Since then, adeles have been refactored to have the direct limit topology and mathlib has RestrictedProduct.locallyCompactSpace_of_addGroup, the result that a restricted product of topological additive groups K_v over compact open subgroups A_v is locally compact.

What we need then is this (note that this is not true for a general Dedekind domain):

Theorem9.3.1

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

If K is a number field and v is a nonzero prime ideal of the integers of K, then the integers of K_v is a compact open subgroup.

Lean code for Theorem9.3.1●1 theorem

theoremdefined in FLT/NumberField/Completion/Finite.lean

complete

theorem NumberField.instCompactSpaceAdicCompletionIntegers.{u_1} (K : Type u_1)
  [Field K] [NumberField K]
  (v :
    IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
  CompactSpace
    ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.instCompactSpaceAdicCompletionIntegers.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  (v :
    IsDedekindDomain.HeightOneSpectrum
      (NumberField.RingOfIntegers K)) :
  CompactSpace
    ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
        K v)

Proof for Theorem 9.3.1

uses 0

Openness should follow from the fact that the integers are \{x : v(x)<v(1/\pi)\} where \pi is a uniformizer. Compactness needs finiteness of the residue field \mathcal{O}_K/v.

Once we have this, the above result from mathlib gives us

Theorem9.3.2

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

The adeles of a number field are locally compact.

Lean code for Theorem9.3.2●1 theorem

theoremdefined in FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean

complete

theorem NumberField.AdeleRing.locallyCompactSpace.{u_1} {K : Type u_1} [Field K]
  [NumberField K] :
  LocallyCompactSpace
    (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)

theorem NumberField.AdeleRing.locallyCompactSpace.{u_1}
  {K : Type u_1} [Field K]
  [NumberField K] :
  LocallyCompactSpace
    (NumberField.AdeleRing
      (NumberField.RingOfIntegers K) K)

Proof for Theorem 9.3.2

uses 0

The adeles of a number field are a product of the finite adeles and the infinite adeles so it suffices to prove that the finite and infinite adeles are locally compact. The infinite adeles are just isomorphic to \R^n as a topological space, so they're certainly locally compact. As for the finite adeles, the mathlib theorem RestrictedProduct.locallyCompactSpace_of_addGroup says that a restricted product of locally compact additive groups with respect to open compact subgroups is locally compact, so this reduces us the previous result.

9.4. Base change🔗

The "theorem" we want is that if L/K is a finite extension of number fields, then \A_L = L \otimes_K \A_K. This isn't a theorem though, this is actually a definition (the map between the two objects) and a theorem about the definition (that it's an isomorphism).

In fact the full claim is that it is both a homeomorphism and an L-algebra isomorphism. Before we can prove the theorem, we need to make the definition.

Recall that the adeles \A_K of a number field is a product \A_K^\infty\times K_\infty of the finite adeles and the infinite adeles. So our "theorem" follows immediately from the "theorems" that \A_L^\infty=L\otimes_K\A_K^\infty and L_\infty=L\otimes_KK_\infty (both of these equalities mean an algebraic and topological isomorphism). We may thus treat the finite and infinite results separately.

9.4.1. Base Change For Nonarchimedean Completions🔗

As pointed out above, the theory of finite adeles works fine for Dedekind domains. So for the time being let A be a Dedekind domain. Recall that the height one spectrum of A is the nonzero prime ideals of A.

Note that because we stick to the literature, rather than to common sense, fields are Dedekind domains in mathlib, and the height one spectrum of a field is empty.

Lemma9.4.1.1

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 9.4.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

If i:K\to L denotes the inclusion then for k\in K we have e\times w(i(k))=v(k), where e is the ramification index of w/v (recall that valuations here are written additively, unlike in mathlib).

Lean code for Lemma9.4.1.1●1 theorem

theoremdefined in FLT/DedekindDomain/IntegralClosure.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.valuation_comap.{u_1, u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain B]
  [IsFractionRing B L] (w : IsDedekindDomain.HeightOneSpectrum B)
  (x : K) :
  (IsDedekindDomain.HeightOneSpectrum.valuation K
          (IsDedekindDomain.HeightOneSpectrum.under A w))
        x ^
      (IsDedekindDomain.HeightOneSpectrum.under A
              w).asIdeal.ramificationIdx
        w.asIdeal =
    (IsDedekindDomain.HeightOneSpectrum.valuation L w)
      ((algebraMap K L) x)

theorem IsDedekindDomain.HeightOneSpectrum.valuation_comap.{u_1,
    u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsDedekindDomain B]
  [IsFractionRing B L]
  (w :
    IsDedekindDomain.HeightOneSpectrum B)
  (x : K) :
  (IsDedekindDomain.HeightOneSpectrum.valuation
          K
          (IsDedekindDomain.HeightOneSpectrum.under
            A w))
        x ^
      (IsDedekindDomain.HeightOneSpectrum.under
              A w).asIdeal.ramificationIdx
        w.asIdeal =
    (IsDedekindDomain.HeightOneSpectrum.valuation
        L w)
      ((algebraMap K L) x)

If w | v then for x ∈ K we have w(x)=v(x)^e where e is the ramification index.

Proof for Lemma 9.4.1.1

uses 0

Standard (and formalized).

Definition9.4.1.2

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 4

Reverse dependency previews

Preview

Lemma 9.4.1.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

markupTeX✓L∃∀N

There's a natural ring map K_v\to L_w extending the map K\to L. It is defined by completing the inclusion K\to L at the finite places v and w (which can be done because the previous lemma shows that the map is uniformly continuous for the v-adic and w-adic topologies).

Lean code for Definition9.4.1.2●1 definition

defdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

def IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] {v : IsDedekindDomain.HeightOneSpectrum A}
  (w : IsDedekindDomain.HeightOneSpectrum.Extension B v) :
  IsDedekindDomain.HeightOneSpectrum.adicCompletion K
      v →ₛₐ[algebraMap K L]
    IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w

def IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  {v :
    IsDedekindDomain.HeightOneSpectrum A}
  (w :
    IsDedekindDomain.HeightOneSpectrum.Extension
      B v) :
  IsDedekindDomain.HeightOneSpectrum.adicCompletion
      K v →ₛₐ[algebraMap K L]
    IsDedekindDomain.HeightOneSpectrum.adicCompletion
      L ↑w

If w of L divides v of K, `underSemialgHom v w pf` is the canonical map
`Kᵥ → L_w` lying above `K → L`. Here we actually use the type synonyms `WithVal K` and `WithVal L`.

Lemma9.4.1.3

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Lemma 9.4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

If i_v:K_v\to L_w denotes the map of the previous definition then for x\in K_v we have e\times w(i(k))=v(k), where e is the ramification index of w/v.

Lean code for Lemma9.4.1.3●1 theorem

theoremdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] {v : IsDedekindDomain.HeightOneSpectrum A}
  (w : IsDedekindDomain.HeightOneSpectrum.Extension B v)
  (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) :
  Valued.v
      ((IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
          K L w)
        x) =
    Valued.v x ^
      (IsDedekindDomain.HeightOneSpectrum.under A
              ↑w).asIdeal.ramificationIdx
        (↑w).asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  {v :
    IsDedekindDomain.HeightOneSpectrum A}
  (w :
    IsDedekindDomain.HeightOneSpectrum.Extension
      B v)
  (x :
    IsDedekindDomain.HeightOneSpectrum.adicCompletion
      K v) :
  Valued.v
      ((IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
          K L w)
        x) =
    Valued.v x ^
      (IsDedekindDomain.HeightOneSpectrum.under
              A
              ↑w).asIdeal.ramificationIdx
        (↑w).asIdeal

The local ramification index for the extension L_w/K_v is equal to the global ramification
index for the extension w/v. In other words, if x in K_v and i:K_v->L_w then w(i(x))=v(x)^e
where e is computed globally.

Proof for Lemma 9.4.1.3

uses 0

Follows by continuity from lemma Lemma 9.4.1.1.

Lemma9.4.1.4

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

The map i_v:K_v\to L_w sends the integer ring A_v into B_w.

Lean code for Lemma9.4.1.4●1 theorem

theoremdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] {v : IsDedekindDomain.HeightOneSpectrum A}
  (w : IsDedekindDomain.HeightOneSpectrum.Extension B v) :
  ⇑(IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
          K L w) ''
      ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⊆
    ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)

theorem IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  {v :
    IsDedekindDomain.HeightOneSpectrum A}
  (w :
    IsDedekindDomain.HeightOneSpectrum.Extension
      B v) :
  ⇑(IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
          K L w) ''
      ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
          K v) ⊆
    ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
        L ↑w)

The canonical map K_v → L_w sends 𝓞_v to 𝓞_w.

Proof for Lemma 9.4.1.4

uses 0

The integer ring is defined by v\geq0 (or v\leq 1 in mathlib, which uses multiplicative valuations) so the result follows from Lemma 9.4.1.3.

Theorem9.4.1.5

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

Giving L_w the K_v-algebra structure coming from the natural map K_v\to L_w, the w-adic topology on L_w is the K_v-module topology.

Lean code for Theorem9.4.1.5●1 theorem

theoremdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] (v : IsDedekindDomain.HeightOneSpectrum A)
  [FiniteDimensional K L]
  (w : IsDedekindDomain.HeightOneSpectrum.Extension B v) :
  IsModuleTopology
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  (v :
    IsDedekindDomain.HeightOneSpectrum A)
  [FiniteDimensional K L]
  (w :
    IsDedekindDomain.HeightOneSpectrum.Extension
      B v) :
  IsModuleTopology
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion
      K v)
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion
      L ↑w)

L_w has the K_v-module topology.

Proof for Theorem 9.4.1.5

uses 0

Any basis for L as a K-vector space spans L_w as a K_v-module, so L_w is finite-dimensional over K_v and the module topology is the same as the product topology. So we need to establish that the product topology on L_w=K_v^n is the w-adic topology. But the w-adic topology is induced by the w-adic norm, which makes L_w into a normed K_v-vector space, and (after picking a basis) the product norm on L_w=K_v^n also makes L_w into a normed K_v-vector space. So the result follows from the standard fact (see for example the lemma on p52 of Cassels-Froelich, formalized as ContinuousLinearEquiv.ofFinrankEq in mathlib) that any two norms on a finite-dimensional vector space over a complete field are equivalent (and thus induce the same topology).

we can view L_w as an L\otimes_KK_v-algebra.

Now instead of fixing w upstairs, we fix v downstairs and consider all w lying over it at once. So say v is in the height one spectrum of A.

Lemma9.4.1.6

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

There are only finitely many primes w of B lying above v.

Lean code for Lemma9.4.1.6●1 theorem

theoremdefined in FLT/DedekindDomain/IntegralClosure.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.Extension.finite.{u_1, u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain B]
  (v : IsDedekindDomain.HeightOneSpectrum A) :
  Finite (IsDedekindDomain.HeightOneSpectrum.Extension B v)

theorem IsDedekindDomain.HeightOneSpectrum.Extension.finite.{u_1,
    u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsDedekindDomain B]
  (v :
    IsDedekindDomain.HeightOneSpectrum
      A) :
  Finite
    (IsDedekindDomain.HeightOneSpectrum.Extension
      B v)

There are only finitely many nonzero primes of B above a nonzero prime of A.

Proof for Lemma 9.4.1.6

uses 0

This is a standard fact about Dedekind domains. The key input is mathlib's theorem primesOver_finite.

We write w|v to denote the fact that w is a prime of B above v of A.

Definition9.4.1.7

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1markupTeX✓L∃∀N

The product of the maps K_v\to L_w for w|v is a natural ring map K_v\to\prod_{w|v}L_w lying over K\to L.

Lean code for Definition9.4.1.7●1 definition

defdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] (v : IsDedekindDomain.HeightOneSpectrum A) :
  IsDedekindDomain.HeightOneSpectrum.adicCompletion K
      v →ₛₐ[algebraMap K L]
    (w : IsDedekindDomain.HeightOneSpectrum.Extension B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  (v :
    IsDedekindDomain.HeightOneSpectrum
      A) :
  IsDedekindDomain.HeightOneSpectrum.adicCompletion
      K v →ₛₐ[algebraMap K L]
    (w :
        IsDedekindDomain.HeightOneSpectrum.Extension
          B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion
        L ↑w

The canonical map `K_v → ∏_{w|v} L_w` extending K → L.

Because K_v\to\prod_{w|v}L_w lies over K\to L, there's an induced L-algebra map L\otimes_KK_v\to\prod_{w|v}L_w. We are now able to state one of the key results in this section. The proof is probably the hardest proof in this section to formalize.

Theorem9.4.1.8

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Lemma 9.4.1.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

The induced L-algebra homomorphism L\otimes_KK_v\to\prod_{w|v}L_w is an isomorphism of rings.

Lean code for Theorem9.4.1.8●1 definition

defdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] [FiniteDimensional K L] [Module.Finite A B]
  (v : IsDedekindDomain.HeightOneSpectrum A) :
  TensorProduct K L
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[L]
    (w : IsDedekindDomain.HeightOneSpectrum.Extension B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  [FiniteDimensional K L]
  [Module.Finite A B]
  (v :
    IsDedekindDomain.HeightOneSpectrum
      A) :
  TensorProduct K L
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion
        K v) ≃ₐ[L]
    (w :
        IsDedekindDomain.HeightOneSpectrum.Extension
          B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion
        L ↑w

The L-algebra isomorphism `L ⊗[K] K_v ≅ ∏_{w|v} L_w`.

Proof for Theorem 9.4.1.8

uses 0

My current proposal to formalize this is as follows. The map is surjective because the image is dense and closed; this has been formalized already. It is also a K_v-algebra homomorphism if we give L_w the obvious K_v-algebra structure. Thus we can conclude the result if we can prove that both spaces are finite-dimensional and have the same dimension. The K_v-dimension of L⊗_KK_v is equal to the K-dimension of L, which is ∑_{w|v} e_w f_w using the standard notation that e_w is the ramification index of w and f_w the residue degree. So it suffices to prove that [L_w:K_v]=e_wf_w. We already have that e_w (defined globally) is equal to the local ramification index (defined as the factor by which the valuations differ on K). So what is left is to prove that (i) the residue field extension induced by L_w/K_v has degree is equal to the globally-defined f_w, (ii) an extension of local fields has degree ef. Now (i) sounds straightforward given what we have (the map from A to \mathcal{O}_v has kernel v and dense image) and (ii) is true for any complete discretely-valued field; I am not suggesting we formalize the following proof, but at least it represents a rigorous justification: A field complete with respect to a discrete valuation is stable in the sense of the book by Bosch-Guntzer-Remmert (Prop 3.6.2.1), so every finite extension of such a field is cartesian (def 3.6.1.1) and thus ef=n (Prop 3.6.2.4, (iii) implies (ii)). Note that if you weaken the hypotheses too much then there are counterexamples; it's possible to have ef<n and BGR goes into details.

Theorem9.4.1.9

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

For v fixed, the product topology on \prod_{w|v}L_w is the K_v-module topology.

Lean code for Theorem9.4.1.9●1 theorem

theoremdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPi.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] (v : IsDedekindDomain.HeightOneSpectrum A)
  [FiniteDimensional K L] :
  IsModuleTopology
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
    ((w : IsDedekindDomain.HeightOneSpectrum.Extension B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPi.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  (v :
    IsDedekindDomain.HeightOneSpectrum A)
  [FiniteDimensional K L] :
  IsModuleTopology
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion
      K v)
    ((w :
        IsDedekindDomain.HeightOneSpectrum.Extension
          B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion
        L ↑w)

∏_{w|v} L_w has the K_v-module topology.

Proof for Theorem 9.4.1.9

uses 0

This is a finite product of K_v-modules each of which has the K_v-module topology by Theorem 9.4.1.5, and the product topology is the module topology for a finite product of modules each of which has the module topology.

Theorem9.4.1.10

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

If we give L\otimes_KK_v the K_v-module topology, then the L-algebra isomorphism L\otimes_K K_v\cong\prod_{w|v}L_w is also a homeomorphism.

Lean code for Theorem9.4.1.10●1 definition

defdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquiv.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] [FiniteDimensional K L] [Module.Finite A B]
  (v : IsDedekindDomain.HeightOneSpectrum A) :
  TensorProduct K L
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃A[L]
    (w : IsDedekindDomain.HeightOneSpectrum.Extension B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquiv.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  [FiniteDimensional K L]
  [Module.Finite A B]
  (v :
    IsDedekindDomain.HeightOneSpectrum
      A) :
  TensorProduct K L
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion
        K v) ≃A[L]
    (w :
        IsDedekindDomain.HeightOneSpectrum.Extension
          B v) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion
        L ↑w

The continuous L-algebra isomorphism `L ⊗[K] K_v ≅ ∏_{w|v} L_w`.

Proof for Theorem 9.4.1.10

uses 0

Indeed, it is a K_v-algebra isomorphism between two modules each of which have the module topology, and any module map is automorphically continuous for the module topologies.

Theorem9.4.1.11

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 9.4.1.16

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The isomorphism L\otimes_KK_v\to\prod_{w|v}L_w induces an isomorphism B\otimes_AA_v\to \prod_{w|v}B_w for all v in the height one spectrum of A.

Lean code for Theorem9.4.1.11●1 theorem

theoremdefined in FLT/DedekindDomain/Completion/BaseChange.lean

complete

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv_bijOn.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsFractionRing B L]
  [IsDedekindDomain B] [FiniteDimensional K L] [Module.Finite A B]
  (v : IsDedekindDomain.HeightOneSpectrum A) :
  Set.BijOn
    (⇑(IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv
        K L B v))
    (Set.range
      ⇑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe
          K B v))
    ↑(Submodule.pi Set.univ fun w ↦
        IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule
          L ↑w)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv_bijOn.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} (K : Type u_2)
  (L : Type u_3) {B : Type u_4}
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Algebra.IsIntegral A B]
  [IsFractionRing B L]
  [IsDedekindDomain B]
  [FiniteDimensional K L]
  [Module.Finite A B]
  (v :
    IsDedekindDomain.HeightOneSpectrum
      A) :
  Set.BijOn
    (⇑(IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv
        K L B v))
    (Set.range
      ⇑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe
          K B v))
    ↑(Submodule.pi Set.univ fun w ↦
        IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule
          L ↑w)

Proof for Theorem 9.4.1.11

uses 0

Certainly the image of the integral elements are integral. The argument in the other direction is more delicate. My original plan was to follow Cassels--Froehlich, Cassels' article Global fields, section 12 lemma, p61, which proves it for all but finitely many primes, but a PR by Matthew Jasper gives another approach which works for all primes. Jasper's argument is to show that the closure of A in K_v is A_v for a valuation on a Dedekind domain, and then that the closure of A in \prod_{v \in S} K_v is \prod_{v \in S} A_v for S a finite set of valuations (using the Chinese remainder theorem). Applying this to B we get that the closure of B in \prod_{w \mid v} L_w is \prod_{w \mid v} B_w. He then shows that this closure is the image of B \otimes_A \mathcal{O}_v by showing that this image is closed because it's open), giving surjectivity; injectivity follows from the statement that L \otimes_K K_v = \prod_{w \mid v} L_w.

A summary of what we have so far: for all finite places v of A we have shown that the natural map L \otimes_K K_v \to \prod_w L_w is an isomorphism of L-algebras, and that if L \otimes_K K_v has the K_v-module topology and each L_w has the valuation topology then this map is also a homeomorphism. Furthermore we have shown that there is an induced algebraic isomorphism B \otimes_A A_v \cong \prod_w B_w on the subrings of the left and right hand sides.

Recall that the finite adeles \A_{A,K}^\infty is defined in mathlib to be the restricted product of the K_v with respect to the A_v, equipped with a certain restricted product topology (which is not the subspace topology of the product topology, indeed \prod_v A_v is open in this topology). We have seen in definition Definition 9.4.1.2 that there's a map K_v\to L_w if w|v, extending K\to L, and we have seen in theorem Lemma 9.4.1.4 that this sends A_v to B_w. We conclude

Definition9.4.1.12

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 9.4.1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

There's a natural ring homomorphism \A_{A,K}^\infty\to\A_{B,L}^\infty lying over K\to L.

Lean code for Definition9.4.1.12●1 definition

defdefined in FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

complete

def IsDedekindDomain.FiniteAdeleRing.mapSemialgHom.{u_1, u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Module.Finite A B] [IsDedekindDomain B]
  [IsFractionRing B L] :
  IsDedekindDomain.FiniteAdeleRing A K →SA[algebraMap K L]
    IsDedekindDomain.FiniteAdeleRing B L

def IsDedekindDomain.FiniteAdeleRing.mapSemialgHom.{u_1,
    u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Module.Finite A B] [IsDedekindDomain B]
  [IsFractionRing B L] :
  IsDedekindDomain.FiniteAdeleRing A
      K →SA[algebraMap K L]
    IsDedekindDomain.FiniteAdeleRing B L

The ring homomorphism `𝔸_K^∞ → 𝔸_L^∞` for `L/K` an extension of number fields,
as a morphism lying over the canonical map `K → L`.

Hence there is a natural L-algebra homomorphism L \otimes_K \A_{A,K}^\infty \to \A_{B,L}^\infty.

We start with the following observation. If M is a K-module then there's a canonical map B\otimes_A M\to L\otimes_K M sending b\otimes m to b\otimes m by the universal property of the tensor product. Our first goal is to show that this map is an isomorphism, so let us establish some lemmas first.

Lemma9.4.1.13

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 2

Reverse dependency previews

Preview

Corollary 9.4.1.14

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

markupTeXXL∃∀N

If 0\not=b\in B then there exists 0\not=a\in A such that b divides the image of a in B.

Proof for Lemma 9.4.1.13

uses 0

Let a=N_{L/K}(b), the norm. This is known to take nonzero elements of L to nonzero elements of K because the norm is the determinant of an invertible linear map, and integral elements to integral elements. Furthermore a/b\in L is the product of the conjugates of b in some normal closure of L, and hence it is integral, so it lies in B.

Corollary9.4.1.14

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0markupTeXXL∃∀N

The A-bilinear map B\times K\to L sending (b,k) to bk is surjective.

Proof for Corollary 9.4.1.14

uses 0

Given \lambda\in L, write it as n/d with 0\not=d\in B. Choose 0\not=a\in A and b\in B with db=a, and then note that \lambda=nb\times a^{-1}.

Corollary9.4.1.15

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0markupTeXXL∃∀N

The natural map B\otimes_AK\to L is a B-algebra isomorphism.

Proof for Corollary 9.4.1.15

uses 0

We write down an inverse. Regard B\otimes_AK as a B-algebra via the action on the left. Note that at this point it's not even clear that B\otimes_AK is a field. We have the structure map B\to B\otimes_AK sending b to b\otimes1, which is B-linear. I claim that every nonzero element of B gets sent to an invertible element of B\otimes_AK. Indeed, if b\not=0 and, using the previous lemma, we choose 0\not=a\in A such that bb'=a, then (b\otimes1)(b'\otimes\frac1a)=1. Thus by the universal property of localization, the B-linear map B\to B\otimes_AK extends to a ring homomorphism from the field of fractions of B to B\otimes_AK, which we claim is our desired inverse. Checking that both composites are the identity should be straightforward. Starting with B\otimes_AK we only have to check on elements of the form b\otimes k; starting with L we only have to check on elements of B. Hopefully both are straightforward.

Our next goal in this section is the following two results. First the algebraic claim.

Theorem9.4.1.16

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Theorem 9.4.1.11

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 4.2.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The natural map L \otimes_K \A_{A,K}^\infty \to \A_{B,L}^\infty is an isomorphism.

Lean code for Theorem9.4.1.16●1 definition

defdefined in FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

complete

def IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv.{u_1, u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Module.Finite A B] [IsDedekindDomain B]
  [IsFractionRing B L]
  [Algebra (IsDedekindDomain.FiniteAdeleRing A K)
      (IsDedekindDomain.FiniteAdeleRing B L)]
  [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul A K L B]
  [FiniteDimensional K L] :
  TensorProduct K L (IsDedekindDomain.FiniteAdeleRing A K) ≃ₐ[L]
    IsDedekindDomain.FiniteAdeleRing B L

def IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv.{u_1,
    u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Module.Finite A B] [IsDedekindDomain B]
  [IsFractionRing B L]
  [Algebra
      (IsDedekindDomain.FiniteAdeleRing A
        K)
      (IsDedekindDomain.FiniteAdeleRing B
        L)]
  [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul
      A K L B]
  [FiniteDimensional K L] :
  TensorProduct K L
      (IsDedekindDomain.FiniteAdeleRing A
        K) ≃ₐ[L]
    IsDedekindDomain.FiniteAdeleRing B L

The `L`-algebra isomorphism `L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞`.

Corollary9.4.1.17

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

If M is any K-module then the canonical map B \otimes_A M \to L \otimes_K M is an isomorphism.

Lean code for Corollary9.4.1.17●1 definition

defdefined in FLT/DedekindDomain/IntegralClosure.lean

complete

def IsDedekindDomain.linearEquivTensorProductModule.{u_1, u_2, u_3, u_4,
    u_5}
  (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [IsIntegralClosure B A L]
  [Algebra.IsAlgebraic K L] (M : Type u_5) [AddCommGroup M] [Module K M]
  [Module A M] [IsScalarTower A K M] :
  TensorProduct K L M ≃ₗ[A] TensorProduct A B M

def IsDedekindDomain.linearEquivTensorProductModule.{u_1,
    u_2, u_3, u_4, u_5}
  (A : Type u_1) (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [IsIntegralClosure B A L]
  [Algebra.IsAlgebraic K L] (M : Type u_5)
  [AddCommGroup M] [Module K M]
  [Module A M] [IsScalarTower A K M] :
  TensorProduct K L M ≃ₗ[A]
    TensorProduct A B M

The canonical `A`-linear isomorphism `L ⊗ M ≅ B ⊗ M` for any `K`-module `M`.

Proof for Corollary 9.4.1.17

uses 0

We can factor this map as B\otimes_AM\cong B\otimes_A(K\otimes_KM)\cong (B\otimes_A K)\cong_KM\to L\otimes_KM, and we just showed that the latter map was an isomorphism.

The reason we care about this is the following.

Theorem9.4.1.18

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1XL∃∀N

B is a finitely presented A-module.

Proof for Theorem 9.4.1.18

uses 0

A is Noetherian as it is a Dedekind domain, so it suffices to prove that B is finitely generated as an A-module. But this is in mathlib already: a proof is around line 101 of BaseChange.lean in FLT at the time of writing.

Theorem9.4.1.19

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1XL∃∀N

If R is a commutative ring, if M is a finitely presented R-module and if N_i are a collection of R-modules, then the canonical map M \otimes_R \prod_i N_i \to \prod_i (M \otimes_R N_i) is an isomorphism.

Proof for Theorem 9.4.1.19

uses 0

If M is finite and free then Maddy Crim has already formalized this in FLT. For the general case present M as R^a \to R^b \to M \to 0 and use that tensor products and arbitrary products preserve surjections.

Definition9.4.1.20

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 9.4.1.16

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

XL∃∀N

Let V and W be index sets, and let f:W→V be a map with finite fibres. Let X_v be sets, with subsets C_v, let Y_w be sets with subsets D_w, and say for all v ∈ V we're given a bijection X_v \to \prod_{w \mid f(w)=v} Y_w, identifying C_v with \prod_{w:f(w)=v} D_w. Then there's an induced bijection between the restricted products ∏'_v(X_v,C_v) and ∏'_w(Y_w,D_w).

Proof for Definition 9.4.1.20

uses 0

Let V be the finite places of K and W the finite places of L, let X_v be B \otimes_A K_v, let C_v be B \otimes_A A_v, let Y_w be L_w, let D_w be B_w, and the result follows from the previous definition, given theorem Theorem 9.4.1.11.

Theorem9.4.1.21

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0XL∃∀N

In the same setup as Definition 9.4.1.20 (V, W index sets, f : W → V, C_v ⊆ X_v and D_w ⊆ Y_w, bijections b_v : X_v → ∏_{w | f(w) = v} Y_w identifying C_v with ∏_{w | f(w) = v} D_w), if all the X_v and Y_w are furthermore topological spaces, all the C_v and D_w are open, and all the b_v are homeomorphisms, then the induced map ∏'_v(X_v,C_v) → ∏'_w(Y_w,D_w) is also a homeomorphism.

Proof for Theorem 9.4.1.21

uses 0

I have only thought about the cofinite filter case, where this should follow easily from the definition of the topology.

Corollary9.4.1.22

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 9.4.1.18

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1XL∃∀N

If S is a finite set of nonzero primes of A then the natural map B\otimes((\prod_{v\in S}K_v)\times(\prod_{v\notin S}A_v))\to (\prod_{v\in S}(B\otimes_AK_v))\times(\prod_{v\notin S}(B\otimes_AA_v)) is an isomorphism.

Proof for Corollary 9.4.1.22

uses 0

Follows from the previous two theorems.

Recall that \A_K^\infty is the finite adeles of K, defined as the restricted product of the K_v with respect to the A_v, where v runs through the nonzero primes of A. Let R denote the restricted product of the B\otimes_A K_v with respect to the B\otimes_A A_v.

Corollary9.4.1.23

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1XL∃∀N

The natural map B\otimes_A\A_K^\infty\to R is a B-algebra isomorphism.

Proof for Corollary 9.4.1.23

uses 0

This follows from the previous corollary and the fact that tensor products commute with filtered colimits.

Corollary9.4.1.24

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1XL∃∀N

The ring R introduced above, the restricted product of the B\otimes_A K_v with respect to the B\otimes_A A_v, is isomorphic to \mathbb{A}_L.

Proof for Corollary 9.4.1.24

uses 0

Let V be the finite places of K and W the finite places of L, let X_v be B\otimes_A K_v, let C_v be B\otimes_A A_v, let Y_w be L_w, let D_w be B_w, and the result follows from the previous definition, given theorem Theorem 9.4.1.11.

From this, we can deduce the theorem we claimed earlier:

Theorem9.4.1.25

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 9.4.1.20

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1XL∃∀N

The natural map B \otimes_A \A_K^\infty \to \A_L^\infty is a B-algebra isomorphism.

Proof for Theorem 9.4.1.25

uses 0

This map factors through the auxiliary ring~R so the result follows from the previous two constructions.

Because this map factors through the isomorphism B\otimes_A\A_K^\infty\to L\otimes_K\A_K^\infty we can finally deduce that the natural map L\otimes_K\A_K^\infty\to\A_L^\infty is an algebraic isomorphism.

Proof for Theorem 9.4.1.16

uses 0

Follows immediately from theorem Theorem 9.4.1.25 and theorem Corollary 9.4.1.17.

Now L \otimes_K \A_{A,K}^\infty is an \A_{A,K}^\infty-module and hence can be given the \A_{A,K}^\infty-module topology. We also claim

Theorem9.4.1.26

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

The induced L-algebra morphism L \otimes_K \A_{A,K}^\infty \to \A_{B,L}^\infty is a topological isomorphism.

Lean code for Theorem9.4.1.26●1 definition

defdefined in FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

complete

def IsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv.{u_1, u_2,
    u_3, u_4}
  (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Module.Finite A B] [IsDedekindDomain B]
  [IsFractionRing B L]
  [Algebra (IsDedekindDomain.FiniteAdeleRing A K)
      (IsDedekindDomain.FiniteAdeleRing B L)]
  [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul A K L B]
  [FiniteDimensional K L] :
  TensorProduct K L (IsDedekindDomain.FiniteAdeleRing A K) ≃A[L]
    IsDedekindDomain.FiniteAdeleRing B L

def IsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv.{u_1,
    u_2, u_3, u_4}
  (A : Type u_1) (K : Type u_2)
  (L : Type u_3) (B : Type u_4)
  [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K]
  [IsFractionRing A K] [Algebra B L]
  [IsDedekindDomain A] [Algebra K L]
  [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L]
  [Module.Finite A B] [IsDedekindDomain B]
  [IsFractionRing B L]
  [Algebra
      (IsDedekindDomain.FiniteAdeleRing A
        K)
      (IsDedekindDomain.FiniteAdeleRing B
        L)]
  [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul
      A K L B]
  [FiniteDimensional K L] :
  TensorProduct K L
      (IsDedekindDomain.FiniteAdeleRing A
        K) ≃A[L]
    IsDedekindDomain.FiniteAdeleRing B L

The continuous `L`-algebra isomorphism `L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞`

Informally, the proofs are simple: componentwise we know that L \otimes_K K_v is isomorphic both algebraically and topologically to \prod_{w \mid v} L_w, and that this isomorphism sends the open set B \otimes_A A_v homeomorphically onto \prod_{w \mid v} B_w, so now it's "just a case of putting everything together". Formally, we really need to spell this out, as there is a lot going on. We do this in the next subsection.

Corollary9.4.1.27

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0XL∃∀N

\mathbb{\A_L^\infty} is homeomorphic to \prod_v(B\otimes_AK_v,B\otimes_AA_v).

Proof for Corollary 9.4.1.27

uses 0

Follows from the previous theorem with X_v=B\otimes_AK_v, D_w=L_w, etc.

Theorem9.4.1.28

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Let S be a set of infinite places of K. The image of K under the embedding K \hookrightarrow (K_v)_{v \in S}, k \mapsto (k)_v, is dense in the product topology.

Lean code for Theorem9.4.1.28●1 theorem

theoremdefined in FLT/NumberField/Completion/Infinite.lean

complete

theorem NumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi.{u_1}
  (K : Type u_1) [Field K] (p : NumberField.InfinitePlace K → Prop)
  [NumberField K] :
  DenseRange ⇑(algebraMap K ((v : Subtype p) → (↑v).Completion))

theorem NumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi.{u_1}
  (K : Type u_1) [Field K]
  (p : NumberField.InfinitePlace K → Prop)
  [NumberField K] :
  DenseRange
    ⇑(algebraMap K
        ((v : Subtype p) →
          (↑v).Completion))

Proof for Theorem 9.4.1.28

uses 0

Let (K, v) denote K equipped with the topology induced by the infinite place v. It suffices to show that the image of K under the embedding K \hookrightarrow \prod_{v \mid \infty} (K, v) is dense in the product topology. By a standard analytic argument, for each v it is possible to select a sequence (x_n^{(v)})_n with the property that x_n^{(v)} \to 1 in v's topology, while x_n^{(v)} \to 0 in any other infinite place's topology. Let (z_v)_v \in \prod_{v \mid \infty} (K, v). For each v, the sequence y_n := \sum_{v \mid \infty} x_n^{(v)} z_v in K converges to z_v in v's topology, so the embedded image of y_n converges to (z_v)_v in the product topology.

Theorem9.4.1.29

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

For a fixed infinite place v of K, we have \dim_{K_v} \prod_{w \mid v} L_w = \dim_{K_v} L \otimes_K K_v.

Lean code for Theorem9.4.1.29●1 theorem

theoremdefined in FLT/NumberField/Completion/Infinite.lean

complete

theorem NumberField.InfinitePlace.Completion.finrank_pi_eq_finrank_tensorProduct.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField L] [NumberField K] :
  Module.finrank v.Completion
      ((w : NumberField.InfinitePlace.Extension L v) →
        (↑w).Completion) =
    Module.finrank v.Completion (TensorProduct K L v.Completion)

theorem NumberField.InfinitePlace.Completion.finrank_pi_eq_finrank_tensorProduct.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  [NumberField L] [NumberField K] :
  Module.finrank v.Completion
      ((w :
          NumberField.InfinitePlace.Extension
            L v) →
        (↑w).Completion) =
    Module.finrank v.Completion
      (TensorProduct K L v.Completion)

Definition9.4.1.30

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Let v be an infinite place of K. There is a continuous K-algebra homomorphism K_v \to \prod_{w \mid v} L_w, whose restriction to K corresponds to the global embedding of K into (L_w)_w.

Lean code for Definition9.4.1.30●1 definition

defdefined in FLT/NumberField/Completion/Infinite.lean

complete

def NumberField.InfinitePlace.Completion.piExtension.{u_1, u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) :
  v.Completion →ₛₐ[algebraMap K L]
    (wv : NumberField.InfinitePlace.Extension L v) → (↑wv).Completion

def NumberField.InfinitePlace.Completion.piExtension.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) :
  v.Completion →ₛₐ[algebraMap K L]
    (wv :
        NumberField.InfinitePlace.Extension
          L v) →
      (↑wv).Completion

The map from `v.Completion` to the product of all completions of `L` lying above `v`.

Definition9.4.1.31

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

Let v be an infinite place of K. There is a natural L-algebra homomorphism L \otimes_K K_v \to \prod_{w \mid v} L_w, whose restriction to 1 \otimes_K K_v corresponds to the map in NumberField.InfinitePlace.Completion.piExtension.

Lean code for Definition9.4.1.31●1 definition

abbrevdefined in FLT/NumberField/Completion/Infinite.lean

complete

abbrev NumberField.InfinitePlace.Completion.baseChange.{u_1, u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) :
  TensorProduct K L v.Completion →ₐ[L]
    (wv : NumberField.InfinitePlace.Extension L v) → (↑wv).Completion

abbrev NumberField.InfinitePlace.Completion.baseChange.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) :
  TensorProduct K L v.Completion →ₐ[L]
    (wv :
        NumberField.InfinitePlace.Extension
          L v) →
      (↑wv).Completion

The `L`-algebra map `L ⊗[K] v.Completion` to the product of all completions of `L` lying
above `v`, induced by `piExtension`.

A map in Definition 9.4.1.30 can be lifted to an L-algebra homomorphism defined on L \otimes_K K_v.

Theorem9.4.1.32

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

For a fixed infinite place v of K, the local infinite-place base-change map L \otimes_K K_v \to \prod_{w \mid v} L_w is surjective.

Lean code for Theorem9.4.1.32●1 theorem

theoremdefined in FLT/NumberField/Completion/Infinite.lean

complete

theorem NumberField.InfinitePlace.Completion.baseChange_surjective.{u_1, u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField L] :
  Function.Surjective
    ⇑(NumberField.InfinitePlace.Completion.baseChange L v)

theorem NumberField.InfinitePlace.Completion.baseChange_surjective.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  [NumberField L] :
  Function.Surjective
    ⇑(NumberField.InfinitePlace.Completion.baseChange
        L v)

Proof for Theorem 9.4.1.32

uses 0

Let (x_i)_i be a K_v-basis of \prod_{w \mid v} L_w. By the density of L in \prod_{w \mid v} L_w from Theorem 9.4.1.28, we can find \alpha_i \in L arbitrarily close to x_i with respect to the sup norm when embedded globally in \prod_{w \mid v} L_w. In particular, it is possible to choose such \alpha_i so that the matrix representing the vector ((\alpha_i)_{w \mid v})_i in the basis (x_i)_i has nonzero determinant. Since (\alpha_i)_{w \mid v} is the image of 1 \otimes \alpha_i under base change, we have that (1 \otimes \alpha_i)_i also forms a basis of L \otimes_K K_v, and base change is surjective.

Theorem9.4.1.33

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

For a fixed infinite place v of K, the local infinite-place base-change map L \otimes_K K_v \to \prod_{w \mid v} L_w is injective.

Lean code for Theorem9.4.1.33●1 theorem

theoremdefined in FLT/NumberField/Completion/Infinite.lean

complete

theorem NumberField.InfinitePlace.Completion.baseChange_injective.{u_1, u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField L] [NumberField K] :
  Function.Injective
    ⇑(NumberField.InfinitePlace.Completion.baseChange L v)

theorem NumberField.InfinitePlace.Completion.baseChange_injective.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  [NumberField L] [NumberField K] :
  Function.Injective
    ⇑(NumberField.InfinitePlace.Completion.baseChange
        L v)

Proof for Theorem 9.4.1.33

uses 0

The L-algebra map L \otimes_K K_v \to \prod_{w \mid v} L_w can equivalently be thought of as K_v-linear, which is injective, because it is surjective by theorem Theorem 9.4.1.32, and both sides have the same K_v-dimension by theorem Theorem 9.4.1.29.

Theorem9.4.1.34

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

If w \mid v is an infinite place of L lying above an infinite place v of K, then L_w has the K_v-module topology.

Lean code for Theorem9.4.1.34●1 theorem

theoremdefined in FLT/NumberField/Completion/Infinite.lean

complete

theorem NumberField.InfinitePlace.Completion.instIsModuleTopologyValEqComapAlgebraMap_fLT.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  {wv : NumberField.InfinitePlace.Extension L v} :
  IsModuleTopology v.Completion (↑wv).Completion

theorem NumberField.InfinitePlace.Completion.instIsModuleTopologyValEqComapAlgebraMap_fLT.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  {wv :
    NumberField.InfinitePlace.Extension L
      v} :
  IsModuleTopology v.Completion
    (↑wv).Completion

Proof for Theorem 9.4.1.34

uses 0

Because L_w is a finite-dimensional normed K_v-vector space, there exists a K_v-linear homeomorphism L_w \cong K_v^n, from which L_w has the K_v-module topology.

Theorem9.4.1.35

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Definition 9.4.1.31

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 9.4.1.36

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Let v be an infinite place of K. There is a natural L-algebra homeomorphism L \otimes_K K_v \cong \prod_{w \mid v} L_w, whose restriction to 1 \otimes_K K_v corresponds to the map in Definition 9.4.1.30.

Lean code for Theorem9.4.1.35●1 definition

defdefined in FLT/NumberField/Completion/Infinite.lean

complete

def NumberField.InfinitePlace.Completion.baseChangeEquiv.{u_1, u_2}
  {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField L] [NumberField K] :
  TensorProduct K L v.Completion ≃A[L]
    (wv : NumberField.InfinitePlace.Extension L v) → (↑wv).Completion

def NumberField.InfinitePlace.Completion.baseChangeEquiv.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  [NumberField L] [NumberField K] :
  TensorProduct K L v.Completion ≃A[L]
    (wv :
        NumberField.InfinitePlace.Extension
          L v) →
      (↑wv).Completion

The `L`-algebra homeomorphism between `L ⊗[K] v.Completion` and the product of all completions
of `L` lying above `v`.

Proof for Theorem 9.4.1.35

uses 0

The map in Definition 9.4.1.31 is an L-algebra isomorphism by the surjectivity theorem Theorem 9.4.1.32 and the injectivity theorem Theorem 9.4.1.33. Every K_v-algebra isomorphism between two K_v-module topological spaces is a homeomorphism. Since the L-algebra isomorphism of Definition 9.4.1.31 can equivalently be viewed as a K_v-algebra isomorphism, it is also a homeomorphism.

Theorem9.4.1.36

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

Let v be an infinite place of K. There is a natural K_v-linear homeomorphism K_v^{[L:K]} \cong \prod_{w \mid v} L_w.

Lean code for Theorem9.4.1.36●1 definition

defdefined in FLT/NumberField/Completion/Infinite.lean

complete

def NumberField.InfinitePlace.Completion.piEquiv.{u_1, u_2} {K : Type u_1}
  (L : Type u_2) [Field K] [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField L] [NumberField K] :
  (Fin (Module.finrank K L) → v.Completion) ≃L[v.Completion]
    (wv : NumberField.InfinitePlace.Extension L v) → (↑wv).Completion

def NumberField.InfinitePlace.Completion.piEquiv.{u_1,
    u_2}
  {K : Type u_1} (L : Type u_2) [Field K]
  [Field L] [Algebra K L]
  (v : NumberField.InfinitePlace K)
  [NumberField L] [NumberField K] :
  (Fin (Module.finrank K L) →
      v.Completion) ≃L[v.Completion]
    (wv :
        NumberField.InfinitePlace.Extension
          L v) →
      (↑wv).Completion

The `Kᵥ`-linear homeomorphism between `Kᵥ^d` and the product of all completions
of `L` lying above `v`, where `d = [K : L]`.

Proof for Theorem 9.4.1.36

uses 0

Compose the K_v-linear isomorphism K_v^{[L:K]} \cong \prod_{w \mid v} L_w with theorem Theorem 9.4.1.35 to get the isomorphism in the statement. Since both sides have the K_v-module topology, then this is also a homeomorphism.

Theorem9.4.1.37

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

There is a natural K_\infty-linear homeomorphism K_\infty^{[L:K]} \cong L_\infty.

Lean code for Theorem9.4.1.37●1 definition

defdefined in FLT/NumberField/InfiniteAdeleRing.lean

complete

def NumberField.InfiniteAdeleRing.piEquiv.{u_1, u_2} (K : Type u_1)
  (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K]
  [NumberField L]
  [Algebra (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  (Fin (Module.finrank K L) →
      NumberField.InfiniteAdeleRing
        K) ≃L[NumberField.InfiniteAdeleRing K]
    NumberField.InfiniteAdeleRing L

def NumberField.InfiniteAdeleRing.piEquiv.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [Field L] [Algebra K L] [NumberField K]
  [NumberField L]
  [Algebra
      (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul
      (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  (Fin (Module.finrank K L) →
      NumberField.InfiniteAdeleRing
        K) ≃L[NumberField.InfiniteAdeleRing
      K]
    NumberField.InfiniteAdeleRing L

The $K_{\infty}$-linear homeomorphism $K_{\infty}^{[L:K]} \cong L_{\infty}$.

Proof for Theorem 9.4.1.37

uses 0

Using the isomorphisms Theorem 9.4.1.36, we clearly have a bijection K_\infty^{[L:K]} \cong \prod_v \prod_{w \mid v} L_w \cong \prod_w L_w. The K_v-linearity of each component isomorphism extends to K_\infty-linearity if the action of \prod_v K_v on \prod_w L_w is constant on the fibers of the restriction map on infinite places. In other words, if, for all x \in K_\infty and y \in L_\infty, we have (x \cdot y)_w = x_{v_w} \cdot y_w, which is true by definition.

Theorem9.4.1.38

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

L_\infty has the K_\infty-module topology.

Lean code for Theorem9.4.1.38●1 theorem

theoremdefined in FLT/NumberField/InfiniteAdeleRing.lean

complete

theorem NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT.{u_1, u_2}
  (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L]
  [NumberField K] [NumberField L]
  [Algebra (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  IsModuleTopology (NumberField.InfiniteAdeleRing K)
    (NumberField.InfiniteAdeleRing L)

theorem NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [Field L] [Algebra K L] [NumberField K]
  [NumberField L]
  [Algebra
      (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul
      (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  IsModuleTopology
    (NumberField.InfiniteAdeleRing K)
    (NumberField.InfiniteAdeleRing L)

Proof for Theorem 9.4.1.38

uses 0

Since L_\infty is homeomorphic to a finite product of K_\infty as a K_\infty-vector space, it has the K_\infty-module topology.

Theorem9.4.1.39

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

There is a natural L-algebra isomorphism L \otimes_K K_\infty \cong L_\infty.

Lean code for Theorem9.4.1.39●1 definition

defdefined in FLT/NumberField/InfiniteAdeleRing.lean

complete

def NumberField.InfiniteAdeleRing.baseChangeAlgEquiv.{u_1, u_2}
  (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L]
  [NumberField K] [NumberField L] :
  TensorProduct K L (NumberField.InfiniteAdeleRing K) ≃ₐ[L]
    NumberField.InfiniteAdeleRing L

def NumberField.InfiniteAdeleRing.baseChangeAlgEquiv.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [Field L] [Algebra K L] [NumberField K]
  [NumberField L] :
  TensorProduct K L
      (NumberField.InfiniteAdeleRing
        K) ≃ₐ[L]
    NumberField.InfiniteAdeleRing L

The $L$-algebra isomorphism $L\otimes_K K_{\infty} \cong L_{\infty}$.

Proof for Theorem 9.4.1.39

uses 0

This follows from the chain of isomorphisms L \otimes_K K_\infty \cong \prod_v (L \otimes_K K_v) \cong \prod_v \prod_{w \mid v} L_w \cong L_\infty. The first isomorphism is the standard L-algebra isomorphism L \otimes_K \prod_v K_v \cong \prod_v (L \otimes_K K_v). The second isomorphism is given by the component L-algebra isomorphisms L \otimes_K K_v \cong \prod_{w \mid v} L_w from Theorem 9.4.1.35.

Theorem9.4.1.40

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

If K -> L is a ring homomorphism between two number fields, then there is a natural isomorphism, both topological and algebraic, L \otimes_K K_\infty \cong L_\infty.

Lean code for Theorem9.4.1.40●2 declarations

defdefined in FLT/NumberField/InfiniteAdeleRing.lean

complete

def NumberField.InfiniteAdeleRing.baseChangeEquiv.{u_1, u_2} (K : Type u_1)
  (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K]
  [NumberField L]
  [Algebra (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  TensorProduct K L (NumberField.InfiniteAdeleRing K) ≃A[L]
    NumberField.InfiniteAdeleRing L

def NumberField.InfiniteAdeleRing.baseChangeEquiv.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [Field L] [Algebra K L] [NumberField K]
  [NumberField L]
  [Algebra
      (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul
      (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  TensorProduct K L
      (NumberField.InfiniteAdeleRing
        K) ≃A[L]
    NumberField.InfiniteAdeleRing L

The canonical `L`-algebra homeomorphism from `L ⊗_K K_∞` to `L_∞` induced by the
`K`-algebra base change map `K_∞ → L_∞`.

theoremdefined in FLT/NumberField/InfiniteAdeleRing.lean

complete

theorem NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT.{u_1, u_2}
  (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L]
  [NumberField K] [NumberField L]
  [Algebra (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  IsModuleTopology (NumberField.InfiniteAdeleRing K)
    (NumberField.InfiniteAdeleRing L)

theorem NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [Field L] [Algebra K L] [NumberField K]
  [NumberField L]
  [Algebra
      (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul
      (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion] :
  IsModuleTopology
    (NumberField.InfiniteAdeleRing K)
    (NumberField.InfiniteAdeleRing L)

Proof for Theorem 9.4.1.40

uses 0

Since both sides of the L-algebra isomorphism in Theorem 9.4.1.39 have the K_{\infty}-module topology, and since the isomorphism can equivalently be viewed as a K_{\infty}-linear isomorphism, it is also a homeomorphism.

9.4.2. Base Change For Adeles🔗

From the previous results we deduce immediately that if L/K is a finite extension of number fields then there's a natural (topological and algebraic) isomorphism L\otimes_K\A_K\to \A_L.

Theorem9.4.2.1

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 9.4.1.16

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 9.4.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

If K\to L is a ring homomorphism between two number fields then there is a natural isomorphism (both topological and algebraic) L\otimes_K\A_K\cong\A_L.

Lean code for Theorem9.4.2.1●1 definition

defdefined in FLT/NumberField/AdeleRing.lean

complete

def NumberField.AdeleRing.baseChangeEquiv.{u_1, u_2} (K : Type u_1)
  (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L]
  [Algebra K L]
  [Algebra
      (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K)
        K)
      (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L)
        L)]
  [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul
      (NumberField.RingOfIntegers K) K L (NumberField.RingOfIntegers L)]
  [Algebra (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion]
  [Algebra (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)
      (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)]
  [Prod.IsProdSMul (NumberField.InfiniteAdeleRing K)
      (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K)
        K)
      (NumberField.InfiniteAdeleRing L)
      (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L)
        L)]
  [IsModuleTopology
      (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)
      (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] :
  TensorProduct K L
      (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃A[L]
    NumberField.AdeleRing (NumberField.RingOfIntegers L) L

def NumberField.AdeleRing.baseChangeEquiv.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [Algebra
      (IsDedekindDomain.FiniteAdeleRing
        (NumberField.RingOfIntegers K) K)
      (IsDedekindDomain.FiniteAdeleRing
        (NumberField.RingOfIntegers L) L)]
  [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul
      (NumberField.RingOfIntegers K) K L
      (NumberField.RingOfIntegers L)]
  [Algebra
      (NumberField.InfiniteAdeleRing K)
      (NumberField.InfiniteAdeleRing L)]
  [Pi.FiberwiseSMul
      (fun a ↦ a.comap (algebraMap K L))
      NumberField.InfinitePlace.Completion
      NumberField.InfinitePlace.Completion]
  [Algebra
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers K) K)
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers L) L)]
  [Prod.IsProdSMul
      (NumberField.InfiniteAdeleRing K)
      (IsDedekindDomain.FiniteAdeleRing
        (NumberField.RingOfIntegers K) K)
      (NumberField.InfiniteAdeleRing L)
      (IsDedekindDomain.FiniteAdeleRing
        (NumberField.RingOfIntegers L) L)]
  [IsModuleTopology
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers K) K)
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers L)
        L)] :
  TensorProduct K L
      (NumberField.AdeleRing
        (NumberField.RingOfIntegers K)
        K) ≃A[L]
    NumberField.AdeleRing
      (NumberField.RingOfIntegers L) L

The `L`-algebra homeomorphism `L ⊗[K] 𝔸 K = 𝔸 L`.

Proof for Theorem 9.4.2.1

uses 0

Follows from the previous results.

Theorem9.4.2.2

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

If K\to L is a ring homomorphism between two number fields, then the topology on \A_L is the \A_K-module topology, where the module structure comes from the natural map \A_K\to\A_L.

Lean code for Theorem9.4.2.2●1 theorem

theoremdefined in FLT/NumberField/AdeleRing.lean

complete

theorem NumberField.AdeleRing.instIsModuleTopology.{u_3, u_4} {K : Type u_3}
  {L : Type u_4} [Field K] [Field L] [NumberField K] [NumberField L]
  [Algebra K L] :
  IsModuleTopology
    (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)
    (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)

theorem NumberField.AdeleRing.instIsModuleTopology.{u_3,
    u_4}
  {K : Type u_3} {L : Type u_4} [Field K]
  [Field L] [NumberField K]
  [NumberField L] [Algebra K L] :
  IsModuleTopology
    (NumberField.AdeleRing
      (NumberField.RingOfIntegers K) K)
    (NumberField.AdeleRing
      (NumberField.RingOfIntegers L) L)

Proof for Theorem 9.4.2.2

uses 0

Indeed \A_L\cong L\otimes_K\A_K is a homeomorphism, and the right hand side has the \A_K-module topology.

9.5. Discreteness and compactness🔗

We need that if K is a number field then K\subseteq\mathbb{A}_K is discrete, and the quotient (with the quotient topology) is compact. Here is a proposed proof.

Theorem9.5.1

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

There's an open subset of \A_{\Q} whose intersection with \Q is \{0\}.

Lean code for Theorem9.5.1●1 theorem

theoremdefined in FLT/NumberField/AdeleRing.lean

complete

theorem Rat.AdeleRing.zero_discrete :
  ∃ U,
    IsOpen U ∧
      ⇑(algebraMap ℚ
              (NumberField.AdeleRing (NumberField.RingOfIntegers ℚ)
                ℚ)) ⁻¹'
          U =
        {0}

theorem Rat.AdeleRing.zero_discrete :
  ∃ U,
    IsOpen U ∧
      ⇑(algebraMap ℚ
              (NumberField.AdeleRing
                (NumberField.RingOfIntegers
                  ℚ)
                ℚ)) ⁻¹'
          U =
        {0}

Proof for Theorem 9.5.1

uses 0

Use \prod_p{\Z_p}\times(-1,1). Any rational q in this set is a p-adic integer for all primes p and hence, writing it in lowest terms as q=n/d, satisfies p\nmid d, meaning that d=\pm1 and thus q\in\Z. The fact that q\in(-1,1) implies q=0.

Theorem9.5.2

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 9.4.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

There's an open subset of \A_{K} whose intersection with K is \{0\}.

Lean code for Theorem9.5.2●1 theorem

theoremdefined in FLT/NumberField/AdeleRing.lean

complete

theorem NumberField.AdeleRing.zero_discrete.{u_1} (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ U,
    IsOpen U ∧
      ⇑(algebraMap K
              (NumberField.AdeleRing (NumberField.RingOfIntegers K)
                K)) ⁻¹'
          U =
        {0}

theorem NumberField.AdeleRing.zero_discrete.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ U,
    IsOpen U ∧
      ⇑(algebraMap K
              (NumberField.AdeleRing
                (NumberField.RingOfIntegers
                  K)
                K)) ⁻¹'
          U =
        {0}

Proof for Theorem 9.5.2

uses 0

By a previous result, we have \A_K=K\otimes_{\Q}\A_{\Q}. Choose a basis of K/\Q; then K can be identified with \Q^n\subseteq(\A_{\Q})^n and the result follows from the previous theorem.

Theorem9.5.3

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

The additive subgroup K of \mathbf{A}_K is discrete.

Lean code for Theorem9.5.3●1 theorem

theoremdefined in FLT/NumberField/AdeleRing.lean

complete

theorem NumberField.AdeleRing.discrete.{u_1} (K : Type u_1) [Field K]
  [NumberField K] (x : K) :
  ∃ U,
    IsOpen U ∧
      ⇑(algebraMap K
              (NumberField.AdeleRing (NumberField.RingOfIntegers K)
                K)) ⁻¹'
          U =
        {x}

theorem NumberField.AdeleRing.discrete.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  (x : K) :
  ∃ U,
    IsOpen U ∧
      ⇑(algebraMap K
              (NumberField.AdeleRing
                (NumberField.RingOfIntegers
                  K)
                K)) ⁻¹'
          U =
        {x}

Proof for Theorem 9.5.3

uses 0

If x\in K and U is the open subset in the previous lemma, then it's easily checked that K\cap U=\{0\} implies K\cap (U+x)=\{x\}, and U+x is open.

Theorem9.5.4

Group: Finite and infinite adeles, with local compactness and base change. (47)

Group member previews

Preview

Theorem 9.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

The quotient \A_{\Q}/\Q is compact.

Lean code for Theorem9.5.4●1 theorem

theoremdefined in FLT/NumberField/AdeleRing.lean

complete

theorem Rat.AdeleRing.cocompact :
  CompactSpace
    (NumberField.AdeleRing (NumberField.RingOfIntegers ℚ) ℚ ⧸
      NumberField.AdeleRing.principalSubgroup
        (NumberField.RingOfIntegers ℚ) ℚ)

theorem Rat.AdeleRing.cocompact :
  CompactSpace
    (NumberField.AdeleRing
        (NumberField.RingOfIntegers ℚ) ℚ ⧸
      NumberField.AdeleRing.principalSubgroup
        (NumberField.RingOfIntegers ℚ) ℚ)

Proof for Theorem 9.5.4

uses 0

The space \prod_p\Z_p\times[0,1] is a product of compact spaces and is hence compact. I claim that it surjects onto \A_{\Q}/\Q. Indeed, if a\in\A_{\Q} then for the finitely many prime numbers p\in S such that a_p\not\in\Z_p we have a_p\in\frac{r_p}{p^{n_p}}+\Z_p with r_p/p^{n_p}\in\Q. If we set q=\sum_{p\in S}\frac{r_p}{p^{n_p}}\in\Q, then a-q\in \prod_p\Z_p\times\R. Subtracting \lfloor a_{\infty}-q\rfloor moves the archimedean coordinate into \prod_p\Z_p\times[0,1), so every class in \A_{\Q}/\Q has a representative in the compact set.