Extending sections of M~ across a closed subset of depth at least two

Let M be a module over a commutative ring R and U an open subset of Spec R. If a, b is a weakly M-regular sequence whose basic opens D(a) and D(b) lie in U, then every section of M~ over U comes from a unique element of M: the map M → M~(U) is bijective. This is the algebraic Hartogs principle for M~ on the affine scheme Spec R.

For a finite module M over a Noetherian ring, the hypothesis is implied by a condition at the points outside U: if depth M_p ≥ 2 for every prime p ∉ U, the vanishing ideal of the complement of U contains a weakly M-regular sequence of length two (TauCeti.exists_isWeaklyRegular_of_le_depth_localizedModule). So sections of M~ extend uniquely across a closed subset all of whose points have depth at least two (Stacks, Lemma 31.5.11 (0E9I), for the affine scheme Spec R and the quasi-coherent sheaf M~). For instance, for M = R = k[x, y] it gives Γ(𝔸² ∖ {0}, 𝒪) = k[x, y], since k[x, y]_{(x, y)} has depth two.

The proof is elementary. A section s over U restricts to fractions x / aⁿ on D(a) and y / bᵐ on D(b). Their agreement on D(ab) gives bʲ x ∈ aⁿ M for some j, so x = aⁿ c because b is regular modulo a. Then s and c agree on D(a), and since a is M-regular, a section over U is determined by its restriction to U ∩ D(a).

Main results

• TauCeti.AlgebraicGeometry.StructureSheaf.res_injective_of_isSMulRegular: for an M-regular element a, a section of M~ over U is determined by its restriction to any open V ⊆ U containing U ∩ D(a).
• TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_injective_of_isSMulRegular: M → M~(U) is injective when D(a) ⊆ U for an M-regular a.
• TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_isWeaklyRegular: M → M~(U) is bijective when D(a), D(b) ⊆ U for a weakly M-regular sequence a, b.
• TauCeti.AlgebraicGeometry.StructureSheaf.exists_isWeaklyRegular_basicOpen_le_of_two_le_depth: for a finite module over a Noetherian ring with depth M_p ≥ 2 at every prime p ∉ U, there is a weakly M-regular sequence a, b with D(a), D(b) ⊆ U.
• TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_two_le_depth: for a finite module over a Noetherian ring, M → M~(U) is bijective when depth M_p ≥ 2 at every prime p ∉ U.
• TauCeti.AlgebraicGeometry.tilde_toOpen_bijective_of_two_le_depth: the same statement for the sheaf of modules M~ on the scheme Spec R.
• TauCeti.AlgebraicGeometry.Spec.presheaf_map_leTop_bijective_iff: restriction of sections of Spec R to U is bijective exactly when R → 𝒪(U) is, so the statements above for M = R describe sections of the scheme Spec R.
• TauCeti.AlgebraicGeometry.isIso_appTop_pullback_fst_ι_of_isWeaklyRegular: for a flat R-algebra C and D(a), D(b) ⊆ U with a, b weakly regular on R, global sections of Spec C do not change under restriction to the preimage of U.

References

• Stacks Project, Lemma 31.5.11.

theorem TauCeti.AlgebraicGeometry.StructureSheaf.res_injective_of_isSMulRegular {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} (hVU : V ≤ U) {a : R} (ha : IsSMulRegular M a) (haV : U ⊓ PrimeSpectrum.basicOpen a ≤ V) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.structureSheafInType R M).obj.map (CategoryTheory.homOfLE hVU).op))

Let a be M-regular and V ⊆ U opens of Spec R with U ∩ D(a) ⊆ V. A section of M~ over U is determined by its restriction to V.

theorem TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_injective_of_isSMulRegular {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} {a : R} (ha : IsSMulRegular M a) (haU : PrimeSpectrum.basicOpen a ≤ U) : Function.Injective ⇑(AlgebraicGeometry.StructureSheaf.toOpenₗ R M U)

Let a be M-regular. If D(a) ⊆ U, then M → M~(U) is injective.

