Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_PDivisibleGroup_BaseChange.lean

definition module

Base change of p-divisible groups in the Hopf-algebra model

Throughout, R is a commutative ring, S a commutative R-algebra, and A a commutative R-bialgebra; G is a PDivisibleGroup R p h, i.e. a tower of finite free cocommutative Hopf R-algebras G.level v of rank p^{vh} together with surjective bialgebra maps G.transition v : G.level (v+1) →ₐc[R] G.level v whose kernels are the ideals Hopf.torsionIdeal R (G.level (v+1)) (p ^ v), the image of the augmentation ideal \ker\varepsilon under the n-fold convolution power Hopf.nsmulAlgHom of the identity (the comorphism of multiplication by n).

The first group of results identifies these data after tensoring. On S\otimes_R A one has nsmulAlgHom S (S ⊗[R] A) n (s ⊗ₜ a) = s ⊗ₜ nsmulAlgHom R A n a, hence nsmulAlgHom S (S ⊗[R] A) n is \mathrm{id}_S\otimes[n]^{*}; the counit over S is \mathrm{id}_S\otimes\varepsilon followed by the canonical isomorphism S\otimes_R S\cong S; and both the augmentation ideal and the n-torsion ideal of S\otimes_R A are the ideals generated by those of A under Algebra.TensorProduct.includeRight. Likewise the kernel of \mathrm{id}_S\otimes G.transition v is generated by \ker(G.transition v).

With these, PDivisibleGroup.baseChange is defined, for S nontrivial: the p-divisible group over S of the same height with levels S\otimes_R G.level v and transitions \mathrm{id}_S\otimes G.transition v; surjectivity is preserved, the rank axiom follows from invariance of the rank of a free module under base change (nontriviality of S forcing R nontrivial), and the kernel axiom from the ideal computations. Equations for levels and transitions are recorded.

Finally, cotangentToBaseChange is the R-linear map on I/I^2 induced by includeRight, sending the class of x to that of 1\otimes x, and cotangentBaseChange is its S-linear extension S\otimes_R G.Cotangent v \to \mathrm{Cotangent} of the augmentation ideal of S\otimes_R G.level v; no bijectivity is asserted here.

Relation to Mathlib

Mathlib has no notion of p-divisible group; the structure PDivisibleGroup and the convolution power Hopf.nsmulAlgHom are the project's own, built on Mathlib's Bialgebra/HopfAlgebra, WithConv, Algebra.TensorProduct and Ideal.Cotangent/Ideal.mapCotangent.

Where it is used

These constructions allow a p-divisible group over a ring to be transported along scalar extensions, for instance from a local ring to its residue field or to a completion, which is how the local theory at p is reduced to simpler base rings in the analysis of the deformation conditions entering the modularity lifting argument.

References

  1. J. Tate, p-divisible groups, in: Proceedings of a Conference on Local Fields (Driebergen, 1966), Springer, 1967, 158–183
  2. W. Messing, The Crystals Associated to Barsotti–Tate Groups, Lecture Notes in Mathematics 264, Springer, 1972

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_PDivisibleGroup_Dimension

set_option autoImplicit false

noncomputable section

open scoped TensorProduct
open Coalgebra Bialgebra WithConv

universe u v w

namespace PDivisibleGroup.Hopf

section BaseChange

variable (R : Type u) [CommRing R] (S : Type w) [CommRing S] [Algebra R S]
  (A : Type v) [CommRing A] [Bialgebra R A]

theorem nsmulAlgHom_baseChange_tmul (n : ℕ) (s : S) (a : A) :
    nsmulAlgHom S (S ⊗[R] A) n (s ⊗ₜ[R] a) = s ⊗ₜ[R] nsmulAlgHom R A n a := by
  induction n generalizing s a with
  | zero =>
    rw [nsmulAlgHom_zero_apply, nsmulAlgHom_zero_apply, TensorProduct.counit_tmul,
      CommSemiring.counit_apply, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHom.id_apply, Algebra.algebraMap_eq_smul_one]
    rw [TensorProduct.smul_tmul]
  | succ n ih =>
    rw [nsmulAlgHom_succ, nsmulAlgHom_succ]
    change (toConv (nsmulAlgHom S (S ⊗[R] A) n) * toConv (AlgHom.id S (S ⊗[R] A))) (s ⊗ₜ[R] a) =
      s ⊗ₜ[R] (toConv (nsmulAlgHom R A n) * toConv (AlgHom.id R A)) a
    rw [AlgHom.convMul_apply, AlgHom.convMul_apply, TensorProduct.comul_tmul,
      CommSemiring.comul_apply]
    obtain ⟨ι, t, f, g, hrep⟩ :=
      (⟨_, _, _, _, (Coalgebra.Repr.arbitrary R a).eq⟩ :
        ∃ (ι : Type v) (t : Finset ι) (f g : ι → A), ∑ i ∈ t, f i ⊗ₜ[R] g i = comul (R := R) a)
    rw [← hrep, TensorProduct.tmul_sum, map_sum, map_sum, map_sum, TensorProduct.tmul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul, Algebra.TensorProduct.lift_tmul,
      Algebra.TensorProduct.lift_tmul]
    change nsmulAlgHom S (S ⊗[R] A) n ((1 : S) ⊗ₜ[R] f i) * (s ⊗ₜ[R] g i) =
      s ⊗ₜ[R] (nsmulAlgHom R A n (f i) * g i)
    rw [ih, Algebra.TensorProduct.tmul_mul_tmul, one_mul]

