The cocycle of three transition data near the real points

For three normalized transition data P_ij, P_jk, P_ik (Hironaka.AnalyticSpace.Glue.Normalize) between the local complexifications of X | U_i, X | U_j, X | U_k, the two morphisms φ_jk ∘ φ_ij and φ_ik out of the common domain D = Ω_ij ∩ φ_ij⁻¹(Ω_jk) ∩ Ω_ik ⊆ Y_i agree on an open subset N ⊆ D containing f_i(U_i ∩ U_j ∩ U_k): the cocycle condition holds on a neighbourhood of the real points (exists_cocycle_nhd), under the hypothesis huniq that two morphisms out of a neighbourhood of the real points of one complexification into another, both compatible with the structure maps f, agree near the real points; the statement needs it. This is as in the proof of [Car57, §3, Proposition 2], where the set on which the cocycle identity holds is an open set containing the closed subspace. This is exists_eq_near_of_huniq applied to the composite and the direct transition, whose compatibility with f_i, f_k and whose ranges are checked from the fields of the data.

Conventions. The range hypotheses of exists_eq_near_of_huniq (the two morphisms land in Y_k ∖ f_k(U_k ∖ (U_i ∩ U_j ∩ U_k))) hold because the real points of every transition domain lie over its overlap (Ωi_le, Ωj_le of each datum), transitions carry real points to real points (toFun_e_hom_val) and only real points to real points (exists_eq_of_toFun_e_hom_eq). Basic tools come first: composition of the inclusions of open subspaces (restrictOpenIncl_trans), the lift of f restricted to a smaller open subset (complexifyIncl_comp_pairLift), the pulled-back open subset P.pullOpens T ⊆ Y_i of T ⊆ Y_j under the transition (imageOpens of the preimage in the restricted space) and PairIso.mem_of_toFun_eq (real points of the domain lie over V). For U_i ∩ U_j ∩ U_k = ∅, N may be empty; for j = i or k = i with the diagonal datum, the composite is the transition itself and N = D works.

theorem AnalyticSpace.Glue.restrictOpenIncl_trans {K : Type} [RCLike K] (A : KLocallyRingedSpace K) {U V W : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} (h₁ : U ≤ V) (h₂ : V ≤ W) : CategoryTheory.CategoryStruct.comp (A.restrictOpenIncl h₁) (A.restrictOpenIncl h₂) = A.restrictOpenIncl ⋯

The inclusions of open subspaces compose.

theorem AnalyticSpace.Glue.complexifyIncl_comp_pairLift {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) {V V' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ U) (hV' : V' ≤ V) (Ω : TopologicalSpace.Opens ↑↑C.Y.toPresheafedSpace) (h : ∀ (v : ↑↑(X.restrictOpen V).toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C.f ⟨↑v, ⋯⟩ ∈ Ω) : CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl hV')) (pairLift C hV Ω h) = pairLift C ⋯ Ω ⋯

The lift of f ∘ incl_V into Ω, restricted to V' ≤ V, is the lift of f ∘ incl_{V'}.

