Complexifications of real-analytic spaces and the morphism α_n

Hironaka [Hir64, Ch. 0, §1, p. 120] identifies ℝ with a topological subfield of ℂ, hence ℝⁿ with a topological subspace of ℂⁿ, and has the natural ℂ-isomorphism α_n : (ℝⁿ, 𝒜_{ℝⁿ} ⊗_ℝ ℂ) → (ℂⁿ, 𝒜_{ℂⁿ})|ℝⁿ. A preanalytic complexification of X is a pair (Y, f) of a preanalytic ℂ-space Y and a ℂ-morphism f : X(ℂ) → Y such that (1) f(X) is a closed subset of |Y| and (2) f induces a ℂ-isomorphism of X(ℂ) onto Y|f(X); an analytic complexification is a preanalytic one with Y an analytic ℂ-space.

• Complexification X: Hironaka's analytic complexification of an analytic ℝ-space X, an analytic ℂ-space Y with a ℂ-morphism f : X(ℂ) ⟶ Y such that (1) f(X) is closed and (2) f is a homeomorphism onto f(X) whose stalk maps 𝒪_{Y,f(x)} → 𝒪_{X(ℂ),x} are bijective — the stalkwise reading of "f induces a ℂ-isomorphism of X(ℂ) onto Y|f(X)" (Y|f(X) has the stalks 𝒪_{Y,f(x)}, and a morphism of sheaves is an isomorphism iff it is so on stalks). Preanalytic ℂ-spaces are not defined in this library, so the preanalytic notion is not transcribed; complexify itself is defined for every ℝ-local-ringed space with real residue fields, which covers the preanalytic case. That every analytic ℝ-space has a complexification is the theorem of Bruhat and Whitney [Hir64, Ch. 0, §1, p. 120, footnote 7].
• localModelSpace K n G f: a local analytic K-space is an analytic K-space (clause (i) with the identity, Hausdorff and countable at infinity as a closed subset of an open of Kⁿ); ℝⁿ itself and every V(f₁, …, f_k) ⊆ G are analytic spaces this way (the example V(x² + y²) ⊆ ℝ² is circleSpace of HironakaExamples/Space/CircleSpace.lean).
• Hom.restrictTo g U U' h : A|U ⟶ B|U', the restriction of a K-morphism to opens with g(U) ⊆ U', the lift through the open immersion B|U' ⟶ B; restrictOpenIncl : A|U ⟶ A|U' for U ≤ U'; IsLocalCoordination X U h, "(U, h) is a local Kⁿ-coordination" as a predicate (the content of LocalCoordination).
• realToComplex n : (ℝⁿ, 𝒜_{ℝⁿ} ⊗_ℝ ℂ) ⟶ (ℂⁿ, 𝒜_{ℂⁿ}), Hironaka's α_n as a ℂ-morphism: the base map is the inclusion ℝⁿ ⊆ ℂⁿ (realInclusion), and a holomorphic function F on an open V ⊆ ℂⁿ is sent to Re(F|ℝⁿ) + Im(F|ℝⁿ) · i on V ∩ ℝⁿ (realToComplexSheafHom); the real and imaginary parts of a holomorphic function are real-analytic (contMDiff_restrictScalars_opens: restriction of scalars, ContDiffAt.restrict_scalars), and the stalk maps are local because a germ is a unit iff its value is nonzero on both sides.
• AnalyticSpace.IsGeometric: the geometric spaces of [BM97, Remarks 1.7 (2)], those whose simple locus is Zariski-dense.

Local analytic K-spaces are analytic K-spaces

