Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Deformation_SplitCoordinates.lean

definition module

Connected–étale splitting data for Honda system lifting

Throughout, \mathcal{O} is a commutative ring with a fixed algebra map to \mathbb{F}_p (p prime), r a natural number, H_1 a Honda system for the element p on \mathcal{O}^r (i.e. commuting \mathcal{O}-linear F,V with FV=VF=p, together with a submodule L satisfying the three Honda axioms), and (G_v)_{v\ge 0} a tower of commutative Hopf \mathbb{F}_p-algebras with bialgebra transition maps s_v\colon G_{v+1}\to G_v and additive maps \pi_v\colon\mathcal{O}^r\to M(G_v) into the Dieudonné module of G_v, the latter being the colimit over n of the groups of truncated Witt-vector covectors u with \Delta u=u\otimes1+1\otimes u.

SplitCoordinates is pure data: integers d,h^c,h^e; towers (G^c_v,s^c_v) and (G^e_v,s^e_v) of commutative Hopf \mathbb{F}_p-algebras; bialgebra maps q^c_v\colon G_v\to G^c_v, \pi^e_v\colon G_v\to G^e_v, a section \sigma_v\colon G^e_v\to G_v, and \Theta_v\colon G_v\to G^c_v\otimes_{\mathbb{F}_p}G^e_v; a d-dimensional formal group law \Phi_0 over \mathbb{F}_p with presentations \kappa_v\colon\mathbb{F}_p[[X_1,\dots,X_d]]\to G^c_v; a tower (E_v,s^t_v) of Hopf \mathcal{O}-algebras with maps \theta^e_v\colon\mathbb{F}_p\otimes_{\mathcal{O}}E_v\to G^e_v and elements \hat c_{i,k,v}\in E_v; submodules M^c,M^{et}\subseteq\mathcal{O}^r, an \mathcal{O}-basis \alpha of L indexed by \mathrm{Fin}\,d, and power series \bar a_{i,k} over \mathbb{F}_p with lifts a_{i,k} over \mathcal{O}.

The predicate Lawful collects, as fields, the identities that make such a datum a connected–étale splitting with coordinates; its hypotheses are grouped as follows, and the groups are summarised. (i) h^c+h^e=r, the p-divisible tower axioms for G^c and G^e (local resp. reduced and formally unramified levels, cocommutative, finite, surjective transitions with kernels the p^v-torsion ideals, ranks p^{vh^c}, p^{vh^e}). (ii) q^c_v,\pi^e_v surjective, \ker\pi^e_v the nilradical, \pi^e_v\circ\sigma_v=\mathrm{id}, \ker q^c_v the ideal generated by \sigma_v of the augmentation ideal, \Theta_v bijective and equal to comultiplication followed by q^c_v\otimes\pi^e_v, and compatibility of q^c,\pi^e,\sigma,\Theta with all transitions. (iii) \Phi_0 commutative, \kappa_v surjective with kernel the ideal generated by the p^v-series of \Phi_0, compatible with s^c_v, given by adic evaluation, with comultiplication of \kappa_v(X_i) computed by the group law, rank p^{h^c} for the quotient by the p-series, d the cotangent rank of the augmentation ideal of G^c_1, kernels of \kappa_v eventually inside arbitrary powers of (X), and joint injectivity and surjectivity onto the inverse limit. (iv) E_v cocommutative, finite free and formally étale over \mathcal{O}, s^t_v surjective with p^v-torsion kernel, \theta^e_v bijective and transition-compatible, and the lifting property that for every p-adically complete \mathcal{O}-algebra reduction mod p is a bijection on \mathcal{O}-algebra maps out of E_v. (v) Witt-coordinate realisations: for each v,i the image of \pi_v(\alpha_i) under \pi^e_v (resp. q^c_v) is represented by a covector of some length n whose (n-1-k)-th coefficient is \theta^e_v(1\otimes\hat c_{i,k,v}) (resp. \kappa_v(\bar a_{i,k})), these terms vanishing for k\ge n. (vi) The Fitting splitting: M^c and M^{et} are complementary, F- and V-stable, free of ranks h^c,h^e, with F^N M^c\subseteq pM^c for some N, F bijective-type behaviour on M^{et}, the divisibility characterisations of membership in M^c and M^{et}, L\cap M^{et}=0, the Honda axioms for the projection of L into M^c along M^{et}, and vanishing of \pi_v composed with \pi^e_v on M^c and with q^c_v on M^{et}. (vii) Normalisations of the coefficient series: a_{i,k} reduces to \bar a_{i,k}, has zero constant term, and \bar a_{i,k}\to0 adically.

