99.13 The stack of algebraic… to 99.16 Moduli of complexes on a…

Section99.13 The stack of algebraic spaces#

Section 99.13 of the Stacks Project, Tag 0D1D. 10 tags here are carried by 22 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0D1D, the section

Tag 0D1D in the Stacks Project.

AlgebraicGeometry.cartesianProperFlatInclusion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpaces.lean, line 130. The attribute's comment: “the subcategory of finitely presented, flat and proper families”.

Stacks 0D1D. The inclusion Spaces'_{fp, flat, proper} ⊂ Spaces'_{ft} of the families of algebraic spaces that are of finite presentation, flat and proper over their base scheme into all the finite-type families, both taken with cartesian morphisms only.

abbrev cartesianProperFlatInclusion :
    CartesianProperFlatSpaces B S hS ⥤ CartesianFiniteTypeSpaces B S hS

AlgebraicGeometry.fullyFaithfulCartesianProperFlatInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpaces.lean, line 139. The attribute's comment: “the subcategory is full”.

Stacks 0D1D. The subcategory Spaces'_{fp, flat, proper} of Spaces'_{ft} is full: a cartesian morphism of finite-type families whose source and target are of finite presentation, flat and proper is a morphism of Spaces'_{fp, flat, proper}, with no further condition.

def fullyFaithfulCartesianProperFlatInclusion :
    (cartesianProperFlatInclusion B S hS).FullyFaithful

AlgebraicGeometry.cartesianProperFlatInclusion_comp_cartesianFiniteTypeProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpaces.lean, line 147. The attribute's comment: “the projection of the subcategory is the restriction of the projection”.

Stacks 0D1D. The projection p'_{fp, flat, proper} is the restriction of the projection p'_{ft} to the subcategory Spaces'_{fp, flat, proper}.

theorem cartesianProperFlatInclusion_comp_cartesianFiniteTypeProjection :
    cartesianProperFlatInclusion B S hS ⋙ cartesianFiniteTypeProjection B S hS =
      cartesianProperFlatProjection B S hS

Declarations registered for the tag:

Tag 0D1E, a lemma

Tag 0D1E in the Stacks Project.

AlgebraicGeometry.cartesianFiniteTypeProjection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CartesianFamilies.lean, line 160. The attribute's comment: “finite-type families”.

Finite-type algebraic spaces over varying base schemes, with cartesian squares as morphisms, form a category fibred in groupoids over the big fppf site of S.

theorem cartesianFiniteTypeProjection_isFiberedInGroupoids :
    (cartesianFiniteTypeProjection B S hS).IsFiberedInGroupoids

AlgebraicGeometry.cartesianProperFlatProjection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CartesianFamilies.lean, line 209. The attribute's comment: “finitely presented, flat and proper families”.

Algebraic spaces whose structure morphism is of finite presentation, flat and proper over a varying base scheme, with cartesian squares as morphisms, form a category fibred in groupoids over the big fppf site of S.

theorem cartesianProperFlatProjection_isFiberedInGroupoids :
    (cartesianProperFlatProjection B S hS).IsFiberedInGroupoids
Tag 0D1F, a lemma

Tag 0D1F in the Stacks Project.

AlgebraicGeometry.Space.hasAlgebraicIsomFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesDiagonal.lean, line 514. The attribute's comment: “the Isom functor of two finitely presented, flat and proper families is an algebraic space, which is criterion (2) of Stacks 045G for the diagonal”.

Criterion (2) of Stacks 045G in concrete form, assuming Stacks 0D01: the isomorphism functor of two finitely presented, flat and proper families over a scheme of the site is an algebraic space.

theorem hasAlgebraicIsomFunctors (hilb : HasHilbertModels B S hS) :
    HasAlgebraicIsomFunctors B S hS

AlgebraicGeometry.Space.hasRepresentableDiagonal_properFlatSpacesStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesDiagonal.lean, line 542. The attribute's comment: “the diagonal is representable by algebraic spaces”.

Stacks 0D1F. The diagonal

  Spaces'_{fp, flat, proper} ⟶ Spaces'_{fp, flat, proper} × Spaces'_{fp, flat, proper}

is representable by algebraic spaces, assuming Stacks 0D01 (hilb) and that the isomorphism presheaf of the fibre of the stack over a scheme U is algebraic whenever the isomorphism functors Isom_U(Z, X) of finitely presented, flat and proper families over U are (hcmp).

theorem hasRepresentableDiagonal_properFlatSpacesStack (hilb : HasHilbertModels B S hS)
    (hcmp : HasAlgebraicIsomFunctors B S hS →
      Stack.IsAlgebraicSpaceIsomPresheaf B S hS (properFlatSpacesStack B S hS)) :
    Stack.HasRepresentableDiagonal B S hS (properFlatSpacesStack B S hS)

AlgebraicGeometry.Space.properFlatSpacesStack_hasRepresentableDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesDiagonalUnconditional.lean, line 69. The attribute's comment: “the diagonal is representable by algebraic spaces; Stacks 0D01 is proved, AlgebraicGeometry.Space.hasHilbertModels”.

The diagonal of Spaces'_{fp, flat, proper} is representable by algebraic spaces. The diagonal

  Spaces'_{fp, flat, proper} ⟶ Spaces'_{fp, flat, proper} × Spaces'_{fp, flat, proper}

of the stack of Stacks 0D1D over the big fppf site of S is representable by algebraic spaces.

theorem properFlatSpacesStack_hasRepresentableDiagonal :
    Stack.HasRepresentableDiagonal B S hS (properFlatSpacesStack B S hS)
Tag 0D1G, a lemma

Tag 0D1G in the Stacks Project.

AlgebraicGeometry.cartesianFiniteTypeProjection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesStack.lean, line 110. The attribute's comment: “Spaces'_ft is fibred in groupoids and a stack (Stacks 02ZJ (3))”.

Stacks 0D1G, the finite-type families, in the form of Stacks 02ZJ (3): Spaces'_ft is fibred in groupoids and is a stack over the big fppf site of S (Stacks 026F).

theorem cartesianFiniteTypeProjection_isStack :
    (cartesianFiniteTypeProjection B S hS).IsFiberedInGroupoids ∧
      (cartesianFiniteTypeProjection B S hS).IsStack (BigFppfOver.topology B S hS)

AlgebraicGeometry.cartesianProperFlatProjection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesStack.lean, line 336. The attribute's comment: “Spaces'_{fp, flat, proper} is fibred in groupoids and a stack (Stacks 02ZJ (3))”.

Stacks 0D1G, the finitely presented, flat and proper families, in the form of Stacks 02ZJ (3): Spaces'_{fp, flat, proper} is fibred in groupoids and is a stack over the big fppf site of S (Stacks 026F).

theorem cartesianProperFlatProjection_isStack :
    (cartesianProperFlatProjection B S hS).IsFiberedInGroupoids ∧
      (cartesianProperFlatProjection B S hS).IsStack (BigFppfOver.topology B S hS)

AlgebraicGeometry.stackOfSpaces_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesStack.lean, line 346.

Stacks 0D1G. The category Spaces'_ft is a stack in groupoids over the big fppf site of S, and so is Spaces'_{fp, flat, proper} (Stacks 02ZI).

theorem stackOfSpaces_isStackInGroupoids.{w} :
    (cartesianFiniteTypeProjection B S hS).IsStackInGroupoids.{w}
        (BigFppfOver.topology B S hS) ∧
      (cartesianProperFlatProjection B S hS).IsStackInGroupoids.{w}
        (BigFppfOver.topology B S hS)

Declarations registered for the tag:

Tag 0E93, a lemma

Tag 0E93 in the Stacks Project.

AlgebraicGeometry.SpacesOverSpace.finiteTypeBaseChange_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/SpacesOverSpaceEquivalence.lean, line 109. The attribute's comment: “the first equivalence: finite type morphisms X ⟶ T and functors 𝒮_T ⟶ Spaces'_ft”.

Stacks 0E93, the first equivalence: finite type morphisms of algebraic spaces X ⟶ T, with isomorphisms over T, are equivalent through base change to the functors over the site from the algebraic stack 𝒮_T of T to the stack Spaces'_ft of finite type families of algebraic spaces.

theorem finiteTypeBaseChange_isEquivalence : (finiteTypeBaseChange B S hS T).IsEquivalence

AlgebraicGeometry.SpacesOverSpace.properFlatBaseChange_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/SpacesOverSpaceEquivalence.lean, line 119. The attribute's comment: “the second equivalence: finitely presented, flat and proper morphisms X ⟶ T and functors 𝒮_T ⟶ Spaces'_{fp, flat, proper}”.

Stacks 0E93, the second equivalence: finitely presented, flat and proper morphisms of algebraic spaces X ⟶ T, with isomorphisms over T, are equivalent through base change to the functors over the site from the algebraic stack 𝒮_T of T to the stack Spaces'_{fp, flat, proper} of finitely presented, flat and proper families.

theorem properFlatBaseChange_isEquivalence : (properFlatBaseChange B S hS T).IsEquivalence

AlgebraicGeometry.SpacesOverSpace.spacesOverSpace_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/SpacesOverSpaceEquivalence.lean, line 128. The attribute's comment: “both equivalences”.

Stacks 0E93. Base change along the points of an algebraic space T gives an equivalence of finite type morphisms X ⟶ T with the functors over the site from 𝒮_T to Spaces'_ft, and an equivalence of finitely presented, flat and proper morphisms X ⟶ T with the functors over the site from 𝒮_T to Spaces'_{fp, flat, proper}.

theorem spacesOverSpace_isEquivalence :
    (finiteTypeBaseChange B S hS T).IsEquivalence ∧
      (properFlatBaseChange B S hS T).IsEquivalence
Tag 0D1H, a remark

Tag 0D1H in the Stacks Project.

AlgebraicGeometry.CartesianFiniteTypeSpacesOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/FamiliesOverBaseSpace.lean, line 196. The attribute's comment: “the category of finite-type families over a base algebraic space”.

Stacks 0D1H. The category Z-Spaces'_{ft} of finite-type families of algebraic spaces over a fixed algebraic space Z: an object is a finite-type family X ⟶ T of algebraic spaces together with a morphism from its base scheme to Z, and a morphism is a cartesian morphism of families commuting with those morphisms.

abbrev CartesianFiniteTypeSpacesOver

AlgebraicGeometry.isEquivalence_cartesianFiniteTypeSpacesOverToTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/FamiliesOverBaseSpace.lean, line 227. The attribute's comment: “the 2-fibre product square for finite-type families”.

Stacks 0D1H for finite-type families. The absolute and the relative categories of finite-type families of algebraic spaces form a 2-fibre product square over the big fppf site of S: the canonical comparison from the finite-type families over Z to the 2-fibre product of the finite-type families with the schemes over Z is an equivalence.

theorem isEquivalence_cartesianFiniteTypeSpacesOverToTwoFibreProduct :
    (cartesianFiniteTypeSpacesOverToTwoFibreProduct B S hS Z).IsEquivalence

AlgebraicGeometry.CartesianProperFlatSpacesOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/FamiliesOverBaseSpace.lean, line 237. The attribute's comment: “the category of finitely presented, flat and proper families over a base space”.

