110.4 Non-quasi-compact inverse… to 110.32 A noninvertible ideal…

Section110.4 Non-quasi-compact inverse limit of quasi-compact spaces#

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

Tag 09ZK, a lemma

Tag 09ZK in the Stacks Project.

Stacks.Examples.exists_inverse_system_isCompact_not_isCompact_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/NonQuasiCompactInverseLimit.lean, line 94.

Stacks 09ZK. There is an inverse system of quasi-compact topological spaces over the natural numbers whose limit is not quasi-compact.

theorem exists_inverse_system_isCompact_not_isCompact_limit :
    ∃ F : ℕᵒᵖ ⥤ TopCat.{0},
      (∀ n, IsCompact (Set.univ : Set (F.obj n))) ∧
        ¬ IsCompact (Set.univ : Set ↑(limit F : TopCat.{0}))

Sources

• Section 110.4, Tag 09ZJ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_inverse_system_isCompact_not_isCompact_limit

Section110.7 Noncomplete completion#

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

Tag 05JC, a lemma

Tag 05JC in the Stacks Project.

Stacks.Examples.CountableVarLocalization.exists_isLocalRing_adicCompletion_not_complete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompletionPathologies.lean, line 43.

Stacks 05JC. There exists a local ring R and a maximal ideal m of it such that the m-adic completion R ^∧ of R is local with maximal ideal different from m R ^∧, is not complete for its own maximal ideal, and is not m-adically complete as an R-module.

theorem exists_isLocalRing_adicCompletion_not_complete :
    ∃ (R : Type) (_ : CommRing R) (_ : IsLocalRing R) (m : Ideal R), m.IsMaximal ∧
      ∃ _ : IsLocalRing (AdicCompletion m R),
        IsLocalRing.maximalIdeal (AdicCompletion m R) ≠ m.map (AdicCompletion.of m R) ∧
        ¬ IsAdicComplete (IsLocalRing.maximalIdeal (AdicCompletion m R))
            (AdicCompletion m R) ∧
        ¬ IsAdicComplete m (AdicCompletion m R)

Sources

• Section 110.7, Tag 05JA
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.CountableVarLocalization.exists_isLocalRing_adicCompletion_not_complete

Section110.8 Noncomplete quotient#

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

Tag 05JE, a lemma

Tag 05JE in the Stacks Project.

Stacks.Examples.exists_complete_principal_ideal_not_complete_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/NoncompleteQuotient.lean, line 421.

Stacks 05JE. A quotient by a principal ideal of a ring complete for another principal ideal need not be complete for the induced ideal.

theorem exists_complete_principal_ideal_not_complete_quotient :
    ∃ (R : Type u) (_ : CommRing R) (I J : Ideal R),
      I.IsPrincipal ∧ J.IsPrincipal ∧ IsAdicComplete I R ∧
        ¬ IsAdicComplete (I.map (Ideal.Quotient.mk J)) (R ⧸ J)

Sources

• Section 110.8, Tag 05JD
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_complete_principal_ideal_not_complete_quotient

Section110.9 Completion is not exact#

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

Tag 05JG, a lemma

Tag 05JG in the Stacks Project.

Stacks.Examples.exists_not_left_exact_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompletionNotExact.lean, line 99. The attribute's comment: “failure of left exactness”.

Stacks 05JG. Adic completion need not preserve the exactness of a short exact sequence at its middle term, so it is not left exact in general.

theorem exists_not_left_exact_adicCompletion :
    ∃ (R : Type u) (_ : CommRing R) (I J : Ideal R),
      I.IsPrincipal ∧ J.IsPrincipal ∧
        Function.Exact (Submodule.subtype (J : Submodule R R))
          (Submodule.mkQ (J : Submodule R R)) ∧
        ¬ Function.Exact
          (AdicCompletion.map I (Submodule.subtype (J : Submodule R R)))
          (AdicCompletion.map I (Submodule.mkQ (J : Submodule R R)))

Stacks.Examples.exists_not_right_exact_adicCompletion_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompletionNotExact.lean, line 152. The attribute's comment: “failure of right exactness on finitely presented modules”.

Stacks 05JG. Completion is not right exact even on finitely presented modules over a ring, with a principal ideal of definition.

theorem exists_not_right_exact_adicCompletion_finitePresentation :
    ∃ (R : Type u) (_ : CommRing R) (I : Ideal R) (f : R),
      I.IsPrincipal ∧
        Module.FinitePresentation R (R ⧸ (Ideal.span {f} : Submodule R R)) ∧
        Function.Exact (LinearMap.mulLeft R f)
          (Submodule.mkQ (Ideal.span {f} : Submodule R R)) ∧
        ¬ Function.Exact
          (AdicCompletion.map I (LinearMap.mulLeft R f))
          (AdicCompletion.map I (Submodule.mkQ (Ideal.span {f} : Submodule R R)))

Sources

• Section 110.9, Tag 05JF
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_not_left_exact_adicCompletion · Stacks.Examples.exists_not_right_exact_adicCompletion_finitePresentation

Section110.10 The category of complete modules is not abelian#

Section 110.10 of the Stacks Project, Tag 07JQ. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07JR, a lemma

Tag 07JR in the Stacks Project.

Stacks.Examples.hasKernels_iAdicallyCompleteModuleCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompleteModuleCategory.lean, line 155. The attribute's comment: “kernels”.

Stacks 07JR. If I is a finitely generated ideal of R, then the category of I-adically complete R-modules has kernels.

