Representability of schemes is a local property

In this file we prove that a sheaf of types F on Sch is representable if it is locally representable.

Main result

• AlgebraicGeometry.Scheme.LocalRepresentability.isRepresentable: 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.

References

• https://stacks.math.columbia.edu/tag/01JJ

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_U {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (a✝ : ι) : (glueData hf).U a✝ = X a✝

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t' {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i j k : ι) : (glueData hf).t' i j k = ⋯.lift₃ (f k) (f i) (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ ⋯ (f j) (f k)) (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ ⋯ (f j) (f k)) (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i j : ι) : (glueData hf).t i j = ⋯.symmetry ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_V {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (x✝ : ι × ι) : (glueData hf).V x✝ = match x✝ with | (i, j) => ⋯.pullback (f j)

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_J {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) : (glueData hf).J = ι

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_f {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i j : ι) : (glueData hf).f i j = ⋯.fst' (f j)

noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.toGlued {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) : X i ⟶ (glueData hf).glued

The map from X i to the glued scheme (glueData hf).glued

Equations

• AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i = (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).ι i

instance AlgebraicGeometry.Scheme.LocalRepresentability.instIsOpenImmersionToGlued {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) : IsOpenImmersion (toGlued hf i)

noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) : zariskiTopology.yoneda.obj (glueData hf).glued ⟶ F

The map from the glued scheme (glueData hf).glued, treated as a sheaf, to F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (toGlued hf i)) (yonedaGluedToSheaf hf).val = f i

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) {Z : CategoryTheory.Functor Schemeᵒᵖ (Type u)} (h : F.val ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (toGlued hf i)) (CategoryTheory.CategoryStruct.comp (yonedaGluedToSheaf hf).val h) = CategoryTheory.CategoryStruct.comp (f i) h

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) {i : ι} : (yonedaGluedToSheaf hf).val.app (Opposite.op (X i)) (toGlued hf i) = CategoryTheory.yonedaEquiv (f i)

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) {V U : Scheme} (γ : V ⟶ U) (α : U ⟶ (glueData hf).glued) : (yonedaGluedToSheaf hf).val.app (Opposite.op V) (CategoryTheory.CategoryStruct.comp γ α) = F.val.map γ.op ((yonedaGluedToSheaf hf).val.app (Opposite.op U) α)

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

theorem AlgebraicGeometry.Scheme.LocalRepresentability.comp_toGlued_eq {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) {U : Scheme} {i j : ι} (a : U ⟶ X i) (b : U ⟶ X j) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map a) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map b) (f j)) : CategoryTheory.CategoryStruct.comp a (toGlued hf i) = CategoryTheory.CategoryStruct.comp b (toGlued hf j)

@[simp]

theorem AlgebraicGeometry.Scheme.LocalRepresentability.glueData_openCover_map {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (j : ι) : (glueData hf).openCover.map j = toGlued hf j

instance AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomObjForgetTypeYonedaGluedToSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) : CategoryTheory.Sheaf.IsLocallyInjective (yonedaGluedToSheaf hf)

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

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

The isomorphism between yoneda.obj (glueData hf).glued and F.

This implies that F is representable.

Equations

• AlgebraicGeometry.Scheme.LocalRepresentability.yonedaIsoSheaf hf = CategoryTheory.asIso (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf)

noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.representableBy {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) [CategoryTheory.Presheaf.IsLocallySurjective zariskiTopology (CategoryTheory.Limits.Sigma.desc f)] : F.val.RepresentableBy (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

Equations

• One or more equations did not get rendered due to their size.

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

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.

Stacks Tag 01JJ