The morphism from X(ℂ) to the glued space

The complexified space X(ℂ) is covered by the open subsets U'_i = {x ∈ U_i | f_i x ∈ A_i} (every x lies in some V_i, and f_i(closure V_i) = core i ⊆ A_i); on X(ℂ) | U'_i the morphism g_i is f_i lifted into the piece Y_i | A_i, followed by the open immersion ιK i into the glued K-space (coverHom); on an overlap U'_i ∩ U'_j the two lifts agree because f_i lands in W_ij there, the transition carries it to f_j (PairIso.compat_restrict), and the glue condition identifies ι_i with t_ij ≫ ι_j on W_ij. Presenting X(ℂ) as the gluing of its own cover (coverIso, Hironaka.AnalyticSpace.Glue.Trivial) and descending (descK), the g_i assemble to toGluedK : X(ℂ) ⟶ gluedK with ofRestrict U'_i ≫ toGluedK = g_i; on points, toGluedK x = ι_i (f_i x) for any i with x ∈ U'_i.

Conventions. pieceLiftOn i hV : (X | V)(ℂ) ⟶ Y_i | A_i is pairLift of f_i for V ≤ U'_i; overlapIso identifies the overlap piece (X(ℂ) | U'_i) | U'_j of the gluing data of the cover with X(ℂ) | (U'_i ⊓ U'_j), and comp_complexifyRestrictIso_inv moves any inclusion of it into X(ℂ) | U'_k through the identification (X | U)(ℂ) ≅ X(ℂ) | U (complexifyRestrictIso). For i = j, W_ii = ⊤ and the compatibility is the identity; for disjoint U'_i, U'_j the overlap piece is empty.

theorem AnalyticSpace.Glue.KGlueData.ofRestrict_comp_ιK {K : Type} [RCLike K] (D : KGlueData K) (i j : D.J) : CategoryTheory.CategoryStruct.comp ((D.Y i).ofRestrict (D.W i j)) (D.ιK i) = CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp ((D.Y j).ofRestrict (D.W j i)) (D.ιK j))

The glue condition of K-gluing data at the level of K-morphisms.

The cover U'_i = f_i⁻¹(A_i) of X

theorem AnalyticSpace.Glue.Shrunk.isOpen_coverSet {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : IsOpen {x : ↑↑X.toPresheafedSpace | ∃ (h : x ∈ D.U i), KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨x, h⟩ ∈ S.A i}

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

The open U'_i = {x ∈ U_i | f_i x ∈ A_i}.

Equations

• S.coverOpens i = { carrier := {x : ↑↑X.toPresheafedSpace | ∃ (h : x ∈ D.U i), AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨x, h⟩ ∈ S.A i}, is_open' := ⋯ }

theorem AnalyticSpace.Glue.Shrunk.mem_coverOpens {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i : D.J} {x : ↑↑X.toPresheafedSpace} : x ∈ S.coverOpens i ↔ ∃ (h : x ∈ D.U i), KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨x, h⟩ ∈ S.A i

theorem AnalyticSpace.Glue.Shrunk.coverOpens_le {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : S.coverOpens i ≤ D.U i

theorem AnalyticSpace.Glue.Shrunk.toFun_mem_A {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i : D.J} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ S.coverOpens i) (v : ↑↑(X.restrictOpen V).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨↑v, ⋯⟩ ∈ S.A i

theorem AnalyticSpace.Glue.Shrunk.exists_mem_coverOpens {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (x : ↑↑X.complexify.toPresheafedSpace) : ∃ (i : D.J), x ∈ S.coverOpens i

The U'_i cover X: x ∈ V_i gives f_i x ∈ core i ⊆ A_i.

The lifts of the f_i into the pieces

noncomputable def AnalyticSpace.Glue.Shrunk.pieceLiftOn {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ S.coverOpens i) : (X.restrictOpen V).complexify ⟶ S.piece i

f_i on (X | V)(ℂ), V ≤ U'_i, lifted into the piece Y_i | A_i.

Equations

• S.pieceLiftOn i hV = AnalyticSpace.Glue.pairLift (D.C i) ⋯ (S.A i) ⋯

theorem AnalyticSpace.Glue.Shrunk.pieceLiftOn_comp_ofRestrict {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ S.coverOpens i) : CategoryTheory.CategoryStruct.comp (S.pieceLiftOn i hV) ((D.C i).Y.ofRestrict (S.A i)) = CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl ⋯)) (D.C i).f

theorem AnalyticSpace.Glue.Shrunk.complexifyIncl_comp_pieceLiftOn {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) {V V' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ S.coverOpens i) (hV' : V' ≤ V) : CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl hV')) (S.pieceLiftOn i hV) = S.pieceLiftOn i ⋯

theorem AnalyticSpace.Glue.Shrunk.complexifyIncl_comp_pieceLiftOn_assoc {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) {V V' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ S.coverOpens i) (hV' : V' ≤ V) {Z : KLocallyRingedSpace ℂ} (h : S.piece i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl hV')) (S.pieceLiftOn i hV)) h = CategoryTheory.CategoryStruct.comp (S.pieceLiftOn i ⋯) h