Stacks 0D1H. The category Z-Spaces'_{fp, flat, proper} of finitely presented, flat and proper families of algebraic spaces over a fixed algebraic space Z: an object is such a family X ⟶ T together with a morphism from its base scheme to Z, and a morphism is a cartesian morphism of families commuting with those morphisms.

abbrev CartesianProperFlatSpacesOver

AlgebraicGeometry.isEquivalence_cartesianProperFlatSpacesOverToTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/FamiliesOverBaseSpace.lean, line 268. The attribute's comment: “the 2-fibre product square for finitely presented, flat and proper families”.

Stacks 0D1H for finitely presented, flat and proper families. The absolute and the relative categories of finitely presented, flat and proper families of algebraic spaces form a 2-fibre product square over the big fppf site of S: the canonical comparison from such families over Z to the 2-fibre product of such families with the schemes over Z is an equivalence.

theorem isEquivalence_cartesianProperFlatSpacesOverToTwoFibreProduct :
    (cartesianProperFlatSpacesOverToTwoFibreProduct B S hS Z).IsEquivalence
Tag 0D1I, a lemma

Tag 0D1I in the Stacks Project.

AlgebraicGeometry.isLimitPreserving_cartesianProperFlatFiberedCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StackOfSpacesLimitPreservingUnconditional.lean, line 187. The attribute's comment: “over the big fppf site of an arbitrary base scheme S; the source's Sch_fppf is S = Spec(ℤ)”.

The stack p'_{fp, flat, proper} : Spaces'_{fp, flat, proper} ⟶ Sch_fppf of finitely presented, flat and proper families of algebraic spaces is limit preserving (Stacks 07XL): for every directed inverse system of affine schemes Tᵢ of the site with limit T in the site, base change is an equivalence from the colimit of the fibre categories over the Tᵢ to the fibre category over T.

The base is the big fppf site of an arbitrary scheme S of the site, which recovers Sch_fppf at S = Spec(ℤ); the index categories are those of the scheme universe, the smallness of the directed sets of Stacks 07XL.

theorem isLimitPreserving_cartesianProperFlatFiberedCategory
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u + 1} B S hS
      (cartesianProperFlatFiberedCategory B S hS)
Tag 0D1J, a lemma

Tag 0D1J in the Stacks Project.

AlgebraicGeometry.Space.properPushoutRS, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ProperPushoutGluingUnconditional.lean, line 44.

[Stacks Project, Tag 0D1J]. For every pushout S' = S ⨿_T T' of schemes of the site along a thickening T ⟶ T' and an affine morphism T ⟶ S, the canonical restriction functor from the finitely presented, flat and proper algebraic spaces over S' to the compatible pairs of such spaces over S and T' is an equivalence.

def properPushoutRS : ProperPushoutRS B S₀ hS₀
Tag 0D1K, a lemma

Tag 0D1K in the Stacks Project.

AlgebraicGeometry.ProperFlatSpaceDeformation.finiteDimensional_predeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ProperFlatStackFiniteDimensional.lean, line 69. The attribute's comment: “(1): for a field k of finite type over Z and an object x of Spaces'_{fp,flat,proper} over Spec k, the predeformation category F_{X,k,x} over C_Z is a deformation category whose tangent space T F_{X,k,x} and infinitesimal automorphisms Inf(F_{X,k,x}) (Section 07WY) are finite dimensional”.

Let k be a field of finite type over ℤ and let x = (X → Spec k) be an object of 𝒳 = Spaces'_{fp, flat, proper} over Spec k. Then the predeformation category 𝓕_{𝒳,k,x} of Stacks 07T2, over 𝒞_ℤ, is a deformation category, its tangent space T𝓕_{𝒳,k,x} is a finite-dimensional k-vector space, and so are its infinitesimal automorphisms Inf(𝓕_{𝒳,k,x}) (Stacks 07WY), at every object of the special fibre and for every choice of its pushforwards.

The stack is formed over the big fppf site of Spec ℤ, and 𝓕_{𝒳,k,x} over 𝒞_Λ with Λ = ℤ, Spec Λ = Spec ℤ the affine open of the base containing the image of Spec k (Stacks 07T2).

theorem finiteDimensional_predeformationCategory {k : Type u} [Field k]
    [Algebra (ULift.{u} ℤ) k] [Algebra.FiniteType (ULift.{u} ℤ) k]
    (x : CartesianProperFlatSpaces B integerBase hZ)
    (hx : (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion).obj x =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap (ULift.{u} ℤ) k)) ≫ 𝟙 integerBase)) :
    ∃ hD : IsDeformationCategory.{u, u, u} (predeformationCategory (𝟙 integerBase)
        (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion) x hx).projection,
      (letI : Fact (IsPredeformationCategory (BasedCategory.ofFunctor (predeformationCategory
          (𝟙 integerBase) (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion)
            x hx).projection).p) := ⟨hD.predeformation⟩;
        letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
          (isomorphismClasses (BasedCategory.ofFunctor (predeformationCategory (𝟙 integerBase)
            (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion) x
              hx).projection) hD.predeformation.cofibered))) := ⟨tangentConditionS2.{u, u, u} hD⟩;
        FiniteDimensional k (artinianTangentSpace (ULift.{u} ℤ) k
          (isomorphismClasses (BasedCategory.ofFunctor (predeformationCategory (𝟙 integerBase)
            (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion) x
              hx).projection) hD.predeformation.cofibered))) ∧
      ∀ y, (predeformationCategory (𝟙 integerBase)
          (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion) x
            hx).projection.obj y = residueFieldObject.{u, u, u} (ULift.{u} ℤ) k →
        ∀ PF : ChosenPushforwardsAt (predeformationCategory (𝟙 integerBase)
            (cartesianProperFlatProjection B integerBase hZ ⋙ Over.post B.inclusion) x
              hx).projection y,
          FiniteDimensional k ↥((infinitesimalAutomorphismLinearLift.{u, u, u} PF
            hD.satisfiesRS).functor.obj (FGModuleCat.of k (ULift.{u} k)))

AlgebraicGeometry.ProperFlatSpaceDeformation.finiteDimensional_tangentFunctor_infinitesimalAutomorphismFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ProperFlatStackFiniteDimensional.lean, line 114. The attribute's comment: “(2): for an object x of Spaces'_{fp,flat,proper} over a field k, the functors T_x and Inf_x of Stacks 07Y9 exist (the stack satisfies RS* by 0D1J) and T_x(k) and Inf_x(k) are finite dimensional; both finiteness statements hold for every k-linear functor carrying the identifications of 07Y9”.

Let k be a field and let x = (X → Spec k) be an object of 𝒳 = Spaces'_{fp, flat, proper} over Spec k. Then the tangent functor T_x and the functor of infinitesimal automorphisms Inf_x of Stacks 07Y9 (Section 07Y6) exist — 𝒳 satisfies (RS*) by Stacks 0D1J — and T_x(k) and Inf_x(k) are finite-dimensional k-vector spaces.

Each functor is stated as a structure (TangentFunctorData, InfinitesimalAutomorphismFunctorData) carrying a k-linear functor on the site modules together with its identification with the isomorphism classes of lifts of x, respectively with the infinitesimal automorphisms of the trivial lifts of x, natural in the module. The statement gives that such a functor exists and that the value at k of every such functor is finite-dimensional, so it holds for the functors T_x and Inf_x of Stacks 07Y9, which are determined by these identifications. No condition on k is assumed.

theorem finiteDimensional_tangentFunctor_infinitesimalAutomorphismFunctor {k : Type u} [Field k]
    (toS : Spec (.of k) ⟶ integerBase) (hk : B.Contains (Spec (.of k)))
    (x : CartesianProperFlatSpaces B integerBase hZ)
    (hx : (cartesianProperFlatProjection B integerBase hZ).obj x =
      algebraOver k B integerBase hZ toS hk) :
    (Nonempty (TangentFunctorData k B integerBase hZ toS hk
        (cartesianProperFlatProjection B integerBase hZ) x hx) ∧
      ∀ T : TangentFunctorData k B integerBase hZ toS hk
          (cartesianProperFlatProjection B integerBase hZ) x hx,
        FiniteDimensional k (T.functor.obj ((fgSiteModule B hk).obj (FGModuleCat.of k k)))) ∧
    (Nonempty (InfinitesimalAutomorphismFunctorData k B integerBase hZ toS hk
        (cartesianProperFlatProjection B integerBase hZ) x hx
        (cartesianProperFlatProjection_isFiberedInGroupoids B integerBase hZ)) ∧
      ∀ I : InfinitesimalAutomorphismFunctorData k B integerBase hZ toS hk
          (cartesianProperFlatProjection B integerBase hZ) x hx
          (cartesianProperFlatProjection_isFiberedInGroupoids B integerBase hZ),
        FiniteDimensional k (I.functor.obj ((fgSiteModule B hk).obj (FGModuleCat.of k k))))
Tag 0D3X, a lemma

Tag 0D3X in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.cartesianProperFlatInclusion · AlgebraicGeometry.fullyFaithfulCartesianProperFlatInclusion · AlgebraicGeometry.cartesianProperFlatInclusion_comp_cartesianFiniteTypeProjection · AlgebraicGeometry.CartesianFiniteTypeSpaces · AlgebraicGeometry.cartesianFiniteTypeProjection · AlgebraicGeometry.isProperFlatSpace · AlgebraicGeometry.CartesianProperFlatSpaces · AlgebraicGeometry.cartesianProperFlatProjection

Section99.14 The stack of polarized proper schemes#

Section 99.14 of the Stacks Project, Tag 0D1L. 15 tags here are carried by 28 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0D1M, a situation

Tag 0D1M in the Stacks Project.

AlgebraicGeometry.PolarizedFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamilies.lean, line 73. The attribute's comment: “objects”.

Stacks 0D1M. A polarized family: a proper, flat, finitely presented morphism from a scheme to a scheme of the big fppf site, together with an invertible module on the total space which is relatively ample for that morphism.

structure PolarizedFamily

AlgebraicGeometry.PolarizedFamily.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamilies.lean, line 103. The attribute's comment: “morphisms”.

Stacks 0D1M. A morphism of polarized families: a morphism of total spaces over a morphism of base schemes whose square is cartesian, together with an isomorphism from the pullback of the polarization of the target to the polarization of the source.

structure Hom (X Y : PolarizedFamily B)

AlgebraicGeometry.PolarizedFamily.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamilies.lean, line 247. The attribute's comment: “category”.

Stacks 0D1M. Polarized families, cartesian squares between them and comparisons of polarizations form a category: the two underlying morphisms compose componentwise and the comparisons compose through the pullback pseudofunctor.

instance instCategory : Category.{u} (PolarizedFamily B)

AlgebraicGeometry.polarizedProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamilies.lean, line 278. The attribute's comment: “projection”.

Stacks 0D1M. The forgetful functor taking a polarized family to its base scheme, which is how the category of polarized families is viewed as a category over the big fppf site.

def polarizedProjection : PolarizedFamily B ⥤ B.Schemes
Tag 0D3Y, an equation

Tag 0D3Y in the Stacks Project.

AlgebraicGeometry.forgetPolarization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesForget.lean, line 258. The attribute's comment: “the forgetful functor”.

Stacks 0D3Y. Forget the polarization of a polarized family, keeping the finitely presented, flat and proper family of algebraic spaces over the same base.