theorem hasKernels_iAdicallyCompleteModuleCat
    (R : Type u) [CommRing R] (I : Ideal R) (hI : I.FG) :
    HasKernels (IAdicallyCompleteModuleCat.{v} R I)

Stacks.Examples.hasCokernels_iAdicallyCompleteModuleCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompleteModuleCategory.lean, line 242. The attribute's comment: “cokernels”.

Stacks 07JR. If I is a finitely generated ideal of R, then the category of I-adically complete R-modules has cokernels.

theorem hasCokernels_iAdicallyCompleteModuleCat
    (R : Type u) [CommRing R] (I : Ideal R) (hI : I.FG) :
    HasCokernels (IAdicallyCompleteModuleCat.{v} R I)

Stacks.Examples.not_abelian_iAdicallyCompleteModuleCat_of_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompleteModulesNotAbelian.lean, line 117. The attribute's comment: “not_abelian, for a named ring and a named principal ideal”.

If R is a Noetherian ring without zero divisors which is complete for a principal ideal I = (π) whose generator is neither zero nor a unit, and E : Type v is an R-module with a linear equivalence E ≃ₗ[R] R, then the category of I-adically complete R-modules in Type v is not abelian.

theorem not_abelian_iAdicallyCompleteModuleCat_of_principal
    (R : Type u) [CommRing R] [IsNoetherianRing R] [NoZeroDivisors R]
    (I : Ideal R) (hR : IsAdicComplete I R) (π : R) (hIspan : I = Ideal.span {π})
    (hπ : π ≠ 0) (hπnonunit : ¬ IsUnit π)
    (E : Type v) [AddCommGroup E] [Module R E] (eER : E ≃ₗ[R] R) :
    ¬ Nonempty (Abelian (IAdicallyCompleteModuleCat.{v} R I))

Stacks.Examples.exists_not_abelian_iAdicallyCompleteModuleCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/CompleteModulesNotAbelian.lean, line 319. The attribute's comment: “not_abelian”.

There is a commutative ring with a finitely generated ideal for which the category of adically complete modules is not abelian.

theorem exists_not_abelian_iAdicallyCompleteModuleCat :
    ∃ (R : Type u) (_ : CommRing R) (I : Ideal R),
      I.FG ∧ ¬ Nonempty (Abelian (IAdicallyCompleteModuleCat.{v} R I))

Sources

• Section 110.10, Tag 07JQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.hasKernels_iAdicallyCompleteModuleCat · Stacks.Examples.hasCokernels_iAdicallyCompleteModuleCat · Stacks.Examples.not_abelian_iAdicallyCompleteModuleCat_of_principal · Stacks.Examples.exists_not_abelian_iAdicallyCompleteModuleCat

Section110.11 The category of derived complete modules#

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

Tag 0ARD, a lemma

Tag 0ARD in the Stacks Project.

Stacks.Examples.derivedCompleteModules_abelian_exact_colimits_not_grothendieck, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Completion/DerivedCompleteModules.lean, line 325.

Stacks 0ARD. Let A be a ring and I ⊂ A an ideal. The category C of derived complete A-modules is abelian, and the inclusion F : C ⥤ ModuleCat A is exact and preserves all limits. If I is finitely generated, then C has all direct sums and all colimits.

These are not preserved by F in general, and filtered colimits in C are not exact in general, so that C is not a Grothendieck abelian category: all of this fails for A = ℤ_[2] and I = (2), where F does not preserve countable direct sums or colimits, sequential colimits in C are not exact, C does not satisfy AB5, and no abelian structure on C is Grothendieck.

theorem derivedCompleteModules_abelian_exact_colimits_not_grothendieck :
    (∀ (A : Type u) [CommRing A] (I : Ideal A),
      letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
        Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
      let P : ObjectProperty (ModuleCat.{u} A) := fun M => IsDerivedCompleteModule I M
      let C := P.FullSubcategory
      let F : C ⥤ ModuleCat.{u} A := P.ι
      Nonempty (Abelian C) ∧ PreservesFiniteLimits F ∧ PreservesFiniteColimits F ∧
        HasLimits C ∧ PreservesLimits F ∧
        (I.FG → HasCoproducts.{u} C ∧ HasColimits C)) ∧
    (letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat (ℤ_[2]))) :=
        Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
      let I : Ideal ℤ_[2] := Ideal.span {2}
      let P : ObjectProperty (ModuleCat (ℤ_[2])) := fun M => IsDerivedCompleteModule I M
      let C := P.FullSubcategory
      let F : C ⥤ ModuleCat (ℤ_[2]) := P.ι
      I.FG ∧ ¬ PreservesColimitsOfShape (Discrete ℕ) F ∧ ¬ PreservesColimits F ∧
        (∃ _ : HasColimitsOfShape ℕ C, ¬ HasExactColimitsOfShape ℕ C) ∧
        (∃ _ : HasFilteredColimits C, ¬ AB5 C) ∧
        ∀ [Abelian C], ¬ IsGrothendieckAbelian C)

Sources

• Section 110.11, Tag 0ARC
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.derivedCompleteModules_abelian_exact_colimits_not_grothendieck

Section110.12 Nonflat completions#

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

Tag 0AL9, a lemma

Tag 0AL9 in the Stacks Project.

Stacks.Examples.finite_iff_piScalarRightHom_nat_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/CountableCoherent.lean, line 69.

A countable module is finitely generated if and only if the canonical map M ⊗[R] (ℕ → R) → (ℕ → M) is surjective.

theorem finite_iff_piScalarRightHom_nat_surjective :
    Module.Finite R M ↔
      Function.Surjective (TensorProduct.piScalarRightHom R R M ℕ)

