Open subspaces of analytic K-spaces

The restriction (U, 𝒪_X|U) of an analytic K-space to an open subset U is an analytic K-space [Hir64, Ch. 0, §1, p. 120]. This file proves it and defines the restriction of spaces and of morphisms to open subsets in the form used by the statement of the resolution theorem.

• Topology of an analytic K-space (not in the sources; routine): every point has an open neighbourhood homeomorphic to an open subset of a local model, itself a closed subset of an open subset of Kⁿ; hence X is locally compact and, being countable at infinity, second countable (locallyCompactSpace, secondCountableTopology), and every open subset is σ-compact.
• AnalyticSpace.restrictOpen X V: the open subspace X | V, an analytic K-space. The local-model clause for X | V follows from that of X by three applications of KLocallyRingedSpace.isoOfRangeEq; this is what the up-to-an-open form of the clause buys (AnalyticSpace.locallyModel).
• openOf U (U if open, the whole space otherwise), restrictSet X U (X | U for open U, X itself for non-open U) and Hom.restrictSet f V : X | f⁻¹V ⟶ Y | V, the lift of f through the open immersions, in which the resolution theorem is stated: restrictSet X U accepts any set U, and the convention for a non-open U keeps Hom.restrictSet total in V (the alternative convention interior U would leave it uninhabitable for a non-open V with empty interior).
• f.IsIsoOver U: f restricts to an isomorphism f⁻¹(U) → U over the set U, clause (2) of [Kol07, Theorem 45]; total in U by the convention of restrictSet.

theorem AnalyticSpace.locallyCompactSpace_localModel (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : LocallyCompactSpace ↑↑(localModel K n G f).toPresheafedSpace

A local model is locally compact: its support is closed in G.

theorem AnalyticSpace.secondCountableTopology_localModel (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : SecondCountableTopology ↑↑(localModel K n G f).toPresheafedSpace

A local model is second countable: its support is a subset of G ⊆ Kⁿ.

theorem AnalyticSpace.exists_nhd_locallyCompact_secondCountable {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : ∃ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ U), LocallyCompactSpace ↥U ∧ SecondCountableTopology ↥U

Every point of an analytic K-space has an open neighbourhood that is locally compact and second countable: it is homeomorphic to an open subset of a local model.

instance AnalyticSpace.locallyCompactSpace {K : Type} [RCLike K] (X : AnalyticSpace K) : LocallyCompactSpace ↑↑X.toPresheafedSpace

An analytic K-space is locally compact.

instance AnalyticSpace.secondCountableTopology {K : Type} [RCLike K] (X : AnalyticSpace K) : SecondCountableTopology ↑↑X.toPresheafedSpace

An analytic K-space is second countable: it is countable at infinity and every point has a second countable open neighbourhood.

instance AnalyticSpace.instSigmaCompactSpaceSubtypeCarrierCarrierCommRingCatMemOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : SigmaCompactSpace ↥V

Every open subset of an analytic K-space is countable at infinity.

@[reducible, inline]

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

The trace on the open subspace X | V of an open U of X, as an open of X | V.

Equations

• X.traceOpens V U = (TopologicalSpace.Opens.map (↑(X.ofRestrict V)).base).obj U

theorem AnalyticSpace.range_toFun_ofRestrict_ofRestrict {K : Type} [RCLike K] (X : AnalyticSpace K) (V U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((X.restrictOpen V).ofRestrict (X.traceOpens V U)) (X.ofRestrict V))) = ↑V ∩ ↑U

The range of the open immersion (X | V) | U' ⟶ X, U' the trace of U on V, is V ∩ U.

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

The open subspace X | V of an analytic K-space is an analytic K-space [Hir64, Ch. 0, §1, p. 120].

Equations

• X.restrictOpen V = { toKLocallyRingedSpace := X.restrictOpen V, locallyModel := ⋯, t2 := ⋯, sigmaCompact := ⋯ }

noncomputable def AnalyticSpace.openOf {K : Type} [RCLike K] (X : AnalyticSpace K) (U : Set ↑↑X.toPresheafedSpace) : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

The open set to which restrictSet restricts: U itself when it is open, the whole space otherwise (restrictSet X U accepts any set U).

Equations

• X.openOf U = if h : IsOpen U then { carrier := U, is_open' := h } else ⊤

theorem AnalyticSpace.openOf_of_isOpen {K : Type} [RCLike K] (X : AnalyticSpace K) {U : Set ↑↑X.toPresheafedSpace} (h : IsOpen U) : X.openOf U = { carrier := U, is_open' := h }

For an open U, openOf X U is U itself.

theorem AnalyticSpace.openOf_of_not_isOpen {K : Type} [RCLike K] (X : AnalyticSpace K) {U : Set ↑↑X.toPresheafedSpace} (h : ¬IsOpen U) : X.openOf U = ⊤

For a non-open U, openOf X U is the whole space.

noncomputable def AnalyticSpace.restrictSet {K : Type} [RCLike K] (X : AnalyticSpace K) (U : Set ↑↑X.toPresheafedSpace) : AnalyticSpace K

X | U for an open U [Hir64, Ch. 0, §1, p. 120], X itself (restricted along ⊤) for a non-open U.

Equations

• X.restrictSet U = X.restrictOpen (X.openOf U)

theorem AnalyticSpace.range_toFun_ofRestrict_comp_subset {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) (V : Set ↑↑Y.toPresheafedSpace) : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp (X.ofRestrict (X.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' V))) f)) ⊆ Set.range (KLocallyRingedSpace.Hom.toFun (Y.ofRestrict (Y.openOf V)))

The lift condition for Hom.restrictSet: f maps f⁻¹V into V, and the whole space into the whole space.

noncomputable def AnalyticSpace.Hom.restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) (V : Set ↑↑Y.toPresheafedSpace) : X.restrictSet (↑f ⁻¹' V) ⟶ Y.restrictSet V

The restriction f | f⁻¹V : X | f⁻¹V ⟶ Y | V of a morphism to an open subset V of the target, the lift of f through the open immersion Y | V ⟶ Y (total in V by the convention openOf). Its source is written with the coercion ⇑f, as in the morphism types of the resolution theorem.

Equations

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

Isomorphisms over a subset of the target

def AnalyticSpace.Hom.IsIsoOver {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) (U : Set ↑↑X.toPresheafedSpace) : Prop

f restricts to an isomorphism f⁻¹(U) → U over the open set U (clause (2) of the resolution problem of [Hir64, Introduction] and of [Kol07, Theorem 45]).

Equations

• AnalyticSpace.Hom.IsIsoOver f U = CategoryTheory.IsIso (AnalyticSpace.Hom.restrictSet f U)