Carrying a local K-isomorphism back to the analytic space

Bookkeeping for the identification of a neighbourhood of a simple point with an open subset of Kⁿ [Hir64, Ch. 0, §1, p. 121]: the K-isomorphism produced at a point of a local model lives on an open of that model, and must be carried back to an open of the analytic space through the isomorphism X|U ≅ (local model)|W of the local-model clause. Three formal facts do this: an iterated open subspace (X|V)|T is the open subspace X|ι(T) (restrictOpen_restrictOpen_iso on imageOpens, Hironaka/AnalyticSpace/OpenSubspaceLemmas.lean, by isoOfRangeEq — open immersions into the same space with the same range are isomorphic); a K-isomorphism A ≅ B restricts to A|e⁻¹(T) ≅ B|T (restrictOpenIso); and the image of the trace V ∩ T, T ≤ V, is T again (imageOpens_map_eq, here, by ext from the membership lemma mem_imageOpens). Also the transport of regularity of stalks in the forward direction of a K-isomorphism and into an open subspace.

theorem AnalyticSpace.KLocallyRingedSpace.mem_imageOpens {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {T : TopologicalSpace.Opens ↑↑(X.restrictOpen V).toPresheafedSpace} {x : ↑↑X.toPresheafedSpace} : x ∈ imageOpens V T ↔ ∃ (hx : x ∈ V), ⟨x, hx⟩ ∈ T

Membership in imageOpens V T: the points of V whose trace lies in T.

theorem AnalyticSpace.KLocallyRingedSpace.imageOpens_map_eq {K : Type} [RCLike K] (X : KLocallyRingedSpace K) {V T : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : T ≤ V) : imageOpens V ((TopologicalSpace.Opens.map (↑(X.ofRestrict V)).base).obj T) = T

The image of the trace of T ≤ V on X|V is T.

theorem AnalyticSpace.KLocallyRingedSpace.isRegularLocalRing_stalk_of_kIso' {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) (h : IsRegularLocalRing ↑(A.presheaf.stalk a)) : IsRegularLocalRing ↑(B.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) a))

Regularity of stalks transports forward along a K-isomorphism: the converse direction of isRegularLocalRing_stalk_of_kIso (Hironaka/AnalyticSpace/RegularStalk.lean).

theorem AnalyticSpace.KLocallyRingedSpace.isRegularLocalRing_stalk_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) (h : IsRegularLocalRing ↑(X.presheaf.stalk ↑x)) : IsRegularLocalRing ↑((X.restrictOpen U).presheaf.stalk x)

Regularity of a stalk passes from X to the open subspace X|U.