Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.LocalRepresentability.representableBy

{F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) →
          [CategoryTheory.Presheaf.IsLocallySurjective AlgebraicGeometry.Scheme.zariskiTopology
                (CategoryTheory.Limits.Sigma.desc f)] →
            F.obj.RepresentableBy (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued

Suppose * F is a Type u-valued sheaf on Sch with respect to the Zariski topology * X : ι → Sch is a family of schemes * f : Π i, yoneda.obj (X i) ⟶ F is a family of relatively representable open immersions * f is jointly surjective Then F is representable, and the representing object is glued from the X is

Defined in

Mathlib.AlgebraicGeometry.Sites.Representability

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Presheaf.IsLocallySurjective