The cocycle identity of the shrunk gluing data

The K-gluing core of the shrunk pieces (Hironaka.AnalyticSpace.Glue.Assemble) satisfies the cocycle identity tRes i j k ≫ tRes j k i ≫ tRes k i j = 𝟙 on the triple pieces Z_ijk = (Y_i | A_i) | (W_ij ⊓ W_ik) (Shrunk.cocycle), hence is K-gluing data (Shrunk.data, Hironaka.AnalyticSpace.Glue.Data) and glues to a K-space (Hironaka.AnalyticSpace.Glue.KSpace). The identity is a morphism identity, not a pointwise one: the points of Z_ijk lie in the cocycle neighbourhoods N_ijk and N_iki (Hironaka.AnalyticSpace.Glue.TripleSet, through the shrinking constraints), on which the transitions satisfy φ_jk ∘ φ_ij = φ_ik and φ_ki ∘ φ_ik = φ_ii = id as morphisms (cocycleNhd_eq, the cocycle on a neighbourhood of the real points, as in the proof of [Car57, §3, Proposition 2]); the three restricted transitions, pushed into the ambient complexifications, are these composites restricted along the inclusion of Z_ijk (uniqueness of lifts along open immersions).

Conventions. inclZTo Ω is the inclusion of Z_ijk into Y_i | Ω for an open subset Ω ⊆ Y_i containing its points; every morphism of the argument out of Z_ijk into a restriction of Y_i is identified with such an inclusion by eq_inclZTo (uniqueness of lifts), and the chains of inclusions collapse by inclZTo_comp_restrictOpenIncl. Repeated indices need no case split: W_ii = ⊤ and P i i = refl, so φ_ii = id (e_P_diag_comp_ofRestrict), and t_comp_incl₂' covers the diagonal transition; for an empty W_ij ⊓ W_ik the identity holds on the empty space by the same argument.

theorem AnalyticSpace.Glue.restrictOpenIncl_comp_incl₂ {K : Type} [RCLike K] (A : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) {W W' : TopologicalSpace.Opens ↑↑(A.restrictOpen U).toPresheafedSpace} (h : W ≤ W') : CategoryTheory.CategoryStruct.comp ((A.restrictOpen U).restrictOpenIncl h) (incl₂ A U W') = incl₂ A U W

The inclusion of a smaller open of a restriction, followed by the double-restriction inclusion, is the double-restriction inclusion of the smaller open.

theorem AnalyticSpace.Glue.restrictOpenIncl_comp_incl₂_assoc {K : Type} [RCLike K] (A : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) {W W' : TopologicalSpace.Opens ↑↑(A.restrictOpen U).toPresheafedSpace} (h : W ≤ W') {Z : KLocallyRingedSpace K} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((A.restrictOpen U).restrictOpenIncl h) (CategoryTheory.CategoryStruct.comp (incl₂ A U W') h✝) = CategoryTheory.CategoryStruct.comp (incl₂ A U W) h✝

The inclusion of a smaller open of a restriction, followed by the double-restriction inclusion, is the double-restriction inclusion of the smaller open.

theorem AnalyticSpace.Glue.LocalData.e_P_diag_comp_ofRestrict {X : AnalyticSpace ℝ} {D : LocalData X} (i : D.J) : CategoryTheory.CategoryStruct.comp (D.P i i).e.hom ((D.C i).Y.ofRestrict (D.P i i).Ωj) = (D.C i).Y.ofRestrict (D.P i i).Ωi

On the diagonal the transition is the identity of Y_i: e_ii ≫ ofRestrict = ofRestrict.

Points of the triple pieces lie in the cocycle neighbourhoods

theorem AnalyticSpace.Glue.Shrunk.mem_WOpen_self {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) (y : ↑↑(D.C i).Y.toPresheafedSpace) : y ∈ S.WOpen 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} {y : ↑↑(D.C i).Y.toPresheafedSpace} (hy : y ∈ S.WOpen i j) : j ∈ D.rel' 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} {y : ↑↑(D.C i).Y.toPresheafedSpace} (hA : y ∈ S.A i) (hy : y ∈ S.WOpen i j) : ↑(KLocallyRingedSpace.Hom.toFun (D.P i j).e.hom ⟨y, ⋯⟩) ∈ S.A j

theorem AnalyticSpace.Glue.Shrunk.mem_cocycleNhd_of_mem_WOpen₂ {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j k : D.J} {y : ↑↑(D.C i).Y.toPresheafedSpace} (hA : y ∈ S.A i) (hy : y ∈ S.WOpen i j) (hy' : y ∈ S.WOpen i k) : y ∈ D.cocycleNhd huniq i j k

A point of A_i ∩ W_ij ∩ W_ik lies in the cocycle neighbourhood N_ijk: the triple constraint of the shrinking.

theorem AnalyticSpace.Glue.Shrunk.mem_cocycleNhd_of_Z {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace) : ↑↑x ∈ D.cocycleNhd huniq i j k

theorem AnalyticSpace.Glue.Shrunk.mem_cocycleNhd_iki_of_Z {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace) : ↑↑x ∈ D.cocycleNhd huniq i k i

The inclusions of the triple pieces

noncomputable def AnalyticSpace.Glue.Shrunk.inclZTo {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) (Ω : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace) (h : ∀ (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace), ↑↑x ∈ Ω) : (S.piece i).restrictOpen (S.W i j ⊓ S.W i k) ⟶ (D.C i).Y.restrictOpen Ω

The inclusion of the triple piece Z_ijk = (Y_i | A_i) | (W_ij ⊓ W_ik) into Y_i | Ω, for an open Ω containing its points.

Equations

• S.inclZTo i j k Ω h = AnalyticSpace.Glue.liftAlong ((D.C i).Y.ofRestrict Ω) (AnalyticSpace.Glue.incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j ⊓ S.W i k)) ⋯

theorem AnalyticSpace.Glue.Shrunk.inclZTo_comp_ofRestrict {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) (Ω : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace) (h : ∀ (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace), ↑↑x ∈ Ω) : CategoryTheory.CategoryStruct.comp (S.inclZTo i j k Ω h) ((D.C i).Y.ofRestrict Ω) = incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j ⊓ S.W i k)

theorem AnalyticSpace.Glue.Shrunk.inclZTo_comp_ofRestrict_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) (Ω : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace) (h : ∀ (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace), ↑↑x ∈ Ω) {Z : KLocallyRingedSpace ℂ} (h✝ : (D.C i).Y.toKLocallyRingedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.inclZTo i j k Ω h) (CategoryTheory.CategoryStruct.comp ((D.C i).Y.ofRestrict Ω) h✝) = CategoryTheory.CategoryStruct.comp (incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j ⊓ S.W i k)) h✝

