Module

CommonCover.lean

Nyll.SchemeTheory.Gluing.CommonCover

2 declarations indexed from sourceView source ↗

Module documentation

Recovering schemes from common open covers

Imports2

Mathlib.AlgebraicGeometry.Gluing
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by5

theorem

exists_iso_of_common_open_cover

L20 ↗

AlgebraicGeometry.Scheme.Cover.exists_iso_of_common_open_cover

Documentation

Two schemes covered by the same charts with the same actual overlaps are isomorphic, with the isomorphism respecting each chart map.

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.Cover

Lean source · statement

theorem exists_iso_of_common_open_cover
    {ι : Type u} (X Y : Scheme.{u}) (A : ι → Scheme.{u}) (V : ι × ι → Scheme.{u})
    (d : ∀ i j : ι, V (i, j) ⟶ A i) (r : ∀ i j : ι, V (i, j) ⟶ A j)
    (a : ∀ i : ι, A i ⟶ X) (b : ∀ i : ι, A i ⟶ Y)
    [∀ i : ι, IsOpenImmersion (a i)] [∀ i : ι, IsOpenImmersion (b i)]
    (ha : ∀ x : X, ∃ (i : ι) (z : A i), a i z = x)
    (hb : ∀ y : Y, ∃ (i : ι) (z : A i), b i z = y)
    (hA : ∀ i j : ι, IsPullback (d i j) (r i j) (a i) (a j))
    (hB : ∀ i j : ι, IsPullback (d i j) (r i j) (b i) (b j)) :
    ∃ e : X ≅ Y, ∀ i : ι, a i ≫ e.hom = b i

theorem

isPullback_of_cartesian_chart_overlap

L65 ↗

AlgebraicGeometry.Scheme.Cover.isPullback_of_cartesian_chart_overlap