Closed subspaces and labelled families descend along a gluing over a base

The resolution of an analytic space comes with its exceptional divisor, a locally finite family of smooth hypersurfaces with simple normal crossings ([Kol07, Definition 24]; [Kol07, Theorem 45, (3)]; [Wlo09, Theorem 2.0.1, (2)]). The sources glue the spaces only: Włodarczyk's Ṽ is "obtained by gluing Ṽ_i along Ṽ_i ∩ Ṽ_j", and the construction "commutes with local analytic isomorphisms" by construction [Wlo09, §4]; Kollár passes from the neighbourhoods of compact sets to their union [Kol07, 44]. That the exceptional families of the pieces glue with the spaces is left to the reader. This module proves the descent step for a gluing datum G : GlueOver X R π dom (Hironaka.AnalyticSpace.Glue.Over):

• Descent of one closed subspace (glueClosedSubspace): closed subspaces C i of the pieces whose restrictions to the gluing open subsets correspond under the transitions (CompatClosedSubspaces) descend to a closed subspace of G.gluedOver: the ideal sheaf with the stalk ideals comap ((ιGlued i).stalkMap y) ((C i).stalkIdeal y) at ιGlued i y, well defined because two representatives of one glued point are related through a transition (KGlueData.exists_of_ι_base_eq), the glue condition identifies the two legs' stalk maps, and compatibility identifies the two stalk ideals (pieceStalkIdeal_eq); its local generators are the pieces' carried through the open immersions (IsOpenImmersion.invApp). It pulls back to C i along every ιGlued i (comap_ιGlued_glueClosedSubspace), its support is the union of the images of the pieces' supports (support_glueClosedSubspace), and it is the only closed subspace with these pull-backs (ext_of_forall_comap_ιGlued_eq, existsUnique_comap_ιGlued_eq).
• The labelled family layer: families H i : κ i → ClosedSubspace (R i) with labels lab i : κ i → Λ, injective on every piece; memberOfLabel H lab i l is the member of the i-th family carrying the label l, the empty subspace ⊤ when the piece has no such member. LabelledCompat asks, label by label, for the compatibility of these members: the partner of a member across an overlap is fixed by its label, and a member absent from a neighbouring piece does not meet the overlap (the ⊤ convention on empty members). Then glueFamily : Λ → ClosedSubspace G.gluedOver glues label by label; it pulls back to the given members (comap_ιGlued_glueFamily_lab), has total support the union of the pieces' total supports (iUnion_support_glueFamily), is locally finite when the pieces' families are (locallyFinite_glueFamily), and is a simple-normal-crossings family (ClosedSubspace.IsSncFamily, Hironaka.AnalyticSpace.SncFamily) when the pieces' are (isSncFamily_glueFamily): the stalk clause at a glued point is the piece's, carried through the ring isomorphism of the open immersion's stalk map, the members through the point matched by the labels.

The label type is arbitrary here. In the resolution of an analytic space the pieces' exceptional families are the traces of one family indexed by the stages of a single run of the resolution functor on the disjoint union of the pieces, so the labelling is the identity (Hironaka.Resolution.Analytic.Kol07Thm45.CoproductGluedFamily), and LabelledCompat comes from the agreement of the stages across the overlaps (CoproductGluedFamilyCompat, ExhaustionChainFamilies, ResolutionOnMembers); the gluing along an exhaustion uses the chain form of Hironaka.Resolution.Analytic.Kol07Thm45.Glue.OverFamilyChain.

noncomputable def AnalyticSpace.GlueOver.restrictGlue {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i j : ι) (Z : (R i).ClosedSubspace) : Manifold.IdealSheaf ((R i).restrictOpen (glueOpens X R π dom i j)).𝒪

The restriction of a closed subspace Z of the i-th piece to the gluing open subset glueOpens i j, as an ideal sheaf of the restricted piece: the pull-back along the open inclusion (the trace on a part).

Equations

• AnalyticSpace.GlueOver.restrictGlue π dom i j Z = AnalyticSpace.QuotientSpace.comap (↑((R i).ofRestrict (AnalyticSpace.GlueOver.glueOpens X R π dom i j))) Z

