Restriction of a complexification to an open subspace

If (Y, f) is a complexification of the open subspace X | U of an analytic ℝ-space X (Complexification, Hironaka.AnalyticSpace.Complexification; the analytic complexifications of [Hir64, Ch. 0, §1, p. 120]: f(X) closed in Y, f a ℂ-isomorphism of X(ℂ) onto Y | f(X)) and V ≤ U is a smaller open subset, then (Y | W, f | V) with W = Y ∖ f(U ∖ V) is a complexification of X | V (Complexification.restrictLe). This is the elementary step of the gluing of local complexifications [BW59, Proposition 1]: the local complexifications of a cover are restricted to the overlaps before their germs are compared. Also here: complexifyIso, the complexification of a K-isomorphism of ℝ-spaces as a ℂ-isomorphism (complexifyHom in both directions), which transports a complexification along an isomorphism of the real space.

Conventions. f(U ∖ V) is closed in Y (isClosed_imageDiff): f(U) is closed and f(U ∩ V) is open in f(U) because f is an embedding, so f(U ∖ V) = f(U) ∖ f(U ∩ V) is closed. The restricted morphism restrictLeHom is f | V composed with the identification (X | U) | V ≅ X | V (restrictOpen_restrictOpen_iso, imageOpens_map_eq) and with complexifyRestrictIso (Hironaka.AnalyticSpace.Complexify); its stalk maps are conjugate to those of f by the stalk isomorphisms of the open immersions (KLocallyRingedSpace.isIso_ofRestrict_stalkMap) and of the K-isomorphisms. For V = U, W = Y and the restriction is f up to the identifications; for V = ⊥, X | ⊥ is empty, W = Y ∖ f(U), and the empty morphism is a complexification.

def AnalyticSpace.KLocallyRingedSpace.complexifyIso {A B : KLocallyRingedSpace ℝ} [A.HasRealResidueFields] [B.HasRealResidueFields] (e : A.KIso B) : A.complexify.KIso B.complexify

The complexification of a K-isomorphism of ℝ-spaces is a ℂ-isomorphism.

Equations

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

def AnalyticSpace.Complexification.fK {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) : (X.restrictOpen U).complexify ⟶ C.Y.toKLocallyRingedSpace

The morphism f of the complexification, typed on X.toK | U (the same term; the uniform typing lets the restriction lemmas of Hironaka.AnalyticSpace.OpenSubspaceLemmas apply syntactically).

Equations

• C.fK = C.f

theorem AnalyticSpace.Complexification.toFun_fK {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) : KLocallyRingedSpace.Hom.toFun C.fK = KLocallyRingedSpace.Hom.toFun C.f

def AnalyticSpace.Complexification.imageDiff {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Set ↑↑C.Y.toPresheafedSpace

The image f(U ∖ V) of the real points of U outside V.

Equations

• C.imageDiff V = AnalyticSpace.KLocallyRingedSpace.Hom.toFun C.f '' {u : ↑↑(X.restrictOpen U).toPresheafedSpace | ↑u ∉ V}

theorem AnalyticSpace.Complexification.mem_imageDiff {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {y : ↑↑C.Y.toPresheafedSpace} : y ∈ C.imageDiff V ↔ ∃ (u : ↑↑(X.restrictOpen U).toPresheafedSpace), ↑u ∉ V ∧ KLocallyRingedSpace.Hom.toFun C.f u = y

theorem AnalyticSpace.Complexification.isClosed_imageDiff {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : IsClosed (C.imageDiff V)

f(U ∖ V) is closed in Y: f(U) is closed and f(U ∩ V) is open in it.

def AnalyticSpace.Complexification.restrictLeOpens {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : TopologicalSpace.Opens ↑↑C.Y.toPresheafedSpace

The open W = Y ∖ f(U ∖ V) on which the restricted complexification lives.

Equations

• C.restrictLeOpens V = { carrier := (C.imageDiff V)ᶜ, is_open' := ⋯ }

theorem AnalyticSpace.Complexification.mem_restrictLeOpens {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {y : ↑↑C.Y.toPresheafedSpace} : y ∈ C.restrictLeOpens V ↔ ∀ (u : ↑↑(X.restrictOpen U).toPresheafedSpace), KLocallyRingedSpace.Hom.toFun C.f u = y → ↑u ∈ V

theorem AnalyticSpace.Complexification.toFun_mem_restrictLeOpens {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (u : ↑↑(X.restrictOpen U).toPresheafedSpace) (hu : ↑u ∈ V) : KLocallyRingedSpace.Hom.toFun C.f u ∈ C.restrictLeOpens V

The real points of V land in W.

noncomputable def AnalyticSpace.Complexification.pullbackOpens {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace

V as an open of X | U.

Equations

• AnalyticSpace.Complexification.pullbackOpens V = (TopologicalSpace.Opens.map (↑(X.ofRestrict U)).base).obj V

theorem AnalyticSpace.Complexification.mem_pullbackOpens {X : AnalyticSpace ℝ} {U V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {u : ↑↑(X.restrictOpen U).toPresheafedSpace} : u ∈ pullbackOpens V ↔ ↑u ∈ V

noncomputable def AnalyticSpace.Complexification.restrictRestrictIso {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hV : V ≤ U) : (X.restrictOpen U).restrictOpen (pullbackOpens V) ≅ X.restrictOpen V

The identification (X | U) | V ≅ X | V for V ≤ U (restrictOpen_restrictOpen_iso).

Equations

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

noncomputable def AnalyticSpace.Complexification.restrictFun {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : ↑↑((X.restrictOpen U).restrictOpen (pullbackOpens V)).toPresheafedSpace → ↥(C.restrictLeOpens V)

The pointwise form of f | V: u ↦ f(u) into W.

Equations

• C.restrictFun V u = ⟨AnalyticSpace.KLocallyRingedSpace.Hom.toFun C.fK ↑u, ⋯⟩

theorem AnalyticSpace.Complexification.isEmbedding_restrictFun {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Topology.IsEmbedding (C.restrictFun V)

noncomputable def AnalyticSpace.Complexification.restrictLeHom {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hV : V ≤ U) : (X.restrictOpen V).complexify ⟶ (C.Y.restrictOpen (C.restrictLeOpens V)).toKLocallyRingedSpace

The restricted morphism f | V : (X | V)(ℂ) ⟶ Y | W.

Equations

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

theorem AnalyticSpace.Complexification.toFun_restrictLeHom {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hV : V ≤ U) : KLocallyRingedSpace.Hom.toFun (C.restrictLeHom V hV) = C.restrictFun V ∘ KLocallyRingedSpace.Hom.toFun (restrictRestrictIso V hV).inv

theorem AnalyticSpace.Complexification.range_toFun_restrictLeHom {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hV : V ≤ U) : Set.range (KLocallyRingedSpace.Hom.toFun (C.restrictLeHom V hV)) = Subtype.val ⁻¹' Set.range (KLocallyRingedSpace.Hom.toFun C.f)

The range of the restricted morphism is the trace of f(U) on W.

theorem AnalyticSpace.Complexification.bijective_stalkMap_restrictLeHom {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hV : V ≤ U) (v : ↑↑(X.restrictOpen V).complexify.toPresheafedSpace) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(C.restrictLeHom V hV)) v))

The stalk maps of the restricted morphism are bijective.

noncomputable def AnalyticSpace.Complexification.restrictLe {X : AnalyticSpace ℝ} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (C : (X.restrictOpen U).Complexification) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hV : V ≤ U) : (X.restrictOpen V).Complexification

The restriction of a complexification of X | U to X | V along V ≤ U: (Y | W, f | V) with W = Y ∖ f(U ∖ V).

Equations

• C.restrictLe V hV = { Y := C.Y.restrictOpen (C.restrictLeOpens V), f := C.restrictLeHom V hV, isClosed_range := ⋯, isEmbedding := ⋯, bijective_stalkMap := ⋯ }