Descent of closed subschemes along flat morphisms

A blow-up sequence pulled back along a surjective smooth morphism determines the original sequence [Kol07, Definition 30, 30.1], and in the proof that maximal contact hypersurfaces give the same blow-up sequence, the centres over a common étale cover are compared through their inverse images [Kol07, Theorem 97, proof]. The two descent lemmas behind these sentences are stated here for ideal sheaves and proved stalkwise, without scheme-theoretic images:

• (a) for f : U ⟶ X flat and closed subschemes Z, Z' ⊆ X whose supports lie in the image of f, f⁻¹Z = f⁻¹Z' implies Z = Z' (IdealSheafData.eq_of_comap_eq_of_flat);
• (b) for f, g : U ⟶ X flat, Z, Z' ⊆ X closed with |Z| ⊆ f(U), |Z'| ⊆ g(U), f⁻¹Z = g⁻¹Z' =: C and f ∘ ι_C = g ∘ ι_C, one has Z = Z' (IdealSheafData.eq_of_comap_eq_of_agreeOn).

The argument

Stalks decide. An ideal sheaf is determined by its stalk ideals J_x ⊆ 𝒪_{X,x} (the ideal generated by the germs of J, IdealSheafData.stalkIdeal): on an affine open U, the stalk at the point of a maximal ideal 𝔪 of Γ(U) is the localization Γ(U)_𝔪, and an ideal of Γ(U) is determined by its localizations at the maximal ideals (Mathlib's Ideal.le_of_localization_maximal). This is IdealSheafData.le_of_stalkIdeal_le and ext_stalkIdeal, extensionality by stalks. Off the support the stalk ideal is the unit ideal (stalkIdeal_eq_top_of_notMem_support: some section of J is a unit at x).

Contraction. For flat f the stalk map 𝒪_{X, f u} → 𝒪_{U, u} is a flat local homomorphism of local rings, hence faithfully flat (Mathlib's Module.FaithfullyFlat.of_flat_of_isLocalHom), so every ideal K of the source is recovered from its extension: comap (map K) = K (Ideal.comap_map_eq_self_of_faithfullyFlat; comap_stalkMap_map_eq_self). The stalk of Z.comap f at u is the extension of the stalk of Z at f u (stalkIdeal_comap).

(a). At x = f u: Z_x = comap (map Z_x) = comap ((Z.comap f)_u) = comap ((Z'.comap f)_u) = Z'_x; at x ∉ f(U), x lies in neither support and both stalk ideals are the unit ideal.

(b). g ∘ ι_C factors through Z' — Z'.comap (ι_C ≫ g) = C.comap ι_C = ⊥ — hence so does f ∘ ι_C, i.e. (Z'.comap f).comap ι_C = ⊥, which says Z'.comap f ≤ C = Z.comap f (Mathlib's Galois connection le_map_iff_comap_le with ι_C.ker = C). Contract stalkwise along f at the points of |Z| (le_of_comap_le_of_flat): Z'_x ≤ comap (map Z'_x) ≤ comap (map Z_x) = Z_x; off |Z| the right side is the unit ideal. So Z' ≤ Z, and by symmetry (contract along g at the points of |Z'|) Z ≤ Z'.

Nothing here assumes X, U Noetherian, f quasi-compact or surjective onto more than the supports; in the application to maximal contact, f is étale with open image and the supports of the centres lie in it.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_eq_top_of_notMem_support {X : Scheme} (J : X.IdealSheafData) {x : ↥X} (hx : x ∉ J.support) : J.stalkIdeal x = ⊤

Off the support the stalk ideal is the unit ideal: some section of J over an affine neighbourhood is a unit at x (Mathlib's mem_zeroLocus_iff, mem_basicOpen).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_mono {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (x : ↥X) : I.stalkIdeal x ≤ J.stalkIdeal x

Monotonicity of the stalk ideal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_stalkIdeal_le {X : Scheme} {I J : X.IdealSheafData} (h : ∀ (x : ↥X), I.stalkIdeal x ≤ J.stalkIdeal x) : I ≤ J

An ideal sheaf is bounded by another as soon as its stalk ideals are: on an affine open V the stalk at the point of a maximal ideal 𝔪 of Γ(V) is the localization at 𝔪, and an ideal is determined by its localizations at the maximal ideals (Ideal.le_of_localization_maximal).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_stalkIdeal {X : Scheme} {I J : X.IdealSheafData} (h : ∀ (x : ↥X), I.stalkIdeal x = J.stalkIdeal x) : I = J

Extensionality by stalks: ideal sheaves with equal stalk ideals at every point are equal.

theorem AlgebraicGeometry.Scheme.Hom.comap_stalkMap_map_eq_self {X U : Scheme} (f : U ⟶ X) [Flat f] (u : ↥U) (K : Ideal ↑(X.presheaf.stalk (f u))) : Ideal.comap (CommRingCat.Hom.hom (stalkMap f u)) (Ideal.map (CommRingCat.Hom.hom (stalkMap f u)) K) = K

For flat f the stalk map 𝒪_{X, f u} → 𝒪_{U, u} is a flat local homomorphism of local rings, hence faithfully flat (Module.FaithfullyFlat.of_flat_of_isLocalHom), so the contraction of the extension of an ideal K of 𝒪_{X, f u} is K (Ideal.comap_map_eq_self_of_faithfullyFlat; [TSPA, Tag 00HQ] at the local rings).

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_comap_le_of_flat {X U : Scheme} (f : U ⟶ X) [Flat f] (Z Z' : X.IdealSheafData) (hZ : ↑Z.support ⊆ Set.range ⇑f) (h : Z'.comap f ≤ Z.comap f) : Z' ≤ Z

The stalkwise half of the descent lemma: for f flat and |Z| ⊆ f(U), an inequality Z'.comap f ≤ Z.comap f of inverse images descends to Z' ≤ Z — contract along the faithfully flat stalk maps at the points of |Z|; off |Z| the stalk of Z is the unit ideal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_of_comap_eq_of_flat {X U : Scheme} (f : U ⟶ X) [Flat f] (Z Z' : X.IdealSheafData) (hZ : ↑Z.support ⊆ Set.range ⇑f) (hZ' : ↑Z'.support ⊆ Set.range ⇑f) (h : Z.comap f = Z'.comap f) : Z = Z'

A closed subscheme with support in the image of a flat map is determined by its inverse image (the pull-back along a surjective smooth morphism determines the blow-up sequence, [Kol07, Definition 30, 30.1]; [TSPA, Tag 00HQ]). For f : U ⟶ X flat and Z, Z' with |Z| ∪ |Z'| ⊆ f(U), f⁻¹Z = f⁻¹Z' implies Z = Z'.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_subschemeι_comp_eq_bot {X Y : Scheme} (W : X.IdealSheafData) (g : Y ⟶ X) : W.comap (CategoryTheory.CategoryStruct.comp (W.comap g).subschemeι g) = ⊥

A morphism ι_C ≫ g out of the closed subscheme C = W.comap g factors through W: W.comap (ι_C ≫ g) = ⊥.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_of_comap_eq_of_agreeOn {X U : Scheme} (f : U ⟶ X) [Flat f] (g : U ⟶ X) [Flat g] (Z Z' : X.IdealSheafData) (hZ : ↑Z.support ⊆ Set.range ⇑f) (hZ' : ↑Z'.support ⊆ Set.range ⇑g) (h : Z.comap f = Z'.comap g) (hfg : CategoryTheory.CategoryStruct.comp (Z.comap f).subschemeι f = CategoryTheory.CategoryStruct.comp (Z.comap f).subschemeι g) : Z = Z'

Two flat maps agreeing on the common preimage give equal centres (the comparison of centres over a common étale cover in the proof of [Kol07, Theorem 97]). For f, g : U ⟶ X flat, Z, Z' with |Z| ⊆ f(U), |Z'| ⊆ g(U), f⁻¹Z = g⁻¹Z' =: C and f ∘ ι_C = g ∘ ι_C, one has Z = Z'; scheme-theoretic images are not needed.