def AnalyticSpace.GlueOver.CompatClosedSubspaces {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (C : (i : ι) → (R i).ClosedSubspace) : Prop

Compatibility of closed subspaces of the pieces: on every gluing open subset the transition t i j pulls the j-th subspace back to the i-th.

Equations

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

theorem AnalyticSpace.GlueOver.exists_t_eq_of_toFun_ιGlued_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {i j : ι} {y : ↑↑(R i).toPresheafedSpace} {y' : ↑↑(R j).toPresheafedSpace} (h : KLocallyRingedSpace.Hom.toFun (G.ιGlued i) y = KLocallyRingedSpace.Hom.toFun (G.ιGlued j) y') : ∃ (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace), ↑x = y ∧ ↑(KLocallyRingedSpace.Hom.toFun (G.t i j) x) = y'

Two representatives of one glued point are related through the transition (KGlueData.exists_of_ι_base_eq, Mathlib's ι_eq_iff_rel underneath).

theorem AnalyticSpace.GlueOver.ofRestrict_comp_ιGlued {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i j : ι) : CategoryTheory.CategoryStruct.comp ↑((R i).ofRestrict (glueOpens X R π dom i j)) ↑(G.ιGlued i) = CategoryTheory.CategoryStruct.comp (↑(G.t i j)) (CategoryTheory.CategoryStruct.comp ↑((R j).ofRestrict (glueOpens X R π dom j i)) ↑(G.ιGlued j))

The glue condition of the gluing over X, on the pieces: ofRestrict ≫ ιGlued i and t i j ≫ ofRestrict ≫ ιGlued j agree on the gluing open subset.

theorem AnalyticSpace.GlueOver.stalkSpecializes_comp_eq_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] {Y : TopCat} (F : TopCat.Presheaf C Y) {x y : ↑Y} (hxy : x = y) (h₁ : x ⤳ y) (h₂ : y ⤳ x) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h₁) (F.stalkSpecializes h₂) = CategoryTheory.CategoryStruct.id (F.stalk y)

Two stalk-specialization maps along an equality of points compose to the identity.

theorem AnalyticSpace.GlueOver.comap_eq_of_stalk_square {A B A' B' S : CommRingCat} (α : A ⟶ A') (β : B ⟶ B') (a : A' ⟶ S) (b : B' ⟶ S) (σ : B ⟶ A) (σ' : A ⟶ B) (hσ : CategoryTheory.CategoryStruct.comp σ σ' = CategoryTheory.CategoryStruct.id B) (ha : Function.Bijective ⇑(CommRingCat.Hom.hom a)) (hb : Function.Bijective ⇑(CommRingCat.Hom.hom b)) (hsq : CategoryTheory.CategoryStruct.comp α a = CategoryTheory.CategoryStruct.comp σ' (CategoryTheory.CategoryStruct.comp β b)) (I : Ideal ↑A') (J : Ideal ↑B') (hIJ : Ideal.map (CommRingCat.Hom.hom a) I = Ideal.map (CommRingCat.Hom.hom b) J) : Ideal.comap (CommRingCat.Hom.hom σ) (Ideal.comap (CommRingCat.Hom.hom α) I) = Ideal.comap (CommRingCat.Hom.hom β) J

The ideal algebra of representative independence: in a commutative square α ≫ a = σ' ≫ β ≫ b with a, b bijective and σ ≫ σ' = 𝟙, ideals I, J with the same image under a, b pull back along α, β to ideals identified by σ.

noncomputable def AnalyticSpace.GlueOver.pieceStalkIdeal {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (i : ι) (y : ↑↑(R i).toPresheafedSpace) : Ideal ↑(G.gluedOver.presheaf.stalk (KLocallyRingedSpace.Hom.toFun (G.ιGlued i) y))

The stalk ideal of the i-th subspace, read on the glued space at the image point.

Equations

• G.pieceStalkIdeal C i y = Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(G.ιGlued i)) y)) (Manifold.IdealSheaf.stalkIdeal (C i) y)

theorem AnalyticSpace.GlueOver.pieceStalkIdeal_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) {i j : ι} {y : ↑↑(R i).toPresheafedSpace} {y' : ↑↑(R j).toPresheafedSpace} (h : KLocallyRingedSpace.Hom.toFun (G.ιGlued i) y = KLocallyRingedSpace.Hom.toFun (G.ιGlued j) y') : Ideal.comap (CommRingCat.Hom.hom (G.gluedOver.presheaf.stalkSpecializes ⋯)) (G.pieceStalkIdeal C i y) = G.pieceStalkIdeal C j y'

Representative independence: the piece stalk ideals of two representatives of one glued point agree under the canonical identification of the stalks.

