A morphism of schemes is of finite type (FiniteType f) if it is locally of finite type and quasi-compact [TSPA, Tag 01T0]. The class bundles Mathlib's LocallyOfFiniteType and QuasiCompact, as Mathlib's IsProper bundles its parts: its parents are instances (FiniteType.toLocallyOfFiniteType supplies the LocallyOfFiniteType that Mathlib's smoothLocus asks for), and conversely FiniteType f is inferred from the two parts.

AlgScheme k is the category of algebraic k-schemes: Mathlib's MorphismProperty.Over for the property "of finite type and separated" of the structure morphism to \operatorname{Spec} k. An object X is a scheme X.left with a structure morphism X.hom having the property, and a morphism h : Y ⟶ X is a morphism of schemes h.left over \operatorname{Spec} k. The instances AlgScheme.over and AlgScheme.finiteType make the structure morphism available to Mathlib's notation X.left ↘ Spec (.of k) and its finite type available to instance search, which does not see through the bundled property.

A point x of a scheme X is simple (X.IsRegularAt x) if the local ring \mathcal{O}_{X,x} is a regular local ring; X is non-singular (IsRegular X, a class with the single field isRegularAt) if every point is simple, and the singular locus X.singularLocus is the set of points that are not simple.

These are Hironaka's notions, defined by the local rings alone and without reference to a base field. In the functorial theorems the singular locus is instead the complement of Mathlib's smoothLocus of the structure morphism over k; over a field of characteristic zero the two agree for a scheme of finite type, since regularity and smoothness coincide over a perfect field.

A family z_1, \dots, z_n in a local ring R is a regular system of parameters if it generates the maximal ideal and n is the Krull dimension of R. In a regular local ring these are the minimal generating systems of \mathfrak m; they play the role of local coordinates in the normal crossings conditions (Definition 2.1.5.1, Definition 2.4.2.2).

The stalk J_x \subseteq \mathcal{O}_{X,x} of an ideal sheaf, J.stalkIdeal x, is the ideal generated by the germs at x of the sections of J over the affine opens containing x. An ideal sheaf has nonzero stalks (IsNonzeroEverywhere J) if J_x \ne 0 at every point: Hironaka's "coherent sheaf of non-zero ideals", read at every stalk. On a non-singular scheme this is Kollár's "not zero on any irreducible component" [Kol07, Theorem 35].

The order of an ideal I of a local ring (R, \mathfrak m) is \operatorname{ord} I = \sup\{r : I \subseteq \mathfrak m^r\} in \mathbb{N} \cup \{\infty\} (IsLocalRing.ord, [Kol07, Definition 47]). The order of an ideal sheaf at a point, J.ord x, is the order of the stalk: Hironaka's \nu(J_x). It is \infty exactly when J_x = 0 (by the Krull intersection theorem) and 0 exactly when J_x is the unit ideal, so an ideal sheaf with nonzero stalks has finite order everywhere, and the maximal order of Main Theorem II (Theorem 4.2.1.2) is a natural number.

An ideal sheaf is invertible if it is locally generated by a single nonzerodivisor; its closed subscheme is then an effective Cartier divisor. IdealSheafData.IsInvertible is the form used by the blow-up construction: every point has an affine open neighbourhood U on which J(U) is generated by one nonzerodivisor [TSPA, Tag 01WS]; [Kol07, Warning 20]. The unit ideal sheaf is invertible (isInvertible_top), which is why a blow-up with empty centre is an isomorphism (Definition 2.2.3.1). The invertibility of a boundary follows from the hypotheses of the main theorems and is not a separate hypothesis (Theorem 4.2.1.2); the notion enters their statements through the blow-up and in the conclusion of Corollary 3 (Theorem 4.2.5.1).

Hironaka's Definition 2: E has only normal crossings with D if at every point x of D there is a regular system of parameters (z_1, \dots, z_n) of \mathcal{O}_{X,x} such that the ideal of each irreducible component of E through x (a minimal prime of E_x) is generated by one of the z_i, and the ideal of D is generated by some of the z_i. With D = X (the zero ideal sheaf) one says that E has only normal crossings.

The components are read locally, as the minimal primes of the stalk, as Hironaka does; on a scheme these are the local ideals of the global irreducible components of E, each asked to be a parameter, so at the points of D the condition is simple normal crossings of the reduced subscheme E, and with D. Nothing is asserted at the points off D (for the empty D the condition always holds), whereas the manifold predicate of the same name (Definition 3.1.5.1) also asserts simple normal crossings of the boundary at every point. The functorial theorems use Kollár's simple normal crossings, which is phrased on a family of global components (Definition 2.4.2.2); the two agree on the family of irreducible components of E (isSncBoundaryWith_iff_hasSncWith_componentFamily, and isSncBoundary_iff_isSnc_componentFamily on a scheme smooth over k).