The restriction to a subset under nesting, and gluing over a base

For the open subspace X.restrictSet S = X.restrictOpen (openOf X S) (Hironaka's X | U [Hir64, Ch. 0, §1, p. 120] with the convention openOf for non-open sets) and an open T ⊆ S:

• the inclusion restrictSetIncl : X | T ⟶ X | S (the K-level restrictIncl of Hironaka/AnalyticSpace/HomGlue.lean at openOf X T ≤ openOf X S), over X (restrictSetIncl_comp_ofRestrict) and the identity on points (toFun_restrictSetIncl), a monomorphism, composing as inclusions do;
• the restriction of a restriction (X | S) | (T ∩ S) ≅ X | T (restrictSet_restrictSet_iso, Mathlib's universal property of open immersions through isoOfRangeEq), and the isomorphism followed by the inclusion is the open immersion of the piece (restrictSet_restrictSet_iso_hom_comp);
• the restriction of a morphism is natural for the inclusions (restrictSet_comp_restrictSetIncl) and for the restriction-of-a-restriction isomorphisms of nested opens; equal sets give identified restrictions (restrictSet_congr_iso), over X.

Gluing over a base. For morphisms f : A ⟶ Z, g : B ⟶ Z of analytic K-spaces, in the K-level view Hom.restrictSetTo of the restriction (which is Hom.restrictSet, Hom.restrictSetTo_eq_restrictSet; kept so that every object is a restrictOpen of a K-local-ringed space and every morphism a K-morphism, and the library's gluing of morphisms along an open cover, glueOfCover of Hironaka/AnalyticSpace/HomGlue.lean and hom_ext_of_cover of Hironaka/AnalyticSpace/HomLocal.lean, applies as it stands): given uniqueness of the morphisms A | f⁻¹N ⟶ B | g⁻¹N over Z | N for every open N (Hom.UniqueOver), local morphisms over the members of an open cover of O agree on the overlaps (gluePieceSet, the pieces read on the members of the cover through the restriction-of-a-restriction isomorphism) and glue to a morphism A | f⁻¹O ⟶ B | g⁻¹O over Z; local isomorphisms over the base around every point of O glue to an isomorphism over O (Hom.UniqueOver.exists_isIso_restrictSetTo, a corollary of KLocallyRingedSpace.exists_isIso_over_of_cover of Hironaka/AnalyticSpace/Glue/GlueIsoOver.lean); and the unique isomorphism over the base transports along an isomorphism of bases. This is the gluing of the local isomorphisms between two local resolutions over the opens of a piece to an isomorphism over their union — the uniqueness argument in the proof of [Kol07, Theorem 36] and the functoriality of [Wlo09, Theorem 6.0.6 (1), (2)]. Routine; used by Hironaka/Resolution/Analytic/Kol07Thm45/RestrictIsoOpen.lean, Hironaka/Resolution/Analytic/Kol07Thm45/RestrictInclusion.lean and Hironaka/Resolution/Analytic/Kol07Thm45/LocalResolutionIndependent.lean.

theorem AnalyticSpace.subset_openOf {K : Type} [RCLike K] (X : AnalyticSpace K) (S : Set ↑↑X.toPresheafedSpace) : S ⊆ ↑(X.openOf S)

Every set lies in the open of the convention: S ⊆ openOf X S (equality for an open S, the whole space otherwise).

theorem AnalyticSpace.openOf_mono_of_isOpen {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : X.openOf T ≤ X.openOf S

The opens of the convention are monotone on an open T ⊆ S.

Every statement below is in the K-level view of the restriction restrictSet: X.toKLocallyRingedSpace.restrictOpen (openOf X T), definitionally (X.restrictSet T).toKLocallyRingedSpace, so that the K-level lemmas on open subspaces apply.

noncomputable def AnalyticSpace.restrictSetIncl {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : X.restrictOpen (X.openOf T) ⟶ X.restrictOpen (X.openOf S)

The inclusion X | T → X | S of the restrictions, T ⊆ S with T open: the K-level restrictIncl at openOf X T ≤ openOf X S.

Equations

• X.restrictSetIncl hT hTS = X.restrictIncl ⋯

theorem AnalyticSpace.restrictSetIncl_comp_ofRestrict {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (X.restrictSetIncl hT hTS) (X.ofRestrict (X.openOf S)) = X.ofRestrict (X.openOf T)

The inclusion lies over X.

theorem AnalyticSpace.toFun_restrictSetIncl {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) (p : ↑↑(X.restrictOpen (X.openOf T)).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (X.restrictSetIncl hT hTS) p) = ↑p

The inclusion is the identity on points.

theorem AnalyticSpace.ext_of_comp_restrictSetIncl {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) {Y : KLocallyRingedSpace K} {a b : Y ⟶ X.restrictOpen (X.openOf T)} (h : CategoryTheory.CategoryStruct.comp a (X.restrictSetIncl hT hTS) = CategoryTheory.CategoryStruct.comp b (X.restrictSetIncl hT hTS)) : a = b

The inclusion X | T → X | S is a monomorphism: two morphisms into X | T with the same composite into X | S are equal (compose further into X, where the open immersion is mono).

theorem AnalyticSpace.restrictSetIncl_comp_restrictSetIncl {K : Type} [RCLike K] (X : AnalyticSpace K) {T S R : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hS : IsOpen S) (hTS : T ⊆ S) (hSR : S ⊆ R) : CategoryTheory.CategoryStruct.comp (X.restrictSetIncl hT hTS) (X.restrictSetIncl hS hSR) = X.restrictSetIncl hT ⋯

The inclusions compose: X | T → X | S → X | R is X | T → X | R.

def AnalyticSpace.restrictSetPieceOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (S : Set ↑↑X.toPresheafedSpace) {T : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) : TopologicalSpace.Opens ↑↑(X.restrictOpen (X.openOf S)).toPresheafedSpace

The piece of X | S over an open T of X: the open T ∩ S of X | S. Packaged as a definition so that the statements about it carry a constant, not an anonymous constructor (the rewrite motives stay type-correct).

Equations

• X.restrictSetPieceOpens S hT = { carrier := Subtype.val ⁻¹' T, is_open' := ⋯ }

theorem AnalyticSpace.mem_restrictSetPieceOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (S : Set ↑↑X.toPresheafedSpace) {T : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (p : ↑↑(X.restrictOpen (X.openOf S)).toPresheafedSpace) : p ∈ X.restrictSetPieceOpens S hT ↔ ↑p ∈ T

Membership in the piece over T.

theorem AnalyticSpace.restrictSetPieceOpens_le {K : Type} [RCLike K] (X : AnalyticSpace K) (S : Set ↑↑X.toPresheafedSpace) {T' T : Set ↑↑X.toPresheafedSpace} (hT' : IsOpen T') (hT : IsOpen T) (h : T' ⊆ T) : X.restrictSetPieceOpens S hT' ≤ X.restrictSetPieceOpens S hT

The pieces are monotone.

theorem AnalyticSpace.range_toFun_ofRestrict_pieceOpens_comp {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((X.restrictOpen (X.openOf S)).ofRestrict (X.restrictSetPieceOpens S hT)) (X.ofRestrict (X.openOf S)))) = Set.range (KLocallyRingedSpace.Hom.toFun (X.ofRestrict (X.openOf T)))

The open immersion (X | S) | (T ∩ S) → X | S → X has range T for an open T ⊆ S.

theorem AnalyticSpace.isOpenImmersion_ofRestrict_pieceOpens_comp {K : Type} [RCLike K] (X : AnalyticSpace K) (S : Set ↑↑X.toPresheafedSpace) {T : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(CategoryTheory.CategoryStruct.comp ((X.restrictOpen (X.openOf S)).ofRestrict (X.restrictSetPieceOpens S hT)) (X.ofRestrict (X.openOf S)))

The open immersion of the piece over T into X (the composite of two ofRestricts).

noncomputable def AnalyticSpace.restrictSet_restrictSet_iso {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : ((X.restrictOpen (X.openOf S)).restrictOpen (X.restrictSetPieceOpens S hT)).KIso (X.restrictOpen (X.openOf T))

The restriction of a restriction: (X | S) | (T ∩ S) ≅ X | T for an open T ⊆ S — the two open immersions into X have the same range T (isoOfRangeEq).

Equations

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

theorem AnalyticSpace.restrictSet_restrictSet_iso_hom_comp_ofRestrict {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (X.restrictSet_restrictSet_iso hT hTS).hom (X.ofRestrict (X.openOf T)) = CategoryTheory.CategoryStruct.comp ((X.restrictOpen (X.openOf S)).ofRestrict (X.restrictSetPieceOpens S hT)) (X.ofRestrict (X.openOf S))

The isomorphism lies over X: followed by the open immersion X | T → X it is the open immersion of the piece (X | S) | (T ∩ S) → X | S → X.

theorem AnalyticSpace.restrictSet_restrictSet_iso_hom_comp {K : Type} [RCLike K] (X : AnalyticSpace K) {T S : Set ↑↑X.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (X.restrictSet_restrictSet_iso hT hTS).hom (X.restrictSetIncl hT hTS) = (X.restrictOpen (X.openOf S)).ofRestrict (X.restrictSetPieceOpens S hT)

The isomorphism followed by the inclusion X | T → X | S is the open immersion of the piece (X | S) | (T ∩ S) → X | S (the open immersion X | S → X is a monomorphism, Hom.ext_of_comp_ofRestrict).

theorem AnalyticSpace.restrictTo_comp_restrictSetIncl {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A ⟶ Z) {T S : Set ↑↑Z.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (KLocallyRingedSpace.Hom.restrictTo f (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' T)) (Z.openOf T) ⋯) (Z.restrictSetIncl hT hTS) = CategoryTheory.CategoryStruct.comp (A.restrictSetIncl ⋯ ⋯) (KLocallyRingedSpace.Hom.restrictTo f (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' S)) (Z.openOf S) ⋯)

Naturality of the restriction for the inclusions of nested opens (the K-level form, Hom.restrictTo at the opens of the convention): f | f⁻¹T followed by Z | T → Z | S is A | f⁻¹T → A | f⁻¹S followed by f | f⁻¹S — both are lifts of A | f⁻¹T → A → Z through the open immersion Z | S → Z (Hom.restrictTo_comp_ofRestrict), which is a monomorphism.

theorem AnalyticSpace.restrictSet_comp_restrictSetIncl {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A ⟶ Z) {T S : Set ↑↑Z.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (Hom.restrictSet f T) (Z.restrictSetIncl hT hTS) = CategoryTheory.CategoryStruct.comp (A.restrictSetIncl ⋯ ⋯) (Hom.restrictSet f S)

The same for Hom.restrictSet (which is Hom.restrictTo at the opens of the convention, Hom.restrictSet_eq_restrictTo).

theorem AnalyticSpace.restrictSet_restrictSet_iso_inv_comp_restrictIncl {K : Type} [RCLike K] (X : AnalyticSpace K) {T' T S : Set ↑↑X.toPresheafedSpace} (hT' : IsOpen T') (hT : IsOpen T) (hT'T : T' ⊆ T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (X.restrictSet_restrictSet_iso hT' ⋯).inv (CategoryTheory.CategoryStruct.comp ((X.restrictOpen (X.openOf S)).restrictIncl ⋯) (X.restrictSet_restrictSet_iso hT hTS).hom) = X.restrictSetIncl hT' hT'T

Naturality of the restriction-of-a-restriction isomorphism for nested opens: for opens T' ⊆ T ⊆ S, the inverse isomorphism of T', the inclusion of the pieces and the isomorphism of T compose to the inclusion X | T' → X | T — every step lies over X.

noncomputable def AnalyticSpace.restrictSet_congr_iso {K : Type} [RCLike K] (X : AnalyticSpace K) {s t : Set ↑↑X.toPresheafedSpace} (h : s = t) : (X.restrictOpen (X.openOf s)).KIso (X.restrictOpen (X.openOf t))

Equal sets give the same restriction: the identification X | s ≅ X | t for s = t (eqToIso), the identity on points.

Equations

• X.restrictSet_congr_iso h = CategoryTheory.eqToIso ⋯

theorem AnalyticSpace.restrictSet_congr_iso_hom_comp_ofRestrict {K : Type} [RCLike K] (X : AnalyticSpace K) {s t : Set ↑↑X.toPresheafedSpace} (h : s = t) : CategoryTheory.CategoryStruct.comp (X.restrictSet_congr_iso h).hom (X.ofRestrict (X.openOf t)) = X.ofRestrict (X.openOf s)

The identification of equal restrictions lies over X.

theorem AnalyticSpace.restrictSet_congr_iso_inv_comp_ofRestrict {K : Type} [RCLike K] (X : AnalyticSpace K) {s t : Set ↑↑X.toPresheafedSpace} (h : s = t) : CategoryTheory.CategoryStruct.comp (X.restrictSet_congr_iso h).inv (X.ofRestrict (X.openOf s)) = X.ofRestrict (X.openOf t)

The inverse identification of equal restrictions lies over X.

Gluing over a base

The gluing and transport statements, for arbitrary morphisms f : A ⟶ Z, g : B ⟶ Z of analytic K-spaces in the K-level view of the restriction (Hom.restrictSetTo, which is Hom.restrictSet): every object is a restrictOpen of a K-local-ringed space at an open of the convention openOf, every morphism a K-morphism, so that the library's gluing of morphisms along an open cover (glueOfCover, hom_ext_of_cover) applies as it stands.

noncomputable def AnalyticSpace.Hom.restrictSetTo {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (N : Set ↑↑Z.toPresheafedSpace) : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N)) ⟶ Z.restrictOpen (Z.openOf N)

The K-view of the restriction f | f⁻¹N : A | f⁻¹N ⟶ Z | N: Hom.restrictTo at the opens of the convention (Hom.restrictSet_eq_restrictTo), stated on the K-local-ringed spaces so that the gluing statements of this section live in one category.

Equations

• AnalyticSpace.Hom.restrictSetTo f N = AnalyticSpace.KLocallyRingedSpace.Hom.restrictTo f (A.openOf (AnalyticSpace.KLocallyRingedSpace.Hom.toFun f ⁻¹' N)) (Z.openOf N) ⋯

theorem AnalyticSpace.Hom.restrictSetTo_eq_restrictSet {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A ⟶ Z) (N : Set ↑↑Z.toPresheafedSpace) : restrictSetTo f N = restrictSet f N

Hom.restrictSetTo is Hom.restrictSet.

theorem AnalyticSpace.Hom.restrictSetTo_comp_ofRestrict {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (N : Set ↑↑Z.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (restrictSetTo f N) (Z.ofRestrict (Z.openOf N)) = CategoryTheory.CategoryStruct.comp (A.ofRestrict (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N))) f

The restriction lies over f.

theorem AnalyticSpace.Hom.restrictSetTo_comp_ofRestrict_assoc {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (N : Set ↑↑Z.toPresheafedSpace) {Y : KLocallyRingedSpace K} (k : Z.toKLocallyRingedSpace ⟶ Y) : CategoryTheory.CategoryStruct.comp (restrictSetTo f N) (CategoryTheory.CategoryStruct.comp (Z.ofRestrict (Z.openOf N)) k) = CategoryTheory.CategoryStruct.comp (A.ofRestrict (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N))) (CategoryTheory.CategoryStruct.comp f k)

The restriction lies over f (reassociated form).

theorem AnalyticSpace.Hom.toFun_restrictSetTo {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (N : Set ↑↑Z.toPresheafedSpace) (p : ↑↑(A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N))).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (restrictSetTo f N) p) = KLocallyRingedSpace.Hom.toFun f ↑p

The restriction on points.

theorem AnalyticSpace.Hom.restrictSetTo_comp_restrictSetIncl {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) {T S : Set ↑↑Z.toPresheafedSpace} (hT : IsOpen T) (hTS : T ⊆ S) : CategoryTheory.CategoryStruct.comp (restrictSetTo f T) (Z.restrictSetIncl hT hTS) = CategoryTheory.CategoryStruct.comp (A.restrictSetIncl ⋯ ⋯) (restrictSetTo f S)

Naturality of the restriction for the inclusions of nested opens, in the K-view.

theorem AnalyticSpace.mem_openOf_iff_of_isOpen {K : Type} [RCLike K] (X : AnalyticSpace K) {S : Set ↑↑X.toPresheafedSpace} (hS : IsOpen S) (x : ↑↑X.toPresheafedSpace) : x ∈ X.openOf S ↔ x ∈ S

Membership in the open of the convention, for an open set.

@[reducible, inline]

abbrev AnalyticSpace.Hom.preimagePieceOpens {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (O : Set ↑↑Z.toPresheafedSpace) {N : Set ↑↑Z.toPresheafedSpace} (hN : IsOpen N) : TopologicalSpace.Opens ↑↑(A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).toPresheafedSpace

The member of the open cover of A | f⁻¹O over an open N of Z: the points of A | f⁻¹O lying over N (the piece restrictSetPieceOpens at f⁻¹N).

Equations

• AnalyticSpace.Hom.preimagePieceOpens f O hN = A.restrictSetPieceOpens (AnalyticSpace.KLocallyRingedSpace.Hom.toFun f ⁻¹' O) ⋯

theorem AnalyticSpace.Hom.mem_preimagePieceOpens {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (O : Set ↑↑Z.toPresheafedSpace) {N : Set ↑↑Z.toPresheafedSpace} (hN : IsOpen N) (a : ↑↑(A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).toPresheafedSpace) : a ∈ preimagePieceOpens f O hN ↔ KLocallyRingedSpace.Hom.toFun f ↑a ∈ N

Membership in the member over N.

theorem AnalyticSpace.Hom.exists_mem_preimagePieceOpens {K : Type} [RCLike K] {A Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) {O : Set ↑↑Z.toPresheafedSpace} (hO : IsOpen O) {ι : Type u_1} (N : ι → Set ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), IsOpen (N i)) (hcov : ∀ x ∈ O, ∃ (i : ι), x ∈ N i) (a : ↑↑(A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).toPresheafedSpace) : ∃ (i : ι), a ∈ preimagePieceOpens f O ⋯

The members over opens N i covering O cover A | f⁻¹O.

def AnalyticSpace.Hom.UniqueOver {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) : Prop

Uniqueness over the base: for every open N of Z, two morphisms A | f⁻¹N ⟶ B | g⁻¹N over Z | N are equal — the hypothesis of the gluing below, which the local resolution maps satisfy.

Equations

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

theorem AnalyticSpace.Hom.toFun_mem_of_comp_restrictSetTo_eq {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) {M O : Set ↑↑Z.toPresheafedSpace} (hM : IsOpen M) (hMO : M ⊆ O) (χ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' M)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' O))) (h : CategoryTheory.CategoryStruct.comp χ (restrictSetTo g O) = CategoryTheory.CategoryStruct.comp (restrictSetTo f M) (Z.restrictSetIncl hM hMO)) (p : ↑↑(A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' M))).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun χ p ∈ preimagePieceOpens g O hM

A morphism A | f⁻¹M ⟶ B | g⁻¹O over Z through the inclusion Z | M ⟶ Z | O maps every point into the member over M.

theorem AnalyticSpace.Hom.UniqueOver.ext_over_incl {K : Type} [RCLike K] {A B Z : AnalyticSpace K} {f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} {g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} (huniq : UniqueOver f g) {M O : Set ↑↑Z.toPresheafedSpace} (hM : IsOpen M) (hMO : M ⊆ O) (χ₁ χ₂ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' M)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' O))) (h₁ : CategoryTheory.CategoryStruct.comp χ₁ (restrictSetTo g O) = CategoryTheory.CategoryStruct.comp (restrictSetTo f M) (Z.restrictSetIncl hM hMO)) (h₂ : CategoryTheory.CategoryStruct.comp χ₂ (restrictSetTo g O) = CategoryTheory.CategoryStruct.comp (restrictSetTo f M) (Z.restrictSetIncl hM hMO)) : χ₁ = χ₂

Uniqueness over the base with the target over a larger open: two morphisms A | f⁻¹M ⟶ B | g⁻¹O (M ⊆ O open) over Z through the inclusion Z | M ⟶ Z | O are equal — each factors through the open B | g⁻¹M (Hom.liftRestrict, the restriction-of-a-restriction isomorphism), the factors are over Z | M (naturality; the inclusion is mono), so the uniqueness over M identifies them.

noncomputable def AnalyticSpace.Hom.gluePieceSet {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) {O N : Set ↑↑Z.toPresheafedSpace} (hN : IsOpen N) (hNO : N ⊆ O) (ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' N))) : (A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).restrictOpen (preimagePieceOpens f O hN) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' O))

The piece of the glued morphism over an open N ⊆ O: the local morphism ψ : A | f⁻¹N ⟶ B | g⁻¹N read on the member of the cover through the restriction-of-a-restriction isomorphism, then into B | g⁻¹O by the inclusion.

Equations

• AnalyticSpace.Hom.gluePieceSet f g hN hNO ψ = CategoryTheory.CategoryStruct.comp (A.restrictSet_restrictSet_iso ⋯ ⋯).hom (CategoryTheory.CategoryStruct.comp ψ (B.restrictSetIncl ⋯ ⋯))

theorem AnalyticSpace.Hom.gluePieceSet_comp_restrictSetTo {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) {O N : Set ↑↑Z.toPresheafedSpace} (hN : IsOpen N) (hNO : N ⊆ O) (ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' N))) (hψ : CategoryTheory.CategoryStruct.comp ψ (restrictSetTo g N) = restrictSetTo f N) : CategoryTheory.CategoryStruct.comp (gluePieceSet f g hN hNO ψ) (restrictSetTo g O) = CategoryTheory.CategoryStruct.comp ((A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).ofRestrict (preimagePieceOpens f O hN)) (restrictSetTo f O)

The piece lies over Z: gluePieceSet ψ ≫ g|O = ofRestrict ≫ f|O when ψ ≫ g|N = f|N (naturality twice, and the restriction-of-a-restriction isomorphism).

theorem AnalyticSpace.Hom.UniqueOver.gluePieceSet_compat {K : Type} [RCLike K] {A B Z : AnalyticSpace K} {f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} {g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} (huniq : UniqueOver f g) {O N N' : Set ↑↑Z.toPresheafedSpace} (hN : IsOpen N) (hNO : N ⊆ O) (hN' : IsOpen N') (hN'O : N' ⊆ O) (ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' N))) (hψ : CategoryTheory.CategoryStruct.comp ψ (restrictSetTo g N) = restrictSetTo f N) (ψ' : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N')) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' N'))) (hψ' : CategoryTheory.CategoryStruct.comp ψ' (restrictSetTo g N') = restrictSetTo f N') : CategoryTheory.CategoryStruct.comp ((A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).restrictIncl ⋯) (gluePieceSet f g hN hNO ψ) = CategoryTheory.CategoryStruct.comp ((A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).restrictIncl ⋯) (gluePieceSet f g hN' hN'O ψ')

Two pieces agree on the overlap of their members (the GlueCompatible of the gluing): both are morphisms A | f⁻¹(N ∩ N') ⟶ B | g⁻¹O over Z through the inclusion Z | (N ∩ N') ⟶ Z | O, equal by the uniqueness over the base; the members are identified with the restrictions to f⁻¹(N ∩ N') by the nested-opens naturality.

theorem AnalyticSpace.Hom.UniqueOver.exists_glue {K : Type} [RCLike K] {A B Z : AnalyticSpace K} {f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} {g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} (huniq : UniqueOver f g) {O : Set ↑↑Z.toPresheafedSpace} (hO : IsOpen O) {ι : Type u_1} (N : ι → Set ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), IsOpen (N i)) (hNO : ∀ (i : ι), N i ⊆ O) (hcov : ∀ x ∈ O, ∃ (i : ι), x ∈ N i) (ψ : (i : ι) → A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N i)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' N i))) (hψ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (ψ i) (restrictSetTo g (N i)) = restrictSetTo f (N i)) : ∃ (Φ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' O))), (∀ (i : ι), CategoryTheory.CategoryStruct.comp ((A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O))).ofRestrict (preimagePieceOpens f O ⋯)) Φ = gluePieceSet f g ⋯ ⋯ (ψ i)) ∧ CategoryTheory.CategoryStruct.comp Φ (restrictSetTo g O) = restrictSetTo f O

The glued morphism (the gluing in the proof of [Kol07, Theorem 36]): local morphisms ψ i : A | f⁻¹(N i) ⟶ B | g⁻¹(N i) over Z, the opens N i ⊆ O covering O, glue (glueOfCover, the pieces being compatible on the overlaps) to a morphism A | f⁻¹O ⟶ B | g⁻¹O restricting to each piece and lying over Z.

theorem AnalyticSpace.Hom.UniqueOver.exists_isIso_restrictSetTo {K : Type} [RCLike K] {A B Z : AnalyticSpace K} {f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} {g : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} (huniq : UniqueOver f g) (_huniq' : UniqueOver g f) {O : Set ↑↑Z.toPresheafedSpace} (hO : IsOpen O) (hloc : ∀ x ∈ O, ∃ (N : Set ↑↑Z.toPresheafedSpace), IsOpen N ∧ x ∈ N ∧ N ⊆ O ∧ ∃ (ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' N)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' N))), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (restrictSetTo g N) = restrictSetTo f N) : ∃ (ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' O))), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (restrictSetTo g O) = restrictSetTo f O

