The open inclusion of a restriction, and inverse images along morphisms of An/K

• AnalyticSpace.restrictInclusion X S : X.restrictSet S ⟶ X, the open inclusion ofRestrict X (openOf X S) of the open subspace X | S (for a non-open S, X.restrictSet S is X restricted along ⊤). The traces of the exceptional members of a local resolution on the part over an overlap are written with it.
• ClosedSubspace.comap_comp_hom, ClosedSubspace.comap_id_hom: the inverse image D.comap f of a closed subspace [Hir64, Ch. 0, §5, pp. 141–142] is functorial along morphisms of An/K — QuotientSpace.comap_comp (Hironaka/AnalyticSpace/QuotientMap.lean) read on these morphisms.

Used by RunFamilyRestrict.lean, ExceptionalTransitionRestrict.lean, HomOfPullbackEqCalculus.lean and Glue/OverFamilyPartner.lean (all in this directory).

noncomputable def AnalyticSpace.restrictInclusion {K : Type} [RCLike K] (X : AnalyticSpace K) (S : Set ↑↑X.toPresheafedSpace) : X.restrictSet S ⟶ X

The open inclusion X | S → X of the open subspace X.restrictSet S: the open immersion ofRestrict X (openOf X S); for a non-open S it is ofRestrict X ⊤ : X | ⊤ → X. Compare the restriction of an analytic space to an open subset in [Hir64, Ch. 0, §1, p. 120]. The traces comap (restrictInclusion Ỹ (Π ⁻¹' N)) (𝓔 j) of the exceptional members on the part over an overlap N are written with it.

Equations

• X.restrictInclusion S = X.ofRestrict (X.openOf S)

theorem AnalyticSpace.ClosedSubspace.comap_comp_hom {K : Type} [RCLike K] {X Y Z : AnalyticSpace K} (g : Y ⟶ Z) (f : X ⟶ Y) (D : Z.ClosedSubspace) : D.comap (CategoryTheory.CategoryStruct.comp f g) = (D.comap g).comap f

The inverse image along a composite is the composite of the inverse images ([Hir64, Ch. 0, §5, pp. 141–142]; QuotientSpace.comap_comp at the composite f ≫ g).

theorem AnalyticSpace.ClosedSubspace.comap_id_hom {K : Type} [RCLike K] {X : AnalyticSpace K} (D : X.ClosedSubspace) : D.comap (CategoryTheory.CategoryStruct.id X) = D

The inverse image along the identity is the subspace itself.