The simple locus and the underlying map under open immersions

Elementary facts about analytic K-spaces used in the comparison of two local resolutions over a piece (Hironaka/Resolution/Analytic/Kol07Thm45/LocalResolutionIndependent.lean, Hironaka/Resolution/Analytic/Kol07Thm45/CoproductGluedFamily.lean, Hironaka/AnalyticSpace/Glue/OverReg.lean, Hironaka/Resolution/Analytic/Kol07Thm45/IsoOverLemmas.lean, Hironaka/Resolution/Analytic/Kol07Thm45/RestrictIsoOpen.lean), where the simple locus of the piece is read through an open immersion and the restricted local resolutions inherit non-singularity:

• a point is simple iff its image under an open immersion is simple (mem_reg_iff_of_isOpenImmersion — the stalk maps of an open immersion are isomorphisms of local rings, and regularity is invariant under ring isomorphisms; the simple points of [Hir64, Ch. 0, §1, p. 121]);
• the underlying map of an open immersion, or of an isomorphism, is injective (injective_toFun_of_isOpenImmersion, injective_toFun_of_isIso) and, for an open immersion, open (isOpenMap_toFun_of_isOpenImmersion);
• an open subspace of a non-singular space is non-singular (isNonsingular_restrictSet, for restrict at any set, with the convention openOf for non-open sets; the open subspaces of [Hir64, Ch. 0, §1, p. 120]).

Routine.

theorem AnalyticSpace.mem_reg_iff_of_isOpenImmersion {K : Type} [RCLike K] {A B : AnalyticSpace K} (φ : A ⟶ B) (hφ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑φ) (a : ↑↑A.toPresheafedSpace) : a ∈ A.regularLocus ↔ ↑φ a ∈ B.regularLocus

A point is simple iff its image under an open immersion is simple: the stalk map of an open immersion at a is an isomorphism 𝒪_{B, φ a} ≅ 𝒪_{A, a} (Mathlib's LocallyRingedSpace.IsOpenImmersion.stalk_iso), and a regular local ring is regular under a ring isomorphism (IsRegularLocalRing.of_ringEquiv, both ways).

theorem AnalyticSpace.injective_toFun_of_isIso {K : Type} [RCLike K] {A B : AnalyticSpace K} (φ : A ⟶ B) (hφ : CategoryTheory.IsIso φ) : Function.Injective ↑φ

The underlying map of an isomorphism of analytic K-spaces is injective (an isomorphism is an open immersion, Mathlib's LocallyRingedSpace.IsOpenImmersion.of_isIso).

theorem AnalyticSpace.injective_toFun_of_isOpenImmersion {K : Type} [RCLike K] {A B : AnalyticSpace K} (φ : A ⟶ B) (hφ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑φ) : Function.Injective ↑φ

The underlying map of an open immersion is injective (its base map is an open embedding, Mathlib's IsOpenImmersion.base_open).

theorem AnalyticSpace.isNonsingular_restrictSet {K : Type} [RCLike K] {X : AnalyticSpace K} (hX : X.IsNonsingular) (S : Set ↑↑X.toPresheafedSpace) : (X.restrictSet S).IsNonsingular

An open subspace of a non-singular analytic K-space is non-singular (restrict at any set, through the convention openOf): the stalks of X | U are the stalks of X (isRegularLocalRing_stalk_restrictOpen_iff).

theorem AnalyticSpace.isOpenMap_toFun_of_isOpenImmersion {K : Type} [RCLike K] {A B : AnalyticSpace K} (φ : A ⟶ B) (hφ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑φ) : IsOpenMap ↑φ

The underlying map of an open immersion is an open map (its base map is an open embedding, Mathlib's IsOpenImmersion.base_open).