The affine computation of the inverse image ideal sheaf

For f : Y ⟶ X and affine opens U ⊆ X, V ⊆ Y with f(V) ⊆ U, the ideal of I.comap f on V is the extension I(U)·Γ(Y, V) along f♯ : Γ(X, U) → Γ(Y, V): the ideal sheaf of the inverse image is the image of f^*I → 𝒪_Y (compare the proof of [TSPA, Tag 0805]). Mathlib defines I.comap f as the kernel of the first projection of Y ×_X V(I) and has only the open-immersion case (ideal_comap_of_isOpenImmersion) and the pushforward direction (ideal_map_of_isAffineHom).

Main declarations

• ker_appTop_Spec_map: the kernel of Γ(Spec R) → Γ(Spec S) induced by φ : R → S is ker φ transported along ΓSpecIso.
• comap_ofIdealTop_Spec_map (the case f = Spec.map φ): the comap of the ideal sheaf of I ⊆ R along Spec S → Spec R is the ideal sheaf of IS.
• ideal_comap_of_le: the general affine formula; map_germ_ideal_comap: its stalk form.
• exists_affineOpen_generator_of_isInvertible: for f admissible for I (the inverse image ideal sheaf invertible), every point has an affine neighbourhood on which the inverse image ideal is generated by the image of an element of I(U), a nonzerodivisor.

The argument (Spec case)

Spec (R/I) → Spec R is a closed immersion with kernel the ideal sheaf of I, so I.comap f is the kernel of Spec S ×_{Spec R} Spec (R/I) → Spec S (ker_fst_of_isClosedImmersion); the fibre product is Spec (S ⊗_R R/I) (pullbackSpecIso), the projection corresponds to S → S ⊗_R R/I, s ↦ s ⊗ 1, and its kernel is IS because S ⊗_R R/I ≅ S/IS (quotIdealMapEquivTensorQuot). A kernel of a morphism into an affine scheme is the ideal sheaf of the kernel of its global sections (ker_of_isAffine).

theorem AlgebraicGeometry.Scheme.IdealSheafData.appTop_Spec_map {R S : CommRingCat} (φ : R ⟶ S) : Hom.appTop (Spec.map φ) = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).hom (CategoryTheory.CategoryStruct.comp φ (ΓSpecIso S).inv)

theorem AlgebraicGeometry.Scheme.IdealSheafData.injective_ΓSpecIso_inv {S : CommRingCat} : Function.Injective ⇑(CommRingCat.Hom.hom (ΓSpecIso S).inv)

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_appTop_Spec_map {R S : CommRingCat} (φ : R ⟶ S) : RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))) = Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) (RingHom.ker (CommRingCat.Hom.hom φ))

The kernel of the map on global sections induced by φ : R → S is ker φ, transported to Γ(Spec R, ⊤).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_Spec_map_mk {R : CommRingCat} (I : Ideal ↑R) : Hom.ker (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) I)

The closed immersion Spec (R/I) → Spec R has kernel the ideal sheaf of I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_ofIdealTop_Spec_map {R S : CommRingCat} (φ : R ⟶ S) (I : Ideal ↑R) : (ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) I)).comap (Spec.map φ) = ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso S).inv) (Ideal.map (CommRingCat.Hom.hom φ) I))

The case f = Spec.map φ: the comap of the ideal sheaf of I ⊆ R along Spec S → Spec R is the ideal sheaf of IS.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isPullback_fromSpec {X : Scheme} (J : X.IdealSheafData) (U : ↑X.affineOpens) : CategoryTheory.IsPullback (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U)))) (J.subschemeCover.f U) (IsAffineOpen.fromSpec ⋯) J.subschemeι

The closed subscheme of J over the affine open U is Spec (Γ(X, U)/J(U)): the square with hU.fromSpec and J.subschemeι is a pullback.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_fromSpec {X : Scheme} (J : X.IdealSheafData) (U : ↑X.affineOpens) : J.comap (IsAffineOpen.fromSpec ⋯) = ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso (X.presheaf.obj (Opposite.op ↑U))).inv) (J.ideal U))

