Documentation

Mathlib.AlgebraicGeometry.Sites.Representability

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 #

References #

source
noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.glueData {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (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.
Instances For
    source
    @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i j : ι) :
    (glueData hf).t i j = ⋯.symmetry ⋯
    source
    @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) :
    (glueData hf).J = ι
    source
    @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (x✝ : ι × ι) :
    (glueData hf).V x✝ = match x✝ with | (i, j) => ⋯.pullback (f j)
    source
    @[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.obj} (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)) ⋯ ⋯
    source
    @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (a✝ : ι) :
    (glueData hf).U a✝ = X a✝
    source
    @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i j : ι) :
    (glueData hf).f i j = ⋯.fst' (f j)
    source
    noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.toGlued {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (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
    Instances For
      source
      instance AlgebraicGeometry.Scheme.LocalRepresentability.instIsOpenImmersionToGlued {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) :
      IsOpenImmersion (toGlued hf i)
      source
      noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (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.
      Instances For
        source
        @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (toGlued hf i)) (yonedaGluedToSheaf hf).hom = f i
        source
        @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (i : ι) {Z : CategoryTheory.Functor Schemeᵒᵖ (Type u)} (h : F.obj ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (toGlued hf i)) (CategoryTheory.CategoryStruct.comp (yonedaGluedToSheaf hf).hom h) = CategoryTheory.CategoryStruct.comp (f i) h
        source
        @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) {i : ι} :
        (CategoryTheory.ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (Opposite.op (X i)))) (toGlued hf i) = CategoryTheory.yonedaEquiv (f i)
        source
        @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) {V U : Scheme} (γ : V ⟶ U) (α : U ⟶ (glueData hf).glued) :
        (CategoryTheory.ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (Opposite.op V))) (CategoryTheory.CategoryStruct.comp γ α) = (CategoryTheory.ConcreteCategory.hom (F.obj.map γ.op)) ((CategoryTheory.ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (Opposite.op U))) α)
        source
        instance AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveFunYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) [CategoryTheory.Presheaf.IsLocallySurjective zariskiTopology (CategoryTheory.Limits.Sigma.desc f)] :
        CategoryTheory.Sheaf.IsLocallySurjective (yonedaGluedToSheaf hf)
        source
        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.obj} (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)
        source
        @[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.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) (j : ι) :
        (glueData hf).openCover.f j = toGlued hf j
        source
        instance AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveFunYonedaGluedToSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) :
        CategoryTheory.Sheaf.IsLocallyInjective (yonedaGluedToSheaf hf)
        source
        instance AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) [CategoryTheory.Presheaf.IsLocallySurjective zariskiTopology (CategoryTheory.Limits.Sigma.desc f)] :
        CategoryTheory.IsIso (yonedaGluedToSheaf hf)
        source
        noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.yonedaIsoSheaf {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (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
        Instances For
          source
          noncomputable def AlgebraicGeometry.Scheme.LocalRepresentability.representableBy {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) [CategoryTheory.Presheaf.IsLocallySurjective zariskiTopology (CategoryTheory.Limits.Sigma.desc f)] :
          F.obj.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.
          Instances For
            source
            theorem AlgebraicGeometry.Scheme.LocalRepresentability.isRepresentable {F : CategoryTheory.Sheaf zariskiTopology (Type u)} {ι : Type u} {X : ι → Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} (hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)) [CategoryTheory.Presheaf.IsLocallySurjective zariskiTopology (CategoryTheory.Limits.Sigma.desc f)] :
            F.obj.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.