Isomorphisms over a base, glued along an open cover of the base

The resolutions of two pieces of a cover are identified over their overlap: the resolution is independent of the chosen embedding up to a canonical isomorphism [Kol07, Theorem 36, proof], and it commutes with open embeddings [Kol07, 44] and with local analytic isomorphisms [Wlo09, §4]. When an isomorphism over the base between two resolutions of one open subset is unique, the identifications given on the members of an open cover of the overlap agree where the members meet, and glue to one over the whole overlap. That is the statement here, for K-locally-ringed spaces over a base with the uniqueness as hypothesis. Two K-locally-ringed spaces A, B over Z (πA, πB), an open subset O ⊆ Z covered by open subsets N i ≤ O, and isomorphisms s i : A|πA⁻¹(N i) ≅ B|πB⁻¹(N i) over Z, unique among such on every open subset O' ≤ O: they glue to an isomorphism A|πA⁻¹O ≅ B|πB⁻¹O over Z.

• KLocallyRingedSpace.restrictOver: the restriction of a morphism over Z between the parts over P to the parts over Q ≤ P, with its compatibility lemmas; an isomorphism over Z restricts to an isomorphism (isIso_restrictOver), and uniqueness of isomorphisms over Z from A to B gives uniqueness from B to A (uniq_symm).
• KLocallyRingedSpace.glueIsoPieces: the morphism A|πA⁻¹O ⟶ B|πB⁻¹O assembled from the s i by glueOfCover on the cover of A|πA⁻¹O by the parts over the N i; the pieces agree on the overlaps by the uniqueness at N i ⊓ N j (gluePiece_compatible); it lies over Z (glueIsoPieces_over) and restricts to the pieces (ofRestrict_comp_glueIsoPieces).
• KLocallyRingedSpace.glueIsoPieces_comp_glueIsoPieces: the assemblies of two piecewise inverse families are inverse (hom_ext_of_cover).
• KLocallyRingedSpace.exists_isIso_over_of_cover: the statement.

The restriction restrictOver is the transition of a gluing datum restricted to the parts over a smaller base open subset (Hironaka.Resolution.Analytic.Kol07Thm45.Glue.OverRigidity, Hironaka.Resolution.Analytic.Kol07Thm45.PieceTransitionGlue, PieceGlueIndep, ResolutionFunctorial, RigidOverLocalResolution, CoproductLevelPair); exists_isIso_over_of_cover gives the transition isomorphisms between the local resolutions of two pieces over their overlap (Hironaka.Resolution.Analytic.Kol07Thm45.PieceTransitionGlue, PieceGlueIndep, ResolutionFunctorial, Hironaka.Resolution.Analytic.Kol07Thm45.RestrictSetIncl).

Restricting a morphism over Z to a smaller open of the base

theorem AnalyticSpace.KLocallyRingedSpace.toFun_π_eq_of_over {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) (x : ↑↑(A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)).toPresheafedSpace) : Hom.toFun πB ↑(Hom.toFun s x) = Hom.toFun πA ↑x

A morphism over Z preserves the point of the base.

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictOver {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) Q) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) Q)

The restriction of a morphism over Z between the parts over P to the parts over Q ≤ P: the lift of A|πA⁻¹Q ⟶ A|πA⁻¹P ⟶ B|πB⁻¹P ⟶ B through B|πB⁻¹Q ⟶ B.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.restrictOver_comp_ofRestrict {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) : CategoryTheory.CategoryStruct.comp (restrictOver πA πB hQP s hs) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) Q)) = CategoryTheory.CategoryStruct.comp (A.restrictIncl ⋯) (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)))

The restriction of s to the parts over Q lies over s: followed by the inclusion of B|πB⁻¹Q into B it is the inclusion of A|πA⁻¹Q into A|πA⁻¹P followed by s and the inclusion into B (liftRestrict's factorization).

theorem AnalyticSpace.KLocallyRingedSpace.restrictOver_comp_ofRestrict_assoc {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) {Z✝ : KLocallyRingedSpace K} (h : B ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (restrictOver πA πB hQP s hs) (CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) Q)) h) = CategoryTheory.CategoryStruct.comp (A.restrictIncl ⋯) (CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) h))

