Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.Scheme.PrincipalParts.RepartitionCohomology

First cohomology as a repartition quotient #

Let X be an integral separated Noetherian curve over a field k, with its codimension-one points identified with the places of k(X). The global principal parts of a divisor D are the quotient of the repartition space A_{k(X)} by its divisor filtration A_{k(X)}(D), while first cohomology is the quotient of those principal parts by global rational functions. This file combines the two quotient descriptions:

Hยน(X, ๐’ช_X(D)) โ‰ƒ A_{k(X)} / (A_{k(X)}(D) + k(X)).

The right-hand side is finite-dimensional for an algebraic function field. Consequently this gives finite-dimensionality of Hยน(X, ๐’ช_X(D)) on the curves to which the scheme/function-field comparison applies. Since the Weil differentials bounded by D are by definition the linear forms on repartitions vanishing on A_{k(X)}(D) + k(X), it also identifies the dual of Hยน(X, ๐’ช_X(D)) with the space ฮฉ(D) of such differentials.

Main declarations #

References #

source
theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.nonemptyTopOpensRepartitionCohomology {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] :
Nonempty โ†ฅโ†‘โŠค

The top open of an integral scheme is nonempty.

source
noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.diagonalRationalFunctionsToRepartitions {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] (hF : IsFunctionField k โ†‘X.functionField) :
โ†‘((Scheme.rationalFunctions X).presheaf.obj (Opposite.op โŠค)) โ†’โ‚—[k] โ†ฅ(repartitionSpace k โ†‘X.functionField)

