57.16 No deformations to 57.18 Countability of derived…

Section57.16 No deformations#

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

Tag 0G0N, a lemma

Tag 0G0N in the Stacks Project.

AlgebraicGeometry.derivedIso_koszulOfLift, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/NoDeformations/LiftedKoszul.lean, line 420. The attribute's comment: “lifted_koszul”.

The chosen finite-free lift of the closed-fibre Koszul complex represents the Koszul complex of its lifted first differential.

public lemma derivedIso_koszulOfLift
    (S : FlatLocalKoszulDeformationSituation.{u}) :
    letI : CommRing S.A := S.commRingA
    let I := Ideal.map (algebraMap S.R S.A) (IsLocalRing.maximalIdeal S.R)
    ∀ (P : CochainComplex (ModuleCat.{u} S.A) ℤ)
      (f : Fin S.r → S.A),
      Nonempty (DerivedCategory.Q.obj P ≅ S.K) →
      Nonempty
        (((ModuleCat.extendScalars (Ideal.Quotient.mk I)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj P ≅
          (Koszul.seqComplex S.residueSequence).extend ComplexShape.embeddingDownNat) →
      (∀ n : ℕ,
        Nonempty (P.X (-(n : ℤ)) ≅
          ModuleCat.of S.A (Fin (S.r.choose n) → S.A))) →
      (∀ i : ℤ, 0 < i → IsZero (P.X i)) →
      (∃ (e₀ : P.X 0 ≅ ModuleCat.of S.A S.A)
        (e₁ : P.X (-1) ≅ ModuleCat.of S.A (Fin S.r → S.A)),
        (∀ i, f i = e₀.hom.hom ((P.d (-1) 0).hom
          (e₁.inv.hom (Pi.single i 1)))) ∧
        (∀ i, Ideal.Quotient.mk I (f i) = S.residueSequence i)) →
      Nonempty
        (S.K ≅ DerivedCategory.Q.obj
          ((Koszul.seqComplex f).extend ComplexShape.embeddingDownNat))

AlgebraicGeometry.exists_koszulDescription_and_flat_quotient_of_fibrewise_koszul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/NoDeformations/LiftedKoszulExistence.lean, line 120. The attribute's comment: “The hypotheses are packaged as FlatLocalKoszulDeformationSituation. The Koszul complex is Mathlib's exterior-algebra complex Koszul.seqComplex, placed in cohomological degrees by ComplexShape.embeddingDownNat, and K is identified with its image under DerivedCategory.Q. The ideal (f₁, …, f_r) is Ideal.span (Set.range f) and "regular sequence" is Mathlib's RingTheory.Sequence.IsRegular, which is Definition 00LF verbatim.”.

The lifted sequence of [Stacks, Tag 0G0N] is regular with flat quotient. In a flat local deformation situation R → A whose closed fibre is Koszul on the regular sequence f̄, there is a sequence f in A reducing to f̄ modulo 𝔪_R A which is regular in A, whose quotient A/(f) is flat over R, and whose Koszul complex represents the deformed perfect complex K in D(A).

public theorem exists_koszulDescription_and_flat_quotient_of_fibrewise_koszul
    (S : FlatLocalKoszulDeformationSituation.{u}) :
    letI : CommRing S.A := S.commRingA
    let I := Ideal.map (algebraMap S.R S.A) (IsLocalRing.maximalIdeal S.R)
    ∃ f : Fin S.r → S.A,
      (∀ i, Ideal.Quotient.mk I (f i) = S.residueSequence i) ∧
        RingTheory.Sequence.IsRegular S.A (List.ofFn f) ∧
          Module.Flat S.R (S.A ⧸ Ideal.span (Set.range f)) ∧
            Nonempty (S.K ≅ DerivedCategory.Q.obj
              ((Koszul.seqComplex f).extend ComplexShape.embeddingDownNat))

Declarations registered for the tag:

Tag 0G0P, a lemma

Tag 0G0P in the Stacks Project.

StacksDraft.Perfect.exists_away_koszul_description, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/KoszulSpreadingOut.lean, line 404.

Stacks Project, Tag 0G0P. A local Koszul presentation of a perfect complex, with flat quotient, spreads to some principal neighbourhood of the prime.

theorem exists_away_koszul_description {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [Algebra.FiniteType R S] [Module.Flat R S]
    (q : Ideal S) [q.IsPrime]
    (K : DerivedCategory (ModuleCat.{u} S)) (hK : StacksDraft.Perfect.IsPerfect K)
    {r : ℕ} (f : Fin r → Localization.AtPrime q)
    (hf : RingTheory.Sequence.IsRegular (Localization.AtPrime q) (List.ofFn f))
    (hflat : Module.Flat R (Localization.AtPrime q ⧸ Ideal.span (Set.range f)))
    (hiso : Nonempty
      ((derivedExtensionScalarsGeneral.{u, u, u}
          (algebraMap S (Localization.AtPrime q))).functor.obj K ≅
        DerivedCategory.Q.obj
          ((Koszul.seqComplex f).extend ComplexShape.embeddingDownNat))) :
    ∃ (g : S) (hg : g ∉ q) (f' : Fin r → Localization.Away g),
      (∀ i, localizationAwayToAtPrime g q hg (f' i) = f i) ∧
      RingTheory.Sequence.IsRegular (Localization.Away g) (List.ofFn f') ∧
      Module.Flat R (Localization.Away g ⧸ Ideal.span (Set.range f')) ∧
      Nonempty
        ((derivedExtensionScalarsGeneral.{u, u, u}
            (algebraMap S (Localization.Away g))).functor.obj K ≅
          DerivedCategory.Q.obj
            ((Koszul.seqComplex f').extend ComplexShape.embeddingDownNat))
Tag 0G0Q, a lemma

Tag 0G0Q in the Stacks Project.

AlgebraicGeometry.exists_isIso_baseChange_of_isIso_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/IsomorphismOnFibre.lean, line 450. References: EGA III (4.6.7), “(ii)”.

Stacks Project, Tag 0G0Q. Let X and Y be proper over a Noetherian scheme S, with X flat over S. An S-morphism X ⟶ Y which is an isomorphism on the fibre at s is an isomorphism after base change to some open neighbourhood of s.

public theorem exists_isIso_baseChange_of_isIso_fiber
    {S : Scheme.{u}} [IsNoetherian S] {X Y : Over S} (p : X ⟶ Y)
    [IsProper X.hom] [IsProper Y.hom] [Flat X.hom] (s : S)
    [IsIso ((Over.pullback (S.fromSpecResidueField s)).map p).left] :
    ∃ U : S.Opens, s ∈ U ∧ IsIso ((Over.pullback U.ι).map p).left
Tag 0G0R, a lemma

Tag 0G0R in the Stacks Project.

AlgebraicGeometry.exists_opens_nonempty_iso_constantFamily_of_isRelativeEquivalenceKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/NoDeformations/Rigidity.lean, line 288.

[Stacks, Tag 0G0R]. Let k be a field, q : S ⟶ Spec k of finite type, s a k-rational point of S (a section of q), and g : Y ⟶ S smooth and proper. Let X = Y_s ×_k S be the constant family with fibre Y_s = Y ×_S Spec k. If K is the Fourier-Mukai kernel of a relative equivalence from X to Y over S whose derived restriction along the comparison morphism i : Y_s ×_k Y_s ⟶ X ×_S Y is the diagonal kernel Δ_{Y_s/k,*}𝒪_{Y_s}, then there is an open U ⊆ S containing the point s picks out with Y|_U isomorphic to Y_s ×_k U over U.

theorem exists_opens_nonempty_iso_constantFamily_of_isRelativeEquivalenceKernel
    (rational : s ≫ q = 𝟙 _)
    (K : DerivedCategory (Limits.pullback (constantFamilyπ q g s) g).Modules)
    (relEquiv : IsRelativeEquivalenceKernel (constantFamilyπ q g s) g K)
    (restrict : Nonempty ((derivedPullback
        (fibreSquareToProductComparison q g s rational).toLRSHom.toShHom).obj K ≅
      diagonalKernel (fibreAtRationalPointπ g s))) :
    ∃ U : S.Opens, Set.range s.base ⊆ (U : Set S) ∧
      Nonempty ((Over.pullback U.ι).obj (Over.mk g) ≅
        Over.mk (Limits.pullback.snd (fibreAtRationalPointπ g s) (U.ι ≫ q)))
Tag 0G0S, a lemma

Tag 0G0S in the Stacks Project.

AlgebraicGeometry.exists_opens_iso_constantFamily_of_isRelativeEquivalenceKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/NoDeformations/LocalTriviality.lean, line 242.

[Stacks, Tag 0G0S]. Let k be algebraically closed, X ⟶ Spec k smooth and proper, g : Y ⟶ S smooth and proper with S of finite type over k, and K the Fourier-Mukai kernel of a relative equivalence from X ×_k S to Y over S. Then every point of S has an open neighbourhood U over which Y is the constant family Y₀ ×_k U of some smooth proper Y₀ over k.

At each k-rational point s this is exists_opens_iso_constantFamily_of_rationalPoint with Y₀ = Y_s, smooth and proper as a base change of g; the opens so obtained cover S by AlgebraicGeometry.exists_mem_opens_of_rationalPoints (S is Jacobson and its closed points are k-rational).

theorem exists_opens_iso_constantFamily_of_isRelativeEquivalenceKernel [IsAlgClosed k]
    (K : DerivedCategory (pullback (pullback.snd a q) g).Modules)
    (hK : IsRelativeEquivalenceKernel (pullback.snd a q) g K) :
    ∀ x : S, ∃ U : S.Opens, x ∈ U ∧ ∃ Y₀ : Over (Spec (.of k)),
      Smooth Y₀.hom ∧ IsProper Y₀.hom ∧
        Nonempty ((Over.pullback U.ι).obj (Over.mk g) ≅ (Over.pullback (U.ι ≫ q)).obj Y₀)
Sources
LeanAlgebraicGeometry.derivedIso_koszulOfLift · AlgebraicGeometry.exists_koszulDescription_and_flat_quotient_of_fibrewise_koszul · Module.Flat.isRegular_and_flat_quotient_ofList_smul_of_isRegular_maximalIdeal · StacksDraft.Perfect.exists_away_koszul_description · AlgebraicGeometry.exists_isIso_baseChange_of_isIso_fiber · AlgebraicGeometry.exists_opens_nonempty_iso_constantFamily_of_isRelativeEquivalenceKernel · AlgebraicGeometry.exists_opens_iso_constantFamily_of_isRelativeEquivalenceKernel

Section57.17 Countability#

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

Tag 0G0U, a lemma

Tag 0G0U in the Stacks Project.

AlgebraicGeometry.countable_hom_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/Countability/FiniteTypeSchemes.lean, line 143. The attribute's comment: “countable_hom”.

Over a countable Noetherian ring, the morphisms over the base between two schemes of finite type form a countable type.

public theorem countable_hom_of_finiteType
    {R : Type u} [CommRing R] [Countable R] [IsNoetherianRing R]
    (X Y : Over (Spec (.of R)))
    [LocallyOfFiniteType X.hom] [QuasiCompact X.hom]
    [LocallyOfFiniteType Y.hom] [QuasiCompact Y.hom] :
    Countable (X ⟶ Y)

AlgebraicGeometry.countable_isomorphismClasses_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/Countability/IsomorphismClasses.lean, line 536. The attribute's comment: “countable_iso_classes”.

There are countably many isomorphism classes of schemes of finite type over a countable Noetherian ring.

public theorem countable_isomorphismClasses_of_finiteType
    (R : Type u) [CommRing R] [Countable R] [IsNoetherianRing R] :
    Countable
      (Quotient (isIsomorphicSetoid
        (ObjectProperty.FullSubcategory (fun X : Over (Spec (.of R)) =>
          LocallyOfFiniteType X.hom ∧ QuasiCompact X.hom))))
Tag 0G0V, a lemma

Tag 0G0V in the Stacks Project.

AlgebraicGeometry.boundedDerivedCategory_essentiallyCountable, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/Countability/BoundedDerivedCategory.lean, line 453.

The bounded derived category of an essentially countable abelian category is essentially countable.

public instance boundedDerivedCategory_essentiallyCountable
    (A : Type u) [Category.{v} A] [Abelian A] [EssentiallyCountableCategory A] :
    EssentiallyCountableCategory (DerivedCategory.Bounded A)
Tag 0G0W, a lemma

Tag 0G0W in the Stacks Project.

AlgebraicGeometry.essentiallyCountable_perfect_and_boundedCoherent_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/Countability/PerfectDerivedCategory.lean, line 209. The attribute's comment: “D_perf(O_X) and D^b_Coh(O_X) are countable categories”.

Stacks Project, Tag 0G0W. Let X be a scheme of finite type over a countable Noetherian ring R. Then the categories D_perf(𝒪_X) and D^b_Coh(𝒪_X) are countable: each has countably many morphisms between any two objects and countably many isomorphism classes of objects, which is CategoryTheory.EssentiallyCountableCategory, the notion of countability of [Stacks, Section 0G0T]. Both are read as full subcategories of D(𝒪_X), at any model of the derived category.

As in the source: X is Noetherian, D_perf(𝒪_X) is a full subcategory of D^b_Coh(𝒪_X) ([Stacks, Tag 0FXU]), D^b_Coh(𝒪_X) = D^b(Coh(𝒪_X)) ([Stacks, Tag 0FDB]), and the bounded derived category of the countable abelian category Coh(𝒪_X) (AlgebraicGeometry.essentiallyCountable_coherentModules_of_finiteType) is countable ([Stacks, Tag 0G0V]).

public theorem essentiallyCountable_perfect_and_boundedCoherent_of_finiteType {R : Type u}
    [CommRing R] [Countable R] [IsNoetherianRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    [LocallyOfFiniteType f] [QuasiCompact f]
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)] :
    EssentiallyCountableCategory
        (ObjectProperty.FullSubcategory
          (fun K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace) =>
            RingedSpace.IsPerfect (X := X.toRingedSpace) K)) ∧
      EssentiallyCountableCategory
        (ObjectProperty.FullSubcategory
          (DerivedCategoryB.derivedCategoryBBounded
            (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)))
Tag 0G0X, a lemma

Tag 0G0X in the Stacks Project.

AlgebraicGeometry.exists_countable_finiteType_isomorphism_families_of_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/CountableIsomorphismFamilies.lean, line 592.

For S of finite type over an algebraically closed field K and X, Y of finite type over S, there is a countable set I, for each i a finite-type morphism S i ⟶ S and an isomorphism X ×_S S i ≅ Y ×_S S i over S i, such that every closed point of S valued in K whose two fibres are isomorphic over K lies in the image of some S i ⟶ S.

public theorem exists_countable_finiteType_isomorphism_families_of_isAlgClosed
    {K : Type u} [Field K] [IsAlgClosed K]
    (S : Over (Spec (.of K))) [LocallyOfFiniteType S.hom] [QuasiCompact S.hom]
    (X Y : Over S.left)
    [LocallyOfFiniteType X.hom] [QuasiCompact X.hom]
    [LocallyOfFiniteType Y.hom] [QuasiCompact Y.hom] :
    ∃ (I : Type (u + 1)) (_ : Countable I) (T : I → Over S.left)
      (_ : ∀ i, LocallyOfFiniteType (T i).hom ∧ QuasiCompact (T i).hom)
      (_ : ∀ i, (Over.pullback (T i).hom).obj X ≅ (Over.pullback (T i).hom).obj Y),
      ∀ (s : Over.mk (𝟙 (Spec (.of K))) ⟶ S),
        Nonempty ((Over.pullback s.left).obj X ≅ (Over.pullback s.left).obj Y) →
          ∃ (i : I) (t : Spec (.of K) ⟶ (T i).left),
            t ≫ (T i).hom = s.left
Tag 0G0Y, a lemma

Tag 0G0Y in the Stacks Project.

AlgebraicGeometry.exists_countable_relativeEquivalenceKernels, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/Countability/RelativeEquivalenceKernels.lean, line 54.

Stacks Project, Tag 0G0Y. Let K be an algebraically closed field. There is a countable set I and for each i ∈ I a system (Sᵢ/K, Xᵢ ⟶ Sᵢ, Yᵢ ⟶ Sᵢ, Mᵢ) with 1. Sᵢ of finite type over K, 2. Xᵢ ⟶ Sᵢ and Yᵢ ⟶ Sᵢ proper and smooth, 3. Mᵢ ∈ D_perf(𝒪_{Xᵢ ×_{Sᵢ} Yᵢ}) the Fourier-Mukai kernel of a relative equivalence from Xᵢ to Yᵢ over Sᵢ, 4. for all smooth proper K-schemes X, Y with a K-linear exact equivalence D_perf(𝒪_X) ⟶ D_perf(𝒪_Y) there are i ∈ I and s ∈ Sᵢ(K) with X ≅ (Xᵢ)ₛ and Y ≅ (Yᵢ)ₛ.

theorem exists_countable_relativeEquivalenceKernels (K : Type u) [Field K] [IsAlgClosed K] :
    ∃ (I : Type (u + 1)) (_ : Countable I)
      (S : I → Over (Spec (.of K)))
      (X Y : (i : I) → Over (S i).left)
      (M : (i : I) → DerivedCategory (pullback (X i).hom (Y i).hom).Modules)
      (_ : ∀ i, LocallyOfFiniteType (S i).hom ∧ QuasiCompact (S i).hom)
      (_ : ∀ i, Smooth (X i).hom ∧ IsProper (X i).hom)
      (_ : ∀ i, Smooth (Y i).hom ∧ IsProper (Y i).hom)
      (_ : ∀ i, IsRelativeEquivalenceKernel (X i).hom (Y i).hom (M i)),
      ∀ (A B : Over (Spec (.of K))),
        Smooth A.hom → IsProper A.hom → Smooth B.hom → IsProper B.hom →
          (letI : Linear K A.left.Modules := modulesLinear K A
           letI : Linear K B.left.Modules := modulesLinear K B
           ∃ e : PerfectDerivedCategory A.left ≌ PerfectDerivedCategory B.left,
             e.functor.Linear K ∧
               ∃ h : e.functor.CommShift ℤ,
                 letI := h
                 e.functor.IsTriangulated) →
            ∃ (i : I) (s : Over.mk (𝟙 (Spec (.of K))) ⟶ S i),
              Nonempty (A ≅ (Over.pullback s.left).obj (X i)) ∧
                Nonempty (B ≅ (Over.pullback s.left).obj (Y i))
Sources
LeanAlgebraicGeometry.countable_hom_of_finiteType · AlgebraicGeometry.countable_isomorphismClasses_of_finiteType · AlgebraicGeometry.boundedDerivedCategory_essentiallyCountable · AlgebraicGeometry.essentiallyCountable_perfect_and_boundedCoherent_of_finiteType · AlgebraicGeometry.exists_countable_finiteType_isomorphism_families_of_isAlgClosed · AlgebraicGeometry.exists_countable_relativeEquivalenceKernels

Section57.18 Countability of derived equivalent varieties#

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

Tag 0G10, a definition

Tag 0G10 in the Stacks Project.

AlgebraicGeometry.DerivedEquivalent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedEquivalence.lean, line 49.

Two schemes over a field k are derived equivalent if their categories of perfect complexes admit a k-linear exact equivalence.

abbrev DerivedEquivalent (k : Type u) [Field k] (X Y : Over (Spec (.of k))) : Prop
Tag 0G11, a theorem

Tag 0G11 in the Stacks Project.

AlgebraicGeometry.countable_isomorphismClasses_derivedEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/Countability/DerivedEquivalentPartners.lean, line 252.

Stacks Project, Tag 0G11. Let K be an algebraically closed field and let X₀ be a smooth proper scheme over K. There are at most countably many isomorphism classes of smooth proper schemes Y over K which are derived equivalent to X₀, i.e. admit a K-linear exact equivalence D_perf(𝒪_{X₀}) ⟶ D_perf(𝒪_Y) ([Stacks, Tag 0G10]).

Proof: [Stacks, Tag 0G0Y] (exists_countable_relativeEquivalenceKernels) produces the countable family of relative equivalences, and countable_isomorphismClasses_derivedEquivalent_of_relativeEquivalenceFamilies counts.

theorem countable_isomorphismClasses_derivedEquivalent
    (X₀ : Over (Spec (CommRingCat.of k))) [Smooth X₀.hom] [IsProper X₀.hom] :
    {c : IsomorphismClassOver k | ∃ Y : Over (Spec (CommRingCat.of k)),
      Smooth Y.hom ∧ IsProper Y.hom ∧
        (letI : Linear k X₀.left.Modules := modulesLinear k X₀
         letI : Linear k Y.left.Modules := modulesLinear k Y
         ∃ e : Stacks.Perfect.BoundedLocallyFreeComplexes.PerfectDerivedCategory X₀.left ≌
             Stacks.Perfect.BoundedLocallyFreeComplexes.PerfectDerivedCategory Y.left,
           e.functor.Linear k ∧
             ∃ h : e.functor.CommShift ℤ,
               letI := h
               e.functor.IsTriangulated) ∧
        c = isomorphismClassOver Y}.Countable
Sources
LeanAlgebraicGeometry.DerivedEquivalent · AlgebraicGeometry.countable_isomorphismClasses_derivedEquivalent

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.