The comap of an ideal sheaf along hU.fromSpec is the ideal sheaf of J(U) on Spec Γ(X, U) (the ΓSpecIso compatibility of ofIdealTop).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le {X Y : Scheme} (I : X.IdealSheafData) (f : Y ⟶ X) (U : ↑X.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : (I.comap f).ideal V = Ideal.map (CommRingCat.Hom.hom (Hom.appLE f (↑U) (↑V) e)) (I.ideal U)

For affine opens U ⊆ X, V ⊆ Y with f(V) ⊆ U, the ideal of I.comap f on V is I(U)·Γ(Y, V) (compare the proof of [TSPA, Tag 0805]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_germ_ideal_comap {X Y : Scheme} (I : X.IdealSheafData) (f : Y ⟶ X) (y : ↥Y) (U : ↑X.affineOpens) (V : ↑Y.affineOpens) (hy : y ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : Ideal.map (CommRingCat.Hom.hom (Y.presheaf.germ (↑V) y hy)) ((I.comap f).ideal V) = Ideal.map (CommRingCat.Hom.hom (Hom.stalkMap f y)) (Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) (f y) ⋯)) (I.ideal U))

The stalk of I.comap f at y, spelled through affine opens V ∋ y and U ∋ f y with f(V) ⊆ U, is generated by the image under f.stalkMap y of the stalk of I at f y.

theorem AlgebraicGeometry.Scheme.IdealSheafData.span_germ_appLE_eq_iff_of_isOpenImmersion {X Y : Scheme} (I : X.IdealSheafData) (j : Y ⟶ X) [IsOpenImmersion j] (y : ↥Y) (U : ↑X.affineOpens) (V : ↑Y.affineOpens) (hy : y ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map j.base).obj ↑U) (a : ↑(X.presheaf.obj (Opposite.op ↑U))) : Ideal.span {(CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ (↑V) y hy)) ((CategoryTheory.ConcreteCategory.hom (Hom.appLE j (↑U) (↑V) e)) a)} = Ideal.map (CommRingCat.Hom.hom (Y.presheaf.germ (↑V) y hy)) ((I.comap j).ideal V) ↔ Ideal.span {(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) (j y) ⋯)) a} = Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) (j y) ⋯)) (I.ideal U)

For an open immersion j the stalk map is an isomorphism, so a generates the stalk ideal of I at j y iff j♯a generates the stalk ideal of I.comap j at y.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_affineOpen_generator_of_isInvertible {X Y : Scheme} (I : X.IdealSheafData) (f : Y ⟶ X) (hf : (I.comap f).IsInvertible) (U : ↑X.affineOpens) (y : ↥Y) (hy : y ∈ (TopologicalSpace.Opens.map f.base).obj ↑U) : ∃ (V : ↑Y.affineOpens), y ∈ ↑V ∧ ∃ (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), ∃ a ∈ I.ideal U, (I.comap f).ideal V = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Hom.appLE f (↑U) (↑V) e)) a} ∧ (CategoryTheory.ConcreteCategory.hom (Hom.appLE f (↑U) (↑V) e)) a ∈ nonZeroDivisors ↑(Y.presheaf.obj (Opposite.op ↑V))

For f : Y ⟶ X admissible for I (the inverse image ideal sheaf invertible), an affine open U ⊆ X and y ∈ f⁻¹(U), there are an affine open V ∋ y with f(V) ⊆ U and a ∈ I(U) such that (I.comap f)(V) = (f♯a) with f♯a a nonzerodivisor of Γ(Y, V). This is the argument of [Hau14, Theorem 4.18, proof (c)] (compare the proof of [TSPA, Tag 0806]) carried from the local ring at y to an affine neighbourhood: a generator h₀ of the inverse image ideal near y is a combination ∑ cᵢ f♯(xᵢ) with xᵢ ∈ I(U), each f♯(xᵢ) is tᵢ h₀, so ∑ cᵢ tᵢ = 1 by cancellation and some tᵢ is not in the prime of y; on the basic open D(tᵢ) the element f♯(xᵢ) = tᵢ h₀ is a unit multiple of h₀.