The affine blow-up: separatedness and properness

The affine blow-up affineBlowUp I = Proj Rees(I) of Spec R along I, with its map affineBlowUp.π I to Spec R [Hau14, Definition 4.7]; [TSPA, Tags 01OF and 0804], is separated, and proper when I is finitely generated [TSPA, Tag 02NS]. Both are inherited from Mathlib's instances on Proj, Scheme.IsSeparated (Proj 𝒜) and IsProper (Proj.toSpecZero 𝒜) under Algebra.FiniteType (𝒜 0) A: the Rees algebra of a finitely generated ideal is of finite type (reesAlgebra.finiteType_of_fg), and the second factor of π is an isomorphism. The hypothesis I.FG enters only here: finiteness belongs to properness, not to the construction; for R Noetherian it is automatic.

The blow-up of a general scheme along a closed subscheme is glued from these affine blow-ups over the affine opens of the base (blowUpOf).

instance AlgebraicGeometry.affineBlowUp.isSeparated {R : Type u} [CommRing R] (I : Ideal R) : (affineBlowUp I).IsSeparated

The affine blow-up is a separated scheme, as every Proj is [TSPA, Tag 01MC].

instance AlgebraicGeometry.affineBlowUp.isSeparated_π {R : Type u} [CommRing R] (I : Ideal R) : IsSeparated (π I)

The blow-up map is separated (Mathlib's IsSeparated (Proj.toSpecZero 𝒜)).

theorem AlgebraicGeometry.affineBlowUp.isProper_π {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) : IsProper (π I)

For I finitely generated the blow-up map is proper [TSPA, Tag 02NS]: Proj.toSpecZero is proper because reesAlgebra I is of finite type over its degree-zero part (reesAlgebra.finiteType_of_fg), and the second factor is an isomorphism.

instance AlgebraicGeometry.affineBlowUp.isProper_π_of_isNoetherianRing {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] : IsProper (π I)

Over a Noetherian ring every blow-up map is proper (every ideal is finitely generated).