5.1.1. Dictionary🔗

The statements use the standard notions of scheme theory [TSPA] under their names in Mathlib or in the library. Each line gives a classical notion, its Lean name, and the node of the library's definition where there is one.

• Scheme; morphism; composite; identity; isomorphism: Scheme, X ⟶ Y, f ≫ g (first f, then g), 𝟙 X, IsIso f.

• Spectrum of a ring; the point \operatorname{Spec} k: Spec R for R : CommRingCat; Spec (.of k).

• Open subsets; affine opens; functions on an open U; stalk at x: X.Opens, X.affineOpens, Γ(X, U), X.presheaf.stalk x.

• The part of f \colon X \to Y over an open U \subseteq Y: f ∣_ U : f ⁻¹ᵁ U ⟶ U, as in the weak form of Main Theorem I (Theorem 4.2.9.1).

• Algebraic k-scheme (separated and of finite type over k): X : AlgScheme k, with scheme X.left and structure morphism X.left ↘ Spec (.of k) (Algebraic k-schemes, Definition 2.1.1.2, Definition 2.1.1.1).

• Closed subscheme, given by its ideal sheaf; its support; inverse image along h: I : X.IdealSheafData, I.support, I.comap h (below).

• Stalk I_x and order \nu(I_x) of an ideal sheaf: I.stalkIdeal x, I.ord x (Definition 2.1.3.1, Definition 2.1.3.2).

• Reduced; irreducible components; integral (a variety, when of finite type over k): IsReduced X, irreducibleComponents X, IsIntegral X.

• Simple point (regular local ring); non-singular scheme; singular locus: X.IsRegularAt x, IsRegular X, X.singularLocus (Definition 2.1.2.1).

• Regular system of parameters, the local coordinates at a point: IsLocalRing.IsRegularSystemOfParameters (Definition 2.1.2.2).

• Smooth morphism, of relative dimension d; smooth locus X^{ns} of X over k: Smooth f, SmoothOfRelativeDimension d f, (X.left ↘ Spec (.of k)).smoothLocus. Over a field of characteristic zero a scheme of finite type is smooth over k exactly at its simple points (Definition 2.1.2.1).

• Cartesian square, P = X \times_S Y; base change along a field extension \sigma: IsPullback; a cartesian square over Spec σ (Definition 4.2.4.4).

• Effective Cartier divisor: the subscheme of an invertible ideal sheaf, I.IsInvertible (Definition 2.1.4.1).

• Blow-up, or monoidal transformation, with centre D; exceptional divisor: D.blowUp, D.blowUpπ, D.exceptionalDivisor (Definition 2.2.2.2, Definition 2.2.5.1).

• Quasi-coherent sheaf of modules, of finite type; projective bundle \mathbf{P}(\mathcal{E}); projective morphism: E : X.Modules with E.IsQuasicoherent and SheafOfModules.IsFiniteType E, E.projectiveBundle, IsProjective f (Definition 2.3.2.1, Definition 2.3.3.1).

• Finite succession of blow-ups: BlowUpSequence X (Definition 2.4.1.1).

• Normal crossings (Hironaka); simple normal crossings divisor (Kollár): IsSncBoundaryWith, IsSncBoundary (Definition 2.1.5.1); DivisorFamily and DivisorFamily.IsSnc (Definition 2.4.2.1, Definition 2.4.2.2).

• Analytic manifold; coherent sheaf of ideals; blow-up of a manifold; analytic space: AnalyticManifold 𝕜 E, Manifold.IdealSheaf, Manifold.IsBlowUp, AnalyticSpace K (Definition 3.1.1.1, Definition 3.1.3.1, Definition 3.1.4.2, Definition 3.3.3.1).

5.1.2. Ideal sheaves and closed subschemes🔗

Closed subschemes, centres and boundaries are given by their ideal sheaves: Mathlib's X.IdealSheafData on a scheme (Algebraic k-schemes, singularities and normal crossings), a locally finitely generated ideal sheaf of the sheaf of analytic functions on a manifold or an analytic space (Analytic manifolds). Ideal sheaves are ordered by inclusion, so a larger ideal sheaf is a smaller subscheme: the unit ideal sheaf ⊤ is the empty subscheme, so a blow-up with centre ⊤ is an isomorphism, and the zero ideal sheaf ⊥ is the whole space. "With nonzero stalks" reads Hironaka's "sheaf of non-zero ideals" at every stalk. The monoidal transformation with centre D is the blow-up along the ideal sheaf of D; "blow-up" and "monoidal transformation" are used interchangeably, as are Kollár's "cosupport" and the library's support of an ideal sheaf.

5.1.3. Names🔗

Declarations are referred to by their full Lean names. On each page the names in rendered signatures are shown relative to the namespaces that page opens, as its legend says; links and hovers keep the full name. The library names its declarations after what they are, in the manner of Mathlib. The algebraic vocabulary is in AlgebraicGeometry, most of it in AlgebraicGeometry.Scheme (the singular locus, blow-up sequences and divisor families) and AlgebraicGeometry.Scheme.IdealSheafData (ideal sheaves, the blow-up and the transforms), with the order of an ideal of a local ring in IsLocalRing, and the inputs and functors of the functorial theorems, with the properties these theorems assert of them, in AlgebraicGeometry. The analytic vocabulary is in AnalyticManifold (manifolds, their ideal sheaves and finite successions), built on the infrastructure in Manifold; analytic spaces, their vocabulary and their resolution theorems are in AnalyticSpace.

5.1.4. Sources🔗

The sources are cited by the keys of references.bib, the bibliography of the library, as [Kol07, Definition 29]: a citation links to the entry in the Blueprint Bibliography, the last part of this document, which lists the sources that the chapters and the annotations cite, with the places they are cited from. Item numbers in citations are the source's own.