Local isomorphisms over the base around every point of an open O glue to an isomorphism over O, given uniqueness over the base (the uniqueness argument in the proof of [Kol07, Theorem 36]; [Wlo09, Theorem 6.0.6 (1)]). Proof: a corollary of KLocallyRingedSpace.exists_isIso_over_of_cover (Hironaka/AnalyticSpace/Glue/GlueIsoOver.lean) — the opens openOf A (f⁻¹N) are the Opens.comap of the open N (openOf_of_isOpen), so the pieces, their over-conditions and the uniqueness transport along eqToIso; the second uniqueness hypothesis _huniq' is kept in the signature (the cited theorem derives it, uniq_symm); the gluing lemmas of this file (gluePieceSet and its properties) are general lemmas not on this proof path.

theorem AnalyticSpace.Hom.isIso_iff_isIso_toKLocallyRingedSpace {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f

f is an isomorphism of An/K iff it is an isomorphism of the underlying K-local-ringed spaces (the categories share composition and identities).

theorem AnalyticSpace.restrictSet_congr_iso_hom_comp_ofRestrict_assoc {K : Type} [RCLike K] (X : AnalyticSpace K) {s t : Set ↑↑X.toPresheafedSpace} (h : s = t) {Y : KLocallyRingedSpace K} (k : X.toKLocallyRingedSpace ⟶ Y) : CategoryTheory.CategoryStruct.comp (X.restrictSet_congr_iso h).hom (CategoryTheory.CategoryStruct.comp (X.ofRestrict (X.openOf t)) k) = CategoryTheory.CategoryStruct.comp (X.ofRestrict (X.openOf s)) k

The identification of equal restrictions lies over X (reassociated form).

theorem AnalyticSpace.restrictSet_congr_iso_inv_comp_ofRestrict_assoc {K : Type} [RCLike K] (X : AnalyticSpace K) {s t : Set ↑↑X.toPresheafedSpace} (h : s = t) {Y : KLocallyRingedSpace K} (k : X.toKLocallyRingedSpace ⟶ Y) : CategoryTheory.CategoryStruct.comp (X.restrictSet_congr_iso h).inv (CategoryTheory.CategoryStruct.comp (X.ofRestrict (X.openOf s)) k) = CategoryTheory.CategoryStruct.comp (X.ofRestrict (X.openOf t)) k

The inverse identification of equal restrictions lies over X (reassociated form).

theorem AnalyticSpace.Hom.existsUnique_isIso_restrictSetTo_transport {K : Type} [RCLike K] {A B Z Z' : AnalyticSpace K} (f : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (g : B.toKLocallyRingedSpace ⟶ Z'.toKLocallyRingedSpace) (φ : Z.toKLocallyRingedSpace ⟶ Z'.toKLocallyRingedSpace) [CategoryTheory.IsIso φ] {O : Set ↑↑Z'.toPresheafedSpace} {O' : Set ↑↑Z.toPresheafedSpace} (hO' : O' = KLocallyRingedSpace.Hom.toFun φ ⁻¹' O) {g' : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace} (hg' : CategoryTheory.CategoryStruct.comp g' φ = g) (h : ∃! ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' O')) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g' ⁻¹' O')), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (restrictSetTo g' O') = restrictSetTo f O') : ∃! ψ : A.restrictOpen (A.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' KLocallyRingedSpace.Hom.toFun φ ⁻¹' O)) ⟶ B.restrictOpen (B.openOf (KLocallyRingedSpace.Hom.toFun g ⁻¹' O)), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (restrictSetTo g O) = CategoryTheory.CategoryStruct.comp (restrictSetTo f (KLocallyRingedSpace.Hom.toFun φ ⁻¹' O)) (restrictSetTo φ O)

Transport of the unique isomorphism over the base along an isomorphism of bases ([Kol07, Theorem 36, proof]; [Wlo09, Theorem 6.0.6 (2)]): for f : A ⟶ Z, g : B ⟶ Z' and an isomorphism φ : Z ⟶ Z', the unique isomorphism A | f⁻¹O' ≅ B | g'⁻¹O' over Z | O' for g' = g ∘ φ⁻¹ and O' = φ⁻¹O is the unique isomorphism A | f⁻¹(φ⁻¹O) ≅ B | g⁻¹O over φ | O — the restrictions transported along the identity of the sets g'⁻¹O' = g⁻¹O (restrictSet_congr_iso), the compatibilities read in Z' (the open immersion Z' | O ⟶ Z' is a monomorphism).