theorem Blowup.blowup_iso_outside_center {R : Type u_1} [CommRing R] (I : Ideal R) : ∃ (U : (blowupAlong I).Opens) (f : ↑U ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)), AlgebraicGeometry.IsOpenImmersion f

Restatement of blowup_iso_away_from_center: the blow-up morphism is an isomorphism over the complement of the center (Prop 34).

theorem Blowup.exceptionalLocus_isClosed {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (C : TopologicalSpace.Closeds ↑Y.toTopCat) : IsClosed ↑(exceptionalLocusSet π C)

The exceptional locus π⁻¹(C) is a closed subset of X.

theorem Blowup.properTransform_eq_closure {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (Z C : TopologicalSpace.Closeds ↑Y.toTopCat) : ↑(properTransformSet π Z C) = closure (⇑π ⁻¹' (↑Z \ ↑C))

The proper transform unfolds to the closure of the preimage of Z \ C.

theorem Blowup.properTransform_isClosed {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (Z C : TopologicalSpace.Closeds ↑Y.toTopCat) : IsClosed ↑(properTransformSet π Z C)

The proper transform is a closed subset of X.

theorem Blowup.exceptionalLocus_eq_preimage {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (C : TopologicalSpace.Closeds ↑Y.toTopCat) : ↑(exceptionalLocusSet π C) = ⇑π ⁻¹' ↑C

The underlying set of the exceptional locus is exactly the preimage of the center.