Locally finitely generated ideal sheaves: basic properties

The elementary theory of the locally finitely generated ideal sheaves IdealSheaf 𝒪 of a sheaf of commutative rings 𝒪 on a topological space.

• A section belongs to J iff its germs lie in the stalk ideals (mem_carrier_iff), so an ideal sheaf is determined by its stalks (ext), and ideal sheaves are ordered stalkwise, with ⊤ and ⊥ the top and bottom elements.
• The ideal sheaf ofStalks 𝒪 I hI has the prescribed stalks (stalkIdeal_ofStalks), so the stalks of ofGlobal 𝒪 f are generated by the germs of the global sections f_i (stalkIdeal_ofGlobal), and those of ⊤, ⊥ and I * J are the unit ideal, the zero ideal and the product (stalkIdeal_top, stalkIdeal_bot, stalkIdeal_mul). The sum I + J and the powers J ^ n are built the same way, with the stalkwise sup and power (stalkIdeal_add, stalkIdeal_pow).
• The support is closed (isClosed_support: a section with germ 1 at a equals 1 near a); the order vanishes exactly off the support (ord_eq_zero_iff) and reverses inclusions (ord_anti).
• For an ideal sheaf J of an analytic manifold, the predicate IsIrreducible of Hironaka's Definition 2 on the closed subspace defined by J (IsNonsingular and IsReduced are in Defs.lean, being statement vocabulary).
• IsInvertible J, for an ideal sheaf of any sheaf of rings: every stalk is generated by a single non-zero-divisor, Hironaka's invertible sheaf of ideals [Hir64, Ch. 0, §2], "everywhere of codimension one" [Hir64, Definition 2]; the stalkwise reading of Scheme.IdealSheafData.IsInvertible.

The spreading of a stalk identity J_x = (g_1, …, g_k) to an open neighbourhood of x is IdealSheaf.exists_opens_stalkIdeal_eq_span of Hironaka/Manifold/Snc/Spreading.lean. On an analytic manifold the cosupport, the order and its semicontinuity are studied in Hironaka/Manifold/IdealSheaf/Order.lean, and the ideal sheaves of the analytic main theorems are those of the structure sheaf (AnalyticManifold.IdealSheaf).

theorem Manifold.IdealSheaf.mem_stalkIdeal_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) {b : ↑X} {s : ↑(𝒪.presheaf.stalk b)} : s ∈ J.stalkIdeal b ↔ ∃ (V : TopologicalSpace.Opens ↑X) (hb : b ∈ V), ∃ g ∈ J.carrier V, (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V b hb)) g = s

theorem Manifold.IdealSheaf.germ_mem_stalkIdeal {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) {U : TopologicalSpace.Opens ↑X} {b : ↑X} (hb : b ∈ U) {f : ↑(𝒪.presheaf.obj (Opposite.op U))} (hf : f ∈ J.carrier U) : (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U b hb)) f ∈ J.stalkIdeal b

theorem Manifold.IdealSheaf.mem_carrier_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) {U : TopologicalSpace.Opens ↑X} {f : ↑(𝒪.presheaf.obj (Opposite.op U))} : f ∈ J.carrier U ↔ ∀ (x : ↑X) (hx : x ∈ U), (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U x hx)) f ∈ J.stalkIdeal x

Sections of the ideal are detected by their germs.

