110.53 Stack with quasi-compact… to 110.78 Flat maps are not…

Section110.53 Stack with quasi-compact flat covering which is not algebraic#

Section 110.53 of the Stacks Project, Tag 04AG. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04AH, a lemma

Tag 04AH in the Stacks Project.

AlgebraicGeometry.Stack.isFiniteType_of_smoothSchemeCovering_classifyingStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/ClassifyingStackSmoothCovering.lean, line 125. The attribute's comment: “conditional on Stacks 04WZ, that the diagonal of a quotient stack is representable by algebraic spaces, and on the implication of Stacks 06PL that an algebraic classifying stack has a group locally of finite presentation over the base”.

Stacks 04AH. Let k be a field and let G be an affine group scheme over k. If the classifying stack [Spec(k)/G] has a smooth surjective covering by a scheme, then G is of finite type over k.

The covering hypothesis is the third clause of Stacks 026O for the classifying stack. The hypotheses hdiag and hfp are Stacks 04WZ and the forward implication of Stacks 06PL, which this library does not have.

theorem isFiniteType_of_smoothSchemeCovering_classifyingStack
    (G : Space.GroupAlgebraicSpace C (Spec (.of k)) hk
      (Space.terminalSpace C (Spec (.of k)) hk).obj
      (Space.terminalSpace C (Spec (.of k)) hk).property)
    (hAffine : Space.IsAffineHom C (Spec (.of k)) hk G.obj.X.hom)
    (hdiag : HasRepresentableDiagonal C (Spec (.of k)) hk (classifyingStack C hk G))
    (hfp : IsAlgebraicStack.{u, u} C (Spec (.of k)) hk (classifyingStack C hk G).val →
      Space.IsLocallyOfFinitePresentation C (Spec (.of k)) hk G.obj.X.hom)
    (hcov :
      ∃ (U : BigFppfOver C (Spec (.of k)) hk)
        (f : (schemeFibredCategory C (Spec (.of k)) hk U).val ⥤ᵇ
          (classifyingStack C hk G).val),
        IsRepresentableByAlgebraicSpaces C (Spec (.of k)) hk f ∧
          ∀ (V : BigFppfOver C (Spec (.of k)) hk)
            (y : BigFppfOver C V.left.1 V.left.2 ⥤ (classifyingStack C hk G).val.obj)
            (_hy : y ⋙ (classifyingStack C hk G).val.p = Over.map V.hom)
            (F : (BigFppfOver C V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
            (hF : IsAlgebraicSpace C V.left.1 V.left.2 F),
            Nonempty (StacksRepresentableCFG.EquivalenceOver
              (TwoFibreProductOver.fst (Over.map V.hom)
                (schemeFibredCategory C (Spec (.of k)) hk U).val.p
                (classifyingStack C hk G).val.p y f.toFunctor)
              (presheafOfCategories (F ⋙ typeToCat)).p) →
              (let g := (algebraicSpaceMap C (Spec (.of k)) hk V
                ((spacesOverSmallerBaseFunctor C V.left.1 (Spec (.of k)) V.left.2 hk
                  V.hom).obj ⟨F, hF⟩)).hom
               Space.IsSurjective C (Spec (.of k)) hk g ∧
                 Space.IsSmooth C (Spec (.of k)) hk g)) :
    Space.IsFiniteType C (Spec (.of k)) hk G.obj.X.hom
Sources
LeanAlgebraicGeometry.Stack.isFiniteType_of_smoothSchemeCovering_classifyingStack

Section110.54 Limit preserving on objects, not limit preserving#

Section 110.54 of the Stacks Project, Tag 07Z0. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07Z1, a lemma

Tag 07Z1 in the Stacks Project.

AlgebraicGeometry.Stack.ObjectwiseLimitPreserving.exists_stack_isLimitPreservingOnObjects_not_isLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/ObjectwiseLimitPreserving.lean, line 2427.

Stacks 07Z1. Over a nonempty base there is a stack in groupoids whose structure morphism to the big fppf site is limit preserving on objects while the stack itself is not limit preserving. The stackiness of the category of torsors, Stacks 04UM, enters as the hypothesis h04UM.

public theorem exists_stack_isLimitPreservingOnObjects_not_isLimitPreserving
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [Nonempty S]
    (h04UM : ∀ {ℬ : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (𝒢 : Grp (Over ℬ)),
      Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) ℬ →
      Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) 𝒢.X.left →
      Functor.IsStackInGroupoids.{u + 1}
        (ClassifyingTorsors.torsorsProjection 𝒢)
        (AlgebraicGeometry.BigFppfOver.topology B S hS)) :
    ∃ 𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
        (AlgebraicGeometry.BigFppfOver B S hS),
      𝒳.val.p.IsStackInGroupoids.{u + 1}
          (AlgebraicGeometry.BigFppfOver.topology B S hS) ∧
        AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, u, u + 1} B S hS 𝒳
          (AlgebraicGeometry.Stack.terminalCFG B S hS)
          (Bicategory.InducedBicategory.mkHom
            (AlgebraicGeometry.Stack.toTerminalCFG B S hS 𝒳)) ∧
        ¬ Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS 𝒳
Sources
LeanAlgebraicGeometry.Stack.ObjectwiseLimitPreserving.exists_stack_isLimitPreservingOnObjects_not_isLimitPreserving

Section110.56 Sheaf with quasi-compact flat covering which is not algebraic#

Section 110.56 of the Stacks Project, Tag 078E. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 078F, a lemma

Tag 078F in the Stacks Project.

AlgebraicGeometry.isSheaf_fpqc_projectiveLinePow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/ProductOfProjectiveLines.lean, line 382. The attribute's comment: “the witness (P^1)^∞ is a sheaf for the fpqc topology”.

(ℙ¹)^∞ satisfies the sheaf condition for the fpqc topology.

theorem isSheaf_fpqc_projectiveLinePow :
    Presheaf.IsSheaf Scheme.fpqcTopology.{u} projectiveLinePow.{u}

AlgebraicGeometry.relativelyRepresentable_diag_projectiveLinePow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/ProductOfProjectiveLines.lean, line 388. The attribute's comment: “the witness (P^1)^∞ has representable diagonal”.

The diagonal of (ℙ¹)^∞ is representable.

theorem relativelyRepresentable_diag_projectiveLinePow :
    yoneda.relativelyRepresentable (diag projectiveLinePow.{u})
Sources
LeanAlgebraicGeometry.isSheaf_fpqc_projectiveLinePow · AlgebraicGeometry.relativelyRepresentable_diag_projectiveLinePow

Section110.58 Sheaves and specializations#

Section 110.58 of the Stacks Project, Tag 05LD. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05LE, a lemma

Tag 05LE in the Stacks Project.

Stacks.Examples.DimensionSheaf.exists_sheaf_detecting_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Sheaves/DimensionDetectingEtaleSheaf.lean, line 1005.

Stacks 05LE. For every big étale site and every natural number n there is a sheaf of abelian groups G on it whose sections over X are zero when \dim(X) < n, are nonzero when \dim(X) \ge n, and restrict isomorphically along a thickening X \subset X'.

public theorem exists_sheaf_detecting_dimension (B : BigEtaleSite.{u}) (n : ℕ) :
    ∃ G : Sheaf B.topology AddCommGrpCat.{u + 1},
      (∀ X : B.Scheme, topologicalKrullDim ((B.inclusion).obj X) < (n : WithBot ℕ∞) →
          Subsingleton (G.obj.obj (Opposite.op X))) ∧
        (∀ X : B.Scheme, (n : WithBot ℕ∞) ≤ topologicalKrullDim ((B.inclusion).obj X) →
          Nontrivial (G.obj.obj (Opposite.op X))) ∧
        (∀ (X X' : B.Scheme) (i : X ⟶ X'),
          Stacks.Thickenings.IsThickening ((B.inclusion).map i) →
            IsIso (G.obj.map i.op))
Sources
LeanStacks.Examples.DimensionSheaf.exists_sheaf_detecting_dimension

Section110.59 Sheaves and constructible functions#

Section 110.59 of the Stacks Project, Tag 05LG. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05LH, a lemma

Tag 05LH in the Stacks Project.

Stacks.Examples.ConstructibleFunctionSheaf.exists_nonzero_limitPreserving_sheaf_vanishing_on_fields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Schemes/ConstructibleFunctionSheaf.lean, line 1423.

A nonzero limit-preserving étale sheaf of abelian groups which vanishes on fields and whose restriction maps along thickenings are isomorphisms.

