Lean-30 : groupes formels multivariés — compagnon natif

Sommaire de la série · Lake formal_groups_lean · Compagnon Grothendieck

Ce notebook rend visibles, sous le vrai kernel Lean 4, les quatre modules du lake formal_groups_lean. « Natif » signifie ici que les imports, exemples et certificats sont contrôlés par le compilateur : la prose explique les sorties, mais ne s’y substitue pas.

Objectifs, prérequis et durée

À la fin de ce parcours, vous saurez :

lire MvFormalGroup comme un \(g\)-uplet de séries formelles en deux blocs de \(g\) variables ;
relier ses champs au terme constant, à la partie linéaire et à l’associativité ;
expliquer le rôle de subst et de HasSubst ;
manipuler la signature des morphismes Hom, de l’identité, de la composition et du changement d’anneau ;
interpréter nthSeries, linearPart et FiniteHeight en caractéristique positive.

Prérequis. Installation Lean/WSL, tactiques élémentaires (rfl, simpa, inferInstance) et notion de série formelle multivariée.
Durée estimée. 40 minutes.

1. Le lake et son environnement formel

Le lake est un port pédagogique d’une définition issue du dépôt anthropics/fermats-last-theorem, commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef, sous licence Apache-2.0. Il cible Lean 4.33.0 et le pin Mathlib db584cd6d46c92f209a44c0f1c829460d327499d.

Ses quatre modules forment une progression : structure et substitution (Basic), morphismes (Hom), exemple additif (Additive), puis itérés et hauteur (Iterates). L’import suivant doit être exécuté depuis le répertoire du lake ; un échec d’import signale un environnement ou un répertoire de travail incorrect, pas une preuve à contourner.

import FormalGroups.Basic
import FormalGroups.Hom
import FormalGroups.Additive
import FormalGroups.Iterates

open MvPowerSeries
open FormalGroups
open FormalGroups.MvFormalGroup

#check MvFormalGroup
#check addMv
#check Hom

import FormalGroups.Basic

import FormalGroups.Hom

import FormalGroups.Additive

import FormalGroups.Iterates

open MvPowerSeries

open FormalGroups

open FormalGroups.MvFormalGroup

#check MvFormalGroup FormalGroups.MvFormalGroup.{u_1} (g : ℕ) (R : Type u_1) [CommRing R] : Type u_1

#check addMv FormalGroups.MvFormalGroup.addMv.{u_1} (g : ℕ) (R : Type u_1) [CommRing R] : MvFormalGroup g R

#check Hom FormalGroups.MvFormalGroup.Hom.{u_1} {g h : ℕ} {R : Type u_1} [CommRing R] (F : MvFormalGroup g R)
  (G : MvFormalGroup h R) : Type u_1

--% env 0

Raw input

{"cmd": "import FormalGroups.Basic\nimport FormalGroups.Hom\nimport FormalGroups.Additive\nimport FormalGroups.Iterates\n\nopen MvPowerSeries\nopen FormalGroups\nopen FormalGroups.MvFormalGroup\n\n#check MvFormalGroup\n#check addMv\n#check Hom"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "FormalGroups.MvFormalGroup.{u_1} (g : ℕ) (R : Type u_1) [CommRing R] : Type u_1"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "FormalGroups.MvFormalGroup.addMv.{u_1} (g : ℕ) (R : Type u_1) [CommRing R] : MvFormalGroup g R"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "FormalGroups.MvFormalGroup.Hom.{u_1} {g h : ℕ} {R : Type u_1} [CommRing R] (F : MvFormalGroup g R)\n  (G : MvFormalGroup h R) : Type u_1"}],
 "env": 0}

2. `MvFormalGroup` : une loi et quatre familles d’axiomes

Pour un anneau commutatif \(R\), toPowerSeries : Fin g → MvPowerSeries (Fin g ⊕ Fin g) R fournit une série par coordonnée. Les deux copies de Fin g représentent les blocs d’entrées \(X\) et \(Y\).

Les champs imposent successivement : un terme constant nul, la matrice identité au degré un dans le bloc gauche, la même condition dans le bloc droit, puis l’associativité exprimée par substitution de séries.

#check @FormalGroups.MvFormalGroup
#print FormalGroups.MvFormalGroup
#check @MvPowerSeries.subst
#check @MvPowerSeries.constantCoeff

#check @FormalGroups.MvFormalGroup MvFormalGroup : ℕ → (R : Type u_1) → [CommRing R] → Type u_1

#print FormalGroups.MvFormalGroup structure FormalGroups.MvFormalGroup.{u_1} (g : ℕ) (R : Type u_1) [CommRing R] : Type u_1
number of parameters: 3
fields:
  FormalGroups.MvFormalGroup.toPowerSeries : Fin g → MvPowerSeries (Fin g ⊕ Fin g) R
  FormalGroups.MvFormalGroup.constantCoeff_eq_zero : ∀ (i : Fin g), constantCoeff (self.toPowerSeries i) = 0
  FormalGroups.MvFormalGroup.coeff_single_inl : ∀ (i j : Fin g),
      (coeff (Finsupp.single (Sum.inl j) 1)) (self.toPowerSeries i) = if i = j then 1 else 0
  FormalGroups.MvFormalGroup.coeff_single_inr : ∀ (i j : Fin g),
      (coeff (Finsupp.single (Sum.inr j) 1)) (self.toPowerSeries i) = if i = j then 1 else 0
  FormalGroups.MvFormalGroup.assoc : ∀ (i : Fin g),
      subst
          (Sum.elim
            (fun j => subst (Sum.elim (fun l => X (Sum.inl l)) fun l => X (Sum.inr (Sum.inl l))) (self.toPowerSeries j))
            fun j => X (Sum.inr (Sum.inr j)))
          (self.toPowerSeries i) =
        subst
          (Sum.elim (fun j => X (Sum.inl j)) fun j =>
            subst (Sum.elim (fun l => X (Sum.inr (Sum.inl l))) fun l => X (Sum.inr (Sum.inr l))) (self.toPowerSeries j))
          (self.toPowerSeries i)
