Serre dans Mathlib — tour guidé des cinq monuments

Navigation : ↑ Lean-37 — capstone de la série Lean | README Serre 100

Série Serre 100 — grain 6 (EPIC #16334) · Notebook compagnon du module Lean serre100_lean/ — le versant preuves du diptyque : le grain 9 (#16374) dresse l’index des #check « Serre » ; ici, nous démontrons.

Jean-Pierre Serre (Prix Abel 2003, première cuvée) a laissé son nom à cinq constructions distinctes que Mathlib formalise chacune dans un coin différent de la bibliothèque. Ce notebook les visite une à une, énoncé formel à l’appui.

#	Monument	Fichier Mathlib	Référence portée par ce fichier
1	Les classes de Serre	`CategoryTheory.Abelian.SerreClass.Basic`	Serre, Groupes d’homotopie et classes de groupes abéliens (1958)
2	La dérivée de Serre	`NumberTheory.ModularForms.Derivative`	aucune bibliographie — la docstring dit « (Ramanujan-)Serre derivative »
3	La construction de Serre	`Algebra.Lie.SerreConstruction`	Serre, Complex Semisimple Lie Algebras, ch. VI, appendice
4	Le critère de Serre (DVR)	`RingTheory.DiscreteValuationRing.Basic`	Serre, Local Fields — « the definition in Serre’s book “Local Fields” »
5	Parfait « au sens de Serre »	`FieldTheory.Perfect`	aucune bibliographie — « perfect in the sense of Serre »

La colonne de droite est ce que le fichier porte, vérifié un à un au pin du lake (db584cd6, v4.33.0) — pas ce qu’on attendrait de lui : sur les cinq, trois portent un livre de Serre (Groupes d’homotopie et classes de groupes abéliens, 1958 — station 1 ; Complex Semisimple Lie Algebras — station 3 ; Local Fields — station 4), et deux aucune (stations 2 et 5).

Prérequis : le kernel lean4-wsl partage un environnement Lean entre toutes les cellules — les import ne sont légaux qu’en tête de session, dans la première cellule de code (pattern du notebook Lean-29).

Mise en route

Le module compagnon Serre100.Tour (dans serre100_lean/) compile les cinq stations contre Mathlib ; ce notebook l’importe puis explore chaque station interactivement.

import Serre100.Tour

open CategoryTheory Derivative UpperHalfPlane
open scoped Manifold ModularForm

-- Le criteres « deux-sur-trois » de la station 1, extrait du module compagnon.
#check @Serre100.member_iff_outer

import Serre100.Tour

open CategoryTheory Derivative UpperHalfPlane

open scoped Manifold ModularForm

-- Le criteres « deux-sur-trois » de la station 1, extrait du module compagnon.

#check @Serre100.member_iff_outer @Serre100.member_iff_outer : ∀ {C : Type u_1} [inst : Category.{u_2, u_1} C] [inst_1 : Abelian C] (P : ObjectProperty C)
  [P.IsSerreClass] {S : ShortComplex C}, S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)

--% env 0

Raw input

{"cmd": "import Serre100.Tour\n\nopen CategoryTheory Derivative UpperHalfPlane\nopen scoped Manifold ModularForm\n\n-- Le criteres \u00ab deux-sur-trois \u00bb de la station 1, extrait du module compagnon.\n#check @Serre100.member_iff_outer"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@Serre100.member_iff_outer : ∀ {C : Type u_1} [inst : Category.{u_2, u_1} C] [inst_1 : Abelian C] (P : ObjectProperty C)\n  [P.IsSerreClass] {S : ShortComplex C}, S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)"}],
 "env": 0}

Station 1 — Les classes de Serre

Une classe de Serre \(P\) sur une catégorie abélienne \(\mathcal{C}\) est une collection d’objets qui contient l’objet nul et passe aux sous-objets, quotients et extensions. C’est le langage dans lequel Corps locaux exprime ses conditions de finitude : « \(X\) est fini », « \(X\) est de torsion », « \(X\) est de longueur finie » sont des classes de Serre de la catégorie des groupes abéliens.

Deux-sur-trois : dans une suite exacte courte \(0 \to X_1 \to X_2 \to X_3 \to 0\), l’objet \(X_2\) est dans la classe si et seulement si \(X_1\) et \(X_3\) y sont.

#check @CategoryTheory.ObjectProperty.IsSerreClass

-- Les deux extremes : tout (T) et presque rien (les objets nuls).
example {C : Type*} [Category C] [Abelian C] :
    (⊤ : ObjectProperty C).IsSerreClass := inferInstance

example {C : Type*} [Category C] [Abelian C] :
    ObjectProperty.IsSerreClass (Limits.IsZero (C := C)) := inferInstance

