Closed analytic subspaces: operations and predicates

The operations on the closed subspaces ClosedSubspace X := IdealSheaf X.𝒪 of an analytic K-space X [Hir64, Ch. 0, §1 and §5], [BM97, §3], and the predicates of [Hir64] on them, read through the ideal sheaf 𝓘 or through the subspace Y = (S(𝓘), (𝒪_X/𝓘)|_{S(𝓘)}), whose stalks are 𝒪_{Y,y} ≅ 𝒪_{X,y}/𝓘_y (QuotientSpace.stalkEquiv).

Main definitions

• support (Hironaka's S(𝓘), the cosupport of the ideal sheaf), top X (the zero ideal sheaf, X as a subspace of itself), le W V (W ⊆ V, i.e. 𝓘_V ⊆ 𝓘_W), IsUnit (𝓘 = 𝒪_X, the empty subspace), IsNonzeroEverywhere (Hironaka's "coherent sheaf of non-zero ideals": every stalk nonzero), ord (Hironaka's order ν(𝓘_x) of the stalk ideal [Hir64, Ch. 0, §3]).
• space W, the subspace Y = (S(𝓘), (𝒪_X/𝓘)|_{S(𝓘)}) as a K-local-ringed space, and through its stalks (Hironaka's definitions "for arbitrary local-ringed spaces" Hir64, Ch. 0, §1, p. 121): IsReduced W (every stalk of 𝒪_Y reduced), IsNonsingular W (every stalk of 𝒪_Y regular), IsSimplePointAt W x (x ∈ |Y| and 𝒪_{Y,x} regular), dim W (sup_{y ∈ |Y|} dim 𝒪_{Y,y}, the Krull dimension of the stalks [Fre17, II 5.2]).
• IsIrreducible W: |W| nonempty and contained in a union of two closed analytic subsets only if contained in one of them (irreducibility in the Zariski topology of [BM97, 3.9], whose closed sets are the supports of closed subspaces; Hironaka's "a maximal reduced irreducible … analytic subspace" [Hir64, Ch. 0, §5, Definition 2, p. 141]).
• IsInvertible E (IdealSheaf.IsInvertible of Hironaka/Manifold/IdealSheaf/Basic.lean, as for any ideal sheaf): 𝓘_E is locally free of rank one — at every point the stalk is generated by a single non-zero-divisor (Hironaka's invertible sheaf of ideals [Hir64, Ch. 0, §2], Definition 2's "everywhere of codimension one").
• HasOnlyNormalCrossingsWith E D, HasOnlyNormalCrossings E: Hironaka's Definition 2 [Hir64, Ch. 0, §5] at the stalk level — at every point x of D a regular system of parameters of 𝒪_{X,x} such that the ideal of each irreducible component of E through x (a minimal prime of 𝓘_{E,x}) is generated by one parameter and 𝓘_{D,x} by some of them; D = X is D = ⊥. The two clauses of a regular system of parameters (it generates 𝔪_x; it has as many members as the Krull dimension) are written out. The boundary predicate of the resolution theorem, IsSncBoundary, reads Definition 2 on global components instead.
• comap D f, the inverse image f⁻¹(𝓘_D)𝒪_Y of a closed subspace D ⊆ X along a morphism f : Y → X [Hir64, Ch. 0, §5], the total transform of D by f.
• IsNormallyFlatAlongAt V W x: Hironaka's Definition 1 [Hir64, Ch. 0, §4] — with J the ideal of W in V, i.e. the image of 𝓘_{W,x} in 𝒪_{V,x} = 𝒪_{X,x}/𝓘_{V,x}, the stalk at x ∈ W of every gr^p = J^p/J^{p+1} is a free 𝒪_{W,x} = 𝒪_{V,x}/J-module. No result of this library is proved about normal flatness.

The subspace's IsReduced and IsNonsingular are those of the analytic space closedSubspace X W by definition; its image in X is the support S(𝓘) (range_toFun_closedSubspaceι), and a point of the space is simple iff its image is a simple point of the subspace (mem_reg_closedSubspace_iff).

instance AnalyticSpace.instIsLocalRingStalkSheaf (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat) : IsLocalRing ↑(X.𝒪.presheaf.stalk x)

The stalks of the structure sheaf of a locally ringed space, read through X.𝒪 (a def in Mathlib, so the instance Mathlib states for X.presheaf.stalk x is not found for it), are local rings — the instance IdealSheaf.ord asks for on IdealSheaf X.𝒪.

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

X itself as a closed subspace: the zero ideal sheaf.

Equations

• AnalyticSpace.ClosedSubspace.top X = ⊥

def AnalyticSpace.ClosedSubspace.le {K : Type} [RCLike K] {X : AnalyticSpace K} (W V : X.ClosedSubspace) : Prop

The inclusion W ⊆ V of closed subspaces is the reverse inclusion 𝓘_V ⊆ 𝓘_W of their ideal sheaves (stalkwise).

Equations

• W.le V = (V ≤ W)

def AnalyticSpace.ClosedSubspace.IsUnit {K : Type} [RCLike K] {X : AnalyticSpace K} (J : X.ClosedSubspace) : Prop

The ideal sheaf of the subspace is the unit ideal sheaf, 𝓘 = 𝒪_X: the empty subspace (the final clause J_γ = 𝒪_{X_γ} of [Hir64, Main Theorem II′(N) (iv), p. 156]).

Equations

• J.IsUnit = (J = ⊤)

def AnalyticSpace.ClosedSubspace.IsNonzeroEverywhere {K : Type} [RCLike K] {X : AnalyticSpace K} (J : X.ClosedSubspace) : Prop

Every stalk of the ideal sheaf is nonzero (Hironaka's "coherent sheaf of non-zero ideals" [Hir64, Main Theorem II'(N), p. 156]).

Equations

• J.IsNonzeroEverywhere = Manifold.IdealSheaf.IsNonzeroEverywhere J

noncomputable def AnalyticSpace.ClosedSubspace.ord {K : Type} [RCLike K] {X : AnalyticSpace K} (J : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : ℕ∞

ν(𝓘_x), the order of the stalk ideal at x [Hir64, Ch. 0, §3]: the largest ν with 𝓘_x ⊆ 𝔪_x^ν, ⊤ when 𝓘_x = 0.

Equations

• J.ord x = Manifold.IdealSheaf.ord J x

@[reducible, inline]

noncomputable abbrev AnalyticSpace.ClosedSubspace.space {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : KLocallyRingedSpace K

The subspace Y = (S(𝓘), (𝒪_X/𝓘)|_{S(𝓘)}) [Hir64, Ch. 0, §1], [BM97, §3] as a K-local-ringed space, with the K-structure induced along the canonical morphism Y ⟶ X. Its stalk at y is 𝒪_{X,y}/𝓘_y (QuotientSpace.stalkEquiv).

Equations

• W.space = X.quotient W

def AnalyticSpace.ClosedSubspace.IsReduced {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : Prop

The subspace is reduced [Hir64, Introduction]: its structure sheaf 𝒪_Y has no nilpotent elements, i.e. every stalk of 𝒪_Y is reduced.

Equations

• W.IsReduced = ∀ (y : ↑↑W.space.toPresheafedSpace), IsReduced ↑(W.space.presheaf.stalk y)

def AnalyticSpace.ClosedSubspace.IsNonsingular {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : Prop

The subspace is non-singular [Hir64, Ch. 0, §1, p. 121]: every point of |Y| is a simple point of Y, its local ring 𝒪_{Y,y} regular.

Equations

• W.IsNonsingular = ∀ (y : ↑↑W.space.toPresheafedSpace), IsRegularLocalRing ↑(W.space.presheaf.stalk y)

def AnalyticSpace.ClosedSubspace.IsSimplePointAt {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : Prop

x is a simple point of the subspace W [Hir64, Ch. 0, §1, p. 121]: x ∈ |W| and the local ring 𝒪_{W,x} of the subspace at x is regular.

Equations

• W.IsSimplePointAt x = ∃ (h : x ∈ Manifold.IdealSheaf.support W), IsRegularLocalRing ↑(W.space.presheaf.stalk ⟨x, h⟩)

noncomputable def AnalyticSpace.ClosedSubspace.dim {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : ℕ∞

The dimension of the subspace W (the dimension of W that Main Theorem I'(n) of [Hir64, Ch. 0, §7, p. 155] uses without defining it there): the supremum over the points y of |W| of the Krull dimension of 𝒪_{W,y} [Fre17, II 5.2] (as an element of ℕ∞; 0 for the empty subspace, whose supremum is over no points; a stalk of a nonempty subspace is a nontrivial local ring, so no ⊥ is ever read).

Equations

• W.dim = ⨆ (y : ↑↑W.space.toPresheafedSpace), WithBot.unbotD 0 (ringKrullDim ↑(W.space.presheaf.stalk y))

def AnalyticSpace.ClosedSubspace.IsIrreducible {K : Type} [RCLike K] {X : AnalyticSpace K} (W : X.ClosedSubspace) : Prop

The subspace is irreducible, and nonempty (Hironaka's "a maximal reduced irreducible … analytic subspace" [Hir64, Ch. 0, §5, Definition 2, p. 141]; the Zariski topology of [BM97, 3.9]): its set of points is not contained in the union of the point sets of two closed analytic subspaces unless it is contained in one of them.

Equations

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

def AnalyticSpace.ClosedSubspace.HasOnlyNormalCrossingsWith {K : Type} [RCLike K] {X : AnalyticSpace K} (E D : X.ClosedSubspace) : Prop

Hironaka's Definition 2 [Hir64, Ch. 0, §5] for analytic spaces, at the stalk level: E has only normal crossings with D if at every point x of D there is a regular system of parameters (z_1, …, z_n) of 𝒪_{X,x} (n generators of the maximal ideal, n the Krull dimension) such that the ideal of each irreducible component of E through x (a minimal prime of 𝓘_{E,x}) is generated by one of the z_i and the ideal 𝓘_{D,x} of D is generated by some of the z_i. Definition 2 presupposes X non-singular, E reduced and 𝓘_E invertible; those are hypotheses of the statements that use the predicate, not part of it.

Equations

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

def AnalyticSpace.ClosedSubspace.HasOnlyNormalCrossings {K : Type} [RCLike K] {X : AnalyticSpace K} (E : X.ClosedSubspace) : Prop

Hironaka's Definition 2 with D = X ("we simply say that E has only normal crossings" [Hir64, Ch. 0, §5]): HasOnlyNormalCrossingsWith E ⊥, the zero ideal sheaf ⊥ being the ideal of X itself (top X).

Equations

• E.HasOnlyNormalCrossings = E.HasOnlyNormalCrossingsWith ⊥

Inverse images

noncomputable def AnalyticSpace.ClosedSubspace.comap {K : Type} [RCLike K] {X Y : AnalyticSpace K} (D : X.ClosedSubspace) (f : Y ⟶ X) : Y.ClosedSubspace

The inverse image f⁻¹(𝓘_D)·𝒪_Y of a closed subspace D ⊆ X along a morphism f : Y → X [Hir64, Ch. 0, §5] (the sheaf of ideals generated by the pull-back of 𝓘_D, the total transform of D by f): the closed subspace of Y whose stalk at y is the ideal generated by the image of 𝓘_{D, f y} under the stalk map — QuotientSpace.comap on the underlying morphism of locally ringed spaces.

Equations

• D.comap f = AnalyticSpace.QuotientSpace.comap (↑f) D

Normal flatness (Hironaka's Definition 1)

@[reducible, inline]

abbrev AnalyticSpace.ClosedSubspace.grPiece {R : Type u_1} [CommRing R] (I : Ideal R) (p : ℕ) : Type u_1

The p-th graded piece I^p / I^{p+1} of the I-adic filtration of R, as a module over R/I (Hironaka's gr^p, the stalk of J^p/J^{p+1} [Hir64, Ch. 0, §4, Definition 1]; Mathlib supplies the R ⧸ I-module structure on M ⧸ I • M).

Equations

• AnalyticSpace.ClosedSubspace.grPiece I p = (↥(I ^ p) ⧸ I • ⊤)

noncomputable def AnalyticSpace.ClosedSubspace.relativeIdeal {K : Type} [RCLike K] {X : AnalyticSpace K} (V W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : Ideal (↑(X.presheaf.stalk x) ⧸ Manifold.IdealSheaf.stalkIdeal V x)

The ideal J of the subspace W in the subspace V at the point x Hir64, Ch. 0, §4, Definition 1: the image of 𝓘_{W,x} in 𝒪_{V,x} = 𝒪_{X,x}/𝓘_{V,x}.

Equations

• V.relativeIdeal W x = Ideal.map (Ideal.Quotient.mk (Manifold.IdealSheaf.stalkIdeal V x)) (Manifold.IdealSheaf.stalkIdeal W x)

def AnalyticSpace.ClosedSubspace.IsNormallyFlatAlongAt {K : Type} [RCLike K] {X : AnalyticSpace K} (V W : X.ClosedSubspace) (x : ↑↑X.toPresheafedSpace) : Prop

Hironaka's Definition 1 [Hir64, Ch. 0, §4]: the analytic subspace V of X is normally flat along its subspace W at the point x of W if, with J the ideal of W in V, the stalk at x of gr^p = J^p/J^{p+1} is a free 𝒪_{W,x}-module for every p ≥ 0, where 𝒪_{W,x} = 𝒪_{V,x}/J_x. With V = top X this is "X is normally flat along W at x". No result of this library is proved about normal flatness.

Equations

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

The closed subspace as an analytic space

theorem AnalyticSpace.range_toFun_closedSubspaceι {K : Type} [RCLike K] (X : AnalyticSpace K) (J : Manifold.IdealSheaf X.𝒪) : Set.range ↑(X.closedSubspaceι J) = J.support

The image of the closed subspace in X is its support S(𝓘).

theorem AnalyticSpace.mem_reg_closedSubspace_iff {K : Type} [RCLike K] (X : AnalyticSpace K) (W : X.ClosedSubspace) (y : ↑↑(X.closedSubspace W).toPresheafedSpace) : y ∈ (X.closedSubspace W).regularLocus ↔ W.IsSimplePointAt (↑(X.closedSubspaceι W) y)