Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GoodReductionJacobian_NsmulEigenSubdatum.lean

definition module

Deck action and eigensections along multiplication by n

Throughout, R is a commutative ring, f : A \to \operatorname{Spec} R a morphism of schemes carrying a relative group law L, and n a natural number; L.schemeNsmul n : A \to A is the n-fold multiplication morphism and, for an R-point x (an element of SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f), L.translate x : A \to A is the translation obtained from the group law applied to the identity point of A and to f followed by x. For an x satisfying T_x followed by [n] equals [n], deckApp is the ring endomorphism of \Gamma(A, [n]^{-1}U) obtained from T_x by appLE, using that this identity forces [n]^{-1}U \le T_x^{-1}([n]^{-1}U); accompanying lemmas record that it commutes with restriction along U \le U', fixes sections pulled back along [n], and fixes nsmulConst n U r, the image of r \in R under the structure map R \to \Gamma(A, [n]^{-1}U) attached to [n] followed by f. Two further lemmas identify the R- and \Gamma(A,U)-actions on the datum OModulePresheaf.pushforwardUnit f (L.schemeNsmul n) with multiplication by nsmulConst and by the appLE-image.

Under the standing hypothesis hG that every x in L.torsionSubset of level n satisfies the above identity, and for a function \chi from R-points to R, IsEigensection asserts that s \in \Gamma(A, [n]^{-1}U) satisfies deckApp of x applied to s equals nsmulConst n U (Ο‡ x) times s for all such x. These sections form an R-submodule eigenSubmodule, stable under multiplication by sections of \mathcal O_A over U and under restriction; eigenSubdatum assembles them into an OModulePresheaf over f, with eigenInclusion the componentwise injective inclusion into the pushforward datum. Multiplication carries a \chi- and a \psi-eigensection to a \chi\psi-eigensection (IsEigensection.mul, eigenMul), and 1 is a 1-eigensection (eigenOne). Finally IsNsmulCharacter Ο‡ is the conjunction of three conditions: \chi is 1 outside the n-torsion subset, \chi of the identity point is 1, and \chi is multiplicative on pairs of points of the n-torsion subset for the group law's multiplication; the constant function 1 satisfies it.

Relation to Mathlib

Mathlib has no relative group law on a scheme over Spec R, and no presheaf-of-modules datum of the shape OModulePresheaf; both, and hence the eigen-submodules and eigen-datum built here, are the project's own notions.

Where it is used

These definitions belong to the infrastructure for relative group laws and the relative Picard functor used in the good-reduction analysis of Jacobians, where the direct image of the structure sheaf along multiplication by n is decomposed according to characters of the n-torsion points.

References

  1. D. Mumford, Abelian Varieties, Tata Institute of Fundamental Research Studies in Mathematics 5, Oxford University Press, 1970, §§7, 15
  2. S. Bosch, W. LΓΌtkebohmert and M. Raynaud, NΓ©ron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete 21, Springer, 1990

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_GoodReductionJacobian_RelativeGroupLawTranslate
import Definitions.Def_AlgebraicGeometry_OModulePresheafConstructions

set_option autoImplicit false

noncomputable section

universe u

open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace AlgebraicGeometry NeronModelInfra

namespace GoodReductionJacobian.RelativeGroupLaw

variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟢ Spec (CommRingCat.of R)}
  (L : RelativeGroupLaw R f) (n : β„•)

theorem appLE_congr_hom {X Y : Scheme.{u}} {g g' : X ⟢ Y} (h : g = g') (U : Y.Opens) (V : X.Opens)
    (e : V ≀ g ⁻¹ᡁ U) (e' : V ≀ g' ⁻¹ᡁ U) : g.appLE U V e = g'.appLE U V e' := by
  subst h; rfl

theorem preimage_le_preimage_preimage_of_comp_eq {X Y : Scheme.{u}} {T : X ⟢ X} {q : X ⟢ Y} (h : T ≫ q = q)
    (U : Y.Opens) : q ⁻¹ᡁ U ≀ T ⁻¹ᡁ (q ⁻¹ᡁ U) := by
  change q ⁻¹ᡁ U ≀ (T ≫ q) ⁻¹ᡁ U
  rw [h]