constructor:
  FormalGroups.MvFormalGroup.mk.{u_1} {g : ℕ} {R : Type u_1} [CommRing R]
    (toPowerSeries : Fin g → MvPowerSeries (Fin g ⊕ Fin g) R)
    (constantCoeff_eq_zero : ∀ (i : Fin g), constantCoeff (toPowerSeries i) = 0)
    (coeff_single_inl :
      ∀ (i j : Fin g), (coeff (Finsupp.single (Sum.inl j) 1)) (toPowerSeries i) = if i = j then 1 else 0)
    (coeff_single_inr :
      ∀ (i j : Fin g), (coeff (Finsupp.single (Sum.inr j) 1)) (toPowerSeries i) = if i = j then 1 else 0)
    (assoc :
      ∀ (i : Fin g),
        subst
            (Sum.elim
              (fun j => subst (Sum.elim (fun l => X (Sum.inl l)) fun l => X (Sum.inr (Sum.inl l))) (toPowerSeries j))
              fun j => X (Sum.inr (Sum.inr j)))
            (toPowerSeries i) =
          subst
            (Sum.elim (fun j => X (Sum.inl j)) fun j =>
              subst (Sum.elim (fun l => X (Sum.inr (Sum.inl l))) fun l => X (Sum.inr (Sum.inr l))) (toPowerSeries j))
            (toPowerSeries i)) :
    MvFormalGroup g R

#check @MvPowerSeries.subst @subst : {σ : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {τ : Type u_3} →
        {S : Type u_4} →
          [inst_1 : CommRing S] → [Algebra R S] → (σ → MvPowerSeries τ S) → MvPowerSeries σ R → MvPowerSeries τ S

#check @MvPowerSeries.constantCoeff @constantCoeff : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → MvPowerSeries σ R →+* R

--% env 1

Raw input

{"cmd": "#check @FormalGroups.MvFormalGroup\n#print FormalGroups.MvFormalGroup\n#check @MvPowerSeries.subst\n#check @MvPowerSeries.constantCoeff", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data": "MvFormalGroup : ℕ → (R : Type u_1) → [CommRing R] → Type u_1"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "structure FormalGroups.MvFormalGroup.{u_1} (g : ℕ) (R : Type u_1) [CommRing R] : Type u_1\nnumber of parameters: 3\nfields:\n  FormalGroups.MvFormalGroup.toPowerSeries : Fin g → MvPowerSeries (Fin g ⊕ Fin g) R\n  FormalGroups.MvFormalGroup.constantCoeff_eq_zero : ∀ (i : Fin g), constantCoeff (self.toPowerSeries i) = 0\n  FormalGroups.MvFormalGroup.coeff_single_inl : ∀ (i j : Fin g),\n      (coeff (Finsupp.single (Sum.inl j) 1)) (self.toPowerSeries i) = if i = j then 1 else 0\n  FormalGroups.MvFormalGroup.coeff_single_inr : ∀ (i j : Fin g),\n      (coeff (Finsupp.single (Sum.inr j) 1)) (self.toPowerSeries i) = if i = j then 1 else 0\n  FormalGroups.MvFormalGroup.assoc : ∀ (i : Fin g),\n      subst\n          (Sum.elim\n            (fun j => subst (Sum.elim (fun l => X (Sum.inl l)) fun l => X (Sum.inr (Sum.inl l))) (self.toPowerSeries j))\n            fun j => X (Sum.inr (Sum.inr j)))\n          (self.toPowerSeries i) =\n        subst\n          (Sum.elim (fun j => X (Sum.inl j)) fun j =>\n            subst (Sum.elim (fun l => X (Sum.inr (Sum.inl l))) fun l => X (Sum.inr (Sum.inr l))) (self.toPowerSeries j))\n          (self.toPowerSeries i)\nconstructor:\n  FormalGroups.MvFormalGroup.mk.{u_1} {g : ℕ} {R : Type u_1} [CommRing R]\n    (toPowerSeries : Fin g → MvPowerSeries (Fin g ⊕ Fin g) R)\n    (constantCoeff_eq_zero : ∀ (i : Fin g), constantCoeff (toPowerSeries i) = 0)\n    (coeff_single_inl :\n      ∀ (i j : Fin g), (coeff (Finsupp.single (Sum.inl j) 1)) (toPowerSeries i) = if i = j then 1 else 0)\n    (coeff_single_inr :\n      ∀ (i j : Fin g), (coeff (Finsupp.single (Sum.inr j) 1)) (toPowerSeries i) = if i = j then 1 else 0)\n    (assoc :\n      ∀ (i : Fin g),\n        subst\n            (Sum.elim\n              (fun j => subst (Sum.elim (fun l => X (Sum.inl l)) fun l => X (Sum.inr (Sum.inl l))) (toPowerSeries j))\n              fun j => X (Sum.inr (Sum.inr j)))\n            (toPowerSeries i) =\n          subst\n            (Sum.elim (fun j => X (Sum.inl j)) fun j =>\n              subst (Sum.elim (fun l => X (Sum.inr (Sum.inl l))) fun l => X (Sum.inr (Sum.inr l))) (toPowerSeries j))\n            (toPowerSeries i)) :\n    MvFormalGroup g R"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@subst : {σ : Type u_1} →\n  {R : Type u_2} →\n    [inst : CommRing R] →\n      {τ : Type u_3} →\n        {S : Type u_4} →\n          [inst_1 : CommRing S] → [Algebra R S] → (σ → MvPowerSeries τ S) → MvPowerSeries σ R → MvPowerSeries τ S"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@constantCoeff : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → MvPowerSeries σ R →+* R"}],
 "env": 1}

