Definitions/Def_AlgebraicGeometry_AdicThickening.lean

Fix a commutative ring R, an ideal I \subseteq R, a scheme X and a morphism f \colon X \to \operatorname{Spec} R. For each natural number n, adicThickeningBase I n is the morphism \operatorname{Spec}(R/I^{n+1}) \to \operatorname{Spec} R obtained by applying \operatorname{Spec} to the quotient map R \to R/I^{n+1} (note the index shift: the n-th stage uses the (n+1)-st power of I). The scheme adicThickening f I n is defined as Mathlib's chosen fibre product X \times_{\operatorname{Spec} R} \operatorname{Spec}(R/I^{n+1}), written X_n below, with adicThickeningι f I n the first projection \iota_n \colon X_n \to X and adicThickeningToBase f I n the second projection X_n \to \operatorname{Spec}(R/I^{n+1}); adicThickeningι_comp records the pullback square, namely that \iota_n followed by f equals the second projection followed by adicThickeningBase I n. Since R \to R/I^{n+1} is surjective, adicThickeningBase I n is a closed immersion, and isClosedImmersion_adicThickeningι registers as an instance that \iota_n is a closed immersion, being a pullback of one.

The comparison between consecutive stages comes from the surjection R/I^{n+2} \to R/I^{n+1} induced by I^{n+2} \subseteq I^{n+1}: adicThickeningBase_succ_comp says that \operatorname{Spec} of this surjection followed by adicThickeningBase I (n+1) is adicThickeningBase I n, and adicThickeningTransition f I n is the resulting morphism \tau_n \colon X_n \to X_{n+1} determined by the universal property, characterised by the two triangles adicThickeningTransition_ι (\tau_n followed by \iota_{n+1} is \iota_n) and adicThickeningTransition_toBase (\tau_n followed by the projection to \operatorname{Spec}(R/I^{n+2}) is the projection of X_n followed by \operatorname{Spec} of the quotient map). Three further lemmas, adicThickening_def, adicThickeningι_def and adicThickeningToBase_def, restate the definitions in terms of pullback, pullback.fst and pullback.snd. The module introduces vocabulary only: the tower X_0 \hookrightarrow X_1 \hookrightarrow \cdots \hookrightarrow X of closed subschemes cut out by the powers of I\mathcal{O}_X.