noncomputable def AnalyticSpace.GlueOver.gluedRep {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (z : ↑↑G.gluedOver.toPresheafedSpace) : (i : ι) × ↑↑(R i).toPresheafedSpace

A representative (i, y) of a point of the glued space.

Equations

• G.gluedRep z = ⟨⋯.choose, ⋯.choose⟩

theorem AnalyticSpace.GlueOver.toFun_ιGlued_gluedRep {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (z : ↑↑G.gluedOver.toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (G.ιGlued (G.gluedRep z).fst) (G.gluedRep z).snd = z

The chosen representative represents: ιGlued (gluedRep z).1 sends (gluedRep z).2 to z.

noncomputable def AnalyticSpace.GlueOver.gluedStalkIdeal {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (z : ↑↑G.gluedOver.toPresheafedSpace) : Ideal ↑(G.gluedOver.presheaf.stalk z)

The glued stalk ideal at z: the piece stalk ideal of a representative, carried to z.

Equations

• G.gluedStalkIdeal C z = Ideal.comap (CommRingCat.Hom.hom (G.gluedOver.presheaf.stalkSpecializes ⋯)) (G.pieceStalkIdeal C (G.gluedRep z).fst (G.gluedRep z).snd)

theorem AnalyticSpace.GlueOver.gluedStalkIdeal_toFun_ιGlued {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) (i : ι) (y : ↑↑(R i).toPresheafedSpace) : G.gluedStalkIdeal C (KLocallyRingedSpace.Hom.toFun (G.ιGlued i) y) = G.pieceStalkIdeal C i y

The glued stalk ideal at the image of y is the i-th piece stalk ideal.

theorem AnalyticSpace.GlueOver.germ_map_eqToHom {Y : TopCat} (F : TopCat.Presheaf CommRingCat Y) {U V : TopologicalSpace.Opens ↑Y} (e : Opposite.op U = Opposite.op V) (x : ↑Y) (hx : x ∈ V) (s : ↑(F.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (F.germ V x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom e))) s) = (CategoryTheory.ConcreteCategory.hom (F.germ U x ⋯)) s

A germ of a section transported along an identity of open subsets is the germ of the section.

theorem AnalyticSpace.GlueOver.stalkMap_germ_invApp {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] (V : TopologicalSpace.Opens ↑X.toTopCat) (b : ↑X.toTopCat) (hb : b ∈ V) (hb' : (CategoryTheory.ConcreteCategory.hom f.base) b ∈ (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj V) (s : ↑(X.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f b)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj V) ((CategoryTheory.ConcreteCategory.hom f.base) b) hb')) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f V)) s)) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V b hb)) s

Along an open immersion, the stalk map carries the germ of the transported section (invApp) to the germ of the section.

theorem AnalyticSpace.GlueOver.hasLocalGenerators_gluedStalkIdeal {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) : Manifold.IdealSheaf.HasLocalGenerators (G.gluedStalkIdeal C)

The glued stalk ideals have local generators: a piece's generators near the representative, carried to the glued space through the open immersion's invApp, generate at every point of the image neighbourhood (stalkMap_germ_invApp; the stalk map is bijective).

noncomputable def AnalyticSpace.GlueOver.glueClosedSubspace {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) : G.gluedOver.ClosedSubspace

The glued closed subspace of compatible closed subspaces of the pieces.

Equations

• G.glueClosedSubspace C hc = Manifold.IdealSheaf.ofStalks G.gluedOver.𝒪 (G.gluedStalkIdeal C) ⋯

theorem AnalyticSpace.GlueOver.comap_ιGlued_glueClosedSubspace {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) (i : ι) : QuotientSpace.comap (↑(G.ιGlued i)) (G.glueClosedSubspace C hc) = C i

The glued closed subspace pulls back along the open immersion of every piece to the given one.

theorem AnalyticSpace.GlueOver.preimage_support_glueClosedSubspace {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) (i : ι) : ⇑(CategoryTheory.ConcreteCategory.hom (↑(G.ιGlued i)).base) ⁻¹' Manifold.IdealSheaf.support (G.glueClosedSubspace C hc) = Manifold.IdealSheaf.support (C i)

The preimage of the glued support under the i-th immersion is the i-th support.

theorem AnalyticSpace.GlueOver.ext_of_forall_comap_ιGlued_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {E E' : G.gluedOver.ClosedSubspace} (h : ∀ (i : ι), QuotientSpace.comap (↑(G.ιGlued i)) E = QuotientSpace.comap (↑(G.ιGlued i)) E') : E = E'

Uniqueness of descent: two closed subspaces of the glued space with the same pull-backs to every piece are equal (the pieces cover, and the stalk maps of the open immersions are isomorphisms).

