Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_FormalUpperHalfPlaneCharts.lean

definition module

Affine charts of the formal Drinfeld upper half plane

Over a commutative ring \mathcal{O}, the module first sets up a lightweight notion of functor on \mathcal{O}-algebras: AlgFunctor π’ͺ consists of an assignment B \mapsto F(B) of a type to every commutative \mathcal{O}-algebra B (ranging over Type), a transport map along every \mathcal{O}-algebra homomorphism B \to B', and the two functoriality laws for the identity and for composition as fields. Around it are recorded natural transformations (a family of maps F(B) \to G(B) together with the naturality square as a field), their identity and composition, the product functor B \mapsto F(B) \times G(B), the corepresentable functor B \mapsto \operatorname{Hom}_{\mathcal{O}\text{-alg}}(A,B) attached to an \mathcal{O}-algebra A, and a structure GroupAction expressing an action of a group \Gamma on F by maps F(B) \to F(B) that are unital, multiplicative and compatible with transport. For \pi \in \mathcal{O}, the predicates NatTrans.IsIsoOnNilp Ο€ and NatTrans.IsMonoOnNilp Ο€ assert that the component at B is bijective, respectively injective, for every \mathcal{O}-algebra B in which \pi has nilpotent image.

The charts are then defined for \pi \in \mathcal{O} and q \in \mathbb{N}: chartV π’ͺ q sends B to \{\zeta \in B : \zeta^{q}-\zeta \in B^{\times}\}; chartE π’ͺ Ο€ q sends B to the set of pairs (\xi,\eta) \in B^{2} with \xi\eta equal to the image of \pi and \xi^{q-1}-1, \eta^{q-1}-1 both units; chartVUnit π’ͺ q imposes on \zeta additionally that \zeta be a unit, and chartVUnitIncl is the natural transformation forgetting that extra condition. Two arithmetic lemmas are proved: if 1 \le q and \zeta^{q}-\zeta is a unit then so is \zeta^{q-1}-1 (by the factorisation \zeta^q-\zeta = \zeta(\zeta^{q-1}-1)), and (ab)^{n+1}-1 is a unit whenever a is nilpotent. They feed vertexToEdge: for 2 \le q and an \mathcal{O}-algebra B in which the image of \pi is nilpotent, the map \zeta \mapsto (\zeta, \pi\zeta^{-1}) from chartVUnit to chartE at B; vertexToEdge_natural states its compatibility with any \mathcal{O}-algebra map f : B \to B' between two such algebras, so that it is a natural transformation over the \pi-nilpotent algebras, where it is defined. Finally, for a prime r, padicChartV and padicChartE are the instances with \mathcal{O} = \mathbb{Z}_{r}, \pi = r, q = r, and SpecialFibreVertexChartShape r is the Prop asserting that for every field \mathbb{F} that is a \mathbb{Z}_{r}-algebra of characteristic r and every \zeta \in \mathbb{F}, \zeta^{r}-\zeta is a unit if and only if \zeta avoids the images of all a \in \mathbb{Z}/r.

Relation to Mathlib

The constructions here are independent of Mathlib's category-theory library: AlgFunctor, its natural transformations, products, corepresentable objects and group actions form the project's own hand-rolled notion of a functor from commutative \mathcal{O}-algebras to types, and the chart functors are project-specific.

Where it is used

These are the two affine charts of the formal model of Drinfeld's p-adic upper half plane β€” the formal affine line with the q rational residue discs removed, and the formal node \xi\eta = \pi with the rational points of the two branches removed β€” glued along the map \zeta \mapsto (\zeta,\pi\zeta^{-1}) on algebras where \pi is nilpotent. They underlie the Čerednik–Drinfeld description of Shimura curves by quotients indexed by the Bruhat–Tits tree, which supplies the local geometry used in the level-lowering part of the argument.

