Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_HopfAlgebra_CharacterClosure.lean

definition module

Vanishing ideals of points, Cartier-dual base change, character closures

Three groups of constructions are made, with no hypotheses beyond the ambient algebra structures.

First, for a commutative ring F, a commutative F-algebra A and a commutative F-algebra L, and a set S of F-algebra maps \nu\colon A\to L, vanishingIdealOfPoints S is the ideal I_S=\{a\in A:\nu(a)=0\ \forall\nu\in S\}; it is antitone in S. Each \nu\in S induces liftPoint \bar\nu\colon A/I_S\to L, and evalPair is the F-algebra map A/I_S\otimes_F A/I_S\to L sending \bar a\otimes\bar b\mapsto \nu(a)\nu'(b) for a chosen pair \nu,\nu'\in S. When A is an F-bialgebra, a submonoid S of the convolution monoid WithConv (A →ₐ[F] L) has underlying point set ptSet S, quotient pointQuot S =A/I_{\mathrm{ptSet}\,S}, and an L-algebra map evalQuot L\otimes_F A/I_{\mathrm{ptSet}\,S}\to (S\to L) with c\otimes\bar a\mapsto(\nu\mapsto c\,\nu(a)).

Second, for O\to F commutative rings and A a commutative O-bialgebra, pointwise formulas record that addition, zero and scalar multiplication on CartierDual are those of the underlying dual module; F\otimes_O \mathrm{CartierDual}\,O\,A is given its ring and F-algebra structure, and \mathrm{CartierDual}\,F\,(F\otimes_O A) is viewed as an O-module by restriction along O\to F. The base change of functionals dualBaseChange sends \varphi to the functional c\otimes a\mapsto c\cdot\mathrm{algebraMap}_{O,F}(\varphi(a)); it is O-linear (dualBaseChangeHom) and extends to the F-linear map dualBaseChangeLin \beta\colon F\otimes_O\mathrm{CartierDual}\,O\,A\to\mathrm{CartierDual}\,F\,(F\otimes_O A), c\otimes\varphi\mapsto c\cdot\mathrm{dualBaseChange}\,\varphi, so \beta(c\otimes\varphi)(c'\otimes a)=cc'\,\mathrm{algebraMap}_{O,F}(\varphi(a)). Only linearity is asserted here.

Third, for a set S of F-algebra maps F\otimes_O A\to L, characterGenericFibre is the F-subalgebra of F\otimes_O\mathrm{CartierDual}\,O\,A generated by \{w:\beta(w)(x)=0\ \forall x\in I_S\}, and, for F a field and A in addition cocommutative, characterClosure is its flatClosure: the O-subalgebra \{g\in\mathrm{CartierDual}\,O\,A: 1\otimes g\in \mathrm{characterGenericFibre}\}. Both are monotone in S.

Relation to Mathlib

Mathlib supplies Module.Dual, the convolution monoid WithConv on dual modules, Algebra.adjoin and Ideal.Quotient.liftₐ; the type CartierDual with its convolution ring structure, the schematic-closure operation flatClosure, the vanishing ideal of a set of algebra-valued points, and the character generic fibre and character closure are the project's own.

Where it is used

The character closure is the intended coordinate ring of the Cartier dual of the schematic closure over O of a set of L-valued points of \mathrm{Spec}(F\otimes_O A), realised as an O-suborder of the Cartier dual of A; it is the vocabulary used when finite subgroups of points are propagated to finite flat Hopf orders in the analysis of group schemes of multiplicative type attached to Galois representations.

References

  1. W. C. Waterhouse, Introduction to Affine Group Schemes, Graduate Texts in Mathematics 66, Springer, 1979
  2. J. Tate and F. Oort, Group schemes of prime order, Annales scientifiques de l'École Normale Supérieure 3 (1970), 1–21
  3. M. Raynaud, Schémas en groupes de type (p,\dots,p), Bulletin de la Société Mathématique de France 102 (1974), 241–280

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_HopfAlgebra_CartierDual
import Definitions.Def_FiniteFlat_SchematicClosure

set_option autoImplicit false

open scoped TensorProduct

namespace HopfAlgebra

section FieldLevel

variable {F : Type*} [CommRing F] {A : Type*} [CommRing A] [Algebra F A]
variable {L : Type*} [CommRing L] [Algebra F L]

def vanishingIdealOfPoints (S : Set (A →ₐ[F] L)) : Ideal A where
  carrier := {a | ∀ ν ∈ S, ν a = 0}
  add_mem' {a b} ha hb := fun ν hν => by rw [map_add, ha ν hν, hb ν hν, add_zero]
  zero_mem' := fun ν _ => map_zero ν
  smul_mem' c {a} ha := fun ν hν => by rw [smul_eq_mul, map_mul, ha ν hν, mul_zero]

@[simp] theorem mem_vanishingIdealOfPoints_iff (S : Set (A →ₐ[F] L)) (a : A) :
    a ∈ vanishingIdealOfPoints S ↔ ∀ ν ∈ S, ν a = 0 := Iff.rfl

theorem vanishingIdealOfPoints_antitone {S T : Set (A →ₐ[F] L)} (h : S ⊆ T) :
    vanishingIdealOfPoints T ≤ vanishingIdealOfPoints S := fun _ ha ν hν => ha ν (h hν)

def liftPoint (S : Set (A →ₐ[F] L)) (ν : A →ₐ[F] L) (hν : ν ∈ S) :
    (A ⧸ vanishingIdealOfPoints S) →ₐ[F] L :=
  Ideal.Quotient.liftₐ (vanishingIdealOfPoints S) ν (fun a ha => ha ν hν)

@[simp] theorem liftPoint_mk (S : Set (A →ₐ[F] L)) (ν : A →ₐ[F] L) (hν : ν ∈ S) (a : A) :
    liftPoint S ν hν (Ideal.Quotient.mk (vanishingIdealOfPoints S) a) = ν a := rfl

noncomputable def evalPair (S : Set (A →ₐ[F] L)) (ν ν' : A →ₐ[F] L) (hν : ν ∈ S) (hν' : ν' ∈ S) :
    (A ⧸ vanishingIdealOfPoints S) ⊗[F] (A ⧸ vanishingIdealOfPoints S) →ₐ[F] L :=
  (Algebra.TensorProduct.lmul' F (S := L)).comp
    (Algebra.TensorProduct.map (liftPoint S ν hν) (liftPoint S ν' hν'))

theorem evalPair_tmul (S : Set (A →ₐ[F] L)) (ν ν' : A →ₐ[F] L) (hν : ν ∈ S) (hν' : ν' ∈ S) (a b : A) :
    evalPair S ν ν' hν hν' (Ideal.Quotient.mk _ a ⊗ₜ[F] Ideal.Quotient.mk _ b) = ν a * ν' b := by
  simp only [evalPair, AlgHom.coe_comp, Function.comp_apply, Algebra.TensorProduct.map_tmul, liftPoint_mk,
    Algebra.TensorProduct.lmul'_apply_tmul]

end FieldLevel

section PointMonoid

variable {F : Type*} [CommRing F] {A : Type*} [CommRing A] [Bialgebra F A]
variable {L : Type*} [CommRing L] [Algebra F L]

def ptSet (S : Submonoid (WithConv (A →ₐ[F] L))) : Set (A →ₐ[F] L) := {ν | WithConv.toConv ν ∈ S}

@[simp] theorem mem_ptSet_iff (S : Submonoid (WithConv (A →ₐ[F] L))) (ν : A →ₐ[F] L) :
    ν ∈ ptSet S ↔ WithConv.toConv ν ∈ S := Iff.rfl

theorem ofConv_mem_ptSet {S : Submonoid (WithConv (A →ₐ[F] L))} (ν : ↥S) : WithConv.ofConv ν.1 ∈ ptSet S := by
  show WithConv.toConv (WithConv.ofConv ν.1) ∈ S
  exact ν.2

theorem ptSet_mono {S T : Submonoid (WithConv (A →ₐ[F] L))} (h : S ≤ T) : ptSet S ⊆ ptSet T :=
  fun _ hν => h hν

abbrev pointQuot (S : Submonoid (WithConv (A →ₐ[F] L))) : Type _ := A ⧸ vanishingIdealOfPoints (ptSet S)

noncomputable def evalQuot (S : Submonoid (WithConv (A →ₐ[F] L))) : L ⊗[F] pointQuot S →ₐ[L] (↥S → L) :=
  Algebra.TensorProduct.lift (Algebra.ofId L _)
    (Pi.algHom F _ fun ν => liftPoint (ptSet S) (WithConv.ofConv ν.1) (ofConv_mem_ptSet ν))
    (fun _ _ => Commute.all _ _)

theorem evalQuot_tmul (S : Submonoid (WithConv (A →ₐ[F] L))) (c : L) (a : A) (ν : ↥S) :
    evalQuot S (c ⊗ₜ[F] Ideal.Quotient.mk _ a) ν = c * (WithConv.ofConv ν.1) a := by
  simp only [evalQuot, Algebra.TensorProduct.lift_tmul, Pi.mul_apply, Pi.algHom_apply]
  rw [Algebra.ofId_apply, Pi.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply]
  rfl

end PointMonoid

end HopfAlgebra

namespace CartierDual

section BaseChange

universe u v w

variable (O : Type u) [CommRing O] (F : Type v) [CommRing F] [Algebra O F]
variable (A : Type w) [CommRing A] [Bialgebra O A]

theorem add_apply_pt {R : Type*} [CommRing R] {X : Type*} [CommRing X] [Bialgebra R X]
    (φ ψ : CartierDual R X) (x : X) : (φ + ψ) x = φ x + ψ x := by
  rw [← CartierDual.toDual_apply (φ + ψ), map_add, LinearMap.add_apply, CartierDual.toDual_apply,
    CartierDual.toDual_apply]

theorem zero_apply_pt {R : Type*} [CommRing R] {X : Type*} [CommRing X] [Bialgebra R X]
    (x : X) : (0 : CartierDual R X) x = 0 := by
  rw [← CartierDual.toDual_apply (0 : CartierDual R X), map_zero, LinearMap.zero_apply]

theorem smul_apply_pt {R : Type*} [CommRing R] {X : Type*} [CommRing X] [Bialgebra R X]
    (c : R) (φ : CartierDual R X) (x : X) : (c • φ) x = c * φ x := by
  rw [← CartierDual.toDual_apply (c • φ), LinearEquiv.map_smul, LinearMap.smul_apply, smul_eq_mul,
    CartierDual.toDual_apply]

noncomputable instance instModuleRestrictBaseChange : Module O (CartierDual F (F ⊗[O] A)) :=
  Module.compHom (CartierDual F (F ⊗[O] A)) (algebraMap O F)

instance instIsScalarTowerRestrictBaseChange : IsScalarTower O F (CartierDual F (F ⊗[O] A)) :=
  IsScalarTower.of_algebraMap_smul fun _ _ => rfl

noncomputable instance instRingBaseChangeDual : Ring (F ⊗[O] CartierDual O A) := Algebra.TensorProduct.instRing

noncomputable instance instAlgebraBaseChangeDual : Algebra F (F ⊗[O] CartierDual O A) :=
  Algebra.TensorProduct.leftAlgebra

variable {O F A}

noncomputable def dualBaseChange (φ : CartierDual O A) : CartierDual F (F ⊗[O] A) :=
  CartierDual.ofDual F (F ⊗[O] A)
    ((TensorProduct.AlgebraTensorModule.rid O F F).toLinearMap ∘ₗ LinearMap.baseChange F (CartierDual.toDual O A φ))

@[simp] theorem dualBaseChange_tmul (φ : CartierDual O A) (c : F) (a : A) :
    dualBaseChange (F := F) φ (c ⊗ₜ[O] a) = c * algebraMap O F (φ a) := by
  show (TensorProduct.AlgebraTensorModule.rid O F F) ((LinearMap.baseChange F (CartierDual.toDual O A φ)) (c ⊗ₜ[O] a)) = _
  rw [LinearMap.baseChange_tmul, TensorProduct.AlgebraTensorModule.rid_tmul, CartierDual.toDual_apply, Algebra.smul_def,
    mul_comm]

variable (O F A) in

noncomputable def dualBaseChangeHom : CartierDual O A →ₗ[O] CartierDual F (F ⊗[O] A) where
  toFun := dualBaseChange
  map_add' φ ψ := by
    refine CartierDual.ext fun x => ?_
    rw [add_apply_pt]
    induction x using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero, map_zero, add_zero]
    | tmul c a =>
      rw [dualBaseChange_tmul, dualBaseChange_tmul, dualBaseChange_tmul, add_apply_pt, map_add, mul_add]
    | add x y hx hy => rw [map_add, map_add, map_add, hx, hy]; abel
  map_smul' r φ := by
    refine CartierDual.ext fun x => ?_
    rw [RingHom.id_apply]
    show dualBaseChange (r • φ) x = ((algebraMap O F r) • dualBaseChange φ) x
    rw [smul_apply_pt]
    induction x using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero, mul_zero]
    | tmul c a => rw [dualBaseChange_tmul, dualBaseChange_tmul, smul_apply_pt, map_mul]; ring
    | add x y hx hy => rw [map_add, map_add, hx, hy, mul_add]

variable (O F A) in

noncomputable def dualBaseChangeLin : F ⊗[O] CartierDual O A →ₗ[F] CartierDual F (F ⊗[O] A) :=
  LinearMap.liftBaseChange F (dualBaseChangeHom O F A)

@[simp] theorem dualBaseChangeLin_tmul (c : F) (φ : CartierDual O A) :
    dualBaseChangeLin O F A (c ⊗ₜ[O] φ) = c • dualBaseChange φ :=
  LinearMap.liftBaseChange_tmul F _ c φ

theorem dualBaseChangeLin_tmul_tmul (c : F) (φ : CartierDual O A) (c' : F) (a : A) :
    dualBaseChangeLin O F A (c ⊗ₜ[O] φ) (c' ⊗ₜ[O] a) = c * c' * algebraMap O F (φ a) := by
  rw [dualBaseChangeLin_tmul, smul_apply_pt, dualBaseChange_tmul, mul_assoc]

end BaseChange

end CartierDual

namespace HopfAlgebra

section Character

universe u v w

variable (O : Type u) [CommRing O] (F : Type v) [CommRing F] [Algebra O F]
variable (A : Type w) [CommRing A] [Bialgebra O A]
variable (L : Type*) [CommRing L] [Algebra F L]

noncomputable def characterGenericFibre (S : Set (F ⊗[O] A →ₐ[F] L)) : Subalgebra F (F ⊗[O] CartierDual O A) :=
  Algebra.adjoin F {w | ∀ x ∈ vanishingIdealOfPoints S, CartierDual.dualBaseChangeLin O F A w x = 0}

theorem characterGenericFibre_mono {S T : Set (F ⊗[O] A →ₐ[F] L)} (h : S ⊆ T) :
    characterGenericFibre O F A L S ≤ characterGenericFibre O F A L T := by
  apply Algebra.adjoin_mono
  intro w hw x hx
  exact hw x (vanishingIdealOfPoints_antitone h hx)

theorem subset_characterGenericFibre (S : Set (F ⊗[O] A →ₐ[F] L)) :
    {w | ∀ x ∈ vanishingIdealOfPoints S, CartierDual.dualBaseChangeLin O F A w x = 0}
      ⊆ (characterGenericFibre O F A L S : Set (F ⊗[O] CartierDual O A)) :=
  Algebra.subset_adjoin

end Character

section Closure

universe u v w

variable (O : Type u) [CommRing O] (F : Type v) [Field F] [Algebra O F]
variable (A : Type w) [CommRing A] [Bialgebra O A] [Coalgebra.IsCocomm O A]
variable (L : Type*) [CommRing L] [Algebra F L]

noncomputable abbrev characterClosure (S : Set (F ⊗[O] A →ₐ[F] L)) : Subalgebra O (CartierDual O A) :=
  flatClosure (characterGenericFibre O F A L S)

theorem mem_characterClosure_iff (S : Set (F ⊗[O] A →ₐ[F] L)) (g : CartierDual O A) :
    g ∈ characterClosure O F A L S ↔ (1 : F) ⊗ₜ[O] g ∈ characterGenericFibre O F A L S := Iff.rfl

theorem characterClosure_mono {S T : Set (F ⊗[O] A →ₐ[F] L)} (h : S ⊆ T) :
    characterClosure O F A L S ≤ characterClosure O F A L T :=
  flatClosure_mono (characterGenericFibre_mono O F A L h)

end Closure

end HopfAlgebra

Statements phrased using this module (13)