Local models near a point: zero sets, simple points, graph ideals

Bookkeeping for the density of the simple points of a reduced complex space (Hironaka/AnalyticSpace/RegDensity.lean; [Fre17, II 5.13]): the generators modelGens of (f)_z read in Conv K n at a point z of a local model and their zero set near 0, which is the translated point set of the model (eventually_forall_evalSeries_modelGens_eq_zero_iff, from the Taylor homomorphism's specification IsTaylorHom; mem_cosupport_modelIdeal_iff_extendSection for the model's points); the transport of regularity and reducedness of stalks along an open subspace and a K-isomorphism in both directions, so that a point of the chart X|U ≅ (localModel)|W is simple in X iff its image is simple in the model (mem_reg_iff_localModel); the graph ideal (X_j − T_j(X ∘ e))_{j ∉ range e}, whose quotient is a regular local ring (isRegularLocalRing_quotient_graphIdeal: n − d germs of the maximal ideal with independent differentials, isRegularLocalRing_quotient_span_range_and_ringKrullDim of Hironaka/AnalyticSpace/RegularParameters.lean), hence a domain — so the graph ideal is prime and Rückert's Nullstellensatz identifies it with the radical model ideal at a graph point; and a separating series for a minimal prime (in every other minimal prime, not in the given one), which isolates one local irreducible component. Routine; used by Hironaka/AnalyticSpace/RegDensity.lean, Hironaka/AnalyticSpace/Nullstellensatz.lean, Hironaka/AnalyticSpace/CoverLemmas.lean, Hironaka/AnalyticSpace/RegOpenImmersion.lean and Hironaka/Resolution/Analytic/Kol07Thm45/PieceModel.lean.

theorem AnalyticSpace.coe_convAt {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) (s : ↑((affine K n).presheaf.stalk q)) : ↑((taylorAffine K n q) s) = (taylorAt K n q) s

The Taylor isomorphism at q, coerced to series, is the Taylor homomorphism.

