Closed subspaces: intersections, unions, reduction, and the predicates through the stalks

The elementary part of the theory of closed subspaces: the constructions on closed subspaces that need no analysis, and the readings of the predicates of Hironaka/AnalyticSpace/ClosedSubspace.lean through the stalks.

• E ∩ F is the subspace of the ideal sheaf generated by those of E and F (inter := E + F), E ∪ F the subspace of their intersection (union, given local generators of the intersection, which hasLocalGenerators_inf of Hironaka/AnalyticSpace/CoherentAnalytic.lean supplies). Their point sets are the intersection and the union of the point sets because, in a local ring, a sum of two ideals is the unit ideal only if one of them is (Ideal.sup_eq_top_iff_of_isLocalRing: two proper ideals lie in the maximal ideal), and an intersection is the unit ideal only if both are.
• red X, the reduction of X [Hir64, Ch. 0, §4], the subspace of the nilradical (given local generators of the nilradicals); |red X| = |X| because 1 is not nilpotent in a nontrivial ring; red X is reduced because the nilradical is a radical ideal; X is reduced iff every stalk has zero nilradical (nilradical_eq_bot_iff), iff X as the subspace top X of itself is reduced.
• X.singularLocus is the set of points with non-regular local ring (by definition), and X is non-singular iff every local ring is regular, iff top X is non-singular (the stalks of the quotient by the zero ideal sheaf are 𝒪_{X,x}/0 ≅ 𝒪_{X,x}, RingEquiv.quotientBot) [Hir64, Ch. 0, §1, p. 121].
• The predicates through the stalks. support, le, IsNonzeroEverywhere, IsIrreducible, HasOnlyNormalCrossingsWith, HasOnlyNormalCrossings (with top X = ⊥) are read off by Iff.rfl; top X has full support and IsUnit means empty support; ord is 0 off the support and ⊤ exactly at a zero stalk (Krull's intersection theorem in the Noetherian stalk); the predicates defined through the subspace's structure sheaf — IsReduced, IsSimplePointAt, IsNonsingular, dim — are read through stalkEquiv : 𝒪_{W,x} ≅ 𝒪_{X,x}/𝓘_x (reducedness of the quotient is radicality of the ideal, Ideal.isRadical_iff_quotient_reduced; regularity and Krull dimension are invariant under ring isomorphisms), the supremum defining dim being bounded by d iff each local dimension is (WithBot.unbotD_le_iff).

theorem Ideal.sup_eq_top_iff_of_isLocalRing {R : Type u_1} [CommRing R] [IsLocalRing R] {I J : Ideal R} : I ⊔ J = ⊤ ↔ I = ⊤ ∨ J = ⊤

In a local ring, a sum of ideals is the unit ideal only if one of them is.

noncomputable def AnalyticSpace.ClosedSubspace.inter {K : Type} [RCLike K] {X : AnalyticSpace K} (E F : X.ClosedSubspace) : X.ClosedSubspace

E ∩ F, the subspace of the ideal sheaf generated by those of E and F.

Equations

• E.inter F = E + F

theorem AnalyticSpace.ClosedSubspace.stalkIdeal_inter {K : Type} [RCLike K] {X : AnalyticSpace K} (E F : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : Manifold.IdealSheaf.stalkIdeal (E.inter F) x = Manifold.IdealSheaf.stalkIdeal E x ⊔ Manifold.IdealSheaf.stalkIdeal F x

theorem AnalyticSpace.ClosedSubspace.support_inter {K : Type} [RCLike K] {X : AnalyticSpace K} (E F : X.ClosedSubspace) : Manifold.IdealSheaf.support (E.inter F) = Manifold.IdealSheaf.support E ∩ Manifold.IdealSheaf.support F

noncomputable def AnalyticSpace.ClosedSubspace.union {K : Type} [RCLike K] {X : AnalyticSpace K} (E F : X.ClosedSubspace) (h : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => Manifold.IdealSheaf.stalkIdeal E x ⊓ Manifold.IdealSheaf.stalkIdeal F x) : X.ClosedSubspace

E ∪ F, the subspace of the intersection of the ideal sheaves of E and F, given local generators h of the intersection.

Equations

• E.union F h = Manifold.IdealSheaf.ofStalks X.𝒪 (fun (x : ↑↑X.toPresheafedSpace) => Manifold.IdealSheaf.stalkIdeal E x ⊓ Manifold.IdealSheaf.stalkIdeal F x) h

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

theorem AnalyticSpace.ClosedSubspace.support_union {K : Type} [RCLike K] {X : AnalyticSpace K} (E F : X.ClosedSubspace) (h : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => Manifold.IdealSheaf.stalkIdeal E x ⊓ Manifold.IdealSheaf.stalkIdeal F x) : Manifold.IdealSheaf.support (E.union F h) = Manifold.IdealSheaf.support E ∪ Manifold.IdealSheaf.support F

noncomputable def AnalyticSpace.red {K : Type} [RCLike K] (X : AnalyticSpace K) (h : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => nilradical ↑(X.presheaf.stalk x)) : X.ClosedSubspace

The reduction red X [Hir64, Ch. 0, §4]: the closed subspace of the nilradical, given local generators h of the nilradicals.

Equations

• X.red h = Manifold.IdealSheaf.ofStalks X.𝒪 (fun (x : ↑↑X.toPresheafedSpace) => nilradical ↑(X.presheaf.stalk x)) h

theorem AnalyticSpace.stalkIdeal_red {K : Type} [RCLike K] (X : AnalyticSpace K) (h : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => nilradical ↑(X.presheaf.stalk x)) (x : ↑↑X.toPresheafedSpace) : Manifold.IdealSheaf.stalkIdeal (X.red h) x = nilradical ↑(X.presheaf.stalk x)

theorem AnalyticSpace.support_red {K : Type} [RCLike K] (X : AnalyticSpace K) (h : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => nilradical ↑(X.presheaf.stalk x)) : Manifold.IdealSheaf.support (X.red h) = Set.univ

theorem AnalyticSpace.isReduced_iff_nilradical_eq_bot {K : Type} [RCLike K] (X : AnalyticSpace K) : X.IsReduced ↔ ∀ (x : ↑↑X.toPresheafedSpace), nilradical ↑(X.presheaf.stalk x) = ⊥

theorem AnalyticSpace.singularLocus_eq {K : Type} [RCLike K] (X : AnalyticSpace K) : X.singularLocus = {x : ↑↑X.toPresheafedSpace | ¬IsRegularLocalRing ↑(X.presheaf.stalk x)}

The multiple points [Hir64, Ch. 0, §1, p. 121]: the points whose local ring is not regular.

theorem AnalyticSpace.isNonsingular_iff {K : Type} [RCLike K] (X : AnalyticSpace K) : X.IsNonsingular ↔ ∀ (x : ↑↑X.toPresheafedSpace), IsRegularLocalRing ↑(X.presheaf.stalk x)

X is non-singular iff every local ring is regular [Hir64, Ch. 0, §1, p. 121].

theorem AnalyticSpace.ClosedSubspace.mem_support_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : x ∈ Manifold.IdealSheaf.support W ↔ Manifold.IdealSheaf.stalkIdeal W x ≠ ⊤

@[simp]

theorem AnalyticSpace.ClosedSubspace.support_top {K : Type} [RCLike K] {X : AnalyticSpace K} : Manifold.IdealSheaf.support (top X) = Set.univ

theorem AnalyticSpace.ClosedSubspace.le_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W V : X.ClosedSubspace) : W.le V ↔ ∀ (x : ↑↑X.toPresheafedSpace), Manifold.IdealSheaf.stalkIdeal V x ≤ Manifold.IdealSheaf.stalkIdeal W x

theorem AnalyticSpace.ClosedSubspace.support_mono {K : Type} [RCLike K] {X : AnalyticSpace K} (W V : X.ClosedSubspace) (h : W.le V) : Manifold.IdealSheaf.support W ⊆ Manifold.IdealSheaf.support V

theorem AnalyticSpace.ClosedSubspace.isUnit_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : W.IsUnit ↔ Manifold.IdealSheaf.support W = ∅

theorem AnalyticSpace.ClosedSubspace.isNonzeroEverywhere_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : W.IsNonzeroEverywhere ↔ ∀ (x : ↑↑X.toPresheafedSpace), Manifold.IdealSheaf.stalkIdeal W x ≠ ⊥

theorem AnalyticSpace.ClosedSubspace.isIrreducible_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : W.IsIrreducible ↔ (Manifold.IdealSheaf.support W).Nonempty ∧ ∀ (Z₁ Z₂ : X.ClosedSubspace), Manifold.IdealSheaf.support W ⊆ Manifold.IdealSheaf.support Z₁ ∪ Manifold.IdealSheaf.support Z₂ → Manifold.IdealSheaf.support W ⊆ Manifold.IdealSheaf.support Z₁ ∨ Manifold.IdealSheaf.support W ⊆ Manifold.IdealSheaf.support Z₂

theorem AnalyticSpace.ClosedSubspace.hasOnlyNormalCrossings_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (E : X.ClosedSubspace) : E.HasOnlyNormalCrossings ↔ E.HasOnlyNormalCrossingsWith (top X)

theorem AnalyticSpace.ClosedSubspace.ord_eq_zero_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : W.ord x = 0 ↔ x ∉ Manifold.IdealSheaf.support W

theorem AnalyticSpace.ClosedSubspace.ord_eq_top_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : W.ord x = ⊤ ↔ Manifold.IdealSheaf.stalkIdeal W x = ⊥

theorem AnalyticSpace.ClosedSubspace.isRegularLocalRing_space_stalk_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) (h : x ∈ Manifold.IdealSheaf.support W) : IsRegularLocalRing ↑(W.space.presheaf.stalk ⟨x, h⟩) ↔ IsRegularLocalRing (↑(X.presheaf.stalk x) ⧸ Manifold.IdealSheaf.stalkIdeal W x)