theorem appLE_comp_appLE_of_comp_eq {X Y : Scheme.{u}} {T : X ⟢ X} {q : X ⟢ Y} (h : T ≫ q = q)
    (U : Y.Opens) (V W : X.Opens) (e₁ : V ≀ q ⁻¹ᡁ U) (eβ‚‚ : W ≀ T ⁻¹ᡁ V) (e₃ : W ≀ q ⁻¹ᡁ U) :
    q.appLE U V e₁ ≫ T.appLE V W eβ‚‚ = q.appLE U W e₃ := by
  rw [Scheme.Hom.appLE_comp_appLE]
  exact appLE_congr_hom h U W _ e₃

def deckApp (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
    (hx : L.translate x ≫ L.schemeNsmul n = L.schemeNsmul n) (U : A.Opens) :
    Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) ⟢ Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) :=
  (L.translate x).appLE ((L.schemeNsmul n) ⁻¹ᡁ U) ((L.schemeNsmul n) ⁻¹ᡁ U)
    (preimage_le_preimage_preimage_of_comp_eq hx U)

theorem deckApp_def (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
    (hx : L.translate x ≫ L.schemeNsmul n = L.schemeNsmul n) (U : A.Opens) :
    L.deckApp n x hx U = (L.translate x).appLE ((L.schemeNsmul n) ⁻¹ᡁ U) ((L.schemeNsmul n) ⁻¹ᡁ U)
      (preimage_le_preimage_preimage_of_comp_eq hx U) := rfl

theorem deckApp_map (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
    (hx : L.translate x ≫ L.schemeNsmul n = L.schemeNsmul n) {U U' : A.Opens} (h : U ≀ U') :
    L.deckApp n x hx U' ≫ A.presheaf.map (homOfLE ((Opens.map (L.schemeNsmul n).base).monotone h)).op =
      A.presheaf.map (homOfLE ((Opens.map (L.schemeNsmul n).base).monotone h)).op ≫ L.deckApp n x hx U := by
  simp only [deckApp_def, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]

theorem deckApp_appLE (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
    (hx : L.translate x ≫ L.schemeNsmul n = L.schemeNsmul n) (U : A.Opens)
    (a : Ξ“(A, U)) :
    (L.deckApp n x hx U).hom (((L.schemeNsmul n).appLE U ((L.schemeNsmul n) ⁻¹ᡁ U) le_rfl).hom a) =
      ((L.schemeNsmul n).appLE U ((L.schemeNsmul n) ⁻¹ᡁ U) le_rfl).hom a := by
  change ((L.schemeNsmul n).appLE U _ le_rfl ≫ L.deckApp n x hx U).hom a = _
  rw [deckApp_def, appLE_comp_appLE_of_comp_eq hx U _ _ le_rfl _ le_rfl]

def nsmulConst (U : A.Opens) (r : R) : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) :=
  letI := Scheme.TwoAffineOpenCover.algebraOfHom (L.schemeNsmul n ≫ f) ((L.schemeNsmul n) ⁻¹ᡁ U)
  algebraMap R _ r

theorem nsmulConst_def (U : A.Opens) (r : R) :
    L.nsmulConst n U r = ((L.schemeNsmul n ≫ f).appLE ⊀ ((L.schemeNsmul n) ⁻¹ᡁ U) le_top).hom
      ((Scheme.Ξ“SpecIso (.of R)).inv.hom r) := rfl

theorem pushforwardUnit_smul_eq (U : A.Opens) (r : R)
    (s : (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U) :
    r β€’ s = (show (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U from
      L.nsmulConst n U r * (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s)) := rfl

theorem pushforwardUnit_sections_smul_eq (U : A.Opens) (a : Ξ“(A, U))
    (s : (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U) :
    a β€’ s = (show (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U from
      ((L.schemeNsmul n).appLE U ((L.schemeNsmul n) ⁻¹ᡁ U) le_rfl).hom a *
        (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s)) := rfl

theorem map_nsmulConst {U U' : A.Opens} (h : U ≀ U') (r : R) :
    (A.presheaf.map (homOfLE ((Opens.map (L.schemeNsmul n).base).monotone h)).op).hom (L.nsmulConst n U' r) =
      L.nsmulConst n U r :=
  letI := Scheme.TwoAffineOpenCover.algebraOfHom (L.schemeNsmul n ≫ f) ((L.schemeNsmul n) ⁻¹ᡁ U)
  letI := Scheme.TwoAffineOpenCover.algebraOfHom (L.schemeNsmul n ≫ f) ((L.schemeNsmul n) ⁻¹ᡁ U')
  (Scheme.TwoAffineOpenCover.restrictAlgHom (L.schemeNsmul n ≫ f)
    ((Opens.map (L.schemeNsmul n).base).monotone h)).commutes r

theorem deckApp_nsmulConst (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
    (hx : L.translate x ≫ L.schemeNsmul n = L.schemeNsmul n) (U : A.Opens) (r : R) :
    (L.deckApp n x hx U).hom (L.nsmulConst n U r) = L.nsmulConst n U r := by
  have hx' : L.translate x ≫ (L.schemeNsmul n ≫ f) = L.schemeNsmul n ≫ f := by
    rw [← Category.assoc, hx]
  change ((L.schemeNsmul n ≫ f).appLE ⊀ _ le_top ≫ L.deckApp n x hx U).hom ((Scheme.Ξ“SpecIso (.of R)).inv.hom r) =
    ((L.schemeNsmul n ≫ f).appLE ⊀ _ le_top).hom ((Scheme.Ξ“SpecIso (.of R)).inv.hom r)
  rw [deckApp_def, appLE_comp_appLE_of_comp_eq hx' ⊀ _ _ le_top _ le_top]

section Eigen

variable (hG : βˆ€ x ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n,
    L.translate x ≫ L.schemeNsmul n = L.schemeNsmul n)
  (Ο‡ : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f β†’ R)

def IsEigensection (U : A.Opens) (s : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U)) : Prop :=
  βˆ€ (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
    (hx : x ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n),
    (L.deckApp n x (hG x hx) U).hom s = L.nsmulConst n U (Ο‡ x) * s

theorem isEigensection_iff (U : A.Opens) (s : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U)) :
    L.IsEigensection n hG Ο‡ U s ↔ βˆ€ (x : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f)
      (hx : x ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n),
      (L.deckApp n x (hG x hx) U).hom s = L.nsmulConst n U (Ο‡ x) * s :=
  Iff.rfl

def eigenSubmodule (U : A.Opens) :
    Submodule R ((OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U) where
  carrier := {s | L.IsEigensection n hG Ο‡ U s}
  zero_mem' := by
    change L.IsEigensection n hG Ο‡ U (0 : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U))
    intro x hx
    rw [map_zero, mul_zero]
  add_mem' := fun {s t} hs ht => by
    change L.IsEigensection n hG Ο‡ U
      ((show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s) + (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from t))
    intro x hx
    rw [map_add, hs x hx, ht x hx, mul_add]
  smul_mem' := fun r s hs => by
    change L.IsEigensection n hG Ο‡ U (L.nsmulConst n U r * (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s))
    intro x hx
    rw [map_mul, deckApp_nsmulConst, hs x hx, mul_left_comm]

theorem mem_eigenSubmodule_iff (U : A.Opens) (s : (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U) :
    s ∈ L.eigenSubmodule n hG Ο‡ U ↔ L.IsEigensection n hG Ο‡ U s :=
  Iff.rfl

theorem sections_smul_mem_eigenSubmodule (U : A.Opens) (a : Ξ“(A, U))
    (s : (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U) (hs : s ∈ L.eigenSubmodule n hG Ο‡ U) :
    a β€’ s ∈ L.eigenSubmodule n hG Ο‡ U := by
  change L.IsEigensection n hG Ο‡ U (((L.schemeNsmul n).appLE U ((L.schemeNsmul n) ⁻¹ᡁ U) le_rfl).hom a *
    (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s))
  intro x hx
  rw [map_mul, deckApp_appLE, hs x hx, mul_left_comm]

theorem res_mem_eigenSubmodule {U U' : A.Opens} (h : U ≀ U')
    (s : (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).obj U') (hs : s ∈ L.eigenSubmodule n hG Ο‡ U') :
    (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).res h s ∈ L.eigenSubmodule n hG Ο‡ U := by
  change L.IsEigensection n hG Ο‡ U
    ((A.presheaf.map (homOfLE ((Opens.map (L.schemeNsmul n).base).monotone h)).op).hom
      (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U') from s))
  intro x hx
  have hnat := congrArg (fun Ο† => Ο†.hom (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U') from s))
    (L.deckApp_map n x (hG x hx) h)
  simp only [CommRingCat.comp_apply] at hnat
  rw [← hnat, hs x hx, map_mul, L.map_nsmulConst n h]

def eigenSubdatum : OModulePresheaf f where
  obj U := L.eigenSubmodule n hG Ο‡ U
  module U := inferInstance
  moduleSections U := OModulePresheaf.submoduleSections U _ (L.sections_smul_mem_eigenSubmodule n hG Ο‡ U)
  isScalarTower U := by
    letI := Scheme.TwoAffineOpenCover.algebraOfHom f U
    letI := OModulePresheaf.submoduleSections U _ (L.sections_smul_mem_eigenSubmodule n hG Ο‡ U)
    exact ⟨fun r a s => Subtype.ext (smul_assoc r a s.1)⟩
  res h := ((OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).res h).restrict
    fun s hs => L.res_mem_eigenSubmodule n hG Ο‡ h s hs
  res_smul h a s := Subtype.ext ((OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).res_smul h a s.1)
  res_refl U := LinearMap.ext fun s =>
    Subtype.ext (LinearMap.congr_fun ((OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).res_refl U) s.1)
  res_comp h h' := LinearMap.ext fun s =>
    Subtype.ext (LinearMap.congr_fun ((OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).res_comp h h') s.1)

@[simp] theorem eigenSubdatum_obj (U : A.Opens) :
    (L.eigenSubdatum n hG Ο‡).obj U = L.eigenSubmodule n hG Ο‡ U := rfl

theorem eigenSubdatum_res_coe {U U' : A.Opens} (h : U ≀ U') (s : (L.eigenSubdatum n hG Ο‡).obj U') :
    ((L.eigenSubdatum n hG Ο‡).res h s).1 = (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)).res h s.1 := rfl

theorem eigenSubdatum_smul_coe (U : A.Opens) (a : Ξ“(A, U)) (s : (L.eigenSubdatum n hG Ο‡).obj U) :
    (a β€’ s).1 = a β€’ s.1 := rfl

def eigenInclusion :
    OModulePresheaf.Hom (L.eigenSubdatum n hG Ο‡) (OModulePresheaf.pushforwardUnit f (L.schemeNsmul n)) where
  app U := (L.eigenSubmodule n hG Ο‡ U).subtype
  app_smul _ _ _ := rfl
  naturality _ := rfl

@[simp] theorem eigenInclusion_app (U : A.Opens) (s : (L.eigenSubdatum n hG Ο‡).obj U) :
    (L.eigenInclusion n hG Ο‡).app U s = s.1 := rfl

theorem eigenInclusion_injective (U : A.Opens) : Function.Injective ((L.eigenInclusion n hG Ο‡).app U) :=
  Subtype.val_injective

theorem IsEigensection.mul {Ο‡ ψ : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f β†’ R} {U : A.Opens}
    {s t : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U)} (hs : L.IsEigensection n hG Ο‡ U s) (ht : L.IsEigensection n hG ψ U t) :
    L.IsEigensection n hG (Ο‡ * ψ) U (s * t) := fun x hx => by
  letI := Scheme.TwoAffineOpenCover.algebraOfHom (L.schemeNsmul n ≫ f) ((L.schemeNsmul n) ⁻¹ᡁ U)
  rw [map_mul, hs x hx, ht x hx, Pi.mul_apply]
  change _ = algebraMap R _ (Ο‡ x * ψ x) * (s * t)
  rw [map_mul]
  change _ = L.nsmulConst n U (Ο‡ x) * L.nsmulConst n U (ψ x) * (s * t)
  ring

theorem isEigensection_one_appLE (U : A.Opens) (a : Ξ“(A, U)) :
    L.IsEigensection n hG 1 U (((L.schemeNsmul n).appLE U ((L.schemeNsmul n) ⁻¹ᡁ U) le_rfl).hom a) := fun x hx => by
  letI := Scheme.TwoAffineOpenCover.algebraOfHom (L.schemeNsmul n ≫ f) ((L.schemeNsmul n) ⁻¹ᡁ U)
  rw [deckApp_appLE, Pi.one_apply]
  change _ = algebraMap R _ 1 * _
  rw [map_one, _root_.one_mul]

theorem isEigensection_one_one (U : A.Opens) :
    L.IsEigensection n hG 1 U 1 := by
  have h := L.isEigensection_one_appLE n hG U 1
  rwa [map_one] at h

def eigenMul {Ο‡ ψ : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f β†’ R} {U : A.Opens}
    (s : (L.eigenSubdatum n hG Ο‡).obj U) (t : (L.eigenSubdatum n hG ψ).obj U) :
    (L.eigenSubdatum n hG (Ο‡ * ψ)).obj U :=
  ⟨(show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s.1) * (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from t.1),
    IsEigensection.mul L n hG s.2 t.2⟩

theorem eigenMul_coe {Ο‡ ψ : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f β†’ R} {U : A.Opens}
    (s : (L.eigenSubdatum n hG Ο‡).obj U) (t : (L.eigenSubdatum n hG ψ).obj U) :
    (L.eigenMul n hG s t).1 = (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from s.1) *
      (show Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U) from t.1) := rfl

def eigenOne (U : A.Opens) : (L.eigenSubdatum n hG 1).obj U :=
  ⟨(1 : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U)), L.isEigensection_one_one n hG U⟩

theorem eigenOne_coe (U : A.Opens) :
    (L.eigenOne n hG U).1 = (1 : Ξ“(A, (L.schemeNsmul n) ⁻¹ᡁ U)) := rfl

end Eigen

def IsNsmulCharacter (Ο‡ : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f β†’ R) : Prop :=
  (βˆ€ x, x βˆ‰ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n β†’ Ο‡ x = 1) ∧
  Ο‡ (L.one (πŸ™ (Spec (CommRingCat.of R)))) = 1 ∧
  βˆ€ x ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n, βˆ€ y ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n,
    Ο‡ (L.mul (πŸ™ (Spec (CommRingCat.of R))) x y) = Ο‡ x * Ο‡ y

theorem isNsmulCharacter_iff (Ο‡ : SchemeHomOver (πŸ™ (Spec (CommRingCat.of R))) f β†’ R) :
    L.IsNsmulCharacter n Ο‡ ↔
      (βˆ€ x, x βˆ‰ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n β†’ Ο‡ x = 1) ∧
      Ο‡ (L.one (πŸ™ (Spec (CommRingCat.of R)))) = 1 ∧
      βˆ€ x ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n, βˆ€ y ∈ L.torsionSubset (πŸ™ (Spec (CommRingCat.of R))) n,
        Ο‡ (L.mul (πŸ™ (Spec (CommRingCat.of R))) x y) = Ο‡ x * Ο‡ y :=
  Iff.rfl

theorem isNsmulCharacter_one : L.IsNsmulCharacter n 1 :=
  ⟨fun _ _ => rfl, rfl, fun _ _ _ _ => (_root_.mul_one _).symm⟩

end GoodReductionJacobian.RelativeGroupLaw

end

Statements phrased using this module (12)