The constraint sets and the shrinking of the pieces

For the local data D (Hironaka.AnalyticSpace.Glue.Setup) and the uniqueness hypothesis huniq (Huniq, defined here as a predicate) of the gluing theorem for complexifications BW59, Proposition 1: the cocycle neighbourhoods N_ijk ⊆ Y_i (chosen from exists_cocycle_nhd, Hironaka.AnalyticSpace.Glue.Cocycle), made empty when the triple overlap U_i ∩ U_j ∩ U_k is empty (nhd'); the closed pair boundaries closure Γ_ij ∖ Γ_ij and the closures of the triple sets {(y, φ_ij y, φ_ik y) : y ∈ Ω_ij ∩ Ω_ik, y ∉ N'_ijk} (tripleSet), both disjoint from the products of real points (by tameness a real limit of the graph lies on the real graph, so its Y_i-coordinate is f_i a with a ∈ U_i ∩ U_j ∩ U_k, whence f_i a ∈ N'_ijk, an open set the approximants avoid); the compact cores K_i = f_i(closure V_i); the finite sets of indices relevant to i (rel, from local finiteness and the compact closure of U_i); and the shrunk pieces A_i ⊇ K_i (Shrunk, from exists_shrink, Hironaka.AnalyticSpace.Glue.Shrink) with A_i × A_j avoiding the pair boundary and A_i × A_j × A_k avoiding the triple set for the relevant pairs and triples.

Conventions. Pairs and triples are constrained only when the other indices are relevant to the first (j ∈ rel' i, k ∈ rel' i, where rel' i also contains i, so that the triples with repeated indices are constrained); the gluing sets of the non-relevant pairs are empty by definition. The triple set with N' = ⊥ forces W_ij ∩ W_ik = ∅ when U_i ∩ U_j ∩ U_k = ∅. For a finite index type every index set is finite anyway; for U_i ∩ U_j = ∅ the pair is not constrained.

def AnalyticSpace.Glue.Huniq (X : AnalyticSpace ℝ) : Prop

The uniqueness hypothesis of the gluing theorem for complexifications, as a predicate: two morphisms out of a neighbourhood of the real points of one complexification into another, both compatible with the structure maps C.f, C'.f, agree on a smaller neighbourhood of the real points.

Equations

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

The cocycle neighbourhoods

noncomputable def AnalyticSpace.Glue.LocalData.cocycleNhd {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace

The cocycle neighbourhood N_ijk ⊆ Y_i (chosen).

Equations

• D.cocycleNhd huniq i j k = ⋯.choose

theorem AnalyticSpace.Glue.LocalData.cocycleNhd_le {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : D.cocycleNhd huniq i j k ≤ tripleDomain (D.P i j) (D.P j k) (D.P i k)

theorem AnalyticSpace.Glue.LocalData.mem_cocycleNhd {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) (v : ↑↑(X.restrictOpen (D.U i ⊓ D.U j ⊓ D.U k)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨↑v, ⋯⟩ ∈ D.cocycleNhd huniq i j k

theorem AnalyticSpace.Glue.LocalData.cocycleNhd_eq {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl ⋯) (compTrans (D.P i j) (D.P j k) (D.P i k)) = CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl ⋯) (directTrans (D.P i j) (D.P j k) (D.P i k))

noncomputable def AnalyticSpace.Glue.LocalData.nhd' {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace

The trimmed cocycle neighbourhood: the cocycle neighbourhood when the triple overlap is nonempty, empty otherwise.

Equations

• D.nhd' huniq i j k = if (↑(D.U i ⊓ D.U j ⊓ D.U k)).Nonempty then D.cocycleNhd huniq i j k else ⊥

theorem AnalyticSpace.Glue.LocalData.nhd'_le_cocycleNhd {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : D.nhd' huniq i j k ≤ D.cocycleNhd huniq i j k

theorem AnalyticSpace.Glue.LocalData.mem_nhd' {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) (v : ↑↑(X.restrictOpen (D.U i ⊓ D.U j ⊓ D.U k)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨↑v, ⋯⟩ ∈ D.nhd' huniq i j k

The closed constraint sets

def AnalyticSpace.Glue.LocalData.pairBoundary {X : AnalyticSpace ℝ} (D : LocalData X) (i j : D.J) : Set (↑↑(D.C i).Y.toPresheafedSpace × ↑↑(D.C j).Y.toPresheafedSpace)

The boundary of the graph of the transition φ_ij.

Equations

• D.pairBoundary i j = closure (D.P i j).graph \ (D.P i j).graph

theorem AnalyticSpace.Glue.LocalData.isClosed_pairBoundary {X : AnalyticSpace ℝ} (D : LocalData X) (i j : D.J) : IsClosed (D.pairBoundary i j)

theorem AnalyticSpace.Glue.LocalData.disjoint_pairBoundary_real {X : AnalyticSpace ℝ} (D : LocalData X) (i j : D.J) : Disjoint (D.pairBoundary i j) (Set.range (KLocallyRingedSpace.Hom.toFun (D.C i).f) ×ˢ Set.range (KLocallyRingedSpace.Hom.toFun (D.C j).f))

def AnalyticSpace.Glue.LocalData.tripleSet {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : Set (↑↑(D.C i).Y.toPresheafedSpace × ↑↑(D.C j).Y.toPresheafedSpace × ↑↑(D.C k).Y.toPresheafedSpace)

The triple set: the points of Ω_ij ∩ Ω_ik off the trimmed cocycle neighbourhood, with their two images.

Equations

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

theorem AnalyticSpace.Glue.LocalData.exists_mem_of_mem_closure_graph_real {X : AnalyticSpace ℝ} (D : LocalData X) (i j : D.J) {a : ↑↑(X.restrictOpen (D.U i)).toPresheafedSpace} {b : ↑↑(X.restrictOpen (D.U j)).toPresheafedSpace} (h : (KLocallyRingedSpace.Hom.toFun (D.C i).f a, KLocallyRingedSpace.Hom.toFun (D.C j).f b) ∈ closure (D.P i j).graph) : ↑a ∈ D.U i ⊓ D.U j

A real limit of a tame graph has its first coordinate over the overlap: the Y_i-coordinate of a point of closure Γ_ij ∩ (R_i × R_j) is f_i a with a ∈ U_i ∩ U_j.

theorem AnalyticSpace.Glue.LocalData.disjoint_closure_tripleSet_real {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) (i j k : D.J) : Disjoint (closure (D.tripleSet huniq i j k)) (Set.range (KLocallyRingedSpace.Hom.toFun (D.C i).f) ×ˢ Set.range (KLocallyRingedSpace.Hom.toFun (D.C j).f) ×ˢ Set.range (KLocallyRingedSpace.Hom.toFun (D.C k).f))

The compact cores and the relevant indices

def AnalyticSpace.Glue.LocalData.core {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : Set ↑↑(D.C i).Y.toPresheafedSpace

The compact core f_i(closure V_i) of the piece Y_i.

Equations

• D.core i = AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.C i).f '' {u : ↑↑(X.restrictOpen (D.U i)).toPresheafedSpace | ↑u ∈ closure ↑(D.V i)}

theorem AnalyticSpace.Glue.LocalData.isCompact_core {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : IsCompact (D.core i)

theorem AnalyticSpace.Glue.LocalData.core_subset_range {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : D.core i ⊆ Set.range (KLocallyRingedSpace.Hom.toFun (D.C i).f)

def AnalyticSpace.Glue.LocalData.rel {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : Set D.J

The indices relevant to i: those whose open meets U_i.

Equations

• D.rel i = {j : D.J | (↑(D.U i) ∩ ↑(D.U j)).Nonempty}

theorem AnalyticSpace.Glue.LocalData.finite_rel {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : (D.rel i).Finite

theorem AnalyticSpace.Glue.LocalData.rel_comm {X : AnalyticSpace ℝ} (D : LocalData X) {i j : D.J} (h : j ∈ D.rel i) : i ∈ D.rel j

def AnalyticSpace.Glue.LocalData.rel' {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : Set D.J

The indices relevant to i together with i itself.

Equations

• D.rel' i = insert i (D.rel i)

theorem AnalyticSpace.Glue.LocalData.finite_rel' {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : (D.rel' i).Finite

theorem AnalyticSpace.Glue.LocalData.self_mem_rel' {X : AnalyticSpace ℝ} (D : LocalData X) (i : D.J) : i ∈ D.rel' i

theorem AnalyticSpace.Glue.LocalData.mem_rel'_of_mem_rel {X : AnalyticSpace ℝ} (D : LocalData X) {i j : D.J} (h : j ∈ D.rel i) : j ∈ D.rel' i

theorem AnalyticSpace.Glue.LocalData.rel'_comm {X : AnalyticSpace ℝ} (D : LocalData X) {i j : D.J} (h : j ∈ D.rel' i) : i ∈ D.rel' j

The shrunk pieces

structure AnalyticSpace.Glue.Shrunk {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) : Type u

The shrunk pieces A_i ⊇ K_i avoiding the pair boundaries and the closures of the triple sets of the relevant pairs and triples.

• A (i : D.J) : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace

  The shrunk piece.

• core_subset (i : D.J) : D.core i ⊆ ↑(self.A i)
• pair (i j : D.J) : j ∈ D.rel' i → Disjoint (↑(self.A i) ×ˢ ↑(self.A j)) (D.pairBoundary i j)

  The pair constraint: A_i × A_j avoids the boundary of the transition graph, so the graph is closed in A_i × A_j; a limit pair (f_i x, z) with f_i x ∈ A_i, z ∈ A_j lies on the graph, so f_i x ∈ Ω_ij, x lies over U_i ∩ U_j and z = f_j x.

• triple (i j k : D.J) : j ∈ D.rel' i → k ∈ D.rel' i → Disjoint (↑(self.A i) ×ˢ ↑(self.A j) ×ˢ ↑(self.A k)) (closure (D.tripleSet huniq i j k))

theorem AnalyticSpace.Glue.exists_shrunk {X : AnalyticSpace ℝ} (D : LocalData X) (huniq : Huniq X) : Nonempty (Shrunk D huniq)