theorem AnalyticSpace.Glue.Shrunk.toFun_pieceLiftOn_val {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : V ≤ S.coverOpens i) (v : ↑↑(X.restrictOpen V).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (S.pieceLiftOn i hV) v) = KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨↑v, ⋯⟩

The compatibility on the overlaps

theorem AnalyticSpace.Glue.Shrunk.overlap_le_left {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : S.coverOpens i ⊓ S.coverOpens j ≤ D.U i ⊓ D.U j

theorem AnalyticSpace.Glue.Shrunk.toFun_mem_WOpen_overlap {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) (v : ↑↑(X.restrictOpen (S.coverOpens i ⊓ S.coverOpens j)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (D.C i).f ⟨↑v, ⋯⟩ ∈ S.WOpen i j

On the overlap, f_i lands in the gluing open W_ij.

theorem AnalyticSpace.Glue.Shrunk.range_pieceLiftOn_overlap_subset {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : Set.range (KLocallyRingedSpace.Hom.toFun (S.pieceLiftOn i ⋯)) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun ((S.piece i).ofRestrict (S.W i j)))

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

f_i on the overlap, lifted into (Y_i | A_i) | W_ij.

Equations

• S.overlapLift i j = AnalyticSpace.Glue.liftAlong ((S.piece i).ofRestrict (S.W i j)) (S.pieceLiftOn i ⋯) ⋯

theorem AnalyticSpace.Glue.Shrunk.overlapLift_comp_ofRestrict {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (S.overlapLift i j) ((S.piece i).ofRestrict (S.W i j)) = S.pieceLiftOn i ⋯

theorem AnalyticSpace.Glue.Shrunk.overlapLift_comp_ι {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (S.overlapLift i j) (S.ι i j) = pairLift (D.C i) ⋯ (D.P i j).Ωi ⋯

theorem AnalyticSpace.Glue.Shrunk.overlapLift_comp_t {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (S.overlapLift i j) (CategoryTheory.CategoryStruct.comp (S.t i j) ((S.piece j).ofRestrict (S.W j i))) = S.pieceLiftOn j ⋯

The transition carries the lift of f_i to the lift of f_j (PairIso.compat restricted to the overlap).

theorem AnalyticSpace.Glue.Shrunk.pieceLiftOn_comp_ιK {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (S.pieceLiftOn i ⋯) (S.data.ιK i) = CategoryTheory.CategoryStruct.comp (S.pieceLiftOn j ⋯) (S.data.ιK j)

The two lifts of the overlap into the glued K-space agree.

The morphisms on the cover and their descent

noncomputable def AnalyticSpace.Glue.Shrunk.coverHom {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : X.complexify.restrictOpen (S.coverOpens i) ⟶ S.data.gluedK

The morphism X(ℂ) | U'_i ⟶ gluedK: f_i lifted into the piece, then the open immersion.

Equations

• S.coverHom i = CategoryTheory.CategoryStruct.comp (X.complexifyRestrictIso (S.coverOpens i)).inv (CategoryTheory.CategoryStruct.comp (S.pieceLiftOn i ⋯) (S.data.ιK i))

noncomputable def AnalyticSpace.Glue.Shrunk.overlapIso {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : (X.complexify.restrictOpen (S.coverOpens i)).restrictOpen (coverW X.complexify S.coverOpens i j) ≅ X.complexify.restrictOpen (S.coverOpens i ⊓ S.coverOpens j)

The overlap piece of the trivial gluing data of the cover is X(ℂ) | (U'_i ⊓ U'_j).

Equations

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

theorem AnalyticSpace.Glue.Shrunk.overlapIso_hom_comp {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (S.overlapIso i j).hom (X.complexify.ofRestrict (S.coverOpens i ⊓ S.coverOpens j)) = incl₂ X.complexify (S.coverOpens i) (coverW X.complexify S.coverOpens i j)

theorem AnalyticSpace.Glue.Shrunk.comp_complexifyRestrictIso_inv {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) {i j k : D.J} (hk : S.coverOpens i ⊓ S.coverOpens j ≤ S.coverOpens k) (a : (X.complexify.restrictOpen (S.coverOpens i)).restrictOpen (coverW X.complexify S.coverOpens i j) ⟶ X.complexify.restrictOpen (S.coverOpens k)) (ha : CategoryTheory.CategoryStruct.comp a (X.complexify.ofRestrict (S.coverOpens k)) = incl₂ X.complexify (S.coverOpens i) (coverW X.complexify S.coverOpens i j)) : CategoryTheory.CategoryStruct.comp a (X.complexifyRestrictIso (S.coverOpens k)).inv = CategoryTheory.CategoryStruct.comp (S.overlapIso i j).hom (CategoryTheory.CategoryStruct.comp (X.complexifyRestrictIso (S.coverOpens i ⊓ S.coverOpens j)).inv (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl hk)))

Any inclusion of the overlap piece into X(ℂ) | U'_k, followed by the identification with (X | U'_k)(ℂ), is the identification of the overlap followed by the complexified inclusion.

theorem AnalyticSpace.Glue.Shrunk.ofRestrict_comp_coverHom {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp ((X.complexify.restrictOpen (S.coverOpens i)).ofRestrict (coverW X.complexify S.coverOpens i j)) (S.coverHom i) = CategoryTheory.CategoryStruct.comp (S.overlapIso i j).hom (CategoryTheory.CategoryStruct.comp (X.complexifyRestrictIso (S.coverOpens i ⊓ S.coverOpens j)).inv (CategoryTheory.CategoryStruct.comp (S.pieceLiftOn i ⋯) (S.data.ιK i)))

theorem AnalyticSpace.Glue.Shrunk.coverT_comp_ofRestrict_comp_coverHom {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (coverT X.complexify S.coverOpens i j) ((X.complexify.restrictOpen (S.coverOpens j)).ofRestrict (coverW X.complexify S.coverOpens j i))) (S.coverHom j) = CategoryTheory.CategoryStruct.comp (S.overlapIso i j).hom (CategoryTheory.CategoryStruct.comp (X.complexifyRestrictIso (S.coverOpens i ⊓ S.coverOpens j)).inv (CategoryTheory.CategoryStruct.comp (S.pieceLiftOn j ⋯) (S.data.ιK j)))

theorem AnalyticSpace.Glue.Shrunk.compat {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i j : D.J) : CategoryTheory.CategoryStruct.comp ((coverData X.complexify S.coverOpens).f i j) ↑(S.coverHom i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑((coverData X.complexify S.coverOpens).t i j)) ((coverData X.complexify S.coverOpens).f j i)) ↑(S.coverHom j)

The compatibility of the g_i on the overlaps, in the form the descent takes.

noncomputable def AnalyticSpace.Glue.Shrunk.toGluedK {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) : X.complexify ⟶ S.data.gluedK

The morphism X(ℂ) ⟶ gluedK: the descent of the g_i along the presentation of X(ℂ) as the gluing of its cover.

Equations

• S.toGluedK = CategoryTheory.CategoryStruct.comp (AnalyticSpace.Glue.coverIso X.complexify S.coverOpens ⋯).inv ((AnalyticSpace.Glue.coverData X.complexify S.coverOpens).descK S.coverHom ⋯)

theorem AnalyticSpace.Glue.Shrunk.ofRestrict_comp_toGluedK {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) : CategoryTheory.CategoryStruct.comp (X.complexify.ofRestrict (S.coverOpens i)) S.toGluedK = S.coverHom i

theorem AnalyticSpace.Glue.Shrunk.toFun_toGluedK {X : AnalyticSpace ℝ} {D : LocalData X} {huniq : Huniq X} (S : Shrunk D huniq) (i : D.J) (x : ↑↑(X.complexify.restrictOpen (S.coverOpens i)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun S.toGluedK ↑x = KLocallyRingedSpace.Hom.toFun (S.data.ιK i) (KLocallyRingedSpace.Hom.toFun (S.pieceLiftOn i ⋯) x)

On points, toGluedK x = ι_i (f_i x) for x ∈ U'_i.