Lecture du résultat

Le constructeur affiché par #print expose les obligations exactes vérifiées par Lean. Fin g ⊕ Fin g n’est donc pas une notation décorative : le type sépare les deux opérandes de la loi, tandis que les coefficients de degré un encodent \(F(X,0)=X\) et \(F(0,Y)=Y\).

Un groupe formel porté par ses séries. Le #print montre l’architecture : MvFormalGroup g R est une structure dont le premier champ est toPowerSeries — la loi F est donnée comme une famille de séries formelles multivariées, et les axiomes (identité, inverse, associativité exprimés par identité de séries) sont des champs additionnels. Le choix de fondation est à lire lentement : plutôt qu’un type abstrait muni d’axiomes, le lake ancre les groupes formels DANS les séries entières, où les identités deviennent des égalités de coefficients — vérifiables terme à terme. C’est ce qui permettra aux exemples canoniques (addMv en section 6) d’être prouvés par rfl : l’égalité des séries se décide sur les coefficients. La hiérarchie g : ℕ (nombre de variables) puis R anneau commutatif suit exactement la théorie classique de Hazewinkel : le cadre est celui des groupes formels multivariés, dont le cas univarié est la spécialisation g = 1.

3. Commutativité et substitution sûre

IsComm exprime l’invariance de la loi après échange des deux blocs. La substitution de séries n’est toutefois bien définie que lorsque les séries substituées ont un terme constant nul : HasSubst rend cette précondition explicite, et hasSubst_toPowerSeries la dérive des champs de la structure.

Le lemme subst_X_add_X est la brique calculatoire qui transforme la substitution dans \(X_s+X_t\) en une somme.

#check @FormalGroups.MvFormalGroup.IsComm
#check @FormalGroups.MvFormalGroup.IsComm.comm
#check @FormalGroups.MvFormalGroup.hasSubst_toPowerSeries
#check @FormalGroups.MvFormalGroup.subst_X_add_X
#check @MvPowerSeries.HasSubst

#check @FormalGroups.MvFormalGroup.IsComm @IsComm : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → Prop

#check @FormalGroups.MvFormalGroup.IsComm.comm @IsComm.comm : ∀ {g : ℕ} {R : Type u_1} {inst : CommRing R} {F : MvFormalGroup g R} [self : F.IsComm] (i : Fin g),
  subst (Sum.elim (fun j => X (Sum.inr j)) fun j => X (Sum.inl j)) (F.toPowerSeries i) = F.toPowerSeries i

#check @FormalGroups.MvFormalGroup.hasSubst_toPowerSeries @hasSubst_toPowerSeries : ∀ {g : ℕ} {R : Type u_1} [inst : CommRing R] (F : MvFormalGroup g R), HasSubst F.toPowerSeries

#check @FormalGroups.MvFormalGroup.subst_X_add_X @subst_X_add_X : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} {τ : Type u_3} [Finite σ]
  {a : σ → MvPowerSeries τ R}, (∀ (s : σ), constantCoeff (a s) = 0) → ∀ (s t : σ), subst a (X s + X t) = a s + a t

#check @MvPowerSeries.HasSubst @HasSubst : {σ : Type u_1} → {τ : Type u_2} → {S : Type u_3} → [CommRing S] → (σ → MvPowerSeries τ S) → Prop

--% env 2

Raw input

{"cmd": "#check @FormalGroups.MvFormalGroup.IsComm\n#check @FormalGroups.MvFormalGroup.IsComm.comm\n#check @FormalGroups.MvFormalGroup.hasSubst_toPowerSeries\n#check @FormalGroups.MvFormalGroup.subst_X_add_X\n#check @MvPowerSeries.HasSubst", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@IsComm : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → Prop"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@IsComm.comm : ∀ {g : ℕ} {R : Type u_1} {inst : CommRing R} {F : MvFormalGroup g R} [self : F.IsComm] (i : Fin g),\n  subst (Sum.elim (fun j => X (Sum.inr j)) fun j => X (Sum.inl j)) (F.toPowerSeries i) = F.toPowerSeries i"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@hasSubst_toPowerSeries : ∀ {g : ℕ} {R : Type u_1} [inst : CommRing R] (F : MvFormalGroup g R), HasSubst F.toPowerSeries"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@subst_X_add_X : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} {τ : Type u_3} [Finite σ]\n  {a : σ → MvPowerSeries τ R}, (∀ (s : σ), constantCoeff (a s) = 0) → ∀ (s t : σ), subst a (X s + X t) = a s + a t"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@HasSubst : {σ : Type u_1} → {τ : Type u_2} → {S : Type u_3} → [CommRing S] → (σ → MvPowerSeries τ S) → Prop"}],
 "env": 2}

Lecture du résultat

Les types affichés montrent que la commutativité est une égalité de séries obtenue par substitution, et non une simple égalité point par point de coefficients écrite à la main. La contrainte HasSubst empêche précisément une composition formelle illégitime.

4. Morphismes, identité et composition

Un Hom F G est un tuple de séries à terme constant nul qui transporte la loi de F vers celle de G. L’identité utilise les variables canoniques X; la composition substitue les séries d’un morphisme dans celles de l’autre. End F spécialise cette structure aux endomorphismes de F.

#check @FormalGroups.MvFormalGroup.Hom
#print FormalGroups.MvFormalGroup.Hom
#check @FormalGroups.MvFormalGroup.Hom.id
#check @FormalGroups.MvFormalGroup.Hom.comp
#check @FormalGroups.MvFormalGroup.End

#check @FormalGroups.MvFormalGroup.Hom @Hom : {g h : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → MvFormalGroup h R → Type u_1

#print FormalGroups.MvFormalGroup.Hom structure FormalGroups.MvFormalGroup.Hom.{u_1} {g h : ℕ} {R : Type u_1} [CommRing R] (F : MvFormalGroup g R)
  (G : MvFormalGroup h R) : Type u_1