-- L'exemple historique : les groupes abeliens finis (Corps locaux, ch. I).
example : AddCommGrpCat.isFinite.IsSerreClass := inferInstance

#check @CategoryTheory.ObjectProperty.IsSerreClass @ObjectProperty.IsSerreClass : {C : Type u_2} → [inst : Category.{u_1, u_2} C] → [Abelian C] → ObjectProperty C → Prop

-- Les deux extremes : tout (T) et presque rien (les objets nuls).

example {C : Type*} [Category C] [Abelian C] :

    (⊤ : ObjectProperty C).IsSerreClass := inferInstance

example {C : Type*} [Category C] [Abelian C] :

    ObjectProperty.IsSerreClass (Limits.IsZero (C := C)) := inferInstance

-- L'exemple historique : les groupes abeliens finis (Corps locaux, ch. I).

example : AddCommGrpCat.isFinite.IsSerreClass := inferInstance

--% env 1

Raw input

{"cmd": "#check @CategoryTheory.ObjectProperty.IsSerreClass\n\n-- Les deux extremes : tout (T) et presque rien (les objets nuls).\nexample {C : Type*} [Category C] [Abelian C] :\n    (\u22a4 : ObjectProperty C).IsSerreClass := inferInstance\n\nexample {C : Type*} [Category C] [Abelian C] :\n    ObjectProperty.IsSerreClass (Limits.IsZero (C := C)) := inferInstance\n\n-- L'exemple historique : les groupes abeliens finis (Corps locaux, ch. I).\nexample : AddCommGrpCat.isFinite.IsSerreClass := inferInstance", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@ObjectProperty.IsSerreClass : {C : Type u_2} → [inst : Category.{u_1, u_2} C] → [Abelian C] → ObjectProperty C → Prop"}],
 "env": 1}

Le critère central se lit alors : la classe des objets finis de AddCommGrp détecte la finitude d’une extension par celle de ses extrêmes.

#check @CategoryTheory.ObjectProperty.prop_iff_of_shortExact

example {C : Type*} [Category C] [Abelian C] (P : ObjectProperty C)
    [P.IsSerreClass] {S : ShortComplex C} (hS : S.ShortExact) :
    P S.X₂ ↔ P S.X₁ ∧ P S.X₃ := P.prop_iff_of_shortExact hS

#check @CategoryTheory.ObjectProperty.prop_iff_of_shortExact @ObjectProperty.prop_iff_of_shortExact : ∀ {C : Type u_2} [inst : Category.{u_1, u_2} C] [inst_1 : Abelian C]
  (P : ObjectProperty C) [P.IsSerreClass] {S : ShortComplex C}, S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)

example {C : Type*} [Category C] [Abelian C] (P : ObjectProperty C)

    [P.IsSerreClass] {S : ShortComplex C} (hS : S.ShortExact) :

    P S.X₂ ↔ P S.X₁ ∧ P S.X₃ := P.prop_iff_of_shortExact hS

--% env 2

Raw input

{"cmd": "#check @CategoryTheory.ObjectProperty.prop_iff_of_shortExact\n\nexample {C : Type*} [Category C] [Abelian C] (P : ObjectProperty C)\n    [P.IsSerreClass] {S : ShortComplex C} (hS : S.ShortExact) :\n    P S.X\u2082 \u2194 P S.X\u2081 \u2227 P S.X\u2083 := P.prop_iff_of_shortExact hS", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@ObjectProperty.prop_iff_of_shortExact : ∀ {C : Type u_2} [inst : Category.{u_1, u_2} C] [inst_1 : Abelian C]\n  (P : ObjectProperty C) [P.IsSerreClass] {S : ShortComplex C}, S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)"}],
 "env": 2}

Station 2 — La dérivée de Serre

Sur le demi-plan supérieur \(\mathbb{H}\), la dérivée de Serre de poids \(k\)

\[\partial_k F = D F - \frac{k}{12} E_2 F\]

corrige la dérivée normalisée \(D = \frac{1}{2\pi i}\frac{d}{dz}\) par le quasi-modulaire \(E_2\). L’ingrédient \(-\frac{k}{12}E_2\) est ce qui doit compenser le défaut de modularité de \(D F\), de sorte que \(\partial_k\) envoie les formes de poids \(k\) sur les formes de poids \(k+2\) — sans quitter le monde modulaire.

C’est un objectif, pas un acquis de la bibliothèque. Au pin du lake, la docstring de NumberTheory.ModularForms.Derivative porte exactement cette phrase dans sa rubrique TODO: — « Serre derivative preserves modularity, i.e. \(\partial_k (M_k) \subseteq M_{k+2}\) ». Ce que Mathlib fournit ici est la définition (serreDerivative) et l’équivariance sous l’action slash (serreDerivative_slash_equivariant) ; la préservation de la modularité reste à prouver. La station visite donc un monument défini, dont le théorème attend encore : c’est une information sur l’état de la formalisation, pas un détail.