public theorem exists_nonzero_limitPreserving_sheaf_vanishing_on_fields
    (B : BigEtaleSite.{u}) [UnivLE.{max v w, u}] :
    ∃ G : Sheaf B.topology AddCommGrpCat.{u},
      (∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k))),
        IsZero (G.obj.obj (Opposite.op (B.obj (Spec (.of k)) hk)))) ∧
      AlgebraicGeometry.LimitPreserving.{u, u, v, w, u + 1, u}
        B.inclusion (G.obj ⋙ forget AddCommGrpCat.{u}) ∧
      (∀ (X X' : Scheme.{u}) (hX : B.Contains X) (hX' : B.Contains X')
        (i : X ⟶ X'), Stacks.Thickenings.IsThickening i →
          IsIso (G.obj.map (ObjectProperty.homMk i :
            B.obj X hX ⟶ B.obj X' hX').op)) ∧
      (∃ X : B.Scheme, ¬ IsZero (G.obj.obj (Opposite.op X)))
Sources
LeanStacks.Examples.ConstructibleFunctionSheaf.exists_nonzero_limitPreserving_sheaf_vanishing_on_fields

Section110.60 The lisse-étale site is not functorial#

Section 110.60 of the Stacks Project, Tag 07BF. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07BG, a lemma

Tag 07BG in the Stacks Project.

AlgebraicGeometry.Stack.LisseEtale.exists_not_isMorphismOfSites_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/LisseEtaleNotFunctorial.lean, line 128.

Stacks 07BG. The lisse-étale site is not functorial, even for morphisms of schemes.

There is a morphism f : X ⟶ Y of schemes over S in a big fppf site for which the base-change functor Y_{lisse,étale} ⥤ X_{lisse,étale} — identified here by a natural isomorphism after forgetting smoothness, so that no particular choice of fibre products is asserted — is continuous, and yet does not define a morphism of sites: its pushforward on sheaves has no left exact left adjoint.

See the module documentation for the counterexample.

theorem exists_not_isMorphismOfSites_pullback :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (X Y : BigFppfOver B S hS) (f : X ⟶ Y)
      (F : LisseEtale.{u, w} B S hS (schemeStack.{u, w} B S hS Y) ⥤
        LisseEtale.{u, w} B S hS (schemeStack.{u, w} B S hS X)),
      Nonempty (F ⋙ inclusion.{u, w} B S hS (schemeStack.{u, w} B S hS X) ≅
        inclusion.{u, w} B S hS (schemeStack.{u, w} B S hS Y) ⋙ Over.pullback f) ∧
      F.IsContinuous (topology.{u, w} B S hS (schemeStack.{u, w} B S hS Y))
        (topology.{u, w} B S hS (schemeStack.{u, w} B S hS X)) ∧
      ¬ IsMorphismOfSites.{u + 1} F
        (topology.{u, w} B S hS (schemeStack.{u, w} B S hS Y))
        (topology.{u, w} B S hS (schemeStack.{u, w} B S hS X))
Sources
LeanAlgebraicGeometry.Stack.LisseEtale.exists_not_isMorphismOfSites_pullback

Section110.61 Sheaves on the category of Noetherian schemes#

Section 110.61 of the Stacks Project, Tag 0GE8. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GE9, a lemma

Tag 0GE9 in the Stacks Project.

AlgebraicGeometry.LocallyNoetherianOver.not_isMorphismOfSites_toBigFppfOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Sites/NoetherianSiteNotMorphismOfSites.lean, line 416.

Stacks 0GE9. With S = Spec 𝐅_p the inclusion functor (Noetherian/S)_{fppf} ⟶ (Sch/S)_{fppf} does not define a morphism of sites.

Its pushforward on sheaves of sets has no left exact left adjoint. Both sites are subcanonical, so a left exact u_s would identify the two Yoneda embeddings and force the inclusion to preserve monomorphisms, which by AlgebraicGeometry.LocallyNoetherianOver.not_preservesMonomorphisms_toBigFppfOver it does not.

public theorem not_isMorphismOfSites_toBigFppfOver
    (p : ℕ) [Fact p.Prime] (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of (ULift.{u} (ZMod p))))) :
    ¬ IsMorphismOfSites.{u + 1}
      (toBigFppfOver B (Spec (.of (ULift.{u} (ZMod p)))) hS)
      (fppfTopology B (Spec (.of (ULift.{u} (ZMod p)))) hS)
      (BigFppfOver.topology B (Spec (.of (ULift.{u} (ZMod p)))) hS)
Sources
LeanAlgebraicGeometry.LocallyNoetherianOver.not_isMorphismOfSites_toBigFppfOver

Section110.62 Derived pushforward of quasi-coherent modules#

Section 110.62 of the Stacks Project, Tag 07DC. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08IY, a lemma

Tag 08IY in the Stacks Project.

AlgebraicGeometry.Stack.exists_isDerivedLimit_truncGETower_of_lqcFbc', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedLimitOfTruncations.lean, line 285. The attribute's comment: “K is the derived limit of its canonical truncations from below, for a complex of fppf modules with cohomology sheaves in LQCoh^fbc; the affine-object vanishing the source cites is carried as the hypothesis hvan”.

Stacks 08IY. Let 𝒳 be an algebraic stack and let K be an object of D(𝒪_𝒳) whose cohomology sheaves are locally quasi-coherent (Stacks 06WJ) and have the flat base change property (Stacks 0762). Then there is a distinguished triangle

K ⟶ ∏_{n ≥ 0} τ_{≥ -n}K ⟶ ∏_{n ≥ 0} τ_{≥ -n}K ⟶ K[1]

in D(𝒪_𝒳): K is the derived limit of its canonical truncations from below.

This is AlgebraicGeometry.Stack.exists_isDerivedLimit_truncGETower_of_lqcFbc with the covering class of the source's proof discharged by AlgebraicGeometry.Stack.hasEnoughObjects_isAffineOver, at the hom universe u + 1 of the fppf site of an algebraic stack. The hypothesis hvan is the source's first sentence, carried; see this file's module documentation for the four cited lemmas it stands for and for why none of them is available.

theorem exists_isDerivedLimit_truncGETower_of_lqcFbc' {𝒳 : Type v} [Category.{u + 1} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    [HasSheafify (BigFppfOver.associatedTopology B S hS p .fppf) AddCommGrpCat.{u}]
    [(BigFppfOver.associatedTopology B S hS p .fppf).WEqualsLocallyBijective AddCommGrpCat.{u}]
    [EnoughInjectives (fppfSiteModules B S hS p hp)]
    (K : DerivedCategory (fppfSiteModules B S hS p hp))
    (hK : ∀ i : ℤ, IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp
      ((DerivedCategory.homologyFunctor (fppfSiteModules B S hS p hp) i).obj K).val)
    (hvan : HasAffineAcyclicLqcFbcModules B E h S hS p hp) :
    ∃ _ : HasProduct fun n : ℕ ↦ (fppfTruncGETower B S hS p hp K).obj ⟨n⟩,
      IsDerivedLimit (fppfTruncGETower B S hS p hp K) K
Tag 08IZ, a lemma

Tag 08IZ in the Stacks Project.

AlgebraicGeometry.Stack.isIso_coproductToProduct_shiftedLqcFbc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ShiftedSumOfModules.lean, line 117. The attribute's comment: “the sum of a family of shifted LQCoh^fbc modules, indexed by n ≥ 0 as the source's proof supports, maps isomorphically to their product in D(𝒪_𝒳); the affine acyclicity the library's Stacks 08IY carries is carried here as that same predicate”.

Stacks 08IZ. Let 𝒳 be an algebraic stack and let ℱ_n, n ≥ 0, be sheaves of 𝒪_𝒳-modules on its big fppf site which are locally quasi-coherent (Stacks 06WJ) and have the flat base change property (Stacks 0762). Then the canonical map

⊕_n ℱ_n[n] ⟶ ∏_n ℱ_n[n]

is an isomorphism in D(𝒪_𝒳).

The vanishing hvan is the hypothesis the library's Stacks 08IY carries, and it is carried in exactly that form; see this file's module documentation.

theorem isIso_coproductToProduct_shiftedLqcFbc (F : ℕ → fppfSiteModules B S hS p hp)
    (hF : ∀ n : ℕ, IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp (F n).val)
    (hvan : HasAffineAcyclicLqcFbcModules B E h S hS p hp) :
    IsIso (Pi.lift (Sigma.π (shiftedSingleFamily B S hS p hp F)))
Tag 07DD, a lemma

Tag 07DD in the Stacks Project.

Stacks.Examples.UnboundedDerivedPushforward.not_isQuasicoherent_of_iso_piStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Examples/UnboundedDerivedPushforward.lean, line 193. The attribute's comment: “the last step of the discussion of Tag 07DC, over its own base S = Spec k[x]: a module identified with the countable product of copies of O_S, which is what that discussion produces as the degree-zero cohomology sheaf of Rf_E, is not quasi-coherent, so Rf_E does not lie in D_QCoh(O_S). Carried as the hypothesis hH is exactly that identification, and with it the quotient stack [Spec k[x]/(Z/pZ)], the quasi-compactness and quasi-separatedness of its structure morphism, the computation Rf_*O_X = sum of O_S[-n] and the identification of E with a product; none of those is established here. Quasi-coherence is that of a module on the scheme S, the sense of the source's not even locally quasi-coherent, and not the local quasi-coherence of Tag 06WJ on the big fppf site”.

Stacks 07DD, in the form this development reaches. The discussion of Stacks 07DC exhibits a quasi-compact and quasi-separated f : 𝒳 = [Spec k[x] / (ℤ/pℤ)] ⟶ S = Spec k[x] and an object E = ⊕_{m ≥ 0} 𝒪_𝒳[m] of D_QCoh(𝒪_𝒳) whose derived pushforward Rf_*E = ∏_{m ≥ 0} ⊕_{n ≥ 0} 𝒪_S[m - n] has, in degree zero, a countable product of copies of 𝒪_S. Here that identification is the hypothesis hH, and the conclusion is the source's: the sheaf so obtained is not quasi-coherent, hence Rf_*E is not an object of D_QCoh(𝒪_S) and Rf_* does not restrict to a functor D_QCoh(𝒪_𝒳) ⟶ D_QCoh(𝒪_S).