number of parameters: 6
fields:
  FormalGroups.MvFormalGroup.Hom.toPowerSeries : Fin h → MvPowerSeries (Fin g) R
  FormalGroups.MvFormalGroup.Hom.constantCoeff_eq_zero : ∀ (i : Fin h), constantCoeff (self.toPowerSeries i) = 0
  FormalGroups.MvFormalGroup.Hom.subst_eq : ∀ (i : Fin h),
      subst F.toPowerSeries (self.toPowerSeries i) =
        subst
          (Sum.elim (fun j => subst (fun l => X (Sum.inl l)) (self.toPowerSeries j)) fun j =>
            subst (fun l => X (Sum.inr l)) (self.toPowerSeries j))
          (G.toPowerSeries i)
constructor:
  FormalGroups.MvFormalGroup.Hom.mk.{u_1} {g h : ℕ} {R : Type u_1} [CommRing R] {F : MvFormalGroup g R}
    {G : MvFormalGroup h R} (toPowerSeries : Fin h → MvPowerSeries (Fin g) R)
    (constantCoeff_eq_zero : ∀ (i : Fin h), constantCoeff (toPowerSeries i) = 0)
    (subst_eq :
      ∀ (i : Fin h),
        subst F.toPowerSeries (toPowerSeries i) =
          subst
            (Sum.elim (fun j => subst (fun l => X (Sum.inl l)) (toPowerSeries j)) fun j =>
              subst (fun l => X (Sum.inr l)) (toPowerSeries j))
            (G.toPowerSeries i)) :
    F.Hom G

#check @FormalGroups.MvFormalGroup.Hom.id @Hom.id : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → (F : MvFormalGroup g R) → F.Hom F

#check @FormalGroups.MvFormalGroup.Hom.comp @Hom.comp : {g h k : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      {F : MvFormalGroup g R} → {G : MvFormalGroup h R} → {H : MvFormalGroup k R} → G.Hom H → F.Hom G → F.Hom H

#check @FormalGroups.MvFormalGroup.End @End : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → Type u_1

--% env 3

Raw input

{"cmd": "#check @FormalGroups.MvFormalGroup.Hom\n#print FormalGroups.MvFormalGroup.Hom\n#check @FormalGroups.MvFormalGroup.Hom.id\n#check @FormalGroups.MvFormalGroup.Hom.comp\n#check @FormalGroups.MvFormalGroup.End", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@Hom : {g h : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → MvFormalGroup h R → Type u_1"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "structure FormalGroups.MvFormalGroup.Hom.{u_1} {g h : ℕ} {R : Type u_1} [CommRing R] (F : MvFormalGroup g R)\n  (G : MvFormalGroup h R) : Type u_1\nnumber of parameters: 6\nfields:\n  FormalGroups.MvFormalGroup.Hom.toPowerSeries : Fin h → MvPowerSeries (Fin g) R\n  FormalGroups.MvFormalGroup.Hom.constantCoeff_eq_zero : ∀ (i : Fin h), constantCoeff (self.toPowerSeries i) = 0\n  FormalGroups.MvFormalGroup.Hom.subst_eq : ∀ (i : Fin h),\n      subst F.toPowerSeries (self.toPowerSeries i) =\n        subst\n          (Sum.elim (fun j => subst (fun l => X (Sum.inl l)) (self.toPowerSeries j)) fun j =>\n            subst (fun l => X (Sum.inr l)) (self.toPowerSeries j))\n          (G.toPowerSeries i)\nconstructor:\n  FormalGroups.MvFormalGroup.Hom.mk.{u_1} {g h : ℕ} {R : Type u_1} [CommRing R] {F : MvFormalGroup g R}\n    {G : MvFormalGroup h R} (toPowerSeries : Fin h → MvPowerSeries (Fin g) R)\n    (constantCoeff_eq_zero : ∀ (i : Fin h), constantCoeff (toPowerSeries i) = 0)\n    (subst_eq :\n      ∀ (i : Fin h),\n        subst F.toPowerSeries (toPowerSeries i) =\n          subst\n            (Sum.elim (fun j => subst (fun l => X (Sum.inl l)) (toPowerSeries j)) fun j =>\n              subst (fun l => X (Sum.inr l)) (toPowerSeries j))\n            (G.toPowerSeries i)) :\n    F.Hom G"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@Hom.id : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → (F : MvFormalGroup g R) → F.Hom F"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@Hom.comp : {g h k : ℕ} →\n  {R : Type u_1} →\n    [inst : CommRing R] →\n      {F : MvFormalGroup g R} → {G : MvFormalGroup h R} → {H : MvFormalGroup k R} → G.Hom H → F.Hom G → F.Hom H"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@End : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → Type u_1"}],
 "env": 3}

Lecture du résultat

Le champ subst_eq est la condition de compatibilité avec les lois formelles. L’égalité entre une composition d’identités et l’identité n’est pas nécessairement définitionnelle : les preuves du module déroulent les propriétés de substitution plutôt que de compter sur rfl.

5. Changement d’anneau : distinguer les deux `map`

Un morphisme d’anneaux R →+* S agit d’abord coefficient par coefficient sur une série. Le lake relève ensuite cette opération en un changement d’anneau de base du groupe formel entier. Les deux déclarations portent le même nom court ; leur qualification complète rend le niveau d’action explicite.

#check @FormalGroups.MvFormalGroup.map
#check @MvPowerSeries.map

#check @FormalGroups.MvFormalGroup.map @MvFormalGroup.map : {g : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] → {S : Type u_2} → [inst_1 : CommRing S] → (R →+* S) → MvFormalGroup g R → MvFormalGroup g S

#check @MvPowerSeries.map @MvPowerSeries.map : {σ : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → MvPowerSeries σ R →+* MvPowerSeries σ S