theorem nsmulAlgHom_baseChange (n : ℕ) :
    nsmulAlgHom S (S ⊗[R] A) n =
      Algebra.TensorProduct.map (AlgHom.id S S) (nsmulAlgHom R A n) := by
  ext a
  change nsmulAlgHom S (S ⊗[R] A) n ((1 : S) ⊗ₜ[R] a) = (1 : S) ⊗ₜ[R] nsmulAlgHom R A n a
  exact nsmulAlgHom_baseChange_tmul R S A n 1 a

theorem counit_baseChange_eq (x : S ⊗[R] A) :
    counit (R := S) x =
      Algebra.TensorProduct.rid R S S
        (Algebra.TensorProduct.map (AlgHom.id S S) (counitAlgHom R A) x) := by
  induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul s a =>
    rw [TensorProduct.counit_tmul, CommSemiring.counit_apply, Algebra.TensorProduct.map_tmul,
      Algebra.TensorProduct.rid_tmul]
    rfl
  | add x y hx hy => rw [map_add, hx, hy, map_add, map_add]

theorem augIdeal_baseChange :
    augIdeal S (S ⊗[R] A) =
      (augIdeal R A).map (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A) := by
  have hsurj : Function.Surjective (counitAlgHom R A) := fun r =>
    ⟨algebraMap R A r, by rw [Bialgebra.counitAlgHom_apply, counit_algebraMap]⟩
  have hker := Algebra.TensorProduct.lTensor_ker (A := S) (counitAlgHom R A) hsurj
  change RingHom.ker (counitAlgHom S (S ⊗[R] A)) = (RingHom.ker (counitAlgHom R A)).map _
  rw [← hker]
  ext x
  rw [RingHom.mem_ker, RingHom.mem_ker, Bialgebra.counitAlgHom_apply, counit_baseChange_eq]
  have hmaps : Algebra.TensorProduct.map (AlgHom.id S S) (counitAlgHom R A) x =
      Algebra.TensorProduct.map (AlgHom.id R S) (counitAlgHom R A) x := by
    induction x using TensorProduct.induction_on with
    | zero => simp only [map_zero]
    | tmul s a => rfl
    | add x y hx hy => rw [map_add, map_add, hx, hy]
  rw [← hmaps]
  exact (Algebra.TensorProduct.rid R S S).map_eq_zero_iff

theorem torsionIdeal_baseChange (n : ℕ) :
    torsionIdeal S (S ⊗[R] A) n =
      (torsionIdeal R A n).map (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A) := by
  rw [torsionIdeal, torsionIdeal, augIdeal_baseChange]
  change ((augIdeal R A).map (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A).toRingHom).map
      (nsmulAlgHom S (S ⊗[R] A) n).toRingHom =
    ((augIdeal R A).map (nsmulAlgHom R A n).toRingHom).map
      (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A).toRingHom
  rw [Ideal.map_map, Ideal.map_map]
  congr 1
  refine RingHom.ext fun a => ?_
  change nsmulAlgHom S (S ⊗[R] A) n ((1 : S) ⊗ₜ[R] a) = (1 : S) ⊗ₜ[R] nsmulAlgHom R A n a
  exact nsmulAlgHom_baseChange_tmul R S A n 1 a

end BaseChange

end PDivisibleGroup.Hopf

namespace PDivisibleGroup

variable {R : Type} [CommRing R] {p h : ℕ} (G : PDivisibleGroup R p h)
  (S : Type) [CommRing S] [Algebra R S]

