AlgebraicGeometry.Scheme.Cover.exists_over_iso_of_common_open_cover
Recovery from common open charts retains the actual structural map to the base.
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.CoverLean source · statement
theorem exists_over_iso_of_common_open_cover
{S : Scheme.{u}} {ι : Type u} (X Y : Over S)
(A : ι → Over S) (V : ι × ι → Scheme.{u})
(d : ∀ i j : ι, V (i, j) ⟶ (A i).left)
(r : ∀ i j : ι, V (i, j) ⟶ (A j).left)
(a : ∀ i : ι, A i ⟶ X) (b : ∀ i : ι, A i ⟶ Y)
[∀ i : ι, IsOpenImmersion (a i).left] [∀ i : ι, IsOpenImmersion (b i).left]
(ha : ∀ x : X.left, ∃ (i : ι) (z : (A i).left), (a i).left z = x)
(hb : ∀ y : Y.left, ∃ (i : ι) (z : (A i).left), (b i).left z = y)
(hA : ∀ i j : ι, IsPullback (d i j) (r i j) (a i).left (a j).left)
(hB : ∀ i j : ι, IsPullback (d i j) (r i j) (b i).left (b j).left) :
∃ e : X ≅ Y, ∀ i : ι, a i ≫ e.hom = b i