Effective Cartier ideal sheaves and blow-ups, from Mathlib's definitions alone

Two notions Mathlib lacks, defined from Mathlib's ideal sheaves X.IdealSheafData of a scheme X, their sections J.ideal U over the affine opens U and their inverse images J.comap f along morphisms f : Y ⟶ X, in a module that imports Mathlib only. The challenge file Challenge/Standard.lean, which imports Mathlib only, repeats them word for word, so that the resolution of a variety by a single blow-up (AlgebraicGeometry.exists_isBlowUpAlong_smooth) can be stated there.

• J.IsEffectiveCartier: the ideal sheaf J is locally generated by a single non-zero-divisor, so that its closed subscheme is an effective Cartier divisor [TSPA, Tag 01WR]; [TSPA, Tag 01WS].
• π.IsBlowUpAlong I: the morphism π : B ⟶ X is a blow-up of X along the ideal sheaf I, characterised by its universal property [TSPA, Tag 0806].

They are the library's Scheme.IdealSheafData.IsInvertible and IsBlowUp restated: Scheme.IdealSheafData.isEffectiveCartier_iff_isInvertible and Scheme.Hom.isBlowUpAlong_iff_isBlowUp (Hironaka.Scheme.BlowUp.BlowUpAlong).

def AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier {X : Scheme} (J : X.IdealSheafData) : Prop

An ideal sheaf J on X is effective Cartier, the ideal sheaf of an effective Cartier divisor, if near every point it is generated by a single non-zero-divisor: every point x has an affine open neighbourhood U and a non-zero-divisor g ∈ Γ(X, U) with J(U) = (g). Equivalently, J is an invertible sheaf (locally free of rank one), the Stacks project's definition of an effective Cartier divisor [TSPA, Tag 01WR]; [TSPA, Tag 01WS].

Equations

• J.IsEffectiveCartier = ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ g ∈ nonZeroDivisors ↑(X.presheaf.obj (Opposite.op ↑U)), J.ideal U = Ideal.span {g}

def AlgebraicGeometry.Scheme.Hom.IsBlowUpAlong {X B : Scheme} (π : B ⟶ X) (I : X.IdealSheafData) : Prop

A morphism π : B ⟶ X is a blow-up of X along the ideal sheaf I if the inverse image of the centre is an effective Cartier divisor (the inverse image I.comap π of I on B is effective Cartier), and every morphism f : Y ⟶ X along which the inverse image of the centre is an effective Cartier divisor (I.comap f is effective Cartier) factors as f = g ≫ π for a unique g : Y ⟶ B [TSPA, Tag 0806]. In other words π is final among the morphisms to X along which the closed subscheme of I pulls back to an effective Cartier divisor, so it is unique up to unique isomorphism over X.

It is the library's IsBlowUp I π (Scheme.Hom.isBlowUpAlong_iff_isBlowUp), and the library's blow-up Scheme.IdealSheafData.blowUp I is one.

Relation to the source.

• Restatement. The Stacks project defines the blow-up of X along I as the relative Proj of the Rees algebra $\bigoplus_n I^n$ and proves that it has this universal property [TSPA, Tag 0806]; Hauser takes the universal property as the definition, for a variety and a closed subvariety [Hau14, Definition 4.4]. Here, as in the Stacks project, X is any scheme, the centre is any closed subscheme, given by its ideal sheaf I, and the test morphisms f come from all schemes Y.

Equations

• One or more equations did not get rendered due to their size.