The stalk of the subspace at ⟨x, h⟩ is 𝒪_{X,x}/𝓘_x, so regularity and reducedness of the subspace at x are those of the quotient ring.

theorem AnalyticSpace.ClosedSubspace.isSimplePointAt_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : W.IsSimplePointAt x ↔ x ∈ Manifold.IdealSheaf.support W ∧ IsRegularLocalRing (↑(X.presheaf.stalk x) ⧸ Manifold.IdealSheaf.stalkIdeal W x)

theorem AnalyticSpace.ClosedSubspace.isNonsingular_iff_forall {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : W.IsNonsingular ↔ ∀ x ∈ Manifold.IdealSheaf.support W, IsRegularLocalRing (↑(X.presheaf.stalk x) ⧸ Manifold.IdealSheaf.stalkIdeal W x)

theorem AnalyticSpace.ClosedSubspace.isReduced_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : W.IsReduced ↔ ∀ (x : ↑↑X.toPresheafedSpace), (Manifold.IdealSheaf.stalkIdeal W x).IsRadical

theorem AnalyticSpace.ClosedSubspace.hasOnlyNormalCrossingsWith_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (E D : X.ClosedSubspace) : E.HasOnlyNormalCrossingsWith D ↔ ∀ x ∈ Manifold.IdealSheaf.support D, ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)) ∧ (∀ P ∈ (Manifold.IdealSheaf.stalkIdeal E x).minimalPrimes, ∃ (i : Fin n), P = Ideal.span {z i}) ∧ ∃ (s : Finset (Fin n)), Manifold.IdealSheaf.stalkIdeal D x = Ideal.span (z '' ↑s)

theorem AnalyticSpace.ClosedSubspace.dim_le_iff {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (d : ℕ∞) : W.dim ≤ d ↔ ∀ x ∈ Manifold.IdealSheaf.support W, ringKrullDim (↑(X.presheaf.stalk x) ⧸ Manifold.IdealSheaf.stalkIdeal W x) ≤ ↑d

theorem AnalyticSpace.isReduced_red {K : Type} [RCLike K] (X : AnalyticSpace K) (h : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => nilradical ↑(X.presheaf.stalk x)) : (X.red h).IsReduced

theorem AnalyticSpace.isReduced_iff_isReduced_top {K : Type} [RCLike K] (X : AnalyticSpace K) : X.IsReduced ↔ (ClosedSubspace.top X).IsReduced

theorem AnalyticSpace.isNonsingular_iff_isNonsingular_top {K : Type} [RCLike K] (X : AnalyticSpace K) : X.IsNonsingular ↔ (ClosedSubspace.top X).IsNonsingular