The partner of a member of an exceptional family across a gluing transition

Across the transition ψ : (R i)|_{glueOpens i j} ≅ (R j)|_{glueOpens j i} of a gluing datum (GlueOver, Hironaka.AnalyticSpace.Glue.Over), the members of two simple-normal-crossings families H₁, H₂ of closed subspaces of the pieces (ClosedSubspace.IsSncFamily, Hironaka.AnalyticSpace.SncFamily) are matched by a label e : Λ₁ → Λ₂. In the resolution of an analytic space the label is the stage of the blow-up sequence at which a member is created: the blow-up sequences of two pieces have the same centres on the overlap at every stage Kol07, Proposition 37, (37.2), so the exceptional divisors created at one stage correspond. Given the labelled identity locally, an open subset around every point on which the pull-back along ψ of the trace of H₂ (e σ) is the trace of H₁ σ, it holds on the whole gluing open subset (comap_restrict_eq_of_forall_exists_local: equality of closed subspaces is stalkwise), and for a member with non-empty trace the partner e σ is the unique member of H₂ whose pull-back is that trace (existsUnique_partner_of_forall_exists_local_label), because two members of a simple-normal-crossings family with the same stalk ideal at a common point of their supports are the same member (IsSncFamily.eq_of_stalkIdeal_eq_of_mem_support): the chart at the point assigns each member through it one parameter of a regular system of parameters, distinct members distinct parameters, and two parameters of a regular system generating the same principal ideal coincide, their classes in 𝔪/𝔪² being linearly independent over the residue field (IsRegularLocalRing.index_eq_of_span_singleton_eq_of_span_range_eq, from IsRegularLocalRing.linearIndependent_toCotangent_of_span_eq of Hironaka.Algebra.RegularSmooth.ParameterCount).

A label-free local correspondence does not determine the partner when members are disconnected: for four disjoint lines A, A', B, B' and the families H₁ = {A ∪ B, A' ∪ B'}, H₂ = {A ∪ B', A' ∪ B}, the local correspondences match A ∪ B to A ∪ B' near A and to A' ∪ B near B. Hence the partner is read as the label.

The two statements about a gluing datum have no code users outside this module: the chain form of Hironaka.Resolution.Analytic.Kol07Thm45.Glue.OverFamilyChain restates them in the restrictOpen spelling of the traces (ClosedSubspace.comap_eq_of_forall_exists_local, existsUnique_comap_eq_of_forall_exists_local), which is what the gluing along an exhaustion uses. The rigidity lemma IsSncFamily.eq_of_stalkIdeal_eq_of_mem_support is used there too.

theorem IsRegularLocalRing.index_eq_of_span_singleton_eq_of_span_range_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {m : ℕ} (z : Fin m → R) (hspan : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R) (hdim : ↑m = ringKrullDim R) {a b : Fin m} (h : Ideal.span {z a} = Ideal.span {z b}) : a = b

Two members of a regular system of parameters of a regular local ring generating the same principal ideal are the same member (the classes of a regular system of parameters in 𝔪/𝔪² are linearly independent over the residue field, IsRegularLocalRing.linearIndependent_toCotangent_of_span_eq): if z a = r * z b, the classes of z a and z b in 𝔪/𝔪² are proportional over the residue field, against their linear independence.

theorem AnalyticSpace.ClosedSubspace.IsSncFamily.isRegularLocalRing_stalk_of_isSncFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) (x : ↑↑X.toPresheafedSpace) : IsRegularLocalRing ↑(X.presheaf.stalk x)

The stalks of a space carrying a simple-normal-crossings family are regular local rings (the ∀ x clause of IsSncFamily).

theorem AnalyticSpace.ClosedSubspace.IsSncFamily.eq_of_stalkIdeal_eq_of_mem_support {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) {σ τ : ι} {x : ↑↑X.toPresheafedSpace} (hσ : x ∈ Manifold.IdealSheaf.support (H σ)) (hτ : x ∈ Manifold.IdealSheaf.support (H τ)) (hst : Manifold.IdealSheaf.stalkIdeal (H σ) x = Manifold.IdealSheaf.stalkIdeal (H τ) x) : σ = τ

Rigidity of the members of a simple-normal-crossings family at one point (Kol07, Definition 24): two members of the family with the same stalk ideal at a common point of their supports are the same member: the chart at the point assigns each member through it one parameter of the regular system of parameters, injectively.

theorem AnalyticSpace.ClosedSubspace.mem_support_of_comap_restrictInclusion {K : Type} [RCLike K] {X : AnalyticSpace K} {A : X.ClosedSubspace} (S : Set ↑↑X.toPresheafedSpace) {p : ↑↑(X.restrictSet S).toPresheafedSpace} (hp : p ∈ Manifold.IdealSheaf.support (A.comap (X.restrictInclusion S))) : ↑p ∈ Manifold.IdealSheaf.support A

A point of the support of a trace on an open subspace lies in the support of the member (QuotientSpace.cosupport_comap).

theorem AnalyticSpace.ClosedSubspace.stalkIdeal_eq_of_comap_restrictInclusion_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {A B : X.ClosedSubspace} (S : Set ↑↑X.toPresheafedSpace) (h : A.comap (X.restrictInclusion S) = B.comap (X.restrictInclusion S)) (p : ↑↑(X.restrictSet S).toPresheafedSpace) : Manifold.IdealSheaf.stalkIdeal A ↑p = Manifold.IdealSheaf.stalkIdeal B ↑p

