Consequences of local Noetherianity on an analytic K-space

Three consequences of the local stationarity of increasing sequences of ideal sheaves of finite type on an analytic K-space X — the property "X is locally Noetherian" of [BM97, (3.8)], which Bierstone and Milman take as a standing property of their categories of spaces. Each theorem takes that local stationarity as an explicit hypothesis hloc; Hironaka/AnalyticSpace/ModelTransport.lean derives hloc from the Noether lemma on the models (G, 𝒜_G), itself taken as a hypothesis.

• stabilizes_of_isCompact_closure_of_locallyStationary ([BM97, 3.9]: "if X (respectively, |X|) is locally Noetherian and |X| is quasi-compact, then X (respectively, |X|) is Noetherian"): a finite subcover of the compact closure of U by the neighbourhoods of local stationarity and the maximum of their indices;
• isNoetherian_of_compactSpace_of_locallyStationary (one direction of "X is Noetherian iff |X| is compact", [BM97, 3.9]): the case U = univ, with IdealSheaf.ext turning stalkwise equality into equality of closed subspaces;
• hasLocalGenerators_iSup_colon_pow_of_locallyStationary (the saturation, [BM97, Proposition 3.13] and the sentence after it): the colon ideal sheaves (J : I^k) (hasLocalGenerators_colon_idealSheaf) form an increasing sequence, stationary near every point, so the stalkwise union is (J : I^N)_x near x — an ideal sheaf of finite type.

theorem AnalyticSpace.stabilizes_of_isCompact_closure_of_locallyStationary {K : Type} [RCLike K] (X : AnalyticSpace K) (W : ℕ → X.ClosedSubspace) (hloc : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ V) (N : ℕ), ∀ m ≥ N, ∀ y ∈ V, Manifold.IdealSheaf.stalkIdeal (W m) y = Manifold.IdealSheaf.stalkIdeal (W N) y) (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

Given local stationarity, on a set with compact closure the sequence stabilizes uniformly [BM97, 3.9].

theorem AnalyticSpace.isNoetherian_of_compactSpace_of_locallyStationary {K : Type} [RCLike K] (X : AnalyticSpace K) [CompactSpace ↑↑X.toPresheafedSpace] (hloc : ∀ (C : ℕ → Manifold.IdealSheaf X.𝒪), (∀ (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) : X.IsNoetherian

A compact analytic K-space on which every increasing sequence of ideal sheaves of finite type is locally stationary is Noetherian: one direction of [BM97, 3.9].

theorem AnalyticSpace.hasLocalGenerators_iSup_colon_pow_of_locallyStationary {K : Type} [RCLike K] (X : AnalyticSpace K) (J I : Manifold.IdealSheaf X.𝒪) (hloc : ∀ (C : ℕ → Manifold.IdealSheaf X.𝒪), (∀ (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) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => ⨆ (k : ℕ), Submodule.colon (J.stalkIdeal x) ↑(I.stalkIdeal x ^ k)

The saturation ⨆_k (J_x : I_x^k) ([BM97, Proposition 3.13] and the sentence after it) has local generators, given local stationarity of increasing sequences of ideal sheaves.