111 Exercises

Chapter 111 of the Stacks Project, Exercises, Tag 0275: the 14 sections of its 66 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 19 tags are carried by 46 declarations of the repository (all in StacksFrontier) and 29 registered declarations.

Section111.2 Colimits#

Section 111.2 of the Stacks Project, Tag 0277. 1 tag here is carried by 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 078I, a definition

Tag 078I in the Stacks Project.

Declarations registered for the tag:

Sources
LeanIsDirected · DirectedSystem

Section111.6 The Spectrum of a ring#

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

Tag 027F, a definition

Tag 027F in the Stacks Project.

TopologicalSpace.ArtinianSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/NoetherianSpace.lean, line 38. The attribute's comment: “Artinian spaces”.

A topological space is Artinian if its ascending chains of closed subsets stabilize.

abbrev ArtinianSpace (X : Type*) [TopologicalSpace X] : Prop

Declarations registered for the tag:

Sources
LeanTopologicalSpace.ArtinianSpace · TopologicalSpace.NoetherianSpace

Section111.18 Catenary rings#

Section 111.18 of the Stacks Project, Tag 027N. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 027O, a definition

Tag 027O in the Stacks Project.

Ideal.ringKrullDim_quotient_localization_eq_height_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/Catenary.lean, line 52. The attribute's comment: “relative_height”. References: EGA 0 (16.1.3), “(16.1.3.2)”; EGA 0 (16.3.1), “more general”.

For q ≤ p with p prime, the Krull dimension of Aₚ/qAₚ is the height of the prime ideal p/q of A/q.

theorem ringKrullDim_quotient_localization_eq_height_map
    {A : Type*} [CommRing A] (q p : Ideal A) [p.IsPrime] (hqp : q ≤ p) :
    ringKrullDim
        (Localization.AtPrime p ⧸ q.map (algebraMap A (Localization.AtPrime p))) =
      ((p.map (Ideal.Quotient.mk q)).height : WithBot ℕ∞)

Declarations registered for the tag:

Sources
LeanIdeal.ringKrullDim_quotient_localization_eq_height_map · IsLocalization.AtPrime.ringKrullDim_eq_height · Ring.IsCatenary · TopologicalSpace.IsTopologicallyCatenary

Section111.22 Finite locally free modules#

Section 111.22 of the Stacks Project, Tag 027Q. 1 tag here is carried by 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 027R, a definition

Tag 027R in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.IsFiniteLocallyFree · Module.Invertible

Section111.26 Hilbert functions#

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

Tag 027X, a definition

Tag 027X in the Stacks Project.

Polynomial.IsNumerical, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Polynomial/Numerical.lean, line 58.

A polynomial over ℚ is numerical if it takes an integer value at every integer.

public abbrev IsNumerical (f : Polynomial ℚ) : Prop
Tag 027Y, a definition

Tag 027Y in the Stacks Project.

GradedModule.IsLocallyFinite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedModule/HilbertFunction.lean, line 60. The attribute's comment: “locally finite graded modules”.

A graded module is locally finite when every homogeneous piece is finitely generated over the base ring.

abbrev IsLocallyFinite (piece : ℤ → Submodule A M) [DirectSum.Decomposition piece] : Prop

GradedModule.EulerPoincareFunction, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedModule/HilbertFunction.lean, line 72. The attribute's comment: “Euler-Poincare functions”.

An Euler–Poincaré function assigns an integer to every finitely generated module and is additive in short exact sequences.

structure EulerPoincareFunction (A : Type u) [Ring A]

GradedModule.hilbertFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedModule/HilbertFunction.lean, line 88. The attribute's comment: “Hilbert functions”.

The Hilbert function of a locally finite graded module with respect to an Euler–Poincaré function: its value at n is the value of the function on the degree-n piece.

def hilbertFunction (piece : ℤ → Submodule A M) [DirectSum.Decomposition piece]
    (hpiece : IsLocallyFinite piece) (φ : EulerPoincareFunction.{u, v} A) : ℤ → ℤ

GradedModule.HasHilbertPolynomial, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedModule/HilbertFunction.lean, line 101. The attribute's comment: “Hilbert polynomials”.

A locally finite graded module has a Hilbert polynomial with respect to φ when its Hilbert function eventually agrees, on integer arguments, with a numerical polynomial.

abbrev HasHilbertPolynomial (piece : ℤ → Submodule A M) [DirectSum.Decomposition piece]
    (hpiece : IsLocallyFinite piece) (φ : EulerPoincareFunction.{u, v} A) : Prop

Declarations registered for the tag:

Sources
LeanPolynomial.IsNumerical · GradedModule.IsLocallyFinite · GradedModule.EulerPoincareFunction · GradedModule.hilbertFunction · GradedModule.HasHilbertPolynomial · DirectSum.Decomposition

Section111.28 Cohen-Macaulay rings of dimension 1#

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

Tag 0285, a definition

Tag 0285 in the Stacks Project.

IsLocalRing.IsCohenMacaulayOfDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/CohenMacaulay.lean, line 39.

A local ring A is Cohen--Macaulay of dimension d if its Krull dimension is d and there is a system of parameters x₁, ..., x_d such that every xᵢ is a nonzerodivisor on the quotient by its predecessors.

abbrev IsCohenMacaulayOfDimension (A : Type*) [CommRing A] [IsLocalRing A] (d : ℕ) : Prop
Sources
LeanIsLocalRing.IsCohenMacaulayOfDimension

Section111.29 Infinitely many primes#

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

Tag 02ER, a remark

Tag 02ER in the Stacks Project.

Polynomial.monic_aeval_isFiniteLocallyFreeOfRank_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/PolynomialSubstitution.lean, line 142. The attribute's comment: “part (1)”.

Substitution by a monic integral polynomial of positive degree is finite locally free of rank equal to its degree.

theorem monic_aeval_isFiniteLocallyFreeOfRank_int (h : Polynomial ℤ)
    (hh : h.Monic) (hd : 0 < h.natDegree) :
    letI : Algebra (Polynomial ℤ) (Polynomial ℤ) := (Polynomial.aeval h).toRingHom.toAlgebra
    letI : Module (Polynomial ℤ) (Polynomial ℤ) := Algebra.toModule
    Module.IsFiniteLocallyFreeOfRank (Polynomial ℤ) (Polynomial ℤ) h.natDegree

Polynomial.monic_aeval_isFiniteLocallyFreeOfRank_zmod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/PolynomialSubstitution.lean, line 152. The attribute's comment: “part (2)”.

After reduction modulo a prime, substitution by the reduced monic polynomial is finite locally free of the original degree.

theorem monic_aeval_isFiniteLocallyFreeOfRank_zmod (h : Polynomial ℤ)
    (hh : h.Monic) (hd : 0 < h.natDegree) (p : ℕ) (hp : p.Prime) :
    let g : Polynomial (ZMod p) := h.map (Int.castRingHom (ZMod p))
    letI : Algebra (Polynomial (ZMod p)) (Polynomial (ZMod p)) :=
      (Polynomial.aeval g).toRingHom.toAlgebra
    letI : Module (Polynomial (ZMod p)) (Polynomial (ZMod p)) := Algebra.toModule
    Module.IsFiniteLocallyFreeOfRank (Polynomial (ZMod p))
      (Polynomial (ZMod p)) h.natDegree
Sources
LeanPolynomial.monic_aeval_isFiniteLocallyFreeOfRank_int · Polynomial.monic_aeval_isFiniteLocallyFreeOfRank_zmod

Section111.30 Filtered derived category#

Section 111.30 of the Stacks Project, Tag 0287. 4 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 028A, a definition

Tag 028A in the Stacks Project.

Declarations registered for the tag:

Tag 028B, a definition

Tag 028B in the Stacks Project.

Declarations registered for the tag:

Tag 028D, a definition

Tag 028D in the Stacks Project.

Declarations registered for the tag:

Tag 028E, a definition

Tag 028E in the Stacks Project.

CategoryTheory.FiniteFilteredObject.filteredAcyclic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/FilteredObject.lean, line 58.

A complex of finite filtered objects is filtered acyclic when every graded-piece complex is acyclic.

abbrev filteredAcyclic (A : Type u) [Category.{v} A] [Abelian A]
    (K : CochainComplex (FiniteFilteredObject A) ℤ) : Prop
Sources
LeanCategoryTheory.FilteredObject.IsFilteredInjective · CategoryTheory.FiniteFilteredObject · CochainComplex.filteredQuasiIso · CategoryTheory.FiniteFilteredObject.filteredAcyclic

Section111.33 Schemes#

Section 111.33 of the Stacks Project, Tag 028O. 1 tag here is carried by 11 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02EY, a remark

Tag 02EY in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.SheafedSpace.restrict · AlgebraicGeometry.SheafedSpace.ofRestrict · AlgebraicGeometry.LocallyRingedSpace.restrict · AlgebraicGeometry.LocallyRingedSpace.ofRestrict · AlgebraicGeometry.Scheme.Opens.toScheme · AlgebraicGeometry.Scheme.Opens.ι · AlgebraicGeometry.Scheme.restrictFunctor · AlgebraicGeometry.IsOpenImmersion

Section111.40 Invertible sheaves#

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

Tag 02AD, a definition

Tag 02AD in the Stacks Project.

AlgebraicGeometry.SheafOfModules.OnSpace.IsInvertible, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/InvertibleSheaves.lean, line 58. The attribute's comment: “invertible sheaves”. References: EGA 0 (5.4.1), “invertible”.

A sheaf of modules is invertible if every point has an open neighbourhood on which it is isomorphic to the structure sheaf.

class IsInvertible {X : TopCat.{u}}
    {R : Sheaf (Opens.grothendieckTopology X) RingCat.{v}}
    (L : _root_.SheafOfModules.{v} R) : Prop

AlgebraicGeometry.SheafOfModules.OnSpace.IsTrivial, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/InvertibleSheaves.lean, line 68. The attribute's comment: “trivial sheaves”.

A sheaf of modules is trivial if it is globally isomorphic to the structure sheaf.

abbrev IsTrivial {X : TopCat.{u}}
    {R : Sheaf (Opens.grothendieckTopology X) RingCat.{v}}
    (L : _root_.SheafOfModules.{v} R) : Prop
Tag 02AG, a definition

Tag 02AG in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.SheafOfModules.OnSpace.IsInvertible · AlgebraicGeometry.SheafOfModules.OnSpace.IsTrivial · Module.Invertible · Module.IsTrivialInvertibleModule

Section111.41 Čech Cohomology#

Section 111.41 of the Stacks Project, Tag 02AO. 1 tag here is carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02AP, a definition

Tag 02AP in the Stacks Project.

Stacks.Cohomology.CechBoundary.exists_covering_localLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechToCohomology/BoundaryCocycle.lean, line 109. The attribute's comment: “existence of a covering with lifts”.

If ψ : ℱ₂ ⟶ ℱ₃ is locally surjective for the topology of open covers, then every section τ of ℱ₃ over an open W admits an open covering of W together with a 0-cochain of ℱ₂ lifting the restrictions of τ.

theorem exists_covering_localLifts {W : Opens X} (τ : ToType (ℱ₃.obj (op W)))
    (hψ : CategoryTheory.Presheaf.IsLocallySurjective (Opens.grothendieckTopology X) ψ) :
    ∃ (I₀ : Type uX) (U₀ : I₀ → Opens X) (hU₀ : W = ⨆ i, U₀ i) (lift : Cochain U₀ ℱ₂ 0),
      ∀ i : Fin 1 → I₀,
        ψ.app (op (inter U₀ i)) (lift i) = restr ℱ₃ (inter_le_of_eq_iSup hU₀ i) τ

Stacks.Cohomology.CechBoundary.exists_cocycle_of_localLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechToCohomology/BoundaryCocycle.lean, line 139. The attribute's comment: “the cocycle”.

Let φ : ℱ₁ ⟶ ℱ₂ be injective on sections and ℱ₁ → ℱ₂ → ℱ₃ exact in the middle on sections. If τ is a section of ℱ₃ over W and lift is a 0-cochain of ℱ₂ lifting the restrictions of τ, then the coboundary of lift is the image of a 1-cocycle of ℱ₁.