The restriction of s to the parts over Q lies over s: followed by the inclusion of B|πB⁻¹Q into B it is the inclusion of A|πA⁻¹Q into A|πA⁻¹P followed by s and the inclusion into B (liftRestrict's factorization).

theorem AnalyticSpace.KLocallyRingedSpace.restrictOver_comp_restrictIncl {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) : CategoryTheory.CategoryStruct.comp (restrictOver πA πB hQP s hs) (B.restrictIncl ⋯) = CategoryTheory.CategoryStruct.comp (A.restrictIncl ⋯) s

The restriction of s to the parts over Q, followed by the inclusion of open subspaces B|πB⁻¹Q ⟶ B|πB⁻¹P, is the inclusion A|πA⁻¹Q ⟶ A|πA⁻¹P followed by s (both sides agree after the open immersion into B).

theorem AnalyticSpace.KLocallyRingedSpace.restrictOver_comp_restrictIncl_assoc {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) {Z✝ : KLocallyRingedSpace K} (h : B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (restrictOver πA πB hQP s hs) (CategoryTheory.CategoryStruct.comp (B.restrictIncl ⋯) h) = CategoryTheory.CategoryStruct.comp (A.restrictIncl ⋯) (CategoryTheory.CategoryStruct.comp s h)

The restriction of s to the parts over Q, followed by the inclusion of open subspaces B|πB⁻¹Q ⟶ B|πB⁻¹P, is the inclusion A|πA⁻¹Q ⟶ A|πA⁻¹P followed by s (both sides agree after the open immersion into B).

theorem AnalyticSpace.KLocallyRingedSpace.restrictOver_over {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) Q)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (restrictOver πA πB hQP s hs) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) Q))) πB

The restriction of a morphism over Z is over Z.

theorem AnalyticSpace.KLocallyRingedSpace.inv_over {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) [CategoryTheory.IsIso s] : CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv s) (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P))) πA

The inverse of an isomorphism over Z is over Z.

theorem AnalyticSpace.KLocallyRingedSpace.restrictOver_comp_restrictOver {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) (t : B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P) ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) (ht : CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P))) πA) (hst : CategoryTheory.CategoryStruct.comp s t = CategoryTheory.CategoryStruct.id (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P))) : CategoryTheory.CategoryStruct.comp (restrictOver πA πB hQP s hs) (restrictOver πB πA hQP t ht) = CategoryTheory.CategoryStruct.id (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) Q))

The restrictions of two piecewise inverse morphisms over Z are inverse.

theorem AnalyticSpace.KLocallyRingedSpace.isIso_restrictOver {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) {P Q : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (hQP : Q ≤ P) (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P)) (hs : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) P)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) P))) πB) [CategoryTheory.IsIso s] : CategoryTheory.IsIso (restrictOver πA πB hQP s hs)

An isomorphism over Z restricts to an isomorphism over Z.

theorem AnalyticSpace.KLocallyRingedSpace.uniq_symm {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') (O' : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hO' : O' ≤ O) (t t' : B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O') ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) (ht : CategoryTheory.IsIso t) (ht' : CategoryTheory.IsIso t') (hto : CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O'))) πA) (hto' : CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t' (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O'))) πA) : t = t'

Uniqueness of the isomorphisms over Z from the parts of A to the parts of B over every open O' ≤ O gives the uniqueness of those from B to A: the inverses are isomorphisms over Z from A to B.

The gluing of the local isomorphisms

