Coherence of the structure sheaf of an analytic K-space

The structure sheaf of an analytic space is coherent ([BM97, (3.8)(3)]; [Fre17, Ch. V, 7.3]): Oka's theorem on the model (Kⁿ, 𝒜_{Kⁿ}) (oka_coherent, Hironaka/AnalyticSpace/Oka/) passes to the open subspace (G, 𝒜_G) (isCoherent_restrict), to the local model (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) (isCoherent_quotientSpace), to its open subspaces, and along the K-isomorphisms of Hironaka's clause (i) to an open cover of any analytic K-space (isCoherent_of_kIso, isCoherent_of_forall_restrictOpen): isCoherent_analyticSpace. Serre's form for every ideal sheaf (isCoherent_idealSheaf) is the q = 1 slice through isCoherent_iff_forall_isCoherent_idealSheaf.

The intersection of two ideal sheaves of finite type is of finite type ([Fre17, Ch. I, 10.7]): the relations of the one-row matrix (e₁, …, e_k, f₁, …, f_l) of local generators of E and F are locally generated (coherence), and E_x ∩ F_x is the image of the relation module under (a, b) ↦ Σ a_i e_i — so the sections Σ_i R_{n,i} e_i for the generators R_n of the relations generate E_x ∩ F_x at every point near x (hasLocalGenerators_inf). The bridge between IdealSheaf.HasLocalGenerators (one generator per section, on the whole space) and HasLocalGeneratorsOn with p = 1 is hasLocalGenerators_iff_hasLocalGeneratorsOn_top. The radical and the saturation of an ideal sheaf are treated in Hironaka/AnalyticSpace/CoherentColon.lean, Hironaka/AnalyticSpace/NoetherDerived.lean and Hironaka/AnalyticSpace/ModelTransport.lean.

def Manifold.idealRow {R : Type u_1} [CommRing R] (I : Ideal R) : Submodule R (Fin 1 → R)

An ideal of R, read as a submodule of Fin 1 → R.

Equations

• Manifold.idealRow I = Submodule.comap (↑(LinearEquiv.funUnique (Fin 1) R R)) I

theorem Manifold.mem_idealRow_iff {R : Type u_1} [CommRing R] (I : Ideal R) (a : Fin 1 → R) : a ∈ idealRow I ↔ a 0 ∈ I

theorem Manifold.hasLocalGenerators_iff_hasLocalGeneratorsOn_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (I : (x : ↑X) → Ideal ↑(𝒪.presheaf.stalk x)) : IdealSheaf.HasLocalGenerators I ↔ HasLocalGeneratorsOn 𝒪 ⊤ 1 fun (x : ↑X) (x_1 : x ∈ ⊤) => idealRow (I x)

Local generation of a family of stalk ideals (IdealSheaf.HasLocalGenerators) is the p = 1 case of HasLocalGeneratorsOn over ⊤.

theorem Manifold.sum_elim_finSumFinEquiv_mul {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {k₁ k₂ : ℕ} (u : Fin k₁ → A) (v : Fin k₂ → A) (a : Fin (k₁ + k₂) → B) : ∑ x : Fin (k₁ + k₂), φ (Sum.elim u v (finSumFinEquiv.symm x)) * a x = ∑ i : Fin k₁, φ (u i) * a (finSumFinEquiv (Sum.inl i)) + ∑ j : Fin k₂, φ (v j) * a (finSumFinEquiv (Sum.inr j))

A sum over the concatenated row (u | v), split.

theorem AnalyticSpace.isCoherent_analyticSpaceOfOpen {K : Type} [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) : Manifold.IsCoherent (analyticSpaceOfOpen K n G).𝒪

Oka's theorem on the open subspace (G, 𝒜_G) of (Kⁿ, 𝒜_{Kⁿ}).

theorem AnalyticSpace.isCoherent_localModel {K : Type} [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : Manifold.IsCoherent (localModel K n G f).𝒪

The structure sheaf of a local model (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) is coherent ([Fre17, Ch. V, 7.3]; [BM97, (3.8)(3)]).

theorem AnalyticSpace.isCoherent_analyticSpace {K : Type} [RCLike K] (X : AnalyticSpace K) : Manifold.IsCoherent X.𝒪

The structure sheaf of an analytic K-space is coherent [BM97, (3.8)(3)].

theorem AnalyticSpace.isCoherent_idealSheaf {K : Type} [RCLike K] (X : AnalyticSpace K) (J : Manifold.IdealSheaf X.𝒪) : J.IsCoherent

Serre's form [BM97, (3.8)(3)]: every ideal sheaf on an analytic K-space is coherent.

theorem AnalyticSpace.hasLocalGenerators_inf {K : Type} [RCLike K] (X : AnalyticSpace K) (E F : Manifold.IdealSheaf X.𝒪) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => E.stalkIdeal x ⊓ F.stalkIdeal x

The intersection of two ideal sheaves of finite type on an analytic K-space is locally finitely generated [Fre17, Ch. I, 10.7].