Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_NumberField_Completion_Finite.lean

definition moduleadapted from the Imperial College London FLT project: FLT/NumberField/Completion/Finite.lean

Local fields at finite places: finiteness, compactness, local compactness

Throughout, K is a number field, v a height-one prime of the ring of integers \mathcal{O}_K, K_v = v.adicCompletion K the v-adic completion (a valued field with values in \mathbb{Z}^{m0} = \mathrm{WithZero}(\mathrm{Multiplicative}\,\mathbb{Z})) and \mathcal{O}_v = v.adicCompletionIntegers K its valuation subring. The module registers the basic topological and finiteness facts about this situation as instances and lemmas.

NumberField.instFiniteResidueFieldAdicCompletionIntegers asserts that the residue field of \mathcal{O}_v is finite; it is obtained by transporting the finiteness of \mathcal{O}_K/v (a nonzero ideal in a ring free of finite rank over \mathbb{Z}) along the ring isomorphism \mathcal{O}_K/v \cong \mathcal{O}_v/\mathfrak{m}_v induced by \mathcal{O}_K \to \mathcal{O}_v. The same statement is then recorded for the residue field \mathfrak{k}[K_v] of the valuation ring attached to the Valued structure on K_v. NumberField.instCompactSpaceAdicCompletionIntegers asserts that \mathcal{O}_v is a compact space; it cites Valued.WithZeroMulInt.integer_compactSpace, whose hypotheses here are completeness of K_v, the discrete-valuation-ring property and rank-one discreteness of its valuation, the finiteness of the residue field just established, and the surjectivity of the valuation of K_v onto \mathbb{Z}^{m0}. NumberField.isCompactAdicCompletionIntegers and NumberField.isOpenAdicCompletionIntegers restate this compactness, and the openness of a valuation subring in a valued field, for \mathcal{O}_v viewed as a subset of K_v.

From these, K_v is shown to be weakly locally compact — each x has the compact open neighbourhood x + \mathcal{O}_v — and hence locally compact; second countability of K_v is also available. Finally, Rat.adicCompletion.locallyCompactSpace records local compactness of the v-adic completion of \mathbb{Q} for a height-one prime v of \mathcal{O}_\mathbb{Q}, deduced from its identification, as a homeomorphism and hence a closed embedding, with the corresponding field \mathbb{Q}_p.

Relation to Mathlib

Mathlib supplies the v-adic completion of a Dedekind domain's fraction field, its valuation subring and the residue-field machinery for valued fields; the finiteness, compactness and (weak) local compactness instances for number fields assembled here are the project's additions, built on the project's comparison of \mathcal{O}_K/v with the residue field of \mathcal{O}_v and on its compactness criterion for \mathbb{Z}^{m0}-valued fields.

Where it is used

These instances make K_v a local field in the topological sense, so that the completions at finite places may be used as topological rings throughout the argument; they are prerequisites for the local analysis of Galois representations at finite places and are relied upon by a large part of the development.

References

  1. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979, Chapters I–II
  2. A. Weil, Basic Number Theory, Grundlehren der mathematischen Wissenschaften 144, Springer, 1974, Chapter I

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_NumberField_Completion_Finite.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_DedekindDomain_AdicValuation_InlineSpecific
import Definitions.Def_Mathlib_Topology_Algebra_Valued_WithZeroMulInt
import Definitions.Def_Mathlib_LinearAlgebra_Countable
set_option maxHeartbeats 1200000
set_option synthInstance.maxHeartbeats 400000

section

variable (K : Type*) [Field K] [NumberField K]

open NumberField

example (I : Ideal (𝓞 K)) (hI : I ≠ 0) : Finite ((𝓞 K) ⧸ I) :=
  Ideal.finiteQuotientOfFreeOfNeBot I hI

open IsDedekindDomain

variable (v : HeightOneSpectrum (𝓞 K))

open IsLocalRing

instance NumberField.instFiniteResidueFieldAdicCompletionIntegers :
    Finite (ResidueField (v.adicCompletionIntegers K)) := by
  apply (HeightOneSpectrum.ResidueFieldEquivCompletionResidueField K v).toEquiv.finite_iff.mp
  exact Ideal.finiteQuotientOfFreeOfNeBot v.asIdeal v.ne_bot

open scoped Valued in
instance : Finite (𝓀[v.adicCompletion K]) :=
  inferInstanceAs (Finite (ResidueField (v.adicCompletionIntegers K)))

instance NumberField.instCompactSpaceAdicCompletionIntegers :
    CompactSpace (v.adicCompletionIntegers K) :=
  Valued.WithZeroMulInt.integer_compactSpace (v.adicCompletion K) inferInstance
    (v.valuedAdicCompletion_surjective K)

lemma NumberField.isCompactAdicCompletionIntegers :
    IsCompact (v.adicCompletionIntegers K : Set (v.adicCompletion K)) := by
  rw [isCompact_iff_compactSpace]
  exact instCompactSpaceAdicCompletionIntegers K v

lemma NumberField.isOpenAdicCompletionIntegers :
    IsOpen (v.adicCompletionIntegers K : Set (v.adicCompletion K)) :=
  Valued.isOpen_valuationSubring _

instance Rat.adicCompletion.locallyCompactSpace (v : HeightOneSpectrum (𝓞 ℚ)) :
    LocallyCompactSpace (v.adicCompletion ℚ) :=
  (Rat.HeightOneSpectrum.adicCompletion.padicEquiv v).toHomeomorph.isClosedEmbedding
  |>.locallyCompactSpace

instance (v : HeightOneSpectrum (𝓞 K)) :
    WeaklyLocallyCompactSpace (v.adicCompletion K) where
  exists_compact_mem_nhds x :=
    open Pointwise in
    ⟨x +ᵥ ((v.adicCompletionIntegers K) : Set (v.adicCompletion K)),
      (isCompact_iff_compactSpace.mpr <| instCompactSpaceAdicCompletionIntegers K v).vadd x,
      ((isOpenAdicCompletionIntegers K v).vadd x).mem_nhds (Set.mem_vadd_set.mpr ⟨0, by simp⟩)⟩

instance (v : HeightOneSpectrum (𝓞 K)) :
    LocallyCompactSpace (v.adicCompletion K) := inferInstance

example (v : HeightOneSpectrum (𝓞 K)) : SecondCountableTopology (v.adicCompletion K) :=
  inferInstance

end

Statements phrased using this module (6)