theorem TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_isWeaklyRegular {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} {a b : R} (h : RingTheory.Sequence.IsWeaklyRegular M [a, b]) (haU : PrimeSpectrum.basicOpen a ≤ U) (hbU : PrimeSpectrum.basicOpen b ≤ U) : Function.Bijective ⇑(AlgebraicGeometry.StructureSheaf.toOpenₗ R M U)

Algebraic Hartogs principle. Let a, b be a weakly M-regular sequence. If D(a) and D(b) lie in the open subset U of Spec R, then M → M~(U) is bijective: every section of M~ over U comes from a unique element of M.

theorem TauCeti.AlgebraicGeometry.StructureSheaf.exists_isWeaklyRegular_basicOpen_le_of_two_le_depth {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (h : ∀ p ∉ U, 2 ≤ IsLocalRing.depth ↧(LocalizedModule p.asIdeal.primeCompl M)) : ∃ (a : R) (b : R), RingTheory.Sequence.IsWeaklyRegular M [a, b] ∧ PrimeSpectrum.basicOpen a ≤ U ∧ PrimeSpectrum.basicOpen b ≤ U

Let M be a finite module over a Noetherian ring R and U an open subset of Spec R such that depth M_p ≥ 2 for every prime p ∉ U. Then there is a weakly M-regular sequence a, b with D(a), D(b) ⊆ U, taken from the vanishing ideal of the complement of U.

theorem TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_two_le_depth {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (h : ∀ p ∉ U, 2 ≤ IsLocalRing.depth ↧(LocalizedModule p.asIdeal.primeCompl M)) : Function.Bijective ⇑(AlgebraicGeometry.StructureSheaf.toOpenₗ R M U)

Hartogs principle for the structure sheaf of a module. Let M be a finite module over a Noetherian ring R and U an open subset of Spec R such that depth M_p ≥ 2 for every prime p ∉ U. Then every section of M~ over U comes from a unique element of M.

theorem TauCeti.AlgebraicGeometry.Spec.presheaf_map_leTop_bijective_iff {R : Type u} [CommRing R] (U : (AlgebraicGeometry.Spec ↧R).Opens) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Spec ↧R).presheaf.map (TopologicalSpace.Opens.leTop U).op)) ↔ Function.Bijective ⇑(AlgebraicGeometry.StructureSheaf.toOpenₗ R R U)

Restriction of sections of Spec R from Spec R to an open U is bijective exactly when the map R → 𝒪(U) is.

theorem TauCeti.AlgebraicGeometry.tilde_toOpen_bijective_of_two_le_depth {R : CommRingCat} [IsNoetherianRing ↑R] (M : ModuleCat ↑R) [Module.Finite ↑R ↑M] (U : (AlgebraicGeometry.Spec R).Opens) (h : ∀ p ∉ U, 2 ≤ IsLocalRing.depth ↧(LocalizedModule p.asIdeal.primeCompl ↑M)) : Function.Bijective ⇑(ModuleCat.Hom.hom (AlgebraicGeometry.tilde.toOpen M U))

Hartogs principle for M~ on Spec R. Let M be a finite module over a Noetherian ring R and U an open subset of Spec R such that depth M_p ≥ 2 for every prime p ∉ U. Then M → M~(U) is bijective: every section of M~ over U comes from a unique element of M. Stacks, Lemma 31.5.11 (0E9I), for the affine scheme Spec R and M~, with M_p the stalk of M~ at p.

theorem TauCeti.AlgebraicGeometry.isIso_appTop_pullback_fst_ι_of_isWeaklyRegular {R : CommRingCat} (C : Type u) [CommRing C] [Algebra (↑R) C] [Module.Flat (↑R) C] (W : (AlgebraicGeometry.Spec R).Opens) {a b : ↑R} (hab : RingTheory.Sequence.IsWeaklyRegular ↑R [a, b]) (ha : PrimeSpectrum.basicOpen a ≤ W) (hb : PrimeSpectrum.basicOpen b ≤ W) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) C))) W.ι))

Let C be a flat R-algebra and W an open subset of Spec R containing D(a) and D(b) for a weakly regular sequence a, b on R. Then restriction of global sections Γ(Spec C, 𝒪) → Γ(Spec C ×_{Spec R} W, 𝒪) is an isomorphism.