Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_GeometricBaseChange.lean

definition module

Geometric base change of subfields of

Fix a field L with a \mathbb{Q}-algebra structure and an intermediate field F_0 of \mathbb{Q}((q))/\mathbb{Q}. Writing coeffEmb L for the project's coefficientwise embedding \mathbb{Q}((q)) \hookrightarrow L((q)) and laurentBaseChange L F₀ for the intermediate field of L((q))/L obtained by adjoining the image of F_0 to L (both from the imported Laurent-coefficient module), the module constructs the comparison map between L \otimes_{\mathbb{Q}} F_0 and this compositum. First, linearIndependent_coeffEmb records linear disjointness in the form: any \mathbb{Q}-linearly independent family in \mathbb{Q}((q)) remains L-linearly independent in L((q)) after applying coeffEmb L; this holds for every field L \supseteq \mathbb{Q}, with no algebraicity hypothesis, and is proved by taking coordinates in a \mathbb{Q}-basis of L. Then baseChangeRatAlgHom is the \mathbb{Q}-algebra map obtained from Algebra.TensorProduct.productMap applied to \operatorname{algebraMap} L\,L((q)) and to coeffEmb L composed with the inclusion of F_0, and baseChangeHom is its upgrade to an L-algebra map L \otimes_{\mathbb{Q}} F_0 \to L((q)), so c \otimes f \mapsto \operatorname{algebraMap}(c)\cdot \mathrm{coeffEmb}(f). It is injective (baseChangeHom_injective, from the linear disjointness statement and a basis of the tensor product) and takes values in laurentBaseChange L F₀ (baseChangeHom_mem); hence the instance instIsDomainTensorProduct that L \otimes_{\mathbb{Q}} F_0 is a domain.

