AlgebraicGeometry.Scheme.GlueData.exists_glueData_iso_of_overlap
Actual local comparison maps whose pairwise overlaps are the gluing overlaps construct an isomorphism from the glued scheme to the scheme they cover.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.GlueDataLean source · statement
theorem exists_glueData_iso_of_overlap
(D : Scheme.GlueData.{u}) (Z : Scheme.{u})
(q : ∀ i, D.U i ⟶ Z) [∀ i, IsOpenImmersion (q i)]
(hcover : ∀ z : Z, ∃ (i : D.J) (x : D.U i), q i x = z)
(hV : ∀ i j, IsPullback (D.f i j) (D.t i j ≫ D.f j i) (q i) (q j)) :
∃ e : D.glued ≅ Z, ∀ i, D.ι i ≫ e.hom = q i