Documentation

Hironaka.AnalyticSpace.Glue.Tame

Tame transition data: the graph of a transition closes only on the graph #

For a normalized transition datum P (Hironaka.AnalyticSpace.Glue.Normalize) between the local complexifications (Y_i, f_i), (Y_j, f_j) over V, write P.graph ⊆ Y_i × Y_j for the graph of the transition on its domain, P.realGraph = {(f_i x, f_j x) : x ∈ V} and P.outer = f_i(U_i ∖ V) × f_j(U_j ∖ V) (a closed set, imageDiff). P is tame when closure P.graph avoids P.outer. Then:

graph_inter_real_eq: the graph meets the real points only in the real graph;
closure_graph_inter_real_subset: for tame P, the closure of the graph meets R_i × R_j only in the graph (the three cases of closure_graphOn_inter_prod_subset, Hironaka.AnalyticSpace.Glue.GraphClosure);
exists_tame: for every datum over V = U_i ⊓ U_j there is a tame datum over V (the domain is shrunk by exists_isOpen_graphOn_closure_disjoint, the transition restricted along KIso.restrictToImage, defined here: the restriction of a K-isomorphism of open subspaces to a smaller open subset and its image).

Conventions. The closedness of the real graph uses V = U_i ⊓ U_j (the real graph is the image of the diagonal of U_i × U_j under the closed embedding f_i × f_j); Y_i × Y_j is metrizable (analytic spaces are regular and second countable). For V = ∅ the real graph is empty, outer = R_i × R_j, and tameness says that the closure of the graph contains no pair of real points.

Tameness is the first arrangement in the gluing of local complexifications [BW59, Proposition 1]: it is what makes the transition graphs of the shrunk pieces closed, hence the glued space Hausdorff.

Restricting a `K`-isomorphism of open subspaces to a smaller open and its image #