theorem AnalyticSpace.Glue.Shrunk.eq_inclZTo {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j k : D.J} {Ω : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace} (h : ∀ (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace), ↑↑x ∈ Ω) {g : (S.piece i).restrictOpen (S.W i j ⊓ S.W i k) ⟶ (D.C i).Y.restrictOpen Ω} (hg : CategoryTheory.CategoryStruct.comp g ((D.C i).Y.ofRestrict Ω) = incl₂ (D.C i).Y.toKLocallyRingedSpace (S.A i) (S.W i j ⊓ S.W i k)) : g = S.inclZTo i j k Ω h

Uniqueness of lifts: a morphism of Z_ijk into Y_i | Ω over the inclusion of Z_ijk into Y_i is the inclusion.

theorem AnalyticSpace.Glue.Shrunk.inclZTo_comp_restrictOpenIncl {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Ω Ω' : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace} (hΩ : Ω ≤ Ω') (h : ∀ (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace), ↑↑x ∈ Ω) : CategoryTheory.CategoryStruct.comp (S.inclZTo i j k Ω h) ((D.C i).Y.restrictOpenIncl hΩ) = S.inclZTo i j k Ω' ⋯

theorem AnalyticSpace.Glue.Shrunk.inclZTo_comp_restrictOpenIncl_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Ω Ω' : TopologicalSpace.Opens ↑↑(D.C i).Y.toPresheafedSpace} (hΩ : Ω ≤ Ω') (h : ∀ (x : ↑↑((S.piece i).restrictOpen (S.W i j ⊓ S.W i k)).toPresheafedSpace), ↑↑x ∈ Ω) {Z : KLocallyRingedSpace ℂ} (h✝ : (D.C i).Y.restrictOpen Ω' ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.inclZTo i j k Ω h) (CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl hΩ) h✝) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k Ω' ⋯) h✝

theorem AnalyticSpace.Glue.Shrunk.restrictOpenIncl_comp_ι_left {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) : CategoryTheory.CategoryStruct.comp ((S.piece i).restrictOpenIncl ⋯) (S.ι i j) = S.inclZTo i j k (D.P i j).Ωi ⋯

theorem AnalyticSpace.Glue.Shrunk.restrictOpenIncl_comp_ι_left_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Z : KLocallyRingedSpace ℂ} (h : (D.C i).Y.restrictOpen (D.P i j).Ωi ⟶ Z) : CategoryTheory.CategoryStruct.comp ((S.piece i).restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (S.ι i j) h) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k (D.P i j).Ωi ⋯) h

theorem AnalyticSpace.Glue.Shrunk.restrictOpenIncl_comp_ι_right {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) : CategoryTheory.CategoryStruct.comp ((S.piece i).restrictOpenIncl ⋯) (S.ι i k) = S.inclZTo i j k (D.P i k).Ωi ⋯

theorem AnalyticSpace.Glue.Shrunk.restrictOpenIncl_comp_ι_right_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Z : KLocallyRingedSpace ℂ} (h : (D.C i).Y.restrictOpen (D.P i k).Ωi ⟶ Z) : CategoryTheory.CategoryStruct.comp ((S.piece i).restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (S.ι i k) h) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k (D.P i k).Ωi ⋯) h

The restricted transitions, pushed into the ambient complexifications

