Open subspaces: helper isomorphisms and local embeddings

Three small consequences of the universal property of open immersions (KLocallyRingedSpace.isoOfRangeEq: two open immersions of K-local-ringed spaces with the same image are K-isomorphic), and Hironaka's local embeddings.

• restrictOpenTopIso : X | ⊤ ≅ X; restrictOpenIso: a K-isomorphism X ≅ Y restricts to X | e⁻¹V ≅ Y | V; restrictOpen_restrictOpen_iso: (X | U) | V ≅ X | (image of V) (imageOpens). Each is isoOfRangeEq of two open immersions into the same space.
• exists_kIso_localModel: every point of an analytic K-space has an open neighbourhood K-isomorphic to a local analytic K-space, the literal form of Hironaka's clause (i) [Hir64, Ch. 0, §1, p. 120], obtained from the form of the definition (an open of a local model) through Hironaka/AnalyticSpace/LocalModelRestrict.lean; exists_finite_cover_by_localModels_of_isCompact_closure: a set with compact closure is covered by finitely many such neighbourhoods (a finite subcover of the compact closure by the neighbourhoods of its points). Hironaka's remark that a relatively compact open embeds properly into some ℝ^N [Hir64, Ch. 0, §1, footnote 10] is not needed: the resolution of an analytic space is assembled locally and glued.

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictOpenTopIso {K : Type} [RCLike K] (X : KLocallyRingedSpace K) : X.restrictOpen ⊤ ≅ X

The restriction to the whole space is the space: X | ⊤ ≅ X.

Equations

• X.restrictOpenTopIso = AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq (X.ofRestrict ⊤) (CategoryTheory.CategoryStruct.id X) ⋯

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictOpenIso {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (e : X ≅ Y) (V : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : X.restrictOpen ((TopologicalSpace.Opens.map (↑e.hom).base).obj V) ≅ Y.restrictOpen V

A K-isomorphism restricts to the open subspaces over an open V of the target.

Equations

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

instance AnalyticSpace.KLocallyRingedSpace.isOpenImmersion_ofRestrict_comp_ofRestrict {K : Type} [RCLike K] {X : KLocallyRingedSpace K} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(CategoryTheory.CategoryStruct.comp ((X.restrictOpen U).ofRestrict V) (X.ofRestrict U))

The restriction of a restriction is the restriction to the image open.

def AnalyticSpace.KLocallyRingedSpace.imageOpens {K : Type} [RCLike K] {X : KLocallyRingedSpace K} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

The image in X of an open V of the open subspace X | U.

Equations

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

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictOpen_restrictOpen_iso {K : Type} [RCLike K] {X : KLocallyRingedSpace K} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) : (X.restrictOpen U).restrictOpen V ≅ X.restrictOpen (imageOpens U V)

The restriction of a restriction is the restriction to the image open.

Equations

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

theorem AnalyticSpace.exists_kIso_localModel {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : ∃ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ U) (n : ℕ) (k : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (f : Fin k → AnalyticFun K n G), Nonempty ((X.restrictOpen U).KIso (localModel K n G f))

Hironaka's clause (i) in its literal form [Hir64, Ch. 0, §1, p. 120]: every point has an open neighbourhood U with X|U K-isomorphic to a local analytic K-space.

theorem AnalyticSpace.exists_finite_cover_by_localModels_of_isCompact_closure {K : Type} [RCLike K] (X : AnalyticSpace K) (U : Set ↑↑X.toPresheafedSpace) (hU : IsCompact (closure U)) : ∃ (s : Finset (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)), U ⊆ ⋃ V ∈ s, ↑V ∧ ∀ V ∈ s, ∃ (n : ℕ) (k : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (f : Fin k → AnalyticFun K n G), Nonempty ((X.restrictOpen V).KIso (localModel K n G f))

A set with compact closure is covered by finitely many open subspaces each K-isomorphic to a local analytic K-space.