Other results

Results named in the rest of Tau Ceti's TauCeti.AlgebraicGeometry modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremAlgebraic Hartogs principle#

Let a, b be a weakly M-regular sequence. If D(a) and D(b) lie in the open subset U of Spec R, then M → M~(U) is bijective: every section of M~ over U comes from a unique element of M.

TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_isWeaklyRegular.{u} {R M : Type u}
  [CommRing R] [AddCommGroup M] [_root_.Module R M]
  {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} {a b : R}
  (h : RingTheory.Sequence.IsWeaklyRegular M [a, b]) (haU : PrimeSpectrum.basicOpen a ≤ U)
  (hbU : PrimeSpectrum.basicOpen b ≤ U) :
  Function.Bijective ⇑(AlgebraicGeometry.StructureSheaf.toOpenₗ R M U)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_isWeaklyRegular.

Sources
LeanTauCeti.AlgebraicGeometry.StructureSheaf.toOpenₗ_bijective_of_isWeaklyRegular

TheoremDeligne's theorem (TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank)#

Let G be a finite locally free commutative group scheme over S whose rank is n at every point of S. Then every point x : X ⟶ G over S is killed by n: its n-th power in the group of X-valued points of G is the unit.

TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank.{u}
  {S : AlgebraicGeometry.Scheme} (G : TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme S) {n : ℕ}
  (hn : ∀ (s : ↥S), AlgebraicGeometry.Scheme.Hom.finrank G.structureMap s = n)
  {X : CategoryTheory.Over S} (x : X ⟶ G.toOver) : x ^ n = 1
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank.

Sources
LeanTauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank
Uses 1 · Used by 1
Proof usesDeligne's theorem (TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk)
Used byTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy

TheoremKrull's principal ideal theorem on a scheme#

A maximal point of the zero locus of a nonzero global function on an integral locally Noetherian scheme, that is, the generic point of an irreducible component of that zero locus, has coheight one.

TauCeti.AlgebraicGeometry.Scheme.coheight_eq_one_of_maximal_mem_zeroLocus.{u}
  {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X]
  [AlgebraicGeometry.IsIntegral X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (ha : a ≠ 0) {x : ↥X}
  (hx : Maximal (fun x => x ∈ X.zeroLocus {a}) x) : Order.coheight x = 1
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.Scheme.coheight_eq_one_of_maximal_mem_zeroLocus.

Sources
LeanTauCeti.AlgebraicGeometry.Scheme.coheight_eq_one_of_maximal_mem_zeroLocus

TheoremThe Riemann–Roch theorem for line bundles, in Serre-duality form#

For every line bundle L and every representative ω of the canonical class,

dim H⁰(X, L) - dim H⁰(X, ω ⊗ L⁻¹) = deg L + 1 - g,

where deg L = χ(L) - χ(𝒪_X) is the Euler-characteristic degree and g = dim H¹(X, 𝒪_X). No rational point is needed: it is the integral closedness of k in k(X) that makes H⁰(X, 𝒪_X) one-dimensional.

TauCeti.AlgebraicGeometry.InvertibleSheaf.finrank_cohomology_zero_sub_finrank_cohomology_zero_tensor_dual.{u}
  {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X]
  [∀ (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)]
  [X.IsSeparated]
  (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k))
  (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : TauCeti.IsFunctionField k ↑X.functionField)
  (hk : IsIntegrallyClosedIn k ↑X.functionField) (L ω : TauCeti.AlgebraicGeometry.InvertibleSheaf X)
  (hω :
    TauCeti.AlgebraicGeometry.LineBundleClass.mk ω =
      TauCeti.AlgebraicGeometry.LineBundleClass.mk
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.canonicalBundle hex hdim hF hk)) :
  ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology L.obj 0)) -
      ↑(Module.finrank k
          (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (ω.tensorProduct L.dual).obj 0)) =
    TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree k L + 1 -
      ↑(AlgebraicGeometry.Scheme.genus k X)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.InvertibleSheaf.finrank_cohomology_zero_sub_finrank_cohomology_zero_tensor_dual.

Sources
LeanTauCeti.AlgebraicGeometry.InvertibleSheaf.finrank_cohomology_zero_sub_finrank_cohomology_zero_tensor_dual
Uses 3 · Used by 1
Proof usesRiemann's theorem · Serre duality in degree zero · The weak approximation theorem
Used byThe Riemann–Roch theorem with the sheaf of differentials

TheoremThe Riemann–Roch theorem on X_F in dimension form#

when k is integrally closed in F, dim_k H⁰(X_F, 𝒪(D)) - dim_k H¹(X_F, 𝒪(D)) = deg D + 1 - g(F).