theorem AnalyticSpace.GlueOver.existsUnique_comap_ιGlued_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) : ∃! E : G.gluedOver.ClosedSubspace, ∀ (i : ι), QuotientSpace.comap (↑(G.ιGlued i)) E = C i

Existence and uniqueness of descent: compatible closed subspaces of the pieces are the pull-backs of exactly one closed subspace of the glued space.

theorem AnalyticSpace.GlueOver.support_glueClosedSubspace {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (C : (i : ι) → (R i).ClosedSubspace) (hc : G.CompatClosedSubspaces C) : Manifold.IdealSheaf.support (G.glueClosedSubspace C hc) = ⋃ (i : ι), KLocallyRingedSpace.Hom.toFun (G.ιGlued i) '' Manifold.IdealSheaf.support (C i)

The support of the glued closed subspace is the union of the images of the pieces' supports.

The family layer: labelled families of closed subspaces glue

The hypothesis is the labelled form: a label type Λ, per-piece labels lab i : κ i → Λ injective on each piece, and for every label the members carrying it compatible across the transitions, with the empty subspace ⊤ standing in where a piece has no member with that label (so a member absent from a neighbouring piece must not meet the overlap: the totality clause, and the convention on empty members).

theorem AnalyticSpace.GlueOver.support_unitIdeal {K : Type} [RCLike K] {Y : AnalyticSpace K} : Manifold.IdealSheaf.support ⊤ = ∅

The unit ideal sheaf (the empty closed subspace) has empty support.

noncomputable def AnalyticSpace.GlueOver.memberOfLabel {K : Type} [RCLike K] {ι : Type u} {R : ι → AnalyticSpace K} {Λ : Type u} {κ : ι → Type u} (H : (i : ι) → κ i → (R i).ClosedSubspace) (lab : (i : ι) → κ i → Λ) (i : ι) (l : Λ) : (R i).ClosedSubspace

The member of the i-th family carrying the label l; the empty subspace ⊤ when no member of the piece carries l.

Equations

• AnalyticSpace.GlueOver.memberOfLabel H lab i l = if h : ∃ (k : κ i), lab i k = l then H i h.choose else ⊤

theorem AnalyticSpace.GlueOver.memberOfLabel_lab {K : Type} [RCLike K] {ι : Type u} {R : ι → AnalyticSpace K} {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) (i : ι) (k : κ i) : memberOfLabel H lab i (lab i k) = H i k

With injective labels, the member of the label lab i k is the member k.

theorem AnalyticSpace.GlueOver.memberOfLabel_of_not_exists {K : Type} [RCLike K] {ι : Type u} {R : ι → AnalyticSpace K} {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} {i : ι} {l : Λ} (h : ¬∃ (k : κ i), lab i k = l) : memberOfLabel H lab i l = ⊤

A label carried by no member of the piece gives the empty subspace ⊤.

theorem AnalyticSpace.GlueOver.support_memberOfLabel_subset {K : Type} [RCLike K] {ι : Type u} {R : ι → AnalyticSpace K} {Λ : Type u} {κ : ι → Type u} (H : (i : ι) → κ i → (R i).ClosedSubspace) (lab : (i : ι) → κ i → Λ) (i : ι) (l : Λ) : Manifold.IdealSheaf.support (memberOfLabel H lab i l) ⊆ ⋃ (k : κ i), Manifold.IdealSheaf.support (H i k)

The support of a label's member lies in the piece's total support.

theorem AnalyticSpace.GlueOver.iUnion_support_memberOfLabel {K : Type} [RCLike K] {ι : Type u} {R : ι → AnalyticSpace K} {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) (i : ι) : ⋃ (l : Λ), Manifold.IdealSheaf.support (memberOfLabel H lab i l) = ⋃ (k : κ i), Manifold.IdealSheaf.support (H i k)

The labels' members have the piece's total support: every member appears at its own label, and absent labels contribute the empty set.

theorem AnalyticSpace.GlueOver.exists_of_mem_support_memberOfLabel {K : Type} [RCLike K] {ι : Type u} {R : ι → AnalyticSpace K} {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) {i : ι} {l : Λ} {y : ↑↑(R i).toPresheafedSpace} (h : y ∈ Manifold.IdealSheaf.support (memberOfLabel H lab i l)) : ∃ (k : κ i), lab i k = l ∧ y ∈ Manifold.IdealSheaf.support (H i k)

A point in the support of a label's member lies in the support of a member carrying that label.

def AnalyticSpace.GlueOver.LabelledCompat {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) {Λ : Type u} {κ : ι → Type u} (H : (i : ι) → κ i → (R i).ClosedSubspace) (lab : (i : ι) → κ i → Λ) : Prop

Labelled compatibility of families: for every label, the members carrying it are compatible closed subspaces of the pieces (⊤ where a piece has no member with that label).

Equations

• G.LabelledCompat H lab = ∀ (l : Λ), G.CompatClosedSubspaces fun (i : ι) => AnalyticSpace.GlueOver.memberOfLabel H lab i l

noncomputable def AnalyticSpace.GlueOver.glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} (H : (i : ι) → κ i → (R i).ClosedSubspace) (lab : (i : ι) → κ i → Λ) (hc : G.LabelledCompat H lab) : Λ → G.gluedOver.ClosedSubspace

