The gluing data of the shrunk pieces

From the shrunk pieces A_i (Hironaka.AnalyticSpace.Glue.TripleSet), the K-gluing core of the gluing theorem for complexifications: pieces Y_i | A_i; gluing open subsets W_ij = A_i ∩ Ω_ij ∩ φ_ij⁻¹(A_j) (everything on the diagonal, nothing for non-relevant pairs); transitions t_ij lifted from φ_ij along the inclusions (the identity on the diagonal). The shrinking constraints give: a point of W_ij ∩ W_ik lies in the trimmed cocycle neighbourhood N'_ijk (mem_nhd'_of_mem), so t_ij lands in W_ji (through the triple (i, j, i)), and t_ij carries W_ij ∩ W_ik into W_jk (t_inter, through the triple (i, j, k) and the pointwise cocycle). This module builds the KGlueCore (Shrunk.core); the cocycle identity, making it KGlueData, is Hironaka.AnalyticSpace.Glue.CocycleData.

Conventions. WOpen i j ⊆ Y_i is the gluing open subset in Y_i; W i j is its preimage in the piece Y_i | A_i. The diagonal transition is the identity transported along i = j (diagTrans, with diagTrans_rfl). For j ∉ rel i with j ≠ i, W i j = ⊥ and every identity about it holds trivially, by ⊥ ≤ _; for U_i ∩ U_j ∩ U_k = ∅ with j, k ∈ rel i, N'_ijk = ⊥, so W_ij ∩ W_ik = ∅.

The diagonal datum, unfolded

theorem AnalyticSpace.Glue.LocalData.Ωi_P_diag {X : AnalyticSpace ℝ} {D : LocalData X} (i : D.J) : (D.P i i).Ωi = ⊤

theorem AnalyticSpace.Glue.LocalData.mem_Ωi_P_diag {X : AnalyticSpace ℝ} {D : LocalData X} (i : D.J) (y : ↑↑(D.C i).Y.toPresheafedSpace) : y ∈ (D.P i i).Ωi

theorem AnalyticSpace.Glue.LocalData.toFun_e_P_diag {X : AnalyticSpace ℝ} {D : LocalData X} (i : D.J) (z : ↑↑((D.C i).Y.restrictOpen (D.P i i).Ωi).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (D.P i i).e.hom z) = ↑z