#check @Derivative.serreDerivative

-- La formule definissoire, relue : derivation normalisee corrigee en E2.
example (k : ℂ) (F : ℍ → ℂ) (z : ℍ) :
    serreDerivative k F z =
      normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z := rfl

#check @Derivative.serreDerivative serreDerivative : ℂ → (ℍ → ℂ) → ℍ → ℂ

-- La formule definissoire, relue : derivation normalisee corrigee en E2.

example (k : ℂ) (F : ℍ → ℂ) (z : ℍ) :

    serreDerivative k F z =

      normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z := rfl

--% env 3

Raw input

{"cmd": "#check @Derivative.serreDerivative\n\n-- La formule definissoire, relue : derivation normalisee corrigee en E2.\nexample (k : \u2102) (F : \u210d \u2192 \u2102) (z : \u210d) :\n    serreDerivative k F z =\n      normalizedDerivOfComplex F z - k * 12\u207b\u00b9 * EisensteinSeries.E2 z * F z := rfl", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data": "serreDerivative : ℂ → (ℍ → ℂ) → ℍ → ℂ"}],
 "env": 3}

La règle de Leibniz pondérée est la signature d’une dérivation graduée : sur un produit, les poids s’ajoutent, et chaque facteur est dérivé avec son propre poids.

example (k₁ k₂ : ℂ) (F G : ℍ → ℂ) (hF : MDiff F) (hG : MDiff G) :
    serreDerivative (k₁ + k₂) (F * G) =
      serreDerivative k₁ F * G + F * serreDerivative k₂ G :=
  serreDerivative_mul k₁ k₂ F G hF hG

#check @Derivative.serreDerivative_mdifferentiable

example (k₁ k₂ : ℂ) (F G : ℍ → ℂ) (hF : MDiff F) (hG : MDiff G) :

    serreDerivative (k₁ + k₂) (F * G) =

      serreDerivative k₁ F * G + F * serreDerivative k₂ G :=

  serreDerivative_mul k₁ k₂ F G hF hG

#check @Derivative.serreDerivative_mdifferentiable @serreDerivative_mdifferentiable : ∀ {F : ℍ → ℂ} (k : ℂ), MDiff F → MDiff (serreDerivative k F)

--% env 4

Raw input

{"cmd": "example (k\u2081 k\u2082 : \u2102) (F G : \u210d \u2192 \u2102) (hF : MDiff F) (hG : MDiff G) :\n    serreDerivative (k\u2081 + k\u2082) (F * G) =\n      serreDerivative k\u2081 F * G + F * serreDerivative k\u2082 G :=\n  serreDerivative_mul k\u2081 k\u2082 F G hF hG\n\n#check @Derivative.serreDerivative_mdifferentiable", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "@serreDerivative_mdifferentiable : ∀ {F : ℍ → ℂ} (k : ℂ), MDiff F → MDiff (serreDerivative k F)"}],
 "env": 4}

Station 3 — La construction de Serre

Soit \(CM\) une matrice de Cartan généralisée. L’algèbre de Lie de Serre associée est le quotient de l’algèbre de Lie libre sur les générateurs \(H_i, E_i, F_i\) (\(i\) parcourt l’ensemble d’indices \(B\)) par l’idéal des relations de Serre :

\([H_i, H_j] = 0\) (les \(H\) commutent),
\([E_i, F_j] = \delta_{ij} H_i\) (crochet diagonal),
\([H_i, E_j] = CM_{ij} E_j\) et \([H_i, F_j] = -CM_{ij} F_j\),
\((\operatorname{ad} E_i)^{1 - CM_{ij}} E_j = 0\) et de même pour les \(F\).

Pour \(CM\) de type \(A_2\), le quotient est \(\mathfrak{sl}_3\) ; le formalisme général ouvre la porte aux algèbres de Kac–Moody.

#check @CartanMatrix.Generators.H
#check @CartanMatrix.Generators.E
#check @CartanMatrix.Generators.F

def cartanA2 : Matrix (Fin 2) (Fin 2) ℤ := !![2, -1; -1, 2]
#check @CartanMatrix.Relations.toIdeal

#check @CartanMatrix.Generators.H @CartanMatrix.Generators.H : {B : Type u_1} → B → CartanMatrix.Generators B

#check @CartanMatrix.Generators.E @CartanMatrix.Generators.E : {B : Type u_1} → B → CartanMatrix.Generators B

#check @CartanMatrix.Generators.F @CartanMatrix.Generators.F : {B : Type u_1} → B → CartanMatrix.Generators B

def cartanA2 : Matrix (Fin 2) (Fin 2) ℤ := !![2, -1; -1, 2]

