Restricting an isomorphism of open subspaces to a smaller open

For a morphism φ : X|U → Y|V of the open subspaces restrictSet and an open S ⊆ V, the preimage φ⁻¹S ⊆ U (Hom.preimageOpen), the image φ(P) ⊆ V of a set P ⊆ U (Hom.imageOpen), and the restriction φ|φ⁻¹S : X|φ⁻¹S → Y|S (Hom.restrictIsoTo, the lift of X|φ⁻¹S → X|U → Y|V → Y through the open immersion Y|S → Y), which lies over φ (restrictIsoTo_comp_restrictSetIncl) and is an isomorphism when φ is (isIso_restrictIsoTo, the inverse being the restriction of φ⁻¹). Needed for the functoriality of the resolution under isomorphisms of open subspaces (clause (5) of the resolution theorem; the functoriality in the proof of [Kol07, Theorem 36]), which transports a piece embedding of Y near φ x along φ (Hironaka/Resolution/Analytic/Kol07Thm45/ResolutionFunctorial.lean) and needs φ restricted to the open of that piece — an isomorphism X|φ⁻¹O' ≅ Y|O' of the open subspaces of the vocabulary, not the nested (X|U)|…. The open subspaces are Hironaka's X | U [Hir64, Ch. 0, §1, p. 120]. Routine.

