Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FieldTheory_RatFuncTower.lean

definition module

Rational function tower over with Galois action

This module sets up the tower \mathbb{Q}[X]\to\overline{\mathbb{Q}}[X]\to\overline{\mathbb{Q}}(X) together with the coefficientwise action of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) on the top field. The field \overline{\mathbb{Q}}(X) is taken to be RatFuncTower.K0, an abbreviation for the fraction ring of the polynomial ring over AlgebraicClosure ℚ, rather than Mathlib's RatFunc construction. The scoped instance RatFuncTower.algebraRatPoly equips K0 with the structure of an algebra over \mathbb{Q}[X] whose structure map is the composite of the coefficientwise map \mathbb{Q}[X]\to\overline{\mathbb{Q}}[X] induced by \mathbb{Q}\hookrightarrow\overline{\mathbb{Q}} with the localisation map \overline{\mathbb{Q}}[X]\to\overline{\mathbb{Q}}(X); being scoped, it is in force for consumers that open the namespace. The lemma RatFuncTower.algebraMap_ratPoly_apply records this description of the structure map: for p\in\mathbb{Q}[X], the image of p in K0 is the image of the polynomial obtained by applying \mathbb{Q}\to\overline{\mathbb{Q}} to each coefficient of p.

For an automorphism \sigma of \overline{\mathbb{Q}} over \mathbb{Q}, RatFuncTower.galLift σ is the automorphism \hat\sigma of K0 as a \mathbb{Q}[X]-algebra obtained by extending the coefficientwise automorphism of \overline{\mathbb{Q}}[X] attached to \sigma to fraction fields; concretely \hat\sigma(p/q)=\sigma(p)/\sigma(q), with \sigma applied to coefficients. That this extension is \mathbb{Q}[X]-linear amounts to the fact that \sigma fixes \mathbb{Q}, so it fixes polynomials with rational coefficients. The lemma RatFuncTower.galLift_algebraMap states the compatibility on the polynomial subring: for p\in\overline{\mathbb{Q}}[X], \hat\sigma applied to the image of p in K0 is the image of the coefficientwise transform of p by \sigma.

Relation to Mathlib

The field here is FractionRing (Polynomial (AlgebraicClosure ℚ)) rather than Mathlib's RatFunc (AlgebraicClosure ℚ). The \mathbb{Q}[X]-algebra structure and the lift of a Galois automorphism are the project's own declarations, built from Mathlib's coefficientwise map on polynomials and from the transport of a ring isomorphism of domains to their fraction fields; no algebra instance \mathbb{Q}[X]\to\overline{\mathbb{Q}}[X] is introduced, and the \mathbb{Q}-algebra structure on the field itself is Mathlib's.

Where it is used

The tower provides the generic fibre of a Weierstrass curve given over \mathbb{Q}[X]: its \overline{\mathbb{Q}}(X)-points carry the action of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) through \sigma\mapsto\hat\sigma, and specialising X to a rational value relates them to the \overline{\mathbb{Q}}-points of the corresponding fibre.

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

Source file: Definitions/Def_FieldTheory_RatFuncTower.lean

Declarations

Source

import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure ↗
import Mathlib.RingTheory.Localization.FractionRing ↗
import Mathlib.Algebra.Polynomial.AlgebraMap ↗
import Mathlib.Algebra.Algebra.Rat ↗

set_option autoImplicit false

noncomputable section

namespace RatFuncTower

abbrev K0 : Type := FractionRing (Polynomial (AlgebraicClosure ℚ))

scoped instance algebraRatPoly : Algebra (Polynomial ℚ) K0 :=
  ((algebraMap (Polynomial (AlgebraicClosure ℚ)) K0).comp
    (Polynomial.mapRingHom (algebraMap ℚ (AlgebraicClosure ℚ)))).toAlgebra

theorem algebraMap_ratPoly_apply (p : Polynomial ℚ) :
    algebraMap (Polynomial ℚ) K0 p =
      algebraMap (Polynomial (AlgebraicClosure ℚ)) K0
        (p.map (algebraMap ℚ (AlgebraicClosure ℚ))) := rfl

def galLift (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) : K0 ≃ₐ[Polynomial ℚ] K0 :=
  AlgEquiv.ofRingEquiv
    (f := IsFractionRing.ringEquivOfRingEquiv
      (A := Polynomial (AlgebraicClosure ℚ)) (B := Polynomial (AlgebraicClosure ℚ))
      (K := K0) (L := K0) (Polynomial.mapAlgEquiv σ).toRingEquiv)
    (by
      intro p
      have hq : ∀ q : Polynomial (AlgebraicClosure ℚ),
          (Polynomial.mapAlgEquiv σ).toRingEquiv q =
            q.map (σ : AlgebraicClosure ℚ →+* AlgebraicClosure ℚ) := fun q => rfl
      rw [algebraMap_ratPoly_apply, IsFractionRing.ringEquivOfRingEquiv_algebraMap, hq,
        Polynomial.map_map]
      congr 2
      ext x
      simp)

theorem galLift_algebraMap (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (p : Polynomial (AlgebraicClosure ℚ)) :
    galLift σ (algebraMap (Polynomial (AlgebraicClosure ℚ)) K0 p) =
      algebraMap (Polynomial (AlgebraicClosure ℚ)) K0
        (p.map (σ : AlgebraicClosure ℚ →+* AlgebraicClosure ℚ)) := by
  simp [galLift]

end RatFuncTower

end

Statements phrased using this module (1)