#check @CartanMatrix.Relations.toIdeal CartanMatrix.Relations.toIdeal : (R : Type u_1) →
  {B : Type u_2} →
    [inst : CommRing R] → Matrix B B ℤ → [DecidableEq B] → LieIdeal R (FreeLieAlgebra R (CartanMatrix.Generators B))

--% env 5

Raw input

{"cmd": "#check @CartanMatrix.Generators.H\n#check @CartanMatrix.Generators.E\n#check @CartanMatrix.Generators.F\n\ndef cartanA2 : Matrix (Fin 2) (Fin 2) \u2124 := !![2, -1; -1, 2]\n#check @CartanMatrix.Relations.toIdeal", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@CartanMatrix.Generators.H : {B : Type u_1} → B → CartanMatrix.Generators B"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@CartanMatrix.Generators.E : {B : Type u_1} → B → CartanMatrix.Generators B"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@CartanMatrix.Generators.F : {B : Type u_1} → B → CartanMatrix.Generators B"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "CartanMatrix.Relations.toIdeal : (R : Type u_1) →\n  {B : Type u_2} →\n    [inst : CommRing R] → Matrix B B ℤ → [DecidableEq B] → LieIdeal R (FreeLieAlgebra R (CartanMatrix.Generators B))"}],
 "env": 5}

Les six familles de relations vivent dans le sous-module CartanMatrix.Relations : HH, EF, HE, HF, adE, adF. L’idéal toIdeal est l’enveloppe (comme idéal de Lie) de leur union — c’est lui qu’on quotientte.

#check @CartanMatrix.Relations.HE
#check @CartanMatrix.Relations.adE

-- Sur A2, la lecture de HE (0, 1) : [H 0, E 1] = (-1) • E 1.
example : cartanA2 0 1 = (-1 : ℤ) := by decide

#check @CartanMatrix.Relations.HE CartanMatrix.Relations.HE : (R : Type u_1) →
  {B : Type u_2} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

#check @CartanMatrix.Relations.adE CartanMatrix.Relations.adE : (R : Type u_1) →
  {B : Type u_2} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

-- Sur A2, la lecture de HE (0, 1) : [H 0, E 1] = (-1) • E 1.

example : cartanA2 0 1 = (-1 : ℤ) := by decide

--% env 6

Raw input

{"cmd": "#check @CartanMatrix.Relations.HE\n#check @CartanMatrix.Relations.adE\n\n-- Sur A2, la lecture de HE (0, 1) : [H 0, E 1] = (-1) \u2022 E 1.\nexample : cartanA2 0 1 = (-1 : \u2124) := by decide", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "CartanMatrix.Relations.HE : (R : Type u_1) →\n  {B : Type u_2} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "CartanMatrix.Relations.adE : (R : Type u_1) →\n  {B : Type u_2} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)"}],
 "env": 6}

Station 4 — Le critère de Serre pour les anneaux de valuation discrète

Corps locaux, ch. I §2, prop. 2 : un anneau de valuation discrète est exactement un anneau intègre principal possédant un unique idéal premier non nul. Ce critère est la porte d’entrée standard pour prouver qu’un anneau est un DVR sans exhiber de valuation.

#check @IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime

example (R : Type*) [CommRing R] [IsDomain R] :
    IsDiscreteValuationRing R ↔
      IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime :=
  IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime R

-- Dans un DVR, il existe des uniformisantes (irreductibles, donc premieres).
#check @IsDiscreteValuationRing.exists_irreducible
#check @IsDiscreteValuationRing.exists_prime

#check @IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
  IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

example (R : Type*) [CommRing R] [IsDomain R] :

    IsDiscreteValuationRing R ↔

      IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime :=

  IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime R

-- Dans un DVR, il existe des uniformisantes (irreductibles, donc premieres).

#check @IsDiscreteValuationRing.exists_irreducible IsDiscreteValuationRing.exists_irreducible : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R]
  [IsDiscreteValuationRing R], ∃ ϖ, Irreducible ϖ

#check @IsDiscreteValuationRing.exists_prime IsDiscreteValuationRing.exists_prime : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R]
  [IsDiscreteValuationRing R], ∃ ϖ, Prime ϖ

--% env 7

Raw input

{"cmd": "#check @IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime\n\nexample (R : Type*) [CommRing R] [IsDomain R] :\n    IsDiscreteValuationRing R \u2194\n      IsPrincipalIdealRing R \u2227 \u2203! P : Ideal R, P \u2260 \u22a5 \u2227 P.IsPrime :=\n  IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime R\n\n-- Dans un DVR, il existe des uniformisantes (irreductibles, donc premieres).\n#check @IsDiscreteValuationRing.exists_irreducible\n#check @IsDiscreteValuationRing.exists_prime", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],\n  IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "IsDiscreteValuationRing.exists_irreducible : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R]\n  [IsDiscreteValuationRing R], ∃ ϖ, Irreducible ϖ"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "IsDiscreteValuationRing.exists_prime : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R]\n  [IsDiscreteValuationRing R], ∃ ϖ, Prime ϖ"}],
 "env": 7}