noncomputable def AnalyticSpace.localModelSpace (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : AnalyticSpace K

A local analytic K-space (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) is an analytic K-space (Hironaka's clause (i) with the identity as the local isomorphism; Hausdorff and countable at infinity as a closed subset of the open G ⊆ Kⁿ, locallyCompactSpace_localModel).

Equations

• AnalyticSpace.localModelSpace K n G f = { toKLocallyRingedSpace := AnalyticSpace.localModel K n G f, locallyModel := ⋯, t2 := ⋯, sigmaCompact := ⋯ }

theorem AnalyticSpace.localModelSpace_toKLocallyRingedSpace (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : (localModelSpace K n G f).toKLocallyRingedSpace = localModel K n G f

Restrictions of morphisms to opens; local coordinations as a predicate

noncomputable def AnalyticSpace.KLocallyRingedSpace.Hom.restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, toFun g a ∈ U') : A.restrictOpen U ⟶ B.restrictOpen U'

The restriction g|U : A|U ⟶ B|U' of a K-morphism to opens with g(U) ⊆ U': the lift of A|U ⟶ A ⟶ B through the open immersion B|U' ⟶ B.

Equations

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

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.restrictTo_comp_ofRestrict {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, toFun g a ∈ U') : CategoryTheory.CategoryStruct.comp (restrictTo g U U' h) (B.ofRestrict U') = CategoryTheory.CategoryStruct.comp (A.ofRestrict U) g

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.restrictTo_comp_ofRestrict_assoc {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, toFun g a ∈ U') {Z : KLocallyRingedSpace K} (h✝ : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictTo g U U' h) (CategoryTheory.CategoryStruct.comp (B.ofRestrict U') h✝) = CategoryTheory.CategoryStruct.comp (A.ofRestrict U) (CategoryTheory.CategoryStruct.comp g h✝)

theorem AnalyticSpace.KLocallyRingedSpace.Hom.toFun_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, toFun g a ∈ U') (a : ↑↑(A.restrictOpen U).toPresheafedSpace) : ↑(toFun (restrictTo g U U' h) a) = toFun g ↑a

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictOpenIncl {K : Type} [RCLike K] (A : KLocallyRingedSpace K) {U U' : TopologicalSpace.Opens ↑↑A.toPresheafedSpace} (h : U ≤ U') : A.restrictOpen U ⟶ A.restrictOpen U'

The inclusion A|U ⟶ A|U' of open subspaces, U ≤ U'.

Equations

• A.restrictOpenIncl h = AnalyticSpace.KLocallyRingedSpace.Hom.restrictTo (CategoryTheory.CategoryStruct.id A) U U' ⋯

def AnalyticSpace.KLocallyRingedSpace.IsLocalCoordination {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {n : ℕ} (h : X.restrictOpen U ⟶ affine K n) : Prop

"(U, h) is a local Kⁿ-coordination of X" [Hir64, Ch. 0, §1, p. 120]: h : X|U ⟶ (Kⁿ, 𝒜_{Kⁿ}) induces a K-isomorphism of X|U onto (an open of) a local analytic K-space in (Kⁿ, 𝒜_{Kⁿ}) — the content of LocalCoordination, as a predicate on the pair.

Equations

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

theorem AnalyticSpace.LocalCoordination.isLocalCoordination {K : Type} [RCLike K] {X : AnalyticSpace K} {x : ↑↑X.toPresheafedSpace} (c : X.LocalCoordination x) : X.IsLocalCoordination c.U c.h

Complexifications

structure AnalyticSpace.Complexification (X : AnalyticSpace ℝ) : Type (u + 1)

An (analytic) complexification of an analytic ℝ-space X [Hir64, Ch. 0, §1, p. 120]: an analytic ℂ-space Y and a ℂ-morphism f : X(ℂ) ⟶ Y such that (1) f(X) is closed in |Y| and (2) f induces a ℂ-isomorphism of X(ℂ) onto Y|f(X) — read stalkwise: f is a homeomorphism onto its image and every stalk map 𝒪_{Y,f(x)} → 𝒪_{X(ℂ),x} is bijective.

• Y : AnalyticSpace ℂ

  The complex space Y.

• f : X.complexify ⟶ self.Y.toKLocallyRingedSpace

  The ℂ-morphism f : X(ℂ) ⟶ Y.

• isClosed_range : IsClosed (Set.range (KLocallyRingedSpace.Hom.toFun self.f))

  Hironaka's (1): f(X) is closed in |Y|.

• isEmbedding : Topology.IsEmbedding (KLocallyRingedSpace.Hom.toFun self.f)

  Hironaka's (2), topological part: f is a homeomorphism onto f(X).

• bijective_stalkMap (x : ↑X.complexify.toTopCat) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑self.f) x))

  Hironaka's (2), sheaf part: the stalk maps 𝒪_{Y,f(x)} → 𝒪_{X(ℂ),x} are bijective.

theorem AnalyticSpace.Complexification.isClosedEmbedding {X : AnalyticSpace ℝ} (C : X.Complexification) : Topology.IsClosedEmbedding (KLocallyRingedSpace.Hom.toFun C.f)

(1) and (2) together: f is a closed embedding of the underlying spaces.

theorem AnalyticSpace.Complexification.injective_toFun {X : AnalyticSpace ℝ} (C : X.Complexification) : Function.Injective (KLocallyRingedSpace.Hom.toFun C.f)

Hironaka's α_n : (ℝⁿ, 𝒜_{ℝⁿ} ⊗_ℝ ℂ) ⟶ (ℂⁿ, 𝒜_{ℂⁿ})

noncomputable def AnalyticSpace.KLocallyRingedSpace.realInclusion (n : ℕ) : Kn ℝ n →L[ℝ] Kn ℂ n

The inclusion ℝⁿ ⊆ ℂⁿ [Hir64, Ch. 0, §1, p. 120], as a continuous ℝ-linear map of the universe-lifted spaces.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.realInclusion_apply (n : ℕ) (p : Kn ℝ n) : (realInclusion n) p = { down := fun (i : Fin n) => ↑(p.down i) }

theorem AnalyticSpace.KLocallyRingedSpace.realInclusion_injective (n : ℕ) : Function.Injective ⇑(realInclusion n)

noncomputable def AnalyticSpace.KLocallyRingedSpace.realInclusionTop (n : ℕ) : ↑(affine ℝ n).complexify.toPresheafedSpace ⟶ ↑(affine ℂ n).toPresheafedSpace

The inclusion ℝⁿ ⊆ ℂⁿ as a map of the underlying spaces of (ℝⁿ, 𝒜_{ℝⁿ} ⊗_ℝ ℂ) and (ℂⁿ, 𝒜_{ℂⁿ}).

Equations

• AnalyticSpace.KLocallyRingedSpace.realInclusionTop n = TopCat.ofHom { toFun := ⇑(AnalyticSpace.KLocallyRingedSpace.realInclusion n), continuous_toFun := ⋯ }

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_subtypeVal_comp_iff_opens {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {M : Type u_3} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_4} [TopologicalSpace N] [ChartedSpace E' N] {m : WithTop ℕ∞} {U : TopologicalSpace.Opens N} (g : M → ↥U) : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') m (Subtype.val ∘ g) ↔ ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') m g

The ω-version of Mathlib's ContMDiff.subtypeVal_comp_iff (stated at ∞ at the pin): a map into an open subset is C^n iff it is C^n into the ambient manifold.

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_restrictScalars_opens (n : ℕ) {V : TopologicalSpace.Opens (Kn ℂ n)} {F : ↥V → ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ (Kn ℂ n)) (modelWithCornersSelf ℂ ℂ) ⊤ F) : ContMDiff (modelWithCornersSelf ℝ (Kn ℂ n)) (modelWithCornersSelf ℝ ℂ) ⊤ F

A holomorphic function on an open V ⊆ ℂⁿ is real-analytic on V viewed as an open of the real vector space ℂⁿ (restriction of scalars).

def AnalyticSpace.KLocallyRingedSpace.realPreimage (n : ℕ) (V : TopologicalSpace.Opens (Kn ℂ n)) : TopologicalSpace.Opens (Kn ℝ n)

The trace V ∩ ℝⁿ ⊆ ℝⁿ of an open V ⊆ ℂⁿ, as an open of ℝⁿ.

Equations

• AnalyticSpace.KLocallyRingedSpace.realPreimage n V = { carrier := ⇑(AnalyticSpace.KLocallyRingedSpace.realInclusion n) ⁻¹' ↑V, is_open' := ⋯ }

theorem AnalyticSpace.KLocallyRingedSpace.mem_realPreimage (n : ℕ) {V : TopologicalSpace.Opens (Kn ℂ n)} {p : Kn ℝ n} : p ∈ realPreimage n V ↔ (realInclusion n) p ∈ V

noncomputable def AnalyticSpace.KLocallyRingedSpace.realInclusionRestrict (n : ℕ) (V : TopologicalSpace.Opens (Kn ℂ n)) : ↥(realPreimage n V) → ↥V

The inclusion ℝⁿ ⊆ ℂⁿ restricted to the trace V ∩ ℝⁿ of an open V ⊆ ℂⁿ.

Equations

• AnalyticSpace.KLocallyRingedSpace.realInclusionRestrict n V p = ⟨(AnalyticSpace.KLocallyRingedSpace.realInclusion n) ↑p, ⋯⟩

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_realInclusionRestrict (n : ℕ) (V : TopologicalSpace.Opens (Kn ℂ n)) : ContMDiff (modelWithCornersSelf ℝ (Kn ℝ n)) (modelWithCornersSelf ℝ (Kn ℂ n)) ⊤ (realInclusionRestrict n V)

The restriction of the inclusion to the trace of an open V ⊆ ℂⁿ is real-analytic.

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_re_restrict (n : ℕ) {V : TopologicalSpace.Opens (Kn ℂ n)} (F : ↑((affine ℂ n).presheaf.obj (Opposite.op V))) : ContMDiff (modelWithCornersSelf ℝ (Kn ℝ n)) (modelWithCornersSelf ℝ ℝ) ⊤ fun (p : ↥(realPreimage n V)) => (↑F (realInclusionRestrict n V p)).re

The real part of a holomorphic function on V ⊆ ℂⁿ, restricted to V ∩ ℝⁿ, is real-analytic.

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_im_restrict (n : ℕ) {V : TopologicalSpace.Opens (Kn ℂ n)} (F : ↑((affine ℂ n).presheaf.obj (Opposite.op V))) : ContMDiff (modelWithCornersSelf ℝ (Kn ℝ n)) (modelWithCornersSelf ℝ ℝ) ⊤ fun (p : ↥(realPreimage n V)) => (↑F (realInclusionRestrict n V p)).im

The imaginary part, likewise.

noncomputable def AnalyticSpace.KLocallyRingedSpace.realToComplexSheafHom (n : ℕ) : (affine ℂ n).presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat (realInclusionTop n)).obj (affine ℝ n).complexify.presheaf