--% env 4

Raw input

{"cmd": "#check @FormalGroups.MvFormalGroup.map\n#check @MvPowerSeries.map", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@MvFormalGroup.map : {g : ℕ} →\n  {R : Type u_1} →\n    [inst : CommRing R] → {S : Type u_2} → [inst_1 : CommRing S] → (R →+* S) → MvFormalGroup g R → MvFormalGroup g S"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@MvPowerSeries.map : {σ : Type u_1} →\n  {R : Type u_2} →\n    {S : Type u_3} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → MvPowerSeries σ R →+* MvPowerSeries σ S"}],
 "env": 4}

Lecture du résultat

La sortie distingue bien la transformation d’une famille structurée MvFormalGroup de l’application sur une seule MvPowerSeries. Le second map est la brique coefficientielle utilisée pour construire le premier.

Les deux map, disambiguisés par leurs types. La sortie montre deux signatures : MvFormalGroup.map prend un morphisme d’anneaux R →+* S et transporte un groupe formel sur R vers un groupe formel sur S (changement de base — le même groupe, lu sur un autre anneau) ; MvPowerSeries.map agit au niveau des séries, coefficient par coefficient. La confusion est le piège d’API classique : les deux s’appellent map, mais le premier préserve la loi (c’est un morphisme de groupes formels au-dessus d’un morphisme d’anneaux) quand le second n’a aucune raison de respecter une loi quelconque — il n’est pas au courant des axiomes. La leçon Lean dépasse le cas : quand deux définitions partagent un nom, le #check @ des signatures est le document qui les sépare ; lire le TYPE d’une fonction est souvent plus sûr que lire son nom. Le point 4 du sommaire annonce exactement ce travail de distinction.

6. `addMv` : l’exemple canonique

addMv g R définit la loi additive composante par composante : la coordonnée \(i\) vaut \(X_i+Y_i\). Le module fournit aussi l’instance de commutativité. Les quatre exemples suivants rejouent les contrôles bornés de la source : forme de la loi, terme constant, coefficient linéaire et résolution d’instance.

example : (addMv 1 ℤ).toPowerSeries 0 = X (Sum.inl 0) + X (Sum.inr 0) := rfl

example : ((addMv 1 ℤ).toPowerSeries 0).constantCoeff = (0 : ℤ) :=
  (addMv 1 ℤ).constantCoeff_eq_zero 0

example : ((addMv 1 ℤ).toPowerSeries 0).coeff
    (Finsupp.single (Sum.inl 0) 1) = 1 := by
  have h := (addMv 1 ℤ).coeff_single_inl 0 0
  simpa using h

example : IsComm (addMv 1 ℤ) := inferInstance

#check (addMv 1 ℤ).constantCoeff_eq_zero

example : (addMv 1 ℤ).toPowerSeries 0 = X (Sum.inl 0) + X (Sum.inr 0) := rfl

example : ((addMv 1 ℤ).toPowerSeries 0).constantCoeff = (0 : ℤ) :=

  (addMv 1 ℤ).constantCoeff_eq_zero 0

example : ((addMv 1 ℤ).toPowerSeries 0).coeff

    (Finsupp.single (Sum.inl 0) 1) = 1 := by

  have h := (addMv 1 ℤ).coeff_single_inl 0 0

  simpa using h

example : IsComm (addMv 1 ℤ) := inferInstance

#check (addMv 1 ℤ).constantCoeff_eq_zero (addMv 1 ℤ).constantCoeff_eq_zero : ∀ (i : Fin 1), constantCoeff ((addMv 1 ℤ).toPowerSeries i) = 0

--% env 5

Raw input

{"cmd": "example : (addMv 1 \u2124).toPowerSeries 0 = X (Sum.inl 0) + X (Sum.inr 0) := rfl\n\nexample : ((addMv 1 \u2124).toPowerSeries 0).constantCoeff = (0 : \u2124) :=\n  (addMv 1 \u2124).constantCoeff_eq_zero 0\n\nexample : ((addMv 1 \u2124).toPowerSeries 0).coeff\n    (Finsupp.single (Sum.inl 0) 1) = 1 := by\n  have h := (addMv 1 \u2124).coeff_single_inl 0 0\n  simpa using h\n\nexample : IsComm (addMv 1 \u2124) := inferInstance\n\n#check (addMv 1 \u2124).constantCoeff_eq_zero", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data":
   "(addMv 1 ℤ).constantCoeff_eq_zero : ∀ (i : Fin 1), constantCoeff ((addMv 1 ℤ).toPowerSeries i) = 0"}],
 "env": 5}

Lecture du résultat

Le compilateur accepte rfl pour la forme explicite, réutilise le champ structurel pour le terme constant, simplifie le test d’égalité d’indices pour le coefficient, puis trouve automatiquement l’instance IsComm. Ces quatre mécanismes sont distincts malgré un exemple mathématique très compact.

addMv, l’exemple canonique — et pourquoi rfl suffit. L’exemple affirme que le terme d’ordre 0 de la loi additive s’écrit X(Sum.inl 0) + X(Sum.inr 0) : les deux coordonnées du Fin g ⊕ Fin g (l’espace ambiant du produit de deux copies) chacune portée par sa variable. Les deux corollaires qui suivent extraient le coefficient constant (0) et le coefficient linéaire (1) — la carte d’identité d’un groupe formel : pas de terme constant, partie linéaire = l’identité. La preuve par rfl n’est pas une économie de moyens mais un théorème déguisé : l’égalité des séries formelles est décidable sur les coefficients, et addMv est défini par ces coefficients — l’évaluateur les compare donc syntaxiquement. Les preuves suivantes (coeff) montrent le travail quand rfl ne suffit plus : exhiber le coefficient via Finsupp.single puis conclure — le pattern lecture-de-coefficient qui revient dans toute la théorie (hauteurs, itérés).