The glued family, indexed by the labels: the label l glues the members carrying it.

Equations

• G.glueFamily H lab hc l = G.glueClosedSubspace (fun (i : ι) => AnalyticSpace.GlueOver.memberOfLabel H lab i l) ⋯

theorem AnalyticSpace.GlueOver.comap_ιGlued_glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hc : G.LabelledCompat H lab) (l : Λ) (i : ι) : QuotientSpace.comap (↑(G.ιGlued i)) (G.glueFamily H lab hc l) = memberOfLabel H lab i l

The glued member with label l pulls back along ιGlued i to the i-th piece's member of that label (⊤ when the piece has none).

theorem AnalyticSpace.GlueOver.comap_ιGlued_glueFamily_lab {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) (hc : G.LabelledCompat H lab) (i : ι) (k : κ i) : QuotientSpace.comap (↑(G.ιGlued i)) (G.glueFamily H lab hc (lab i k)) = H i k

Pulled back to the i-th piece, the glued member with label lab i k is the member k.

theorem AnalyticSpace.GlueOver.preimage_support_glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hc : G.LabelledCompat H lab) (l : Λ) (i : ι) : ⇑(CategoryTheory.ConcreteCategory.hom (↑(G.ιGlued i)).base) ⁻¹' Manifold.IdealSheaf.support (G.glueFamily H lab hc l) = Manifold.IdealSheaf.support (memberOfLabel H lab i l)

The preimage under ιGlued i of a glued member's support is the support of the piece's member of that label.

theorem AnalyticSpace.GlueOver.support_glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hc : G.LabelledCompat H lab) (l : Λ) : Manifold.IdealSheaf.support (G.glueFamily H lab hc l) = ⋃ (i : ι), KLocallyRingedSpace.Hom.toFun (G.ιGlued i) '' Manifold.IdealSheaf.support (memberOfLabel H lab i l)

The support of a glued member is the union of the images of the pieces' members of that label.

theorem AnalyticSpace.GlueOver.iUnion_support_glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) (hc : G.LabelledCompat H lab) : ⋃ (l : Λ), Manifold.IdealSheaf.support (G.glueFamily H lab hc l) = ⋃ (i : ι), KLocallyRingedSpace.Hom.toFun (G.ιGlued i) '' ⋃ (k : κ i), Manifold.IdealSheaf.support (H i k)

The total support of the glued family is the union of the images of the pieces' total supports.

theorem AnalyticSpace.GlueOver.locallyFinite_glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) (hc : G.LabelledCompat H lab) (hfin : ∀ (i : ι), LocallyFinite fun (k : κ i) => Manifold.IdealSheaf.support (H i k)) : LocallyFinite fun (l : Λ) => Manifold.IdealSheaf.support (G.glueFamily H lab hc l)

Local finiteness of the glued family, from local finiteness on every piece.

theorem AnalyticSpace.GlueOver.isSncFamily_glueFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] {Λ : Type u} {κ : ι → Type u} {H : (i : ι) → κ i → (R i).ClosedSubspace} {lab : (i : ι) → κ i → Λ} (hlab : ∀ (i : ι), Function.Injective (lab i)) (hc : G.LabelledCompat H lab) (hsnc : ∀ (i : ι), ClosedSubspace.IsSncFamily (H i)) : ClosedSubspace.IsSncFamily (G.glueFamily H lab hc)

Simple normal crossings glue ([Kol07, Definition 24], the local form of the divisor with simple normal crossings; ClosedSubspace.IsSncFamily): the glued family of labelled simple-normal-crossings families is one: the stalk data at a glued point are the piece's, carried through the stalk isomorphism of the open immersion; the glued members through the point are the piece's members through its representative, matched by the labels.