The second predicate, NormalForm, constrains the lifted series: the linear part of (a_{i,0})_i reduces mod p to the identity, and the (i,j) entries of the linear part of (a_{i,1})_i with j\le i lie in (p).

Relation to Mathlib

Mathlib has no notion of Honda systems, of Dieudonné modules of towers of Hopf algebras, or of connected–étale splittings; these are the project's own, built on Mathlib's bialgebra and Hopf algebra API, truncated Witt vectors and multivariate power series. The p^v-torsion ideals occurring in the transition-kernel conditions are those of the project's PDivisibleGroup.Hopf development, defined as the image of the augmentation ideal under the p^v-fold convolution power of the identity.

Where it is used

These data package Fontaine's connected–étale splitting with coordinates, used in formalising the classification of p-divisible groups and finite flat group schemes in characteristic p by Honda systems. That classification underlies the analysis of the local-at-p deformation conditions in the Galois deformation theory of the Frey curve.

References

  1. J.-M. Fontaine, Groupes p-divisibles sur les corps locaux, Astérisque 47–48, Société Mathématique de France, 1977, Ch. IV §1
  2. J. T. Tate, p-divisible groups, in: Proceedings of a Conference on Local Fields (Driebergen, 1966), Springer, 1967, 158–183
  3. B. Conrad, Finite group schemes over bases with low ramification, Compositio Mathematica 119 (1999), 239–320

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_Dieudonne_DatumAndHonda
import Definitions.Def_Dieudonne_WittVectorHom
import Definitions.Def_Dieudonne_WittHomColimit
import Definitions.Def_PDivisibleGroup_Basic
import Definitions.Def_MvFormalGroup_BasicV2
import Definitions.Def_MvFormalGroup_PointsV2

set_option autoImplicit false

open scoped TensorProduct
open MvPowerSeries

universe u v

namespace Deformation.HondaSystem

variable {𝓞 : Type u} [CommRing 𝓞] (p : ℕ) [Fact p.Prime] [Algebra 𝓞 (ZMod p)]
variable (r : ℕ) (H₁ : Deformation.HondaSystem (p : 𝓞) (Fin r → 𝓞))
variable (G : ℕ → Type v) [∀ v, CommRing (G v)] [∀ v, HopfAlgebra (ZMod p) (G v)]