The pieces and the gluing opens

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.Shrunk.piece {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : KLocallyRingedSpace ℂ

The shrunk piece Y_i | A_i, as a K-space.

Equations

• S.piece i = (D.C i).Y.restrictOpen (S.A i)

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

The gluing open A_i ∩ Ω_ij ∩ φ_ij⁻¹(A_j) ⊆ Y_i (everything on the diagonal, nothing for a non-relevant pair).

Equations

• S.WOpen i j = if i = j then ⊤ else if j ∈ D.rel i then S.A i ⊓ (D.P i j).Ωi ⊓ (D.P i j).pullOpens (S.A j) else ⊥

noncomputable def AnalyticSpace.Glue.Shrunk.W {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : TopologicalSpace.Opens ↑↑(S.piece i).toPresheafedSpace

The gluing open as an open of the piece.

Equations

• S.W i j = (TopologicalSpace.Opens.map (↑((D.C i).Y.ofRestrict (S.A i))).base).obj (S.WOpen i j)

theorem AnalyticSpace.Glue.Shrunk.mem_W {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (x : ↑↑(S.piece i).toPresheafedSpace) : x ∈ S.W i j ↔ ↑x ∈ S.WOpen i j

theorem AnalyticSpace.Glue.Shrunk.WOpen_self {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : S.WOpen i i = ⊤

theorem AnalyticSpace.Glue.Shrunk.WOpen_of_ne_of_mem {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) (hj : j ∈ D.rel i) : S.WOpen i j = S.A i ⊓ (D.P i j).Ωi ⊓ (D.P i j).pullOpens (S.A j)

theorem AnalyticSpace.Glue.Shrunk.WOpen_of_notMem {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) (hj : j ∉ D.rel i) : S.WOpen i j = ⊥

theorem AnalyticSpace.Glue.Shrunk.W_self {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : S.W i i = ⊤

theorem AnalyticSpace.Glue.Shrunk.mem_rel_of_mem_WOpen {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : j ∈ D.rel i

theorem AnalyticSpace.Glue.Shrunk.mem_A_of_mem_WOpen {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : y ∈ S.A i

theorem AnalyticSpace.Glue.Shrunk.mem_Ω_of_mem_WOpen {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : y ∈ (D.P i j).Ωi

theorem AnalyticSpace.Glue.Shrunk.toFun_e_mem_A_of_mem_WOpen {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : ↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨y, ⋯⟩) ∈ S.A j

The shrinking constraints on points

theorem AnalyticSpace.Glue.Shrunk.mem_nhd'_of_mem {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j k : D.J} (hj : j ∈ D.rel' i) (hk : k ∈ D.rel' i) {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.A i) (hΩj : y ∈ (D.P i j).Ωi) (hΩk : y ∈ (D.P i k).Ωi) (hAj : ↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨y, hΩj⟩) ∈ S.A j) (hAk : ↑(KLocallyRingedSpace.Hom.toFun (D.P i k).e.hom ⟨y, hΩk⟩) ∈ S.A k) : y ∈ D.nhd' huniq i j k

A point of A_i ∩ Ω_ij ∩ Ω_ik whose two images lie in A_j, A_k lies in the trimmed cocycle neighbourhood N'_ijk (the triple constraint of the shrinking).

theorem AnalyticSpace.Glue.Shrunk.nhd'_cases {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 ∧ (↑(D.U i ⊓ D.U j ⊓ D.U k)).Nonempty ∨ D.nhd' huniq i j k = ⊥

The trimmed neighbourhood is either the cocycle neighbourhood (nonempty triple overlap) or empty.

theorem AnalyticSpace.Glue.Shrunk.mem_cocycleNhd_of_mem_nhd' {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} {i j k : D.J} {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ D.nhd' huniq i j k) : y ∈ D.cocycleNhd huniq i j k ∧ (↑(D.U i ⊓ D.U j ⊓ D.U k)).Nonempty

A point of the trimmed neighbourhood lies in the cocycle neighbourhood, and the triple overlap is nonempty.

theorem AnalyticSpace.Glue.Shrunk.toFun_e_e_eq {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} {i j k : D.J} {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ D.cocycleNhd huniq i j k) : ↑(KLocallyRingedSpace.Hom.toFun (D.P j k).e.hom ⟨↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨y, ⋯⟩), ⋯⟩) = ↑(KLocallyRingedSpace.Hom.toFun (D.P i k).e.hom ⟨y, ⋯⟩)

The pointwise cocycle on the cocycle neighbourhood: φ_jk (φ_ij y) = φ_ik y.

The transition lands in the gluing open of the other piece

theorem AnalyticSpace.Glue.Shrunk.mem_nhd'_of_mem_WOpen {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : y ∈ D.nhd' huniq i j i

theorem AnalyticSpace.Glue.Shrunk.toFun_e_mem_WOpen {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : ↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨y, ⋯⟩) ∈ S.WOpen j i

The image of a point of W_ij under φ_ij lies in W_ji.

The transitions

theorem AnalyticSpace.Glue.Shrunk.range_incl₂_subset_Ω {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : Set.range (KLocallyRingedSpace.Hom.toFun (incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j))) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun ((D.C i).Y.ofRestrict (D.P i j).Ωi))

noncomputable def AnalyticSpace.Glue.Shrunk.ι {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : (S.piece i).restrictOpen (S.W i j) ⟶ (D.C i).Y.restrictOpen (D.P i j).Ωi

The inclusion of the gluing open into the transition domain Y_i | Ω_ij.

Equations

• S.ι i j = AnalyticSpace.Glue.liftAlong ((D.C i).Y.ofRestrict (D.P i j).Ωi) (AnalyticSpace.Glue.incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j)) ⋯

theorem AnalyticSpace.Glue.Shrunk.ι_comp_ofRestrict {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (S.ι i j) ((D.C i).Y.ofRestrict (D.P i j).Ωi) = incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j)

theorem AnalyticSpace.Glue.Shrunk.toFun_ι_val {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) (x : ↑↑((S.piece i).restrictOpen (S.W i j)).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (S.ι i j) x) = ↑↑x

noncomputable def AnalyticSpace.Glue.Shrunk.tW {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : (S.piece i).restrictOpen (S.W i j) ⟶ (D.C j).Y.toKLocallyRingedSpace

The transition into Y_j.

Equations

• S.tW i j = CategoryTheory.CategoryStruct.comp (S.ι i j) (CategoryTheory.CategoryStruct.comp (D.P i j).e.hom ((D.C j).Y.ofRestrict (D.P i j).Ωj))

theorem AnalyticSpace.Glue.Shrunk.toFun_tW {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) (x : ↑↑((S.piece i).restrictOpen (S.W i j)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (S.tW i j) x = ↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨↑↑x, ⋯⟩)

theorem AnalyticSpace.Glue.Shrunk.range_tW_subset {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) : Set.range (KLocallyRingedSpace.Hom.toFun (S.tW i j)) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun (incl₂ (D.C j).Y.toKLocallyRingedSpace (S.A j) (S.W j i)))

noncomputable def AnalyticSpace.Glue.Shrunk.diagTrans {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) (h : i = j) : (S.piece i).restrictOpen (S.W i j) ⟶ (S.piece j).restrictOpen (S.W j i)

The identity transition on the diagonal, transported along i = j.

Equations

• S.diagTrans i j h = h ▸ CategoryTheory.CategoryStruct.id ((S.piece i).restrictOpen (S.W i i))

theorem AnalyticSpace.Glue.Shrunk.diagTrans_rfl {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : S.diagTrans i i ⋯ = CategoryTheory.CategoryStruct.id ((S.piece i).restrictOpen (S.W i i))

noncomputable def AnalyticSpace.Glue.Shrunk.t {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : (S.piece i).restrictOpen (S.W i j) ⟶ (S.piece j).restrictOpen (S.W j i)

The transition t_ij : W_ij ⟶ W_ji.

Equations

• S.t i j = if h : i = j then S.diagTrans i j h else AnalyticSpace.Glue.liftAlong (AnalyticSpace.Glue.incl₂ (D.C j).Y.toKLocallyRingedSpace (S.A j) (S.W j i)) (S.tW i j) ⋯

theorem AnalyticSpace.Glue.Shrunk.t_self {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : S.t i i = CategoryTheory.CategoryStruct.id ((S.piece i).restrictOpen (S.W i i))

theorem AnalyticSpace.Glue.Shrunk.t_comp_incl₂ {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) : CategoryTheory.CategoryStruct.comp (S.t i j) (incl₂ (D.C j).Y.toKLocallyRingedSpace (S.A j) (S.W j i)) = S.tW i j

theorem AnalyticSpace.Glue.Shrunk.toFun_t_val {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j : D.J} (h : i ≠ j) (x : ↑↑((S.piece i).restrictOpen (S.W i j)).toPresheafedSpace) : ↑↑(KLocallyRingedSpace.Hom.toFun (S.t i j) x) = ↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨↑↑x, ⋯⟩)

The gluing core

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.Shrunk.core {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) : KGlueCore ℂ

The K-gluing core of the shrunk pieces.

Equations

• S.core = { J := D.J, Y := S.piece, W := S.W, W_id := ⋯, t := S.t, t_id := ⋯, t_inter := ⋯ }