The restricted complexification over its inclusions #
The hypotheses of the gluing of complexifications are stated for the restricted complexifications
C.restrictLe V of Hironaka.AnalyticSpace.Glue.Restrict; this module restates them in one
uniform setting, morphisms out of the complexified open subspaces (X | V)(ℂ) into the spaces
Y_i, compared after the monomorphic inclusions.
- Bridge lemmas, chiefly
Complexification.restrictLeHom_comp_ofRestrict:f | Vfollowed by the inclusion of its targetY | (Y ∖ f(U ∖ V)) ⟶ Yis the complexified inclusion(X | V)(ℂ) ⟶ (X | U)(ℂ)followed byf. pairLift, the lift off ∘ incl_Vinto an open subsetΩ ∋ f(V), and the normalized transition datumPairIso Ci Cj V: domainsΩi,Ωjcontaining the images ofVand inside the loci where the real points lie overV, aK-isomorphisme : Y_i | Ωi ≅ Y_j | Ωj, and compatibility withf_i,f_j; withsymm,refl, and the real-point lemmas (toFun_e_hom_val,exists_eq_of_toFun_e_hom_eq).PairIso.ofHiso, the datum extracted from the local isomorphisms of two complexifications near the real points (the hypothesishisoof the gluing theorem).exists_eq_near_of_huniq, the uniqueness hypothesishuniqof the gluing theorem in the uniform setting: two morphisms out of an open subset ofY_icontainingf_i(V), both compatible withf_i,f_k, agree on an open subset containingf_i(V).
Conventions. The complexification functor complexifyHom (Hironaka.AnalyticSpace.Complexify) is
applied to the inclusion restrictOpenIncl; complexifyRestrictIso has the identity as underlying
morphism, so complexifyRestrictIso.hom ≫ ofRestrict = complexifyHom (ofRestrict) is an equality of
sheaf components (complexifyRestrictIso_hom_comp_ofRestrict); the identification
restrictRestrictIso is over X (restrictRestrictIso_inv_comp_ofRestrict). For V = U,
restrictLeHom is f transported along X | U ≅ (X | U) | ⊤. Not in the sources.
The inverse of the isomorphism of two open immersions with the same range is over the target.
Transport along an equality of opens is over the space.
Transport along an equality of opens is over the space (hom form).
The identification (X | U)(ℂ) ≅ X(ℂ) | U followed by the inclusion is the complexified
inclusion.
The identification (X | U) | V ≅ X | V is over X.
The identification (X | U) | V ≅ X | imageOpens U V is over X (hom form).
The identification (X | U) | V ≅ X | imageOpens U V is over X (inverse form).
The inclusion of A | ⊤ is an isomorphism (restrictOpenTopIso).
The morphism of the restricted complexification, followed by the inclusion of its target, is
the complexified inclusion (X | V)(ℂ) ⟶ (X | U)(ℂ) followed by f.
On points, the complexified inclusion followed by f is f.
On points, the morphism of the restricted complexification is f.
The lift of f ∘ (inclusion of V) into the open Ω ⊆ Y containing f(V).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A normalized transition datum between two local complexifications over the open V: opens
Ωi ⊆ Y_i, Ωj ⊆ Y_j containing the images of V, inside the loci where the real points lie over
V, and a K-isomorphism Y_i | Ωi ≅ Y_j | Ωj compatible with f_i and f_j on V.
- Ωi : TopologicalSpace.Opens ↑↑Ci.Y.toPresheafedSpace
The domain in
Y_i. - Ωj : TopologicalSpace.Opens ↑↑Cj.Y.toPresheafedSpace
The domain in
Y_j. - e : (Ci.Y.restrictOpen self.Ωi).KIso (Cj.Y.restrictOpen self.Ωj)
The transition isomorphism.
- mem_Ωi (v : ↑↑(X.restrictOpen V).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun Ci.f ⟨↑v, ⋯⟩ ∈ self.Ωi
- mem_Ωj (v : ↑↑(X.restrictOpen V).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun Cj.f ⟨↑v, ⋯⟩ ∈ self.Ωj
- compat : CategoryTheory.CategoryStruct.comp (pairLift Ci hVi self.Ωi ⋯) (CategoryTheory.CategoryStruct.comp self.e.hom (Cj.Y.ofRestrict self.Ωj)) = CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.complexifyHom (X.restrictOpenIncl hVj)) Cj.f
Instances For
On the image of a point of V, the transition is f_i x ↦ f_j x.
A point of the domain whose image under the transition is a real point of Y_j is a real point
of Y_i over V (transitions preserve non-real points): the real points of Ωj lie over V, and
on them the inverse of the transition is f_j x ↦ f_i x.
The transposed datum.
Equations
Instances For
The images of V lie in the image of an open W ⊆ Y | (Y ∖ f(U ∖ V)) containing
f | V (V).
The normalized datum extracted from the data of the hypothesis hiso of the gluing theorem (the
open subsets W, W' of the restricted complexifications and the K-isomorphism e between
them): the domains are the images of W, W' in Y_i, Y_j, the isomorphism is e transported
along the identifications of Hironaka.AnalyticSpace.OpenSubspaceLemmas, and the compatibility
follows from the given one after cancelling the isomorphism (X | V)(ℂ) | ⊤ ≅ (X | V)(ℂ) and the
monomorphic inclusions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diagonal datum: the identity of Y_i on ⊤.
Equations
- AnalyticSpace.Glue.PairIso.refl Ci = { Ωi := ⊤, Ωj := ⊤, e := CategoryTheory.Iso.refl (Ci.Y.restrictOpen ⊤), mem_Ωi := ⋯, mem_Ωj := ⋯, Ωi_le := ⋯, Ωj_le := ⋯, compat := ⋯ }
Instances For
The uniqueness hypothesis of the gluing theorem in the uniform setting #
The uniqueness hypothesis huniq of the gluing theorem, restated for two K-morphisms g₁ g₂
out of an open subset D ⊆ Y_i containing f_i(V) and inside Y_i ∖ f_i(U_i ∖ V), both compatible
with f_i, f_k on V and with range inside Y_k ∖ f_k(U_k ∖ V): they agree on an open subset
N ⊆ D containing f_i(V). The proof applies huniq to the restricted complexifications
C_i | V, C_k | V and translates along the identifications and the bridge lemma
restrictLeHom_comp_ofRestrict.