Station 5 — Parfait « au sens de Serre »

Corps locaux, ch. II §3 : un anneau de caractéristique \(p\) est parfait lorsque le Frobenius \(x \mapsto x^p\) est bijectif. Mathlib nomme cette notion PerfectRing et signale dans sa docstring qu’il s’agit du sens de Serre — à ne pas confondre avec la perfection de Bass (couvertures projectives). L’argument type : un anneau fini et réduit est parfait, car injectif entre finis de même cardinal suffit.

#check @PerfectRing.ofFiniteOfIsReduced
#check @PerfectRing.toPerfectField

example : PerfectRing (ZMod 2) 2 := inferInstance

example : PerfectRing (ZMod 5) 5 := by
  letI : Fact (Nat.Prime 5) := ⟨by decide⟩
  exact inferInstance

-- Le pont exige Field (ZMod 7) des l'elaboration de l'enonce : le Fact
-- litteral doit donc etre enregistre AVANT l'exemple (les instances
-- litterales n'existent que pour 2 et 3).
local instance : Fact (Nat.Prime 7) := ⟨by decide⟩

example : PerfectField (ZMod 7) := PerfectRing.toPerfectField (ZMod 7) 7

#check @PerfectRing.ofFiniteOfIsReduced PerfectRing.ofFiniteOfIsReduced : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [ExpChar R p] [Finite R] [IsReduced R],
  PerfectRing R p

#check @PerfectRing.toPerfectField PerfectRing.toPerfectField : ∀ (K : Type u_1) (p : ℕ) [inst : Field K] [ExpChar K p] [PerfectRing K p], PerfectField K

example : PerfectRing (ZMod 2) 2 := inferInstance