TauCeti.AlgebraicGeometry.twoChartModel.finrank_cohomology_zero_sheaf_sub_finrank_cohomology_one_sheaf.{u}
  {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : TauCeti.IsFunctionField k F} {x : F}
  {hx : x ≠ 0} (hxt : Transcendental k x) (hk : IsIntegrallyClosedIn k F)
  (D :
    TauCeti.AlgebraicGeometry.SchemeWeilDivisor (TauCeti.AlgebraicGeometry.twoChartModel hF hx)) :
  ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 0)) -
      ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 1)) =
    TauCeti.Divisor.degree ((TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor hxt) D) + 1 -
      ↑(TauCeti.genus k F)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.twoChartModel.finrank_cohomology_zero_sheaf_sub_finrank_cohomology_one_sheaf.

Other forms

The Riemann–Roch theorem on X_F in Euler-characteristic form. Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.twoChartModel.eulerCharBelow_sheaf_eq_degree_add_one_sub_genus.

TauCeti.AlgebraicGeometry.twoChartModel.eulerCharBelow_sheaf_eq_degree_add_one_sub_genus.{u}
  {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : TauCeti.IsFunctionField k F} {x : F}
  {hx : x ≠ 0} (hxt : Transcendental k x) (hk : IsIntegrallyClosedIn k F)
  (D :
    TauCeti.AlgebraicGeometry.SchemeWeilDivisor (TauCeti.AlgebraicGeometry.twoChartModel hF hx)) :
  AlgebraicGeometry.Scheme.Modules.eulerCharBelow k (TauCeti.AlgebraicGeometry.twoChartModel hF hx)
      D.sheaf 2 =
    TauCeti.Divisor.degree ((TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor hxt) D) + 1 -
      ↑(TauCeti.genus k F)
Sources
LeanTauCeti.AlgebraicGeometry.twoChartModel.finrank_cohomology_zero_sheaf_sub_finrank_cohomology_one_sheaf · TauCeti.AlgebraicGeometry.twoChartModel.eulerCharBelow_sheaf_eq_degree_add_one_sub_genus
Uses 4
Proof usesKrull–Akizuki for Mathlib's integralClosure · Riemann's theorem · TauCeti.Ring.IsJapanese · The weak approximation theorem

TheoremSerre duality in degree zero#

The dual of H⁰(X, L) is linearly isomorphic to H¹(X, ω ⊗ L⁻¹) for any representative ω of the canonical class.

TauCeti.AlgebraicGeometry.InvertibleSheaf.nonempty_cohomologyZeroDualEquivCohomologyOne_tensor_dual.{u}
  {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X]
  [∀ (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)]
  [X.IsSeparated]
  (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k))
  (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : TauCeti.IsFunctionField k ↑X.functionField)
  (hk : IsIntegrallyClosedIn k ↑X.functionField) (L ω : TauCeti.AlgebraicGeometry.InvertibleSheaf X)
  (hω :
    TauCeti.AlgebraicGeometry.LineBundleClass.mk ω =
      TauCeti.AlgebraicGeometry.LineBundleClass.mk
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.canonicalBundle hex hdim hF hk)) :
  Nonempty
    (Module.Dual k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology L.obj 0) ≃ₗ[k]
      TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (ω.tensorProduct L.dual).obj 1)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.InvertibleSheaf.nonempty_cohomologyZeroDualEquivCohomologyOne_tensor_dual.

Other forms

Serre duality for line bundles. Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.InvertibleSheaf.nonempty_cohomologyOneDualEquivCohomologyZero_tensor_dual.

TauCeti.AlgebraicGeometry.InvertibleSheaf.nonempty_cohomologyOneDualEquivCohomologyZero_tensor_dual.{u}
  {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X]
  [∀ (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)]
  [X.IsSeparated]
  (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k))
  (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : TauCeti.IsFunctionField k ↑X.functionField)
  (hk : IsIntegrallyClosedIn k ↑X.functionField) (L ω : TauCeti.AlgebraicGeometry.InvertibleSheaf X)
  (hω :
    TauCeti.AlgebraicGeometry.LineBundleClass.mk ω =
      TauCeti.AlgebraicGeometry.LineBundleClass.mk
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.canonicalBundle hex hdim hF hk)) :
  Nonempty
    (Module.Dual k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology L.obj 1) ≃ₗ[k]
      TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (ω.tensorProduct L.dual).obj 0)
Sources
LeanTauCeti.AlgebraicGeometry.InvertibleSheaf.nonempty_cohomologyZeroDualEquivCohomologyOne_tensor_dual · TauCeti.AlgebraicGeometry.InvertibleSheaf.nonempty_cohomologyOneDualEquivCohomologyZero_tensor_dual
Uses 3 · Used by 2
Proof usesThe duality theorem, in dimensions · Riemann's theorem · The weak approximation theorem
Used byThe Riemann–Roch theorem for line bundles, in Serre-duality form · TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual

TheoremSerre duality on X_F, in dimensions#

for every divisor K on X_F whose image in F represents canonicalClass hF hk, dim_k H¹(X_F, 𝒪(D)) = dim_k H⁰(X_F, 𝒪(K - D)).

TauCeti.AlgebraicGeometry.twoChartModel.finrank_cohomology_one_sheaf_eq_finrank_cohomology_zero_sheaf_sub.{u}
  {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : TauCeti.IsFunctionField k F} {x : F}
  {hx : x ≠ 0} (hxt : Transcendental k x) (hk : IsIntegrallyClosedIn k F)
  {K : TauCeti.AlgebraicGeometry.SchemeWeilDivisor (TauCeti.AlgebraicGeometry.twoChartModel hF hx)}
  (hK :
    (TauCeti.Place.orderSystem hF).divisorClass
        ((TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor hxt) K) =
      TauCeti.canonicalClass hF hk)
  (D :
    TauCeti.AlgebraicGeometry.SchemeWeilDivisor (TauCeti.AlgebraicGeometry.twoChartModel hF hx)) :
  Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 1) =
    Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (K - D).sheaf 0)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.twoChartModel.finrank_cohomology_one_sheaf_eq_finrank_cohomology_zero_sheaf_sub.

Sources
LeanTauCeti.AlgebraicGeometry.twoChartModel.finrank_cohomology_one_sheaf_eq_finrank_cohomology_zero_sheaf_sub
Uses 5
Proof usesKrull–Akizuki for Mathlib's integralClosure · Riemann's theorem · Serre duality, in dimensions · TauCeti.Ring.IsJapanese · The weak approximation theorem

TheoremSerre duality, in dimensions#

Assume k is integrally closed in k(X). For every canonical divisor K on the curve X (a divisor whose function-field divisor represents the canonical class) and every Weil divisor D, dim_k H¹(X, 𝒪_X(D)) = dim_k H⁰(X, 𝒪_X(K - D)).

TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_one_sheaf_eq_finrank_cohomology_zero_sheaf_sub.{u}
  {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsIntegral X]
  [∀ (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)]
  [X.IsSeparated]
  (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k))
  (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) [AlgebraicGeometry.IsNoetherian X]
  (hF : TauCeti.IsFunctionField k ↑X.functionField) (hk : IsIntegrallyClosedIn k ↑X.functionField)
  {K : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X}
  (hK :
    (TauCeti.Place.orderSystem hF).divisorClass
        ((TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor hex hdim) K) =
      TauCeti.canonicalClass hF hk)
  (D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X) :
  Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 1) =
    Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (K - D).sheaf 0)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_one_sheaf_eq_finrank_cohomology_zero_sheaf_sub.

Sources
LeanTauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_one_sheaf_eq_finrank_cohomology_zero_sheaf_sub
Uses 3 · Used by 1
Proof usesThe duality theorem, in dimensions · Riemann's theorem · The weak approximation theorem
Used bySerre duality on X_F, in dimensions

TheoremSerre's vanishing theorem on affine opens#

Serre's vanishing theorem on affine opens (Hartshorne, Algebraic Geometry, Theorem III.3.5, without the Noetherian hypothesis): a sheaf of modules that is quasi-coherent over an affine open subset U of a scheme (for example, a quasi-coherent sheaf on the scheme) has no cohomology in positive degrees on U.

AlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_succ_of_isAffineOpen.{u}
  {X : AlgebraicGeometry.Scheme} (M : X.Modules) {U : X.Opens}
  (hU : AlgebraicGeometry.IsAffineOpen U) [SheafOfModules.IsQuasicoherent (M.restrict U.ι)]
  (n : ℕ) : Subsingleton ↑(TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOn M (n + 1) U)
Lean

Formalized in Tau Ceti as AlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_succ_of_isAffineOpen.

Other forms

Serre's vanishing theorem on affine schemes. Formalized in Tau Ceti as AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_succ_of_isAffine.

AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_succ_of_isAffine.{u}
  {X : AlgebraicGeometry.Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M]
  [AlgebraicGeometry.IsAffine X] (n : ℕ) :
  Subsingleton (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M (n + 1))
Sources
LeanAlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_succ_of_isAffineOpen · AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_succ_of_isAffine
Uses 1 · Used by 2
Proof usesCartan's criterion
Used byThe Abel–Jacobi map into the degree-zero Picard fppf sheaf · The Abel–Jacobi map of a curve of positive genus separates points over every field extension

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.