Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_RatFuncPlaceClassification.lean

definition module

Classification of places of the rational function field

Throughout, K is a field and places are taken in the project's sense: a Place K F is a valuation subring of F containing the image of K, distinct from F itself, and whose underlying ring is a principal ideal ring (hence a discrete valuation ring); two places are equal exactly when their valuation subrings coincide. For F = \mathrm{RatFunc}\,K the two sources of places are Place.ofHeightOneSpectrum w, the valuation subring of the w-adic valuation attached to a height-one prime w of K[X], and placeInfty K, the valuation subring of Mathlib's RatFunc.inftyValuation. An instance records that the value group of RatFunc.inftyValuation K is nontrivial, the witness being X.

The separation statement placeInfty_ne_ofHeightOneSpectrum says that placeInfty K differs from Place.ofHeightOneSpectrum w for every height-one prime w of K[X], and placeOfPoint_ne_placeInfty specialises this to the place \mathrm{placeOfPoint}\,K\,a cut out by the prime (X - a). The classification eq_ofHeightOneSpectrum_or_eq_placeInfty asserts that every place v of \mathrm{RatFunc}\,K over K is either of the form Place.ofHeightOneSpectrum w for some height-one prime w of K[X], or equals placeInfty K; the proof compares valuation subrings through v's associated \mathbb{Z}^{m0}-valued adic valuation and invokes Mathlib's dichotomy RatFunc.valuation_isEquiv_infty_or_adic. When K is algebraically closed, exists_eq_placeOfPoint identifies each Place.ofHeightOneSpectrum w with some \mathrm{placeOfPoint}\,K\,a, via a generator of w, necessarily associate to X - a for a root a; combining these gives eq_placeOfPoint_or_eq_placeInfty. These facts are packaged as placeEquivOption K, an explicit bijection \mathrm{Place}\,K\,(\mathrm{RatFunc}\,K) \simeq \mathrm{Option}\,K sending \mathrm{placeOfPoint}\,K\,a to some a and placeInfty K to none, with the four corresponding rewriting lemmas.

Relation to Mathlib

Place is the project's own structure (a valuation subring of F containing K, proper, and principal), not a Mathlib notion; the inputs used here — RatFunc.inftyValuation, the adic valuations of the height-one spectrum of K[X], and the dichotomy RatFunc.valuation_isEquiv_infty_or_adic — are Mathlib's, and the content of this module is their translation into statements about Place.

Where it is used

The resulting bijection \mathrm{Place}\,K(t) \simeq K \sqcup \{\infty\} is the place-theoretic form of \mathbb{P}^1(K) = K \sqcup \{\infty\} for algebraically closed K, and is used in the project's description of the j-line over an algebraically closed field, its affine points and its single cusp, which underlies the divisor-theoretic treatment of Hecke correspondences in the special fibre.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Graduate Texts in Mathematics 254, Springer, 2009, Chapter I
  2. M. Rosen, Number Theory in Function Fields, Graduate Texts in Mathematics 210, Springer, 2002, Chapter 5

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_RatFuncPlaces
import Definitions.Def_AlgebraicCurve_RatFuncPlaceInfty

set_option autoImplicit false

noncomputable section

open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial

namespace AlgebraicCurve

namespace RationalFunctionField

variable (K : Type*) [Field K]

section PlaceInfty

variable [DecidableEq (RatFunc K)]

instance instNontrivialSubtypeUnitsWithZeroMultiplicativeIntMemSubgroupValueGroupRatFuncValuationInftyValuation_definitions :
    Nontrivial (MonoidWithZeroHom.valueGroup (MonoidWithZeroHom.ofClass (RatFunc.inftyValuation K))) := by
  rw [Subgroup.nontrivial_iff_exists_ne_one]
  refine ⟨Units.mk0 (RatFunc.inftyValuation K RatFunc.X)
    (by rw [RatFunc.inftyValuation.X]; exact exp_ne_zero), ?_, ?_⟩
  · exact MonoidWithZeroHom.mem_valueGroup _ ⟨RatFunc.X, rfl⟩
  · rw [ne_eq, Units.ext_iff, Units.val_mk0, Units.val_one, RatFunc.inftyValuation.X]
    simp

theorem placeInfty_ne_ofHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    placeInfty K ≠ Place.ofHeightOneSpectrum w := by
  intro h
  refine RatFunc.adicValuation_not_isEquiv_infty_valuation w
    ((Valuation.isEquiv_iff_valuationSubring _ _).mpr ?_)
  have h2 := congrArg Place.toValuationSubring h
  rw [placeInfty_toValuationSubring, Place.ofHeightOneSpectrum_toValuationSubring] at h2
  exact h2.symm

end PlaceInfty

variable {K}

