Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_FrobeniusEndo.lean

definition module

Frobenius endomorphisms of function fields and their norms

Throughout, K and F are fields with F a K-algebra, and \ell is a natural number. The structure AlgebraicCurve.IsFrobeniusEndo ℓ φ, for a K-algebra endomorphism \varphi : F \to F, is a proposition with two fields: pow_mem_range asserts that for every x \in F there is y \in F with \varphi(y) = x^{\ell}, and mem_range_pow asserts that for every y \in F there is x \in F with \varphi(y) = x^{\ell}. Together these say that the image \varphi(F) is exactly the set of \ell-th powers in F; the predicate is imposed on a chosen endomorphism \varphi rather than on an abstractly constructed Frobenius twist, and no characteristic hypothesis is built into it.

Given such an h : \mathrm{IsFrobeniusEndo}\ \ell\ \varphi, the operation frobNorm assigns to each f \in F an element h.\mathrm{frobNorm}(f) chosen from the existential statement of pow_mem_range, so that map_frobNorm records its defining property \varphi(h.\mathrm{frobNorm}(f)) = f^{\ell}; it is thus a preimage under \varphi of the \ell-th power of f, a choice rather than a canonical construction. Two further facts are supplied: frobNorm_ne_zero, that h.\mathrm{frobNorm}(f) \neq 0 whenever f \neq 0 (immediate from \varphi(0) = 0 and f^{\ell} \neq 0), and isIntegral, that for \ell \neq 0 the underlying ring homomorphism of \varphi is integral in the sense of RingHom.IsIntegral: each x \in F satisfies the monic polynomial X^{\ell} - C(h.\mathrm{frobNorm}(x)) with coefficients pushed forward along \varphi, since evaluating it at x gives x^{\ell} - \varphi(h.\mathrm{frobNorm}(x)) = 0.

Relation to Mathlib

Mathlib's frobenius concerns the p-power map on a ring of characteristic p; the predicate here is the project's own notion, a condition on an arbitrary K-algebra endomorphism of a field identifying its image with the subfield of \ell-th powers. The integrality conclusion is phrased with Mathlib's RingHom.IsIntegral.

Where it is used

The integrality statement isIntegral provides precisely the hypothesis φ.toRingHom.IsIntegral under which divisors can be pulled back and pushed forward along a K-algebra homomorphism of function fields, and hence under which correspondences on divisors and on \mathrm{Pic}^0 are formed in the correspondence machinery. That machinery is used for the Frobenius and Verschiebung operators entering the Eichler–Shimura relation on the Jacobian in characteristic \ell.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Graduate Texts in Mathematics 254, Springer, 2009
  2. N. Bourbaki, Algebra II, Chapters 4–7, Springer, 1990 (Chapter V, purely inseparable extensions)

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_AlgebraicCurve_FrobeniusEndo.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_Correspondence
import Mathlib.Algebra.CharP.Reduced ↗

set_option autoImplicit false

noncomputable section

namespace AlgebraicCurve

section Package

variable {K F : Type*} [Field K] [Field F] [Algebra K F]

variable (ℓ : ℕ)

structure IsFrobeniusEndo (φ : F →ₐ[K] F) : Prop where

  pow_mem_range : ∀ x : F, ∃ y : F, φ y = x ^ ℓ

  mem_range_pow : ∀ y : F, ∃ x : F, φ y = x ^ ℓ

variable {ℓ : ℕ} {φ : F →ₐ[K] F}

namespace IsFrobeniusEndo

def frobNorm (h : IsFrobeniusEndo ℓ φ) (f : F) : F :=
  (h.pow_mem_range f).choose

theorem map_frobNorm (h : IsFrobeniusEndo ℓ φ) (f : F) : φ (h.frobNorm f) = f ^ ℓ :=
  (h.pow_mem_range f).choose_spec

theorem frobNorm_ne_zero (h : IsFrobeniusEndo ℓ φ) {f : F} (hf : f ≠ 0) :
    h.frobNorm f ≠ 0 := by
  intro h0
  have := h.map_frobNorm f
  rw [h0, map_zero] at this
  exact pow_ne_zero ℓ hf this.symm

theorem isIntegral (h : IsFrobeniusEndo ℓ φ) (hℓ : ℓ ≠ 0) : φ.toRingHom.IsIntegral := by
  intro x
  refine ⟨Polynomial.X ^ ℓ - Polynomial.C (h.frobNorm x), ?_, ?_⟩
  · exact Polynomial.monic_X_pow_sub_C _ hℓ
  · simp [Polynomial.eval₂_sub, h.map_frobNorm x]

end IsFrobeniusEndo

end Package

end AlgebraicCurve

Statements phrased using this module (5)