The hypothesis is satisfiable: the product exists, so H may be taken to be it with hH the identity. Its content — the quotient stack, the morphism, and the computation of the pushforward — is what this repository does not have; see this file's module documentation for the step-by-step comparison.

public theorem not_isQuasicoherent_of_iso_piStructureSheaf {k : Type u} [CommRing k]
    [Nontrivial k] (H : (Spec (CommRingCat.of (Polynomial k))).Modules)
    (hH : H ≅ ∏ᶜ (fun _ : ℕ => SheafOfModules.unit
      (Spec (CommRingCat.of (Polynomial k))).ringCatSheaf)) :
    ¬ H.IsQuasicoherent
Sources
LeanAlgebraicGeometry.Stack.exists_isDerivedLimit_truncGETower_of_lqcFbc' · AlgebraicGeometry.Stack.isIso_coproductToProduct_shiftedLqcFbc · Stacks.Examples.UnboundedDerivedPushforward.not_isQuasicoherent_of_iso_piStructureSheaf

Section110.63 A big abelian category#

Section 110.63 of the Stacks Project, Tag 07JS. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07JT, a lemma

Tag 07JT in the Stacks Project.

Stacks.Examples.exists_abelian_not_hasExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/CategoryTheory/AbelianCategoryWithLargeExt.lean, line 270.

Stacks 07JT. There exists a large abelian category whose Ext-groups are not small in the next lower universe.

theorem exists_abelian_not_hasExt :
    ∃ (C : Type (u + 1)) (_ : Category.{u} C) (_ : Abelian C),
      ¬ HasExt.{u} C
Sources
LeanStacks.Examples.exists_abelian_not_hasExt

Section110.64 Weakly associated points and scheme theoretic density#

Section 110.64 of the Stacks Project, Tag 084J. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 084K, a lemma

Tag 084K in the Stacks Project.

Stacks.Examples.exists_isSchemeTheoreticallyDense_open_notMem_weaklyAssociatedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Schemes/SchemeTheoreticallyDenseOpenMissingWeaklyAssociatedPoint.lean, line 193.

Stacks 084K. A reduced scheme can have a scheme-theoretically dense open subscheme that omits a weakly associated point.

theorem exists_isSchemeTheoreticallyDense_open_notMem_weaklyAssociatedPoint :
    ∃ (X : Scheme.{u}) (U : X.Opens) (x : X),
      IsReduced X ∧ Scheme.Opens.IsSchemeTheoreticallyDense U ∧
        x ∈ Stacks.Divisors.schemeWeaklyAssociatedPoints X ∧ x ∉ (U : Set X)
Sources
LeanStacks.Examples.exists_isSchemeTheoreticallyDense_open_notMem_weaklyAssociatedPoint

Section110.65 Example of non-additivity of traces#

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

Tag 087K, an equation

Tag 087K in the Stacks Project.

Stacks.Examples.dualNumber_diagram_commutes_up_to_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/DualNumberHomotopyDiagram.lean, line 95.

The prescribed endomorphism of the left column and the identity endomorphisms of the middle and right columns make the two squares commute in the homotopy category.

public theorem dualNumber_diagram_commutes_up_to_homotopy :
    ∃ (i : dualNumberLeftComplex k ⟶ dualNumberMiddleComplex k)
      (p : dualNumberMiddleComplex k ⟶ dualNumberRightComplex k)
      (a : dualNumberLeftComplex k ⟶ dualNumberLeftComplex k),
      (i.f 1 = 𝟙 _) ∧
      (∀ n : ℤ, n ≠ 1 → i.f n = 0) ∧
      (p.f 0 = 𝟙 _) ∧
      (∀ n : ℤ, n ≠ 0 → p.f n = 0) ∧
      (a.f 1 = ModuleCat.ofHom (LinearMap.mulLeft (dualNumberRing k)
        (1 + (DualNumber.eps : dualNumberRing k)))) ∧
      (∀ n : ℤ, n ≠ 1 → a.f n = 0) ∧
      ((HomotopyCategory.quotient (DualNumberModuleCat k) (ComplexShape.up ℤ)).map a ≫
          (HomotopyCategory.quotient (DualNumberModuleCat k) (ComplexShape.up ℤ)).map i =
        (HomotopyCategory.quotient (DualNumberModuleCat k) (ComplexShape.up ℤ)).map i) ∧
      (i ≫ p = 0)
Tag 087L, a lemma

Tag 087L in the Stacks Project.

Stacks.Examples.exists_distinguished_triangle_trace_nonadditive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/NonAdditivityOfTraces.lean, line 492.

Stacks 087L. Trace need not be additive on an endomorphism of a distinguished triangle of perfect complexes in the homotopy category.

public theorem exists_distinguished_triangle_trace_nonadditive :
    ∃ (R : Type u) (hR : Ring R),
      letI : Ring R := hR
      ∃ (P Q S : CochainComplex (ModuleCat.{v} R) ℤ)
        (hP : CategoryTheory.FilteredDerived.finiteProjectiveComplex R P)
        (hQ : CategoryTheory.FilteredDerived.finiteProjectiveComplex R Q)
        (hS : CategoryTheory.FilteredDerived.finiteProjectiveComplex R S),
        let q := HomotopyCategory.quotient (ModuleCat.{v} R) (ComplexShape.up ℤ)
        ∃ (f : q.obj P ⟶ q.obj Q) (g : q.obj Q ⟶ q.obj S)
          (h : q.obj S ⟶ (q.obj P)⟦(1 : ℤ)⟧)
          (a : P ⟶ P) (b : Q ⟶ Q) (c : S ⟶ S),
          (Triangle.mk f g h ∈ distTriang _) ∧
          (∃ t : Triangle.mk f g h ⟶ Triangle.mk f g h,
            t.hom₁ = q.map a ∧ t.hom₂ = q.map b ∧ t.hom₃ = q.map c) ∧
          CategoryTheory.FilteredDerived.alternatingTrace R P hP a +
            CategoryTheory.FilteredDerived.alternatingTrace R S hS c ≠
            CategoryTheory.FilteredDerived.alternatingTrace R Q hQ b
Sources
LeanStacks.Examples.dualNumber_diagram_commutes_up_to_homotopy · Stacks.Examples.exists_distinguished_triangle_trace_nonadditive

Section110.67 Being projective is not local on the base#

Section 110.67 of the Stacks Project, Tag 08J0. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08J1, a lemma

Tag 08J1 in the Stacks Project.

Stacks.Examples.ProjectivityNotLocalOnBase.not_isZariskiLocalAtTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Examples/ProjectivityNotLocalOnBase.lean, line 290. The attribute's comment: “the tag's two assertions REDUCED TO HIRONAKA'S EXAMPLE, which is NOT proved. The witness is the named hypothesis ProperLocallyProjectiveNotProjective (:220) -- a proper, Zariski-locally projective, non-projective morphism -- and it carries the whole content of the tag; hRL and hBCL are the source's own Tags 07RL and 0BCL (1), also carried. What IS proved unconditionally, and is the reason the reduction is exact rather than circular: isLocallyProjective_iff_isProjective (:192) shows that Zariski-locality of projectivity is precisely the collapse of Tag 01W8 (1) onto Tag 01W8 (3), i.e. of IsProjective onto IsLocallyProjective, so refuting locality is exactly exhibiting a morphism separating those two notions -- nothing more is needed and nothing less suffices. The fpqc assertions follow from the Zariski ones at :293, :301, :310 via zariskiPrecoverage_le_fpqcPrecoverage. Of the construction, step 3 is fully proved over any domain in Examples/HironakaConicIntersection.lean: the two conics meet exactly in the two points P and Q (conicIdealC_sup_conicIdealD_eq_inf, :366) and that intersection is reduced (isRadical_conicIdealC_sup_conicIdealD, :372). Absent: the conics as smooth closed subschemes of P^3, the two iterated blow-up towers and their gluing over Y - P - Q, Tags 01OE and 0BCL (1) for 01W8-projectivity, and the rational equivalences on the exceptional surface. Tag 02TI, which the degree argument consumes, IS present (Stacks.Chow.firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor)”.

[Stacks, Tag 08J1], granted Hironaka's example and the two comparisons of Tags 07RL and 0BCL. Neither projectivity nor quasi-projectivity is Zariski local on the base.

theorem not_isZariskiLocalAtTarget (hH : ProperLocallyProjectiveNotProjective.{u})
    (hRL : ProjectiveIsQuasiProjective.{u}) (hBCL : ProperQuasiProjectiveIsProjective.{u}) :
    ¬ IsZariskiLocalAtTarget projectiveProperty.{u} ∧
      ¬ IsZariskiLocalAtTarget quasiProjectiveProperty.{u}

Stacks.Examples.ProjectivityNotLocalOnBase.not_isZariskiLocalAtTarget_and_not_isLocalAtTarget_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Examples/ProjectivityNotLocalOnBaseUnconditional.lean, line 132.

The properties "f is projective" and "f is quasi-projective" are not Zariski local on the base; a fortiori, they are not fpqc local on the base.

The witness is Hironaka's example, Stacks.Examples.ProjectivityNotLocalOnBase.properLocallyProjectiveNotProjective.