def AnalyticSpace.Hom.preimageOpen {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (S : Set ↑↑Y.toPresheafedSpace) : Set ↑↑X.toPresheafedSpace

The preimage in X of a set S ⊆ Y under φ : X|U → Y|V: the points of U whose image lies in S.

Equations

• AnalyticSpace.Hom.preimageOpen φ S = Subtype.val '' AnalyticSpace.KLocallyRingedSpace.Hom.toFun φ ⁻¹' Subtype.val ⁻¹' S

theorem AnalyticSpace.Hom.isOpen_preimageOpen {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) : IsOpen (preimageOpen φ S)

The preimage of an open is open (Subtype.val is an open map on the open subspace).

theorem AnalyticSpace.Hom.preimageOpen_subset {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) : preimageOpen φ S ⊆ U

The preimage lies in U.

theorem AnalyticSpace.Hom.mem_preimageOpen_iff {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (S : Set ↑↑Y.toPresheafedSpace) (x : ↑↑X.toPresheafedSpace) : x ∈ preimageOpen φ S ↔ ∃ (p : ↑↑(X.restrictSet U).toPresheafedSpace), ↑p = x ∧ ↑(KLocallyRingedSpace.Hom.toFun φ p) ∈ S

Membership in the preimage.

def AnalyticSpace.Hom.imageOpen {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (P : Set ↑↑X.toPresheafedSpace) : Set ↑↑Y.toPresheafedSpace

The image in Y of a set P ⊆ X under φ : X|U → Y|V.

Equations

• AnalyticSpace.Hom.imageOpen φ P = Subtype.val '' AnalyticSpace.KLocallyRingedSpace.Hom.toFun φ '' Subtype.val ⁻¹' P

theorem AnalyticSpace.Hom.isOpen_imageOpen {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hφ : CategoryTheory.IsIso φ) (P : Set ↑↑X.toPresheafedSpace) (hP : IsOpen P) : IsOpen (imageOpen φ P)

The image of an open under an isomorphism is open (the underlying homeomorphism KIso.homeomorph, then Subtype.val).

theorem AnalyticSpace.Hom.imageOpen_subset {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hV : IsOpen V) (P : Set ↑↑X.toPresheafedSpace) : imageOpen φ P ⊆ V

The image lies in V.

theorem AnalyticSpace.Hom.mem_imageOpen_iff {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (P : Set ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) : y ∈ imageOpen φ P ↔ ∃ (p : ↑↑(X.restrictSet U).toPresheafedSpace), ↑p ∈ P ∧ ↑(KLocallyRingedSpace.Hom.toFun φ p) = y

Membership in the image.

theorem AnalyticSpace.Hom.preimageOpen_imageOpen {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hφ : CategoryTheory.IsIso φ) (hU : IsOpen U) (P : Set ↑↑X.toPresheafedSpace) (hPU : P ⊆ U) : preimageOpen φ (imageOpen φ P) = P

For an isomorphism, the preimage of the image of P ⊆ U is P (injective_toFun_of_isIso).

noncomputable def AnalyticSpace.Hom.restrictIsoTo {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) : X.restrictOpen (X.openOf (preimageOpen φ S)) ⟶ Y.restrictOpen (Y.openOf S)

The restriction of φ : X|U → Y|V to an open S ⊆ V, X|φ⁻¹S → Y|S: the lift of X|φ⁻¹S → X|U → Y|V → Y through the open immersion Y|S → Y (Hom.liftRestrict).

Equations

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

theorem AnalyticSpace.Hom.restrictIsoTo_comp_ofRestrict {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) : CategoryTheory.CategoryStruct.comp (restrictIsoTo φ hU S hS) (Y.ofRestrict (Y.openOf S)) = CategoryTheory.CategoryStruct.comp (X.restrictSetIncl ⋯ ⋯) (CategoryTheory.CategoryStruct.comp φ (Y.ofRestrict (Y.openOf V)))

The defining factorization of the restriction: followed by the open immersion Y|S → Y it is X|φ⁻¹S → X|U → Y|V → Y.

theorem AnalyticSpace.Hom.restrictIsoTo_comp_restrictSetIncl {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) (hSV : S ⊆ V) : CategoryTheory.CategoryStruct.comp (restrictIsoTo φ hU S hS) (Y.restrictSetIncl hS hSV) = CategoryTheory.CategoryStruct.comp (X.restrictSetIncl ⋯ ⋯) φ

The restriction lies over φ: followed by the inclusion Y|S → Y|V it is the inclusion X|φ⁻¹S → X|U followed by φ (both sides agree after the monomorphism Y|V → Y).

theorem AnalyticSpace.Hom.toFun_restrictIsoTo {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) (p : ↑↑(X.restrictOpen (X.openOf (preimageOpen φ S))).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (restrictIsoTo φ hU S hS) p) = ↑(KLocallyRingedSpace.Hom.toFun φ (KLocallyRingedSpace.Hom.toFun (X.restrictSetIncl ⋯ ⋯) p))

The restriction on points: the image of p is the image under φ of p read in X|U.

theorem AnalyticSpace.Hom.toFun_restrictIsoTo_mem_imageOpen_iff {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hφ : CategoryTheory.IsIso φ) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) (P : Set ↑↑X.toPresheafedSpace) (p : ↑↑(X.restrictOpen (X.openOf (preimageOpen φ S))).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (restrictIsoTo φ hU S hS) p) ∈ imageOpen φ P ↔ ↑p ∈ P

A point of X|φ⁻¹S maps into the image of P iff it lies in P (injective_toFun_of_isIso).

noncomputable def AnalyticSpace.Hom.restrictIsoToInv {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hφ : CategoryTheory.IsIso φ) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) (hSV : S ⊆ V) : Y.restrictOpen (Y.openOf S) ⟶ X.restrictOpen (X.openOf (preimageOpen φ S))

The inverse of the restriction of an isomorphism: the restriction of φ⁻¹ to φ⁻¹S, as the lift of Y|S → Y|V → X|U → X through X|φ⁻¹S → X.

Equations

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

theorem AnalyticSpace.Hom.restrictIsoToInv_comp_ofRestrict {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hφ : CategoryTheory.IsIso φ) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) (hSV : S ⊆ V) : CategoryTheory.CategoryStruct.comp (restrictIsoToInv φ hφ S hS hSV) (X.ofRestrict (X.openOf (preimageOpen φ S))) = CategoryTheory.CategoryStruct.comp (Y.restrictSetIncl hS hSV) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv φ) (X.ofRestrict (X.openOf U)))

The inverse's factorization through the open immersion X|φ⁻¹S → X.

theorem AnalyticSpace.Hom.isIso_restrictIsoTo {K : Type} [RCLike K] {X Y : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} {V : Set ↑↑Y.toPresheafedSpace} (φ : X.restrictSet U ⟶ Y.restrictSet V) (hφ : CategoryTheory.IsIso φ) (hU : IsOpen U) (S : Set ↑↑Y.toPresheafedSpace) (hS : IsOpen S) (hSV : S ⊆ V) : CategoryTheory.IsIso (restrictIsoTo φ hU S hS)

The restriction of an isomorphism is an isomorphism: the inverse is the restriction of φ⁻¹ (restrictIsoToInv); both composites are the identity after the monomorphisms X|φ⁻¹S → X, Y|S → Y.