The sheaf map of α_n: a holomorphic function F on V ⊆ ℂⁿ goes to Re(F|ℝⁿ) + Im(F|ℝⁿ) · i on V ∩ ℝⁿ.

Equations

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

noncomputable def AnalyticSpace.KLocallyRingedSpace.realToComplexAux (n : ℕ) : (affine ℝ n).complexify.toPresheafedSpace ⟶ (affine ℂ n).toPresheafedSpace

(Implementation.) α_n as a morphism of presheafed spaces.

Equations

• AnalyticSpace.KLocallyRingedSpace.realToComplexAux n = { base := AnalyticSpace.KLocallyRingedSpace.realInclusionTop n, c := AnalyticSpace.KLocallyRingedSpace.realToComplexSheafHom n }

theorem AnalyticSpace.KLocallyRingedSpace.realToComplexAux_c_app_re (n : ℕ) {V : TopologicalSpace.Opens (Kn ℂ n)} (F : ↑((affine ℂ n).presheaf.obj (Opposite.op V))) (p : ↥(realPreimage n V)) : ↑((CategoryTheory.ConcreteCategory.hom ((realToComplexAux n).c.app (Opposite.op V))) F).re p = (↑F (realInclusionRestrict n V p)).re

theorem AnalyticSpace.KLocallyRingedSpace.realToComplexAux_c_app_im (n : ℕ) {V : TopologicalSpace.Opens (Kn ℂ n)} (F : ↑((affine ℂ n).presheaf.obj (Opposite.op V))) (p : ↥(realPreimage n V)) : ↑((CategoryTheory.ConcreteCategory.hom ((realToComplexAux n).c.app (Opposite.op V))) F).im p = (↑F (realInclusionRestrict n V p)).im

