Inverse images of products of ideal sheaves

For a morphism of schemes f : X ⟶ Y, the inverse image I.comap f of an ideal sheaf I on Y is the ideal sheaf f⁻¹I·𝒪_X. This file shows that it is multiplicative: (I * J).comap f = I.comap f * J.comap f. Mathlib already has comap_sup, comap_bot and comap_top. With multiplicativity, taking inverse images respects all the semiring operations on ideal sheaves.

These are unconditional identities of ideal sheaves. When the ideals involved, including their inverse images, define effective Cartier divisors, they give the corresponding compatibility of divisor sums with pullback.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.comap_mul: (I * J).comap f = I.comap f * J.comap f.
• AlgebraicGeometry.Scheme.IdealSheafData.comap_pow: (I ^ n).comap f = I.comap f ^ n.
• AlgebraicGeometry.Scheme.IdealSheafData.pow_le_map_pow: if J.comap f ≤ I, then J ^ n ≤ (I ^ n).map f.
• AlgebraicGeometry.Scheme.IdealSheafData.comap_prod: the inverse image of a finite product is the product of the inverse images.
• AlgebraicGeometry.Scheme.IdealSheafData.compl_support_comap: the complement of the support of I.comap f is the inverse image of the complement of the support of I.
• AlgebraicGeometry.Scheme.IdealSheafData.comap_eq_top_iff: I.comap f is the unit ideal sheaf exactly when f maps into the complement of the support of I.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_mul {X Y : Scheme} (I J : Y.IdealSheafData) (f : X ⟶ Y) : (I * J).comap f = I.comap f * J.comap f

Inverse images of ideal sheaves are multiplicative. For every morphism f : X ⟶ Y, the inverse image of I * J is I.comap f * J.comap f. If these ideals define effective Cartier divisors, this is the ideal-sheaf identity underlying compatibility of their sum with pullback.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_pow {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) (n : ℕ) : (I ^ n).comap f = I.comap f ^ n

The inverse image of a power of an ideal sheaf is the power of the inverse image. When the ideals define effective Cartier divisors, this identifies the inverse image of n • D with n times the inverse image of D.

theorem AlgebraicGeometry.Scheme.IdealSheafData.pow_le_map_pow {X Y : Scheme} {I : X.IdealSheafData} {J : Y.IdealSheafData} {f : X ⟶ Y} (hf : J.comap f ≤ I) (n : ℕ) : J ^ n ≤ (I ^ n).map f

If J.comap f ≤ I, i.e. f carries V(I) into V(J) scheme-theoretically, then J ^ n ≤ (I ^ n).map f, so f carries V(I ^ n) into V(J ^ n).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_prod {X Y : Scheme} {ι : Type u_1} (s : Finset ι) (I : ι → Y.IdealSheafData) (f : X ⟶ Y) : (∏ i ∈ s, I i).comap f = ∏ i ∈ s, (I i).comap f

The inverse image of a finite product of ideal sheaves is the product of the inverse images. When the ideals involved define effective Cartier divisors, this is the corresponding identity for a finite sum of divisors.

theorem AlgebraicGeometry.Scheme.IdealSheafData.compl_support_comap {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) : (I.comap f).support.compl = (TopologicalSpace.Opens.map f.base).obj I.support.compl

The open complement of the support of I.comap f is the inverse image of the open complement of the support of I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_eq_top_iff {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) : I.comap f = ⊤ ↔ (TopologicalSpace.Opens.map f.base).obj I.support.compl = ⊤

The inverse image of an ideal sheaf I along f is the unit ideal sheaf exactly when f maps into the open complement of V(I).