The direct limit of a compatible family #
From a compatible family C : CompatibleFamily T and a compact exhaustion Kex of M, the
extension-compatible family AnalyticManifold.ExtensionCompatibleFamily M of the main
theorems ([Wlo09, Theorem 2.0.3, (1) and (4)]; [Wlo09, §4.1]; [Kol07, 44]; [BM97, §1] on
non-compact analytic spaces): the end results M'_n of the values on the relatively compact opens
M_n = relCompactOpen Kex n form an ℕ-chain along the end-result embeddings
(CompatibleFamily.endResultChain), whose direct limit is the space M̃
(CompatibleFamily.endResultLimit); the composite blow-downs M'_n → M_n ⊆ M glue to
σ : M̃ → M (CompatibleFamily.limitBlowDown, Włodarczyk's prin : M̃ → M) with
σ⁻¹(M_n) = M'_n (CompatibleFamily.limitBlowDown_preimage_relCompactOpen); and the fields of
the extension-compatible family follow one by one (ExtensionCompatibleFamily.ofCompatibleFamily):
nhd K is the first M_n ⊇ K (relCompactOpenIndex, monotone in K by Nat.find_mono),
seq K the family's value on it, toSpace K the inclusion of the piece M'_n into the limit,
map_toSpace the glued square, toSpace_isIso (U_r = Ũ in [Wlo09, Theorem 2.0.3, (1)]) from
σ⁻¹(M_n) = M'_n, and isExtensionOf_restrict the extension clause at U₁ := nhd K₁,
U₂ := nhd K₂.
The four properties of the end-result embeddings (analytic open embeddings, over M, onto the
preimage of the smaller open, and the restriction an extension) enter every declaration below as
the hypotheses hemb, hcomp, hrange, hext; they are proved in
Hironaka.Resolution.Analytic.Functor.EndResultEmbeddingLemmas, which this module does not
import, and supplied where the family is built as resolveFamExt
(Hironaka.Resolution.Analytic.Wlo09.FamilyExt).
exists_subset_relCompactOpen,relCompactOpenIndex,subset_relCompactOpen_index,relCompactOpenIndex_mono: the firstM_ncontaining a compact set.CompatibleFamily.endResultOn,CompatibleFamily.endResultChain,CompatibleFamily.blowDownOn,CompatibleFamily.blowDownOn_endResultEmbedding,CompatibleFamily.range_endResultChain_ι.CompatibleFamily.endResultLimit,CompatibleFamily.limitBlowDown,CompatibleFamily.limitBlowDown_preimage_relCompactOpen.ExtensionCompatibleFamily.ofCompatibleFamily.
The first relatively compact open of the exhaustion containing a compact set #
Every compact set lies in some M_n = relCompactOpen Kex n
(CompactExhaustion.exists_superset_of_isCompact, K n ⊆ int K (n+1)).
The first index n with
K ⊆ M_n.
Equations
Instances For
K ⊆ M_{relCompactOpenIndex K} (subset_nhd).
The index is monotone in K (nhd_mono; [Wlo09, Theorem 2.0.3, (4)], for opens U₁ ⊂ U₂).
The end results of a compatible family along the exhaustion, as a chain #
The end result M'_m of the family's value on M_m = relCompactOpen Kex m
(relatively compact).
Equations
- C.endResultOn Kex m = (C.seqOn (Manifold.relCompactOpen Kex m) ⋯).stage (Fin.last (C.seqOn (Manifold.relCompactOpen Kex m) ⋯).length)
Instances For
The end results along the exhaustion
M_0 ⊆ M_1 ⊆ ⋯, with embeddings as the transition maps, as an ℕ-chain of analytic open
embeddings — given isAnalyticOpenEmbedding_endResultEmbedding as hemb.
Equations
- C.endResultChain Kex hemb = { X := fun (m : ℕ) => C.endResultOn Kex m, ι := fun (m : ℕ) => C.endResultEmbedding ⋯ ⋯ ⋯, isAnalyticOpenEmbedding := ⋯ }
Instances For
The composite blow-down Π^{(m)} : M'_m → M_m ⊆ M of the end result over
M_m, read in M.
Equations
- C.blowDownOn Kex m = ContMDiffMap.comp (M.inclusion (Manifold.relCompactOpen Kex m)) (C.seqOn (Manifold.relCompactOpen Kex m) ⋯).toSuccession.composite
Instances For
The blow-downs are compatible with the embeddings:
composite_endResultEmbedding (hcomp) read in M, where the inclusion M_m ⊆ M_{m+1}
disappears.
The range of the embedding M'_m → M'_{m+1} is the preimage of M_m under the
blow-down of M'_{m+1} — range_endResultEmbedding (hrange) with
range_restrictLE.
The
direct limit M̃ = ⋃ₙ M'_n of the end results.
Equations
- C.endResultLimit Kex hemb = (C.endResultChain Kex hemb).limitManifold
Instances For
The blow-down σ : M̃ → M
of the direct limit, the Π^{(m)} glued.
Equations
- C.limitBlowDown Kex hemb hcomp = (C.endResultChain Kex hemb).limitDesc (C.blowDownOn Kex) ⋯
Instances For
σ⁻¹(M_m) is the m-th piece M'_m of the limit.
The extension-compatible family ExtensionCompatibleFamily M from a compatible family and a
compact exhaustion: the space is the direct limit of the end results, the map its blow-down, the
neighbourhood of a compact K the first M_n ⊇ K, the succession over it the family's value
there, the identification of the end result with σ⁻¹(M_n) the inclusion of the piece, and the
extension clause that of the end-result embeddings. The four properties of the end-result
embeddings are the hypotheses hemb, hcomp, hrange, hext (see the module docstring).
Equations
- One or more equations did not get rendered due to their size.