Blueprint.lean

import Verso
import VersoManual
import VersoBlueprint
import VersoBlueprint.Commands.Graph
import VersoBlueprint.Commands.Summary

import Blueprint.Chapters.Series
import Blueprint.Chapters.Theorem1
import Blueprint.Chapters.Points
import Blueprint.Chapters.Theorem2
import Blueprint.Chapters.Reciprocity

open Verso.Genre
open Verso.Genre.Manual
open Informal

#doc (Manual) "Lubin–Tate Theory Blueprint" =>

A blueprint for the `FormalGroupLaws.LubinTateTheory` part of this project: a formalization of

> J. Lubin and J. Tate, *Formal complex multiplication in local fields*,
> Annals of Mathematics *81* (1965), 380–387.

The chapters follow the paper. Section 1 constructs, for each prime $`\pi` of a nonarchimedean
local field $`k` and each $`f \in \mathcal{F}_\pi`, a formal group law $`F_f` over
$`A = \mathcal{O}_k` together with a formal $`A`-module structure (Theorem 1), and studies its
torsion points (Theorem 2). Section 2 builds the reciprocity homomorphism $`r_\pi` and proves
that it is independent of $`\pi` (Theorem 3).

The dictionary between the paper's notation and the Lean names is kept in
`FormalGroupLaws/LubinTateTheory/README.md`; each blueprint node below links directly to the Lean
declaration that formalizes it, so the progress bars and the dependency graph are computed from
the actual state of the Lean development.

{include 0 Blueprint.Chapters.Series}

{include 0 Blueprint.Chapters.Theorem1}

{include 0 Blueprint.Chapters.Points}

{include 0 Blueprint.Chapters.Theorem2}

{include 0 Blueprint.Chapters.Reciprocity}

{blueprint_graph}

{blueprint_summary}