References

  1. 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, I Β§4
  2. V. G. Drinfeld, Coverings of p-adic symmetric domains, Functional Analysis and its Applications 10 (1976), 107–115

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_LatticeTreeOrbital
import Definitions.Def_CerednikDrinfeld_BruhatTitsTree

set_option autoImplicit false

namespace CerednikDrinfeld
namespace FormalOmega

structure AlgFunctor (π’ͺ : Type) [CommRing π’ͺ] : Type 1 where

  obj : βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B], Type

  map : βˆ€ {B : Type} [CommRing B] [Algebra π’ͺ B] {B' : Type} [CommRing B'] [Algebra π’ͺ B'],
    (B →ₐ[π’ͺ] B') β†’ obj B β†’ obj B'

  map_id : βˆ€ {B : Type} [CommRing B] [Algebra π’ͺ B] (x : obj B), map (AlgHom.id π’ͺ B) x = x

  map_comp : βˆ€ {B₁ : Type} [CommRing B₁] [Algebra π’ͺ B₁] {Bβ‚‚ : Type} [CommRing Bβ‚‚] [Algebra π’ͺ Bβ‚‚]
    {B₃ : Type} [CommRing B₃] [Algebra π’ͺ B₃] (f : B₁ →ₐ[π’ͺ] Bβ‚‚) (g : Bβ‚‚ →ₐ[π’ͺ] B₃) (x : obj B₁),
    map (g.comp f) x = map g (map f x)

namespace AlgFunctor

variable {π’ͺ : Type} [CommRing π’ͺ]

structure NatTrans (F G : AlgFunctor π’ͺ) : Type 1 where

  app : βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B], F.obj B β†’ G.obj B

  naturality : βˆ€ {B : Type} [CommRing B] [Algebra π’ͺ B] {B' : Type} [CommRing B'] [Algebra π’ͺ B']
    (f : B →ₐ[π’ͺ] B') (x : F.obj B), app B' (F.map f x) = G.map f (app B x)

def NatTrans.id (F : AlgFunctor π’ͺ) : NatTrans F F where
  app := fun _ _ _ x => x
  naturality _ _ := rfl

def NatTrans.comp {F G H : AlgFunctor π’ͺ} (Ξ· : NatTrans F G) (ΞΈ : NatTrans G H) : NatTrans F H where
  app := fun B _ _ x => ΞΈ.app B (Ξ·.app B x)
  naturality f x := by rw [Ξ·.naturality, ΞΈ.naturality]

def NatTrans.IsIsoOnNilp (Ο€ : π’ͺ) {F G : AlgFunctor π’ͺ} (Ξ· : NatTrans F G) : Prop :=
  βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B], IsNilpotent (algebraMap π’ͺ B Ο€) β†’ Function.Bijective (Ξ·.app B)

def NatTrans.IsMonoOnNilp (Ο€ : π’ͺ) {F G : AlgFunctor π’ͺ} (Ξ· : NatTrans F G) : Prop :=
  βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B], IsNilpotent (algebraMap π’ͺ B Ο€) β†’ Function.Injective (Ξ·.app B)

def prod (F G : AlgFunctor π’ͺ) : AlgFunctor π’ͺ where
  obj B := F.obj B Γ— G.obj B
  map f x := (F.map f x.1, G.map f x.2)
  map_id x := by rw [F.map_id, G.map_id]
  map_comp f g x := by rw [F.map_comp, G.map_comp]

def corep (A : Type) [CommRing A] [Algebra π’ͺ A] : AlgFunctor π’ͺ where
  obj B := A →ₐ[π’ͺ] B
  map f ψ := f.comp ψ
  map_id _ := AlgHom.ext fun _ => rfl
  map_comp _ _ _ := AlgHom.ext fun _ => rfl

structure GroupAction (Ξ“ : Type) [Group Ξ“] (F : AlgFunctor π’ͺ) : Type 1 where

  act : βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B], Ξ“ β†’ F.obj B β†’ F.obj B
  act_one : βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B] (x : F.obj B), act B 1 x = x
  act_mul : βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B] (g h : Ξ“) (x : F.obj B), act B (g * h) x = act B g (act B h x)

  act_map : βˆ€ {B : Type} [CommRing B] [Algebra π’ͺ B] {B' : Type} [CommRing B'] [Algebra π’ͺ B']
    (f : B →ₐ[π’ͺ] B') (g : Ξ“) (x : F.obj B), F.map f (act B g x) = act B' g (F.map f x)

end AlgFunctor

section Charts

variable (π’ͺ : Type) [CommRing π’ͺ]

def chartV (q : β„•) : AlgFunctor π’ͺ where
  obj B := { ΞΆ : B // IsUnit (ΞΆ ^ q - ΞΆ) }
  map f x := ⟨f x.1, by
    have h := x.2.map f
    rwa [map_sub, map_pow] at h⟩
  map_id _ := Subtype.ext rfl
  map_comp _ _ _ := Subtype.ext rfl

def chartE (Ο€ : π’ͺ) (q : β„•) : AlgFunctor π’ͺ where
  obj B := { p : B Γ— B // p.1 * p.2 = algebraMap π’ͺ B Ο€ ∧ IsUnit (p.1 ^ (q - 1) - 1) ∧ IsUnit (p.2 ^ (q - 1) - 1) }
  map f x := ⟨(f x.1.1, f x.1.2), by
    obtain ⟨h₁, hβ‚‚, hβ‚ƒβŸ© := x.2
    refine ⟨?_, ?_, ?_⟩
    Β· rw [← map_mul, h₁, AlgHom.commutes]
    Β· have h := hβ‚‚.map f
      rwa [map_sub, map_pow, map_one] at h
    Β· have h := h₃.map f
      rwa [map_sub, map_pow, map_one] at h⟩
  map_id _ := Subtype.ext rfl
  map_comp _ _ _ := Subtype.ext rfl

def chartVUnit (q : β„•) : AlgFunctor π’ͺ where
  obj B := { ΢ : B // IsUnit (΢ ^ q - ΢) ∧ IsUnit ΢ }
  map f x := ⟨f x.1, by
    obtain ⟨h₁, hβ‚‚βŸ© := x.2
    refine ⟨?_, hβ‚‚.map f⟩
    have h := h₁.map f
    rwa [map_sub, map_pow] at h⟩
  map_id _ := Subtype.ext rfl
  map_comp _ _ _ := Subtype.ext rfl

def chartVUnitIncl (q : β„•) : AlgFunctor.NatTrans (chartVUnit π’ͺ q) (chartV π’ͺ q) where
  app := fun _ _ _ x => ⟨x.1, x.2.1⟩
  naturality _ _ := Subtype.ext rfl

variable {π’ͺ}

theorem isUnit_pow_pred_sub_one_of_isUnit_pow_sub {B : Type} [CommRing B] {q : β„•} (hq : 1 ≀ q) {ΞΆ : B}
    (h : IsUnit (ΞΆ ^ q - ΞΆ)) : IsUnit (ΞΆ ^ (q - 1) - 1) := by
  have hpow : ΞΆ ^ q = ΞΆ ^ (q - 1) * ΞΆ := by
    rw [← pow_succ, Nat.sub_add_cancel hq]
  have hfac : ΞΆ ^ q - ΞΆ = ΞΆ * (ΞΆ ^ (q - 1) - 1) := by
    rw [hpow]; ring
  rw [hfac] at h
  exact isUnit_of_mul_isUnit_right h

theorem isUnit_pow_succ_sub_one_of_isNilpotent {B : Type} [CommRing B] {a : B} (ha : IsNilpotent a) (b : B) (n : β„•) :
    IsUnit ((a * b) ^ (n + 1) - 1) := by
  have hab : IsNilpotent (a * b) := Commute.isNilpotent_mul_right (Commute.all a b) ha
  have hpow : IsNilpotent ((a * b) ^ (n + 1)) := by
    obtain ⟨m, hm⟩ := hab
    exact ⟨m, by rw [← pow_mul, Nat.mul_comm (n + 1) m, pow_mul, hm, zero_pow (Nat.succ_ne_zero n)]⟩
  exact hpow.isUnit_sub_one

noncomputable def vertexToEdge (Ο€ : π’ͺ) {q : β„•} (hq : 2 ≀ q) (B : Type) [CommRing B] [Algebra π’ͺ B]
    (hB : IsNilpotent (algebraMap π’ͺ B Ο€)) (x : (chartVUnit π’ͺ q).obj B) : (chartE π’ͺ Ο€ q).obj B :=
  ⟨(x.1, algebraMap π’ͺ B Ο€ * ↑(x.2.2.unit⁻¹)), by
    refine ⟨?_, ?_, ?_⟩
    Β·
      calc x.1 * (algebraMap π’ͺ B Ο€ * ↑(x.2.2.unit⁻¹))
          = algebraMap π’ͺ B Ο€ * (x.1 * ↑(x.2.2.unit⁻¹)) := by ring
        _ = algebraMap π’ͺ B Ο€ := by rw [IsUnit.mul_val_inv, mul_one]
    Β· exact isUnit_pow_pred_sub_one_of_isUnit_pow_sub (le_trans (by norm_num) hq) x.2.1
    Β· obtain ⟨n, hn⟩ : βˆƒ n, q - 1 = n + 1 := ⟨q - 2, by omega⟩
      rw [hn]
      exact isUnit_pow_succ_sub_one_of_isNilpotent hB _ n⟩

theorem vertexToEdge_natural (Ο€ : π’ͺ) {q : β„•} (hq : 2 ≀ q) {B : Type} [CommRing B] [Algebra π’ͺ B] {B' : Type} [CommRing B']
    [Algebra π’ͺ B'] (hB : IsNilpotent (algebraMap π’ͺ B Ο€)) (hB' : IsNilpotent (algebraMap π’ͺ B' Ο€)) (f : B →ₐ[π’ͺ] B')
    (x : (chartVUnit π’ͺ q).obj B) :
    (chartE π’ͺ Ο€ q).map f (vertexToEdge Ο€ hq B hB x) = vertexToEdge Ο€ hq B' hB' ((chartVUnit π’ͺ q).map f x) := by
  apply Subtype.ext

  refine Prod.ext rfl ?_
  show f (algebraMap π’ͺ B Ο€ * ↑(x.2.2.unit⁻¹)) = algebraMap π’ͺ B' Ο€ * ↑(((chartVUnit π’ͺ q).map f x).2.2.unit⁻¹)
  rw [map_mul, AlgHom.commutes]
  congr 1
  have h1 : f x.1 * f ↑(x.2.2.unit⁻¹) = 1 := by
    rw [← map_mul, IsUnit.mul_val_inv, map_one]
  have h2 : f x.1 * ↑(((chartVUnit π’ͺ q).map f x).2.2.unit⁻¹) = 1 := by
    exact IsUnit.mul_val_inv _
  exact (IsUnit.mul_right_injective (x.2.2.map f)) (h1.trans h2.symm)

end Charts

section PadicInstance

variable (r : β„•) [Fact r.Prime]

noncomputable abbrev padicChartV : AlgFunctor β„€_[r] := chartV β„€_[r] r

noncomputable abbrev padicChartE : AlgFunctor β„€_[r] := chartE β„€_[r] (r : β„€_[r]) r

def SpecialFibreVertexChartShape : Prop :=
  βˆ€ (𝔽 : Type) [Field 𝔽] [Algebra β„€_[r] 𝔽] [CharP 𝔽 r] (ΞΆ : 𝔽),
    IsUnit (ΞΆ ^ r - ΞΆ) ↔ βˆ€ a : ZMod r, (ΞΆ : 𝔽) β‰  (a.cast : 𝔽)

end PadicInstance

end FormalOmega
end CerednikDrinfeld

Statements phrased using this module (14)