Transport from the local models: the Noether lemma and Cartan's radical theorem

Two statements about ideal sheaves are available on the models (G, 𝒜_G), G ⊆ Kⁿ open: the Noether lemma (every increasing sequence of ideal sheaves of finite type is locally stationary) and Cartan's theorem on radicals (the radical of an ideal sheaf of finite type is of finite type). This file carries them to an arbitrary analytic K-space X. Near x ∈ X Hironaka's clause (i) gives a K-isomorphism e : X|U ≅ localModel K n G f (exists_kIso_localModel); an ideal sheaf on X restricts to X|U (restrictIdeal, the pull-back along the open immersion), is pulled back along e⁻¹ to the local model (QuotientSpace.comap), and is lifted to (G, 𝒜_G) (QuotientSpace.liftIdeal: the preimage of the stalk ideal under the surjective stalk map of the quotient at the points of the support, the unit ideal elsewhere). All three steps are monotone (comap_mono, liftIdeal_mono), and each is injective on stalk ideals — Ideal.comap along a surjection and Ideal.map along a bijection — so a stalkwise equality on G descends to X. The points of the neighbourhood in X are parametrized from the model side, y = incl (e⁻¹ z), so that no round trip e⁻¹ (e y') = y' is needed.

Each theorem takes the model statement as an explicit argument (hK1 for the Noether lemma, hK2 for Cartan's theorem), so that the transport is separate from the analysis.

• locallyStationary_of_noether: the Noether lemma on the models gives local stationarity of every increasing sequence of ideal sheaves of finite type on X;
• stabilizes_of_isCompact_closure_of_noether, isNoetherian_of_compactSpace_of_noether, hasLocalGenerators_iSup_colon_pow_of_noether: the derivations of Hironaka/AnalyticSpace/NoetherDerived.lean with that hypothesis discharged from hK1;
• hasLocalGenerators_radical_of_cartan: the radical of an ideal sheaf of finite type on X has local generators, from hK2.

theorem AnalyticSpace.ideal_map_injective_of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Bijective ⇑f) : Function.Injective (Ideal.map f)

Ideal.map along a bijective ring homomorphism is injective.

theorem AnalyticSpace.QuotientSpace.comap_mono {X' X : AlgebraicGeometry.LocallyRingedSpace} (φ : X' ⟶ X) {J J' : Manifold.IdealSheaf X.𝒪} (h : J ≤ J') : comap φ J ≤ comap φ J'

The pull-back of ideal sheaves along a morphism is monotone.

theorem AnalyticSpace.QuotientSpace.liftIdeal_mono (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) {J' J'' : Manifold.IdealSheaf (quotientSpace X J).𝒪} (h : J' ≤ J'') : liftIdeal X J J' ≤ liftIdeal X J J''

The lift of ideal sheaves from the quotient is monotone.

theorem AnalyticSpace.locallyStationary_of_noether {K : Type} [RCLike K] (X : AnalyticSpace K) (hK1 : ∀ (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (J : ℕ → Manifold.IdealSheaf (analyticSpaceOfOpen K n G).𝒪), (∀ (m : ℕ), J m ≤ J (m + 1)) → ∀ (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), ∃ (U : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (_ : x ∈ U) (N : ℕ), ∀ m ≥ N, ∀ y ∈ U, (J m).stalkIdeal y = (J N).stalkIdeal y) (C : ℕ → Manifold.IdealSheaf X.𝒪) (hC : ∀ (m : ℕ), C m ≤ C (m + 1)) (x : ↑↑X.toPresheafedSpace) : ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ V) (N : ℕ), ∀ m ≥ N, ∀ y ∈ V, (C m).stalkIdeal y = (C N).stalkIdeal y

Local stationarity on an analytic K-space of an increasing sequence of ideal sheaves of finite type, from the Noether lemma on the models (the hypothesis hK1).

theorem AnalyticSpace.stabilizes_of_isCompact_closure_of_noether {K : Type} [RCLike K] (X : AnalyticSpace K) (hK1 : ∀ (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (J : ℕ → Manifold.IdealSheaf (analyticSpaceOfOpen K n G).𝒪), (∀ (m : ℕ), J m ≤ J (m + 1)) → ∀ (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), ∃ (U : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (_ : x ∈ U) (N : ℕ), ∀ m ≥ N, ∀ y ∈ U, (J m).stalkIdeal y = (J N).stalkIdeal y) (W : ℕ → X.ClosedSubspace) (hW : ∀ (m : ℕ), (W (m + 1)).le (W m)) (U : Set ↑↑X.toPresheafedSpace) (hU : IsCompact (closure U)) : ∃ (N : ℕ), ∀ m ≥ N, ∀ x ∈ U, Manifold.IdealSheaf.stalkIdeal (W m) x = Manifold.IdealSheaf.stalkIdeal (W N) x

On a set with compact closure every decreasing sequence of closed subspaces stabilizes, from the Noether lemma on the models ([BM97, 3.9]).

theorem AnalyticSpace.isNoetherian_of_compactSpace_of_noether {K : Type} [RCLike K] (X : AnalyticSpace K) [CompactSpace ↑↑X.toPresheafedSpace] (hK1 : ∀ (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (J : ℕ → Manifold.IdealSheaf (analyticSpaceOfOpen K n G).𝒪), (∀ (m : ℕ), J m ≤ J (m + 1)) → ∀ (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), ∃ (U : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (_ : x ∈ U) (N : ℕ), ∀ m ≥ N, ∀ y ∈ U, (J m).stalkIdeal y = (J N).stalkIdeal y) : X.IsNoetherian

A compact analytic K-space is Noetherian, from the Noether lemma on the models ([BM97, 3.9]).

theorem AnalyticSpace.hasLocalGenerators_iSup_colon_pow_of_noether {K : Type} [RCLike K] (X : AnalyticSpace K) (hK1 : ∀ (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (J : ℕ → Manifold.IdealSheaf (analyticSpaceOfOpen K n G).𝒪), (∀ (m : ℕ), J m ≤ J (m + 1)) → ∀ (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), ∃ (U : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (_ : x ∈ U) (N : ℕ), ∀ m ≥ N, ∀ y ∈ U, (J m).stalkIdeal y = (J N).stalkIdeal y) (J I : Manifold.IdealSheaf X.𝒪) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => ⨆ (k : ℕ), Submodule.colon (J.stalkIdeal x) ↑(I.stalkIdeal x ^ k)

The saturation ⨆_k (J : I^k) has local generators, from the Noether lemma on the models.

theorem AnalyticSpace.hasLocalGenerators_radical_of_cartan {K : Type} [RCLike K] (X : AnalyticSpace K) (hK2 : ∀ (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (J : Manifold.IdealSheaf (analyticSpaceOfOpen K n G).𝒪), Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑(analyticSpaceOfOpen K n G).toTopCat) => (J.stalkIdeal x).radical) (J : Manifold.IdealSheaf X.𝒪) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => (J.stalkIdeal x).radical

The radical of an ideal sheaf of finite type on an analytic K-space has local generators, from Cartan's theorem on the models (the hypothesis hK2): the radical of the lifted ideal is the preimage of the radical, so the local generators on the model map to local generators of the radical on X.