Gluing over a base from transitions: uniqueness gives the cocycle, continuity gives Hausdorffness

In Włodarczyk's gluing of local desingularizations [Wlo09, §4] the embeddings (V_i ∩ V_j)~ → Ṽ_i are the unique lifts of the identity of the overlap (the desingularization of a germ is independent of the choice of ambient manifold), so they satisfy the cocycle identity automatically; and "let Ṽ be a manifold obtained by gluing Ṽ_i along Ṽ_i ∩ Ṽ_j" takes the Hausdorffness of Ṽ for granted. Both are proved here once, for every gluing over a base whose transitions lie over the base:

• KLocallyRingedSpace.toFun_restrictOpenIncl_val: the inclusion of open subspaces on points;
• Glue.KGlueCore.isIso_tRes_of_comp_eq_id: when the transitions of a gluing core are mutually inverse, their restrictions to the meets (tRes) are isomorphisms;
• GlueOver.isClosed_transitionGraph_overData, t2Space_overData_of_compat: the transition graphs are closed, the glued space is Hausdorff;
• GlueOver.exists_glueOver_of_transitions: a GlueOver from transitions that are isomorphisms over X, unique among such on the points over an open subset of the base;
• GlueOver.toFun_π_t_eq, t_inter_of_compat: the point-level content of compat, a transition preserves the fibre over X, hence maps the points over dom k to points over dom k;
• GlueOver.t_comp_t_eq_id_of_uniq, t_id_of_uniq: transitions that are isomorphisms over X, unique among such on the preimage open subsets, are mutually inverse and the identity on the diagonal.

exists_glueOver_of_transitions is how the gluing datum of the local resolutions is built (Hironaka.Resolution.Analytic.Kol07Thm45.PieceGlueDatum, PieceGlueIndep). Not in the sources as separate statements.

theorem AnalyticSpace.KLocallyRingedSpace.toFun_restrictOpenIncl_val {K : Type} [RCLike K] (A : KLocallyRingedSpace K) {U U' : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} (h : U ≤ U') (x : ↑↑(A.restrictOpen U).toPresheafedSpace) : ↑(Hom.toFun (A.restrictOpenIncl h) x) = ↑x

The inclusion of open subspaces is the identity on points.

theorem AnalyticSpace.Glue.KGlueCore.isIso_tRes_of_comp_eq_id {K : Type} [RCLike K] (D : KGlueCore K) (hinv : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.t i j) (D.t j i) = CategoryTheory.CategoryStruct.id ((D.Y i).restrictOpen (D.W i j))) (i j k : D.J) : CategoryTheory.IsIso (D.tRes i j k)

When the transitions are mutually inverse, their restrictions to the meets are isomorphisms: the inverse of tRes i j k is tRes j i k between the commuted meets.