theorem AnalyticSpace.eventually_evalSeries_convAt_germ {K : Type} [RCLike K] {n : ℕ} (p : Kn K n) {U : TopologicalSpace.Opens (Kn K n)} (hp : p ∈ U) (F : ↑((affine K n).presheaf.obj (Opposite.op U))) : ∀ᶠ (y' : Fin n → K) in nhds 0, Analytic.evalSeries (↑((taylorAffine K n p) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U p hp)) F))) y' = Manifold.extendSection K (Kn K n) F { down := p.down + y' }

The function of the Taylor series at p of the germ of a section F is F near p.

noncomputable def AnalyticSpace.modelGens {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) (j : Fin k) : ↥(Analytic.Conv K n)

The generators of (f)_z read in Conv K n.

Equations

• AnalyticSpace.modelGens G f z j = (AnalyticSpace.taylorAffine K n ↑↑z) ((CategoryTheory.ConcreteCategory.hom ((AnalyticSpace.affine K n).presheaf.germ G ↑↑z ⋯)) (f j))

theorem AnalyticSpace.span_range_modelGens {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : Ideal.span (Set.range (modelGens G f z)) = modelIdealAt G f z

theorem AnalyticSpace.eventually_forall_evalSeries_modelGens_eq_zero_iff {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : ∀ᶠ (y' : Fin n → K) in nhds 0, (∀ (j : Fin k), Analytic.evalSeries (↑(modelGens G f z j)) y' = 0) ↔ ∀ (j : Fin k), Manifold.extendSection K (Kn K n) (f j) { down := (↑↑z).down + y' } = 0

The zero set of (f)_z near 0 is the translated point set of the model.

theorem AnalyticSpace.mem_cosupport_modelIdeal_iff_extendSection {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : x ∈ (modelIdeal K n G f).support ↔ ∀ (j : Fin k), Manifold.extendSection K (Kn K n) (f j) ↑x = 0

Membership of a point of G in the model: all equations vanish.

theorem AnalyticSpace.isRegularLocalRing_stalk_restrictOpen_iff {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) : IsRegularLocalRing ↑((X.restrictOpen U).presheaf.stalk x) ↔ IsRegularLocalRing ↑(X.presheaf.stalk ↑x)

Regularity of a stalk of X|U is regularity of the stalk of X.

theorem AnalyticSpace.isRegularLocalRing_stalk_kIso_iff {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) : IsRegularLocalRing ↑(B.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) a)) ↔ IsRegularLocalRing ↑(A.presheaf.stalk a)

Regularity of stalks is invariant under a K-isomorphism.

theorem AnalyticSpace.mem_reg_iff_localModel {K : Type} [RCLike K] {X : AnalyticSpace K} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {n k : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {f : Fin k → AnalyticFun K n G} {W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} (e : (X.restrictOpen U).KIso ((localModel K n G f).restrictOpen W)) {y : ↑↑X.toPresheafedSpace} (hy : y ∈ U) : y ∈ X.regularLocus ↔ IsRegularLocalRing ↑((localModel K n G f).presheaf.stalk ↑((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) ⟨y, hy⟩))

A point of the chart X|U ≅ (localModel)|W is simple in X iff its image is a simple point of the local model.

theorem AnalyticSpace.coeff_single_convEmbed_of_not_mem_range {n d : ℕ} (e : Fin d ↪ Fin n) (T : ↥(Analytic.Conv ℂ d)) {i : Fin n} (hi : i ∉ Set.range ⇑e) : (MvPowerSeries.coeff (Finsupp.single i 1)) ↑((Analytic.convEmbed ℂ e) T) = 0

A series in the base coordinates has no linear term in a fibre coordinate.

theorem AnalyticSpace.constantCoeff_convEmbed {n d : ℕ} (e : Fin d ↪ Fin n) (T : ↥(Analytic.Conv ℂ d)) : MvPowerSeries.constantCoeff ↑((Analytic.convEmbed ℂ e) T) = MvPowerSeries.constantCoeff ↑T

theorem AnalyticSpace.mem_maximalIdeal_stalk_iff_convAt {n : ℕ} (q : Kn ℂ n) (s : ↑((affine ℂ n).presheaf.stalk q)) : s ∈ IsLocalRing.maximalIdeal ↑((affine ℂ n).presheaf.stalk q) ↔ MvPowerSeries.constantCoeff ↑((taylorAffine ℂ n q) s) = 0

Membership in the maximal ideal of 𝒜_{ℂⁿ,q}, read through the Taylor isomorphism.

theorem AnalyticSpace.dlin_eq_coeff_convAt {n : ℕ} (q : Kn ℂ n) (s : ↑((affine ℂ n).presheaf.stalk q)) (i : Fin n) : (dlin ℂ n q) s i = (MvPowerSeries.coeff (Finsupp.single i 1)) ↑((taylorAffine ℂ n q) s)

The differential of a germ at q, read through the Taylor isomorphism: the linear coefficients of its series.

theorem AnalyticSpace.isRegularLocalRing_quotient_graphIdeal {n d : ℕ} (e : Fin d ↪ Fin n) (T : Fin n → ↥(Analytic.Conv ℂ d)) (hT0 : ∀ j ∉ Set.range ⇑e, MvPowerSeries.constantCoeff ↑(T j) = 0) : IsRegularLocalRing (↥(Analytic.Conv ℂ n) ⧸ Ideal.span (Set.range fun (j : { j : Fin n // j ∉ Set.range ⇑e }) => Analytic.convX ℂ ↑j - (Analytic.convEmbed ℂ e) (T ↑j)))

The quotient of 𝒪_n by the graph ideal (X_j − T_j(X ∘ e))_{j ∉ range e}, T_j(0) = 0, is a regular local ring (n − d germs of 𝔪 with independent differentials, isRegularLocalRing_quotient_span_range_and_ringKrullDim).

noncomputable def AnalyticSpace.stalkEquivQuotientModelIdealAt {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} (z : ↑↑(localModel K n G f).toPresheafedSpace) : ↑((localModel K n G f).presheaf.stalk z) ≃+* ↥(Analytic.Conv K n) ⧸ modelIdealAt G f z

The stalk of the local model at z is 𝒪_n / (f)_z.

Equations

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

theorem AnalyticSpace.mem_reg_iff_isRegularLocalRing_quotient {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {X : AnalyticSpace K} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} (e : (X.restrictOpen U).KIso ((localModel K n G f).restrictOpen W)) {y : ↑↑X.toPresheafedSpace} (hy : y ∈ U) : y ∈ X.regularLocus ↔ IsRegularLocalRing (↥(Analytic.Conv K n) ⧸ modelIdealAt G f ↑((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) ⟨y, hy⟩))

A point of the chart is simple iff 𝒪_n/(f)_z is regular at its image.

theorem AnalyticSpace.isReduced_stalk_restrictOpen_iff {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) : _root_.IsReduced ↑((X.restrictOpen U).presheaf.stalk x) ↔ _root_.IsReduced ↑(X.presheaf.stalk ↑x)

Reducedness of stalks passes to an open subspace and back.

theorem AnalyticSpace.isReduced_stalk_of_kIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) (h : _root_.IsReduced ↑(A.presheaf.stalk a)) : _root_.IsReduced ↑(B.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) a))

Reducedness of stalks transports forward along a K-isomorphism.

theorem AnalyticSpace.isRadical_modelIdealAt_of_isReduced {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {X : AnalyticSpace K} (hX : X.IsReduced) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} (e : (X.restrictOpen U).KIso ((localModel K n G f).restrictOpen W)) {y : ↑↑X.toPresheafedSpace} (hy : y ∈ U) : (modelIdealAt G f ↑((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) ⟨y, hy⟩)).IsRadical

On a reduced space, the ideal (f)_z of the model at the image of a point is radical.

theorem AnalyticSpace.isRegularLocalRing_quotient_comap_iff {K : Type} [RCLike K] {n : ℕ} (σ : ↥(Analytic.Conv K n) ≃ₐ[K] ↥(Analytic.Conv K n)) (J : Ideal ↥(Analytic.Conv K n)) : IsRegularLocalRing (↥(Analytic.Conv K n) ⧸ Ideal.comap σ J) ↔ IsRegularLocalRing (↥(Analytic.Conv K n) ⧸ J)

Transport of regularity of a quotient along σ: 𝒪_n / comap σ J ≅ 𝒪_n / J.

theorem AnalyticSpace.eventually_exists_localModel_pt {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : ∀ᶠ (y' : Fin n → K) in nhds 0, (∀ (j : Fin k), Analytic.evalSeries (↑(modelGens G f z j)) y' = 0) → ∃ (z' : ↑↑(localModel K n G f).toPresheafedSpace), ↑↑z' = { down := (↑↑z).down + y' }

Near a point z of the model, a point z.1.1 + y' of Kⁿ at which all equations vanish is a point of the model.

theorem AnalyticSpace.exists_mem_nhds_of_mem_nhds_localModel_restrict {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) {W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} {z : ↑↑(localModel K n G f).toPresheafedSpace} (hz : z ∈ W) {N : Set ↑↑((localModel K n G f).restrictOpen W).toPresheafedSpace} (hN : N ∈ nhds ⟨z, hz⟩) : ∃ O ∈ nhds ↑↑z, ∀ (z' : ↑↑(localModel K n G f).toPresheafedSpace) (hz' : z' ∈ W), ↑↑z' ∈ O → ⟨z', hz'⟩ ∈ N

A neighbourhood of a point of (localModel)|W contains all points of the model over an open of Kⁿ around the point.

theorem AnalyticSpace.exists_mem_nhds_of_mem_opens_localModel {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) {W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} {z : ↑↑(localModel K n G f).toPresheafedSpace} (hz : z ∈ W) : ∃ O ∈ nhds ↑↑z, ∀ (z' : ↑↑(localModel K n G f).toPresheafedSpace), ↑↑z' ∈ O → z' ∈ W

An open of the model containing z contains all points of the model over an open of Kⁿ around z.1.1.

theorem Analytic.mul_mem_of_mem_minimalPrimes_of_forall_mem {n : ℕ} {I P : Ideal ↥(Conv ℂ n)} (hI : I.IsRadical) (hP : P ∈ I.minimalPrimes) {h₀ : ↥(Conv ℂ n)} (hh₀ : ∀ Q ∈ I.minimalPrimes, Q ≠ P → h₀ ∈ Q) {F : ↥(Conv ℂ n)} (hF : F ∈ P) : F * h₀ ∈ I

The other components are avoided: for I radical, P a minimal prime of I and h₀ in every other minimal prime, F · h₀ ∈ I for every F ∈ P.

theorem Analytic.exists_mem_forall_minimalPrimes_ne_of_mem_minimalPrimes {n : ℕ} {I P : Ideal ↥(Conv ℂ n)} (hP : P ∈ I.minimalPrimes) : ∃ (h₀ : ↥(Conv ℂ n)), (∀ Q ∈ I.minimalPrimes, Q ≠ P → h₀ ∈ Q) ∧ h₀ ∉ P

A separating element for a minimal prime: h₀ in every other minimal prime and not in P.