Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_MumfordGlueLevel.lean

definition module

Level- Mumford gluing data for the formal upper half plane

Fix a commutative ring \mathcal O, an element \pi\in\mathcal O, a field K_0 that is an \mathcal O-algebra, a natural number r, a matrix g_1\in GL_2(K_0), a subgroup N\le PGL_2(K_0) and a level n. Write A_n for the quotient of the edge chart ring chartERing π’ͺ Ο€ r β€” the localisation of \mathcal O[X_0,X_1]/(X_0X_1-\pi) away from (X_0^{r-1}-1)(X_1^{r-1}-1), with coordinates \xi,\eta β€” by the ideal generated by \pi^{n+1}, and V_n for the corresponding quotient of the vertex chart ring chartVRing π’ͺ r, the localisation of \mathcal O[X] away from X^r-X, with coordinate \zeta. The structure MumfordGlueLevel packages: a scheme Z with a flat separated morphism zb to \operatorname{Spec}(\mathcal O/\pi^{n+1}); for every h\in GL_2(K_0) a morphism \zeta_h:\operatorname{Spec}A_n\to Z which is an open immersion and lies over \operatorname{Spec}\mathcal O, such that finitely many of the \zeta_h already cover Z and \zeta_{gh}=\zeta_h whenever the class of g lies in N; an \mathcal O-algebra map \iota:A_n\to V_n with \iota(\xi)=\zeta and \iota(\eta)\zeta=\pi, exhibiting V_n as the localisation of A_n away from \xi; and families of \mathcal O-algebra automorphisms \tau_g of V_n and \alpha_g of A_n, defined for all g but constrained only by Ο„_spec and Ξ±_spec. Those two fields are characterisations on chart-valued points: for any \mathcal O-algebra B and any \mathcal O-algebra map out of V_n (respectively A_n) to B, two Deligne data d,d' over B whose lines at the standard lattice and at its g_1-translate are the explicit spans dictated by the chart coordinates (before and after composing with \tau_g, resp. \alpha_g), and which satisfy InEdgeChart for the pair (the condition that at every prime of B the lattice inclusions and nondegeneracy requirements of the edge chart hold), are required to satisfy DeligneDatum.IsPullback for g^{-1}; the hypothesis on g is that g fixes the standard vertex, resp. that g preserves the pair consisting of the standard vertex and its g_1-translate, fixing or swapping them. Further fields impose the gluing identities \zeta_{hg}=\zeta_h\circ\operatorname{Spec}\alpha_g for edge-preserving g and \zeta_{hg}\circ\operatorname{Spec}\iota=\zeta_h\circ\operatorname{Spec}\iota\circ\operatorname{Spec}\tau_g for vertex-fixing g; an incidence bound ΞΆ_preimage_le saying that, when no N-translate of the pair (h\,s_0,h\,s_1) of vertices matches (h's_0,h's_1) in either order, the \zeta_{h'}-preimage of the open image of \zeta_h is contained in the supremum of the basic open set of \xi, taken only if some N-translate carries h's_0 to h s_0 or h s_1, and of the basic open set of \eta, taken under the analogous condition on h's_1; and finally desc, a universal property at the level of charts: any family of morphisms t_h:\operatorname{Spec}A_n\to T satisfying the same N-invariance and the same \alpha- and \tau-compatibilities factors through the \zeta_h by a unique u:Z\to T.

Relation to Mathlib

The scheme-theoretic ingredients (the category of schemes, Flat and IsSeparated for morphisms, Spec.map, IsOpenImmersion, PrimeSpectrum.basicOpen, IsLocalization.Away) are Mathlib's; the gluing datum together with its chart-level universal property, and the chart rings it is built from, are the project's own notions rather than an instance of Mathlib's Scheme.GlueData.

Where it is used

The structure is the one-level input for the Čerednik–Drinfeld part of the argument: a compatible system of such data, one for each n, assembles the formal scheme whose quotient by the arithmetic group yields the p-adic uniformisation of the relevant Shimura curve. It is imported by the statement modules that construct and compare these levels.

References

  1. D. Mumford, An analytic construction of degenerating curves over complete local rings, Compositio Mathematica 24 (1972), 129–174, Β§3
  2. L. Gerritzen and M. van der Put, Schottky groups and Mumford curves, Lecture Notes in Mathematics 817, Springer, 1980, Chapter III
  3. J.-F. Boutot and H. Carayol, Uniformisation p-adique des courbes de Shimura: les thΓ©orΓ¨mes de Čerednik et de Drinfeld, AstΓ©risque 196–197 (1991), 45–158

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CerednikDrinfeld_FormalUpperHalfPlanePoints
import Definitions.Def_CerednikDrinfeld_FormalUpperHalfPlaneChartRings

set_option autoImplicit false

open scoped TensorProduct MatrixGroups
open CategoryTheory AlgebraicGeometry LT.LatticeTree