theorem Manifold.IdealSheaf.ext {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {I J : IdealSheaf 𝒪} (h : ∀ (x : ↑X), I.stalkIdeal x = J.stalkIdeal x) : I = J

@[instance_reducible]

instance Manifold.IdealSheaf.instLE {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : LE (IdealSheaf 𝒪)

Equations

• Manifold.IdealSheaf.instLE = { le := fun (I J : Manifold.IdealSheaf 𝒪) => ∀ (x : ↑X), I.stalkIdeal x ≤ J.stalkIdeal x }

theorem Manifold.IdealSheaf.le_def {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {I J : IdealSheaf 𝒪} : I ≤ J ↔ ∀ (x : ↑X), I.stalkIdeal x ≤ J.stalkIdeal x

@[instance_reducible]

instance Manifold.IdealSheaf.instPartialOrder {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : PartialOrder (IdealSheaf 𝒪)

Equations

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

theorem Manifold.IdealSheaf.carrier_mono {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {I J : IdealSheaf 𝒪} (h : I ≤ J) (U : TopologicalSpace.Opens ↑X) : I.carrier U ≤ J.carrier U

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_ofStalks {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (I : (x : ↑X) → Ideal ↑(𝒪.presheaf.stalk x)) (hI : HasLocalGenerators I) (b : ↑X) : (ofStalks 𝒪 I hI).stalkIdeal b = I b

theorem Manifold.IdealSheaf.stalkIdeal_ofGlobal {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) {k : ℕ} (f : Fin k → ↑(𝒪.presheaf.obj (Opposite.op ⊤))) (x : ↑X) : (ofGlobal 𝒪 f).stalkIdeal x = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ ⊤ x trivial)) (f i))

The stalk at x of the ideal sheaf generated by global sections f₁, …, f_k is generated by their germs at x.

The unit and zero ideal sheaves, sums, products, powers

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (x : ↑X) : ⊤.stalkIdeal x = ⊤

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_bot {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (x : ↑X) : ⊥.stalkIdeal x = ⊥

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instBoundedOrder {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : BoundedOrder (IdealSheaf 𝒪)

Equations

• Manifold.IdealSheaf.instBoundedOrder = { toTop := Manifold.IdealSheaf.instTop, le_top := ⋯, toBot := Manifold.IdealSheaf.instBot, bot_le := ⋯ }

theorem Manifold.IdealSheaf.carrier_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (U : TopologicalSpace.Opens ↑X) : ⊤.carrier U = ⊤

theorem Manifold.IdealSheaf.carrier_bot {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (U : TopologicalSpace.Opens ↑X) : ⊥.carrier U = ⊥

The zero ideal sheaf has no nonzero sections (the sheaf condition of 𝒪).

theorem Manifold.IdealSheaf.range_germ_map {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U W : TopologicalSpace.Opens ↑X} (i : W ⟶ U) {b : ↑X} (hb : b ∈ W) {ι : Type u_1} (f : ι → ↑(𝒪.presheaf.obj (Opposite.op U))) : (Set.range fun (j : ι) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ W b hb)) ((CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map i.op)) (f j))) = Set.range fun (j : ι) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U b ⋯)) (f j)

The germs of restricted sections are the germs of the sections.

theorem Manifold.IdealSheaf.hasLocalGenerators_sup {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (I J : IdealSheaf 𝒪) : HasLocalGenerators fun (x : ↑X) => I.stalkIdeal x ⊔ J.stalkIdeal x

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instAdd {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : Add (IdealSheaf 𝒪)

Equations

• Manifold.IdealSheaf.instAdd = { add := fun (I J : Manifold.IdealSheaf 𝒪) => Manifold.IdealSheaf.ofStalks 𝒪 (fun (x : ↑X) => I.stalkIdeal x ⊔ J.stalkIdeal x) ⋯ }

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_add {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (I J : IdealSheaf 𝒪) (x : ↑X) : (I + J).stalkIdeal x = I.stalkIdeal x ⊔ J.stalkIdeal x

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_mul {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (I J : IdealSheaf 𝒪) (x : ↑X) : (I * J).stalkIdeal x = I.stalkIdeal x * J.stalkIdeal x

def Manifold.IdealSheaf.pow {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) : ℕ → IdealSheaf 𝒪

Powers: J ^ 0 = ⊤, J ^ (n + 1) = J ^ n * J.

Equations

• J.pow 0 = ⊤
• J.pow n.succ = J.pow n * J

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instPowNat {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : Pow (IdealSheaf 𝒪) ℕ

Equations

• Manifold.IdealSheaf.instPowNat = { pow := Manifold.IdealSheaf.pow }

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_pow {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) (n : ℕ) (x : ↑X) : (J ^ n).stalkIdeal x = J.stalkIdeal x ^ n

The cosupport and the order

@[simp]

theorem Manifold.IdealSheaf.mem_support {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) {x : ↑X} : x ∈ J.support ↔ J.stalkIdeal x ≠ ⊤

theorem Manifold.IdealSheaf.isOpen_compl_support {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) : IsOpen J.supportᶜ

The cosupport is closed: a section with germ 1 at a equals 1 near a.

theorem Manifold.IdealSheaf.isClosed_support {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) : IsClosed J.support

theorem Ideal.span_eq_top_iff_exists_isUnit {R : Type u_1} [CommRing R] [IsLocalRing R] (S : Set R) : span S = ⊤ ↔ ∃ s ∈ S, IsUnit s

In a local ring, a span is the unit ideal iff one of the generators is a unit.

def Manifold.IdealSheaf.IsInvertible {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) : Prop

The ideal sheaf is invertible: at every point its stalk is generated by a single non-zero-divisor, i.e. J is locally free of rank one — Hironaka's invertible sheaf of ideals [Hir64, Ch. 0, §2], "everywhere of codimension one" [Hir64, Ch. 0, §5, Definition 2, p. 141], the condition on the boundary E in Main Theorem II'(N). Read at the stalks, as every predicate of the ideal-sheaf vocabulary is (no main theorem states it, which is why it is not in Defs.lean); compare Scheme.IdealSheafData.IsInvertible on schemes, whose stalkwise reading this is (isInvertible_iff_forall_stalkIdeal_eq_span, on a locally Noetherian scheme).

Equations

• J.IsInvertible = ∀ (x : ↑X), ∃ a ∈ nonZeroDivisors ↑(𝒪.presheaf.stalk x), J.stalkIdeal x = Ideal.span {a}

theorem Manifold.IdealSheaf.ord_eq_zero_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)] {x : ↑X} : J.ord x = 0 ↔ x ∉ J.support

theorem Manifold.IdealSheaf.ord_eq_top_of_stalkIdeal_eq_bot {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)] {x : ↑X} (h : J.stalkIdeal x = ⊥) : J.ord x = ⊤

theorem Manifold.IdealSheaf.ord_anti {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)] {I J : IdealSheaf 𝒪} (h : I ≤ J) (x : ↑X) : J.ord x ≤ I.ord x

theorem Manifold.IdealSheaf.stalkIdeal_eq_top_iff_exists_isUnit {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)] {U : TopologicalSpace.Opens ↑X} {k : ℕ} {f : Fin k → ↑(𝒪.presheaf.obj (Opposite.op U))} {b : ↑X} (hb : b ∈ U) (hf : J.stalkIdeal b = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U b hb)) (f i))) : J.stalkIdeal b = ⊤ ↔ ∃ (i : Fin k), IsUnit ((CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U b hb)) (f i))

On a generating open set the cosupport is the set of points where every generator is a non-unit germ.

Predicates on the closed subspace defined by an ideal sheaf of an analytic manifold

def AnalyticManifold.IdealSheaf.IsIrreducible {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : Prop

The closed analytic subspace defined by J is irreducible (and nonempty): its set of points is not the union of two proper Zariski-closed subsets, the cosupports of locally finitely generated ideal sheaves [BM97, Definitions and remarks 3.9] — Hironaka's "maximal reduced irreducible analytic subspace" [Hir64, Definition 2, p. 141], as a condition on the set of points.

Equations

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