structure SplitCoordinates (s : ∀ v, G (v + 1) →ₐc[ZMod p] G v)
    (π : ∀ v, (Fin r → 𝓞) →+ Deformation.DieudonneModule (ZMod p) p (G v)) where

  d : ℕ

  hc : ℕ
  he : ℕ

  Gc : ℕ → Type v
  Ge : ℕ → Type v
  [instCommRingGc : ∀ v, CommRing (Gc v)]
  [instHopfGc : ∀ v, HopfAlgebra (ZMod p) (Gc v)]
  [instCommRingGe : ∀ v, CommRing (Ge v)]
  [instHopfGe : ∀ v, HopfAlgebra (ZMod p) (Ge v)]
  sc : ∀ v, Gc (v + 1) →ₐc[ZMod p] Gc v
  se : ∀ v, Ge (v + 1) →ₐc[ZMod p] Ge v

  qc : ∀ v, G v →ₐc[ZMod p] Gc v

  πe : ∀ v, G v →ₐc[ZMod p] Ge v

  σ : ∀ v, Ge v →ₐc[ZMod p] G v

  Θ : ∀ v, G v →ₐc[ZMod p] Gc v ⊗[ZMod p] Ge v

  Φ₀ : MvFormalGroup d (ZMod p)
  κ : ∀ v, MvPowerSeries (Fin d) (ZMod p) →ₐ[ZMod p] Gc v

  Et : ℕ → Type u
  [instCommRingEt : ∀ v, CommRing (Et v)]
  [instHopfEt : ∀ v, HopfAlgebra 𝓞 (Et v)]
  st : ∀ v, Et (v + 1) →ₐc[𝓞] Et v
  θe : ∀ v, ZMod p ⊗[𝓞] Et v →ₐc[ZMod p] Ge v

  ĉ : Fin d → ℕ → ∀ v, Et v

  Mc : Submodule 𝓞 (Fin r → 𝓞)
  Met : Submodule 𝓞 (Fin r → 𝓞)
  α : Module.Basis (Fin d) 𝓞 H₁.L
  abar : Fin d → ℕ → MvPowerSeries (Fin d) (ZMod p)
  a : Fin d → ℕ → MvPowerSeries (Fin d) 𝓞

attribute [instance] SplitCoordinates.instCommRingGc SplitCoordinates.instHopfGc
  SplitCoordinates.instCommRingGe SplitCoordinates.instHopfGe
  SplitCoordinates.instCommRingEt SplitCoordinates.instHopfEt

namespace SplitCoordinates

variable {p r H₁ G s π}
variable (𝒮 : SplitCoordinates p r H₁ G s π)