theorem eq_ofHeightOneSpectrum_or_eq_placeInfty [DecidableEq (RatFunc K)]
    (v : Place K (RatFunc K)) :
    (∃ w : HeightOneSpectrum K[X], v = Place.ofHeightOneSpectrum w) ∨ v = placeInfty K := by
  rcases (RatFunc.valuation_isEquiv_infty_or_adic (v := v.adicValuation)).or with h | h
  · exact Or.inr (Place.ext (v.adicValuation_valuationSubring.symm.trans
      ((Valuation.isEquiv_iff_valuationSubring _ _).mp h)))
  · obtain ⟨w, hw, -⟩ := h
    exact Or.inl ⟨w, Place.ext (v.adicValuation_valuationSubring.symm.trans
      ((Valuation.isEquiv_iff_valuationSubring _ _).mp hw))⟩

variable (K)

theorem placeOfPoint_ne_placeInfty [DecidableEq (RatFunc K)] (a : K) :
    placeOfPoint K a ≠ placeInfty K := by
  rw [placeOfPoint_eq_ofHeightOneSpectrum]
  exact fun h => placeInfty_ne_ofHeightOneSpectrum K _ h.symm

theorem exists_eq_placeOfPoint [IsAlgClosed K] (w : HeightOneSpectrum K[X]) :
    ∃ a : K, Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w = placeOfPoint K a := by
  obtain ⟨p, hp, hwp⟩ := exists_irreducible_span K w
  have hdeg : p.degree ≠ 0 := by
    rw [IsAlgClosed.degree_eq_one_of_irreducible K hp]; exact one_ne_zero
  obtain ⟨a, ha⟩ := IsAlgClosed.exists_root p hdeg
  refine ⟨a, ?_⟩
  have hassoc : Associated ((X : K[X]) - C a) p :=
    (irreducible_X_sub_C a).associated_of_dvd hp (dvd_iff_isRoot.mpr ha)
  have hideal : w = heightOneSpectrumOfIrreducible K (irreducible_X_sub_C a) :=
    HeightOneSpectrum.ext (by
      rw [hwp, heightOneSpectrumOfIrreducible_asIdeal]
      exact (Ideal.span_singleton_eq_span_singleton.mpr hassoc).symm)
  rw [hideal, placeOfPoint_eq_ofHeightOneSpectrum]

theorem eq_placeOfPoint_or_eq_placeInfty [IsAlgClosed K] [DecidableEq (RatFunc K)]
    (v : Place K (RatFunc K)) :
    (∃ a : K, v = placeOfPoint K a) ∨ v = placeInfty K := by
  rcases eq_ofHeightOneSpectrum_or_eq_placeInfty v with ⟨w, hw⟩ | hw
  · obtain ⟨a, ha⟩ := exists_eq_placeOfPoint K w
    exact Or.inl ⟨a, hw.trans ha⟩
  · exact Or.inr hw

private def ofOption [DecidableEq (RatFunc K)] : Option K → Place K (RatFunc K) :=
  fun o => o.elim (placeInfty K) (placeOfPoint K)

private theorem ofOption_bijective [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    Function.Bijective (ofOption K) := by
  constructor
  · rintro (_ | a) (_ | b) h
    · rfl
    · exact absurd h.symm (placeOfPoint_ne_placeInfty K b)
    · exact absurd h (placeOfPoint_ne_placeInfty K a)
    · exact congrArg some (placeOfPoint_injective K h)
  · intro v
    rcases eq_placeOfPoint_or_eq_placeInfty K v with ⟨a, ha⟩ | ha
    · exact ⟨some a, ha.symm⟩
    · exact ⟨none, ha.symm⟩

def placeEquivOption [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    Place K (RatFunc K) ≃ Option K :=
  (Equiv.ofBijective (ofOption K) (ofOption_bijective K)).symm

@[simp]
theorem placeEquivOption_symm_some [IsAlgClosed K] [DecidableEq (RatFunc K)] (a : K) :
    (placeEquivOption K).symm (some a) = placeOfPoint K a := rfl

@[simp]
theorem placeEquivOption_symm_none [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    (placeEquivOption K).symm none = placeInfty K := rfl

@[simp]
theorem placeEquivOption_placeOfPoint [IsAlgClosed K] [DecidableEq (RatFunc K)] (a : K) :
    placeEquivOption K (placeOfPoint K a) = some a :=
  (Equiv.ofBijective (ofOption K) (ofOption_bijective K)).symm_apply_apply (some a)

@[simp]
theorem placeEquivOption_placeInfty [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    placeEquivOption K (placeInfty K) = none :=
  (Equiv.ofBijective (ofOption K) (ofOption_bijective K)).symm_apply_apply none

end RationalFunctionField

end AlgebraicCurve

Statements phrased using this module (5)