example : PerfectRing (ZMod 5) 5 := by

  letI : Fact (Nat.Prime 5) := ⟨by decide⟩🟨 Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`

  exact inferInstance

-- Le pont exige Field (ZMod 7) des l'elaboration de l'enonce : le Fact

-- litteral doit donc etre enregistre AVANT l'exemple (les instances

-- litterales n'existent que pour 2 et 3).

local instance : Fact (Nat.Prime 7) := ⟨by decide⟩

example : PerfectField (ZMod 7) := PerfectRing.toPerfectField (ZMod 7) 7

--% env 8

Raw input

{"cmd": "#check @PerfectRing.ofFiniteOfIsReduced\n#check @PerfectRing.toPerfectField\n\nexample : PerfectRing (ZMod 2) 2 := inferInstance\n\nexample : PerfectRing (ZMod 5) 5 := by\n  letI : Fact (Nat.Prime 5) := \u27e8by decide\u27e9\n  exact inferInstance\n\n-- Le pont exige Field (ZMod 7) des l'elaboration de l'enonce : le Fact\n-- litteral doit donc etre enregistre AVANT l'exemple (les instances\n-- litterales n'existent que pour 2 et 3).\nlocal instance : Fact (Nat.Prime 7) := \u27e8by decide\u27e9\n\nexample : PerfectField (ZMod 7) := PerfectRing.toPerfectField (ZMod 7) 7", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PerfectRing.ofFiniteOfIsReduced : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [ExpChar R p] [Finite R] [IsReduced R],\n  PerfectRing R p"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "PerfectRing.toPerfectField : ∀ (K : Type u_1) (p : ℕ) [inst : Field K] [ExpChar K p] [PerfectRing K p], PerfectField K"},
  {"severity": "warning",
   "pos": {"line": 7, "column": 2},
   "endPos": {"line": 7, "column": 42},
   "data":
   "Try this: \n  letI̵\n\nThe goal is a proposition, so `let` is preferred over `letI`.\nThe difference between `let` and `letI` is that `letI` inlines the value.\nBut this is not relevant for proofs because of proof irrelevance.\n\nNote: This linter can be disabled with `set_option linter.style.haveILetI false`"}],
 "env": 8}

Lecture de la sortie — l’avertissement 🟨 de la station 5

La sortie ci-dessus porte un avertissement du linter (linter.style.haveILetI) sur la ligne letI : Fact (Nat.Prime 5) : « The goal is a proposition, so let is preferred over letI ». Le signalement est exact, et pourtant sans conséquence ici : dans une preuve, let et letI s’échangent par irrélevance des preuves — c’est la seconde ligne de l’avertissement lui-même. letI reste le bon idiome là où la valeur doit être enregistrée comme instance pour l’élaboration de la suite, et c’est exactement ce que fait le local instance deux lignes plus bas, que le linter ne signale pas.

L’avertissement est laissé tel quel : le masquer par set_option linter.style.haveILetI false priverait le lecteur d’une distinction — let lie une valeur, letI lie une instance — que cette station est justement en train d’enseigner.

Contre-exemple calculé : `ZMod 4` n’est pas réduit

La réduction est essentielle : sur ZMod 4 (caractéristique \(2^2\)), le Frobenius \(x \mapsto x^2\) écrase \(2\) sur \(0\) — il n’est pas injectif, donc ZMod 4 n’est parfait en aucun sens. L’énumération le montre crûment :

-- Le carre (Frobenius p = 2) sur ZMod 4 : 0 et 2 ont la meme image.
#eval (List.range 4).map (fun n => (n : ZMod 4) ^ 2)

-- Le carre (Frobenius p = 2) sur ZMod 4 : 0 et 2 ont la meme image.

#eval (List.range 4).map (fun n => (n : ZMod 4) ^ 2) [0, 1, 0, 1]

--% env 9

Raw input

{"cmd": "-- Le carre (Frobenius p = 2) sur ZMod 4 : 0 et 2 ont la meme image.\n#eval (List.range 4).map (fun n => (n : ZMod 4) ^ 2)", "env": 8}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "[0, 1, 0, 1]"}],
 "env": 9}

Exercices

Les exercices couvrent les stations 1, 2, 3 et 5 ; la station 4 — le critère de Serre pour les anneaux de valuation discrète — n’en a pas, et cet écart est assumé et déclaré : un DVR se visite comme une lecture de la bibliothèque, pas comme un calcul à compléter. Les énoncés sont donnés en commentaire avec un TODO étudiant : à compléter. Les cellules s’exécutent sans erreur même non complétées — la preuve attendue est un commentaire.

Exercice 1 — Une extension concrète : `ZMod 6` extension de `ZMod 3` par `ZMod 2`

Indice : la suite \(0 \to \mathbb{Z}/2 \xrightarrow{\times 3} \mathbb{Z}/6 \xrightarrow{\bmod 3} \mathbb{Z}/3 \to 0\) est exacte. Vérifiez la nullité de la composée par énumération (decide), puis appliquez prop_iff_of_shortExact pour conclure que la finitude du milieu hérite de celle des extrêmes.

-- Exercice 1 : la suite 0 -> ZMod 2 -> ZMod 6 -> ZMod 3 -> 0.
def f1 : ZMod 2 → ZMod 6 := fun x => (3 * x.val : ℕ)
def g1 : ZMod 6 → ZMod 3 := fun y => (y.val % 3 : ℕ)

-- La composee est nulle (enumeration des 2 cas).
example : ∀ x : ZMod 2, g1 (f1 x) = 0 := by decide

-- Objectif : construire le ShortComplex correspondant, prouver ShortExact,
-- puis en deduire par member_iff_outer que le milieu herite de toute
-- propriete de Serre des extremites.
-- TODO etudiant : a completer.
#check @CategoryTheory.ObjectProperty.prop_iff_of_shortExact

-- Exercice 1 : la suite 0 -> ZMod 2 -> ZMod 6 -> ZMod 3 -> 0.

def f1 : ZMod 2 → ZMod 6 := fun x => (3 * x.val : ℕ)

def g1 : ZMod 6 → ZMod 3 := fun y => (y.val % 3 : ℕ)

-- La composee est nulle (enumeration des 2 cas).

example : ∀ x : ZMod 2, g1 (f1 x) = 0 := by decide

-- Objectif : construire le ShortComplex correspondant, prouver ShortExact,

-- puis en deduire par member_iff_outer que le milieu herite de toute

-- propriete de Serre des extremites.

-- TODO etudiant : a completer.

#check @CategoryTheory.ObjectProperty.prop_iff_of_shortExact @ObjectProperty.prop_iff_of_shortExact : ∀ {C : Type u_2} [inst : Category.{u_1, u_2} C] [inst_1 : Abelian C]
  (P : ObjectProperty C) [P.IsSerreClass] {S : ShortComplex C}, S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)

--% env 10

Raw input

{"cmd": "-- Exercice 1 : la suite 0 -> ZMod 2 -> ZMod 6 -> ZMod 3 -> 0.\ndef f1 : ZMod 2 \u2192 ZMod 6 := fun x => (3 * x.val : \u2115)\ndef g1 : ZMod 6 \u2192 ZMod 3 := fun y => (y.val % 3 : \u2115)\n\n-- La composee est nulle (enumeration des 2 cas).\nexample : \u2200 x : ZMod 2, g1 (f1 x) = 0 := by decide\n\n-- Objectif : construire le ShortComplex correspondant, prouver ShortExact,\n-- puis en deduire par member_iff_outer que le milieu herite de toute\n-- propriete de Serre des extremites.\n-- TODO etudiant : a completer.\n#check @CategoryTheory.ObjectProperty.prop_iff_of_shortExact", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "@ObjectProperty.prop_iff_of_shortExact : ∀ {C : Type u_2} [inst : Category.{u_1, u_2} C] [inst_1 : Abelian C]\n  (P : ObjectProperty C) [P.IsSerreClass] {S : ShortComplex C}, S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)"}],
 "env": 10}

Exercice 2 — Linéarité de la dérivée de Serre

Indice : le lemme serreDerivative_smul est déjà dans Mathlib ; retrouvez sa preuve à la main : ext z, simp [serreDerivative], puis ring.

#check @Derivative.serreDerivative_smul

-- Exercice 2 : montrer la C-linearite en la fonction, a poids fixe.
-- Objectif : etablir, pour (c : ℂ) (F : ℍ → ℂ) (hF : MDiff F) :
--   serreDerivative k (c • F) = c • serreDerivative k F
-- TODO etudiant : a completer (indice : ext z ; simp [Derivative.serreDerivative] ; ring).

#check @Derivative.serreDerivative_smul serreDerivative_smul : ∀ (k c : ℂ) (F : ℍ → ℂ), MDiff F → serreDerivative k (c • F) = c • serreDerivative k F

-- Exercice 2 : montrer la C-linearite en la fonction, a poids fixe.

-- Objectif : etablir, pour (c : ℂ) (F : ℍ → ℂ) (hF : MDiff F) :

--   serreDerivative k (c • F) = c • serreDerivative k F

-- TODO etudiant : a completer (indice : ext z ; simp [Derivative.serreDerivative] ; ring).

--% env 11

Raw input

{"cmd": "#check @Derivative.serreDerivative_smul\n\n-- Exercice 2 : montrer la C-linearite en la fonction, a poids fixe.\n-- Objectif : etablir, pour (c : \u2102) (F : \u210d \u2192 \u2102) (hF : MDiff F) :\n--   serreDerivative k (c \u2022 F) = c \u2022 serreDerivative k F\n-- TODO etudiant : a completer (indice : ext z ; simp [Derivative.serreDerivative] ; ring).", "env": 10}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "serreDerivative_smul : ∀ (k c : ℂ) (F : ℍ → ℂ), MDiff F → serreDerivative k (c • F) = c • serreDerivative k F"}],
 "env": 11}

Exercice 3 — Géométrie de la matrice \(A_2\)

Deux conventions, un seul exposant. Le nombre classique \(1 - CM_{ij}\) compte les crans de la relation de Serre. La bibliothèque, elle, écrit ad (E i) ^ (-CM i j).toNat <| ⁅E i, E j⁆ (SerreConstruction.lean) : l’exposant y est décalé d’un cran, parce que le crochet intérieur ⁅E i, E j⁆ est déjà une application de ad (E i) — l’indice du carnet calcule l’ordre total, le code en compte le reste.

Entrée	\(1 - CM_{ij}\) (total)	`(-CM i j).toNat` (reste)	Ce qui reste à appliquer
diagonale, \(CM_{ii} = 2\)	\(-1\)	\(0\)	rien — le crochet \(⁅E_i, E_i⁆ = 0\) ferme la relation
anti-diagonale, \(CM_{ij} = -1\)	\(2\)	\(1\)	une application de `ad (E i)` après le crochet

Indice : les deux écritures sont donc le même énoncé à ce décalage près — c’est cette réconciliation, et non l’un des deux nombres seul, que l’étape finale de l’exercice te demande d’écrire.

-- Exercice 3 : la matrice de Cartan encode l'ordre de nilpotence.
example : ∀ i : Fin 2, cartanA2 i i = (2 : ℤ) := by decide
example : cartanA2 0 1 = (-1 : ℤ) ∧ cartanA2 1 0 = (-1 : ℤ) := by decide

-- Objectif : verifier que (-cartanA2 0 1).toNat = 1 et interpreter :
-- l'ordre impose a ad (E 0) sur E 1 vaut exactement 1.
-- TODO etudiant : a completer (indice : Int.toNat et Relations.adE).
#check @CartanMatrix.Relations.adE

-- Exercice 3 : la matrice de Cartan encode l'ordre de nilpotence.

example : ∀ i : Fin 2, cartanA2 i i = (2 : ℤ) := by decide

example : cartanA2 0 1 = (-1 : ℤ) ∧ cartanA2 1 0 = (-1 : ℤ) := by decide

-- Objectif : verifier que (-cartanA2 0 1).toNat = 1 et interpreter :

-- l'ordre impose a ad (E 0) sur E 1 vaut exactement 1.

-- TODO etudiant : a completer (indice : Int.toNat et Relations.adE).

#check @CartanMatrix.Relations.adE CartanMatrix.Relations.adE : (R : Type u_1) →
  {B : Type u_2} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

--% env 12

Raw input

{"cmd": "-- Exercice 3 : la matrice de Cartan encode l'ordre de nilpotence.\nexample : \u2200 i : Fin 2, cartanA2 i i = (2 : \u2124) := by decide\nexample : cartanA2 0 1 = (-1 : \u2124) \u2227 cartanA2 1 0 = (-1 : \u2124) := by decide\n\n-- Objectif : verifier que (-cartanA2 0 1).toNat = 1 et interpreter :\n-- l'ordre impose a ad (E 0) sur E 1 vaut exactement 1.\n-- TODO etudiant : a completer (indice : Int.toNat et Relations.adE).\n#check @CartanMatrix.Relations.adE", "env": 11}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "CartanMatrix.Relations.adE : (R : Type u_1) →\n  {B : Type u_2} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)"}],
 "env": 12}

Exercice 4 — Parfaire un autre corps premier

Indice : réutilisez le pont PerfectRing.toPerfectField avec ZMod 11.

#check @PerfectRing.toPerfectField

-- Exercice 4 : etablir PerfectField (ZMod 11).
-- Objectif : le pont de Serre, sur un autre corps premier.
-- TODO etudiant : a completer (indice : PerfectRing.toPerfectField (ZMod 11) 11).

#check @PerfectRing.toPerfectField PerfectRing.toPerfectField : ∀ (K : Type u_1) (p : ℕ) [inst : Field K] [ExpChar K p] [PerfectRing K p], PerfectField K

-- Exercice 4 : etablir PerfectField (ZMod 11).

-- Objectif : le pont de Serre, sur un autre corps premier.

-- TODO etudiant : a completer (indice : PerfectRing.toPerfectField (ZMod 11) 11).

--% env 13

Raw input

{"cmd": "#check @PerfectRing.toPerfectField\n\n-- Exercice 4 : etablir PerfectField (ZMod 11).\n-- Objectif : le pont de Serre, sur un autre corps premier.\n-- TODO etudiant : a completer (indice : PerfectRing.toPerfectField (ZMod 11) 11).", "env": 12}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PerfectRing.toPerfectField : ∀ (K : Type u_1) (p : ℕ) [inst : Field K] [ExpChar K p] [PerfectRing K p], PerfectField K"}],
 "env": 13}

Conclusion

Le nom « Serre » indexe cinq chapitres de Mathlib, du catégorique (classes) à l’arithmétique (DVR, perfection) en passant par l’analyse modulaire et les algèbres de Lie. Trois constantes de ce tour :

chaque station énonce un critère (deux-sur-trois, Leibniz pondéré, présentation par générateurs-relations, PID + unique premier, Frobenius bijectif) ;
l’argument diagonal est la finitude : finies + réduites ⇒ parfaites, finies par extensions ;
la bibliothèque porte un livre de Serre à trois des cinq stations — Groupes d’homotopie et classes de groupes abéliens (1958) à la station 1, Complex Semisimple Lie Algebras à la station 3, Local Fields (l’édition anglaise de Corps locaux) à la station 4 — vérifié fichier par fichier au pin du lake.

Le versant index (recensement exhaustif des #check Serre) est livré par le grain 9 (#16374) ; ce notebook en était le versant preuves.

Références

J.-P. Serre, Corps locaux, Hermann, 1962 — ch. I, ch. I §2, ch. II §3.
J.-P. Serre, Cours d’arithmétique, PUF, 1970 — ch. VII (formes modulaires).
J.-P. Serre, Complex semisimple Lie algebras, Springer, 1966.
mathlib4, pins du lake compagnon : db584cd6d46c (v4.33.0).

Retour au sommet

Mise en route

Station 1 — Les classes de Serre

Station 2 — La dérivée de Serre

Station 3 — La construction de Serre

Station 4 — Le critère de Serre pour les anneaux de valuation discrète

Station 5 — Parfait « au sens de Serre »

Lecture de la sortie — l’avertissement 🟨 de la station 5

Contre-exemple calculé : ZMod 4 n’est pas réduit

Exercices

Exercice 1 — Une extension concrète : ZMod 6 extension de ZMod 3 par ZMod 2

Exercice 2 — Linéarité de la dérivée de Serre

Exercice 3 — Géométrie de la matrice \(A_2\)

Exercice 4 — Parfaire un autre corps premier

Conclusion

Références

Contre-exemple calculé : `ZMod 4` n’est pas réduit

Exercice 1 — Une extension concrète : `ZMod 6` extension de `ZMod 3` par `ZMod 2`