noncomputable def AnalyticSpace.Glue.PairIso.pullOpens {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {hVi : V ≤ Ui} {hVj : V ≤ Uj} (P : PairIso Ci Cj V hVi hVj) (T : TopologicalSpace.Opens ↑↑Cj.Y.toPresheafedSpace) : TopologicalSpace.Opens ↑↑Ci.Y.toPresheafedSpace

The preimage of an open subset T ⊆ Y_j under the transition, as an open subset of Y_i.

Equations

• P.pullOpens T = AnalyticSpace.KLocallyRingedSpace.imageOpens P.Ωi ((TopologicalSpace.Opens.map (↑(CategoryTheory.CategoryStruct.comp P.e.hom (Cj.Y.ofRestrict P.Ωj))).base).obj T)

theorem AnalyticSpace.Glue.PairIso.mem_pullOpens {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {hVi : V ≤ Ui} {hVj : V ≤ Uj} (P : PairIso Ci Cj V hVi hVj) (T : TopologicalSpace.Opens ↑↑Cj.Y.toPresheafedSpace) (y : ↑↑Ci.Y.toPresheafedSpace) : y ∈ P.pullOpens T ↔ ∃ (h : y ∈ P.Ωi), ↑(KLocallyRingedSpace.Hom.toFun P.e.hom ⟨y, h⟩) ∈ T

theorem AnalyticSpace.Glue.PairIso.pullOpens_le {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {hVi : V ≤ Ui} {hVj : V ≤ Uj} (P : PairIso Ci Cj V hVi hVj) (T : TopologicalSpace.Opens ↑↑Cj.Y.toPresheafedSpace) : P.pullOpens T ≤ P.Ωi

theorem AnalyticSpace.Glue.PairIso.mem_of_toFun_eq {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {hVi : V ≤ Ui} {hVj : V ≤ Uj} (P : PairIso Ci Cj V hVi hVj) (u : ↑↑(X.restrictOpen Ui).toPresheafedSpace) (hu : KLocallyRingedSpace.Hom.toFun Ci.f u ∈ P.Ωi) : ↑u ∈ V

A real point of the domain lies over V.

theorem AnalyticSpace.Glue.PairIso.mem_of_toFun_eq' {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {hVi : V ≤ Ui} {hVj : V ≤ Uj} (P : PairIso Ci Cj V hVi hVj) (u : ↑↑(X.restrictOpen Uj).toPresheafedSpace) (hu : KLocallyRingedSpace.Hom.toFun Cj.f u ∈ P.Ωj) : ↑u ∈ V

Compatibility restricted to a smaller open

theorem AnalyticSpace.Glue.complexifyIncl_comp_complexifyIncl_comp {X : AnalyticSpace ℝ} {U V W : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h₁ : U ≤ V) (h₂ : V ≤ W) {Z : KLocallyRingedSpace ℂ} (g : (X.restrictOpen W).complexify ⟶ Z) : CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl h₁)) (CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl h₂)) g) = CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl ⋯)) g

Two complexified inclusions compose (h₁.trans h₂), followed by any g.