theorem AnalyticSpace.Glue.Shrunk.t_comp_incl₂' {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.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

The transition followed by the inclusion into Y_j, on the diagonal included.

theorem AnalyticSpace.Glue.Shrunk.tRes_comp_incl₂ {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (incl₂ (D.C j).Y.toKLocallyRingedSpace (S.A j) (S.W j k ⊓ S.W j i)) = CategoryTheory.CategoryStruct.comp ((S.piece i).restrictOpenIncl ⋯) (S.tW i j)

The restricted transition tRes i j k, pushed into Y_j, is φ_ij on the points of Z_ijk.

theorem AnalyticSpace.Glue.Shrunk.tRes_comp_incl₂_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Z : KLocallyRingedSpace ℂ} (h : (D.C j).Y.toKLocallyRingedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (CategoryTheory.CategoryStruct.comp (incl₂ (D.C j).Y.toKLocallyRingedSpace (S.A j) (S.W j k ⊓ S.W j i)) h) = CategoryTheory.CategoryStruct.comp ((S.piece i).restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (S.tW i j) h)

The restricted transition tRes i j k, pushed into Y_j, is φ_ij on the points of Z_ijk.

theorem AnalyticSpace.Glue.Shrunk.tRes_comp_restrictOpenIncl_comp_ι {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (CategoryTheory.CategoryStruct.comp ((S.piece j).restrictOpenIncl ⋯) (S.ι j k)) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k (D.cocycleNhd huniq i j k) ⋯) (CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl ⋯) (tripleFirst (D.P i j) (D.P j k) (D.P i k)))

The first restricted transition, pushed into Y_j | Ω_jk: the first factor of the composite transition compTrans restricted to Z_ijk ⊆ N_ijk.

theorem AnalyticSpace.Glue.Shrunk.tRes_comp_restrictOpenIncl_comp_ι_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Z : KLocallyRingedSpace ℂ} (h : (D.C j).Y.restrictOpen (D.P j k).Ωi ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (CategoryTheory.CategoryStruct.comp ((S.piece j).restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (S.ι j k) h)) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k (D.cocycleNhd huniq i j k) ⋯) (CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (tripleFirst (D.P i j) (D.P j k) (D.P i k)) h))

The first restricted transition, pushed into Y_j | Ω_jk: the first factor of the composite transition compTrans restricted to Z_ijk ⊆ N_ijk.

theorem AnalyticSpace.Glue.Shrunk.tRes_comp_tRes_comp_restrictOpenIncl_comp_ι {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (CategoryTheory.CategoryStruct.comp (S.core.tRes j k i) (CategoryTheory.CategoryStruct.comp ((S.piece k).restrictOpenIncl ⋯) (S.ι k i))) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k (D.cocycleNhd huniq i k i) ⋯) (CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl ⋯) (tripleFirst (D.P i k) (D.P k i) (D.P i i)))

The first two restricted transitions, pushed into Y_k | Ω_ki: by the cocycle on N_ijk they are φ_ik on the points of Z_ijk, the first factor of compTrans for the triple (i, k, i) restricted to Z_ijk ⊆ N_iki.

theorem AnalyticSpace.Glue.Shrunk.tRes_comp_tRes_comp_restrictOpenIncl_comp_ι_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) {Z : KLocallyRingedSpace ℂ} (h : (D.C k).Y.restrictOpen (D.P k i).Ωi ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (CategoryTheory.CategoryStruct.comp (S.core.tRes j k i) (CategoryTheory.CategoryStruct.comp ((S.piece k).restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (S.ι k i) h))) = CategoryTheory.CategoryStruct.comp (S.inclZTo i j k (D.cocycleNhd huniq i k i) ⋯) (CategoryTheory.CategoryStruct.comp ((D.C i).Y.restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp (tripleFirst (D.P i k) (D.P k i) (D.P i i)) h))

The first two restricted transitions, pushed into Y_k | Ω_ki: by the cocycle on N_ijk they are φ_ik on the points of Z_ijk, the first factor of compTrans for the triple (i, k, i) restricted to Z_ijk ⊆ N_iki.

The cocycle identity and the gluing data

theorem AnalyticSpace.Glue.Shrunk.cocycle {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j k : D.J) : CategoryTheory.CategoryStruct.comp (S.core.tRes i j k) (CategoryTheory.CategoryStruct.comp (S.core.tRes j k i) (S.core.tRes k i j)) = CategoryTheory.CategoryStruct.id ((S.core.Y i).restrictOpen (S.core.W i j ⊓ S.core.W i k))

The cocycle identity of the shrunk gluing core: by the cocycles on N_ijk and N_iki the composite of the three restricted transitions, pushed into Y_i, is φ_ii = id on the points of Z_ijk, hence the inclusion of Z_ijk.

@[reducible, inline]

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

The K-gluing data of the shrunk pieces.

Equations

• S.data = { toKGlueCore := S.core, cocycle := ⋯ }

theorem AnalyticSpace.Glue.Shrunk.data_toKGlueCore {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) : S.data.toKGlueCore = S.core