7. Itérés, partie linéaire et hauteur

nthSeries F 0 est la famille nulle et nthSeries F (n+1) substitue l’itéré précédent dans le premier bloc de la loi. linearPart extrait la matrice des coefficients de degré un. Enfin, en caractéristique \(p\), FiniteHeight p F demande la dimension finie du quotient par l’idéal engendré par les composantes de l’itéré d’ordre \(p\).

Le lake s’arrête volontairement avant les vecteurs de Witt, le théorème de Cartier et les séries d’Artin–Hasse.

#check @FormalGroups.MvFormalGroup.nthSeries
#check @FormalGroups.MvFormalGroup.nthSeries_zero
#check @FormalGroups.MvFormalGroup.nthSeries_succ
#check @FormalGroups.MvFormalGroup.linearPart
#check @FormalGroups.MvFormalGroup.FiniteHeight

example : (addMv 1 ℤ).nthSeries 0 = fun _ => 0 := rfl

#check @FormalGroups.MvFormalGroup.nthSeries @nthSeries : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → ℕ → Fin g → MvPowerSeries (Fin g) R

#check @FormalGroups.MvFormalGroup.nthSeries_zero @nthSeries_zero : ∀ {g : ℕ} {R : Type u_1} [inst : CommRing R] (F : MvFormalGroup g R), F.nthSeries 0 = fun x => 0

#check @FormalGroups.MvFormalGroup.nthSeries_succ @nthSeries_succ : ∀ {g : ℕ} {R : Type u_1} [inst : CommRing R] (F : MvFormalGroup g R) (n : ℕ),
  F.nthSeries (n + 1) = fun i => subst (Sum.elim (F.nthSeries n) fun j => X j) (F.toPowerSeries i)

#check @FormalGroups.MvFormalGroup.linearPart @linearPart : {g h : ℕ} → {R : Type u_1} → [CommRing R] → (Fin h → MvPowerSeries (Fin g) R) → Matrix (Fin h) (Fin g) R

#check @FormalGroups.MvFormalGroup.FiniteHeight @FiniteHeight : {g : ℕ} → (p : ℕ) → {K : Type u_1} → [inst : Field K] → [CharP K p] → MvFormalGroup g K → Prop

example : (addMv 1 ℤ).nthSeries 0 = fun _ => 0 := rfl

--% env 6

Raw input

{"cmd": "#check @FormalGroups.MvFormalGroup.nthSeries\n#check @FormalGroups.MvFormalGroup.nthSeries_zero\n#check @FormalGroups.MvFormalGroup.nthSeries_succ\n#check @FormalGroups.MvFormalGroup.linearPart\n#check @FormalGroups.MvFormalGroup.FiniteHeight\n\nexample : (addMv 1 \u2124).nthSeries 0 = fun _ => 0 := rfl", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@nthSeries : {g : ℕ} → {R : Type u_1} → [inst : CommRing R] → MvFormalGroup g R → ℕ → Fin g → MvPowerSeries (Fin g) R"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@nthSeries_zero : ∀ {g : ℕ} {R : Type u_1} [inst : CommRing R] (F : MvFormalGroup g R), F.nthSeries 0 = fun x => 0"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@nthSeries_succ : ∀ {g : ℕ} {R : Type u_1} [inst : CommRing R] (F : MvFormalGroup g R) (n : ℕ),\n  F.nthSeries (n + 1) = fun i => subst (Sum.elim (F.nthSeries n) fun j => X j) (F.toPowerSeries i)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@linearPart : {g h : ℕ} → {R : Type u_1} → [CommRing R] → (Fin h → MvPowerSeries (Fin g) R) → Matrix (Fin h) (Fin g) R"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@FiniteHeight : {g : ℕ} → (p : ℕ) → {K : Type u_1} → [inst : Field K] → [CharP K p] → MvFormalGroup g K → Prop"}],
 "env": 6}

Lecture du résultat

La loi récursive est visible dans le type de nthSeries_succ; l’exemple d’ordre zéro se ferme par réduction définitionnelle. linearPart passe d’une famille de séries à une matrice, tandis que FiniteHeight transforme les itérés en invariant de dimension d’un quotient.

8. Transparence axiomatique

#print axioms demande au noyau de remonter les dépendances axiomatiques des déclarations réellement utilisées. Une sortie vide ou des axiomes standards de Mathlib doivent être lus tels qu’affichés ; sorryAx ou native_decide seraient en revanche des signaux de dette formelle.

#print axioms FormalGroups.MvFormalGroup.addMv
#print axioms FormalGroups.MvFormalGroup.Hom.id
#print axioms FormalGroups.MvFormalGroup.Hom.comp
#print axioms FormalGroups.MvFormalGroup.map
#print axioms FormalGroups.MvFormalGroup.subst_X_add_X
#print axioms FormalGroups.MvFormalGroup.nthSeries

#print axioms FormalGroups.MvFormalGroup.addMv 'FormalGroups.MvFormalGroup.addMv' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms FormalGroups.MvFormalGroup.Hom.id 'FormalGroups.MvFormalGroup.Hom.id' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms FormalGroups.MvFormalGroup.Hom.comp 'FormalGroups.MvFormalGroup.Hom.comp' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms FormalGroups.MvFormalGroup.map 'FormalGroups.MvFormalGroup.map' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms FormalGroups.MvFormalGroup.subst_X_add_X 'FormalGroups.MvFormalGroup.subst_X_add_X' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms FormalGroups.MvFormalGroup.nthSeries 'FormalGroups.MvFormalGroup.nthSeries' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 7

Raw input

