Blowing up a product centre: the generic layer #
Blowing up X along I and then blowing up the result along the inverse image of J is the
blow-up of X along I·J [TSPA, Tag 080A]. This module proves the mathematics of that lemma
once, for arbitrary morphisms carrying the relevant clause of the universal property
[Hau14, Definition 4.4] — admissibility (the inverse image of the centre is invertible) and
universality (unique lifts of admissible morphisms) — so that the statements about the blow-up
AlgebraicGeometry.Scheme.IdealSheafData.blowUp (Hironaka.Scheme.BlowUp.Glue.Product) are
instances. The chart lemmas are also used for the charts of blow-ups of smooth centres
(Hironaka.Scheme.Smooth.ChartIso, Hironaka.Scheme.Smooth.BlowUpSmoothChart) and for normal
crossings divisors (Hironaka.Resolution.Algebraic.Snc.SncInvertible).
Main declarations #
AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.of_mul: the factors of an invertible ideal sheaf are invertible (fromIdeal.IsInvertible.of_mul); powers of an invertible ideal sheaf are invertible byisInvertible_powofHironaka.Scheme.BlowUp.Transform.affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors_of_mem: a nonzerodivisor ofRis a nonzerodivisor ofR[I/a].isInvertible_comap_of_charts: a morphism covered by chartsSpec R[I/a]pulls invertible ideal sheaves back to invertible ones.isInvertible_comap_mul_comp: the composite of two admissible morphisms is admissible for the product centre.existsUnique_lift_comp: the composite of two universal morphisms is universal for the product centre.exists_iso_of_universal: two admissible universal morphisms for the same centre are isomorphic over the base by a unique isomorphism [Hau14, Remark 4.5].IsBlowUp.comp,IsBlowUp.exists_iso,IsBlowUp.comp_iso: the same, packaged with the predicateIsBlowUpofHironaka.Scheme.BlowUp.UniversalProperty.
The arguments #
Multiplicativity of the inverse image ideal sheaf (comap_mul, comap_pow) is proved in
Hironaka.Scheme.BlowUp.Transform.StrictTransform.
Pullback of an invertible ideal sheaf along a chart-covered morphism. Let y ∈ B and
x = π y. Invertibility of K gives an affine U ∋ x with K.ideal U = (k), k a
nonzerodivisor of Γ(X, U); y ∈ π⁻¹U lies in the image of some chart chart U a. The inverse
image of K.comap π along the chart is the inverse image of K along chart U a ≫ π = Spec (Γ(X, U) → Γ(X, U)[I(U)/a]) ≫ fromSpec, i.e. (comap_fromSpec, comap_ofIdealTop_Spec_map)
the ideal sheaf of the principal ideal generated by the image of k in Γ(X, U)[I(U)/a]; that
image is a nonzerodivisor (R → R_a preserves nonzerodivisors, and R[I/a] ⊆ R_a is a subring),
so this ideal sheaf is invertible (isInvertible_ofIdealTop_span_singleton); the charts of this
kind cover B, and invertibility descends along a cover by open immersions
(IsInvertible.of_forall_comap_isOpenImmersion).
Admissibility of the composite. (I·J).comap (b' ≫ b) = I.comap (b' ≫ b) · (J.comap b).comap b' is a product of two invertible ideal sheaves (IsInvertible.mul).
Universality of the composite. A morphism f admissible for I·J is admissible for
I and for J (IsInvertible.of_mul), so lifts uniquely to g₁ along b; then
(J.comap b).comap g₁ = J.comap (g₁ ≫ b) = J.comap f is invertible, so g₁ lifts uniquely to g₂
along b'; and any lift g of f along b' ≫ b has g ≫ b' a lift of f along b, hence
g ≫ b' = g₁, hence g = g₂.
Uniqueness of universal objects. With π₁, π₂ both admissible and universal for K,
π₁ lifts along π₂ to u and π₂ lifts along π₁ to v; u ≫ v and 𝟙 are both lifts of
π₁ along π₁, so they coincide, and symmetrically; u is the unique morphism over X.
The pullback of an effective Cartier divisor along a blow-up is [TSPA, Tag 0809]; the universal property of the blow-up is [TSPA, Tag 0806]; [Hau14, Definition 4.4].
The ideal sheaf of an ideal of R on Spec R (specIdealSheaf) is
multiplicative: ofIdealTop is a ring isomorphism (equivOfIsAffine) and Ideal.map is
multiplicative.
The factors of an invertible ideal sheaf are invertible (from Ideal.IsInvertible.of_mul
through the affine-local criterion isInvertible_iff_forall_ideal): if I * J is invertible, so
are I and J.
The converse for m ≥ 1: if I ^ m is invertible, so is I.
The image in R[I/a] of a nonzerodivisor of R is a nonzerodivisor, because R → R_a
preserves nonzerodivisors
(IsLocalization.map_nonZeroDivisors_le) and R[I/a] ⊆ R_a is a subring
(mem_nonZeroDivisors_of_injective).
The ideal sheaf on Spec R[I/a] of the extension of a principal ideal J = (k) of R with
k a nonzerodivisor is invertible: its generator, the image of k, is a nonzerodivisor of
R[I/a] and hence of Γ(Spec R[I/a], ⊤). (Stated with R a plain ring: the chart computation
comap_comap_eq_of_chart_π lands exactly here with R = Γ(X, U).)
The inverse image of K.comap π along a chart chart U a with
chart U a ≫ π = Spec (algebraMap) ≫ fromSpec is the ideal sheaf on Spec Γ(X, U)[I(U)/a] of the
extension of K.ideal U (comap_fromSpec, comap_ofIdealTop_Spec_map).
Every point of B lies on a chart over an affine open U on which the invertible K has a
nonzerodivisor generator (the pointwise definition of IsInvertible and the chart cover of
π⁻¹U).
On a chart over an affine open U where K.ideal U = (k) with k a nonzerodivisor, the
inverse image of K.comap π is the ideal sheaf of the principal ideal generated by the image of
k in Γ(X, U)[I(U)/a], a nonzerodivisor (algebraMap_mem_nonZeroDivisors_of_mem), hence
invertible (isInvertible_ofIdealTop_span_singleton).
Bookkeeping for isInvertible_comap_of_charts: the charts relevant to an invertible K — an
affine open U,
a chart index a ∈ I(U), and a nonzerodivisor generator k of K(U). (A structure rather than
a subtype of a sigma type: it keeps the index terms small for unification.)
- U : ↑X.affineOpens
The affine open.
The chart over
U.- k : ↑(X.presheaf.obj (Opposite.op ↑self.U))
A generator of
K(U). The generator is a nonzerodivisor.
K(U) = (k).
Instances For
A chart-covered morphism pulls invertible ideal sheaves back to invertible ones
([TSPA, Tag 080A]; the pullback of an effective Cartier divisor along a blow-up, [TSPA, Tag 0809]):
a morphism π : B ⟶ X covered by charts — open immersions
chart U a : Spec Γ(X, U)[I(U)/a] ⟶ B with
chart U a ≫ π = Spec (algebraMap) ≫ U.isoSpec.inv ≫ U.ι whose images cover π⁻¹U — pulls
every invertible ideal sheaf K on X back to an invertible ideal sheaf on B.
Admissibility of the composite [TSPA, Tag 080A] (the ideal of E'' = E' + (b')⁻¹E is
(b ∘ b')⁻¹𝓘 (b ∘ b')⁻¹𝓙 𝓞_{X''}): if I pulls back along b' ≫ b to an invertible ideal sheaf
and J.comap b pulls back along b' to an invertible ideal sheaf (the exceptional
ideal of b'), then b' ≫ b is admissible for I * J (comap_mul, IsInvertible.mul).
Universality of the composite [TSPA, Tag 080A]; [Hau14, Definition 4.4] (clause (ii)): if b
is universal for I and b' is universal for J.comap b (unique lifts of admissible morphisms),
then b' ≫ b is universal for I * J. An f admissible
for I * J is admissible for I (IsInvertible.of_mul) and lifts uniquely to g₁ along b;
(J.comap b).comap g₁ = J.comap f is invertible, so g₁ lifts uniquely to g₂ along b'; a lift
g of f along b' ≫ b has g ≫ b' a lift of f along b, so g ≫ b' = g₁ and g = g₂.
Uniqueness of the blow-up up to unique isomorphism [Hau14, Remark 4.5]; [TSPA, Tag 080A]:
two morphisms π₁ : B₁ ⟶ X, π₂ : B₂ ⟶ X, both admissible and universal for K, are isomorphic
over
X by a unique isomorphism: e.hom is the lift of π₁ along π₂, e.inv the lift of π₂
along π₁, and the composites are identities because 𝟙 is the unique lift of πᵢ along πᵢ.
Two morphisms over X from a source admissible for K into a target universal for K
coincide (hom_ext for any universal morphism).
The composite of two blow-ups is the blow-up of the product centre [TSPA, Tag 080A], with
the predicate IsBlowUp [Hau14, Definition 4.4]: if b is a blow-up of X along I, b' a
blow-up of X' along J.comap b, and I pulls back along b' ≫ b to an invertible ideal sheaf,
then b' ≫ b is a blow-up of X along I * J.
Two blow-ups of X along K are isomorphic over X by a unique isomorphism
[Hau14, Remark 4.5].
The blow-up predicate transported along an isomorphism of the base (used to read the blow-up
of an affine chart over Spec Γ(U), [Hau14, Theorem 4.19]) — if π : B ⟶ X
is a blow-up along I, then π ≫ e.hom : B ⟶ X' is a blow-up along I.comap e.inv.