Faltings's theorem

StructurePlace#✓fully proved

Let \(F\) be a field and \(K\) a field with \(F\) a \(K\)-algebra. A place of \(F/K\) is a valuation ring of \(F\) containing \(K\) and different from \(F\): a \(K\)-subalgebra \(\mathcal{O}\) of \(F\) with \(\mathcal{O} \neq F\) such that \(z \in \mathcal{O}\) or \(z^{-1} \in \mathcal{O}\) for every \(z \in F\). See [Stichtenoth, Definition 1.1.4 and 1.1.8].

Stichtenoth calls the maximal ideal of \(\mathcal{O}\) the place, which determines \(\mathcal{O}\), and also requires \(\mathcal{O} \neq K\); that condition is omitted since it is automatic.

@[ext] structure Place extends ValuationSubalgebra K F where
  ne_top : toSubalgebra ≠ ⊤

Used by 8

Used byAdele ring · Faltings' theorem (Mordell conjecture) · Finitely many poles · Genus as the dimension of the adele class space · The adele algebra map is the principal embedding · Integral adeles · Principal adele map · Coordinates of a principal adele

TheoremFinitely many poles#●ready to prove

Let \(F\) be a function field over a field \(K\), that is, a finite extension of the rational function field \(K(t)\). For every \(x \in F\), there are only finitely many places \(P\) of \(F/K\) whose valuation ring \(\mathcal{O}_P\) does not contain \(x\), that is, \(x\) has only finitely many poles. See [Stichtenoth, Corollary 1.3.4].

public theorem_wanted finite_setOf_place_notMem [BundledFunctionField K F] (x : F) :
    {v : Place K F | x ∉ v}.Finite

Sources

-. Problem faltings of the lean-eval benchmark.

Uses 1

Statement usesPlace

AbbreviationAdele ring#✓fully proved

Let \(F\) be a field and \(K\) a field with \(F\) a \(K\)-algebra. The adele ring \(\mathcal{A}_F\) of \(F/K\) is the restricted product of copies of \(F\) indexed by the places \(P\) of \(F/K\), with respect to their valuation rings \(\mathcal{O}_P\) and the cofinite filter: its elements are the families \(\alpha = (\alpha_P)_P\) with \(\alpha_P \in F\) for every place \(P\) and \(\alpha_P \in \mathcal{O}_P\) for all but finitely many \(P\). See [Stichtenoth, Definition 1.5.2].

abbrev Adele : Type _ :=
  RestrictedProduct (fun _ ↦ F) (fun v : Place K F ↦ (v : Set F)) Filter.cofinite

Uses 1 · Used by 5

Statement usesPlace

Used byGenus as the dimension of the adele class space · The adele algebra map is the principal embedding · Integral adeles · Principal adele map · Coordinates of a principal adele

DefinitionPrincipal adele map#●ready to state

Let \(F\) be a function field over a field \(K\), that is, a finite extension of the rational function field \(K(t)\). The principal adele map is a ring homomorphism from \(F\) to the adele ring \(\mathcal{A}_F\) of \(F/K\). It is meant to be the diagonal embedding sending \(x \in F\) to the adele whose coordinate at every place \(P\) of \(F/K\) is \(x\), which is well defined since \(x\) has only finitely many poles; this coordinate formula is stated separately.

public def_wanted Adele.principal [BundledFunctionField K F] : F →+* Adele K F

Sources

-. Problem faltings of the lean-eval benchmark.

Uses 2 · Used by 2

Statement usesAdele ring · Place

Used byThe adele algebra map is the principal embedding · Coordinates of a principal adele

TheoremCoordinates of a principal adele#●statement formalized

Let \(F\) be a function field over a field \(K\), that is, a finite extension of the rational function field \(K(t)\). For every \(x \in F\) and every place \(P\) of \(F/K\), the coordinate at \(P\) of the principal adele of \(x\) is \(x\).

public theorem_wanted Adele.principal_apply [BundledFunctionField K F] (x : F)
    (v : Place K F) : (❰Adele.principal❱ K x) v = x

Sources

-. Problem faltings of the lean-eval benchmark.

Uses 3

Statement usesAdele ring · Principal adele map · Place

TheoremThe adele algebra map is the principal embedding#●statement formalized