structure Lawful : Prop where

  hc_add_he : 𝒮.hc + 𝒮.he = r
  isLocalRing_Gc : ∀ v, IsLocalRing (𝒮.Gc v)
  isReduced_Ge : ∀ v, IsReduced (𝒮.Ge v)
  isCocomm_Gc : ∀ v, Coalgebra.IsCocomm (ZMod p) (𝒮.Gc v)
  isCocomm_Ge : ∀ v, Coalgebra.IsCocomm (ZMod p) (𝒮.Ge v)
  finite_Gc : ∀ v, Module.Finite (ZMod p) (𝒮.Gc v)
  finite_Ge : ∀ v, Module.Finite (ZMod p) (𝒮.Ge v)
  sc_surjective : ∀ v, Function.Surjective (𝒮.sc v)
  se_surjective : ∀ v, Function.Surjective (𝒮.se v)
  finrank_Gc : ∀ v, Module.finrank (ZMod p) (𝒮.Gc v) = p ^ (v * 𝒮.hc)
  finrank_Ge : ∀ v, Module.finrank (ZMod p) (𝒮.Ge v) = p ^ (v * 𝒮.he)
  ker_sc : ∀ v, RingHom.ker (𝒮.sc v) = PDivisibleGroup.Hopf.torsionIdeal (ZMod p) (𝒮.Gc (v + 1)) (p ^ v)
  ker_se : ∀ v, RingHom.ker (𝒮.se v) = PDivisibleGroup.Hopf.torsionIdeal (ZMod p) (𝒮.Ge (v + 1)) (p ^ v)
  qc_surjective : ∀ v, Function.Surjective (𝒮.qc v)
  πe_surjective : ∀ v, Function.Surjective (𝒮.πe v)
  ker_πe : ∀ v, RingHom.ker (𝒮.πe v : G v →ₐ[ZMod p] 𝒮.Ge v) = nilradical (G v)
  πe_comp_σ : ∀ v, (𝒮.πe v).comp (𝒮.σ v) = BialgHom.id (ZMod p) (𝒮.Ge v)
  ker_qc : ∀ v, RingHom.ker (𝒮.qc v : G v →ₐ[ZMod p] 𝒮.Gc v) =
    Ideal.map (𝒮.σ v : 𝒮.Ge v →ₐ[ZMod p] G v) (RingHom.ker (Bialgebra.counitAlgHom (ZMod p) (𝒮.Ge v)))
  Θ_bijective : ∀ v, Function.Bijective (𝒮.Θ v)
  Θ_apply : ∀ v b, 𝒮.Θ v b = Algebra.TensorProduct.map (𝒮.qc v : G v →ₐ[ZMod p] 𝒮.Gc v)
    (𝒮.πe v : G v →ₐ[ZMod p] 𝒮.Ge v) (Coalgebra.comul (R := ZMod p) b)
  qc_comp_s : ∀ v, (𝒮.qc v).comp (s v) = (𝒮.sc v).comp (𝒮.qc (v + 1))
  πe_comp_s : ∀ v, (𝒮.πe v).comp (s v) = (𝒮.se v).comp (𝒮.πe (v + 1))
  s_comp_σ : ∀ v, (s v).comp (𝒮.σ (v + 1)) = (𝒮.σ v).comp (𝒮.se v)

  Θ_comp_s : ∀ v, (𝒮.Θ v).comp (s v) = (Bialgebra.TensorProduct.map (𝒮.sc v) (𝒮.se v)).comp (𝒮.Θ (v + 1))
  formallyUnramified_Ge : ∀ v, Algebra.FormallyUnramified (ZMod p) (𝒮.Ge v)

  isComm_Φ₀ : 𝒮.Φ₀.IsComm
  κ_surjective : ∀ v, Function.Surjective (𝒮.κ v)
  ker_κ : ∀ v, RingHom.ker (𝒮.κ v) = Ideal.span (Set.range (𝒮.Φ₀.nthSeries (p ^ v)))
  sc_comp_κ : ∀ v, (𝒮.sc v : 𝒮.Gc (v + 1) →ₐ[ZMod p] 𝒮.Gc v).comp (𝒮.κ (v + 1)) = 𝒮.κ v
  counit_κ_X : ∀ v i, Coalgebra.counit (R := ZMod p) (𝒮.κ v (X i)) = 0

  κ_X_mem_radical : ∀ v i, 𝒮.κ v (X i) ∈ (Ideal.span {(p : 𝒮.Gc v)}).radical
  κ_eval : ∀ v F, 𝒮.κ v F = MvFormalGroup.adicEval (Ideal.span {(p : 𝒮.Gc v)}) (fun i => 𝒮.κ v (X i)) F
  comul_κ_X : ∀ v i, Coalgebra.comul (R := ZMod p) (𝒮.κ v (X i)) =
    MvFormalGroup.adicEval (Ideal.span {(p : 𝒮.Gc v ⊗[ZMod p] 𝒮.Gc v)})
      (Sum.elim (fun j => 𝒮.κ v (X j) ⊗ₜ[ZMod p] (1 : 𝒮.Gc v)) (fun j => (1 : 𝒮.Gc v) ⊗ₜ[ZMod p] 𝒮.κ v (X j)))
      (𝒮.Φ₀.toPowerSeries i)
  finrank_quot_nthSeries : Module.finrank (ZMod p)
    (MvPowerSeries (Fin 𝒮.d) (ZMod p) ⧸ Ideal.span (Set.range (𝒮.Φ₀.nthSeries p))) = p ^ 𝒮.hc

  d_eq_finrank_cotangent : 𝒮.d = Module.finrank (ZMod p) (PDivisibleGroup.Hopf.augIdeal (ZMod p) (𝒮.Gc 1)).Cotangent
  ker_κ_le_pow : ∀ N : ℕ, ∃ v, RingHom.ker (𝒮.κ v) ≤
    (Ideal.span (Set.range (X : Fin 𝒮.d → MvPowerSeries (Fin 𝒮.d) (ZMod p)))) ^ N
  κ_injective_joint : ∀ F, (∀ v, 𝒮.κ v F = 0) → F = 0
  κ_surjective_joint : ∀ z : ∀ v, 𝒮.Gc v, (∀ v, 𝒮.sc v (z (v + 1)) = z v) → ∃ F, ∀ v, 𝒮.κ v F = z v

  isCocomm_Et : ∀ v, Coalgebra.IsCocomm 𝓞 (𝒮.Et v)
  free_Et : ∀ v, Module.Free 𝓞 (𝒮.Et v)
  finite_Et : ∀ v, Module.Finite 𝓞 (𝒮.Et v)
  formallyEtale_Et : ∀ v, Algebra.FormallyEtale 𝓞 (𝒮.Et v)
  st_surjective : ∀ v, Function.Surjective (𝒮.st v)
  ker_st : ∀ v, RingHom.ker (𝒮.st v) = PDivisibleGroup.Hopf.torsionIdeal 𝓞 (𝒮.Et (v + 1)) (p ^ v)
  θe_bijective : ∀ v, Function.Bijective (𝒮.θe v)
  θe_comp : ∀ v, (𝒮.θe v).comp (Bialgebra.TensorProduct.map (BialgHom.id (ZMod p) (ZMod p)) (𝒮.st v)) =
    (𝒮.se v).comp (𝒮.θe (v + 1))

  bijective_comp_mk : ∀ (g : Type u) [CommRing g] [Algebra 𝓞 g] [IsAdicComplete (Ideal.span {(p : g)}) g] (v : ℕ),
    Function.Bijective fun f : 𝒮.Et v →ₐ[𝓞] g => (Ideal.Quotient.mkₐ 𝓞 (Ideal.span {(p : g)})).comp f

  st_ĉ : ∀ i k v, 𝒮.st v (𝒮.ĉ i k (v + 1)) = 𝒮.ĉ i k v
  counit_ĉ : ∀ i k v, Coalgebra.counit (R := 𝓞) (𝒮.ĉ i k v) = 0

  realisation_etale : ∀ v i, ∃ (n : ℕ) (u : Deformation.wittHom (ZMod p) p n (𝒮.Ge v)),
    Deformation.DieudonneModule.of (ZMod p) p (𝒮.Ge v) n u =
      Deformation.DieudonneModule.map (ZMod p) p (𝒮.πe v) (π v ((𝒮.α i : H₁.L) : Fin r → 𝓞)) ∧
    (∀ (k : ℕ) (hk : k < n), (u : TruncatedWittVector p n (𝒮.Ge v)).coeff ⟨n - 1 - k, by omega⟩ =
      𝒮.θe v ((1 : ZMod p) ⊗ₜ[𝓞] 𝒮.ĉ i k v)) ∧
    (∀ k, n ≤ k → 𝒮.θe v ((1 : ZMod p) ⊗ₜ[𝓞] 𝒮.ĉ i k v) = 0)

  isCompl : IsCompl 𝒮.Mc 𝒮.Met
  F_mem_Mc : ∀ m ∈ 𝒮.Mc, H₁.F m ∈ 𝒮.Mc
  V_mem_Mc : ∀ m ∈ 𝒮.Mc, H₁.V m ∈ 𝒮.Mc
  F_mem_Met : ∀ m ∈ 𝒮.Met, H₁.F m ∈ 𝒮.Met
  V_mem_Met : ∀ m ∈ 𝒮.Met, H₁.V m ∈ 𝒮.Met

  pow_F_Mc : ∃ N : ℕ, ∀ m ∈ 𝒮.Mc, ∃ y ∈ 𝒮.Mc, (H₁.F ^ N) m = (p : 𝓞) • y

  F_surjOn_Met : ∀ m ∈ 𝒮.Met, ∃ m' ∈ 𝒮.Met, H₁.F m' = m
  Met_le_range_F : 𝒮.Met ≤ LinearMap.range H₁.F

  mem_Met_iff : ∀ m, m ∈ 𝒮.Met ↔ ∀ N : ℕ, ∃ y, (H₁.F ^ N) y = m
  mem_Mc_iff : ∀ m, m ∈ 𝒮.Mc ↔ ∀ k : ℕ, ∃ N : ℕ, ∃ y, (H₁.F ^ N) m = (p : 𝓞) ^ k • y

  free_Mc : Module.Free 𝓞 𝒮.Mc
  free_Met : Module.Free 𝓞 𝒮.Met
  finrank_Mc : Module.finrank 𝓞 𝒮.Mc = 𝒮.hc
  finrank_Met : Module.finrank 𝓞 𝒮.Met = 𝒮.he

  L_inf_Met : H₁.L ⊓ 𝒮.Met = ⊥

  sh1_le_Lc : ∀ x ∈ (H₁.L).map (𝒮.Mc.subtype ∘ₗ Submodule.projectionOnto 𝒮.Mc 𝒮.Met isCompl),
    x ∈ LinearMap.range H₁.F →
      ∃ y ∈ (H₁.L).map (𝒮.Mc.subtype ∘ₗ Submodule.projectionOnto 𝒮.Mc 𝒮.Met isCompl), x = (p : 𝓞) • y
  sh1_ge_Lc : ∀ y ∈ (H₁.L).map (𝒮.Mc.subtype ∘ₗ Submodule.projectionOnto 𝒮.Mc 𝒮.Met isCompl),
    (p : 𝓞) • y ∈ LinearMap.range H₁.F
  sh2_Lc : LinearMap.range H₁.F ⊔ (H₁.L).map (𝒮.Mc.subtype ∘ₗ Submodule.projectionOnto 𝒮.Mc 𝒮.Met isCompl) = ⊤

  map_πe_π_eq_zero : ∀ v, ∀ m ∈ 𝒮.Mc, Deformation.DieudonneModule.map (ZMod p) p (𝒮.πe v) (π v m) = 0
  map_qc_π_eq_zero : ∀ v, ∀ m ∈ 𝒮.Met, Deformation.DieudonneModule.map (ZMod p) p (𝒮.qc v) (π v m) = 0

  a_map : ∀ i k, (𝒮.a i k).map (algebraMap 𝓞 (ZMod p)) = 𝒮.abar i k
  constantCoeff_a : ∀ i k, MvPowerSeries.constantCoeff (𝒮.a i k) = 0
  abar_tendsto : ∀ i N, ∃ k₀, ∀ k, k₀ ≤ k →
    𝒮.abar i k ∈ (Ideal.span (Set.range (X : Fin 𝒮.d → MvPowerSeries (Fin 𝒮.d) (ZMod p)))) ^ N
  realisation_conn : ∀ v i, ∃ (n : ℕ) (u : Deformation.wittHom (ZMod p) p n (𝒮.Gc v)),
    Deformation.DieudonneModule.of (ZMod p) p (𝒮.Gc v) n u =
      Deformation.DieudonneModule.map (ZMod p) p (𝒮.qc v) (π v ((𝒮.α i : H₁.L) : Fin r → 𝓞)) ∧
    (∀ (k : ℕ) (hk : k < n), (u : TruncatedWittVector p n (𝒮.Gc v)).coeff ⟨n - 1 - k, by omega⟩ = 𝒮.κ v (𝒮.abar i k)) ∧
    (∀ k, n ≤ k → 𝒮.κ v (𝒮.abar i k) = 0)

structure NormalForm : Prop where
  linearPart_zero : (MvFormalGroup.linearPart fun i => 𝒮.a i 0).map (Ideal.Quotient.mk (Ideal.span {(p : 𝓞)})) = 1
  linearPart_one : ∀ i j : Fin 𝒮.d, j ≤ i → MvFormalGroup.linearPart (fun i => 𝒮.a i 1) i j ∈ Ideal.span {(p : 𝓞)}

end SplitCoordinates

end Deformation.HondaSystem

Statements phrased using this module (9)