Under the further hypothesis that L/\mathbb{Q} is algebraic, L \otimes_{\mathbb{Q}} F_0 is a field (isField_tensorProduct, from Mathlib's tensor-product criterion), so the image of baseChangeHom is an intermediate field containing the generators of the compositum; exists_baseChangeHom_eq gives surjectivity onto laurentBaseChange L F₀ and baseChangeEquiv is the resulting L-algebra isomorphism L \otimes_{\mathbb{Q}} F_0 \simeq L\cdot F_0, with lemmas computing its values on 1 \otimes f and c \otimes f and its inverse. Finally geomAut is the monoid homomorphism sending a \mathbb{Q}-automorphism \sigma of F_0 to the L-automorphism of laurentBaseChange L F₀ conjugate, through baseChangeEquiv, to \mathrm{id}_L \otimes \sigma; geomAut_coeffEmb and coe_geomAut_coeffEmb say that it sends \mathrm{coeffEmb}(f) to \mathrm{coeffEmb}(\sigma f) for f \in F_0. Note that geomAut keeps the same F_0 on source and target.

Relation to Mathlib

Mathlib supplies the tensor-product algebra API used here (Algebra.TensorProduct.productMap, Algebra.TensorProduct.basis, Algebra.TensorProduct.isField_of_isAlgebraic, Algebra.TensorProduct.congr) and a general notion of linear disjointness, but the Laurent-series coefficient embedding coeffEmb and the compositum laurentBaseChange are the project's own (from the imported module), as are all the declarations here.

Where it is used

Taken with L = \overline{\mathbb{Q}} (an algebraic closure of \mathbb{Q}) and F_0 the modular function field attached to X_0(N), baseChangeEquiv identifies \overline{\mathbb{Q}} \otimes_{\mathbb{Q}} F_0 with the geometric function field, and geomAut transports \mathbb{Q}-automorphisms of the modular function field — the Atkin–Lehner and Fricke involutions, and twists of degeneracy maps — to \overline{\mathbb{Q}}-automorphisms of it, which then act on places of the curve and on J_0(N). This is the mechanism by which the Fricke involution and the cusp 0 are defined at the geometric level in the later cuspidal-class material.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  2. S. Lang, Algebra, 3rd edition, Graduate Texts in Mathematics 211, Springer, 2002 (linear disjointness and tensor products of field 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_ModularCurve_GeometricBaseChange.lean

Imports

Imported by

Declarations

Source

import Mathlib.FieldTheory.LinearDisjoint ↗
import Mathlib.RingTheory.TensorProduct.Free ↗
import Mathlib.Algebra.Algebra.Hom.Rat ↗
import Mathlib.Algebra.Module.LinearMap.Rat ↗
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_FieldTheory_RatAlgClosureGalois

set_option autoImplicit false

noncomputable section

open scoped TensorProduct
open IntermediateField

namespace ModularCurve

section LinearDisjoint

variable (L : Type*) [Field L] [Algebra ℚ L]

theorem linearIndependent_coeffEmb {ι : Type*} {v : ι → LaurentSeries ℚ}
    (hv : LinearIndependent ℚ v) : LinearIndependent L (fun i => coeffEmb L (v i)) := by
  classical
  rw [linearIndependent_iff'] at hv ⊢
  intro s g hg i hi
  let b := Module.Free.chooseBasis ℚ L
  refine b.forall_coord_eq_zero_iff.mp fun k => ?_
  have hk : ∑ j ∈ s, (b.coord k (g j)) • v j = 0 := by
    ext n
    have hn := congrArg (fun x : LaurentSeries L => b.coord k (x.coeff n)) hg
    simp only [HahnSeries.coeff_sum, HahnSeries.coeff_smul, coeffEmb_coeff, smul_eq_mul,
      HahnSeries.coeff_zero, map_zero] at hn
    simp only [HahnSeries.coeff_sum, HahnSeries.coeff_smul, smul_eq_mul, HahnSeries.coeff_zero]
    rw [← hn, map_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [mul_comm (g j), ← Algebra.smul_def, map_smul, smul_eq_mul, mul_comm]
  exact hv s (fun j => b.coord k (g j)) hk i hi

end LinearDisjoint

section BaseChange

variable (L : Type*) [Field L]

private theorem algebraMap_mul_eq_smul (c : L) (y : LaurentSeries L) :
    algebraMap L (LaurentSeries L) c * y = c • y := by
  rw [algebraMap_laurentSeries_eq_single, HahnSeries.single_zero_mul_eq_smul]

variable [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))

def baseChangeRatAlgHom : L ⊗[ℚ] F₀ →ₐ[ℚ] LaurentSeries L :=
  Algebra.TensorProduct.productMap (algebraMap L (LaurentSeries L)).toRatAlgHom
    ((coeffEmb L).comp (F₀.val : F₀ →+* LaurentSeries ℚ)).toRatAlgHom

theorem baseChangeRatAlgHom_tmul (c : L) (f : F₀) :
    baseChangeRatAlgHom L F₀ (c ⊗ₜ f) =
      algebraMap L (LaurentSeries L) c * coeffEmb L (f : LaurentSeries ℚ) :=
  Algebra.TensorProduct.productMap_apply_tmul _ _ c f

def baseChangeHom : L ⊗[ℚ] F₀ →ₐ[L] LaurentSeries L :=
  { baseChangeRatAlgHom L F₀ with
    commutes' := fun c => by
      change baseChangeRatAlgHom L F₀ (algebraMap L (L ⊗[ℚ] F₀) c) =
        algebraMap L (LaurentSeries L) c
      rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
        baseChangeRatAlgHom_tmul, OneMemClass.coe_one, map_one, mul_one] }

@[simp]
theorem baseChangeHom_tmul (c : L) (f : F₀) :
    baseChangeHom L F₀ (c ⊗ₜ f) =
      algebraMap L (LaurentSeries L) c * coeffEmb L (f : LaurentSeries ℚ) :=
  baseChangeRatAlgHom_tmul L F₀ c f

theorem baseChangeHom_one_tmul (f : F₀) :
    baseChangeHom L F₀ (1 ⊗ₜ f) = coeffEmb L (f : LaurentSeries ℚ) := by
  rw [baseChangeHom_tmul, map_one, one_mul]

private def baseChangeLinear : L ⊗[ℚ] F₀ →ₗ[L] LaurentSeries L where
  toFun := baseChangeHom L F₀
  map_add' := map_add _
  map_smul' c x := by
    rw [RingHom.id_apply, ← algebraMap_mul_eq_smul, ← (baseChangeHom L F₀).commutes c,
      ← map_mul, ← Algebra.smul_def]

private theorem baseChangeLinear_apply (x : L ⊗[ℚ] F₀) :
    baseChangeLinear L F₀ x = baseChangeHom L F₀ x := rfl

private def valRatLinear : F₀ →ₗ[ℚ] LaurentSeries ℚ :=
  ((F₀.val : F₀ →+* LaurentSeries ℚ) : F₀ →+ LaurentSeries ℚ).toRatLinearMap

private theorem valRatLinear_apply (f : F₀) : valRatLinear F₀ f = (f : LaurentSeries ℚ) := rfl

private theorem baseChangeLinear_injective : Function.Injective (baseChangeLinear L F₀) := by
  classical
  let bF := Module.Free.chooseBasis ℚ F₀
  let B := Algebra.TensorProduct.basis L bF
  have hli : LinearIndependent L (baseChangeLinear L F₀ ∘ B) := by
    have h : (baseChangeLinear L F₀ ∘ B : _ → LaurentSeries L) =
        fun i => coeffEmb L (valRatLinear F₀ (bF i)) := by
      funext i
      rw [Function.comp_apply, baseChangeLinear_apply, Algebra.TensorProduct.basis_apply,
        baseChangeHom_one_tmul, valRatLinear_apply]
    rw [h]
    refine linearIndependent_coeffEmb L ?_
    refine bF.linearIndependent.map' (valRatLinear F₀) (LinearMap.ker_eq_bot.mpr ?_)
    exact Subtype.val_injective
  rw [injective_iff_map_eq_zero]
  intro x hx
  have hrepr : Finsupp.linearCombination L (baseChangeLinear L F₀ ∘ B) (B.repr x) = 0 := by
    rw [← Finsupp.apply_linearCombination, B.linearCombination_repr]
    exact hx
  have h0 : B.repr x = 0 := linearIndependent_iff.mp hli (B.repr x) hrepr
  rw [← B.linearCombination_repr x, h0, map_zero]

theorem baseChangeHom_injective : Function.Injective (baseChangeHom L F₀) :=
  baseChangeLinear_injective L F₀

theorem baseChangeHom_mem (x : L ⊗[ℚ] F₀) :
    baseChangeHom L F₀ x ∈ laurentBaseChange L F₀ := by
  induction x using TensorProduct.induction_on with
  | zero => rw [map_zero]; exact zero_mem _
  | tmul c f =>
      rw [baseChangeHom_tmul]
      exact mul_mem ((laurentBaseChange L F₀).algebraMap_mem c)
        (coeffEmb_mem_laurentBaseChange L f.2)
  | add x y hx hy => rw [map_add]; exact add_mem hx hy

instance instIsDomainTensorProduct : IsDomain (L ⊗[ℚ] F₀) :=
  Function.Injective.isDomain (baseChangeHom L F₀).toRingHom (baseChangeHom_injective L F₀)

variable [Algebra.IsAlgebraic ℚ L]

theorem isField_tensorProduct : IsField (L ⊗[ℚ] F₀) :=
  Algebra.TensorProduct.isField_of_isAlgebraic ℚ L F₀ (Or.inl inferInstance)

private theorem isField_range_baseChangeHom : IsField (baseChangeHom L F₀).range :=
  MulEquiv.isField (isField_tensorProduct L F₀)
    (AlgEquiv.ofInjective _ (baseChangeHom_injective L F₀)).symm.toMulEquiv

theorem exists_baseChangeHom_eq {y : LaurentSeries L} (hy : y ∈ laurentBaseChange L F₀) :
    ∃ x : L ⊗[ℚ] F₀, baseChangeHom L F₀ x = y := by
  let K : IntermediateField L (LaurentSeries L) :=
    (baseChangeHom L F₀).range.toIntermediateField' (isField_range_baseChangeHom L F₀)
  have hle : laurentBaseChange L F₀ ≤ K := by
    change IntermediateField.adjoin L _ ≤ K
    refine IntermediateField.adjoin_le_iff.mpr ?_
    rintro _ ⟨f, hf, rfl⟩
    exact ⟨(1 : L) ⊗ₜ ⟨f, hf⟩, baseChangeHom_one_tmul L F₀ ⟨f, hf⟩⟩
  exact hle hy

def baseChangeEquiv : L ⊗[ℚ] F₀ ≃ₐ[L] laurentBaseChange L F₀ :=
  AlgEquiv.ofBijective
    { toFun := fun x => ⟨baseChangeHom L F₀ x, baseChangeHom_mem L F₀ x⟩
      map_one' := Subtype.ext (map_one _)
      map_mul' := fun x y => Subtype.ext (map_mul _ x y)
      map_zero' := Subtype.ext (map_zero _)
      map_add' := fun x y => Subtype.ext (map_add _ x y)
      commutes' := fun c => Subtype.ext ((baseChangeHom L F₀).commutes c) }
    ⟨fun x y h => baseChangeHom_injective L F₀ (congrArg Subtype.val h), fun y => by
      obtain ⟨x, hx⟩ := exists_baseChangeHom_eq L F₀ y.2
      exact ⟨x, Subtype.ext hx⟩⟩

@[simp]
theorem coe_baseChangeEquiv_apply (x : L ⊗[ℚ] F₀) :
    (baseChangeEquiv L F₀ x : LaurentSeries L) = baseChangeHom L F₀ x := rfl

theorem baseChangeEquiv_one_tmul (f : F₀) :
    baseChangeEquiv L F₀ (1 ⊗ₜ f) = ⟨coeffEmb L f, coeffEmb_mem_laurentBaseChange L f.2⟩ :=
  Subtype.ext (baseChangeHom_one_tmul L F₀ f)

theorem baseChangeEquiv_symm_coeffEmb (f : F₀) :
    (baseChangeEquiv L F₀).symm ⟨coeffEmb L f, coeffEmb_mem_laurentBaseChange L f.2⟩ = 1 ⊗ₜ f := by
  rw [← baseChangeEquiv_one_tmul, AlgEquiv.symm_apply_apply]

theorem baseChangeEquiv_tmul (c : L) (f : F₀) :
    baseChangeEquiv L F₀ (c ⊗ₜ f) =
      algebraMap L (laurentBaseChange L F₀) c *
        ⟨coeffEmb L f, coeffEmb_mem_laurentBaseChange L f.2⟩ := by
  rw [show c ⊗ₜ[ℚ] f = algebraMap L (L ⊗[ℚ] F₀) c * (1 ⊗ₜ f) by
      rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
        Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul],
    map_mul, AlgEquiv.commutes, baseChangeEquiv_one_tmul]

def geomAut : (F₀ ≃ₐ[ℚ] F₀) →* (laurentBaseChange L F₀ ≃ₐ[L] laurentBaseChange L F₀) :=
  MonoidHom.mk'
    (fun σ => ((baseChangeEquiv L F₀).symm.trans
      (Algebra.TensorProduct.congr (AlgEquiv.refl : L ≃ₐ[L] L) σ)).trans (baseChangeEquiv L F₀))
    (fun σ τ => AlgEquiv.ext fun x => by
      change baseChangeEquiv L F₀ (Algebra.TensorProduct.congr (AlgEquiv.refl : L ≃ₐ[L] L) (σ * τ)
          ((baseChangeEquiv L F₀).symm x)) =
        baseChangeEquiv L F₀ (Algebra.TensorProduct.congr (AlgEquiv.refl : L ≃ₐ[L] L) σ
          ((baseChangeEquiv L F₀).symm (baseChangeEquiv L F₀
            (Algebra.TensorProduct.congr (AlgEquiv.refl : L ≃ₐ[L] L) τ
              ((baseChangeEquiv L F₀).symm x)))))
      rw [AlgEquiv.symm_apply_apply]
      congr 1
      induction (baseChangeEquiv L F₀).symm x using TensorProduct.induction_on with
      | zero => simp only [map_zero]
      | tmul c f => rfl
      | add y z hy hz => simp only [map_add, hy, hz])

theorem geomAut_apply (σ : F₀ ≃ₐ[ℚ] F₀) (x : laurentBaseChange L F₀) :
    geomAut L F₀ σ x = baseChangeEquiv L F₀
      (Algebra.TensorProduct.congr (AlgEquiv.refl : L ≃ₐ[L] L) σ ((baseChangeEquiv L F₀).symm x)) :=
  rfl

theorem geomAut_baseChangeEquiv_tmul (σ : F₀ ≃ₐ[ℚ] F₀) (c : L) (f : F₀) :
    geomAut L F₀ σ (baseChangeEquiv L F₀ (c ⊗ₜ f)) = baseChangeEquiv L F₀ (c ⊗ₜ σ f) := by
  rw [geomAut_apply, AlgEquiv.symm_apply_apply]
  rfl

theorem geomAut_coeffEmb (σ : F₀ ≃ₐ[ℚ] F₀) (f : F₀) :
    geomAut L F₀ σ ⟨coeffEmb L f, coeffEmb_mem_laurentBaseChange L f.2⟩ =
      ⟨coeffEmb L (σ f), coeffEmb_mem_laurentBaseChange L (σ f).2⟩ := by
  rw [← baseChangeEquiv_one_tmul, geomAut_baseChangeEquiv_tmul, baseChangeEquiv_one_tmul]

theorem coe_geomAut_coeffEmb (σ : F₀ ≃ₐ[ℚ] F₀) (f : F₀) :
    (geomAut L F₀ σ ⟨coeffEmb L f, coeffEmb_mem_laurentBaseChange L f.2⟩ : LaurentSeries L) =
      coeffEmb L (σ f) :=
  congrArg Subtype.val (geomAut_coeffEmb L F₀ σ f)

end BaseChange

end ModularCurve

end

Statements phrased using this module (67)