Let \(F\) be a function field over a field \(K\), that is, a finite extension of the rational function field \(K(t)\). The algebra map \(F \to \mathcal{A}_F\) of the \(F\)-algebra structure on the adele ring \(\mathcal{A}_F\) equals the principal adele map \(F \to \mathcal{A}_F\).

public theorem_wanted instAlgebraAdele_algebraMap [BundledFunctionField K F] :
    algebraMap F (Adele K F) = ❰Adele.principal❱ K

Sources

-. Problem faltings of the lean-eval benchmark.

Uses 3

Statement usesAdele ring · Principal adele map · Place

DefinitionIntegral adeles#✓fully proved

Let \(F\) be a field and \(K\) a field with \(F\) a \(K\)-algebra. The integral adeles \(\mathcal{A}_F(0)\) form the \(K\)-subspace of the adele ring \(\mathcal{A}_F\) of \(F/K\) consisting of the adeles \(\alpha = (\alpha_P)_P\) whose coordinate \(\alpha_P\) lies in the valuation ring \(\mathcal{O}_P\) of \(P\) for every place \(P\) of \(F/K\). See [Stichtenoth, Definition 1.5.3].

def integralAdele : Submodule K (Adele K F) where
  carrier := {x | ∀ v, x v ∈ v}
  add_mem' h₁ h₂ v := add_mem (h₁ v) (h₂ v)
  zero_mem' _ := zero_mem _
  smul_mem' _ _ h v := v.smul_mem (h v) _

Uses 2 · Used by 1

Statement usesAdele ring · Place

Used byGenus as the dimension of the adele class space

DefinitionGenus of a function field#●ready to state

For a function field \(F\) over a field \(K\), that is, a finite extension of the rational function field \(K(t)\), the genus of \(F/K\) is a natural number \(g\), specified by the separately stated formula \(g = \dim_K \mathcal{A}_F / (\mathcal{A}_F(0) + F)\), where \(\mathcal{A}_F\) is the adele ring and \(\mathcal{A}_F(0)\) the integral adeles. See [Stichtenoth, Corollary 1.5.5].

public noncomputable def_wanted genus [BundledFunctionField K F] : ℕ

Sources

-. Problem faltings of the lean-eval benchmark.

Used by 2

Used byFaltings' theorem (Mordell conjecture) · Genus as the dimension of the adele class space

TheoremGenus as the dimension of the adele class space#●statement formalized

Let \(F\) be a function field over a field \(K\), that is, a finite extension of the rational function field \(K(t)\). The genus \(g\) of \(F/K\) equals the dimension over \(K\) of the quotient \(\mathcal{A}_F / (\mathcal{A}_F(0) + F)\), where \(\mathcal{A}_F\) is the adele ring, \(\mathcal{A}_F(0)\) the integral adeles, and \(F\) is embedded in \(\mathcal{A}_F\) by the algebra map of the \(F\)-algebra structure on the adeles (stated separately to be the principal embedding). See [Stichtenoth, Corollary 1.5.5].

The dimension is the finite rank, taken to be \(0\) if the quotient is infinite-dimensional.

public theorem_wanted genus_eq [BundledFunctionField K F] :
    ❰genus❱ = Module.finrank K
      (Adele K F ⧸ integralAdele K F ⊔ (IsScalarTower.toAlgHom K F _).toLinearMap.range)

Sources

-. Problem faltings of the lean-eval benchmark.

Uses 4

Statement usesAdele ring · Place · Genus of a function field · Integral adeles

TheoremFaltings' theorem (Mordell conjecture)#●statement formalized

Let \(K\) be a number field and \(F\) a function field over \(K\), that is, a finite extension of the rational function field \(K(t)\). If the genus of \(F/K\) is at least \(2\), then \(F/K\) has only finitely many places of degree one, that is, places \(P\) whose residue field (the quotient of the valuation ring of \(P\) by its maximal ideal) has dimension \(1\) over \(K\).

public theorem_wanted faltings [NumberField K] [BundledFunctionField K F] :
    2 ≤ ❰genus❱ K F →
    {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1}.Finite

Sources

-. Problem faltings of the lean-eval benchmark.

Uses 2

Statement usesPlace · Genus of a function field

3 fully proved1 ready to prove4 statement formalized2 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.