Finite-type propagation of stalk equalities

If the stalk 𝒥_x of an ideal sheaf 𝒥 with local generators g₁, …, g_k near x is generated by the germs of sections h₁, …, h_c, then 𝒥_y is generated by their germs for every y in a neighbourhood of x — "𝒥 = (h₁, …, h_c) on a neighbourhood". The two ingredients are elementary facts about germs of a presheaf of commutative rings: membership of a germ in a stalk ideal spreads to a neighbourhood (mem_stalkIdeal_iff hands over a section of 𝒥 with the same germ, germ_eq a neighbourhood where the sections agree), and membership of a germ in the ideal generated by finitely many germs spreads likewise (each coefficient is a germ of a section, germ_eq again). Hironaka's passage from the local ring to a neighbourhood in the Jacobian-criterion sentence [Hir64, Ch. 0, §1, p. 121] — from 𝓘_x = (h)_x to X = V(h) near x — uses this. Not in the sources as a stated result; routine.

• exists_forall_germ_mem_stalkIdeal: a germ in 𝒥_x is in 𝒥_y for y near x;
• exists_forall_germ_mem_span: a germ in (germ_x h) is in (germ_y h) for y near x;
• exists_stalkIdeal_eq_span_of_stalkIdeal_eq_span: the propagation.

theorem AnalyticSpace.mem_iInf_opens {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} [Finite ι] {V : ι → TopologicalSpace.Opens α} {x : α} : x ∈ ⨅ (i : ι), V i ↔ ∀ (i : ι), x ∈ V i

Membership in a finite infimum of opens.

theorem AnalyticSpace.exists_forall_germ_mem_span {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} {x : ↑X} (hx : x ∈ U) (s : ↑(F.obj (Opposite.op U))) {c : ℕ} (h : Fin c → ↑(F.obj (Opposite.op U))) (hs : (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s ∈ Ideal.span (Set.range fun (i : Fin c) => (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) (h i))) : ∃ (W : TopologicalSpace.Opens ↑X) (_ : x ∈ W) (hWU : W ≤ U), ∀ (y : ↑X) (hy : y ∈ W), (CategoryTheory.ConcreteCategory.hom (F.germ U y ⋯)) s ∈ Ideal.span (Set.range fun (i : Fin c) => (CategoryTheory.ConcreteCategory.hom (F.germ U y ⋯)) (h i))

Membership of a germ in the ideal generated by finitely many germs spreads to a neighbourhood: if germ_x s ∈ (germ_x h₁, …, germ_x h_c), then germ_y s ∈ (germ_y h₁, …, germ_y h_c) for all y in some open W ≤ U containing x.

theorem AnalyticSpace.exists_forall_germ_mem_stalkIdeal {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) (J : Manifold.IdealSheaf 𝒪) {U : TopologicalSpace.Opens ↑X} {x : ↑X} (hx : x ∈ U) (s : ↑(𝒪.presheaf.obj (Opposite.op U))) (hs : (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U x hx)) s ∈ J.stalkIdeal x) : ∃ (W : TopologicalSpace.Opens ↑X) (_ : x ∈ W) (hWU : W ≤ U), ∀ (y : ↑X) (hy : y ∈ W), (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U y ⋯)) s ∈ J.stalkIdeal y

Membership of a germ in a stalk ideal spreads to a neighbourhood: if germ_x s ∈ 𝒥_x, then germ_y s ∈ 𝒥_y for all y in some open W ≤ U containing x (mem_stalkIdeal_iff: 𝒥_x consists of the germs of sections of 𝒥).

theorem AnalyticSpace.exists_stalkIdeal_eq_span_of_stalkIdeal_eq_span {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) (J : Manifold.IdealSheaf 𝒪) {U : TopologicalSpace.Opens ↑X} {x : ↑X} (hx : x ∈ U) {k : ℕ} (g : Fin k → ↑(𝒪.presheaf.obj (Opposite.op U))) (hg : ∀ (y : ↑X) (hy : y ∈ U), J.stalkIdeal y = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U y hy)) (g i))) {c : ℕ} (h : Fin c → ↑(𝒪.presheaf.obj (Opposite.op U))) (hJ : J.stalkIdeal x = Ideal.span (Set.range fun (i : Fin c) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U x hx)) (h i))) : ∃ (V : TopologicalSpace.Opens ↑X) (_ : x ∈ V) (i : V ⟶ U), ∀ (y : ↑X) (hy : y ∈ V), J.stalkIdeal y = Ideal.span (Set.range fun (j : Fin c) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V y hy)) ((CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map i.op)) (h j)))

The finite-type propagation: if an ideal sheaf 𝒥 has local generators g₁, …, g_k near x (its stalks at the points of U ∋ x are generated by their germs) and the stalk 𝒥_x is generated by the germs of sections h₁, …, h_c over U, then 𝒥_y is generated by their germs for every y in a neighbourhood V ⊆ U of x.