The local data: cover, shrinking, complexifications, tame transitions

LocalData X bundles the choices of the proof of the gluing theorem for complexifications BW59, Proposition 1: a countable locally finite cover U i of X by relatively compact open subsets, each with a complexification C i of X | U i; a shrinking V i (closure (V i) ⊆ U i, still covering); and for every pair a tame normalized transition datum P i j over U i ⊓ U j (Hironaka.AnalyticSpace.Glue.Normalize, Hironaka.AnalyticSpace.Glue.Tame), the identity on the diagonal. exists_localData produces one from the hypotheses hloc (local existence of complexifications) and hiso (local isomorphisms near the real points) of the gluing theorem: the cover by exists_locallyFinite_cover (the property of admitting a complexification is stable under Complexification.restrictLe), the shrinking by the shrinking lemma (X is paracompact and Hausdorff, hence normal), the transitions by PairIso.ofHiso and PairIso.exists_tame. The two covers are the pair of locally finite covers V_i ⊆ U_i of the proof of [Car57, §3, Proposition 2].

Conventions. The diagonal datum is PairIso.refl transported along U i = U i ⊓ U i (PairIso.ofEq); it is tame because its outer set is empty. For X = ∅ any countable index type works (the empty cover; LocalData.countable asks for countability); for a finite index type the local finiteness is automatic.

noncomputable def AnalyticSpace.Glue.PairIso.ofEq {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') (hVi' : V' ≤ Ui) (hVj' : V' ≤ Uj) : PairIso Ci Cj V' hVi' hVj'

Transport of a datum along an equality of the base open V = V'.

Equations

• P.ofEq h hVi' hVj' = { Ωi := P.Ωi, Ωj := P.Ωj, e := P.e, mem_Ωi := ⋯, mem_Ωj := ⋯, Ωi_le := ⋯, Ωj_le := ⋯, compat := ⋯ }

theorem AnalyticSpace.Glue.PairIso.tame_refl_ofEq {X : AnalyticSpace ℝ} {Ui : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (Ci : (X.restrictOpen Ui).Complexification) (h : Ui = Ui ⊓ Ui) : ((refl Ci).ofEq h ⋯ ⋯).Tame

The diagonal datum is tame: its outer set is empty.

noncomputable def AnalyticSpace.Glue.diagDatum {X : AnalyticSpace ℝ} {J : Type u} (U : J → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (C : (i : J) → (X.restrictOpen (U i)).Complexification) (i j : J) (h : i = j) : PairIso (C i) (C j) (U i ⊓ U j) ⋯ ⋯

The diagonal datum P i i, the identity transition transported to the pair type.

Equations

• AnalyticSpace.Glue.diagDatum U C i j h = h ▸ (AnalyticSpace.Glue.PairIso.refl (C i)).ofEq ⋯ ⋯ ⋯

theorem AnalyticSpace.Glue.diagDatum_rfl {X : AnalyticSpace ℝ} {J : Type u} (U : J → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (C : (i : J) → (X.restrictOpen (U i)).Complexification) (i : J) : diagDatum U C i i ⋯ = (PairIso.refl (C i)).ofEq ⋯ ⋯ ⋯

structure AnalyticSpace.Glue.LocalData (X : AnalyticSpace ℝ) : Type (u + 1)

The local data of the proof of the gluing theorem for complexifications.

• J : Type u

  The index type of the cover.

• countable : Countable self.J
• U : self.J → TopologicalSpace.Opens ↑↑X.toPresheafedSpace

  The cover.

• lf : LocallyFinite fun (i : self.J) => ↑(self.U i)
• cpt (i : self.J) : IsCompact (closure ↑(self.U i))
• cover : ⋃ (i : self.J), ↑(self.U i) = Set.univ
• C (i : self.J) : (X.restrictOpen (self.U i)).Complexification

  The local complexifications.

• V : self.J → TopologicalSpace.Opens ↑↑X.toPresheafedSpace

  The shrinking.

• closure_V_subset (i : self.J) : closure ↑(self.V i) ⊆ ↑(self.U i)
• V_cover : ⋃ (i : self.J), ↑(self.V i) = Set.univ
• P (i j : self.J) : PairIso (self.C i) (self.C j) (self.U i ⊓ self.U j) ⋯ ⋯

  The tame transition data, the identity on the diagonal.

• tame (i j : self.J) : (self.P i j).Tame
• P_diag (i : self.J) : self.P i i = (PairIso.refl (self.C i)).ofEq ⋯ ⋯ ⋯

theorem AnalyticSpace.Glue.exists_localData {X : AnalyticSpace ℝ} (hloc : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), x ∈ U ∧ Nonempty (X.restrictOpen U).Complexification) (hiso : ∀ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (C C' : (X.restrictOpen V).Complexification), ∃ (W : TopologicalSpace.Opens ↑↑C.Y.toPresheafedSpace) (W' : TopologicalSpace.Opens ↑↑C'.Y.toPresheafedSpace) (hW : ∀ (x : ↑↑(X.restrictOpen V).complexify.toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C.f x ∈ W) (hW' : ∀ (x : ↑↑(X.restrictOpen V).complexify.toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C'.f x ∈ W') (e : (C.Y.restrictOpen W).KIso (C'.Y.restrictOpen W')), CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.Hom.restrictTo C.f ⊤ W ⋯) e.hom = KLocallyRingedSpace.Hom.restrictTo C'.f ⊤ W' ⋯) : Nonempty (LocalData X)

The existence of the local data from the hypotheses hloc and hiso of the gluing theorem.