theorem not_isZariskiLocalAtTarget_and_not_isLocalAtTarget_fpqc :
    (¬ IsZariskiLocalAtTarget projectiveProperty.{u} ∧
      ¬ IsZariskiLocalAtTarget quasiProjectiveProperty.{u}) ∧
    (¬ projectiveProperty.{u}.IsLocalAtTarget Scheme.fpqcPrecoverage ∧
      ¬ quasiProjectiveProperty.{u}.IsLocalAtTarget Scheme.fpqcPrecoverage)
Sources
LeanStacks.Examples.ProjectivityNotLocalOnBase.not_isZariskiLocalAtTarget · Stacks.Examples.ProjectivityNotLocalOnBase.not_isZariskiLocalAtTarget_and_not_isLocalAtTarget_fpqc

Section110.68 Non-effective descent data for projective schemes#

Section 110.68 of the Stacks Project, Tag 08KE. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08KF, a lemma

Tag 08KF in the Stacks Project.

Stacks.Examples.NonEffectiveProjectiveDescent.exists_nonEffectiveDescentData_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Examples/NonEffectiveProjectiveDescent.lean, line 241. The attribute's comment: “THE EXISTENCE IS NOT ASSERTED. What is proved is the reduction of the tag to its family form: given an étale covering family whose members are H-projective over the base and whose descent datum is not family-effective, the coproduct is a single étale morphism, is projective, and its datum is not effective. The witness itself is carried as EtaleProjectiveNonEffectiveFamily, which is what the chain of Tags 0D5E (existence half, blocked on Artin contraction), 0E6F (no library carrier at all) and 02W5 (fppf case, only the general-site halves are proved) would produce”.

[Stacks, Tag 08KF], granted the construction of the witness. There are an étale covering of a scheme consisting of a single morphism f : X ⟶ S and a descent datum relative to f whose scheme over X is projective over X and which is not effective in the category of schemes.

theorem exists_nonEffectiveDescentData_projective
    (hW : EtaleProjectiveNonEffectiveFamily.{u}) :
    ∃ (S X : Scheme.{u}) (f : X ⟶ S)
      (D : DescentData (S := S) (X := fun _ : Unit ↦ X) (fun _ ↦ f)),
      Presieve.singleton f ∈ Scheme.etalePrecoverage S ∧
        IsProjective (D.obj ()).hom ∧ ¬ D.IsEffective
Sources
LeanStacks.Examples.NonEffectiveProjectiveDescent.exists_nonEffectiveDescentData_projective

Section110.69 A family of curves whose total space is not a scheme#

Section 110.69 of the Stacks Project, Tag 0D5D. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0D5E, a lemma

Tag 0D5E in the Stacks Project.

Stacks.Examples.CurveFamilyNotScheme.not_exists_scheme_of_no_dominating_closed_avoiding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/CurveFamilyNotScheme.lean, line 197. The attribute's comment: “the obstruction: no scheme carries the geometry of the construction, conditional on Artin's contraction theorem and on the choice of the point on the central fibre, whose outputs are the hypotheses”.

Stacks 0D5E. There exists a field k and a family of curves X → A¹_k such that X is not a scheme.

What is proved is the obstruction: no scheme carries the geometry that the construction produces. Explicitly, there is no scheme X with a proper morphism f : X ⟶ S to an affine base whose fibres are all infinite, together with a point x of X such that no closed subset of X avoiding x surjects onto S.

The total space of the source's family satisfies the three hypotheses with S = A¹_k: it is proper over the affine line with one-dimensional, hence infinite, fibres, and the point x to which the strict transform of the central fibre is contracted is avoided by no dominating closed subset, because such a subset would push down to a proper closed subscheme of the cubic surface Y dominating the affine line and meeting Y₀ only in the chosen point y. So the total space is not a scheme.

What is not proved is that the family exists. Its construction needs Artin's contraction theorem for algebraic spaces, which this library does not have, and the point y on the Fermat cubic is chosen by a countability argument against the Picard group of the rational surface Y; both are inputs rather than conclusions here, and what they deliver is precisely the third hypothesis below.

theorem not_exists_scheme_of_no_dominating_closed_avoiding (S : Scheme.{u}) [IsAffine S] :
    ¬ ∃ (X : Scheme.{u}) (f : X ⟶ S) (_ : IsProper f) (x : X),
        (∀ s : S, ¬ (f ⁻¹' {s}).Finite) ∧
          ∀ T : Set X, IsClosed T → x ∉ T → ∃ s : S, ∀ y ∈ T, f y ≠ s
Sources
LeanStacks.Examples.CurveFamilyNotScheme.not_exists_scheme_of_no_dominating_closed_avoiding

Section110.70 Derived base change#

Section 110.70 of the Stacks Project, Tag 08J2. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08J3, a lemma

Tag 08J3 in the Stacks Project.

Stacks.Examples.no_derived_base_change, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/NoDerivedBaseChange.lean, line 811.

In general, derived base change of A-modules to R' does not factor through the derived category of the ordinary tensor-product algebra.

public theorem no_derived_base_change :
    ∃ (R : Type u), ∃ (hR : CommRing R),
      letI : CommRing R := hR
      ∃ (A : Type u), ∃ (hA : CommRing A),
        letI : CommRing A := hA
        ∃ (R' : Type u), ∃ (hR' : CommRing R'),
          letI : CommRing R' := hR'
          ∃ (f : R →+* A) (g : R →+* R'),
            letI : Algebra R A := f.toAlgebra
            letI : Algebra R R' := g.toAlgebra
            letI : Algebra R' (A ⊗[R] R') := Algebra.TensorProduct.rightAlgebra
            ¬ ∃ (T : DerivedCategory (ModuleCat.{u} A) ⥤
                DerivedCategory (ModuleCat.{u} (A ⊗[R] R'))),
              ∀ (M : ModuleCat.{u} A),
                Nonempty
                  (((ModuleCat.restrictScalars
                      (algebraMap R' (A ⊗[R] R'))).mapDerivedCategory.obj
                        (T.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj M))) ≅
                    ((derivedExtensionScalarsGeneral.{u, u, u} g).functor.obj
                      ((ModuleCat.restrictScalars f).mapDerivedCategory.obj
                        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj M))))
Sources
LeanStacks.Examples.no_derived_base_change

Section110.71 An interesting compact object#

Section 110.71 of the Stacks Project, Tag 09R4. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09R5, a lemma

Tag 09R5 in the Stacks Project.

Stacks.Examples.exists_isCompactObject_not_representable_by_finite_gradedProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/CompactObjectNoFiniteProjectiveModel.lean, line 1081.

[Stacks, Tag 09R5]. "There exists a differential graded algebra (A, d) and a compact object E of D(A, d) such that E cannot be represented by a finite and graded projective differential graded A-module."

The algebra is A = k[x, y]/(y²) over k = ZMod 2, with x of degree 0, y of degree -1 and d y = x² + x, and E is the summand of the regular module cut out by the idempotent given by multiplication by x (Tag 09R4). The obstruction is Stacks.Examples.not_representable_by_finite_gradedProjective_of_retract_charTwoRegularModule; compactness of E enters only to discharge the first conjunct.

theorem exists_isCompactObject_not_representable_by_finite_gradedProjective :
    ∃ (A : DifferentialGradedAlgebra.{0, 0} (ZMod 2)) (E : derivedCategory' A),
      IsCompactObject.{0} E ∧
        ¬ ∃ P : DifferentialGradedModule.{0, 0, 0} A, IsFinite P ∧
            Stacks.DifferentialGraded.DGModule.IsProjectiveAsGradedModule.{0, 0, 0, 0}
              (Unbundled.module P) ∧
            Nonempty (E ≅ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P)
Sources
LeanStacks.Examples.exists_isCompactObject_not_representable_by_finite_gradedProjective

Section110.74 An example of a non-algebraic Hom-stack#

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

Tag 0AF9, a lemma

Tag 0AF9 in the Stacks Project.

AlgebraicGeometry.fppfH1_restriction_genericPoint_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianSchemeFirstCohomologyGenericPoint.lean, line 183. The attribute's comment: “with the sketch's conclusion that a G-torsor with a K-point is trivial as htrivial”.

Stacks 0AF9. Let W be a two dimensional regular integral Noetherian scheme with function field K and let G → W be an abelian scheme. Then the restriction map H¹_fppf(W, G) → H¹_fppf(Spec K, G) along the generic point is injective.

The geometric conclusion of the source's sketch of proof — an fppf G-torsor with a section over Spec K is trivial — is the hypothesis htrivial; the sketch obtains it from a step the source itself leaves to an unwritten reference on resolving indeterminacies of morphisms for surfaces. See the implementation notes of this file.

public theorem fppfH1_restriction_genericPoint_injective
    [IsIntegral W] [AlgebraicGeometry.IsNoetherian W] (_hreg : IsRegular W)
    (_hdim : topologicalKrullDim (W : Type u) = (2 : WithBot ℕ∞))
    (hK : B.Contains (Spec W.functionField))
    (G : Over W) [GrpObj G] [IsAbelianScheme G] (hG : B.Contains G.left)
    [HasSheafify (BigFppfOver.topology B W hW) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (BigFppfOver.topology B W hW) AddCommGrpCat.{u})]
    (htrivial : ∀ F : Stacks.Cohomology.Torsors.AbelianTorsor (pointsSheaf B W hW G hG),
      Nonempty (F.1.presheaf.obj (op (genericPointObj B W hW hK))) → F.1.IsTrivial) :
    Function.Injective (((pointsSheaf B W hW G hG).cohomologyPresheaf 1).map
      (genericPointToBase B W hW hK).op)
Tag 0H8E, a remark

Tag 0H8E in the Stacks Project.

AlgebraicGeometry.injective_torsorSectionsRestrictGenericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianSchemeTorsorSectionsGenericPoint.lean, line 170. The attribute's comment: “part (1), the injectivity half, for every G-torsor and with the two-dimensionality hypothesis of Stacks 0AF9 absent: the hypotheses on W are exactly noetherian, regular and integral. The surjectivity half of part (1) is the statement that the schematic closure of a rational section of P → W is a section; it is not proved, and is the hypothesis hsurj of bijective_torsorSectionsRestrictGenericPoint_of_surjective, which states part (1) in full. The tag obtains surjectivity by identifying G with the identity component of the Picard scheme of the dual abelian scheme and extending a generically defined invertible sheaf over the regular base, and neither the dual abelian scheme nor that identity component is available in this library”.

Stacks 0H8E, the injectivity half of part (1). Let W be a regular integral Noetherian scheme with function field K and let G → W be an abelian scheme. For every fppf G-torsor P the restriction map P(W) → P(K) on sections is injective. No hypothesis on the dimension of W enters.

A torsor with no section over W has nothing to separate. A torsor with one is trivial, and by naturality of the trivialising isomorphism its restriction map is then conjugate to the restriction map G(W) → G(K) on the points of G, which is injective.

public theorem injective_torsorSectionsRestrictGenericPoint
    [IsIntegral W] [AlgebraicGeometry.IsNoetherian W] (_hreg : IsRegular W)
    (hK : B.Contains (Spec W.functionField))
    (G : Over W) [GrpObj G] [IsAbelianScheme G] (hG : B.Contains G.left)
    (F : Stacks.Cohomology.Torsors.AbelianTorsor (pointsSheaf B W hW G hG)) :
    Function.Injective (torsorSectionsRestrictGenericPoint B W hW hK G hG F)

AlgebraicGeometry.fppfH1_restriction_genericPoint_injective_of_isTrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianSchemeTorsorSectionsGenericPoint.lean, line 232. The attribute's comment: “part (2): the conclusion of Stacks 0AF9 with its two-dimensionality hypothesis dropped, which is what the tag asserts; the hypotheses on W are exactly noetherian, regular and integral. As in Stacks 0AF9 the geometric content is the hypothesis htrivial, that a G-torsor with a section over Spec K is trivial. The tag derives part (2) from its part (1), the bijectivity of P(W) → P(K): the injectivity half of part (1) is proved here, in injective_torsorSectionsRestrictGenericPoint, and its surjectivity half -- the statement that the schematic closure of a rational section of P → W is a section, which supplies htrivial by fppfH1_restriction_genericPoint_injective_of_surjective_sections -- is not, the tag obtaining it by identifying G with the identity component of the Picard scheme of the dual abelian scheme and extending a generically defined invertible sheaf over the regular base, and neither the dual abelian scheme nor that identity component is available in this library. The tag's further remarks, that regularity may be weakened to local factoriality of smooth W-schemes and the attribution of the argument, carry no assertion”.

Stacks 0H8E, part (2). Let W be a regular integral Noetherian scheme with function field K and let G → W be an abelian scheme. Then the restriction map H¹_fppf(W, G) → H¹_fppf(Spec K, G) on first cohomology is injective. No hypothesis on the dimension of W enters.

A class in the kernel of the restriction map is the class of a torsor having a section over Spec K, and such a torsor is trivial by the hypothesis htrivial, so the class is zero.

public theorem fppfH1_restriction_genericPoint_injective_of_isTrivial
    [IsIntegral W] [AlgebraicGeometry.IsNoetherian W] (_hreg : IsRegular W)
    (hK : B.Contains (Spec W.functionField))
    (G : Over W) [GrpObj G] [IsAbelianScheme G] (hG : B.Contains G.left)
    [HasSheafify (BigFppfOver.topology B W hW) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (BigFppfOver.topology B W hW) AddCommGrpCat.{u})]
    (htrivial : ∀ F : Stacks.Cohomology.Torsors.AbelianTorsor (pointsSheaf B W hW G hG),
      Nonempty (F.1.presheaf.obj (op (genericPointObj B W hW hK))) → F.1.IsTrivial) :
    Function.Injective (((pointsSheaf B W hW G hG).cohomologyPresheaf 1).map
      (genericPointToBase B W hW hK).op)
Tag 0AFA, a lemma

Tag 0AFA in the Stacks Project.

AlgebraicGeometry.Space.fppfH1_isAddTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothGroupFirstCohomologyTorsion.lean, line 1103.

Stacks 0AFA. The first fppf cohomology group of a smooth commutative group algebraic space over a field is torsion.

public theorem Space.fppfH1_isAddTorsion
    (k : Type u) [Field k]
    (B : AlgebraicGeometry.BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k)))
    [HasSheafify (AlgebraicGeometry.BigFppfOver.topology B (Spec (.of k)) hk) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigFppfOver.topology B (Spec (.of k)) hk)
      AddCommGrpCat.{u})]
    (G : Sheaf (AlgebraicGeometry.BigFppfOver.topology B (Spec (.of k)) hk)
      AddCommGrpCat.{u})
    (hG : AlgebraicGeometry.IsAlgebraicSpace B (Spec (.of k)) hk
      (G.obj ⋙ forget AddCommGrpCat))
    (hSmooth : AlgebraicGeometry.Space.IsSmooth B (Spec (.of k)) hk
      (terminal.from (G.obj ⋙ forget AddCommGrpCat))) :
    IsAddTorsion (Sheaf.H G 1)
Tag 0AFB, a lemma

Tag 0AFB in the Stacks Project.

Stacks.Examples.NonAlgebraicHomStack.exists_compatible_ne_restrictTotal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/NonAlgebraicHomStack.lean, line 319. The attribute's comment: “the source's own reduction of the tag to the non-surjectivity of H¹(X, A) → lim H¹(Xₙ, A), with the three inputs of its proof as the hypotheses htorsion (0AF9 and 0AFA), hsurjective (part (b)) and hnotTorsion (part (a)); the identification of the Hom-stack's fibre categories with groupoids of torsors, by which the tag's essential surjectivity is this surjectivity, is not formalized”.

Stacks 0AFB, in the shape to which the source reduces it. For the example of a non-algebraic Hom-stack over S = Spec k⟦t⟧, with Xₙ = X ×_S Sₙ the thickenings of the special fibre and A the constant abelian scheme, there is a compatible system of classes in H¹_fppf(Xₙ, A) which is the restriction of no class in H¹_fppf(X, A).

The system is constructed: its level 0 is a class of infinite order, supplied by hnotTorsion, and each next level is a preimage of the level below under the surjection of hsurjective. No class on X restricts to it, because a class on X has finite order by htorsion and hence so does its restriction to X₀.

public theorem exists_compatible_ne_restrictTotal
    (htorsion : IsAddTorsion (Sheaf.H' 𝒜 1 (totalObj B hS fX hX)))
    (hsurjective : ∀ n, Function.Surjective (restrictSucc B hS fX hXn 𝒜 n))
    (hnotTorsion :
      ¬ IsAddTorsion (Sheaf.H' 𝒜 1 (thickeningObj B hS fX hXn 0))) :
    ∃ s : ∀ n, Sheaf.H' 𝒜 1 (thickeningObj B hS fX hXn n),
      (¬ IsOfFinAddOrder (s 0)) ∧
      (∀ n, restrictSucc B hS fX hXn 𝒜 n (s (n + 1)) = s n) ∧
      ∀ ξ : Sheaf.H' 𝒜 1 (totalObj B hS fX hX),
        ∃ n, restrictTotal B hS fX hX hXn 𝒜 n ξ ≠ s n

Stacks.Examples.NonAlgebraicHomStack.not_surjective_toCompatibleSystems, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/NonAlgebraicHomStack.lean, line 342. The attribute's comment: “the source's own reduction of the tag to the non-surjectivity of H¹(X, A) → lim H¹(Xₙ, A), with the three inputs of its proof as the hypotheses htorsion (0AF9 and 0AFA), hsurjective (part (b)) and hnotTorsion (part (a)); the identification of the Hom-stack's fibre categories with groupoids of torsors, by which the tag's essential surjectivity is this surjectivity, is not formalized”.

Stacks 0AFB, in the shape to which the source reduces it: the comparison map H¹_fppf(X, A) ⟶ lim H¹_fppf(Xₙ, A) is not surjective.

public theorem not_surjective_toCompatibleSystems
    (htorsion : IsAddTorsion (Sheaf.H' 𝒜 1 (totalObj B hS fX hX)))
    (hsurjective : ∀ n, Function.Surjective (restrictSucc B hS fX hXn 𝒜 n))
    (hnotTorsion :
      ¬ IsAddTorsion (Sheaf.H' 𝒜 1 (thickeningObj B hS fX hXn 0))) :
    ¬ Function.Surjective (toCompatibleSystems B hS fX hX hXn 𝒜)
Tag 0AFC, a proposition

Tag 0AFC in the Stacks Project.

Stacks.Examples.NonAlgebraicHomStack.not_isAlgebraicStack_of_not_essSurj_approximationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/NonAlgebraicHomStack.lean, line 382. The attribute's comment: “the deduction of the tag from Stacks 07X8 and Stacks 0AFB only, and not about the tag's subject: for a category fibred in groupoids over the big fppf site of a locally Noetherian base, 07X8 as the named hypothesis h07X8 together with the failure of essential surjectivity of the comparison functor of Stacks 07X6 for that category give non-algebraicity. The tag's subject, the Hom-stack Mor_S(X, [S/A]), cannot be named — this library defines no Hom-stack of two algebraic stacks — so 0AFC is not asserted of it, and the implication is not instantiated at the example: the 0AFB available in this file is the non-surjectivity of H¹(X, A) → lim H¹(Xₙ, A), and its identification with the failure of essential surjectivity hypothesised here is the source's unformalized computation of the Hom-stack's fibre categories. 07X8 is a hypothesis, not a result of this library”.

Stacks 0AFC, as the deduction the source makes, for a hypothesised subject. Let B be a big fppf site, S a locally Noetherian scheme in it and 𝒳 a category over the big fppf site over S which is fibred in groupoids. Assume Stacks 07X8, as the hypothesis h07X8: every algebraic stack over S has an equivalence for its comparison functor of Stacks 07X6, from objects over a Noetherian complete local base to compatible systems over the infinitesimal thickenings of its closed point. If that comparison functor is not essentially surjective for 𝒳 — which is Stacks 0AFB for the source's 𝒳 = Mor_S(X, [S/A]) — then 𝒳 is not an algebraic stack.

The source's 𝒳 cannot be named here: this library has no Hom-stack of two algebraic stacks. See the module documentation.

public theorem not_isAlgebraicStack_of_not_essSurj_approximationFunctor
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (𝒳 : CategoryTheory.BasedCategory.{v, t} (AlgebraicGeometry.BigFppfOver B S hS))
    (hp : 𝒳.p.IsFiberedInGroupoids)
    (h07X8 : ∀ 𝒴 : CategoryTheory.BasedCategory.{v, t}
        (AlgebraicGeometry.BigFppfOver B S hS),
        AlgebraicGeometry.Stack.IsAlgebraicStack.{u, w} B S hS 𝒴 →
          ∀ hq : 𝒴.p.IsFiberedInGroupoids,
            (Deformation.Artin.approximationFunctor B S hS 𝒴.p hq).IsEquivalence)
    (h0AFB : ¬ (Deformation.Artin.approximationFunctor B S hS 𝒳.p hp).EssSurj) :
    ¬ AlgebraicGeometry.Stack.IsAlgebraicStack.{u, w} B S hS 𝒳

Stacks.Examples.NonAlgebraicHomStack.not_isAlgebraicStack_of_exists_not_isEffective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/NonAlgebraicHomStack.lean, line 414. The attribute's comment: “the deduction of the tag from Stacks 07X8 and Stacks 0AFB only, and not about the tag's subject: for a category fibred in groupoids over the big fppf site of a locally Noetherian base, 07X8 as the named hypothesis h07X8 together with a formal object of that category that is not effective give non-algebraicity. The tag's subject, the Hom-stack Mor_S(X, [S/A]), cannot be named — this library defines no Hom-stack of two algebraic stacks — so 0AFC is not asserted of it, and the implication is not instantiated at the example: the 0AFB available in this file is the non-surjectivity of H¹(X, A) → lim H¹(Xₙ, A), and its identification with the non-effective formal object hypothesised here is the source's unformalized computation of the Hom-stack's fibre categories. 07X8 is a hypothesis, not a result of this library”.

Stacks 0AFC, in the vocabulary of effective formal objects. Under Stacks 07X8 as the hypothesis h07X8, a category fibred in groupoids over the big fppf site of a locally Noetherian base which has a formal object that is not effective, in the sense of Stacks 07X7, is not an algebraic stack. This is the form in which the source's Remark 0AFD diagnoses the example: "the problem is the non-effectivity of formal objects for Mor_S(X, [S/A])".

The source's 𝒳 cannot be named here: this library has no Hom-stack of two algebraic stacks. See the module documentation.

public theorem not_isAlgebraicStack_of_exists_not_isEffective
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (𝒳 : CategoryTheory.BasedCategory.{v, t} (AlgebraicGeometry.BigFppfOver B S hS))
    (hp : 𝒳.p.IsFiberedInGroupoids)
    (h07X8 : ∀ 𝒴 : CategoryTheory.BasedCategory.{v, t}
        (AlgebraicGeometry.BigFppfOver B S hS),
        AlgebraicGeometry.Stack.IsAlgebraicStack.{u, w} B S hS 𝒴 →
          ∀ hq : 𝒴.p.IsFiberedInGroupoids,
            (Deformation.Artin.approximationFunctor B S hS 𝒴.p hq).IsEquivalence)
    (h0AFB : ∃ ξ : Deformation.Artin.FormalObject B S hS 𝒳.p,
      ¬ Deformation.Artin.FormalObject.IsEffective B S hS 𝒳.p hp ξ) :
    ¬ AlgebraicGeometry.Stack.IsAlgebraicStack.{u, w} B S hS 𝒳

Stacks.Examples.NonAlgebraicHomStack.not_isAlgebraicStack_powerSeriesBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/NonAlgebraicHomStack.lean, line 446. The attribute's comment: “the deduction of the tag from Stacks 07X8 and Stacks 0AFB only, over the section's base S = Spec k⟦t⟧ but not about the tag's subject: 07X8 as the named hypothesis h07X8 together with a formal object that is not effective give non-algebraicity. The tag's subject, the Hom-stack Mor_S(X, [S/A]), cannot be named — this library defines no Hom-stack of two algebraic stacks — so 0AFC is not asserted of it, and the implication is not instantiated at the example: the 0AFB available in this file is the non-surjectivity of H¹(X, A) → lim H¹(Xₙ, A), and its identification with the non-effective formal object hypothesised here is the source's unformalized computation of the Hom-stack's fibre categories. 07X8 is a hypothesis, not a result of this library”.

Stacks 0AFC over the section's own base S = Spec k⟦t⟧. Under Stacks 07X8 as the hypothesis h07X8, a category fibred in groupoids over the big fppf site over S which has a formal object that is not effective is not an algebraic stack. Only the base of the source's example is pinned down here; its 𝒳 = Mor_S(X, [S/A]) still cannot be named, so 𝒳 remains a hypothesis. See the module documentation.

public theorem not_isAlgebraicStack_powerSeriesBase
    {k : Type u} [Field k] (B : AlgebraicGeometry.BigFppfSite.{u})
    (hS : B.Contains (base k))
    (𝒳 : CategoryTheory.BasedCategory.{v, t} (AlgebraicGeometry.BigFppfOver B (base k) hS))
    (hp : 𝒳.p.IsFiberedInGroupoids)
    (h07X8 : ∀ 𝒴 : CategoryTheory.BasedCategory.{v, t}
        (AlgebraicGeometry.BigFppfOver B (base k) hS),
        AlgebraicGeometry.Stack.IsAlgebraicStack.{u, w} B (base k) hS 𝒴 →
          ∀ hq : 𝒴.p.IsFiberedInGroupoids,
            (Deformation.Artin.approximationFunctor B (base k) hS 𝒴.p hq).IsEquivalence)
    (h0AFB : ∃ ξ : Deformation.Artin.FormalObject B (base k) hS 𝒳.p,
      ¬ Deformation.Artin.FormalObject.IsEffective B (base k) hS 𝒳.p hp ξ) :
    ¬ AlgebraicGeometry.Stack.IsAlgebraicStack.{u, w} B (base k) hS 𝒳
Tag 0AFD, a remark

Tag 0AFD in the Stacks Project.

Stacks.Examples.NonAlgebraicHomStack.not_forall_isAlgebraicStack_of_isAbsolutelySeparated_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/HomStackSeparatedTargetCriterion.lean, line 124. The attribute's comment: “the mathematical assertion of the remark and not its bibliography: the criterion the Erratum asserts -- that a Hom-stack is algebraic as soon as its target is separated -- is false, because the target [S/A] of the non-algebraic Hom-stack of Stacks 0AFC is separated. Both legs are derived, not hypothesised: separatedness of [S/A] from Stacks 0DTY part (6) read at the groupoid of the trivial action, and non-algebraicity from Stacks 0AFC of StacksFrontier.Examples.Stacks.NonAlgebraicHomStack. NOT carried: the bibliographic claims (that Stacks 0AFC contradicts Theorem 1.1 of AokiHomStacks, and that the criterion is the Erratum's), which are cited in the docstring only. The tag's subject, the Hom-stack Mor_S(Y, Z), cannot be named -- this library defines no Hom-stack of two algebraic stacks -- so the criterion is stated for an arbitrary assignment Mor of a based category to a pair of algebraic stacks, and the source's unformalized identification of the Hom-stack's fibre categories with groupoids of torsors is the hypothesis h0AFB, a non-effective formal object of Mor Y Z. Stacks 07X8 is the hypothesis h07X8 and is not a result of this library; separatedness inherits from Stacks 0DTY, for the source's unqualified (absolute) separatedness, the hypothesis hBase on the algebraic stack of the base scheme”.

Stacks 0AFD, the mathematical assertion the remark makes: the criterion that a Hom-stack is algebraic whenever its target is separated is false.

Let S = Spec k⟦t⟧, let A be a group algebraic space over the terminal algebraic space over S which is proper, flat and locally of finite presentation — the source's abelian scheme — and let 𝒵 be an algebraic stack equivalent over the site to the quotient stack of the trivial action of A, that is to [S/A]. Let Mor be any assignment of a based category over the site to a pair of algebraic stacks over S, let 𝒴 be an algebraic stack and suppose, as the source computes, that Mor 𝒴 𝒵 has a formal object which is not effective. Then, assuming Stacks 07X8, it is not the case that Mor 𝒴' 𝒵' is an algebraic stack for every 𝒴' and every separated 𝒵'.

The two legs are derived: [S/A] is separated by Stacks 0DTY part (6) at the trivial-action groupoid, and Mor 𝒴 𝒵 is not algebraic by Stacks 0AFC of the neighbouring module. See the module documentation.

public theorem not_forall_isAlgebraicStack_of_isAbsolutelySeparated_target
    {k : Type u} [Field k] (B : BigFppfSite.{u}) (hS : B.Contains (base k))
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hBase : Stack.AlgebraicStacks.IsAbsolutelySeparated.{u, w} B (base k) hS hZ
      (Stack.schemeStack.{u, w} B (base k) hS (Over.mk (𝟙 (B.obj hS)))))
    (A : Over (Space.terminalSpace B (base k) hS).obj) [GrpObj A]
    (hA : IsAlgebraicSpace B (base k) hS A.left)
    (Agpd : Space.ActionGroupoidConstruction (Space.terminalSpace B (base k) hS) A
      (𝟙_ (Over (Space.terminalSpace B (base k) hS).obj)) hA
      (Space.terminalSpace B (base k) hS).property)
    (𝒵 : Stack.AlgebraicStacks.{u, w} B (base k) hS)
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (Stack.quotientStack Agpd.groupoid).p 𝒵.val.val.p))
    (hproper : Space.IsProper B (base k) hS A.hom)
    (hflat : Space.IsFlat B (base k) hS A.hom)
    (hlfp : Space.IsLocallyOfFinitePresentation B (base k) hS A.hom)
    (Mor : Stack.AlgebraicStacks.{u, w} B (base k) hS →
      Stack.AlgebraicStacks.{u, w} B (base k) hS →
      BasedCategory.{v, t} (BigFppfOver B (base k) hS))
    (𝒴 : Stack.AlgebraicStacks.{u, w} B (base k) hS)
    (hp : (Mor 𝒴 𝒵).p.IsFiberedInGroupoids)
    (h07X8 : ∀ 𝒲 : BasedCategory.{v, t} (BigFppfOver B (base k) hS),
        Stack.IsAlgebraicStack.{u, w} B (base k) hS 𝒲 →
          ∀ hq : 𝒲.p.IsFiberedInGroupoids,
            (Deformation.Artin.approximationFunctor B (base k) hS 𝒲.p hq).IsEquivalence)
    (h0AFB : ∃ ξ : Deformation.Artin.FormalObject B (base k) hS (Mor 𝒴 𝒵).p,
      ¬ Deformation.Artin.FormalObject.IsEffective B (base k) hS (Mor 𝒴 𝒵).p hp ξ) :
    ¬ ∀ 𝒴' 𝒵' : Stack.AlgebraicStacks.{u, w} B (base k) hS,
        Stack.AlgebraicStacks.IsAbsolutelySeparated.{u, w} B (base k) hS hZ 𝒵' →
          Stack.IsAlgebraicStack.{u, w} B (base k) hS (Mor 𝒴' 𝒵')
Sources
LeanAlgebraicGeometry.fppfH1_restriction_genericPoint_injective · AlgebraicGeometry.injective_torsorSectionsRestrictGenericPoint · AlgebraicGeometry.fppfH1_restriction_genericPoint_injective_of_isTrivial · AlgebraicGeometry.Space.fppfH1_isAddTorsion · Stacks.Examples.NonAlgebraicHomStack.exists_compatible_ne_restrictTotal · Stacks.Examples.NonAlgebraicHomStack.not_surjective_toCompatibleSystems · Stacks.Examples.NonAlgebraicHomStack.not_isAlgebraicStack_of_not_essSurj_approximationFunctor · Stacks.Examples.NonAlgebraicHomStack.not_isAlgebraicStack_of_exists_not_isEffective

Section110.75 An algebraic stack not satisfying strong formal effectiveness#

Section 110.75 of the Stacks Project, Tag 0CXW. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CXX, a lemma

Tag 0CXX in the Stacks Project.

Deformation.Artin.exists_nonEffectiveSystem_quotientStack_trivialAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/NonEffectiveSystem.lean, line 335. The attribute's comment: “RESTRICTED: Tag 0AFB (lifting an object along a thickening) is the hypothesis h0AFB, Tags 0AF9 and 0AFA (finite order of the class over the limit) are h0AF9, the non-torsion rational point of the abelian variety with Tag 0AEN is ξ₀ with hnontorsion, and the class of a torsor is the data H, cls, hcls; the site realization is U, cU, e, eL, he, heL, hchart”.

Stacks Project, Tag 0CXX. Let k be an algebraically closed field which is not the algebraic closure of a finite field, let A be an abelian variety over k and let 𝒳 = [Spec(k)/A]. There is an inverse system of k-algebras whose transition maps are surjective with locally nilpotent kernels — the thickenings of the triangle of three affine lines — and a system of objects of 𝒳 over the spectra of its levels, which is not effective in the sense of Tag 0CXT.

The mathematical inputs the library does not have are hypotheses: h0AFB is the lifting of an object along a nilpotent thickening of the triangle, the method of Tag 0AFB; h0AF9 is the finiteness of the order of the class of every object over the limit, Tag 0AF9 together with Tag 0AFA; ξ₀ together with hnontorsion is the object over the reduced triangle whose class has infinite order, which the source builds from a non-torsion rational point of A and Tag 0AEN; H, cls and hcls are the first cohomology class of an object of 𝒳, that is, the description of the fibre categories of a classifying stack as groupoids of torsors; and U, cU, e, eL, he, heL, hchart realize the spectra of the levels of the inverse system and of its limit as objects of the chosen big fppf site. Non-effectivity is nowhere assumed, and the system of objects is constructed rather than supposed.

public theorem exists_nonEffectiveSystem_quotientStack_trivialAction
    [IsAlgClosed k]
    (_hkinf : ∀ F : Subfield k, Finite F → ¬ Algebra.IsAlgebraic F k)
    (U : ℕ ⥤ fppfOverField k C hk) (cU : Cocone U)
    (cR : Cone (triangleThickenings k)) (hcR : IsLimit cR)
    (e : ∀ n : ℕ, (schemeOverField k C hk).obj (U.obj n) ≅
      Spec (.of ((triangleThickenings k).obj (.op n))))
    (eL : (schemeOverField k C hk).obj cU.pt ≅ Spec (.of cR.pt))
    (he : ∀ {i j : ℕ} (g : i ⟶ j), (schemeOverField k C hk).map (U.map g) ≫ (e j).hom =
      (e i).hom ≫ Scheme.Spec.map
        (CommRingCat.ofHom ((triangleThickenings k).map g.op).hom.toRingHom).op)
    (heL : ∀ n : ℕ, (schemeOverField k C hk).map (cU.ι.app n) ≫ eL.hom =
      (e n).hom ≫ Scheme.Spec.map
        (CommRingCat.ofHom (cR.π.app (.op n)).hom.toRingHom).op)
    (hchart : eL.inv ≫ C.inclusion.map cU.pt.hom =
      Scheme.Spec.map (CommRingCat.ofHom (algebraMap k cR.pt)).op)
    (H : (fppfOverField k C hk)ᵒᵖ ⥤ AddCommGrpCat.{u})
    (cls : (x : (Stack.quotientStack Q.groupoid).obj) →
      H.obj (.op ((Stack.quotientStack Q.groupoid).p.obj x)))
    (hcls : ∀ {x y : (Stack.quotientStack Q.groupoid).obj} (φ : x ⟶ y),
      cls x = H.map ((Stack.quotientStack Q.groupoid).p.map φ).op (cls y))
    (ξ₀ : (Stack.quotientStack Q.groupoid).obj)
    (hξ₀ : (Stack.quotientStack Q.groupoid).p.obj ξ₀ ≅ U.obj 0)
    (hnontorsion : ¬ IsOfFinAddOrder (cls ξ₀))
    (h0AF9 : ∀ x : (Stack.quotientStack Q.groupoid).obj,
      (Stack.quotientStack Q.groupoid).p.obj x = cU.pt → IsOfFinAddOrder (cls x))
    (h0AFB : ∀ (n : ℕ) (x : (Stack.quotientStack Q.groupoid).obj)
      (a : (Stack.quotientStack Q.groupoid).p.obj x ≅ U.obj n),
      ∃ (y : (Stack.quotientStack Q.groupoid).obj)
        (b : (Stack.quotientStack Q.groupoid).p.obj y ≅ U.obj (n + 1))
        (φ : x ⟶ y), (Stack.quotientStack Q.groupoid).p.map φ ≫ b.hom =
          a.hom ≫ U.map (homOfLE (Nat.le_succ n))) :
    ∃ (R : ℕᵒᵖ ⥤ CommAlgCat.{u} k) (cS : Cone R)
      (ξ : ℕ ⥤ (Stack.quotientStack Q.groupoid).obj)
      (c : Cocone (ξ ⋙ (Stack.quotientStack Q.groupoid).p))
      (f : ∀ n : ℕ, (schemeOverField k C hk).obj
        ((ξ ⋙ (Stack.quotientStack Q.groupoid).p).obj n) ≅ Spec (.of (R.obj (.op n))))
      (fL : (schemeOverField k C hk).obj c.pt ≅ Spec (.of cS.pt)),
      Nonempty (IsLimit cS) ∧
      (∀ {i j : ℕᵒᵖ} (g : i ⟶ j), Function.Surjective (R.map g).hom) ∧
      (∀ {i j : ℕᵒᵖ} (g : i ⟶ j),
        (RingHom.ker (R.map g).hom.toRingHom).LocallyNilpotent) ∧
      (∀ {i j : ℕ} (g : i ⟶ j), (schemeOverField k C hk).map
          ((ξ ⋙ (Stack.quotientStack Q.groupoid).p).map g) ≫ (f j).hom =
        (f i).hom ≫ Scheme.Spec.map (CommRingCat.ofHom (R.map g.op).hom.toRingHom).op) ∧
      (∀ n : ℕ, (schemeOverField k C hk).map (c.ι.app n) ≫ fL.hom =
        (f n).hom ≫ Scheme.Spec.map (CommRingCat.ofHom (cS.π.app (.op n)).hom.toRingHom).op) ∧
      (fL.inv ≫ C.inclusion.map c.pt.hom =
        Scheme.Spec.map (CommRingCat.ofHom (algebraMap k cS.pt)).op) ∧
      ¬ IsEffectiveSystem (Stack.quotientStack Q.groupoid).p ξ c
Sources
LeanDeformation.Artin.exists_nonEffectiveSystem_quotientStack_trivialAction

Section110.77 Affine formal algebraic spaces#

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

Tag 0CBC, a lemma

Tag 0CBC in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isAffineFormalAlgebraicSpace_not_hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NotMcQuillanExample.lean, line 56.

Stacks 0CBC. There exists an affine formal algebraic space which is not McQuillan: the example of Stacks 0CBD admits no presentation by affine thickenings whose section-ring projections are all surjective.

public theorem exists_isAffineFormalAlgebraicSpace_not_hasSomeSurjectivePresentation :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (X : FppfSheaf B S hS),
      IsAffineFormalAlgebraicSpace B S hS X ∧ ¬ HasSomeSurjectivePresentation B S hS X
Tag 0CBD, a lemma

Tag 0CBD in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isAffineFormalAlgebraicSpace_sections_isField_reduction_infinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SectionsDoNotSeparatePoints.lean, line 840.

Stacks 0CBD. There is an affine formal algebraic space whose regular functions do not separate points: writing X = colim X_λ as in Stacks 0AI7, the inverse limit of the rings Γ(X_λ, O_{X_λ}) is a field, while the reduction of X has infinitely many points. The reduction is exhibited as a reduced affine scheme T of the site together with a representable thickening T ⟶ X through which every morphism to X from a reduced algebraic space factors uniquely, which determines it up to unique isomorphism.

public theorem exists_isAffineFormalAlgebraicSpace_sections_isField_reduction_infinite :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (X : FppfSheaf B S hS),
      IsAffineFormalAlgebraicSpace B S hS X ∧
      (∃ (I : Type (u + 1)) (pre : Preorder I),
        letI : Preorder I := pre
        Nonempty I ∧ IsDirected I (· ≤ ·) ∧
          ∃ D : I ⥤ BigAffineFppf B S hS,
            (∀ ⦃i j : I⦄ (f : i ⟶ j),
              Stacks.Thickenings.IsThickening
                ((BigAffineFppf.toScheme B S hS).map (D.map f))) ∧
            Nonempty (X ≅ colimit
              (D ⋙ BigAffineFppf.inclusion B S hS ⋙
                Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))) ∧
            (letI : CommRing (sectionDiagram B S hS D ⋙ forget CommRingCat.{u}).sections :=
              @Subring.toCommRing (∀ j, (sectionDiagram B S hS D).obj j) _
                (RingCat.sectionsSubring
                  (sectionDiagram B S hS D ⋙ forget₂ CommRingCat RingCat.{u}))
            IsField (sectionDiagram B S hS D ⋙ forget CommRingCat.{u}).sections)) ∧
      (∃ T : BigFppfOver B S hS,
        IsReduced ((BigFppfOver.toScheme B S hS).obj T) ∧
        Infinite ((BigFppfOver.toScheme B S hS).obj T) ∧
        ∃ ι : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj T ⟶ X,
          (MorphismProperty.relative
            (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
            (MorphismProperty.inverseImage
              (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
              (BigFppfOver.toScheme B S hS))) ι ∧
          ∀ U : FppfSheaf B S hS, Space.IsAlgebraicSpaceULift.{u + 1} B S hS U.obj →
            (∃ (V : BigFppfOver B S hS) (p : (uliftYoneda.{u + 1}).obj V ⟶ U.obj),
              (MorphismProperty.relative (uliftYoneda.{u + 1})
                (MorphismProperty.inverseImage
                  (@Surjective.{u} : MorphismProperty Scheme.{u})
                  (BigFppfOver.toScheme B S hS))) p ∧
              (MorphismProperty.relative (uliftYoneda.{u + 1})
                (MorphismProperty.inverseImage
                  (@Etale.{u} : MorphismProperty Scheme.{u})
                  (BigFppfOver.toScheme B S hS))) p ∧
              IsReduced ((BigFppfOver.toScheme B S hS).obj V)) →
            ∀ g : U ⟶ X, ∃! l : U ⟶
              (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj T, l ≫ ι = g)
Tag 0CBE, a lemma

Tag 0CBE in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_representable_hasSomeSurjectivePresentation_not, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableOverMcQuillan.lean, line 635.

There exists a representable morphism f : X ⟶ Y of affine formal algebraic spaces with Y McQuillan, but X not McQuillan. The morphism is representable by schemes, and every represented base change of it is moreover an affine morphism of schemes.

theorem exists_representable_hasSomeSurjectivePresentation_not :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (inS : B.Contains S) (X Y : FppfSheaf B S inS)
      (f : X ⟶ Y),
      IsAffineFormalAlgebraicSpace B S inS X ∧ IsAffineFormalAlgebraicSpace B S inS Y ∧
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S inS)).relativelyRepresentable f ∧
      (MorphismProperty.inverseImage (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S inS)).relative
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S inS)) f ∧
      HasSomeSurjectivePresentation B S inS Y ∧ ¬ HasSomeSurjectivePresentation B S inS X
Sources
LeanAlgebraicGeometry.FormalSpace.exists_isAffineFormalAlgebraicSpace_not_hasSomeSurjectivePresentation · AlgebraicGeometry.FormalSpace.exists_isAffineFormalAlgebraicSpace_sections_isField_reduction_infinite · AlgebraicGeometry.FormalSpace.exists_representable_hasSomeSurjectivePresentation_not

Section110.78 Flat maps are not directed limits of finitely presented flat maps#

Section 110.78 of the Stacks Project, Tag 0ATE. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ATF, a lemma

Tag 0ATF in the Stacks Project.

Stacks.Examples.exists_flat_algebra_not_filteredColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/FlatAlgebraNotFilteredColimitAlternatives.lean, line 43.

There is a commutative ring with a flat algebra which is the colimit of no filtered diagram of finitely presented flat algebras; the ring may be chosen to be a finite type algebra over 𝔽_p for a prime p, or a one-dimensional Noetherian local ring whose residue field has characteristic zero.

theorem exists_flat_algebra_not_filteredColimit :
    (∃ (A : CommRingCat.{max u v}) (B : CommAlgCat.{max u v} A), Module.Flat A B ∧
      ∀ (J : Type v) [SmallCategory J] [IsFiltered J] (F : J ⥤ CommAlgCat.{max u v} A),
        (∀ j, Algebra.FinitePresentation A (F.obj j) ∧ Module.Flat A (F.obj j)) →
          ∀ c : Cocone F, c.pt = B → IsEmpty (IsColimit c)) ∧
    (∃ p : ℕ, p.Prime ∧ ∃ (A : CommRingCat.{max u v}) (_ : Algebra (ZMod p) A),
      Algebra.FiniteType (ZMod p) A ∧ ∃ B : CommAlgCat.{max u v} A, Module.Flat A B ∧
        ∀ (J : Type v) [SmallCategory J] [IsFiltered J] (F : J ⥤ CommAlgCat.{max u v} A),
          (∀ j, Algebra.FinitePresentation A (F.obj j) ∧ Module.Flat A (F.obj j)) →
            ∀ c : Cocone F, c.pt = B → IsEmpty (IsColimit c)) ∧
    (∃ A : CommRingCat.{max u v}, ∃ hloc : IsLocalRing A,
      letI : IsLocalRing A := hloc
      IsNoetherianRing A ∧ ringKrullDim A = 1 ∧
        CharZero (IsLocalRing.ResidueField A) ∧
          ∃ B : CommAlgCat.{max u v} A, Module.Flat A B ∧
            ∀ (J : Type v) [SmallCategory J] [IsFiltered J]
              (F : J ⥤ CommAlgCat.{max u v} A),
              (∀ j, Algebra.FinitePresentation A (F.obj j) ∧
                Module.Flat A (F.obj j)) →
                ∀ c : Cocone F, c.pt = B → IsEmpty (IsColimit c))
Sources
LeanStacks.Examples.exists_flat_algebra_not_filteredColimit

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.