Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_HopfAlgebra_HasFVectDevissage.lean

definition module

Inductive dévissage predicate for Hopf algebras with -vector layers

Fix a local ring R, a field K that is an R-algebra, and a prime p. The module defines a Prop-valued inductive family HopfAlgebra.HasFVectDevissage R K p A, indexed by commutative Hopf K-algebras A, generated by two constructors. The base case nil asserts the predicate for any A with \dim_K A = 1. The inductive case step asserts it for A (commutative, cocommutative and finite-dimensional over K) given: a second such Hopf algebra \bar A, a bialgebra homomorphism \pi\colon A \to \bar A which is surjective as a function; an integer r \neq 0 and a finite field F with \#F = p^{r}; the requirement that p^{r}-1 be a unit of R; a group homomorphism \chi\colon F^{\times}\to R^{\times} and a ring homomorphism \iota\colon F \to R/\mathfrak m_R with \chi(l) \bmod \mathfrak m_R = \iota(l) for all l \in F^{\times}; the rank condition \dim_K H = p^{r}, where H = HopfAlgebra.hopfKer π is the subalgebra \{a \in A : (\mathrm{id}\otimes\pi)(\Delta a) = a \otimes 1\} of A, itself a commutative cocommutative Hopf K-algebra with comultiplication, counit and antipode induced from those of A; a term of HopfAlgebra.FVectStructure F K H, i.e. a family of bialgebra endomorphisms [a] of H indexed by a \in F with [1] = \mathrm{id}, [ab] = [a]\circ[b], [0] equal to the unit of the convolution algebra and [a+b] = [a]\ast[b]; and, recursively, the predicate for \bar A. Thus the predicate records a filtration of A by Hopf quotients whose successive Hopf kernels are of dimension p^{r} and carry an F-vector space structure, together with the data in R (p^{r}-1 invertible, a multiplicative character lifting \iota) needed for Raynaud's normal form.

Relation to Mathlib

Mathlib supplies the ambient notions used here (HopfAlgebra, bialgebra homomorphisms, cocommutativity, and the convolution monoid WithConv), but has no notion of Hopf kernel, of F-vector space structure on a Hopf algebra, or of such a dévissage; these are the project's own, the first two defined in the imported modules.

Where it is used

The predicate is the induction hypothesis on which the project's treatment of Raynaud's theory of group schemes of type (p,\dots,p) runs: the dévissage is produced after a suitable base change, and equality of nested Hopf orders is then proved by induction along it, one F-vector space layer at a time.

References

  1. M. Raynaud, Schémas en groupes de type (p,\dots,p), Bulletin de la Société Mathématique de France 102 (1974), 241–280
  2. M. E. Sweedler, Hopf Algebras, Mathematics Lecture Note Series, Benjamin, 1969

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_HopfAlgebra_HopfKer
import Definitions.Def_HopfAlgebra_HopfKerHopf
import Definitions.Def_HopfAlgebra_FVectStructure

set_option autoImplicit false

universe u v

inductive HopfAlgebra.HasFVectDevissage (R : Type u) [CommRing R] [IsLocalRing R] (K : Type u) [Field K] [Algebra R K]
    (p : ℕ) [Fact p.Prime] : ∀ (A : Type v) [CommRing A] [HopfAlgebra K A], Prop
  | nil (A : Type v) [CommRing A] [HopfAlgebra K A] (h1 : Module.finrank K A = 1) : HasFVectDevissage R K p A
  | step (A : Type v) [CommRing A] [HopfAlgebra K A] [Coalgebra.IsCocomm K A] [Module.Finite K A]
      (Ā : Type v) [CommRing Ā] [HopfAlgebra K Ā] [Coalgebra.IsCocomm K Ā] [Module.Finite K Ā]
      (π : A →ₐc[K] Ā) (hπ : Function.Surjective π)
      (r : ℕ) [NeZero r] (F : Type) [Field F] [Fintype F] (hF : Fintype.card F = p ^ r)
      (hq : IsUnit ((p ^ r : R) - 1))
      (χ : Fˣ →* Rˣ) (ι : F →+* IsLocalRing.ResidueField R)
      (hχ : ∀ l : Fˣ, IsLocalRing.residue R (χ l : R) = ι l)
      (hrank : Module.finrank K ↥(HopfAlgebra.hopfKer π) = p ^ r)
      (σ : HopfAlgebra.FVectStructure F K ↥(HopfAlgebra.hopfKer π))
      (hĀ : HasFVectDevissage R K p Ā) : HasFVectDevissage R K p A

Statements phrased using this module (4)