def AnalyticSpace.KLocallyRingedSpace.glueCoverOpens {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (i : ι) : TopologicalSpace.Opens ↑↑(A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).toPresheafedSpace

The cover of A|πA⁻¹O by the parts over the N i.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.mem_glueCoverOpens {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {i : ι} {x : ↑↑(A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).toPresheafedSpace} : x ∈ glueCoverOpens πA O N i ↔ Hom.toFun πA ↑x ∈ N i

A point of A|πA⁻¹O lies in the i-th member of the cover iff its base point lies in N i (definitional).

theorem AnalyticSpace.KLocallyRingedSpace.glueCoverOpens_cover {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (x : ↑↑(A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).toPresheafedSpace) : ∃ (i : ι), x ∈ glueCoverOpens πA O N i

The parts over the N i cover A|πA⁻¹O, since the N i cover O.

noncomputable def AnalyticSpace.KLocallyRingedSpace.pieceIncl {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (i : ι) : (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).restrictOpen (glueCoverOpens πA O N i) ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))

The inclusion of a member of the cover into the part of A over N i.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.pieceIncl_comp_ofRestrict {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (i : ι) : CategoryTheory.CategoryStruct.comp (pieceIncl πA O N i) (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) = CategoryTheory.CategoryStruct.comp ((A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).ofRestrict (glueCoverOpens πA O N i)) (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O))

The inclusion of a member of the cover into A|πA⁻¹(N i), followed by the open immersion into A, is the composite of the two open immersions (A|πA⁻¹O)|_{cover} ⟶ A|πA⁻¹O ⟶ A (liftRestrict's factorization).

theorem AnalyticSpace.KLocallyRingedSpace.pieceIncl_comp_ofRestrict_assoc {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (i : ι) {Z✝ : KLocallyRingedSpace K} (h : A ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pieceIncl πA O N i) (CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) h) = CategoryTheory.CategoryStruct.comp ((A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).ofRestrict (glueCoverOpens πA O N i)) (CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)) h)

The inclusion of a member of the cover into A|πA⁻¹(N i), followed by the open immersion into A, is the composite of the two open immersions (A|πA⁻¹O)|_{cover} ⟶ A|πA⁻¹O ⟶ A (liftRestrict's factorization).

noncomputable def AnalyticSpace.KLocallyRingedSpace.gluePiece {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (i : ι) : (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).restrictOpen (glueCoverOpens πA O N i) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O)

The piece of the gluing over N i: s i on the part over N i, followed by the inclusion into B|πB⁻¹O.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.gluePiece_comp_ofRestrict {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (i : ι) : CategoryTheory.CategoryStruct.comp (gluePiece πA πB O N hN s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O)) = CategoryTheory.CategoryStruct.comp (pieceIncl πA O N i) (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))))

The i-th piece of the gluing, followed by the open immersion B|πB⁻¹O ⟶ B, is pieceIncl i ≫ s i followed by the open immersion B|πB⁻¹(N i) ⟶ B (liftRestrict's factorization).

theorem AnalyticSpace.KLocallyRingedSpace.gluePiece_comp_ofRestrict_assoc {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (i : ι) {Z✝ : KLocallyRingedSpace K} (h : B ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (gluePiece πA πB O N hN s i) (CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O)) h) = CategoryTheory.CategoryStruct.comp (pieceIncl πA O N i) (CategoryTheory.CategoryStruct.comp (s i) (CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) h))