def forgetPolarization :
    PolarizedFamily B ⥤ CartesianProperFlatSpaces B integerBase B.contains_integerBase

AlgebraicGeometry.forgetPolarization_obj_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesForget.lean, line 306. The attribute's comment: “the forgetful functor is over the site”.

Stacks 0D3Y. Forgetting the polarization keeps the base scheme, so the forgetful functor is a functor over the big fppf site.

theorem forgetPolarization_obj_base (X : PolarizedFamily B) :
    (cartesianProperFlatProjection B integerBase B.contains_integerBase).obj
      ((forgetPolarization B).obj X) = (schemeOverIntegers B).obj X.base

AlgebraicGeometry.forgetPolarization_map_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesForget.lean, line 313. The attribute's comment: “the forgetful functor is over the site”.

Stacks 0D3Y. Forgetting the polarization keeps the morphism of base schemes.

theorem forgetPolarization_map_base {X Y : PolarizedFamily B} (f : X ⟶ Y) :
    (cartesianProperFlatProjection B integerBase B.contains_integerBase).map
      ((forgetPolarization B).map f) = (schemeOverIntegers B).map f.baseMap
Tag 0D3Z, a lemma

Tag 0D3Z in the Stacks Project.

AlgebraicGeometry.polarizedSpacesForget_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesFiberedForget.lean, line 122. The attribute's comment: “fibred in groupoids over the stack of finitely presented, flat and proper families”.

Stacks 0D3Z. Polarized families are fibred in groupoids over the finitely presented, flat and proper families of algebraic spaces of Stacks 0D1E.

Condition (a) of Stacks 003S is base change of the polarized family along the base scheme of the given family of algebraic spaces, and condition (b) holds because the base morphism the fill-in must lie over is forced by the two comparison isomorphisms, so the fill-in is the one AlgebraicGeometry.polarizedProjection_uniqueLift provides over the site.

theorem polarizedSpacesForget_isFiberedInGroupoids :
    (polarizedSpacesForget B).IsFiberedInGroupoids

AlgebraicGeometry.toPolarizedSpaces_comp_polarizedSpacesForget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesFiberedForget.lean, line 149. The attribute's comment: “identification of the replacement category with the polarized families”.

Stacks 0D3Z. The comparison equivalence carries the projection of AlgebraicGeometry.PolarizedSpaces to the family of algebraic spaces back to the forgetful functor of Stacks 0D3Y, so AlgebraicGeometry.polarizedSpacesForget_isFiberedInGroupoids is the assertion of the tag for AlgebraicGeometry.forgetPolarization.

theorem toPolarizedSpaces_comp_polarizedSpacesForget :
    toPolarizedSpaces B ⋙ polarizedSpacesForget B = forgetPolarization B

AlgebraicGeometry.polarizedProjection_isFiberedInGroupoids_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedStackUnconditional.lean, line 59. The attribute's comment: “fibred in groupoids over the fppf site of schemes”.

Stacks 003S for polarized families, with no hypothesis. Polarized families of Stacks 0D1M form a category fibred in groupoids over the big fppf site.

This is also Stacks 0D3Z over the big fppf site of schemes: condition (a) of Stacks 003S is AlgebraicGeometry.polarizedProjection_existsLift, by base change, and condition (b) is AlgebraicGeometry.polarizedProjection_uniqueLift.

theorem polarizedProjection_isFiberedInGroupoids_unconditional {B : BigFppfSite.{u}} :
    (polarizedProjection B).IsFiberedInGroupoids
Tag 0D40, a lemma

Tag 0D40 in the Stacks Project.

AlgebraicGeometry.polarized_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedStackRepresentable.lean, line 872.

Stacks 0D40. The category 𝒫olarized of polarized families is a stack in groupoids over Spaces'_{fp, flat, proper}, endowed with the topology inherited from the big fppf site (Stacks 06NV), and it is a stack in groupoids over the big fppf site of schemes.

theorem polarized_isStackInGroupoids :
    (polarizedSpacesForget B).IsStackInGroupoids.{w}
        ((polarizedFamiliesProperFlatProjection B).inheritedTopology B.topology) ∧
      (polarizedProjection B).IsStackInGroupoids.{w} B.topology
Tag 0E94, a lemma

Tag 0E94 in the Stacks Project.

AlgebraicGeometry.PolarizedOverSpace.polarizedBaseChange_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedOverSpaceEquivalence.lean, line 68. The attribute's comment: “base change is an equivalence of the polarized proper flat finitely presented spaces over T with Mor_{Cat/Sch_fppf}(S_T, Polarized)”.

Let T be an algebraic space over Spec(ℤ) and 𝒮_T its algebraic stack. Base change is an equivalence from the category of pairs (X ⟶ T, L), where X ⟶ T is a proper, flat and finitely presented morphism of algebraic spaces and L is an invertible module ample on X/T, to the category of functors over the site from 𝒮_T to Polarized (Mor_{Cat/Sch_fppf}(𝒮_T, Polarized)).

theorem polarizedBaseChange_isEquivalence : (polarizedBaseChange B T).IsEquivalence
Tag 0D1N, a remark

Tag 0D1N in the Stacks Project.

AlgebraicGeometry.PolarizedFamilyOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesOverSpace.lean, line 81. The attribute's comment: “objects”.

Stacks 0D1N. A polarized family over the space A: a polarized family together with a structure morphism of its base scheme over the base of the site and a point of A there.

structure PolarizedFamilyOver

AlgebraicGeometry.PolarizedFamilyOver.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesOverSpace.lean, line 102. The attribute's comment: “morphisms”.

Stacks 0D1N. A morphism of polarized families over A: a morphism of the underlying polarized families whose base map lies over the base of the site and carries the point of the target to the point of the source.

structure Hom (X Y : PolarizedFamilyOver B S hS A)

AlgebraicGeometry.PolarizedFamilyOver.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesOverSpace.lean, line 135. The attribute's comment: “category”.

Stacks 0D1N. Polarized families over A and the morphisms compatible with their points form a category, with the identities and composition of the underlying polarized families.

instance instCategory : Category.{u} (PolarizedFamilyOver B S hS A)

AlgebraicGeometry.PolarizedFamilyOver.isEquivalence_toCategoricalPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFamiliesOverSpace.lean, line 293. The attribute's comment: “the 2-fibre product square”.

Stacks 0D1N. The canonical comparison from polarized families over A to the 2-fibre product of polarized families and schemes carrying a point of A, over the big fppf site of schemes, is an equivalence: the displayed square is a 2-fibre product square.

theorem isEquivalence_toCategoricalPullback :
    (toCategoricalPullback B S hS A).IsEquivalence
Tag 0D41, a lemma

Tag 0D41 in the Stacks Project.

AlgebraicGeometry.isAlgebraicMorphism_forgetPolarizationOneMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedForgetAlgebraicMorphism.lean, line 65.

Stacks 0D41. The forgetful functor of Stacks 0D3Y, (X ⟶ S, ℒ) ↦ (X ⟶ S), defines a 1-morphism Polarized ⟶ Spaces'_{fp, flat, proper} of stacks in groupoids over the big fppf site of Spec ℤ (Stacks 0D40, 0D1G) which is algebraic in the sense of Stacks 06CF: its 2-fibre product with every scheme-valued point of Spaces'_{fp, flat, proper} is an algebraic stack.

theorem isAlgebraicMorphism_forgetPolarizationOneMorphism :
    Stack.IsAlgebraicMorphism.{u, w, w, w} B integerBase B.contains_integerBase
      (𝒳 := polarizedStackInGroupoids.{w} B (polarizedProjection_isStack B))
      (𝒴 := properFlatSpacesStackInGroupoids.{w} B integerBase B.contains_integerBase)
      (forgetPolarizationBased B)
Tag 0D42, a lemma

Tag 0D42 in the Stacks Project.

AlgebraicGeometry.hasRepresentableDiagonal_polarizedStackUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedDiagonal.lean, line 64.

The diagonal 𝒫olarized ⟶ 𝒫olarized × 𝒫olarized of the stack of polarized proper flat families of finite presentation, over the big fppf site of a terminal base scheme, is representable by algebraic spaces.

theorem hasRepresentableDiagonal_polarizedStackUnconditional :
    Stack.HasRepresentableDiagonal B S hS (polarizedStackUnconditional B hS hT)
Tag 0D43, a lemma

Tag 0D43 in the Stacks Project.

AlgebraicGeometry.isLimitPreservingPolarizedUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedLimitPreservingProof.lean, line 79. The attribute's comment: “at a small index category”.

Stacks 0D43. The stack in groupoids 𝒫olarized of polarized proper schemes is limit preserving in the sense of Stacks 07XL: for every cofiltered inverse system of affine schemes over the terminal base whose limit of underlying schemes is T, the canonical comparison colim 𝒫olarized_{Tᵢ} ⥤ 𝒫olarized_T is an equivalence of categories. The index category is taken in the scheme universe, which is the smallness the source's directed sets have.

theorem isLimitPreservingPolarizedUnconditional (B : BigFppfSite.{u}) {S : Scheme.{u}}
    (hS : B.Contains S) (hT : IsTerminal (B.obj hS)) :
    IsLimitPreservingPolarizedUnconditional.{u, u, u} B hS hT
Tag 0D44, a lemma

Tag 0D44 in the Stacks Project.

AlgebraicGeometry.polarizedPushoutRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedPushout.lean, line 350. The attribute's comment: “the functor of the comparison on fibre categories; that it is an equivalence is not proved here, Stacks 07RX being absent”.

Stacks 0D44. For a commutative square f ≫ h = i ≫ g of schemes of the big fppf site, the comparison functor from the polarized families with base S' to the 2-fibre product of those with base S and those with base T' over those with base T.

def polarizedPushoutRestriction {T T' S S' : B.Schemes} (i : T ⟶ T') (f : T ⟶ S) (g : T' ⟶ S')
    (h : S ⟶ S') (hsq : f ≫ h = i ≫ g) :
    (polarizedProjection B).Fiber S' ⥤
      (polarizedFiberPullback B f) ⊡ (polarizedFiberPullback B i)

AlgebraicGeometry.isEquivalence_polarizedPushoutRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedPushoutEquivalence.lean, line 284. The attribute's comment: “the comparison functor polarizedPushoutRestriction of a pushout square of schemes with T ⟶ T' a thickening and T ⟶ S affine is an equivalence”.

Stacks 0D44. Let

T  --i-->  T'
|          |
f          g
|          |
v          v
S  --h-->  S'

be a pushout in the category of schemes, of schemes of the big fppf site, where T ⟶ T' is a thickening and T ⟶ S is affine. Then the functor on fibre categories of the stack of polarized schemes

𝒫olarized_{S'} ⟶ 𝒫olarized_S ×_{𝒫olarized_T} 𝒫olarized_{T'}

is an equivalence. (The source states the lemma "in Situation 08KB"; that situation fixes data which the statement does not use.)

theorem isEquivalence_polarizedPushoutRestriction {T T' S S' : B.Schemes} (i : T ⟶ T')
    (f : T ⟶ S) (g : T' ⟶ S') (h : S ⟶ S') (hsq : f ≫ h = i ≫ g)
    (hpush : IsPushout (B.inclusion.map f) (B.inclusion.map i) (B.inclusion.map h)
      (B.inclusion.map g))
    (hi : IsThickening (B.inclusion.map i)) [IsAffineHom (B.inclusion.map f)] :
    (polarizedPushoutRestriction B i f g h hsq).IsEquivalence
Tag 0D4S, a lemma

Tag 0D4S in the Stacks Project.

AlgebraicGeometry.PolarizedDeformation.finiteDimensional_tangentFunctor_infinitesimalAutomorphismFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedDeformationFiniteDimensional.lean, line 64. The attribute's comment: “(2): for a polarized proper scheme x over any field k, the functors T_x and Inf_x of Stacks 07Y9 exist (𝒫olarized satisfies RS* by 0D44) and T_x(k) and Inf_x(k) are finite dimensional; both finiteness statements hold for every k-linear functor carrying the identifications of 07Y9”.

Stacks Project, Tag 0D4S, part (2). Let k be a field and let x = (X → Spec k, ℒ) be an object of 𝒫olarized over Spec k. Then the tangent functor T_x and the functor of infinitesimal automorphisms Inf_x of Stacks 07Y9 exist, and T_x(k) and Inf_x(k) are finite-dimensional k-vector spaces.

Each functor is stated as a structure (TangentFunctorData, InfinitesimalAutomorphismFunctorData) carrying a k-linear functor on the site modules together with its identification with the isomorphism classes of lifts of x, respectively with the infinitesimal automorphisms of the trivial lifts of x, natural in the module. The statement gives that such a functor exists and that the value at k of every such functor is finite-dimensional. No condition on k is assumed.

theorem finiteDimensional_tangentFunctor_infinitesimalAutomorphismFunctor {k : Type u} [Field k]
    (toS : Spec (.of k) ⟶ S) (hk : B.Contains (Spec (.of k))) (x : PolarizedFamily B)
    (hx : (polarizedSliceProjection B hS hT).obj x = algebraOver k B S hS toS hk) :
    (Nonempty (TangentFunctorData k B S hS toS hk (polarizedSliceProjection B hS hT) x hx) ∧
      ∀ T : TangentFunctorData k B S hS toS hk (polarizedSliceProjection B hS hT) x hx,
        FiniteDimensional k (T.functor.obj ((fgSiteModule B hk).obj (FGModuleCat.of k k)))) ∧
    (Nonempty (InfinitesimalAutomorphismFunctorData k B S hS toS hk
        (polarizedSliceProjection B hS hT) x hx
        (isFiberedInGroupoids_polarizedSliceProjection B hS hT)) ∧
      ∀ I : InfinitesimalAutomorphismFunctorData k B S hS toS hk
          (polarizedSliceProjection B hS hT) x hx
          (isFiberedInGroupoids_polarizedSliceProjection B hS hT),
        FiniteDimensional k (I.functor.obj ((fgSiteModule B hk).obj (FGModuleCat.of k k))))

AlgebraicGeometry.PolarizedDeformation.isFiniteDimensionalDeformationCategory_predeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedDeformationFiniteDimensional.lean, line 98. The attribute's comment: “(1): for a field k of finite type over the base and a polarized proper scheme x over k, the deformation category F_{X,k,x} has finite dimensional tangent space T F_{X,k,x} and finite dimensional Inf(F_{X,k,x}); the base is any terminal scheme of the site, e.g. Spec Z”.

Stacks Project, Tag 0D4S, part (1). Let k be a field of finite type over the base (for the base Spec ℤ: of finite type over ℤ), presented through Spec k ⟶ Spec Λ ⟶ S, and let x = (X → Spec k, ℒ) be an object of 𝒫olarized over Spec k. Then the predeformation category 𝓕_{𝒳,k,x} of Stacks 07T2 is a deformation category whose tangent space T𝓕_{𝒳,k,x} and whose infinitesimal automorphisms Inf(𝓕_{𝒳,k,x}) (Stacks 07WY) are finite-dimensional k-vector spaces.

The base is any scheme S which is terminal in the big fppf site; no condition is put on Λ beyond the factorization.

theorem isFiniteDimensionalDeformationCategory_predeformationCategory
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] (iΛ : Spec (.of Λ) ⟶ S)
    (x : PolarizedFamily B)
    (hx₀ : (polarizedSliceProjection B hS hT ⋙ Over.post B.inclusion).obj x =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    IsFiniteDimensionalDeformationCategory
      (predeformationCategory iΛ (polarizedSliceProjection B hS hT ⋙ Over.post B.inclusion) x
        hx₀).projection
Tag 0D4T, a lemma

Tag 0D4T in the Stacks Project.

Stacks.PolarizedAlgebraization.exists_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PolarizedAlgebraization/StrongFormalEffectiveness.lean, line 115. References: SGA 7 IX (7.1.3), “partial”.

Strong formal effectiveness for polarized schemes. Let (R_n) be an inverse system of rings with surjective transition maps whose kernels are locally nilpotent, and R = lim R_n. Let X_n ⟶ Spec R_n be schemes with cartesian squares over the transitions Spec R_n ⟶ Spec R_{n + 1}, ℒ_n invertible 𝒪_{X_n}-modules and φ_n : i_n^* ℒ_{n + 1} ≅ ℒ_n. If every X_n ⟶ Spec R_n is proper, flat and of finite presentation, and ℒ_0 is ample, then there are a proper, flat, finitely presented X ⟶ Spec R, an ample invertible ℒ on X, identifications X_n ≅ X ×_{Spec R} Spec R_n (cartesian squares through j_n : X_n ⟶ X) and isomorphisms e_n : ℒ|_{X_n} ≅ ℒ_n, compatible with the i_n and the φ_n. The index n : ℕ stands for the source's n + 1.

theorem exists_algebraization (R : ℕᵒᵖ ⥤ CommRingCat.{u})
    (hsurj : ∀ n : ℕ, Function.Surjective (R.map (homOfLE (Nat.le_succ n)).op).hom)
    (hnil : ∀ n : ℕ,
      RingHom.ker (R.map (homOfLE (Nat.le_succ n)).op).hom ≤ nilradical (R.obj (op (n + 1))))
    (X : ℕ → Scheme.{u}) (f : ∀ n : ℕ, X n ⟶ Spec (R.obj (op n)))
    (i : ∀ n : ℕ, X n ⟶ X (n + 1))
    (hpb : ∀ n : ℕ,
      IsPullback (i n) (f n) (f (n + 1)) (Spec.map (R.map (homOfLE (Nat.le_succ n)).op)))
    (L : ∀ n : ℕ, (X n).Modules) [hL : ∀ n : ℕ, IsInvertibleModule (X n) (L n)]
    (φ : ∀ n : ℕ, (Scheme.Modules.pullback (i n)).obj (L (n + 1)) ≅ L n)
    [hproper : ∀ n : ℕ, IsProper (f n)] [hflat : ∀ n : ℕ, Flat (f n)]
    (hfp : ∀ n : ℕ, _root_.AlgebraicGeometry.FinitePresentation (f n))
    (hample : IsAmple (X 0) (L 0)) :
    ∃ (Y : Scheme.{u}) (g : Y ⟶ Spec (limit R)) (ℒ : Y.Modules) (_ : IsInvertibleModule Y ℒ)
      (j : ∀ n : ℕ, X n ⟶ Y) (hj : ∀ n : ℕ, i n ≫ j (n + 1) = j n)
      (e : ∀ n : ℕ, (Scheme.Modules.pullback (j n)).obj ℒ ⟶ L n),
      IsProper g ∧ Flat g ∧ _root_.AlgebraicGeometry.FinitePresentation g ∧ IsAmple Y ℒ ∧
      (∀ n : ℕ, IsPullback (j n) (f n) g (Spec.map (limit.π R (op n)))) ∧
      (∀ n : ℕ, IsIso (e n)) ∧
      ∀ n : ℕ, (Scheme.Modules.pullbackComp (i n) (j (n + 1))).hom.app ℒ ≫
          (Scheme.Modules.pullbackCongr (hj n)).hom.app ℒ ≫ e n =
        (Scheme.Modules.pullback (i n)).map (e (n + 1)) ≫ (φ n).hom
Tag 0D4U, a lemma

Tag 0D4U in the Stacks Project.

AlgebraicGeometry.polarizedFormalObject_isEffective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedFormalEffective.lean, line 474.

Stacks 0D4U. Consider the stack 𝒫olarized over the base scheme Spec ℤ. Then every formal object (Stacks 07X4) is effective (Stacks 07X7): it is, up to isomorphism, the system of restrictions to the infinitesimal thickenings Spec(R / 𝔪^{n+1}) of a polarized family over its complete local base Spec R.

theorem polarizedFormalObject_isEffective (B : BigFppfSite.{u})
    (hZ : B.Contains (Spec (CommRingCat.of (ULift.{u} ℤ))))
    (ξ : FormalObject B _ hZ (polarizedSliceProjection B hZ (isTerminal_obj_specULiftZ B hZ))) :
    FormalObject.IsEffective B _ hZ (polarizedSliceProjection B hZ (isTerminal_obj_specULiftZ B hZ))
      (polarizedProjection_isFiberedInGroupoids_unconditional.sliceAtTerminal
        (isTerminal_obj_specULiftZ B hZ)) ξ
Tag 0D4V, a lemma

Tag 0D4V in the Stacks Project.

AlgebraicGeometry.hasOpenVersality_polarizedStackUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedVersality/PolarizedOpennessOfVersality.lean, line 55. The attribute's comment: “openness of versality for 𝒫olarized over Spec(ℤ)”.

The stack in groupoids 𝒫olarized of polarized proper flat families of finite presentation (Stacks 0D1M), over the big fppf site of Spec(ℤ), satisfies openness of versality: if an object over a scheme U locally of finite type over Spec(ℤ) is versal at a finite type point u₀, it is versal at every finite type point of an open neighbourhood of u₀.

theorem hasOpenVersality_polarizedStackUnconditional (B : BigFppfSite.{u})
    (hZ : B.Contains (Spec (CommRingCat.of (ULift.{u} ℤ)))) :
    HasOpenVersality
      ((polarizedStackUnconditional B hZ (isTerminal_obj_specULiftZ B hZ)).val.p ⋙
        Over.post B.inclusion)

AlgebraicGeometry.hasOpenVersality_polarizedOverNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedVersality/PolarizedOpennessOfVersality.lean, line 72. The attribute's comment: “openness of versality for S-𝒫olarized over a Noetherian base scheme S”.

For a Noetherian scheme S, the stack S-𝒫olarized of Remark 0D1N — polarized proper flat families of finite presentation together with a morphism of their base to S — over the big fppf site of S satisfies openness of versality: if an object over a scheme U locally of finite type over S is versal at a finite type point u₀, it is versal at every finite type point of an open neighbourhood of u₀.

theorem hasOpenVersality_polarizedOverNoetherian (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) [IsNoetherian S] :
    HasOpenVersality
      ((PolarizedVersality.PolarizedOver.stack B S hS).val.p ⋙ Over.post B.inclusion)
Tag 0D4X, a theorem

Tag 0D4X in the Stacks Project.

AlgebraicGeometry.isAlgebraicStack_polarizedStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedAlgebraicStack.lean, line 94.

Stacks 0D4X. The stack 𝒫olarized of polarized proper schemes (Situation 0D1M) over the big fppf site of Spec ℤ is an algebraic stack. In fact, for every algebraic space A over Spec ℤ, the stack A-Polarized of Remark 0D1N, of polarized proper schemes (X ⟶ S, ℒ) together with a morphism S ⟶ A, is an algebraic stack.

theorem isAlgebraicStack_polarizedStack :
    Stack.IsAlgebraicStack.{u, w} B integerBase B.contains_integerBase
        (polarizedStackUnconditional B B.contains_integerBase
          (isTerminal_obj_specULiftZ B B.contains_integerBase)).val ∧
      ∀ (A : (BigFppfOver B integerBase B.contains_integerBase)ᵒᵖ ⥤ Type u),
        IsAlgebraicSpace B integerBase B.contains_integerBase A →
        Stack.IsAlgebraicStack.{u, w} B integerBase B.contains_integerBase
          (BasedCategory.ofFunctor
            (AlgebraicGeometry.PolarizedFamilyOver.projection B integerBase
              B.contains_integerBase A))
Sources
LeanAlgebraicGeometry.PolarizedFamily · AlgebraicGeometry.PolarizedFamily.Hom · AlgebraicGeometry.PolarizedFamily.instCategory · AlgebraicGeometry.polarizedProjection · AlgebraicGeometry.forgetPolarization · AlgebraicGeometry.forgetPolarization_obj_base · AlgebraicGeometry.forgetPolarization_map_base · AlgebraicGeometry.polarizedSpacesForget_isFiberedInGroupoids

Section99.15 The stack of curves#

Section 99.15 of the Stacks Project, Tag 0D4Y. 14 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0D4Z, a situation

Tag 0D4Z in the Stacks Project.

AlgebraicGeometry.CurveFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilies.lean, line 83. The attribute's comment: “objects”.

A family of curves: a morphism from an algebraic space to a scheme of the big fppf site which is flat, proper, of finite presentation and of relative dimension at most one.

structure CurveFamily

AlgebraicGeometry.CurveFamily.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilies.lean, line 109. The attribute's comment: “morphisms”.

A morphism of families of curves: a morphism of total spaces over a morphism of base schemes whose square is cartesian.

structure Hom (X Y : CurveFamily B hZ)

An instance with no name in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilies.lean, line 135. The attribute's comment: “category”.

Families of curves and cartesian squares between them form a category, with componentwise identities and composition.

instance : Category (CurveFamily B hZ)

AlgebraicGeometry.curvesProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilies.lean, line 153. The attribute's comment: “projection”.

The forgetful functor taking a family of curves to its base scheme, which makes the category of families of curves a category over the big fppf site.

def curvesProjection : CurveFamily B hZ ⥤ B.Schemes
Tag 0D50, an equation

Tag 0D50 in the Stacks Project.

AlgebraicGeometry.curvesToCartesianProperFlat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesFibered.lean, line 403. The attribute's comment: “the inclusion”.

Stacks equation 0D50. The inclusion of the category of families of curves into the category of finitely presented, flat and proper families of algebraic spaces over varying base schemes, forgetting the bound on the relative dimension of the structure morphism: on objects it is AlgebraicGeometry.CurveFamily.toCartesianProperFlat and on morphisms it keeps the morphism of total spaces and the morphism of base schemes, the cartesian square of a morphism of families of curves being exactly the strongly cartesian condition on the larger side.

The equation displays only this inclusion. That the two sides are categories fibred in groupoids over the big fppf site and that the inclusion is one of categories over that site is the ambient Situation 99.15.1 of the source, realised here by AlgebraicGeometry.curvesProjection_isFiberedInGroupoids, AlgebraicGeometry.cartesianProperFlatProjection_isFiberedInGroupoids and AlgebraicGeometry.curvesToCartesianProperFlat_comp_cartesianProperFlatProjection; that the inclusion is one of a full subcategory is AlgebraicGeometry.curvesToCartesianProperFlat_full together with AlgebraicGeometry.curvesToCartesianProperFlat_faithful.

def curvesToCartesianProperFlat :
    CurveFamily B hZ ⥤ CartesianProperFlatSpaces B integerBase hZ
Tag 0D51, a lemma

Tag 0D51 in the Stacks Project.

AlgebraicGeometry.curvesProjection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesFibered.lean, line 182.

Stacks 0D51. The category of families of curves is fibred in groupoids over the big fppf site of schemes.

theorem curvesProjection_isFiberedInGroupoids :
    (curvesProjection B hZ).IsFiberedInGroupoids
Tag 0D52, a lemma

Tag 0D52 in the Stacks Project.

AlgebraicGeometry.curvesProjection_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesStack.lean, line 262.

Stacks 0D52. The category of families of curves is a stack in groupoids over the big fppf site of schemes, for covering families indexed in every universe.

It is a stack (AlgebraicGeometry.curvesProjection_isStack) whose projection is fibred in groupoids (Stacks 0D51, AlgebraicGeometry.curvesProjection_isFiberedInGroupoids), and such a stack is a stack in groupoids by the implication (3) ⟹ (1) of Stacks 02ZJ.

theorem curvesProjection_isStackInGroupoids :
    (curvesProjection B hZ).IsStackInGroupoids.{w} B.topology
Tag 0D53, a lemma

Tag 0D53 in the Stacks Project.

Declarations registered for the tag:

Tag 0D54, a remark

Tag 0D54 in the Stacks Project.

AlgebraicGeometry.CurveFamilyOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesOverSpace.lean, line 95. The attribute's comment: “the category of families of curves over a base algebraic space”.

Stacks 0D54. The category of families of curves over a fixed algebraic space A: an object is a family of curves together with a morphism from its base scheme to A, and a morphism is a morphism of families of curves commuting with those morphisms.

abbrev CurveFamilyOver (A : AlgebraicSpaces B integerBase hZ)

AlgebraicGeometry.CurveFamilyOver.isEquivalence_toTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesOverSpace.lean, line 179. The attribute's comment: “the base-change square”.

Stacks 0D54. The absolute and the relative categories of curves form a 2-fibre product square over the big fppf site of schemes: the canonical comparison from families of curves over A to the 2-fibre product of families of curves with the schemes over A is an equivalence.

theorem isEquivalence_toTwoFibreProduct (A : AlgebraicSpaces B integerBase hZ) :
    (toTwoFibreProduct B hZ A).IsEquivalence
Tag 0D55, a lemma

Tag 0D55 in the Stacks Project.

AlgebraicGeometry.isLimitPreserving_curvesFiberedCategory_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLimitPreservingUnconditional.lean, line 51. The attribute's comment: “at a small index category”.

Stacks 0D55. The stack of families of curves over the big fppf site of Spec(ℤ) is limit preserving in the sense of Artin's Axioms, Definition 07XL: for every inverse system of affine schemes of the site whose limit of underlying schemes is T, the canonical comparison colim Curves_{Tᵢ} ⥤ Curves_T is an equivalence of categories. The index category is taken in the universe of the schemes.

theorem isLimitPreserving_curvesFiberedCategory_unconditional :
    Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u + 1} B integerBase hZ
      (curvesFiberedCategory B hZ)
Tag 0D56, a lemma

Tag 0D56 in the Stacks Project.

AlgebraicGeometry.curvePushoutEquivalenceOfIsPushout, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ProperPushoutGluingUnconditional.lean, line 58.

[Stacks Project, Tag 0D56]. For a pushout S' = S ⨿_T T' of schemes along a thickening i : T ⟶ T' and an affine morphism f : T ⟶ S, the canonical restriction functor from the families of curves over S' to the compatible pairs of families over S and T' is an equivalence.

def curvePushoutEquivalenceOfIsPushout {T T' S S' : B.Schemes}
    (i : T ⟶ T') (f : T ⟶ S) (g : T' ⟶ S') (h : S ⟶ S')
    (hi : Stacks.Thickenings.IsThickening (B.inclusion.map i))
    [IsAffineHom (B.inclusion.map f)]
    (hsq : IsPushout (B.inclusion.map i) (B.inclusion.map f)
      (B.inclusion.map g) (B.inclusion.map h)) :
    CurvePushoutEquivalenceData B hZ i f g h
Tag 0D57, a lemma

Tag 0D57 in the Stacks Project.

AlgebraicGeometry.CurveDeformation.finiteDimensional_predeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveDeformationsFiniteDimensional.lean, line 68. The attribute's comment: “(1): for a family of curves x over any field k and any Λ with Spec k → Spec Λ, the predeformation category F_{X,k,x} is a deformation category whose tangent space T F and infinitesimal automorphisms Inf(F) are finite dimensional; k need not be of finite type over Z”.

Stacks Project, Tag 0D57, part (1). Let k be a field and let x = (X → Spec k) be a family of curves over Spec k, lying over Spec k → Spec Λ → Spec ℤ. Then the predeformation category 𝓕_{𝒳,k,x} over 𝒞_Λ is a deformation category, its tangent space T𝓕_{𝒳,k,x} is a finite-dimensional k-vector space, and so are its infinitesimal automorphisms Inf(𝓕_{𝒳,k,x}), the kernel of Aut_{k[ε]}(x'₀) → Aut_k(x₀), at every object of the special fibre and for every choice of its pushforwards.

This generalizes the source: k need not be of finite type over ℤ, and Λ is any ring with a Λ-algebra structure on k and any morphism Spec Λ ⟶ Spec ℤ. The proof identifies 𝓕_{𝒳,k,x} with the deformation category of the scheme X (the total space of a curve over a field is a scheme, Stacks 0ADD) and applies the finiteness of Stacks 0DYA for that category, in place of the source's appeal to Stacks 0D1K.

theorem finiteDimensional_predeformation :
    letI := (predeformation x hx).category
    ∃ hD : IsDeformationCategory.{u, u, u} (predeformation x hx).projection,
      (letI : Fact (IsPredeformationCategory
          (BasedCategory.ofFunctor (predeformation x hx).projection).p) := ⟨hD.predeformation⟩;
        letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
          (isomorphismClasses (BasedCategory.ofFunctor (predeformation x hx).projection)
            hD.predeformation.cofibered))) := ⟨tangentConditionS2.{u, u, u} hD⟩;
        FiniteDimensional k (artinianTangentSpace Λ k
          (isomorphismClasses (BasedCategory.ofFunctor (predeformation x hx).projection)
            hD.predeformation.cofibered))) ∧
      ∀ y, (predeformation x hx).projection.obj y = residueFieldObject.{u, u, u} Λ k →
        ∀ PF : ChosenPushforwardsAt (predeformation x hx).projection y,
          FiniteDimensional k ↥((infinitesimalAutomorphismLinearLift.{u, u, u} PF
            hD.satisfiesRS).functor.obj (FGModuleCat.of k (ULift.{u} k)))

AlgebraicGeometry.finiteDimensional_curves_tangentFunctor_infinitesimalAutomorphismFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveTangentFunctor.lean, line 68. The attribute's comment: “(2): for a family of curves x over a field k, the tangent functor T_x and the functor Inf_x of Stacks 07Y9 exist, and T_x(k) and Inf_x(k) are finite dimensional; both are stated for every k-linear functor carrying the identifications of 07Y9”.

Let k be a field and let x = (X → Spec k) be a family of curves over Spec k. Then the tangent functor T_x and the functor of infinitesimal automorphisms Inf_x of Stacks 07Y9 exist, and T_x(k) and Inf_x(k) are finite-dimensional k-vector spaces.

Each functor is stated as a structure (TangentFunctorData, InfinitesimalAutomorphismFunctorData) carrying a k-linear functor on the site modules together with its identification with the isomorphism classes of lifts of x, respectively with the infinitesimal automorphisms of the trivial lifts of x, natural in the module. The statement gives that such a functor exists and that the value at k of every such functor is finite-dimensional, so it holds for the functors T_x and Inf_x of Stacks 07Y9, which are determined by these identifications. No condition on k is assumed.

theorem finiteDimensional_curves_tangentFunctor_infinitesimalAutomorphismFunctor {k : Type u}
    [Field k] {toS : Spec (.of k) ⟶ integerBase} {hk : B.Contains (Spec (.of k))}
    (x : CurveFamily B hZ)
    (hx : (curvesProjectionOver B hZ).obj x = algebraOver k B integerBase hZ toS hk) :
    (Nonempty (TangentFunctorData k B integerBase hZ toS hk (curvesProjectionOver B hZ) x hx) ∧
      ∀ T : TangentFunctorData k B integerBase hZ toS hk (curvesProjectionOver B hZ) x hx,
        FiniteDimensional k (T.functor.obj ((fgSiteModule B hk).obj (FGModuleCat.of k k)))) ∧
    (Nonempty (InfinitesimalAutomorphismFunctorData k B integerBase hZ toS hk
        (curvesProjectionOver B hZ) x hx
        CurveDeformation.curvesProjectionOver_isFiberedInGroupoids) ∧
      ∀ I : InfinitesimalAutomorphismFunctorData k B integerBase hZ toS hk
          (curvesProjectionOver B hZ) x hx
          CurveDeformation.curvesProjectionOver_isFiberedInGroupoids,
        FiniteDimensional k (I.functor.obj ((fgSiteModule B hk).obj (FGModuleCat.of k k))))
Tag 0D58, a lemma

Tag 0D58 in the Stacks Project.

AlgebraicGeometry.curvesFormalObject_isEffective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesFormalEffectiveUnconditional.lean, line 54.

Every formal object of the stack Curves of families of curves over Spec(ℤ) is effective: it comes, up to isomorphism of formal objects, from a family of curves over the spectrum of its Noetherian complete local base.

theorem curvesFormalObject_isEffective (B : BigFppfSite.{u}) (hZ : B.Contains integerBase)
    (ξ : Deformation.Artin.FormalObject B integerBase hZ (curvesProjectionOver B hZ)) :
    Deformation.Artin.FormalObject.IsEffective B integerBase hZ (curvesProjectionOver B hZ)
      (Functor.IsFiberedInGroupoids.of_comp_over (B.obj hZ) (curvesProjection B hZ)
        (curvesProjectionOver B hZ) (by rfl) (curvesProjection_isFiberedInGroupoids B hZ)) ξ
Tag 0D59, a lemma

Tag 0D59 in the Stacks Project.

Declarations registered for the tag:

Tag 0D5A, a theorem

Tag 0D5A in the Stacks Project.

AlgebraicGeometry.isAlgebraicStack_curvesStack_and_curveFamilyOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesAlgebraicStackUnconditional.lean, line 47.

The stack Curves (Situation 0D4Z) is algebraic. In fact, for every algebraic space A the stack A-Curves of families of curves over A (Remark 0D54) is algebraic.

theorem isAlgebraicStack_curvesStack_and_curveFamilyOver :
    Stack.IsAlgebraicStack.{u, u + 1, u + 1, u + 1} B integerBase hZ
        (curvesFiberedCategory B hZ).val ∧
      ∀ A : AlgebraicSpaces B integerBase hZ,
        Stack.IsAlgebraicStack.{u, u + 1} B integerBase hZ (curveFamilyOverBased B hZ A)
Tag 0D5B, a lemma

Tag 0D5B in the Stacks Project.

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_curvesToCartesianProperFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesFibered.lean, line 1153. The attribute's comment: “representability by algebraic spaces”.

Stacks 0D5B. The 1-morphism from the category of families of curves to the category of finitely presented, flat and proper families of algebraic spaces of Stacks equation 0D50 is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_curvesToCartesianProperFlat :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
      (curvesToCartesianProperFlatHom B hZ).hom

AlgebraicGeometry.isOpenImmersion_curvesToCartesianProperFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesFibered.lean, line 1194. The attribute's comment: “open immersions”.

Stacks 0D5B. The 1-morphism from the category of families of curves to the category of finitely presented, flat and proper families of algebraic spaces of Stacks equation 0D50 is an open immersion: every algebraic space representing one of its base changes has open immersion structural morphism.

theorem isOpenImmersion_curvesToCartesianProperFlat :
    Stack.IsOpenImmersion B integerBase hZ (curvesToCartesianProperFlatHom B hZ)

AlgebraicGeometry.isClosedImmersion_curvesToCartesianProperFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesFibered.lean, line 1205. The attribute's comment: “closed immersions”.

Stacks 0D5B. The 1-morphism from the category of families of curves to the category of finitely presented, flat and proper families of algebraic spaces of Stacks equation 0D50 is a closed immersion: every algebraic space representing one of its base changes has closed immersion structural morphism.

theorem isClosedImmersion_curvesToCartesianProperFlat :
    Stack.IsClosedImmersion B integerBase hZ (curvesToCartesianProperFlatHom B hZ)
Tag 0D5C, a remark

Tag 0D5C in the Stacks Project.

AlgebraicGeometry.polarizedCurvesToCurves_isAlgebraic_smooth_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/C1783/PolarizedCurvesRemark.lean, line 176.

Stacks 0D5C. Let PolarizedCurves = 𝒞urves ×_{𝒮paces'_{fp, flat, proper}} 𝒫olarized (AlgebraicGeometry.polarizedCurvesUnconditional), over the big fppf site of Spec ℤ.

  1. PolarizedCurves parametrizes polarized curves: its first projection is an equivalence onto the category of polarized families of relative dimension at most one, i.e. of families of curves endowed with a relatively ample invertible sheaf.
  2. PolarizedCurves is an open and closed substack of the algebraic stack 𝒫olarized: 𝒫olarized is an algebraic stack, the projection PolarizedCurves ⟶ 𝒫olarized is representable by algebraic spaces, an open immersion and a closed immersion, and PolarizedCurves is an algebraic stack.
  3. PolarizedCurves ⟶ 𝒞urves is a base change of the arrow 𝒫olarized ⟶ 𝒮paces'_{fp,flat,proper} of Stacks 0D41: its base change along every scheme point z of 𝒞urves is equivalent over the site to the base change of the forgetful 1-morphism of Stacks 0D41 along the image of z in 𝒮paces'_{fp, flat, proper}.
  4. PolarizedCurves ⟶ 𝒞urves is algebraic (Stacks 06CF): its base change along every scheme point of 𝒞urves is an algebraic stack.
  5. PolarizedCurves ⟶ 𝒞urves is smooth: each of these base changes is smooth over the scheme (Stacks 075U).
  6. PolarizedCurves ⟶ 𝒞urves is surjective: every point of 𝒞urves is in the image (surjectivity on objects, Stacks 06D4), and the 1-morphism of algebraic stacks is surjective on points (Stacks 04ZS).
  7. Another approach to the algebraicity of 𝒞urves: 𝒞urves is an algebraic stack, as the target of the smooth, surjective, algebraic 1-morphism PolarizedCurves ⟶ 𝒞urves from the algebraic stack PolarizedCurves.

Clauses 4–6 are stated for the hom-shrunk models AlgebraicGeometry.polarizedCurvesSmall and AlgebraicGeometry.curvesSmall, equivalent over the site to PolarizedCurves and 𝒞urves, with the projection AlgebraicGeometry.polarizedCurvesSmallToCurvesSmall; surjectivity on objects in clause 6 is also stated for PolarizedCurves itself.

theorem polarizedCurvesToCurves_isAlgebraic_smooth_surjective :
    -- (1) PolarizedCurves parametrizes polarized curves
    (polarizedCurvesToIsPolarizedCurve B hZ).IsEquivalence ∧
    -- (2) PolarizedCurves is an open and closed substack of the algebraic stack `𝒫olarized`
    (Stack.IsAlgebraicStack.{u, w} B integerBase hZ (polarizedFiberedCategory B hZ
        (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B)).val ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (polarizedCurvesToPolarizedUnconditional B hZ).hom ∧
      Stack.IsOpenImmersion B integerBase hZ (polarizedCurvesToPolarizedUnconditional B hZ) ∧
      Stack.IsClosedImmersion B integerBase hZ (polarizedCurvesToPolarizedUnconditional B hZ) ∧
      Stack.IsAlgebraicStack.{u, w} B integerBase hZ (polarizedCurvesUnconditional B hZ).val) ∧
    -- (3) `PolarizedCurves ⟶ 𝒞urves` is a base change of the arrow of Stacks 0D41
    (∀ (Z : BigFppfOver B integerBase hZ)
      (z : BigFppfOver B Z.left.1 Z.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj),
      z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map Z.hom →
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.structureFunctor (Over.map Z.hom)
          (polarizedProjection B ⋙ schemeOverIntegers B)
          (cartesianProperFlatProjection B integerBase hZ)
          (z ⋙ curvesToCartesianProperFlat B hZ) (forgetPolarization B))
        (TwoFibreProductOver.structureFunctor (Over.map Z.hom)
          (polarizedCurvesUnconditional B hZ).val.p (curvesFiberedCategory B hZ).val.p z
          (CatFiberedInGroupoids.homFunctor (polarizedCurvesSquare B hZ
            (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B)).snd)))) ∧
    -- (4) `PolarizedCurves ⟶ 𝒞urves` is algebraic
    (∀ (Z : BigFppfOver B integerBase hZ)
      (z : BigFppfOver B Z.left.1 Z.left.2 ⥤ (curvesSmall B hZ).val.obj)
      (hz : z ⋙ (curvesSmall B hZ).val.p = Over.map Z.hom),
      Stack.IsAlgebraicStack.{u, w} B integerBase hZ
        (CatFiberedInGroupoids.twoFibreProductSquare.{u, u, u + 1, u + 1}
          (Stack.schemeSliceMap B integerBase hZ Z z hz)
          (polarizedCurvesSmallToCurvesSmall B hZ
            (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B))).pt.val) ∧
    -- (5) `PolarizedCurves ⟶ 𝒞urves` is smooth
    (∀ (Z : BigFppfOver B integerBase hZ)
      (z : BigFppfOver B Z.left.1 Z.left.2 ⥤ (curvesSmall B hZ).val.obj)
      (hz : z ⋙ (curvesSmall B hZ).val.p = Over.map Z.hom),
      Stack.HasPropertyOnSomeSmoothDiagram B integerBase hZ
        (fun _ _ h => Space.IsSmooth B integerBase hZ h)
        (CatFiberedInGroupoids.twoFibreProductSquare.{u, u, u + 1, u + 1}
          (Stack.schemeSliceMap B integerBase hZ Z z hz)
          (polarizedCurvesSmallToCurvesSmall B hZ
            (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B))).fst) ∧
    -- (6) `PolarizedCurves ⟶ 𝒞urves` is surjective
    (Stack.IsSurjectiveOnObjects B integerBase hZ
        (polarizedCurvesUnconditional B hZ).val.p (curvesFiberedCategory B hZ).val.p
        (CatFiberedInGroupoids.homFunctor (polarizedCurvesSquare B hZ
          (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B)).snd) ∧
      Stack.IsSurjectiveOnObjects B integerBase hZ
        (polarizedCurvesSmall B hZ
          (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B)).val.p
        (curvesSmall B hZ).val.p
        (CatFiberedInGroupoids.homFunctor (polarizedCurvesSmallToCurvesSmall B hZ
          (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B))) ∧
      ∃ (hX : Stack.IsAlgebraicStack.{u, w} B integerBase hZ
          (polarizedCurvesUnconditional B hZ).val)
        (hY : Stack.IsAlgebraicStack.{u, w} B integerBase hZ (curvesFiberedCategory B hZ).val),
        Stack.IsSurjective B integerBase hZ (polarizedCurvesToCurvesAlgebraic B hZ
          (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B) hX hY)) ∧
    -- (7) `𝒞urves` is an algebraic stack
    Stack.IsAlgebraicStack.{u, w} B integerBase hZ (curvesFiberedCategory B hZ).val
Sources
LeanAlgebraicGeometry.CurveFamily · AlgebraicGeometry.CurveFamily.Hom · AlgebraicGeometry.curvesProjection · AlgebraicGeometry.curvesToCartesianProperFlat · AlgebraicGeometry.curvesProjection_isFiberedInGroupoids · AlgebraicGeometry.curvesProjection_isStackInGroupoids · AlgebraicGeometry.C1590Private.hasRepresentableDiagonal_curvesFiberedCategory · AlgebraicGeometry.CurveFamilyOver

Section99.16 Moduli of complexes on a proper morphism#

Section 99.16 of the Stacks Project, Tag 0DLB. 12 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DLC, a lemma

Tag 0DLC in the Stacks Project.

AlgebraicGeometry.Space.exists_negativeExtLocus_and_vanishing_and_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDerivedHomDualProved.lean, line 222.

Stacks 0DLC. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is proper, flat and of finite presentation, and let K, E ∈ D(𝒪_X) with K pseudo-coherent and E Y-perfect (Stacks 0DKN). For a point y : Spec(k) ⟶ Y with values in a field write K_y, E_y for the pullbacks to the fibre X_y. 1. There is an open W ⊆ Y characterized by: y ∈ |W| if and only if Ext^i_{𝒪_{X_y}}(K_y, E_y) = 0 for i < 0 (AlgebraicGeometry.Space.IsNegativeExtLocus). 2. For such a W and every algebraic space V over Y whose morphism to Y factors through W, Ext^i_{𝒪_{X_V}}(K_V, E_V) = 0 for i < 0, where X_V is the base change of X and K_V, E_V are the derived pullbacks of K and E to X_V. 3. For such a W, the functor V ↦ Hom_{𝒪_{X_V}}(K_V, E_V) on the schemes over W is representable by an algebraic space affine and of finite presentation over W (in particular it is a sheaf).

theorem exists_negativeExtLocus_and_vanishing_and_representable
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hproper : IsProper B S hS f.hom)
    (hflat : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (K E : derivedModules B S hS X) (hK : (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent K)
    (hE : IsPerfectRelativeToCanonical B S hS f hflat hfp.1 E) :
    (∃ W : OpenSubspaces B S hS Y.1, IsNegativeExtLocus f K E W) ∧
      (∀ W : OpenSubspaces B S hS Y.1, IsNegativeExtLocus f K E W →
        ∀ V : Over Y, (∃ g : V.left ⟶ openSubspaceAsSpace B S hS W,
            g ≫ openSubspaceImmersion B S hS W = V.hom) →
        ∀ i : ℤ, i < 0 →
          Subsingleton (((smallEtaleDerivedPullbackData B S hS).pull (overProjection f V)).obj K ⟶
            (((smallEtaleDerivedPullbackData B S hS).pull (overProjection f V)).obj E)⟦i⟧)) ∧
      (∀ W : OpenSubspaces B S hS Y.1, IsNegativeExtLocus f K E W →
        IsAffineFinitePresentationAlgebraicSpaceOver (openSubspaceAsSpace B S hS W)
          (relativeDerivedHomOverOpen f K E W))
Tag 0DLD, a lemma

Tag 0DLD in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.conditions_negativeSelfExt_selfHom_overBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDerivedHomDualProved.lean, line 257.

Stacks 0DLD. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is proper, flat and of finite presentation, and let E ∈ D(𝒪_X). Assume that E is Y-perfect (Stacks 0DKN) and that Ext^i_{𝒪_{X_y}}(E_y, E_y) = 0 for i < 0 at every point y : Spec(k) ⟶ Y with values in a field, E_y the derived pullback to the fibre X_y. Then * (a) both conditions hold for X_V ⟶ V and E_V after every base change V ⟶ Y; * (b) Ext^i_{𝒪_{X_V}}(E_V, E_V) = 0 for i < 0 and every algebraic space V over Y; * (c) V ↦ Hom_{𝒪_{X_V}}(E_V, E_V) is representable by an algebraic space affine and of finite presentation over Y. Here X_V is the base change of X and E_V the derived pullback of E to X_V.

theorem conditions_negativeSelfExt_selfHom_overBaseChange (E : derivedModules B S hS D.X)
    (h1 : IsPerfectRelativeToCanonical B S hS D.f D.flat D.finitePresentation.1 E)
    (h2 : HasNoNegativeFieldFibreExt D.f E) :
    (∀ V : Over D.Y,
      IsPerfectRelativeToCanonical B S hS (overInclusion D.f V) (D.overInclusion_isFlat V)
          (D.overInclusion_isLocallyOfFinitePresentation V)
          (((smallEtaleDerivedPullbackData B S hS).pull (overProjection D.f V)).obj E) ∧
        HasNoNegativeFieldFibreExt (overInclusion D.f V)
          (((smallEtaleDerivedPullbackData B S hS).pull (overProjection D.f V)).obj E)) ∧
      (∀ (V : Over D.Y) (i : ℤ), i < 0 →
        Subsingleton
          (((smallEtaleDerivedPullbackData B S hS).pull (overProjection D.f V)).obj E ⟶
            (((smallEtaleDerivedPullbackData B S hS).pull (overProjection D.f V)).obj E)⟦i⟧)) ∧
      IsAffineFinitePresentationAlgebraicSpaceOver D.Y (relativeDerivedHom D.f E E)
Tag 0DLE, a situation

Tag 0DLE in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 318. The attribute's comment: “the standing situation: a proper, flat, finitely presented morphism of algebraic spaces”.

Stacks 0DLE, the standing data. A morphism f : X ⟶ Y of algebraic spaces over S which is proper, flat and of finite presentation: the relative algebraic space whose relatively perfect complexes the category Complexes_{X/Y} classifies.

It is the standing datum AlgebraicGeometry.Space.CoherentSituation of Stacks 08KB, which assumes only finite presentation, together with the two further hypotheses of Stacks 0DLE.

structure ComplexesSituation (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    extends CoherentSituation B S hS

AlgebraicGeometry.Space.ComplexesObject, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 522. The attribute's comment: “objects”.

Stacks 0DLE, the objects. An object of Complexes_{X/Y}: a scheme T of the site over Y together with an object of D(𝒪_{X_T}) satisfying conditions (1) and (2) of Stacks 0DLD.

structure ComplexesObject (D : ComplexesSituation B S hS)

AlgebraicGeometry.Space.ComplexesHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 536. The attribute's comment: “morphisms”.

Stacks 0DLE, the morphisms. A morphism of Complexes_{X/Y}: a morphism h : T ⟶ T' of test schemes over Y together with an isomorphism L(X_h)^*E' ⟶ E of D(𝒪_{X_T}).

structure ComplexesHom {D : ComplexesSituation B S hS} (A A' : ComplexesObject D)

AlgebraicGeometry.Space.ComplexesSituation.complexesCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 684. The attribute's comment: “the category structure on the objects: the hom-sets are the pairs (h, φ), with the identity and the composition the tag designates”.

The category Complexes_{X/Y} of Stacks 0DLE. The category structure on the objects whose hom-sets are AlgebraicGeometry.Space.ComplexesHom, whose identity is AlgebraicGeometry.Space.ComplexesHom.id and whose composition is AlgebraicGeometry.Space.ComplexesHom.comp.

def complexesCategory : Category.{u + 1} (ComplexesObject D)

AlgebraicGeometry.Space.ComplexesSituation.complexesProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 695. The attribute's comment: “the functor (T, g, E) ↦ (T, g) to the test schemes over the base”.

The projection of Complexes_{X/Y} to the test schemes over Y of Stacks 0DLE, (T, g, E) ↦ (T, g): it forgets the complex and keeps the base map of a morphism.

def complexesProjection :
    letI : Category.{u + 1} (ComplexesObject D) := complexesCategory D
    ComplexesObject D ⥤ SchemesOver D.Y

AlgebraicGeometry.Space.ComplexesSituation.complexesFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 734. The attribute's comment: “the functor p : Complexes_{X/B} ⥤ (Sch/S)_fppf, (T, g, E) ↦ T”.

The functor p : Complexes_{X/Y} ⥤ (Sch/S)_fppf of Stacks 0DLE, (T, g, E) ↦ T: the projection to the test schemes over Y followed by forgetting the morphism to Y.

def complexesFunctor :
    letI : Category.{u + 1} (ComplexesObject D) := complexesCategory D
    ComplexesObject D ⥤ BigFppfOver B S hS

AlgebraicGeometry.Space.ComplexesSituation.isGroupoid_fiber_complexesFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 802. The attribute's comment: “the fibre categories of p over the schemes T are groupoids”.

The fibre categories of p : Complexes_{X/Y} ⥤ (Sch/S)_fppf are groupoids, as Stacks 0DLE asserts.

theorem isGroupoid_fiber_complexesFunctor (T : BigFppfOver B S hS) :
    IsGroupoid ((complexesFunctor D).Fiber T)

AlgebraicGeometry.Space.ComplexesSituation.complexesCategory_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStack.lean, line 838. The attribute's comment: “the whole statement: the category Complexes_{X/B} of the triples (T, g, E) and the pairs (h, φ), with the designated identity and composition, the functor p : (T, g, E) ↦ T to (Sch/S)_fppf, and its fibre categories being groupoids”.

Stacks 0DLE in full. Complexes_{X/Y} is a category whose objects are the triples (T, g, E) of AlgebraicGeometry.Space.ComplexesObject — a scheme T over S, a morphism g : T ⟶ Y and an object E of D(𝒪_{X_T}) satisfying conditions (1) and (2) of Stacks 0DLD — and whose morphisms are the pairs (h, φ) of AlgebraicGeometry.Space.ComplexesHom, with the identity and the composition the tag designates; the rule (T, g, E) ↦ T is a functor p to (Sch/S)_fppf, and its fibre categories are groupoids.

The conjuncts are: the hom-sets, the identity, the composition, the two clauses saying that p is the designated rule, and that the fibre categories of p are groupoids. That the objects and the morphisms are the designated data is the definition of AlgebraicGeometry.Space.ComplexesObject and AlgebraicGeometry.Space.ComplexesHom, and that the category laws hold is AlgebraicGeometry.Space.ComplexesSituation.complexesCategory, whose existence is asserted by the statement being about it.

theorem complexesCategory_spec :
    letI : Category.{u + 1} (ComplexesObject D) := complexesCategory D
    (∀ A A' : ComplexesObject D, (A ⟶ A') = ComplexesHom A A') ∧
      (∀ A : ComplexesObject D, (𝟙 A : ComplexesHom A A) = ComplexesHom.id A) ∧
      (∀ {A A' A'' : ComplexesObject D} (m : ComplexesHom A A') (n : ComplexesHom A' A''),
        ((m ≫ n : A ⟶ A'') : ComplexesHom A A'') = ComplexesHom.comp m n) ∧
      (∀ A : ComplexesObject D, (complexesFunctor D).obj A = A.T.left) ∧
      (∀ {A A' : ComplexesObject D} (m : ComplexesHom A A'),
        (complexesFunctor D).map (m : A ⟶ A') = m.base.left) ∧
      ∀ T : BigFppfOver B S hS, IsGroupoid ((complexesFunctor D).Fiber T)
Tag 0DLF, a lemma

Tag 0DLF in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.complexesFunctor_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackBaseChange.lean, line 264. The attribute's comment: “the functor p : Complexes_{X/B} ⥤ (Sch/S)_fppf, (T, g, E) ↦ T, is fibred in groupoids”.

Stacks 0DLF. In Situation 0DLE the functor p : Complexes_{X/B} ⥤ (Sch/S)_fppf, (T, g, E) ↦ T, is fibred in groupoids: every morphism h : T ⟶ T' of schemes over S lifts at every object (T', g', E'), to (T, g' ∘ h, L(h')^*E') ⟶ (T', g', E') with the identity as comparison of complexes, and fill-ins exist and are unique.

The lift is an object because both conditions of Stacks 0DLD survive pullback (AlgebraicGeometry.Space.ComplexesSituation.relativelyPerfectBaseChange and AlgebraicGeometry.Space.ComplexesSituation.hasNoNegativeFibreExt_pull); the fill-in is AlgebraicGeometry.Space.ComplexesSituation.fillIn.

theorem complexesFunctor_isFiberedInGroupoids :
    letI : Category.{u + 1} (ComplexesObject D) := complexesCategory D
    (complexesFunctor D).IsFiberedInGroupoids
Tag 0DLG, a lemma

Tag 0DLG in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.complexes_hasRepresentableDiagonal_proved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackProved.lean, line 64.

Stacks 0DLG. In Situation 0DLE (f : X ⟶ Y proper, flat and of finite presentation), the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 of 𝒳 = Complexes_{X/Y} is representable by algebraic spaces: AlgebraicGeometry.Space.ComplexesSituation.complexes_hasRepresentableDiagonal with Stacks 0DLC, parts (1) and (3), discharged.

theorem complexes_hasRepresentableDiagonal_proved :
    Stack.HasRepresentableDiagonal B S hS
      (CatFiberedInGroupoids.mk (complexesBasedCategory D)
        (complexesFunctor_isFiberedInGroupoids D))
Tag 0DLH, a lemma

Tag 0DLH in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.complexesFunctor_isStackInGroupoids_proved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackCechDescentProved.lean, line 74.

In a Complexes situation D over S, the category Complexes_{X/Y} fibred in groupoids over (Sch/S)_fppf is a stack in groupoids.

theorem complexesFunctor_isStackInGroupoids_proved {S : Scheme.{u}} {hS : B.Contains S}
    (D : ComplexesSituation B S hS) :
    (complexesFunctor D).IsStackInGroupoids.{u + 1} (BigFppfOver.topology B S hS)
Tag 0DLI, a remark

Tag 0DLI in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.complexesToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackBaseChangeSquare.lean, line 176. The attribute's comment: “the 1-morphism Complexes_{X/B} → 𝒮_B, (T, g, E) ↦ (T, g)”.

The projection to the base. The rule (T, g, E) ↦ (T, g) which forgets the complex is a 1-morphism Complexes_{X/B} ⟶ 𝒮_B of categories over the big fppf site of S.

def complexesToBase (D : ComplexesSituation B S hS) :
    complexesBasedCategory D ⥤ᵇ baseBasedCategory D.Y

AlgebraicGeometry.Space.ComplexesSituation.baseChangeSquare_isTwoFibreProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackBaseChangeSquare.lean, line 630. The attribute's comment: “the square Complexes_{X'/B'} → Complexes_{X/B} over 𝒮_{B'} → 𝒮_B is a 2-fibre product”.

**The square

Complexes_{X'/B'} ⟶ Complexes_{X/B}, 𝒮_{B'} ⟶ 𝒮_B

is a 2-fibre product.** That is, Complexes_{X'/B'}, with the base-change functor and the projection which forgets the complex, is a 2-fibre product of the projection Complexes_{X/B} ⟶ 𝒮_B with the morphism 𝒮_{B'} ⟶ 𝒮_B induced by g : B' ⟶ B.

def baseChangeSquare_isTwoFibreProduct (g : Y' ⟶ D.Y) :
    Bicategory.IsTwoFibreProduct (D.baseChangeSquare g)
Tag 0DLJ, a lemma

Tag 0DLJ in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.isLimitPreserving_complexes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackProved.lean, line 88.

Stacks 0DLJ. In Situation 0DLE assume that Y ⟶ S is locally of finite presentation. Then p : Complexes_{X/Y} ⥤ (Sch/S)_fppf is limit preserving (Stacks 07XL): AlgebraicGeometry.Space.ComplexesSituation.isLimitPreserving_of_existsNegativeExtLocus with Stacks 0DKW and Stacks 0DLC (1) discharged.

theorem isLimitPreserving_complexes
    (hY : IsLocallyOfFinitePresentation B S hS (terminal.from D.Y.1)) :
    Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u + 1} B S hS
      (CatFiberedInGroupoids.mk (complexesBasedCategory D)
        (complexesFunctor_isFiberedInGroupoids D))
Tag 0DLK, a lemma

Tag 0DLK in the Stacks Project.

Declarations registered for the tag:

Tag 0DLL, a lemma

Tag 0DLL in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.finiteDimensional_tangentSpace_infinitesimalAutomorphisms_complexes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackTangentFiniteDimensional.lean, line 88.

In Situation 0DLE (f : X ⟶ Y proper, flat and of finite presentation, the B of the source being Y), assume that S is locally Noetherian and Y ⟶ S is locally of finite presentation. Let k be a field of finite type over S, presented as in Stacks Section 07T2 through an affine open Spec Λ ⊆ S with Λ → k finite, and let x₀ be an object of 𝒳 = Complexes_{X/Y} over Spec k. Then 𝒳 satisfies (RS), so that the predeformation category 𝓕_{𝒳,k,x₀} is a deformation category and the spaces of Stacks Section 07WY are defined, and the tangent space T𝓕_{𝒳,k,x₀} (Deformation.Artin.tangentSpaceModuleOfSatisfiesRS) and the infinitesimal automorphisms Inf(𝓕_{𝒳,k,x₀}) (Deformation.Artin.infinitesimalAutomorphismModuleOfSatisfiesRS, at every object over k and every choice of pushforwards) are finite dimensional over k.

theorem finiteDimensional_tangentSpace_infinitesimalAutomorphisms_complexes
    (D : ComplexesSituation B S hS) [_root_.AlgebraicGeometry.IsLocallyNoetherian S]
    (hY : IsLocallyOfFinitePresentation B S hS (terminal.from D.Y.obj))
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : ComplexesObject D)
    (hx₀ : (complexesFunctor D ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    SatisfiesRS B S hS (complexesFunctor D) (complexesFunctor_isFiberedInGroupoids D) ∧
      ∀ hRS : SatisfiesRS B S hS (complexesFunctor D) (complexesFunctor_isFiberedInGroupoids D),
        FiniteDimensional k (tangentSpaceModuleOfSatisfiesRS B S hS (complexesFunctor D)
            (complexesFunctor_isFiberedInGroupoids D) hRS iΛ x₀ hx₀
            (locallyOfFiniteType_specMap_comp_of_isOpenImmersion iΛ hiΛ)
            (quasiCompact_of_spec_field _)) ∧
          ∀ x P, FiniteDimensional k (infinitesimalAutomorphismModuleOfSatisfiesRS B S hS
            (complexesFunctor D) (complexesFunctor_isFiberedInGroupoids D) hRS iΛ x₀ hx₀
            (locallyOfFiniteType_specMap_comp_of_isOpenImmersion iΛ hiΛ)
            (quasiCompact_of_spec_field _) x P)
Tag 0DLM, a lemma

Tag 0DLM in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.isStronglyFormallyEffective_complexes_proved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackFormalEffectivenessProved.lean, line 51.

Complexes_{X/S} is strongly formally effective: in a ComplexesSituation whose target Y of f : X ⟶ Y is terminal over S, with S locally Noetherian, the functor p : Complexes_{X/S} ⟶ (Sch/S)_fppf is strongly formally effective.

theorem isStronglyFormallyEffective_complexes_proved {S : Scheme.{u}} {hS : B.Contains S}
    (D : ComplexesSituation B S hS) [_root_.AlgebraicGeometry.IsLocallyNoetherian S]
    (hY : IsTerminal D.Y) :
    IsStronglyFormallyEffective B S hS (complexesFunctor D)
      (complexesFunctor_isFiberedInGroupoids D)
Tag 0DLN, a theorem

Tag 0DLN in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.isAlgebraicStack_complexes_proved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackAlgebraicStackProved.lean, line 112.

Stacks 0DLN: Complexes_{X/Y} is an algebraic stack. In Situation 0DLE over S (f : X ⟶ Y proper, flat and of finite presentation), Complexes_{X/Y} is an algebraic stack over S.

This is ComplexesSituation.isAlgebraicStack_complexes_of_cechDescent_of_derivedExistence with Stacks 0DLA, Čech case, given by AlgebraicGeometry.Space.ComplexesSituation.cechDescent_proved and Stacks 0DIQ given by AlgebraicGeometry.Space.ComplexesSituation.SpecLimitTower.exists_restriction_proved.

theorem isAlgebraicStack_complexes_proved {S : Scheme.{u}} (hS : B.Contains S)
    (D : ComplexesSituation B S hS) :
    Stack.IsAlgebraicStack.{u, z, u + 1, u + 1} B S hS (complexesBasedCategory D)
Sources
LeanAlgebraicGeometry.Space.exists_negativeExtLocus_and_vanishing_and_representable · AlgebraicGeometry.Space.ComplexesSituation.conditions_negativeSelfExt_selfHom_overBaseChange · AlgebraicGeometry.Space.ComplexesSituation · AlgebraicGeometry.Space.ComplexesObject · AlgebraicGeometry.Space.ComplexesHom · AlgebraicGeometry.Space.ComplexesSituation.complexesCategory · AlgebraicGeometry.Space.ComplexesSituation.complexesProjection · AlgebraicGeometry.Space.ComplexesSituation.complexesFunctor

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.