theorem ker_map_transition (v : ℕ) :
    RingHom.ker (Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v)) =
      (RingHom.ker (G.transition v)).map
        (Algebra.TensorProduct.includeRight : G.level (v + 1) →ₐ[R] S ⊗[R] G.level (v + 1)) := by
  have hker : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R S) (G.transitionAlgHom v)) =
      (RingHom.ker (G.transition v)).map
        (Algebra.TensorProduct.includeRight : G.level (v + 1) →ₐ[R] S ⊗[R] G.level (v + 1)) :=
    Algebra.TensorProduct.lTensor_ker (A := S) (G.transitionAlgHom v) (G.transition_surjective v)
  rw [← hker]
  ext x
  rw [RingHom.mem_ker, RingHom.mem_ker]
  have hmaps : Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v) x =
      Algebra.TensorProduct.map (AlgHom.id R S) (G.transitionAlgHom v) x := by
    induction x using TensorProduct.induction_on with
    | zero => simp only [map_zero]
    | tmul s a => rfl
    | add x y hx hy => rw [map_add, map_add, hx, hy]
  rw [hmaps]

variable [Nontrivial S]

def baseChange : PDivisibleGroup S p h where
  level v := S ⊗[R] G.level v
  transition v := Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v)
  transition_surjective v :=
    Algebra.TensorProduct.map_surjective (AlgHom.id S S) (G.transitionAlgHom v)
      Function.surjective_id (G.transition_surjective v)
  finrank_level v := by
    haveI : Nontrivial R := (algebraMap R S).domain_nontrivial
    rw [Module.finrank_baseChange, G.finrank_level]
  ker_transition v := by
    rw [ker_map_transition, G.ker_transition, Hopf.torsionIdeal_baseChange]

@[simp] theorem baseChange_level (v : ℕ) : (G.baseChange S).level v = (S ⊗[R] G.level v) := rfl

theorem baseChange_transition (v : ℕ) :
    (G.baseChange S).transition v = Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v) :=
  rfl

@[simp] theorem baseChange_transition_tmul (v : ℕ) (s : S) (a : G.level (v + 1)) :
    (G.baseChange S).transition v (s ⊗ₜ[R] a) = s ⊗ₜ[R] G.transition v a := rfl

theorem augIdeal_baseChange (v : ℕ) :
    Hopf.augIdeal S ((G.baseChange S).level v) =
      (Hopf.augIdeal R (G.level v)).map
        (Algebra.TensorProduct.includeRight : G.level v →ₐ[R] S ⊗[R] G.level v) :=
  Hopf.augIdeal_baseChange R S (G.level v)

omit [Nontrivial S] in
theorem augIdeal_le_comap_includeRight (v : ℕ) :
    G.augIdeal v ≤ (Hopf.augIdeal S (S ⊗[R] G.level v)).comap
      (Algebra.TensorProduct.includeRight : G.level v →ₐ[R] S ⊗[R] G.level v) := by
  rw [Hopf.augIdeal_baseChange R S (G.level v)]
  exact Ideal.le_comap_map

theorem baseChange_cotangent_eq (v : ℕ) :
    (G.baseChange S).Cotangent v = (Hopf.augIdeal S (S ⊗[R] G.level v)).Cotangent := rfl

omit [Nontrivial S] in

def cotangentToBaseChange (v : ℕ) :
    G.Cotangent v →ₗ[R] (Hopf.augIdeal S (S ⊗[R] G.level v)).Cotangent :=
  Ideal.mapCotangent (G.augIdeal v) (Hopf.augIdeal S (S ⊗[R] G.level v))
    (Algebra.TensorProduct.includeRight : G.level v →ₐ[R] S ⊗[R] G.level v)
    (G.augIdeal_le_comap_includeRight S v)

omit [Nontrivial S] in
@[simp] theorem cotangentToBaseChange_toCotangent (v : ℕ) (x : G.augIdeal v) :
    G.cotangentToBaseChange S v ((G.augIdeal v).toCotangent x) =
      (Hopf.augIdeal S (S ⊗[R] G.level v)).toCotangent
        ⟨(1 : S) ⊗ₜ[R] (x : G.level v), G.augIdeal_le_comap_includeRight S v x.2⟩ := rfl

omit [Nontrivial S] in

def cotangentBaseChange (v : ℕ) :
    S ⊗[R] G.Cotangent v →ₗ[S] (Hopf.augIdeal S (S ⊗[R] G.level v)).Cotangent :=
  (G.cotangentToBaseChange S v).liftBaseChange S

omit [Nontrivial S] in
@[simp] theorem cotangentBaseChange_tmul (v : ℕ) (s : S) (y : G.Cotangent v) :
    G.cotangentBaseChange S v (s ⊗ₜ[R] y) = s • G.cotangentToBaseChange S v y := by
  rw [cotangentBaseChange, LinearMap.liftBaseChange_tmul]

end PDivisibleGroup

end

Statements phrased using this module (18)