Tag 0ALA, a lemma

Tag 0ALA in the Stacks Project.

Stacks.Examples.finitePresentation_iff_piScalarRightHom_nat_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/CountableCoherent.lean, line 105.

A countable module over a countable ring is finitely presented if and only if the canonical map M ⊗[R] (ℕ → R) → (ℕ → M) is bijective.

theorem finitePresentation_iff_piScalarRightHom_nat_bijective :
    Module.FinitePresentation R M ↔
      Function.Bijective (TensorProduct.piScalarRightHom R R M ℕ)

Tag 0ALB, a lemma

Tag 0ALB in the Stacks Project.

Stacks.Examples.isCoherentRing_iff_flat_pi_nat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/CountableCoherent.lean, line 168.

A countable commutative ring is coherent if and only if its countable product, as a module over itself, is flat.

theorem isCoherentRing_iff_flat_pi_nat (R : Type u) [CommRing R] [Countable R] :
    IsCoherentRing R ↔ Module.Flat R (ℕ → R)

Tag 0ALC, a lemma

Tag 0ALC in the Stacks Project.

Stacks.Examples.exists_powerSeries_not_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/PowerSeriesNotFlat.lean, line 116.

For some commutative ring, its formal power series ring is flat over neither the coefficient ring nor the polynomial ring.

theorem exists_powerSeries_not_flat :
    ∃ (R : Type u) (hR : CommRing R),
      letI : CommRing R := hR
      (¬ Module.Flat R (PowerSeries R)) ∧
        (¬ Module.Flat (Polynomial R) (PowerSeries R))

Tag 0F1Y, a lemma

Tag 0F1Y in the Stacks Project.

Stacks.Examples.normal_iff_isCompletelyNormal_of_powerSeries_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/CompletelyNormalOfPowerSeriesFlat.lean, line 271.

A domain whose power series ring is flat over its polynomial ring is normal if and only if it is completely normal.

theorem normal_iff_isCompletelyNormal_of_powerSeries_flat
    (R : Type*) [CommRing R] [IsDomain R]
    (hflat : Module.Flat (Polynomial R) (PowerSeries R)) :
    IsIntegrallyClosed R ↔ IsCompletelyNormal R

Tag 0F1Z, a lemma

Tag 0F1Z in the Stacks Project.

Stacks.Examples.instFlatPowerSeriesOfValuationRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/PowerSeriesOverValuationRing.lean, line 63. The attribute's comment: “flat over the coefficient ring”.

The power series ring over a valuation ring is flat over its coefficient ring.

instance instFlatPowerSeriesOfValuationRing (R : Type*) [CommRing R] [IsDomain R]
    [ValuationRing R] : Module.Flat R (PowerSeries R)

Stacks.Examples.not_flat_powerSeries_over_polynomial_of_dim_gt_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/PowerSeriesOverValuationRing.lean, line 130. The attribute's comment: “not flat over the polynomial ring”.

In dimension greater than one, the power series ring over a valuation ring is not flat over its polynomial ring.

theorem not_flat_powerSeries_over_polynomial_of_dim_gt_one (R : Type*)
    [CommRing R] [IsDomain R] [ValuationRing R] (hdim : 1 < ringKrullDim R) :
    ¬ Module.Flat (Polynomial R) (PowerSeries R)

Tag 0ALD, an equation

Tag 0ALD in the Stacks Project.

Stacks.Examples.not_flat_powerSeries_map_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/PowerSeriesLocalizationNotFlat.lean, line 957.

The coefficientwise localization map from the power series ring of k[y, z, aᵢ]/(y aᵢ, aᵢ aⱼ) to the power series ring of its localization at z is not flat.

theorem not_flat_powerSeries_map_localizationAway
    (k : Type u) [Field k] :
    ¬ (PowerSeries.map
      (algebraMap (nonflatPowerSeriesRing k)
        (Localization.Away (nonflatPowerSeriesElement k)))).Flat

Tag 0ALE, a lemma

Tag 0ALE in the Stacks Project.

Stacks.Examples.exists_nonflat_completed_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/CompletedLocalizationNotFlat.lean, line 384.

There is a ring complete for a principal ideal whose completed principal localization is not flat over the ring.

theorem exists_nonflat_completed_localization :
    ∃ (A : Type*) (_ : CommRing A) (x f : A),
      IsAdicComplete (Ideal.span {x}) A ∧
        ¬ Module.Flat A
          (AdicCompletion
            ((Ideal.span {x}).map (algebraMap A (Localization.Away f)))
            (Localization.Away f))

Sources

• Section 110.12, Tag 0AL8
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.finite_iff_piScalarRightHom_nat_surjective · Stacks.Examples.finitePresentation_iff_piScalarRightHom_nat_bijective · Stacks.Examples.isCoherentRing_iff_flat_pi_nat · Stacks.Examples.exists_powerSeries_not_flat · Stacks.Examples.normal_iff_isCompletelyNormal_of_powerSeries_flat · Stacks.Examples.instFlatPowerSeriesOfValuationRing · Stacks.Examples.not_flat_powerSeries_over_polynomial_of_dim_gt_one · Stacks.Examples.not_flat_powerSeries_map_localizationAway

Section110.13 Nonabelian category of quasi-coherent modules#

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

Tag 0ALG, a lemma

Tag 0ALG in the Stacks Project.

AlgebraicGeometry.FormalSpace.not_nonempty_abelian_quasicoherentModules_padicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionQuasicoherentNotAbelian.lean, line 142. The attribute's comment: “the source's example Spf(ℤ_p), for every prime p”.

Stacks 0ALG, the source's example. For a prime p, the formal spectrum X = Spf(ℤ_p) over Spec ℤ is a Noetherian affine formal algebraic space whose category of quasi-coherent modules (Stacks 06WG) admits no abelian structure: by Examples, Section 0ALF, it is the category of p-adically complete abelian groups, which is not abelian (Stacks 07JR).

theorem not_nonempty_abelian_quasicoherentModules_padicCompletion (B : BigFppfSite.{u})
    (hZ : B.Contains (Spec (.of (ULift.{u} ℤ)))) (hZp : B.Contains (Spec (.of (ULift.{u} ℤ_[p])))) :
    IsAffineFormalAlgebraicSpace B _ hZ (padicCompletion p B hZ hZp) ∧
      IsNoetherian B _ hZ (padicCompletion p B hZ hZp) ∧
      ¬ Nonempty (Abelian (FibredSite.quasicoherentModules.{u, u + 1, u + 1, u} B _ hZ
        (completionFibred B _ hZ (specULiftZIsTerminal.from _) hZp
          (Ideal.span {(p : ULift.{u} ℤ_[p])})).p
        (isFiberedInGroupoids_completionFibred B _ hZ _ hZp _)))

AlgebraicGeometry.FormalSpace.exists_isNoetherian_not_nonempty_abelian_quasicoherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionQuasicoherentNotAbelian.lean, line 164.

Stacks 0ALG. The category of quasi-coherent modules on a formal algebraic space is not abelian in general, even for a Noetherian affine formal algebraic space: there is a big fppf site with a base scheme and a Noetherian affine formal algebraic space X over it — Spf(ℤ_2) over Spec ℤ — whose category of quasi-coherent modules (Stacks 06WG, on the category fibred in groupoids of X) admits no abelian structure.

theorem exists_isNoetherian_not_nonempty_abelian_quasicoherentModules :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (X : FppfSheaf B S hS),
      IsAffineFormalAlgebraicSpace B S hS X ∧ IsNoetherian B S hS X ∧
      ¬ Nonempty (Abelian (FibredSite.quasicoherentModules.{u, u + 1, u + 1, u} B S hS
        (presheafOfGroupoids (X.obj ⋙ typeToGrpd)).p
        (isFiberedInGroupoids_presheafOfGroupoids _)))

Sources

• Section 110.13, Tag 0ALF
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FormalSpace.not_nonempty_abelian_quasicoherentModules_padicCompletion · AlgebraicGeometry.FormalSpace.exists_isNoetherian_not_nonempty_abelian_quasicoherentModules

Section110.14 Nonsplit locally split sequence#

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

Tag 0H7G, a lemma

Tag 0H7G in the Stacks Project.

Stacks.Examples.exists_nonsplit_shortExact_locally_split, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/NonsplitLocallySplit.lean, line 329.

A short exact sequence of integer modules that is nonsplit but splits Zariski locally.

theorem exists_nonsplit_shortExact_locally_split.{u} :
    ∃ S : ShortComplex (ModuleCat.{u} ℤ),
      S.ShortExact ∧
        (¬ Nonempty S.Splitting) ∧
        ∀ p : PrimeSpectrum ℤ,
          ∃ f : ℤ, f ∉ p.asIdeal ∧
            Nonempty
              ((S.map (ModuleCat.localizedModuleFunctor.{u} (Submonoid.powers f))).Splitting)

Sources

• Section 110.14, Tag 0H7F
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_nonsplit_shortExact_locally_split

Section110.15 Regular sequences and base change#

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

Tag 0640, a lemma

Tag 0640 in the Stacks Project.

Stacks.Examples.exists_regularSequence_with_common_annihilator_mod_last, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/StrangeRegularSequence.lean, line 921.

A regular sequence in a local ring can have its first two terms annihilate a common nonzero element modulo its last term.

theorem exists_regularSequence_with_common_annihilator_mod_last :
    ∃ (R : Type u) (_ : CommRing R) (_ : IsLocalRing R) (x y z : R),
      x ∈ maximalIdeal R ∧ y ∈ maximalIdeal R ∧ z ∈ maximalIdeal R ∧
        RingTheory.Sequence.IsRegular R [x, y, z] ∧
        ∃ δ : R ⧸ Ideal.span {z},
          δ ≠ 0 ∧
            (Ideal.Quotient.mk (Ideal.span {z}) x) * δ = 0 ∧
            (Ideal.Quotient.mk (Ideal.span {z}) y) * δ = 0

Tag 0641, a lemma

Tag 0641 in the Stacks Project.

Stacks.Examples.exists_regular_sequence_flat_quotient_not_koszulRegular_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/RegularSequenceClosedFibre.lean, line 65.

A regular sequence in a local ring can give a flat quotient over a local base while its closed-fiber sequence fails even Koszul regularity.

theorem exists_regular_sequence_flat_quotient_not_koszulRegular_fiber :
    ∃ (A : Type u) (B : Type v) (_ : CommRing A) (_ : CommRing B)
      (_ : IsLocalRing A) (_ : IsLocalRing B) (_ : Algebra A B)
      (_ : IsLocalHom (algebraMap A B)) (x y : B),
      let I : Ideal B := (IsLocalRing.maximalIdeal A).map (algebraMap A B)
      x ∈ IsLocalRing.maximalIdeal B ∧
      y ∈ IsLocalRing.maximalIdeal B ∧
      RingTheory.Sequence.IsRegular B [x, y] ∧
      Module.Flat A (B ⧸ Ideal.ofList [x, y]) ∧
      ¬ RingTheory.Sequence.IsRegular (B ⧸ I)
        [Ideal.Quotient.mk I x, Ideal.Quotient.mk I y] ∧
      ¬ Koszul.IsKoszulRegular
        (fun i : Fin 2 =>
          if i = 0 then Ideal.Quotient.mk I x else Ideal.Quotient.mk I y)

Sources

• Section 110.15, Tag 063Z
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_regularSequence_with_common_annihilator_mod_last · Stacks.Examples.exists_regular_sequence_flat_quotient_not_koszulRegular_fiber

Section110.18 Another local ring with nonreduced completion#

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

Tag 0GHI, a lemma

Tag 0GHI in the Stacks Project.

exists_nonreduced_adicCompletion_localization_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/NonreducedLocalizedCompletion.lean, line 345.

Stacks 0GHI. There is a local Noetherian two-dimensional domain B, complete with respect to a principal ideal I = (b), and an element f of its maximal ideal outside I, such that the I-adic completion C = (B_f)^ of the principal localization B_f is nonreduced, and even such that C[1/b] is nonreduced.

theorem exists_nonreduced_adicCompletion_localization_away :
    ∃ (B : Type u) (_ : CommRing B) (_ : IsDomain B) (_ : IsLocalRing B)
      (_ : IsNoetherianRing B) (b f : B),
      ringKrullDim B = 2 ∧
        IsAdicComplete (Ideal.span {b}) B ∧
        f ∈ IsLocalRing.maximalIdeal B ∧
        f ∉ Ideal.span {b} ∧
        (let C := AdicCompletion
            ((Ideal.span {b}).map (algebraMap B (Localization.Away f)))
            (Localization.Away f);
          (¬ IsReduced C) ∧
            (¬ IsReduced (Localization.Away (algebraMap B C b))))

Sources

• Section 110.18, Tag 0GHH
• AxiomMath/Stacks at 5ed82d14

Leanexists_nonreduced_adicCompletion_localization_away

Section110.21 Dimension in Noetherian Jacobson rings#

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

Tag 0EEI, a lemma

Tag 0EEI in the Stacks Project.

exists_isJacobsonRing_isUniversallyCatenary_localization_ringKrullDim_one_and_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/MaximalIdealHeight.lean, line 297. References: EGA IV (10.7.3), “n = 2 case”.

Stacks 0EEI. There is a Jacobson, universally catenary, Noetherian domain B with maximal ideals 𝔪₁ and 𝔪₂ such that dim B_{𝔪₁} = 1 and dim B_{𝔪₂} = 2.

theorem exists_isJacobsonRing_isUniversallyCatenary_localization_ringKrullDim_one_and_two :
    ∃ (B : Type u) (_ : CommRing B) (_ : IsNoetherianRing B) (_ : IsDomain B),
      IsJacobsonRing B ∧ Ring.IsUniversallyCatenary B ∧
        ∃ m₁ m₂ : MaximalSpectrum B,
          ringKrullDim (Localization.AtPrime m₁.asIdeal) = 1 ∧
          ringKrullDim (Localization.AtPrime m₂.asIdeal) = 2

Sources

• Section 110.21, Tag 0EEH
• AxiomMath/Stacks at 5ed82d14

Leanexists_isJacobsonRing_isUniversallyCatenary_localization_ringKrullDim_one_and_two

Section110.22 Underlying space Noetherian not Noetherian#

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

Tag 0G62, an example

Tag 0G62 in the Stacks Project.

Stacks.Examples.isPrime_iff_eq_infiniteSquareZeroVariableIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/NoetherianSpaceNotNoetherianRing.lean, line 109. The attribute's comment: “unique_prime”.

Stacks 0G62. The ideal generated by the square-zero variables is the unique prime ideal of S k = k[x₀, x₁, …]/(x₀², x₁², …).

theorem isPrime_iff_eq_infiniteSquareZeroVariableIdeal (k : Type*) [Field k]
    (P : Ideal (S k)) : P.IsPrime ↔ P = infiniteSquareZeroVariableIdeal k

Stacks.Examples.uniquePrimeSpectrum, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/NoetherianSpaceNotNoetherianRing.lean, line 121. The attribute's comment: “singleton_spectrum”.

Stacks 0G62. The spectrum of S k = k[x₀, x₁, …]/(x₀², x₁², …) has exactly one point.

noncomputable instance uniquePrimeSpectrum (k : Type*) [Field k] :
    Unique (PrimeSpectrum (S k))

Stacks.Examples.noetherianSpace_primeSpectrum, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/NoetherianSpaceNotNoetherianRing.lean, line 130. The attribute's comment: “noetherian_underlying_space”.

Stacks 0G62. The spectrum of S k = k[x₀, x₁, …]/(x₀², x₁², …) is a Noetherian topological space.

noncomputable instance noetherianSpace_primeSpectrum (k : Type*) [Field k] :
    TopologicalSpace.NoetherianSpace (PrimeSpectrum (S k))

Stacks.Examples.infiniteSquareZeroVariableIdeal_not_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/NoetherianSpaceNotNoetherianRing.lean, line 152. The attribute's comment: “prime_not_finitely_generated”.

Stacks 0G62. The ideal generated by the variables of S k = k[x₀, x₁, …]/(x₀², x₁², …) is not finitely generated; in particular S k is not a Noetherian ring even though its spectrum is a Noetherian space.

theorem infiniteSquareZeroVariableIdeal_not_fg (k : Type*) [Field k] :
    ¬ (infiniteSquareZeroVariableIdeal k).FG

Tag 0G63, an example

Tag 0G63 in the Stacks Project.

ManyMonomial.subalgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 68. The attribute's comment: “the algebra”.

The subalgebra generated over k by all x y^i.

def subalgebra : Subalgebra k (MvPolynomial (Fin 2) k)

ManyMonomial.monomialIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 84. The attribute's comment: “the monomial ideal”.

The ideal generated by all x y^i.

def monomialIdeal : Ideal (subalgebra k)

ManyMonomial.localization_away_x_equiv_laurentPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 312. The attribute's comment: “localization description”.

Inverting x gives Laurent polynomials in x over k[y].

theorem localization_away_x_equiv_laurentPolynomial :
    ∃ e : Localization.Away (x k) ≃+* LaurentPolynomial (Polynomial k),
      (∀ c : k,
        e (algebraMap (subalgebra k) (Localization.Away (x k))
          (algebraMap k (subalgebra k) c)) =
        LaurentPolynomial.C (Polynomial.C c)) ∧
      e (algebraMap (subalgebra k) (Localization.Away (x k)) (x k)) =
        LaurentPolynomial.T 1 ∧
      (∀ i : ℕ,
        e (algebraMap (subalgebra k) (Localization.Away (x k))
          (xyPowIn k i)) =
        LaurentPolynomial.T 1 * LaurentPolynomial.C (Polynomial.X ^ i))

ManyMonomial.monomialIdeal_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 339. The attribute's comment: “the prime containing x”.

The monomial ideal is prime.

theorem monomialIdeal_isPrime : (monomialIdeal k).IsPrime

ManyMonomial.xyPowIn_mem_prime_of_x_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 348. The attribute's comment: “monomials belong to primes containing x”.

Each monomial x y^i belongs to a prime ideal containing x.

theorem xyPowIn_mem_prime_of_x_mem
    (p : Ideal (subalgebra k)) [p.IsPrime] (h : x k ∈ p) (i : ℕ) :
    xyPowIn k i ∈ p

ManyMonomial.prime_eq_monomialIdeal_of_x_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 363. The attribute's comment: “uniqueness of the prime containing x”.

Every prime containing x is the monomial ideal.

theorem prime_eq_monomialIdeal_of_x_mem
    (p : Ideal (subalgebra k)) [p.IsPrime] (h : x k ∈ p) :
    p = monomialIdeal k

ManyMonomial.noetherianSpace_primeSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 380. The attribute's comment: “Noetherian spectrum”.

The spectrum of the monomial algebra is Noetherian.

theorem noetherianSpace_primeSpectrum :
    TopologicalSpace.NoetherianSpace (PrimeSpectrum (subalgebra k))

ManyMonomial.monomialIdeal_not_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 473. The attribute's comment: “non-finitely generated ideal”.

The unique prime above x is not finitely generated.

theorem monomialIdeal_not_fg : ¬ (monomialIdeal k).FG

ManyMonomial.not_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 496. The attribute's comment: “non-Noetherian ring”.

The monomial algebra is not a Noetherian ring.

theorem not_isNoetherianRing : ¬ IsNoetherianRing (subalgebra k)

Declarations registered for the tag:

• IsLocalization.primeSpectrumOrderIso registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 57 (StacksFrontier): “prime correspondence”. References: EGA 0 (1.2.6); EGA I (1.2.6), “partial”; EGA IV (10.7.3), “partial”.
• Subalgebra.isDomain registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/ManyMonomialAlgebra.lean, line 58 (StacksFrontier): “domain”.

Sources

• Section 110.22, Tag 0G61
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.isPrime_iff_eq_infiniteSquareZeroVariableIdeal · Stacks.Examples.uniquePrimeSpectrum · Stacks.Examples.noetherianSpace_primeSpectrum · Stacks.Examples.infiniteSquareZeroVariableIdeal_not_fg · ManyMonomial.subalgebra · ManyMonomial.monomialIdeal · ManyMonomial.localization_away_x_equiv_laurentPolynomial · ManyMonomial.monomialIdeal_isPrime

Section110.23 Non-quasi-affine variety with quasi-affine normalization#

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

Tag 0272, a lemma

Tag 0272 in the Stacks Project.

Stacks.Examples.exists_isVariety_normalization_isQuasiAffine_not_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/PinchedPlane/Variety.lean, line 430.

Stacks Project, Tag 0272. Over any field there is a variety whose normalization is quasi-affine but which is itself not quasi-affine: the punctured plane with its two punctured coordinate axes glued to one another.

theorem exists_isVariety_normalization_isQuasiAffine_not_isQuasiAffine
    (k : Type u) [Field k] :
    ∃ (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
      (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite),
      AlgebraicGeometry.IsVariety k f ∧
        Scheme.IsQuasiAffine (Scheme.normalizationScheme X hX) ∧
        ¬ Scheme.IsQuasiAffine X

Sources

• Section 110.23, Tag 0271
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_isVariety_normalization_isQuasiAffine_not_isQuasiAffine

Section110.25 Images of locally closed subsets#

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

Tag 0GZM, a lemma

Tag 0GZM in the Stacks Project.

Stacks.Examples.exists_affine_finitePresentation_image_not_finiteUnionLocallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/ImageNotFiniteUnionLocallyClosed.lean, line 429.

Stacks 0GZM. A finite-presentation morphism of affine schemes can take a locally closed subset to a set that is not a finite union of locally closed subsets.

theorem exists_affine_finitePresentation_image_not_finiteUnionLocallyClosed :
    ∃ (X Y : Scheme.{u}) (f : X ⟶ Y) (T : Set X),
      IsAffine X ∧ IsAffine Y ∧ FinitePresentation f ∧
        IsLocallyClosed T ∧ ¬ IsFiniteUnionLocallyClosed (f.base '' T)

Sources

• Section 110.25, Tag 0GZL
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_affine_finitePresentation_image_not_finiteUnionLocallyClosed

Section110.27 Nonexistence of suitable opens#

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

Tag 086H, a lemma

Tag 086H in the Stacks Project.

Stacks.Examples.exists_affine_scheme_punctured_without_quasiCompact_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/PuncturedAxes.lean, line 265. The attribute's comment: “punctured_affine”.

There is an affine scheme with a closed point such that its punctured complement contains no quasi-compact dense open subset.

theorem exists_affine_scheme_punctured_without_quasiCompact_dense_open :
    ∃ (S : Scheme.{u}) (_ : IsAffine S) (s : S),
      IsClosed ({s} : Set S) ∧
        ¬ ∃ U : Set {x : S // x ≠ s}, IsOpen U ∧ IsCompact U ∧ Dense U

Stacks.Examples.exists_affineOpen_without_disjoint_quasiCompact_dense_union, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/PuncturedAxes.lean, line 279. The attribute's comment: “disjoint_dense_union”.

In some affine scheme, an affine open has no disjoint quasi-compact open whose union with it is dense.

theorem exists_affineOpen_without_disjoint_quasiCompact_dense_union :
    ∃ (S : Scheme.{u}) (_ : IsAffine S) (U : S.Opens),
      IsAffineOpen U ∧
        ¬ ∃ V : S.Opens, IsCompact V.1 ∧ (U ⊓ V = ⊥) ∧ Dense (U.1 ∪ V.1)

Tag 086I, a lemma

Tag 086I in the Stacks Project.

Stacks.Examples.exists_qcqs_without_separated_quasiCompact_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/QcqsWithoutSeparatedDenseOpen.lean, line 357.

Stacks 086I. There is a quasi-compact quasi-separated scheme with no separated quasi-compact dense open.

theorem exists_qcqs_without_separated_quasiCompact_dense_open :
    ∃ X : Scheme.{u}, CompactSpace X ∧ QuasiSeparatedSpace X ∧
      ¬ ∃ V : X.Opens, IsCompact (V : Set X) ∧ Dense (V : Set X) ∧
        Scheme.IsSeparated V

Sources

• Section 110.27, Tag 086G
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_affine_scheme_punctured_without_quasiCompact_dense_open · Stacks.Examples.exists_affineOpen_without_disjoint_quasiCompact_dense_union · Stacks.Examples.exists_qcqs_without_separated_quasiCompact_dense_open

Section110.28 Nonexistence of quasi-compact dense open subscheme#

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

Tag 087I, a lemma

Tag 087I in the Stacks Project.

Stacks.Examples.AxesReflection.exists_quasiCompact_quasiSeparated_without_quasiCompact_dense_open_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/QcqsWithoutQuasiCompactDenseOpen.lean, line 421. The attribute's comment: “a quasi-compact quasi-separated algebraic space with no quasi-compact dense open subscheme: the quotient of a line glued to countably many axes by a reflection”.

Stacks 087I. There exists a quasi-compact and quasi-separated algebraic space which does not contain a quasi-compact dense open subscheme.

The space is the quotient of Spec k[x, z₁, z₂, …]/(x zᵢ, zᵢ zⱼ) by the reflection x ↦ -x over the punctured line, for k of characteristic different from two.

The space is an algebraic space by Stacks 02WW, through Stacks 0265 and the effective descent along the covering sieves at the monomorphisms locally of finite type that it consumes. The big fppf site carrying it is produced inside the proof, and so is existentially quantified.

theorem exists_quasiCompact_quasiSeparated_without_quasiCompact_dense_open_subscheme :
    ∃ (B : BigFppfSite.{u}) (hZ : B.Contains (⊤_ Scheme.{u}))
      (F : (BigFppfOver B (⊤_ Scheme.{u}) hZ)ᵒᵖ ⥤ Type u)
      (_ : IsAlgebraicSpace B (⊤_ Scheme.{u}) hZ F),
      Space.IsQuasiCompactSpace B (⊤_ Scheme.{u}) hZ F ∧
      Space.IsAbsolutelyQuasiSeparated B (⊤_ Scheme.{u}) hZ hZ F ∧
      ¬ ∃ (V : BigFppfOver B (⊤_ Scheme.{u}) hZ) (f : yoneda.obj V ⟶ F),
        CompactSpace ((BigFppfOver.toScheme B (⊤_ Scheme.{u}) hZ).obj V) ∧
        Space.IsOpenImmersion B (⊤_ Scheme.{u}) hZ f ∧
        Dense (Set.range (Space.pointsMap B (⊤_ Scheme.{u}) hZ (yoneda.obj V) f))

Sources

• Section 110.28, Tag 087H
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.AxesReflection.exists_quasiCompact_quasiSeparated_without_quasiCompact_dense_open_subscheme

Section110.29 Affines over algebraic spaces#

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

Tag 088W, a lemma

Tag 088W in the Stacks Project.

Stacks.Examples.exists_finiteType_affine_not_immersion_into_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/AffineOverSpaceNoImmersion.lean, line 743. The attribute's comment: “the counterexample”.

Stacks 088W. There is a finite-type morphism Y ⟶ X of algebraic spaces with Y an affine scheme and X quasi-separated which admits no immersion of Y, over X, into relative affine n-space over X for any n.

Take for X the quotient 𝔸¹_k/R of Stacks 02Z1 over a field in which two is invertible, for Y its chart 𝔸¹_k, and for the morphism the chart itself: it is étale, hence locally of finite type, and quasi-compact because its source is quasi-compact and X is quasi-separated — that is AffineOverAlgebraicSpace.isFiniteType_quotientSpaceMap. The nonexistence of an immersion is AffineOverAlgebraicSpace.not_isImmersion_affineSpaceOver_quotientSpaceMap.

Algebraicity and quasi-separatedness of the target come from Stacks 02Z1 in the form in which the relation of this example is an affine morphism, so Stacks 0265 applies to it with no effective-descent input: AlgebraicGeometry.AffineLineInvolution.isAlgebraicSpace_involutionQuotient_of_isAffineHom rests on the relation being affine, which is Mathlib's IsAffineHom instance for a morphism between affine schemes, and the descent that Stacks 0265 then consumes is effective descent at the affine monomorphisms locally of finite type, proved outright in StacksFrontier/AlgebraicGeometry/Descent/AffineHomCoveringSieveDescent.lean.

theorem exists_finiteType_affine_not_immersion_into_affineSpace
    (k : Type u) [Field k] (hchar : (2 : k) ≠ 0)
    (B : BigFppfSite.{u}) (hS : B.Contains (Spec (.of k)))
    (hZ : B.Contains (⊤_ Scheme.{u}))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    ∃ (Y : BigFppfOver B (Spec (.of k)) hS)
      (X : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u)
      (f : yoneda.obj Y ⟶ X),
      IsAffine ((BigFppfOver.toScheme B (Spec (.of k)) hS).obj Y) ∧
      IsAlgebraicSpace B (Spec (.of k)) hS (yoneda.obj Y) ∧
      IsAlgebraicSpace B (Spec (.of k)) hS X ∧
      Space.IsFiniteType B (Spec (.of k)) hS f ∧
      Space.IsAbsolutelyQuasiSeparated B (Spec (.of k)) hS hZ X ∧
      ∀ (n : ℕ) (j : yoneda.obj Y ⟶ Space.affineSpaceOver B (Spec (.of k)) hS X n),
        j ≫ prod.fst = f → ¬ Space.IsImmersion B (Spec (.of k)) hS j

Sources

• Section 110.29, Tag 088V
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_finiteType_affine_not_immersion_into_affineSpace

Section110.30 Pushforward of quasi-coherent modules#

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

Tag 078D, a lemma

Tag 078D in the Stacks Project.

Stacks.Examples.QcohPushforward.exists_quasiCompact_not_quasiSeparated_pushforward_not_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/QuasiCoherentPushforward/NotQuasiSeparated.lean, line 521. The attribute's comment: “non_quasi_separated”.

Stacks Project, Tag 078D (non-quasi-separated case). A quasi-compact morphism need not be quasi-separated, and may send its quasi-coherent structure sheaf to a module which is not quasi-coherent.

theorem exists_quasiCompact_not_quasiSeparated_pushforward_not_isQuasicoherent :
    ∃ (X Y : Scheme.{u}) (f : X ⟶ Y),
      QuasiCompact f ∧
      ¬ QuasiSeparated f ∧
      (SheafOfModules.unit X.ringCatSheaf).IsQuasicoherent ∧
      ¬ ((Scheme.Modules.pushforward f).obj
        (SheafOfModules.unit X.ringCatSheaf)).IsQuasicoherent

Stacks.Examples.QcohPushforward.exists_isSeparated_not_quasiCompact_pushforward_not_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/QuasiCoherentPushforward/SeparatedNotQuasiCompact.lean, line 263. The attribute's comment: “non_quasi_compact”.

Stacks Project, Tag 078D (non-quasi-compact case). Over Spec ℤ, a separated, non-quasi-compact morphism can push a quasi-coherent structure sheaf to a sheaf which is not quasi-coherent.

theorem exists_isSeparated_not_quasiCompact_pushforward_not_isQuasicoherent :
    ∃ (X : Scheme) (f : X ⟶ Spec (.of ℤ)),
      IsSeparated f ∧ ¬ QuasiCompact f ∧
        (SheafOfModules.unit X.ringCatSheaf).IsQuasicoherent ∧
          ¬ ((Scheme.Modules.pushforward f).obj
            (SheafOfModules.unit X.ringCatSheaf)).IsQuasicoherent

Sources

• Section 110.30, Tag 078C
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.QcohPushforward.exists_quasiCompact_not_quasiSeparated_pushforward_not_isQuasicoherent · Stacks.Examples.QcohPushforward.exists_isSeparated_not_quasiCompact_pushforward_not_isQuasicoherent

Section110.32 A noninvertible ideal invertible in stalks#

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

Tag 0CC0, a lemma

Tag 0CC0 in the Stacks Project.

Stacks.Examples.exists_locally_principal_ideal_not_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/LocallyPrincipalNotInvertible.lean, line 215.

Stacks 0CC0. A nonzero ideal in a domain can be principal at every prime localization without being invertible as a module.

theorem exists_locally_principal_ideal_not_invertible :
    ∃ (A : Type*) (_ : CommRing A) (_ : IsDomain A) (I : Ideal A),
      I ≠ ⊥ ∧
      (∀ (q : Ideal A) [q.IsPrime],
        Submodule.IsPrincipal
          (I.map (algebraMap A (Localization.AtPrime q)))) ∧
      ¬ Module.Invertible A I

Sources

• Section 110.32, Tag 0CBZ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.exists_locally_principal_ideal_not_invertible

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.