{"cmd": "#print axioms FormalGroups.MvFormalGroup.addMv\n#print axioms FormalGroups.MvFormalGroup.Hom.id\n#print axioms FormalGroups.MvFormalGroup.Hom.comp\n#print axioms FormalGroups.MvFormalGroup.map\n#print axioms FormalGroups.MvFormalGroup.subst_X_add_X\n#print axioms FormalGroups.MvFormalGroup.nthSeries", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'FormalGroups.MvFormalGroup.addMv' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "'FormalGroups.MvFormalGroup.Hom.id' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "'FormalGroups.MvFormalGroup.Hom.comp' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "'FormalGroups.MvFormalGroup.map' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "'FormalGroups.MvFormalGroup.subst_X_add_X' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "'FormalGroups.MvFormalGroup.nthSeries' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 7}

Lecture du résultat

Ces certificats sont produits par Lean sur la fermeture de dépendances compilée. Ils permettent de séparer trois dimensions : validité formelle (ce que le noyau accepte), exposition pédagogique (ce que ce notebook explique) et maturité mathématique (les constructions avancées encore hors périmètre).

Transparence axiomatique : le #print axioms comme audit. La sortie liste propext, Classical.choice, Quot.sound — les trois axiomes standard de Lean 4, et rien d’autre. Ce que cela certifie : ni addMv ni Hom.id (ni, par la même commande sur les autres théorèmes du lake) n’introduisent d’axiome ad hoc — aucune hypothèse smugglée sous forme d’axiome local, aucune tricherie sorry (un sorry apparaîtrait dans la liste). C’est le rituel d’hygiène des compagnons natifs : après chaque théorème majeur, l’audit axiomatique rend la preuve inspectable — le lecteur n’a pas à faire confiance au lake, il vérifie que tout se réduit aux fondations standard. Dans un notebook pédagogique, le geste vaut plus que le résultat : il enseigne le réflexe d’auditer ce qu’on importe, exactement comme un #print axioms sur une preuve de Mathlib apprend qu’elle ne repose que sur les choix constructifs attendus.

9. Exercices

Les cellules restent exécutables avant résolution : chaque TODO étudiant porte un stub calculable ou un énoncé commenté. Remplacez le stub, puis relancez le témoin associé.

Exercice 1 — Compter l’espace ambiant

La loi de dimension \(g\) reçoit deux blocs de \(g\) variables. Complétez nbVariables, puis obtenez 6 et 10 sur les deux témoins.

-- TODO étudiant : remplacer le corps par le nombre de variables de Fin g ⊕ Fin g.
def nbVariables (g : ℕ) : ℕ :=
  0

#eval nbVariables 3   -- attendu : 6
#eval nbVariables 5   -- attendu : 10

-- TODO étudiant : remplacer le corps par le nombre de variables de Fin g ⊕ Fin g.

def nbVariables (g : ℕ) : ℕ :=🟨 Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

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

#eval nbVariables 3   -- attendu : 6 0

#eval nbVariables 5   -- attendu : 10 0

--% env 8

Raw input

{"cmd": "-- TODO \u00e9tudiant : remplacer le corps par le nombre de variables de Fin g \u2295 Fin g.\ndef nbVariables (g : \u2115) : \u2115 :=\n  0\n\n#eval nbVariables 3   -- attendu : 6\n#eval nbVariables 5   -- attendu : 10", "env": 7}

Raw output

{"messages":
 [{"severity": "warning",
   "pos": {"line": 2, "column": 17},
   "endPos": {"line": 2, "column": 18},
   "data":
   "Variable name `g` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n  [apply] _g\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 5},
   "data": "0"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "0"}],
 "env": 8}

Exercice 2 — Échanger les deux blocs

IsComm.comm permute les injections gauche et droite. Remplacez l’identité par l’involution correspondante ; le témoin doit alors devenir true.

-- TODO étudiant : remplacer ce stub identité par l'échange Sum.inl ↔ Sum.inr.
def echangeBlocs (g : ℕ) : (Fin g ⊕ Fin g) → (Fin g ⊕ Fin g) :=
  fun s => s

def echangeBlocsOK : Bool :=
  echangeBlocs 2 (Sum.inl 0) == Sum.inr 0
  && echangeBlocs 2 (Sum.inr 0) == Sum.inl 0
  && echangeBlocs 2 (Sum.inl 1) == Sum.inr 1
  && echangeBlocs 2 (Sum.inr 1) == Sum.inl 1

#eval echangeBlocsOK   -- false avec le stub, true attendu

-- TODO étudiant : remplacer ce stub identité par l'échange Sum.inl ↔ Sum.inr.

def echangeBlocs (g : ℕ) : (Fin g ⊕ Fin g) → (Fin g ⊕ Fin g) :=

  fun s => s

def echangeBlocsOK : Bool :=

  echangeBlocs 2 (Sum.inl 0) == Sum.inr 0

  && echangeBlocs 2 (Sum.inr 0) == Sum.inl 0

  && echangeBlocs 2 (Sum.inl 1) == Sum.inr 1

  && echangeBlocs 2 (Sum.inr 1) == Sum.inl 1

#eval echangeBlocsOK   -- false avec le stub, true attendu false

--% env 9

Raw input

{"cmd": "-- TODO \u00e9tudiant : remplacer ce stub identit\u00e9 par l'\u00e9change Sum.inl \u2194 Sum.inr.\ndef echangeBlocs (g : \u2115) : (Fin g \u2295 Fin g) \u2192 (Fin g \u2295 Fin g) :=\n  fun s => s\n\ndef echangeBlocsOK : Bool :=\n  echangeBlocs 2 (Sum.inl 0) == Sum.inr 0\n  && echangeBlocs 2 (Sum.inr 0) == Sum.inl 0\n  && echangeBlocs 2 (Sum.inl 1) == Sum.inr 1\n  && echangeBlocs 2 (Sum.inr 1) == Sum.inl 1\n\n#eval echangeBlocsOK   -- false avec le stub, true attendu", "env": 8}

Raw output

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

Exercice 3 — Premier itéré de la loi additive

Montrez que le premier itéré de addMv 1 ℤ est la variable canonique. Commencez par nthSeries_succ, puis utilisez les lemmes de substitution vus plus haut. L’énoncé est commenté pour conserver une exécution complète sans sorry.

-- TODO étudiant : décommenter l'énoncé et compléter la preuve.
-- example : (addMv 1 ℤ).nthSeries 1 =
--     fun i => (X i : MvPowerSeries (Fin 1) ℤ) := by
--   rw [nthSeries_succ]
--   -- utilisez ensuite les lemmes de substitution du lake

#check FormalGroups.MvFormalGroup.nthSeries_succ

-- TODO étudiant : décommenter l'énoncé et compléter la preuve.

-- example : (addMv 1 ℤ).nthSeries 1 =

--     fun i => (X i : MvPowerSeries (Fin 1) ℤ) := by

--   rw [nthSeries_succ]

--   -- utilisez ensuite les lemmes de substitution du lake

#check FormalGroups.MvFormalGroup.nthSeries_succ FormalGroups.MvFormalGroup.nthSeries_succ.{u_1} {g : ℕ} {R : Type u_1} [CommRing R] (F : MvFormalGroup g R) (n : ℕ) :
  F.nthSeries (n + 1) = fun i => subst (Sum.elim (F.nthSeries n) fun j => X j) (F.toPowerSeries i)

--% env 10

Raw input

{"cmd": "-- TODO \u00e9tudiant : d\u00e9commenter l'\u00e9nonc\u00e9 et compl\u00e9ter la preuve.\n-- example : (addMv 1 \u2124).nthSeries 1 =\n--     fun i => (X i : MvPowerSeries (Fin 1) \u2124) := by\n--   rw [nthSeries_succ]\n--   -- utilisez ensuite les lemmes de substitution du lake\n\n#check FormalGroups.MvFormalGroup.nthSeries_succ", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "FormalGroups.MvFormalGroup.nthSeries_succ.{u_1} {g : ℕ} {R : Type u_1} [CommRing R] (F : MvFormalGroup g R) (n : ℕ) :\n  F.nthSeries (n + 1) = fun i => subst (Sum.elim (F.nthSeries n) fun j => X j) (F.toPowerSeries i)"}],
 "env": 10}