namespace CerednikDrinfeld
namespace FormalOmega

set_option genInjectivity false in
set_option genSizeOfSpec false in

structure MumfordGlueLevel
    (π’ͺ : Type) [CommRing π’ͺ] (Ο€ : π’ͺ) (Kβ‚€ : Type) [Field Kβ‚€] [Algebra π’ͺ Kβ‚€] (r : β„•)
    (g₁ : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (N : Subgroup (PGL(2, Kβ‚€))) (n : β„•) : Type 1 where

  Z : Scheme.{0}

  zb : Z ⟢ Spec (CommRingCat.of (π’ͺ β§Έ Ideal.span {Ο€ ^ (n + 1)}))

  zb_flat : Flat zb

  zb_isSeparated : IsSeparated zb

  ΞΆ : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), Spec (CommRingCat.of ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) ⟢ Z

  ΞΆ_over : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€),
    ΞΆ h ≫ zb ≫ Spec.map (CommRingCat.ofHom (algebraMap π’ͺ (π’ͺ β§Έ Ideal.span {Ο€ ^ (n + 1)}))) =
      Spec.map (CommRingCat.ofHom (algebraMap π’ͺ ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))))

  ΞΆ_isOpenImmersion : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), IsOpenImmersion (ΞΆ h)

  ΞΆ_cover : βˆƒ S : Finset (Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), βˆ€ z : Z, βˆƒ h ∈ S, z ∈ Set.range (ΞΆ h).base

  ΞΆ_inv : βˆ€ (g h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), Matrix.ProjGenLinGroup.mk g ∈ N β†’ ΞΆ (g * h) = ΞΆ h

  ΞΉ : ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) →ₐ[π’ͺ] (chartVRing π’ͺ r β§Έ Ideal.span {(algebraMap π’ͺ (chartVRing π’ͺ r) Ο€) ^ (n + 1)})

  ΞΉ_ΞΎ : ΞΉ (Ideal.Quotient.mk _ (chartERing.ΞΎ π’ͺ Ο€ r)) = Ideal.Quotient.mk _ (chartVRing.ΞΆ π’ͺ r)

  ΞΉ_Ξ· : ΞΉ (Ideal.Quotient.mk _ (chartERing.Ξ· π’ͺ Ο€ r)) * Ideal.Quotient.mk _ (chartVRing.ΞΆ π’ͺ r) = algebraMap π’ͺ (chartVRing π’ͺ r β§Έ Ideal.span {(algebraMap π’ͺ (chartVRing π’ͺ r) Ο€) ^ (n + 1)}) Ο€

  ΞΉ_isLocalization : @IsLocalization.Away ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) _ (Ideal.Quotient.mk _ (chartERing.ΞΎ π’ͺ Ο€ r)) (chartVRing π’ͺ r β§Έ Ideal.span {(algebraMap π’ͺ (chartVRing π’ͺ r) Ο€) ^ (n + 1)}) _ ΞΉ.toRingHom.toAlgebra

  Ο„ : βˆ€ (g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), (chartVRing π’ͺ r β§Έ Ideal.span {(algebraMap π’ͺ (chartVRing π’ͺ r) Ο€) ^ (n + 1)}) ≃ₐ[π’ͺ] (chartVRing π’ͺ r β§Έ Ideal.span {(algebraMap π’ͺ (chartVRing π’ͺ r) Ο€) ^ (n + 1)})

  Ο„_spec : βˆ€ (g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), Vertex.act g (stdVertex π’ͺ Kβ‚€) = (stdVertex π’ͺ Kβ‚€) β†’ βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B]
    (y : (chartVRing π’ͺ r β§Έ Ideal.span {(algebraMap π’ͺ (chartVRing π’ͺ r) Ο€) ^ (n + 1)}) →ₐ[π’ͺ] B) (d d' : DeligneDatum (K := Kβ‚€) Ο€ B),
    (d.line (stdFullLattice Kβ‚€) =
          Submodule.span B {(y (Ideal.Quotient.mk _ (chartVRing.ΞΆ π’ͺ r))) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(y (Ideal.Quotient.mk _ (chartVRing.ΞΆ π’ͺ r))) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 +
              (algebraMap π’ͺ B Ο€) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    (d'.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((y.comp (Ο„ g).toAlgHom) (Ideal.Quotient.mk _ (chartVRing.ΞΆ π’ͺ r))) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d'.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {((y.comp (Ο„ g).toAlgHom) (Ideal.Quotient.mk _ (chartVRing.ΞΆ π’ͺ r))) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 +
              (algebraMap π’ͺ B Ο€) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d'.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B g⁻¹ d d'

  Ξ± : βˆ€ (g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) ≃ₐ[π’ͺ] ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))

  Ξ±_spec : βˆ€ (g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), (Vertex.act g (stdVertex π’ͺ Kβ‚€) = (stdVertex π’ͺ Kβ‚€) ∧ Vertex.act g (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€))) ∨ (Vertex.act g (stdVertex π’ͺ Kβ‚€) = (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) ∧ Vertex.act g (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = (stdVertex π’ͺ Kβ‚€)) β†’
    βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B]
    (xq : ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) →ₐ[π’ͺ] B) (d d' : DeligneDatum (K := Kβ‚€) Ο€ B),
    (d.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    (d'.line (stdFullLattice Kβ‚€) =
          Submodule.span B {(((xq.comp (Ξ± g).toAlgHom).comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d'.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (((xq.comp (Ξ± g).toAlgHom).comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d'.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B g⁻¹ d d'

  ΞΆ_edge : βˆ€ (h g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), (Vertex.act g (stdVertex π’ͺ Kβ‚€) = (stdVertex π’ͺ Kβ‚€) ∧ Vertex.act g (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€))) ∨ (Vertex.act g (stdVertex π’ͺ Kβ‚€) = (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) ∧ Vertex.act g (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = (stdVertex π’ͺ Kβ‚€)) β†’
    ΞΆ (h * g) = Spec.map (CommRingCat.ofHom (Ξ± g).toAlgHom.toRingHom) ≫ ΞΆ h

  ΞΆ_vertex : βˆ€ (h g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), Vertex.act g (stdVertex π’ͺ Kβ‚€) = (stdVertex π’ͺ Kβ‚€) β†’
    Spec.map (CommRingCat.ofHom ΞΉ.toRingHom) ≫ ΞΆ (h * g) =
      Spec.map (CommRingCat.ofHom (Ο„ g).toAlgHom.toRingHom) ≫ Spec.map (CommRingCat.ofHom ΞΉ.toRingHom) ≫ ΞΆ h

  ΞΆ_preimage_le : βˆ€ (h h' : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€),
    (βˆ€ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N β†’
      Β¬ ((Vertex.act h' (stdVertex π’ͺ Kβ‚€) = Vertex.act (g * h) (stdVertex π’ͺ Kβ‚€) ∧ Vertex.act h' (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = Vertex.act (g * h) (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€))) ∨
         (Vertex.act h' (stdVertex π’ͺ Kβ‚€) = Vertex.act (g * h) (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) ∧ Vertex.act h' (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = Vertex.act (g * h) (stdVertex π’ͺ Kβ‚€)))) β†’
    (ΞΆ h') ⁻¹ᡁ (@Scheme.Hom.opensRange _ _ (ΞΆ h) (ΞΆ_isOpenImmersion h)) ≀
      (⨆ (_ : βˆƒ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N ∧
          (Vertex.act h' (stdVertex π’ͺ Kβ‚€) = Vertex.act (g * h) (stdVertex π’ͺ Kβ‚€) ∨ Vertex.act h' (stdVertex π’ͺ Kβ‚€) = Vertex.act (g * h) (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)))),
        PrimeSpectrum.basicOpen (Ideal.Quotient.mk (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}) (chartERing.ΞΎ π’ͺ Ο€ r))) βŠ”
      (⨆ (_ : βˆƒ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N ∧
          (Vertex.act h' (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = Vertex.act (g * h) (stdVertex π’ͺ Kβ‚€) ∨ Vertex.act h' (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = Vertex.act (g * h) (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)))),
        PrimeSpectrum.basicOpen (Ideal.Quotient.mk (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}) (chartERing.Ξ· π’ͺ Ο€ r)))

  desc : βˆ€ (T : Scheme.{0}) (t : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€ β†’ (Spec (CommRingCat.of ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) ⟢ T)),
    (βˆ€ g h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N β†’ t (g * h) = t h) β†’
    (βˆ€ h g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, (Vertex.act g (stdVertex π’ͺ Kβ‚€) = (stdVertex π’ͺ Kβ‚€) ∧ Vertex.act g (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€))) ∨ (Vertex.act g (stdVertex π’ͺ Kβ‚€) = (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) ∧ Vertex.act g (Vertex.act g₁ (stdVertex π’ͺ Kβ‚€)) = (stdVertex π’ͺ Kβ‚€)) β†’ t (h * g) = Spec.map (CommRingCat.ofHom (Ξ± g).toAlgHom.toRingHom) ≫ t h) β†’
    (βˆ€ h g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Vertex.act g (stdVertex π’ͺ Kβ‚€) = (stdVertex π’ͺ Kβ‚€) β†’
      Spec.map (CommRingCat.ofHom ΞΉ.toRingHom) ≫ t (h * g) =
        Spec.map (CommRingCat.ofHom (Ο„ g).toAlgHom.toRingHom) ≫ Spec.map (CommRingCat.ofHom ΞΉ.toRingHom) ≫ t h) β†’
    βˆƒ! u : Z ⟢ T, βˆ€ h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, ΞΆ h ≫ u = t h

end FormalOmega
end CerednikDrinfeld

Statements phrased using this module (8)