theorem AnalyticSpace.GlueOver.toFun_π_t_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (compat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (i j : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (π j) ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) = KLocallyRingedSpace.Hom.toFun (π i) ↑x

compat at the point level: a transition preserves the fibre over X.

theorem AnalyticSpace.GlueOver.t_inter_of_compat {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (compat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace) (hx : ↑x ∈ glueOpens X R π dom i k) : ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) ∈ glueOpens X R π dom j k

The t_inter field from compat: the transition maps the points over dom k to points over dom k.

theorem AnalyticSpace.GlueOver.t_comp_t_eq_id_of_uniq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (hiso : ∀ (i j : ι), CategoryTheory.IsIso (t i j)) (compat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (huniq : ∀ (i j : ι), ∀ O ≤ dom i ⊓ dom j, ∀ (s s' : (R i).restrictOpen (overOpens π i O) ⟶ (R j).restrictOpen (overOpens π j O)), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (overOpens π i O)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((R j).ofRestrict (overOpens π j O))) (π j) → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (overOpens π i O)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' ((R j).ofRestrict (overOpens π j O))) (π j) → s = s') (i j : ι) : CategoryTheory.CategoryStruct.comp (t i j) (t j i) = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i j))

Transitions that are isomorphisms over X, unique among such on the points over an open of the base, are mutually inverse.

theorem AnalyticSpace.GlueOver.t_id_of_uniq {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (hiso : ∀ (i j : ι), CategoryTheory.IsIso (t i j)) (compat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (huniq : ∀ (i j : ι), ∀ O ≤ dom i ⊓ dom j, ∀ (s s' : (R i).restrictOpen (overOpens π i O) ⟶ (R j).restrictOpen (overOpens π j O)), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (overOpens π i O)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((R j).ofRestrict (overOpens π j O))) (π j) → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (overOpens π i O)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' ((R j).ofRestrict (overOpens π j O))) (π j) → s = s') (i : ι) : t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))

Transitions that are isomorphisms over X, unique among such, are the identity on the diagonal: the t_id field.

The transition graphs are closed, the glued space is Hausdorff

theorem AnalyticSpace.GlueOver.transitionGraph_overData {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (t_id : ∀ (i : ι), t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))) (t_inter : ∀ (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace), ↑x ∈ glueOpens X R π dom i k → ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) ∈ glueOpens X R π dom j k) (cocycle : ∀ (i j k : (overCore X R π dom hrange t t_id t_inter).J), CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes i j k) (CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes j k i) ((overCore X R π dom hrange t t_id t_inter).tRes k i j)) = CategoryTheory.CategoryStruct.id (((overCore X R π dom hrange t t_id t_inter).Y i).restrictOpen ((overCore X R π dom hrange t t_id t_inter).W i j ⊓ (overCore X R π dom hrange t t_id t_inter).W i k))) (i j : ι) : Glue.transitionGraph (overData X R π dom hrange t t_id t_inter cocycle).topGlueData i j = Set.range fun (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace) => (↑x, ↑(KLocallyRingedSpace.Hom.toFun (t i j) x))

The transition graph of the gluing over X, as the graph of the transition on points.

theorem AnalyticSpace.GlueOver.isClosed_transitionGraph_overData {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (t_id : ∀ (i : ι), t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))) (t_inter : ∀ (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace), ↑x ∈ glueOpens X R π dom i k → ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) ∈ glueOpens X R π dom j k) (hcompat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (cocycle : ∀ (i j k : (overCore X R π dom hrange t t_id t_inter).J), CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes i j k) (CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes j k i) ((overCore X R π dom hrange t t_id t_inter).tRes k i j)) = CategoryTheory.CategoryStruct.id (((overCore X R π dom hrange t t_id t_inter).Y i).restrictOpen ((overCore X R π dom hrange t t_id t_inter).W i j ⊓ (overCore X R π dom hrange t t_id t_inter).W i k))) (i j : ι) : IsClosed (Glue.transitionGraph (overData X R π dom hrange t t_id t_inter cocycle).topGlueData i j)

The transition graph is closed: a limit (p, q) of graph points satisfies π_i p = π_j q (compat, continuity, X Hausdorff), so p and q lie over the overlap, where the graph is the closed graph of the continuous transition into the Hausdorff piece.

theorem AnalyticSpace.GlueOver.t2Space_overData_of_compat {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (t_id : ∀ (i : ι), t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))) (t_inter : ∀ (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace), ↑x ∈ glueOpens X R π dom i k → ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) ∈ glueOpens X R π dom j k) (hcompat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (cocycle : ∀ (i j k : (overCore X R π dom hrange t t_id t_inter).J), CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes i j k) (CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes j k i) ((overCore X R π dom hrange t t_id t_inter).tRes k i j)) = CategoryTheory.CategoryStruct.id (((overCore X R π dom hrange t t_id t_inter).Y i).restrictOpen ((overCore X R π dom hrange t t_id t_inter).W i j ⊓ (overCore X R π dom hrange t t_id t_inter).W i k))) : T2Space ↑(overData X R π dom hrange t t_id t_inter cocycle).glued.toTopCat

A gluing over X whose transitions lie over X glues to a Hausdorff space (the closed-graph criterion t2Space_of_isClosed_transitionGraph).

The gluing datum from transitions

theorem AnalyticSpace.GlueOver.exists_glueOver_of_transitions {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (hiso : ∀ (i j : ι), CategoryTheory.IsIso (t i j)) (hcompat : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)) (huniq : ∀ (i j : ι), ∀ O ≤ dom i ⊓ dom j, ∀ (s s' : (R i).restrictOpen (overOpens π i O) ⟶ (R j).restrictOpen (overOpens π j O)), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (overOpens π i O)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((R j).ofRestrict (overOpens π j O))) (π j) → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (overOpens π i O)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' ((R j).ofRestrict (overOpens π j O))) (π j) → s = s') : Nonempty (X.GlueOver R π dom)

The gluing datum from transitions ([Wlo09, §4], with the uniqueness of the lifts): transitions that are isomorphisms over X on the gluing open subsets, unique among such on the points over every open subset of the base contained in the overlap, form a GlueOver: t_id and the cocycle identity by uniqueness (against the identity), t_inter from compat, Hausdorffness by t2Space_overData_of_compat. The cocycle's composite is an isomorphism over X by isIso_tRes_of_comp_eq_id.