Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.LocalRepresentability.glueData

{F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) → AlgebraicGeometry.Scheme.GlueData

We get a family of gluing data by taking U i = X i and V i j = (hf i).rep.pullback (f j).

Defined in

Mathlib.AlgebraicGeometry.Sites.Representability

Cited by

13 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound