The simple locus of a closed subspace of a manifold, read in the ambient

CenterComponents.lean reads the simple points of the closed subspace V(J) = Sp(A)/J of a manifold A (IdealSheaf.toAnalyticSpace) as the subset regSet J ⊆ A, the image of Reg (V(J)) under the canonical inclusion. This module supplies the elementary facts about that reading:

• the stalk of V(J) at a point y is the quotient 𝒪_{A,y} / J_y of the ambient stalk (QuotientSpace.stalkEquiv), so V(J) is reduced when J has radical stalks (isReduced_toAnalyticSpace_of_isRadical; a space is reduced when its local rings have no nilpotent elements, [Hir64, Introduction]); the simple points themselves are read through mem_reg_toAnalyticSpace_iff (Hironaka/Resolution/Analytic/Wlo09/Clauses);
• the inclusion V(J) → A is continuous with range the support |J| (the underlying space of a local analytic space (S(𝓘), 𝒜_G/𝓘) is the support of 𝒜_G/𝓘, [Hir64, Ch. 0, §1, p. 119]), so regSet J ⊆ |J|.

theorem Manifold.isReduced_toAnalyticSpace_of_isRadical {K : Type} [RCLike K] {n : ℕ} {A : AnalyticManifold K (Fin n → K)} (J : A.IdealSheaf) (hJ : ∀ (x : ↑↧A.carrier), (IdealSheaf.stalkIdeal J x).IsRadical) : J.toAnalyticSpace.IsReduced

The closed subspace V(J) is reduced when J has radical stalks: its stalks are the quotients 𝒪_{A,y} / J_y (QuotientSpace.stalkEquiv), and reducedness means that the local rings have no nilpotent elements [Hir64, Introduction].

theorem Manifold.range_toFun_toAnalyticSpaceι {K : Type} [RCLike K] {n : ℕ} {A : AnalyticManifold K (Fin n → K)} (J : A.IdealSheaf) : (Set.range fun (y : ↑↑J.toAnalyticSpace.toPresheafedSpace) => ↑J.toAnalyticSpaceι y) = IdealSheaf.support J

The range of the inclusion V(J) → A is the support |J| (range_toFun_closedSubspaceι, in the form of regSet); the underlying space of a local analytic space is the support of its structure sheaf [Hir64, Ch. 0, §1, p. 119].

theorem Manifold.regSet_subset_cosupport {K : Type} [RCLike K] {n : ℕ} {A : AnalyticManifold K (Fin n → K)} (J : A.IdealSheaf) : J.regSet ⊆ IdealSheaf.support J

The simple locus of V(J), read in A, lies in the support |J|.

theorem Manifold.continuous_toFun_toAnalyticSpaceι {K : Type} [RCLike K] {n : ℕ} {A : AnalyticManifold K (Fin n → K)} (J : A.IdealSheaf) : Continuous fun (y : ↑↑J.toAnalyticSpace.toPresheafedSpace) => ↑J.toAnalyticSpaceι y

The inclusion V(J) → A is continuous (the base map of the canonical morphism).