theorem exists_cocycle_of_localLifts
    (hmono : ∀ V : Opens X, Function.Injective (φ.app (op V)))
    (hexact : ∀ (V : Opens X) (b : ToType (ℱ₂.obj (op V))), ψ.app (op V) b = 0 →
      ∃ a, φ.app (op V) a = b)
    (hlift : ∀ i, ψ.app (op (inter U i)) (lift i) = restr ℱ₃ (hle i) τ) :
    ∃ c : cocycles1 U ℱ₁, push U φ 1 (c : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift

Stacks.Cohomology.CechBoundary.cls_eq_of_localLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechToCohomology/BoundaryCocycle.lean, line 162. The attribute's comment: “well-definedness in the lifts”.

Let φ : ℱ₁ ⟶ ℱ₂ be injective on sections and ℱ₁ → ℱ₂ → ℱ₃ exact in the middle on sections. Two systems of lifts of the same section give 1-cocycles of ℱ₁ with the same class in Ȟ¹(𝒰, ℱ₁).

theorem cls_eq_of_localLifts
    (hmono : ∀ V : Opens X, Function.Injective (φ.app (op V)))
    (hexact : ∀ (V : Opens X) (b : ToType (ℱ₂.obj (op V))), ψ.app (op V) b = 0 →
      ∃ a, φ.app (op V) a = b)
    {lift' : Cochain U ℱ₂ 0}
    (hlift : ∀ i, ψ.app (op (inter U i)) (lift i) = restr ℱ₃ (hle i) τ)
    (hlift' : ∀ i, ψ.app (op (inter U i)) (lift' i) = restr ℱ₃ (hle i) τ)
    {c c' : cocycles1 U ℱ₁}
    (hc : push U φ 1 (c : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift)
    (hc' : push U φ 1 (c' : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift') :
    cls U ℱ₁ c = cls U ℱ₁ c'

Stacks.Cohomology.CechBoundary.cls_add_of_localLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechToCohomology/BoundaryCocycle.lean, line 190. The attribute's comment: “additivity of the boundary map”.

Let φ : ℱ₁ ⟶ ℱ₂ be injective on sections. The class attached to the sum of two systems of local lifts is the sum of the two classes.

theorem cls_add_of_localLifts
    (hmono : ∀ V : Opens X, Function.Injective (φ.app (op V)))
    {lift' : Cochain U ℱ₂ 0} {c c' d : cocycles1 U ℱ₁}
    (hc : push U φ 1 (c : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift)
    (hc' : push U φ 1 (c' : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift')
    (hd : push U φ 1 (d : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 (lift + lift')) :
    cls U ℱ₁ d = cls U ℱ₁ c + cls U ℱ₁ c'

Stacks.Cohomology.CechBoundary.cls_eq_of_refinement_of_localLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechToCohomology/BoundaryCocycle.lean, line 221. The attribute's comment: “independence of the covering, on a given common refinement”.

Let φ : ℱ₁ ⟶ ℱ₂ be injective on sections and ℱ₁ → ℱ₂ → ℱ₃ exact in the middle on sections. Let 𝒰 and 𝒰' be two families of opens over W, each carrying a system of lifts of the same section τ of ℱ₃, and let 𝒱 be a common refinement of the two: a family of opens with refinement functions into the index sets of 𝒰 and of 𝒰'. Then the two classes attached to τ have the same image in Ȟ¹(𝒱, ℱ₁).

theorem cls_eq_of_refinement_of_localLifts
    (U' : I' → Opens X) (V : K → Opens X)
    (r : K → I) (hr : ∀ k, V k ≤ U (r k))
    (r' : K → I') (hr' : ∀ k, V k ≤ U' (r' k))
    (hle' : ∀ i : Fin 1 → I', inter U' i ≤ W)
    (hmono : ∀ V₀ : Opens X, Function.Injective (φ.app (op V₀)))
    (hexact : ∀ (V₀ : Opens X) (b : ToType (ℱ₂.obj (op V₀))), ψ.app (op V₀) b = 0 →
      ∃ a, φ.app (op V₀) a = b)
    {lift' : Cochain U' ℱ₂ 0}
    (hlift : ∀ i, ψ.app (op (inter U i)) (lift i) = restr ℱ₃ (hle i) τ)
    (hlift' : ∀ i, ψ.app (op (inter U' i)) (lift' i) = restr ℱ₃ (hle' i) τ)
    {c : cocycles1 U ℱ₁} {c' : cocycles1 U' ℱ₁}
    (hc : push U φ 1 (c : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift)
    (hc' : push U' φ 1 (c' : Cochain U' ℱ₁ 1) = cechD U' ℱ₂ 0 lift') :
    refinementCechH1 U V r hr ℱ₁ (cls U ℱ₁ c) =
      refinementCechH1 U' V r' hr' ℱ₁ (cls U' ℱ₁ c')

Stacks.Cohomology.CechBoundary.exists_common_refinement_cls_eq_of_localLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechToCohomology/BoundaryCocycle.lean, line 263. The attribute's comment: “independence of the covering”.

Let φ : ℱ₁ ⟶ ℱ₂ be injective on sections and ℱ₁ → ℱ₂ → ℱ₃ exact in the middle on sections. Two families of opens covering W, each carrying a system of lifts of the same section τ of ℱ₃, admit a common refinement covering W, the family of their pairwise intersections, on which the two classes attached to τ agree.

theorem exists_common_refinement_cls_eq_of_localLifts
    (U' : I' → Opens X) (hU : W = ⨆ i, U i) (hU' : W = ⨆ i', U' i')
    (hmono : ∀ V₀ : Opens X, Function.Injective (φ.app (op V₀)))
    (hexact : ∀ (V₀ : Opens X) (b : ToType (ℱ₂.obj (op V₀))), ψ.app (op V₀) b = 0 →
      ∃ a, φ.app (op V₀) a = b)
    {lift' : Cochain U' ℱ₂ 0}
    (hlift : ∀ i, ψ.app (op (inter U i)) (lift i) = restr ℱ₃ (inter_le_of_eq_iSup hU i) τ)
    (hlift' : ∀ i, ψ.app (op (inter U' i)) (lift' i) = restr ℱ₃ (inter_le_of_eq_iSup hU' i) τ)
    {c : cocycles1 U ℱ₁} {c' : cocycles1 U' ℱ₁}
    (hc : push U φ 1 (c : Cochain U ℱ₁ 1) = cechD U ℱ₂ 0 lift)
    (hc' : push U' φ 1 (c' : Cochain U' ℱ₁ 1) = cechD U' ℱ₂ 0 lift') :
    ∃ (V : I × I' → Opens X) (r : I × I' → I) (hr : ∀ k, V k ≤ U (r k))
      (r' : I × I' → I') (hr' : ∀ k, V k ≤ U' (r' k)),
      W = ⨆ k, V k ∧
        refinementCechH1 U V r hr ℱ₁ (cls U ℱ₁ c) =
          refinementCechH1 U' V r' hr' ℱ₁ (cls U' ℱ₁ c')
Sources
LeanStacks.Cohomology.CechBoundary.exists_covering_localLifts · Stacks.Cohomology.CechBoundary.exists_cocycle_of_localLifts · Stacks.Cohomology.CechBoundary.cls_eq_of_localLifts · Stacks.Cohomology.CechBoundary.cls_add_of_localLifts · Stacks.Cohomology.CechBoundary.cls_eq_of_refinement_of_localLifts · Stacks.Cohomology.CechBoundary.exists_common_refinement_cls_eq_of_localLifts

Section111.49 Divisors#

Section 111.49 of the Stacks Project, Tag 02AQ. 1 tag here is carried by 14 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02AR, a definition

Tag 02AR in the Stacks Project.

AlgebraicGeometry.Scheme.mono_toTotalQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierDivisor.lean, line 164. The attribute's comment: “unit_sheaf_sequence”.

Stacks 02AR part (6). The structure sheaf of a scheme is a subsheaf of its sheaf of total quotient rings.

theorem Scheme.mono_toTotalQuotientSheaf (Y : Scheme.{u}) :
    Mono Y.toTotalQuotientSheaf

AlgebraicGeometry.Scheme.shortExact_unitGroupSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierDivisor.lean, line 171. The attribute's comment: “unit_sheaf_sequence”.

Stacks 02AR part (6). The sequence 0 ⟶ 𝒪_X^* ⟶ 𝒦_X^* ⟶ 𝒦_X^*/𝒪_X^* ⟶ 0 of unit-group sheaves of a scheme is short exact.

theorem Scheme.shortExact_unitGroupSheaf (Y : Scheme.{u}) :
    (ShortComplex.mk (unitGroupSheafMap Y.toTotalQuotientSheaf)
      (unitGroupQuotientMap Y.toTotalQuotientSheaf) (by
        change (presheafToSheaf (Opens.grothendieckTopology Y.toPresheafedSpace)
            AddCommGrpCat.{u}).map (unitGroupMap Y.toTotalQuotientSheaf) ≫
          (presheafToSheaf (Opens.grothendieckTopology Y.toPresheafedSpace)
            AddCommGrpCat.{u}).map
            (cokernel.π (unitGroupMap Y.toTotalQuotientSheaf)) = 0
        rw [← Functor.map_comp]
        simp)).ShortExact

AlgebraicGeometry.Scheme.CartierDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierDivisor.lean, line 187. The attribute's comment: “cartier_divisor”.

Stacks 02AR part (7). A Cartier divisor on a scheme is a global section of the quotient sheaf 𝒦_X^*/𝒪_X^*.

abbrev Scheme.CartierDivisor (Y : Scheme.{u}) : Type u

AlgebraicGeometry.exists_affineOpen_local_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierWeilDivisor.lean, line 576. The attribute's comment: “cartier_weil_divisor”.

Tag 02AR part (8), the local presentation of clause (b). Near any point of a locally Noetherian integral scheme, a Cartier divisor is the image of a unit of the sheaf of total quotient rings over an affine open neighbourhood, and that unit is the fraction a / b of two regular functions on that neighbourhood with b nonzero.

theorem exists_affineOpen_local_representation [IsIntegral X] [IsLocallyNoetherian X]
    (τ : X.CartierDivisor) (x : X) :
    ∃ (U : X.Opens) (_ : IsAffineOpen U) (_ : x ∈ U) (a b : Γ(X, U)) (_ : b ≠ 0)
      (v : (unitGroupPresheaf X.totalQuotientSheaf).obj (op U)),
      (Additive.toMul v).val * X.toTotalQuotientSheaf.hom.app (op U) b =
          X.toTotalQuotientSheaf.hom.app (op U) a ∧
        (unitGroupQuotientSheaf X.toTotalQuotientSheaf).presheaf.map (homOfLE le_top).op τ =
          (rawUnitGroupQuotientMap X.toTotalQuotientSheaf).app (op U) v

AlgebraicGeometry.cartierWeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierWeilDivisor.lean, line 724. The attribute's comment: “cartier_weil_divisor”.

Stacks 02AR part (8). The Weil divisor [τ] = Σ v_Z(τ) [Z] of a Cartier divisor on a Noetherian integral scheme.

def cartierWeilDivisor [IsNoetherian X] [IsIntegral X] (τ : X.CartierDivisor) : WeilDivisor X

AlgebraicGeometry.cartierWeilDivisor_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierWeilDivisor.lean, line 731. The attribute's comment: “cartier_weil_divisor”.

Stacks 02AR part (8). The coefficient of [τ] at a prime divisor is the order v_Z(τ).

theorem cartierWeilDivisor_apply [IsNoetherian X] [IsIntegral X] (τ : X.CartierDivisor)
    (Z : PrimeDivisor X) :
    (cartierWeilDivisor τ).1 Z = cartierMultiplicity τ Z.genericPoint

AlgebraicGeometry.cartierWeilDivisor_apply_of_germ_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierWeilDivisor.lean, line 739. The attribute's comment: “cartier_weil_divisor”.

Stacks 02AR part (8), clause (a). The coefficient of [τ] vanishes at a prime divisor at whose generic point the germ of τ is zero.

theorem cartierWeilDivisor_apply_of_germ_eq_zero [IsNoetherian X] [IsIntegral X]
    (τ : X.CartierDivisor) (Z : PrimeDivisor X)
    (hτ : (unitGroupQuotientSheaf X.toTotalQuotientSheaf).presheaf.Γgerm Z.genericPoint τ = 0) :
    (cartierWeilDivisor τ).1 Z = 0

AlgebraicGeometry.cartierWeilDivisor_apply_of_local_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CartierWeilDivisor.lean, line 748. The attribute's comment: “cartier_weil_divisor”.

Stacks 02AR part (8), clause (b). The coefficient of [τ] at a prime divisor computed from a local presentation a / b of τ on an open neighbourhood of its generic point.

theorem cartierWeilDivisor_apply_of_local_eq [IsNoetherian X] [IsIntegral X]
    (τ : X.CartierDivisor) (Z : PrimeDivisor X) (U : X.Opens) (hξ : Z.genericPoint ∈ U)
    (a b : Γ(X, U)) (hb : b ≠ 0)
    (v : (unitGroupPresheaf X.totalQuotientSheaf).obj (op U))
    (hab : (Additive.toMul v).val * X.toTotalQuotientSheaf.hom.app (op U) b =
      X.toTotalQuotientSheaf.hom.app (op U) a)
    (hτ : (unitGroupQuotientSheaf X.toTotalQuotientSheaf).presheaf.map (homOfLE le_top).op τ =
      (rawUnitGroupQuotientMap X.toTotalQuotientSheaf).app (op U) v) :
    (cartierWeilDivisor τ).1 Z =
      ((Module.length (X.presheaf.stalk Z.genericPoint)
        ((X.presheaf.stalk Z.genericPoint) ⧸
          Ideal.span {X.presheaf.germ U Z.genericPoint hξ a})).toNat : ℤ) -
      ((Module.length (X.presheaf.stalk Z.genericPoint)
        ((X.presheaf.stalk Z.genericPoint) ⧸
          Ideal.span {X.presheaf.germ U Z.genericPoint hξ b})).toNat : ℤ)

AlgebraicGeometry.effectiveCartierWeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierWeilDivisor.lean, line 314. The attribute's comment: “effective_cartier_weil_divisor”.

Stacks 02AR part (5). The Weil divisor [D] = Σ v_Z(D) [Z] of an effective Cartier divisor on a Noetherian integral scheme.

The hypothesis is not used by the term — the coefficient family of an arbitrary ideal sheaf is already finitely supported — but it is what makes the coefficients the orders of Tag 02AR, since only for an effective Cartier divisor is the local length finite.

def effectiveCartierWeilDivisor [IsNoetherian X] [IsIntegral X] (I : X.IdealSheafData)
    (_hI : Stacks.Divisors.IsEffectiveCartierDivisor I) : WeilDivisor X

AlgebraicGeometry.effectiveCartierWeilDivisor_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierWeilDivisor.lean, line 323. The attribute's comment: “effective_cartier_weil_divisor”.

Stacks 02AR part (5). The coefficient of [D] at a prime divisor is the order v_Z(D).

theorem effectiveCartierWeilDivisor_apply [IsNoetherian X] [IsIntegral X]
    (I : X.IdealSheafData) (hI : Stacks.Divisors.IsEffectiveCartierDivisor I)
    (Z : PrimeDivisor X) :
    (effectiveCartierWeilDivisor I hI).1 Z = effectiveCartierMultiplicity I Z

AlgebraicGeometry.effectiveCartierWeilDivisor_apply_of_notMem_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierWeilDivisor.lean, line 331. The attribute's comment: “effective_cartier_weil_divisor”.

Stacks 02AR part (5), clause (a). The coefficient of [D] at a prime divisor whose generic point lies outside D is zero.

theorem effectiveCartierWeilDivisor_apply_of_notMem_support [IsNoetherian X] [IsIntegral X]
    (I : X.IdealSheafData) (hI : Stacks.Divisors.IsEffectiveCartierDivisor I)
    (Z : PrimeDivisor X) (hZ : Z.genericPoint ∉ I.support) :
    (effectiveCartierWeilDivisor I hI).1 Z = 0

AlgebraicGeometry.effectiveCartierWeilDivisor_apply_of_ideal_eq_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierWeilDivisor.lean, line 352. The attribute's comment: “effective_cartier_weil_divisor”.

Stacks 02AR part (5), clause (b). When the generic point of Z lies in D, the coefficient of [D] at Z is the length of 𝒪_{X, Z} / (f) for the nonzerodivisor f that defines D on an affine open neighbourhood of that generic point, as in part (4).

theorem effectiveCartierWeilDivisor_apply_of_ideal_eq_span [IsNoetherian X] [IsIntegral X]
    {I : X.IdealSheafData} (hI : Stacks.Divisors.IsEffectiveCartierDivisor I)
    (Z : PrimeDivisor X) {U : X.affineOpens} (hxU : Z.genericPoint ∈ U.1) {f : Γ(X, U.1)}
    (hf : I.ideal U = Ideal.span {f}) :
    (effectiveCartierWeilDivisor I hI).1 Z =
      ((Module.length (X.presheaf.stalk Z.genericPoint)
        ((X.presheaf.stalk Z.genericPoint) ⧸
          Ideal.span {(X.presheaf.germ U.1 Z.genericPoint hxU).hom f})).toNat : ℤ)

AlgebraicGeometry.Scheme.totalQuotientSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TotalQuotient.lean, line 83. The attribute's comment: “total_quotient_sheaf”. References: EGA IV (20.1.3).

The sheaf of total quotient rings of a scheme. It is the sheafification of the presheaf which, on each open set, localizes the ring of regular functions at the sections whose germs are nonzerodivisors everywhere on that open set.

noncomputable abbrev Scheme.totalQuotientSheaf (Y : Scheme.{u}) :
    TopCat.Sheaf CommRingCat.{u} Y

AlgebraicGeometry.Scheme.toTotalQuotientSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TotalQuotient.lean, line 90. The attribute's comment: “total_quotient_sheaf”.

The canonical morphism from the structure sheaf to the sheaf of total quotient rings, giving the latter its structure as a sheaf of 𝒪_X-algebras.

noncomputable def Scheme.toTotalQuotientSheaf (Y : Scheme.{u}) :
    Y.sheaf ⟶ Y.totalQuotientSheaf

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Scheme.mono_toTotalQuotientSheaf · AlgebraicGeometry.Scheme.shortExact_unitGroupSheaf · AlgebraicGeometry.Scheme.CartierDivisor · AlgebraicGeometry.exists_affineOpen_local_representation · AlgebraicGeometry.cartierWeilDivisor · AlgebraicGeometry.cartierWeilDivisor_apply · AlgebraicGeometry.cartierWeilDivisor_apply_of_germ_eq_zero · AlgebraicGeometry.cartierWeilDivisor_apply_of_local_eq

Section111.52 Schemes, Final Exam, Spring 2009#

Section 111.52 of the Stacks Project, Tag 02AV. 1 tag here is carried by 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02AX, a remark

Tag 02AX in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.ProjectiveSpectrum.Proj.twistSheafOfModules

Section111.56 Schemes, Final Exam, Fall 2013#

Section 111.56 of the Stacks Project, Tag 09TV. 1 tag here is carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09U0, a situation

Tag 09U0 in the Stacks Project.

Stacks.Divisors.IsDivisorOfRationalDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MeromorphicOrder/RationalDifferential.lean, line 79. The attribute's comment: “the divisor of zeros and poles of ω”.

Stacks 09U0. A Weil divisor D on X is the divisor of zeros and poles of the rational differential ω ∈ Ω[K⁄k], read through an identification e of K with the function field of X, when its coefficient at every prime divisor Z is the order of vanishing at Z of every g for which ω = g · dt with t of order one at Z.

On a nonsingular projective curve over a field, taking ω to be the distinguished differential of an irreducible plane curve makes this the canonical divisor K_C.

def IsDivisorOfRationalDifferential (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
    (e : K ≃+* X.functionField) (ω : Ω[K⁄k]) (D : WeilDivisor X) : Prop

Stacks.Divisors.isDivisorOfRationalDifferential_weilDivisorOfMeromorphicSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MeromorphicOrder/RationalDifferential.lean, line 96. The attribute's comment: “the divisor of zeros and poles of ω”.

Stacks 09U0. The divisor of zeros and poles of a rational differential exists as soon as the differential is realized in an invertible module.

Let L be a module on X that is trivialized near every point, and let E realize the rational differentials of K over k inside the generic stalk of L, semilinearly over the identification e of K with R(X). If dt is realized by a basis of the stalk of L at the generic point of Z whenever t has order one at Z — which is the local structure of the sheaf of differentials on a nonsingular curve — then the Weil divisor of E ω, regarded as a meromorphic section of L, is the divisor of zeros and poles of ω.

theorem isDivisorOfRationalDifferential_weilDivisorOfMeromorphicSection
    (hL : ∀ x : X, IsTrivializedNear L x) (e : K ≃+* X.functionField)
    (E : Ω[K⁄k] →+ L.presheaf.stalk (genericPoint X))
    (hE : ∀ (g : K) (ν : Ω[K⁄k]), E (g • ν) = e g • E ν) (ω : Ω[K⁄k])
    (hbasis : ∀ (Z : PrimeDivisor X) (t : K), X.ord (e t) Z.genericPoint = 1 →
      ∃ m : L.presheaf.stalk Z.genericPoint, IsStalkBasis L Z.genericPoint m ∧
        toGenericStalk L Z.genericPoint m = E (KaehlerDifferential.D k K t)) :
    IsDivisorOfRationalDifferential X e ω (weilDivisorOfMeromorphicSection hL (E ω))

Stacks.Divisors.exists_isDivisorOfRationalDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MeromorphicOrder/RationalDifferential.lean, line 113. The attribute's comment: “the divisor of zeros and poles of ω”.

Stacks 09U0. A rational differential realized in a module trivialized near every point, whose exact differentials at uniformizers are bases of the stalks, has a divisor of zeros and poles.

theorem exists_isDivisorOfRationalDifferential
    (hL : ∀ x : X, IsTrivializedNear L x) (e : K ≃+* X.functionField)
    (E : Ω[K⁄k] →+ L.presheaf.stalk (genericPoint X))
    (hE : ∀ (g : K) (ν : Ω[K⁄k]), E (g • ν) = e g • E ν) (ω : Ω[K⁄k])
    (hbasis : ∀ (Z : PrimeDivisor X) (t : K), X.ord (e t) Z.genericPoint = 1 →
      ∃ m : L.presheaf.stalk Z.genericPoint, IsStalkBasis L Z.genericPoint m ∧
        toGenericStalk L Z.genericPoint m = E (KaehlerDifferential.D k K t)) :
    ∃ D : WeilDivisor X, IsDivisorOfRationalDifferential X e ω D

AlgebraicGeometry.AffinePlaneCurve.partialX_ne_zero_or_partialY_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 358. The attribute's comment: “well-definedness of ω: a partial derivative survives”.

Stacks 09U0. At least one of the two partial derivatives of an irreducible plane equation over a perfect field is nonzero in the function field of the curve it cuts out. This is what makes the differential ω = dx/f_y = -dy/f_x well defined.

theorem partialX_ne_zero_or_partialY_ne_zero [PerfectField k] :
    C.partialX ≠ 0 ∨ C.partialY ≠ 0

AlgebraicGeometry.AffinePlaneCurve.inv_partialY_smul_D_x_eq_neg_inv_partialX_smul_D_y, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 486. The attribute's comment: “well-definedness of ω: the two formulas agree”.

Stacks 09U0. Where both partial derivatives are nonzero, the two formulas dx/f_y and -dy/f_x for the distinguished differential agree.

theorem inv_partialY_smul_D_x_eq_neg_inv_partialX_smul_D_y
    (hx : C.partialX ≠ 0) (hy : C.partialY ≠ 0) :
    C.partialY⁻¹ • KaehlerDifferential.D k C.FunctionField C.x =
      -(C.partialX⁻¹ • KaehlerDifferential.D k C.FunctionField C.y)

AlgebraicGeometry.AffinePlaneCurve.inv_partialY_smul_D_x_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 505. The attribute's comment: “well-definedness of ω: dx/f_y is nonzero”.

Stacks 09U0. If the partial derivative with respect to y is nonzero, then dx/f_y is a nonzero differential.

theorem inv_partialY_smul_D_x_ne_zero (hy : C.partialY ≠ 0) :
    C.partialY⁻¹ • KaehlerDifferential.D k C.FunctionField C.x ≠ 0

AlgebraicGeometry.AffinePlaneCurve.neg_inv_partialX_smul_D_y_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 512. The attribute's comment: “well-definedness of ω: -dy/f_x is nonzero”.

Stacks 09U0. If the partial derivative with respect to x is nonzero, then -dy/f_x is a nonzero differential.

theorem neg_inv_partialX_smul_D_y_ne_zero (hx : C.partialX ≠ 0) :
    -(C.partialX⁻¹ • KaehlerDifferential.D k C.FunctionField C.y) ≠ 0

AlgebraicGeometry.AffinePlaneCurve.differential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 521. The attribute's comment: “the differential ω”.

Stacks 09U0. The distinguished rational differential ω = dx/f_y = -dy/f_x of an irreducible affine plane curve.

def differential : Ω[C.FunctionField⁄k]

AlgebraicGeometry.AffinePlaneCurve.differential_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 542. The attribute's comment: “ω is nonzero”.

Stacks 09U0. The distinguished differential of an irreducible plane curve over a perfect field is nonzero.

theorem differential_ne_zero [PerfectField k] : C.differential ≠ 0

AlgebraicGeometry.ProjectivePlaneCurve, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 562. The attribute's comment: “the plane-curve situation”.

Stacks 09U0. An irreducible projective plane curve D = V(F) over a field, together with the affine plane curve cut out on the standard chart X₀ = 1 by the dehomogenization f(x, y) = F(1, x, y).

The irreducibility of the dehomogenization is carried as a field rather than deduced from the irreducibility of F and the assumption that F is not a scalar multiple of the first coordinate.

structure ProjectivePlaneCurve (k : Type u) [Field k]

AlgebraicGeometry.ProjectivePlaneCurve.curve, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 606. The attribute's comment: “the projective plane curve D = V(F)”.

Stacks 09U0. The projective plane curve D = V(F), as the reduced induced closed subscheme of the projective plane on the vanishing set of F.

def curve : Scheme.{u}

AlgebraicGeometry.ProjectivePlaneCurve.inclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 612. The attribute's comment: “the closed immersion of D into the projective plane”.

Stacks 09U0. The closed immersion of the projective plane curve into the projective plane.

def inclusion : D.curve ⟶ D.projectivePlane

AlgebraicGeometry.ProjectivePlaneCurve.differential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PlaneCurveDifferential.lean, line 618. The attribute's comment: “the differential ω of the plane curve”.

Stacks 09U0. The distinguished rational differential ω = dx/f_y = -dy/f_x of the plane curve, taken on its standard affine chart.

def differential : Ω[D.affineChart.FunctionField⁄k]
Sources
LeanStacks.Divisors.IsDivisorOfRationalDifferential · Stacks.Divisors.isDivisorOfRationalDifferential_weilDivisorOfMeromorphicSection · Stacks.Divisors.exists_isDivisorOfRationalDifferential · AlgebraicGeometry.AffinePlaneCurve.partialX_ne_zero_or_partialY_ne_zero · AlgebraicGeometry.AffinePlaneCurve.inv_partialY_smul_D_x_eq_neg_inv_partialX_smul_D_y · AlgebraicGeometry.AffinePlaneCurve.inv_partialY_smul_D_x_ne_zero · AlgebraicGeometry.AffinePlaneCurve.neg_inv_partialX_smul_D_y_ne_zero · AlgebraicGeometry.AffinePlaneCurve.differential

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.