theorem AnalyticSpace.Glue.pairLift_comp_restrictOpenIncl {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ U) (D Ω : TopologicalSpace.Opens ↑↑C.Y.toPresheafedSpace) (hDΩ : D ≤ Ω) (hD : ∀ (v : ↑↑(X.restrictOpen V).toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C.f ⟨↑v, ⋯⟩ ∈ D) : CategoryTheory.CategoryStruct.comp (pairLift C hV D hD) (C.Y.restrictOpenIncl hDΩ) = pairLift C hV Ω ⋯

The lift into D ≤ Ω followed by the inclusion D ≤ Ω is the lift into Ω.

theorem AnalyticSpace.Glue.PairIso.compat_restrict {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {V' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {hVi' : V' ≤ Ui} {hVj' : V' ≤ Uj} (P : PairIso Ci Cj V' hVi' hVj') {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : V ≤ V') : CategoryTheory.CategoryStruct.comp (pairLift Ci ⋯ P.Ωi ⋯) (CategoryTheory.CategoryStruct.comp P.e.hom (Cj.Y.ofRestrict P.Ωj)) = CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl ⋯)) Cj.f

The compatibility of a datum over V', restricted to V ≤ V'.

The cocycle near the real points

noncomputable def AnalyticSpace.Glue.tripleDomain {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : TopologicalSpace.Opens ↑↑Ci.Y.toPresheafedSpace

The common domain Ω_ij ∩ φ_ij⁻¹(Ω_jk) ∩ Ω_ik ⊆ Y_i of the composite and the direct transition.

Equations

• AnalyticSpace.Glue.tripleDomain Pij Pjk Pik = Pij.Ωi ⊓ Pij.pullOpens Pjk.Ωi ⊓ Pik.Ωi

theorem AnalyticSpace.Glue.tripleDomain_le_Ωij {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : tripleDomain Pij Pjk Pik ≤ Pij.Ωi

theorem AnalyticSpace.Glue.tripleDomain_le_Ωik {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : tripleDomain Pij Pjk Pik ≤ Pik.Ωi

theorem AnalyticSpace.Glue.mem_pullOpens_of_mem_tripleDomain {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) {y : ↑↑Ci.Y.toPresheafedSpace} (hy : y ∈ tripleDomain Pij Pjk Pik) : ↑(KLocallyRingedSpace.Hom.toFun Pij.e.hom ⟨y, ⋯⟩) ∈ Pjk.Ωi

theorem AnalyticSpace.Glue.range_tripleFirst_subset {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp (Ci.Y.restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp Pij.e.hom (Cj.Y.ofRestrict Pij.Ωj)))) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun (Cj.Y.ofRestrict Pjk.Ωi))

noncomputable def AnalyticSpace.Glue.tripleFirst {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik) ⟶ Cj.Y.restrictOpen Pjk.Ωi

The first factor of the composite: D ⟶ Y_j | Ω_jk.

Equations

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

noncomputable def AnalyticSpace.Glue.compTrans {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik) ⟶ Ck.Y.toKLocallyRingedSpace

The composite transition φ_jk ∘ φ_ij on the common domain.

Equations

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

noncomputable def AnalyticSpace.Glue.directTrans {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik) ⟶ Ck.Y.toKLocallyRingedSpace

The direct transition φ_ik on the common domain.

Equations

• AnalyticSpace.Glue.directTrans Pij Pjk Pik = CategoryTheory.CategoryStruct.comp (Ci.Y.restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp Pik.e.hom (Ck.Y.ofRestrict Pik.Ωj))

theorem AnalyticSpace.Glue.toFun_tripleFirst_val {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (y : ↑↑(Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik)).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (tripleFirst Pij Pjk Pik) y) = ↑(KLocallyRingedSpace.Hom.toFun Pij.e.hom ⟨↑y, ⋯⟩)

theorem AnalyticSpace.Glue.toFun_directTrans_val {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (y : ↑↑(Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (directTrans Pij Pjk Pik) y = ↑(KLocallyRingedSpace.Hom.toFun Pik.e.hom ⟨↑y, ⋯⟩)

theorem AnalyticSpace.Glue.toFun_compTrans_val {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (y : ↑↑(Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (compTrans Pij Pjk Pik) y = ↑(KLocallyRingedSpace.Hom.toFun Pjk.e.hom ⟨↑(KLocallyRingedSpace.Hom.toFun Pij.e.hom ⟨↑y, ⋯⟩), ⋯⟩)

theorem AnalyticSpace.Glue.tripleV_le_Ui {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} : Ui ⊓ Uj ⊓ Uk ≤ Ui

theorem AnalyticSpace.Glue.tripleV_le_Uj {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} : Ui ⊓ Uj ⊓ Uk ≤ Uj

theorem AnalyticSpace.Glue.tripleV_le_Uk {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} : Ui ⊓ Uj ⊓ Uk ≤ Uk

theorem AnalyticSpace.Glue.mem_tripleDomain {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (v : ↑↑(X.restrictOpen (Ui ⊓ Uj ⊓ Uk)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun Ci.f ⟨↑v, ⋯⟩ ∈ tripleDomain Pij Pjk Pik

f_i(U_i ∩ U_j ∩ U_k) lies in the common domain.

theorem AnalyticSpace.Glue.tripleDomain_le_restrictLeOpens {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : tripleDomain Pij Pjk Pik ≤ Ci.restrictLeOpens (Ui ⊓ Uj ⊓ Uk)

The real points of the common domain lie over U_i ∩ U_j ∩ U_k.

theorem AnalyticSpace.Glue.pairLift_comp_directTrans {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : CategoryTheory.CategoryStruct.comp (pairLift Ci ⋯ (tripleDomain Pij Pjk Pik) ⋯) (directTrans Pij Pjk Pik) = CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl ⋯)) Ck.f

The direct transition is compatible with f_i, f_k on the triple overlap.

theorem AnalyticSpace.Glue.pairLift_comp_compTrans {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) : CategoryTheory.CategoryStruct.comp (pairLift Ci ⋯ (tripleDomain Pij Pjk Pik) ⋯) (compTrans Pij Pjk Pik) = CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl ⋯)) Ck.f

The composite transition is compatible with f_i, f_k on the triple overlap.

theorem AnalyticSpace.Glue.toFun_directTrans_mem {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (y : ↑↑(Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (directTrans Pij Pjk Pik) y ∈ Ck.restrictLeOpens (Ui ⊓ Uj ⊓ Uk)

The direct transition sends the common domain into Y_k ∖ f_k(U_k ∖ (U_i ∩ U_j ∩ U_k)).

theorem AnalyticSpace.Glue.toFun_compTrans_mem {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (y : ↑↑(Ci.Y.restrictOpen (tripleDomain Pij Pjk Pik)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (compTrans Pij Pjk Pik) y ∈ Ck.restrictLeOpens (Ui ⊓ Uj ⊓ Uk)

The composite transition sends the common domain into Y_k ∖ f_k(U_k ∖ (U_i ∩ U_j ∩ U_k)).

theorem AnalyticSpace.Glue.exists_cocycle_nhd {X : AnalyticSpace ℝ} {Ui Uj Uk : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} {Ck : (X.restrictOpen Uk).Complexification} (Pij : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) (Pjk : PairIso Cj Ck (Uj ⊓ Uk) ⋯ ⋯) (Pik : PairIso Ci Ck (Ui ⊓ Uk) ⋯ ⋯) (huniq : ∀ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (C C' : (X.restrictOpen V).Complexification) (W : TopologicalSpace.Opens ↑↑C.Y.toPresheafedSpace) (hW : ∀ (x : ↑↑(X.restrictOpen V).complexify.toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C.f x ∈ W) (g₁ g₂ : C.Y.restrictOpen W ⟶ C'.Y.toKLocallyRingedSpace), CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.Hom.restrictTo C.f ⊤ W ⋯) g₁ = CategoryTheory.CategoryStruct.comp ((X.restrictOpen V).complexify.ofRestrict ⊤) C'.f → CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.Hom.restrictTo C.f ⊤ W ⋯) g₂ = CategoryTheory.CategoryStruct.comp ((X.restrictOpen V).complexify.ofRestrict ⊤) C'.f → ∃ (W₀ : TopologicalSpace.Opens ↑↑C.Y.toPresheafedSpace) (hle : W₀ ≤ W), (∀ (x : ↑↑(X.restrictOpen V).complexify.toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C.f x ∈ W₀) ∧ CategoryTheory.CategoryStruct.comp (C.Y.restrictOpenIncl hle) g₁ = CategoryTheory.CategoryStruct.comp (C.Y.restrictOpenIncl hle) g₂) : ∃ (N : TopologicalSpace.Opens ↑↑Ci.Y.toPresheafedSpace) (hle : N ≤ tripleDomain Pij Pjk Pik), (∀ (v : ↑↑(X.restrictOpen (Ui ⊓ Uj ⊓ Uk)).toPresheafedSpace), KLocallyRingedSpace.Hom.toFun Ci.f ⟨↑v, ⋯⟩ ∈ N) ∧ CategoryTheory.CategoryStruct.comp (Ci.Y.restrictOpenIncl hle) (compTrans Pij Pjk Pik) = CategoryTheory.CategoryStruct.comp (Ci.Y.restrictOpenIncl hle) (directTrans Pij Pjk Pik)

The cocycle near the real points. Under the uniqueness hypothesis huniq (two morphisms out of a neighbourhood of the real points of one complexification into another, both compatible with the structure maps, agree on a smaller such neighbourhood), the composite φ_jk ∘ φ_ij and the direct φ_ik agree on an open subset N ⊆ D containing f_i(U_i ∩ U_j ∩ U_k).