theorem AnalyticSpace.KLocallyRingedSpace.isLocalHom_stalkMap_realToComplexAux (n : ℕ) (p : Kn ℝ n) : IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (realToComplexAux n) p))

The stalk maps of α_n are local: a germ is a unit iff its value is nonzero, on both sides (contMDiffSheafCommRing.isUnit_stalk_iff, Complexified.isUnit_iff_isUnit_norm), and |F(p)|² = Re(F(p))² + Im(F(p))².

noncomputable def AnalyticSpace.KLocallyRingedSpace.realToComplex (n : ℕ) : (affine ℝ n).complexify ⟶ affine ℂ n

The natural ℂ-morphism α_n : (ℝⁿ, 𝒜_{ℝⁿ} ⊗_ℝ ℂ) ⟶ (ℂⁿ, 𝒜_{ℂⁿ}) [Hir64, Ch. 0, §1, p. 120], the inclusion ℝⁿ ⊆ ℂⁿ with F ↦ Re(F|ℝⁿ) + Im(F|ℝⁿ) · i on sections.

Equations

• AnalyticSpace.KLocallyRingedSpace.realToComplex n = ⟨{ toHom := AnalyticSpace.KLocallyRingedSpace.realToComplexAux n, prop := ⋯ }, ⋯⟩

theorem AnalyticSpace.KLocallyRingedSpace.toFun_realToComplex (n : ℕ) (p : Kn ℝ n) : Hom.toFun (realToComplex n) p = (realInclusion n) p

Geometric spaces

def AnalyticSpace.IsGeometric {K : Type} [RCLike K] (X : AnalyticSpace K) : Prop

Bierstone and Milman's geometric analytic spaces [BM97, Remarks 1.7 (2)]: X is geometric when its simple locus X.regularLocus is Zariski-dense in |X| — no closed analytic subspace other than X itself contains all the simple points: every closed subspace W with X.regularLocus ⊆ |W| has |W| = |X|.

Equations

• X.IsGeometric = ∀ (W : X.ClosedSubspace), X.regularLocus ⊆ Manifold.IdealSheaf.support W → Manifold.IdealSheaf.support W = Set.univ