Two closed subspaces with the same trace on an open subspace have the same stalk ideal at every point of the open subset: the stalk map of the open inclusion is an isomorphism (KLocallyRingedSpace.isIso_ofRestrict_stalkMap, QuotientSpace.stalkIdeal_comap).

theorem AnalyticSpace.ClosedSubspace.IsSncFamily.eq_of_comap_restrictInclusion_eq_of_nonempty {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) (S : Set ↑↑X.toPresheafedSpace) {σ τ : ι} (heq : (H σ).comap (X.restrictInclusion S) = (H τ).comap (X.restrictInclusion S)) (hne : (Manifold.IdealSheaf.support ((H σ).comap (X.restrictInclusion S))).Nonempty) : σ = τ

Two members of a simple-normal-crossings family with the same trace on an open subspace, the trace non-empty, are the same member.

theorem AnalyticSpace.GlueOver.comap_restrict_eq_of_forall_exists_local {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Λ₁ Λ₂ : Type u} (i j : ι) (H₁ : Λ₁ → (R i).ClosedSubspace) (H₂ : Λ₂ → (R j).ClosedSubspace) (ψ : (R i).restrictSet ↑(glueOpens X R π dom i j) ⟶ (R j).restrictSet ↑(glueOpens X R π dom j i)) (e : Λ₁ → Λ₂) (hloc : ∀ (x : ↑↑((R i).restrictSet ↑(glueOpens X R π dom i j)).toPresheafedSpace), ∃ (V : Set ↑↑((R i).restrictSet ↑(glueOpens X R π dom i j)).toPresheafedSpace), IsOpen V ∧ x ∈ V ∧ ∀ (σ : Λ₁), (((H₂ (e σ)).comap ((R j).restrictInclusion ↑(glueOpens X R π dom j i))).comap ψ).comap (((R i).restrictSet ↑(glueOpens X R π dom i j)).restrictInclusion V) = ((H₁ σ).comap ((R i).restrictInclusion ↑(glueOpens X R π dom i j))).comap (((R i).restrictSet ↑(glueOpens X R π dom i j)).restrictInclusion V)) (σ : Λ₁) : ((H₂ (e σ)).comap ((R j).restrictInclusion ↑(glueOpens X R π dom j i))).comap ψ = (H₁ σ).comap ((R i).restrictInclusion ↑(glueOpens X R π dom i j))

The labelled identity is local ([Kol07, Proposition 37, (37.2)]: the centres of the blow-up sequences of two pieces agree on the overlap at every stage): the pull-back along the transition of the trace of the label-e σ member of H₂ is the trace of H₁ σ on the whole gluing open subset as soon as it is so near every point, for every σ, because equality of closed subspaces is stalkwise. No simple-normal-crossings hypothesis.

theorem AnalyticSpace.GlueOver.existsUnique_partner_of_forall_exists_local_label {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Λ₁ Λ₂ : Type u} (i j : ι) (H₁ : Λ₁ → (R i).ClosedSubspace) (H₂ : Λ₂ → (R j).ClosedSubspace) (h₂ : ClosedSubspace.IsSncFamily H₂) (ψ : (R i).restrictSet ↑(glueOpens X R π dom i j) ⟶ (R j).restrictSet ↑(glueOpens X R π dom j i)) (hψ : CategoryTheory.IsIso ψ) (e : Λ₁ → Λ₂) (hloc : ∀ (x : ↑↑((R i).restrictSet ↑(glueOpens X R π dom i j)).toPresheafedSpace), ∃ (V : Set ↑↑((R i).restrictSet ↑(glueOpens X R π dom i j)).toPresheafedSpace), IsOpen V ∧ x ∈ V ∧ ∀ (σ : Λ₁), (((H₂ (e σ)).comap ((R j).restrictInclusion ↑(glueOpens X R π dom j i))).comap ψ).comap (((R i).restrictSet ↑(glueOpens X R π dom i j)).restrictInclusion V) = ((H₁ σ).comap ((R i).restrictInclusion ↑(glueOpens X R π dom i j))).comap (((R i).restrictSet ↑(glueOpens X R π dom i j)).restrictInclusion V)) (σ : Λ₁) (hσ : (Manifold.IdealSheaf.support ((H₁ σ).comap ((R i).restrictInclusion ↑(glueOpens X R π dom i j)))).Nonempty) : ∃! τ : Λ₂, ((H₂ τ).comap ((R j).restrictInclusion ↑(glueOpens X R π dom j i))).comap ψ = (H₁ σ).comap ((R i).restrictInclusion ↑(glueOpens X R π dom i j))

The partner is the label, unique among the members of H₂: for a member of H₁ with non-empty trace on the gluing open subset, e σ is the unique member of H₂ whose trace pulls back along the transition to the trace of H₁ σ: existence by comap_restrict_eq_of_forall_exists_local, uniqueness by the rigidity of the simple-normal-crossings family fun τ => comap ψ (trace of H₂ τ) (isSncFamily_comap_of_isIso, IsSncFamily.comap_ofRestrict) at a point of the non-empty support.