theorem AnalyticSpace.Glue.KIso.toFun_hom_inv {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (z : ↑↑(B.restrictOpen Ω').toPresheafedSpace) :

KLocallyRingedSpace.Hom.toFun e.hom (KLocallyRingedSpace.Hom.toFun e.inv z) = z

theorem AnalyticSpace.Glue.KIso.toFun_inv_hom {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (y : ↑↑(A.restrictOpen Ω).toPresheafedSpace) :

KLocallyRingedSpace.Hom.toFun e.inv (KLocallyRingedSpace.Hom.toFun e.hom y) = y

theorem AnalyticSpace.Glue.KIso.restrictToImage_le {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (S : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (S' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hS' : ↑S' = Subtype.val '' KLocallyRingedSpace.Hom.toFun e.hom '' {y : ↑↑(A.restrictOpen Ω).toPresheafedSpace | ↑y ∈ S}) :

S' ≤ Ω'

theorem AnalyticSpace.Glue.KIso.range_hom_subset {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (S : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (hS : S ≤ Ω) (S' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hS' : ↑S' = Subtype.val '' KLocallyRingedSpace.Hom.toFun e.hom '' {y : ↑↑(A.restrictOpen Ω).toPresheafedSpace | ↑y ∈ S}) :

Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp (A.restrictOpenIncl hS) (CategoryTheory.CategoryStruct.comp e.hom (B.ofRestrict Ω')))) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun (B.ofRestrict S'))

theorem AnalyticSpace.Glue.KIso.range_inv_subset {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (S : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (_hS : S ≤ Ω) (S' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hS' : ↑S' = Subtype.val '' KLocallyRingedSpace.Hom.toFun e.hom '' {y : ↑↑(A.restrictOpen Ω).toPresheafedSpace | ↑y ∈ S}) :

Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp (B.restrictOpenIncl ⋯) (CategoryTheory.CategoryStruct.comp e.inv (A.ofRestrict Ω)))) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun (A.ofRestrict S))

noncomputable def AnalyticSpace.Glue.KIso.restrictToImage {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (S : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (hS : S ≤ Ω) (S' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hS' : ↑S' = Subtype.val '' KLocallyRingedSpace.Hom.toFun e.hom '' {y : ↑↑(A.restrictOpen Ω).toPresheafedSpace | ↑y ∈ S}) :

(A.restrictOpen S).KIso (B.restrictOpen S')

The restriction of a K-isomorphism A | Ω ≅ B | Ω' to an open S ≤ Ω and its image S'.

Equations

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

Instances For

theorem AnalyticSpace.Glue.KIso.restrictToImage_hom_comp {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (S : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (hS : S ≤ Ω) (S' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hS' : ↑S' = Subtype.val '' KLocallyRingedSpace.Hom.toFun e.hom '' {y : ↑↑(A.restrictOpen Ω).toPresheafedSpace | ↑y ∈ S}) :

CategoryTheory.CategoryStruct.comp (restrictToImage e S hS S' hS').hom (B.ofRestrict S') = CategoryTheory.CategoryStruct.comp (A.restrictOpenIncl hS) (CategoryTheory.CategoryStruct.comp e.hom (B.ofRestrict Ω'))

theorem AnalyticSpace.Glue.KIso.toFun_restrictToImage_hom_val {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {Ω : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} {Ω' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (e : (A.restrictOpen Ω).KIso (B.restrictOpen Ω')) (S : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (hS : S ≤ Ω) (S' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hS' : ↑S' = Subtype.val '' KLocallyRingedSpace.Hom.toFun e.hom '' {y : ↑↑(A.restrictOpen Ω).toPresheafedSpace | ↑y ∈ S}) (y : ↑↑(A.restrictOpen S).toPresheafedSpace) :

↑(KLocallyRingedSpace.Hom.toFun (restrictToImage e S hS S' hS').hom y) = ↑(KLocallyRingedSpace.Hom.toFun e.hom ⟨↑y, ⋯⟩)

The graph of a transition datum #

noncomputable def AnalyticSpace.Glue.PairIso.toMap {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) :

↑↑P.Ωi → ↑↑Cj.Y.toPresheafedSpace

The transition as a map on its domain, valued in Y_j.

Equations

P.toMap y = ↑(AnalyticSpace.KLocallyRingedSpace.Hom.toFun P.e.hom y)

Instances For

theorem AnalyticSpace.Glue.PairIso.continuous_toMap {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) :

Continuous P.toMap

noncomputable def AnalyticSpace.Glue.PairIso.invMap {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) :

↑↑P.Ωj → ↑↑Ci.Y.toPresheafedSpace

The inverse transition as a map on its domain, valued in Y_i.

Equations

P.invMap z = ↑(AnalyticSpace.KLocallyRingedSpace.Hom.toFun P.e.inv z)

Instances For

theorem AnalyticSpace.Glue.PairIso.continuous_invMap {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) :

Continuous P.invMap

def AnalyticSpace.Glue.PairIso.graph {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) :

Set (↑↑Ci.Y.toPresheafedSpace × ↑↑Cj.Y.toPresheafedSpace)

The graph of the transition.

Equations

P.graph = AnalyticSpace.Glue.graphOn P.toMap ↑P.Ωi

Instances For

def AnalyticSpace.Glue.PairIso.realGraph {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) :

Set (↑↑Ci.Y.toPresheafedSpace × ↑↑Cj.Y.toPresheafedSpace)

The real graph {(f_i x, f_j x) : x ∈ V}.

Equations

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

Instances For

def AnalyticSpace.Glue.PairIso.outer {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) :

Set (↑↑Ci.Y.toPresheafedSpace × ↑↑Cj.Y.toPresheafedSpace)

The pairs of real points outside both domains, f_i(U_i ∖ V) × f_j(U_j ∖ V).

Equations

_P.outer = Ci.imageDiff V ×ˢ Cj.imageDiff V

Instances For

def AnalyticSpace.Glue.PairIso.Tame {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) :

A datum is tame when the closure of its graph avoids outer.

Equations

P.Tame = Disjoint (closure P.graph) P.outer

Instances For

theorem AnalyticSpace.Glue.PairIso.isClosed_outer {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) :

IsClosed P.outer

theorem AnalyticSpace.Glue.PairIso.realGraph_subset_graph {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) :

P.realGraph ⊆ P.graph

theorem AnalyticSpace.Glue.PairIso.disjoint_realGraph_outer {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) :

Disjoint P.realGraph P.outer

theorem AnalyticSpace.Glue.PairIso.isClosed_realGraph {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) (hV : Ui ⊓ Uj ≤ V) :

IsClosed P.realGraph

For V = U_i ⊓ U_j the real graph is closed: it is the image of the diagonal of U_i × U_j under the closed embedding f_i × f_j.

theorem AnalyticSpace.Glue.PairIso.mem_imageDiff_of_notMem {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) {y : ↑↑Ci.Y.toPresheafedSpace} (hy : y ∈ Set.range (KLocallyRingedSpace.Hom.toFun Ci.f)) (hΩ : y ∉ P.Ωi) :

y ∈ Ci.imageDiff V

A real point of Y_i outside the domain lies over U_i ∖ V.

theorem AnalyticSpace.Glue.PairIso.mem_imageDiff_of_notMem' {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) {z : ↑↑Cj.Y.toPresheafedSpace} (hz : z ∈ Set.range (KLocallyRingedSpace.Hom.toFun Cj.f)) (hΩ : z ∉ P.Ωj) :

z ∈ Cj.imageDiff V

theorem AnalyticSpace.Glue.PairIso.graph_inter_real_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) :

P.graph ∩ Set.range (KLocallyRingedSpace.Hom.toFun Ci.f) ×ˢ Set.range (KLocallyRingedSpace.Hom.toFun Cj.f) = P.realGraph

The graph meets the real points only in the real graph.

theorem AnalyticSpace.Glue.PairIso.closure_graph_inter_real_subset {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) (hP : P.Tame) :

closure P.graph ∩ Set.range (KLocallyRingedSpace.Hom.toFun Ci.f) ×ˢ Set.range (KLocallyRingedSpace.Hom.toFun Cj.f) ⊆ P.graph

For a tame datum the closure of the graph meets the real points only in the graph.

For every datum over `U_i ⊓ U_j` there is a tame datum #

theorem AnalyticSpace.Glue.PairIso.exists_tame {X : AnalyticSpace ℝ} {Ui Uj : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {Ci : (X.restrictOpen Ui).Complexification} {Cj : (X.restrictOpen Uj).Complexification} (P : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯) :

∃ (P' : PairIso Ci Cj (Ui ⊓ Uj) ⋯ ⋯), P'.Tame