Global rational functions, viewed as diagonal elements of the repartition space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.diagonalRationalFunctionsToRepartitions_apply {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] {hF : IsFunctionField k โ†‘X.functionField} (f : โ†‘((Scheme.rationalFunctions X).presheaf.obj (Opposite.op โŠค))) :
    โ†‘((diagonalRationalFunctionsToRepartitions hF) f) = Function.const (Place k โ†‘X.functionField) ((Scheme.rationalFunctionsEquiv โŠค) f)
    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.range_diagonalRationalFunctionsToRepartitions {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] (hF : IsFunctionField k โ†‘X.functionField) :
    (diagonalRationalFunctionsToRepartitions hF).range = (diagonalRepartitions k โ†‘X.functionField).submoduleOf (repartitionSpace k โ†‘X.functionField)

    The image of global rational functions is the diagonal inside the repartition space.

    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.diagonalRationalFunctionsToRepartitions_injective {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] (hF : IsFunctionField k โ†‘X.functionField) :
    Function.Injective โ‡‘(diagonalRationalFunctionsToRepartitions hF)

    Global rational functions embed into the repartition space diagonally.

    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToPrincipalParts_diagonalRationalFunctionsToRepartitions {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) {hF : IsFunctionField k โ†‘X.functionField} (D : SchemeWeilDivisor X) (f : โ†‘((Scheme.rationalFunctions X).presheaf.obj (Opposite.op โŠค))) :
    (repartitionToPrincipalParts hex hdim D) ((diagonalRationalFunctionsToRepartitions hF) f) = (globalToPrincipalPartsBaseLinear k D) f

    Taking principal parts of the diagonal repartition of a global rational function recovers the usual global principal-parts map.

    source
    noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToCohomologyOne {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (D : SchemeWeilDivisor X) :
    โ†ฅ(repartitionSpace k โ†‘X.functionField) โ†’โ‚—[k] Scheme.Modules.Cohomology D.sheaf 1

    The first cohomology class represented by a repartition.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToCohomologyOne_apply {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (D : SchemeWeilDivisor X) (a : โ†ฅ(repartitionSpace k โ†‘X.functionField)) :
      (repartitionToCohomologyOne hex hdim D) a = (principalPartsBoundary k โ‹ฏ D) ((repartitionToPrincipalParts hex hdim D) a)
      source
      theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToCohomologyOne_surjective {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (D : SchemeWeilDivisor X) :
      Function.Surjective โ‡‘(repartitionToCohomologyOne hex hdim D)

      Every first cohomology class is represented by a repartition.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsBoundary_repartitionToPrincipalParts_diagonalRationalFunctionsToRepartitions {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) {hF : IsFunctionField k โ†‘X.functionField} (D : SchemeWeilDivisor X) (f : โ†‘((Scheme.rationalFunctions X).presheaf.obj (Opposite.op โŠค))) :
      (principalPartsBoundary k โ‹ฏ D) ((repartitionToPrincipalParts hex hdim D) ((diagonalRationalFunctionsToRepartitions hF) f)) = 0

      The cohomology class of the diagonal repartition of a global rational function vanishes.

      source
      theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ker_repartitionToCohomologyOne {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (hF : IsFunctionField k โ†‘X.functionField) (D : SchemeWeilDivisor X) :
      (repartitionToCohomologyOne hex hdim D).ker = submoduleOfAdeleFiltrationSupDiagonalRepartitions ((equivFunctionFieldDivisor hex hdim) D)

      The repartitions representing the zero class in Hยน(X, ๐’ช_X(D)) are exactly the sums of a repartition bounded by D and a diagonal rational function.

      source
      noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionQuotientEquivCohomologyOne {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (hF : IsFunctionField k โ†‘X.functionField) (D : SchemeWeilDivisor X) :
      (โ†ฅ(repartitionSpace k โ†‘X.functionField) โงธ submoduleOfAdeleFiltrationSupDiagonalRepartitions ((equivFunctionFieldDivisor hex hdim) D)) โ‰ƒโ‚—[k] Scheme.Modules.Cohomology D.sheaf 1

      First cohomology as a repartition quotient. The quotient of the repartition space by the divisor filtration and diagonal rational functions is linearly equivalent to Hยน(X, ๐’ช_X(D)).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionQuotientEquivCohomologyOne_mk {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (hF : IsFunctionField k โ†‘X.functionField) (D : SchemeWeilDivisor X) (a : โ†ฅ(repartitionSpace k โ†‘X.functionField)) :
        (repartitionQuotientEquivCohomologyOne hex hdim hF D) (Submodule.Quotient.mk a) = (repartitionToCohomologyOne hex hdim D) a

        The repartition-quotient equivalence sends the class of a repartition to its first cohomology class.

        source
        noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.cohomologyOneDualEquivWeilDifferentialFiltration {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (hF : IsFunctionField k โ†‘X.functionField) (D : SchemeWeilDivisor X) :
        Module.Dual k (Scheme.Modules.Cohomology D.sheaf 1) โ‰ƒโ‚—[k] โ†ฅ(weilDifferentialFiltration ((equivFunctionFieldDivisor hex hdim) D))

        The dual of Hยน(X, ๐’ช_X(D)) is the space ฮฉ(D) of Weil differentials bounded by D. First cohomology is the repartition quotient A_{k(X)} / (A_{k(X)}(D) + k(X)), whose linear forms are the linear forms on repartitions vanishing on A_{k(X)}(D) + k(X).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.cohomologyOneDualEquivWeilDifferentialFiltration_apply_apply {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (hF : IsFunctionField k โ†‘X.functionField) (D : SchemeWeilDivisor X) (ฯ† : Module.Dual k (Scheme.Modules.Cohomology D.sheaf 1)) (a : โ†ฅ(repartitionSpace k โ†‘X.functionField)) :
          โ†‘((cohomologyOneDualEquivWeilDifferentialFiltration hex hdim hF D) ฯ†) a = ฯ† ((repartitionToCohomologyOne hex hdim D) a)

          The Weil differential attached to a linear form ฯ† on Hยน(X, ๐’ช_X(D)) evaluates a repartition by applying ฯ† to its cohomology class.

          source
          theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finiteDimensional_cohomology_one_sheaf_of_isFunctionField {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec โ†งk)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] [โˆ€ (x : CodimensionOnePoint X), IsDiscreteValuationRing โ†‘(X.presheaf.stalk โ†‘x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X โ†˜ AlgebraicGeometry.Spec โ†งk)) (hdim : โˆ€ (x : โ†ฅX), Order.coheight x โ‰ค 1) (hF : IsFunctionField k โ†‘X.functionField) (D : SchemeWeilDivisor X) :
          FiniteDimensional k (Scheme.Modules.Cohomology D.sheaf 1)

          The first cohomology of a divisor sheaf is finite-dimensional.