Attendus et anti-pièges (exercices 1 à 3)

Exercice 1 (compter l’espace ambiant). Attendu : nbVariables g = 2 * g — l’espace Fin g ⊕ Fin g est la réunion disjointe de deux copies de Fin g, donc 2g éléments. La preuve : Fin.card (Fin g ⊕ Fin g) = 2 * g via Finsupp.card ou Fin.card_sum. La sortie du stub montre l’avertissement du linter (variable non référencée) — le squelette attend une définition qui utilise g. Anti-piège : répondre g + g syntaxiquement sans preuve d’égalité — l’énoncé demande un Nat, la vérification attendue est nbVariables 2 = 4 (ou l’égalité prouvée), pas une formule non testée.

Exercice 2 (l’échange des blocs). Attendu : fun s => Sum.elim Sum.inr Sum.inl s (ou un match équivalent) — l’involution qui échange inl ↔︎ inr. La vérification echangeBlocsOK teste quatre croisements : inl 0 → inr 0, inr 0 → inl 0, inl 1 → inr 1 et inr 1 → inl 1 (les deux cases de chaque bloc pour g = 2). Lire le Bool attendu : echangeBlocsOK = true seulement si l’échange est correct sur TOUTES les cases testées. Anti-piège : définir l’échange seulement sur inl (match partiel) — le type (Fin g ⊕ Fin g) → (Fin g ⊕ Fin g) exige la totalité, et le test échoue sur inr.

Exercice 3 (premier itéré de la loi additive). Attendu : l’énoncé décommenté se prouve par rw [nthSeries_succ] puis les lemmes de substitution du lake — le premier itéré de addMv est la série linéaire identité fun i => X i. Intuition : itérer la loi donne F(F(x), y) − dont la partie de bas degré est la partie linéaire de F, qui pour la loi additive EST l’identité. Anti-piège : vouloir conclure par rfl — après le rw, le but est une égalité de fonctions vers des séries ; il faut funext puis l’égalité de séries (ou le lemme nthSeries_succ déjà orienté). Le #check du bas de cellule donne les noms disponibles : la preuve attendue est une composition de lemmes du lake, pas une expansion manuelle des coefficients.

Conclusion

Le kernel a chargé les quatre modules, inspecté les structures, recompilé les exemples additifs et demandé au noyau les dépendances axiomatiques de six déclarations. Le lake reste la source de vérité formelle ; ce compagnon fournit un parcours exécutable pour lire ses choix de types et ses invariants.

Pour prolonger l’étude, consultez le README du lake et ses modules bilingues. Les vecteurs de Witt, Cartier et Artin–Hasse constituent des extensions futures, non des résultats déjà couverts ici.

Retour au sommet

Objectifs, prérequis et durée

1. Le lake et son environnement formel

2. MvFormalGroup : une loi et quatre familles d’axiomes

Lecture du résultat

3. Commutativité et substitution sûre

Lecture du résultat

4. Morphismes, identité et composition

Lecture du résultat

5. Changement d’anneau : distinguer les deux map

Lecture du résultat

6. addMv : l’exemple canonique

Lecture du résultat

7. Itérés, partie linéaire et hauteur

Lecture du résultat

8. Transparence axiomatique

Lecture du résultat

9. Exercices

Exercice 1 — Compter l’espace ambiant

Exercice 2 — Échanger les deux blocs

Exercice 3 — Premier itéré de la loi additive

Attendus et anti-pièges (exercices 1 à 3)

Conclusion

2. `MvFormalGroup` : une loi et quatre familles d’axiomes

5. Changement d’anneau : distinguer les deux `map`

6. `addMv` : l’exemple canonique