Colon of an ideal sheaf by a locally principal ideal sheaf

The nonmonomial part N(I) = I : M(I) of an ideal sheaf I (Kollár's Definition–Lemma 110 in the form used by this library, BMO/NonmonomialPart.lean) is the colon of I by its monomial part M(I), and M(I) is locally principal, generated near every point by a section whose germs are non-zero-divisors. This file provides the sheaf-theoretic tool that makes such a colon an ideal sheaf: when J is locally generated by a non-zero-divisor section s and I ⊆ J stalkwise, the quotients of finitely many local generators of I by s generate the stalks of the colon I : J near the point, so the colon has local generators. No coordinates enter; the statements are about an arbitrary sheaf of commutative rings on a topological space.

The two ring-theoretic lemmas at the top are elementary facts about colon ideals in a commutative ring; the sheaf-level statements follow. Not in the sources; auxiliary for the fine split I = M(I) · N(I) of [Kol07, Definition–Lemma 110].

theorem Ideal.colon_span_singleton_eq_colon_singleton {R : Type u_1} [CommRing R] (K : Ideal R) (s : R) : Submodule.colon K ↑(span {s}) = Submodule.colon K {s}

The colon of K by the principal ideal span {s}, taken as a set, equals the colon by the singleton {s}: testing multiplication by every multiple of s is testing multiplication by s. An elementary fact about colon ideals, not in the sources.

theorem Ideal.colon_span_range_mul_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {s : R} (hs : s ∈ nonZeroDivisors R) {ι : Type u_2} [Finite ι] (g : ι → R) : Submodule.colon (span (Set.range fun (j : ι) => s * g j)) {s} = span (Set.range g)

Dividing the generators of span (range fun j => s * g j) by the non-zero-divisor s (as the colon by {s}) recovers span (range g). The non-zero-divisor form of Ideal.colon_span_range_pow_mul, used with a single factor s for the local generators of the colon. Not in the sources.

theorem Hironaka.Manifold.exists_nhds_forall_germ_mul_eq {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} {U V W : TopologicalSpace.Opens X} {x : X} (hxU : x ∈ U) (hxV : x ∈ V) (hxW : x ∈ W) (s : ↑(𝒪.presheaf.obj (Opposite.op U))) (t : ↑(𝒪.presheaf.obj (Opposite.op V))) (r : ↑(𝒪.presheaf.obj (Opposite.op W))) (heq : (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V x hxV)) t = (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U x hxU)) s * (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ W x hxW)) r) : ∃ (O : TopologicalSpace.Opens X) (_ : x ∈ O) (hOU : O ≤ U) (hOV : O ≤ V) (hOW : O ≤ W), ∀ (y : X) (hy : y ∈ O), (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V y ⋯)) t = (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U y ⋯)) s * (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ W y ⋯)) r

A relation germ t = germ s · germ r between germs at x extends to a neighbourhood: the sections satisfy the same relation, germ by germ, at every point of some open neighbourhood of x. This is the germ-shrinking step behind the local generators of a colon.

def Manifold.IdealSheaf.HasLocalRegularGenerator {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} (J : IdealSheaf 𝒪) : Prop

An ideal sheaf is locally regularly principal when, near every point, it is generated by a single section whose germs are non-zero-divisors — the section-level form of stalkwise principality by a non-zero-divisor. The colon of an ideal sheaf I by such a sheaf is generated by dividing the generators of I by that section (HasLocalRegularGenerator.hasLocalGenerators_colon).

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.IdealSheaf.hasLocalRegularGenerator_of_stalks {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} (J : IdealSheaf 𝒪) (hJ : ∀ (x : X), ∃ g ∈ nonZeroDivisors ↑(𝒪.presheaf.stalk x), J.stalkIdeal x = Ideal.span {g}) : J.HasLocalRegularGenerator

An ideal sheaf whose stalks are principal, each generated by a non-zero-divisor, is locally regularly principal: near every point it is generated by a single section whose germs are non-zero-divisors. The stalkwise hypothesis is upgraded to a section-level one by shrinking the neighbourhood finitely many times. Not in the sources.

theorem Manifold.IdealSheaf.HasLocalRegularGenerator.hasLocalGenerators_colon {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} {I J : IdealSheaf 𝒪} (hJ : J.HasLocalRegularGenerator) (hIJ : ∀ (x : ↑↧X), I.stalkIdeal x ≤ J.stalkIdeal x) : HasLocalGenerators fun (x : ↑↧X) => Submodule.colon (I.stalkIdeal x) ↑(J.stalkIdeal x)

If I ≤ J stalkwise and J is locally regularly principal, then the colon x ↦ (I_x : J_x) has local generators: near a point where J is generated by the non-zero-divisor section s, each generator of I is s times a section, and these quotients generate the colon (Ideal.colon_span_range_mul_of_mem_nonZeroDivisors). Applied to J = M(I), this is what makes the nonmonomial part N(I) = I : M(I) of [Kol07, Definition–Lemma 110] an ideal sheaf.