The i-th piece of the gluing, followed by the open immersion B|πB⁻¹O ⟶ B, is pieceIncl i ≫ s i followed by the open immersion B|πB⁻¹(N i) ⟶ B (liftRestrict's factorization).

theorem AnalyticSpace.KLocallyRingedSpace.gluePiece_compatible {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (hiso : ∀ (i : ι), CategoryTheory.IsIso (s i)) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') : GlueCompatible (glueCoverOpens πA O N) (gluePiece πA πB O N hN s)

The pieces agree on the overlaps: both restrictions to the part over N i ⊓ N j are isomorphisms over Z, hence equal by the uniqueness hypothesis.

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueIsoPieces {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (hiso : ∀ (i : ι), CategoryTheory.IsIso (s i)) (hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O)

The morphism A|πA⁻¹O ⟶ B|πB⁻¹O glued from the local isomorphisms s i along the cover of A|πA⁻¹O by the parts over the N i.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.ofRestrict_comp_glueIsoPieces {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (hiso : ∀ (i : ι), CategoryTheory.IsIso (s i)) (hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') (i : ι) : CategoryTheory.CategoryStruct.comp ((A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).ofRestrict (glueCoverOpens πA O N i)) (glueIsoPieces πA πB O N hN s hs hiso hcov huniq) = gluePiece πA πB O N hN s i

The glued morphism restricts to the i-th piece on the i-th member of the cover (ofRestrict_comp_glueOfCover).

theorem AnalyticSpace.KLocallyRingedSpace.ofRestrict_comp_glueIsoPieces_assoc {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (hiso : ∀ (i : ι), CategoryTheory.IsIso (s i)) (hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') (i : ι) {Z✝ : KLocallyRingedSpace K} (h : B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).ofRestrict (glueCoverOpens πA O N i)) (CategoryTheory.CategoryStruct.comp (glueIsoPieces πA πB O N hN s hs hiso hcov huniq) h) = CategoryTheory.CategoryStruct.comp (gluePiece πA πB O N hN s i) h

The glued morphism restricts to the i-th piece on the i-th member of the cover (ofRestrict_comp_glueOfCover).

theorem AnalyticSpace.KLocallyRingedSpace.glueIsoPieces_over {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (hiso : ∀ (i : ι), CategoryTheory.IsIso (s i)) (hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') : CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (glueIsoPieces πA πB O N hN s hs hiso hcov huniq) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O))) πB

The glued morphism lies over Z.

theorem AnalyticSpace.KLocallyRingedSpace.glueIsoPieces_comp_glueIsoPieces {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (s : (i : ι) → A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (s i) (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (hiso : ∀ (i : ι), CategoryTheory.IsIso (s i)) (hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') (t : (i : ι) → B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)) ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) (ht : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t i) (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)))) πA) (htiso : ∀ (i : ι), CategoryTheory.IsIso (t i)) (huniqB : ∀ O' ≤ O, ∀ (s s' : B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O') ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O'))) πA → CategoryTheory.CategoryStruct.comp (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')) πB = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O'))) πA → s = s') (hst : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (s i) (t i) = CategoryTheory.CategoryStruct.id (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)))) : CategoryTheory.CategoryStruct.comp (glueIsoPieces πA πB O N hN s hs hiso hcov huniq) (glueIsoPieces πB πA O N hN t ht htiso hcov huniqB) = CategoryTheory.CategoryStruct.id (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O))

The assemblies of two piecewise inverse families of isomorphisms over Z are inverse.

theorem AnalyticSpace.KLocallyRingedSpace.exists_isIso_over_of_cover {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (πB : B ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (_hN : ∀ (i : ι), N i ≤ O) (_hcov : ∀ z ∈ O, ∃ (i : ι), z ∈ N i) (_hloc : ∀ (i : ι), ∃ (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i)) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i))), CategoryTheory.IsIso s ∧ CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) (N i))) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) (N i)))) πB) (_huniq : ∀ O' ≤ O, ∀ (s s' : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O') ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O')), CategoryTheory.IsIso s → CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O')) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O'))) πB → s = s') : ∃ (s : A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O) ⟶ B.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s ∧ CategoryTheory.CategoryStruct.comp (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)) πA = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (B.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πB, continuous_toFun := ⋯ }) O))) πB

Isomorphisms over Z glue along an open cover of the base: isomorphisms over Z between the parts of A and B over the members of an open cover of an open subset O ⊆ Z, unique among such on every open subset of O, glue to an isomorphism over Z between the parts over O (glueOfCover on the cover pulled back to A, hom_ext_of_cover).