Algebraic curves — function fields, divisors, and Riemann–Roch

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself#

the divisor of a nonzero Weil differential is a Riemann–Roch divisor for the genus.

TauCeti.isRiemannRochDivisor_weilDifferentialDivisor.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(TauCeti.repartitionSpace k F)}
  (hmem : ω ∈ TauCeti.weilDifferentialSpace k F) (hω : ω ≠ 0) :
  (TauCeti.weilDifferentialDivisor hF hex hmem hω).IsRiemannRochDivisor (TauCeti.genus k F)

Lean

Formalized in Tau Ceti as TauCeti.isRiemannRochDivisor_weilDifferentialDivisor.

Other forms

Riemann--Roch in high degree (Stichtenoth, Theorem 1.5.17). Formalized in Tau Ceti as TauCeti.Divisor.dim_eq_degree_add_one_sub_genus_of_two_mul_genus_sub_one_le_degree.

TauCeti.Divisor.dim_eq_degree_add_one_sub_genus_of_two_mul_genus_sub_one_le_degree.{u_1, u_2}
  {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {D : TauCeti.Divisor k F}
  (hD : 2 * ↑(TauCeti.genus k F) - 1 ≤ TauCeti.Divisor.degree D) :
  ↑D.dim = TauCeti.Divisor.degree D + 1 - ↑(TauCeti.genus k F)

The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15). Formalized in Tau Ceti as TauCeti.isRiemannRochDivisor_of_isGreatest_mem_weilDifferentialFiltration.

TauCeti.isRiemannRochDivisor_of_isGreatest_mem_weilDifferentialFiltration.{u_1, u_2} {k : Type u_1}
  {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(TauCeti.repartitionSpace k F)} (hω : ω ≠ 0)
  {W : TauCeti.Divisor k F} (hW : IsGreatest {D | ω ∈ TauCeti.weilDifferentialFiltration D} W) :
  W.IsRiemannRochDivisor (TauCeti.genus k F)

The Riemann–Roch theorem, existence form (Stichtenoth, Theorem 1.5.15). Formalized in Tau Ceti as TauCeti.exists_isRiemannRochDivisor.

TauCeti.exists_isRiemannRochDivisor.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k] [Field F]
  [Algebra k F] (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) :
  ∃ W, W.IsRiemannRochDivisor (TauCeti.genus k F)

Sources

• Tau Ceti documentation: TauCeti.isRiemannRochDivisor_weilDifferentialDivisor
• Source of TauCeti.isRiemannRochDivisor_weilDifferentialDivisor in TauCeti/FieldTheory/FunctionField/Differential/CanonicalDivisor.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.isRiemannRochDivisor_weilDifferentialDivisor · TauCeti.Divisor.dim_eq_degree_add_one_sub_genus_of_two_mul_genus_sub_one_le_degree · TauCeti.isRiemannRochDivisor_of_isGreatest_mem_weilDifferentialFiltration · TauCeti.exists_isRiemannRochDivisor

Uses 3 · Used by 15

Proof usesThe duality theorem, in dimensions · Riemann's theorem · The weak approximation theorem

Used byThe Hurwitz genus formula for y² = x³ - x over K(x), as a numerical identity · A curve of genus zero with a divisor of degree one has nodal reduction · TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The Abel–Jacobi map of a curve of positive genus separates points over every field extension · The Riemann–Roch theorem · The Riemann–Roch theorem with the sheaf of differentials · High powers of a transcendental function have pole divisors whose section ring is generated in degree one · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3) · Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3) · Clifford's theorem · Riemann's inequality (Stichtenoth, Corollary 3.11.4) · The residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x)) · Weierstrass gap theorem (Stichtenoth, Theorem 1.6.8)

TheoremThe Hurwitz genus formula (Stichtenoth, Theorem 3.4.13)#

for a finite separable extension F' / k' of the function field F / k, both with exact constants and with k' / k finite separable, [k' : k] · (2g' - 2) = [F' : F] · (2g - 2) + [k' : k] · deg Diff(F'/F).

TauCeti.hurwitz_genus_formula.{u, u', v, v'} {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'}
  [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F']
  [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F'] [FiniteDimensional k k']
  [Algebra.IsSeparable k k'] (hF : TauCeti.IsFunctionField k F)
  (hF' : TauCeti.IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F)
  (hex' : IsIntegrallyClosedIn k' F') :
  ↑(Module.finrank k k') * (2 * ↑(TauCeti.genus k' F') - 2) =
    ↑(Module.finrank F F') * (2 * ↑(TauCeti.genus k F) - 2) +
      ↑(Module.finrank k k') * TauCeti.Divisor.degree (TauCeti.Divisor.different k' F' hF)

Lean

Formalized in Tau Ceti as TauCeti.hurwitz_genus_formula.

Other forms

The Hurwitz genus formula over a rational subfield (Stichtenoth, Corollary 3.4.14). Formalized in Tau Ceti as TauCeti.hurwitz_genus_formula_ratFunc.

TauCeti.hurwitz_genus_formula_ratFunc.{u, v} {k : Type u} {F : Type v} [Field k] [Field F]
  [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F]
  [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F]
  (hex : IsIntegrallyClosedIn k F) :
  2 * ↑(TauCeti.genus k F) - 2 =
    -2 * ↑(Module.finrank (RatFunc k) F) + TauCeti.Divisor.degree (TauCeti.Divisor.different k F ⋯)

The Hurwitz genus formula through the geometric degree (Stichtenoth, Theorem 3.4.13). Formalized in Tau Ceti as TauCeti.hurwitz_genus_formula_geometricDegree.

TauCeti.hurwitz_genus_formula_geometricDegree.{u, u', v, v'} {k : Type u} {k' : Type u'}
  {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F]
  [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F'] [FiniteDimensional k k']
  [Algebra.IsSeparable k k'] (hF : TauCeti.IsFunctionField k F)
  (hF' : TauCeti.IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F)
  (hex' : IsIntegrallyClosedIn k' F') :
  2 * ↑(TauCeti.genus k' F') - 2 =
    ↑(TauCeti.geometricDegree F k' F') * (2 * ↑(TauCeti.genus k F) - 2) +
      TauCeti.Divisor.degree (TauCeti.Divisor.different k' F' hF)

The Hurwitz genus formula, tame case (Stichtenoth, Corollary 3.5.6(b)). Formalized in Tau Ceti as TauCeti.two_mul_genus_sub_two_eq_iff_forall_isTame.

TauCeti.two_mul_genus_sub_two_eq_iff_forall_isTame.{u, u', v, v'} {k : Type u} {k' : Type u'}
  {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F]
  [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F'] [FiniteDimensional k k']
  [Algebra.IsSeparable k k'] (hF : TauCeti.IsFunctionField k F)
  (hF' : TauCeti.IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F)
  (hex' : IsIntegrallyClosedIn k' F') :
  2 * ↑(TauCeti.genus k' F') - 2 =
      ↑(TauCeti.geometricDegree F k' F') * (2 * ↑(TauCeti.genus k F) - 2) +
        TauCeti.Divisor.degree (TauCeti.Divisor.tameDifferent k' F' hF) ↔
    ∀ (P' : TauCeti.Place k' F'), TauCeti.Place.IsTame k F P'

The Hurwitz genus formula, tame lower bound (Stichtenoth, Corollary 3.5.6(a)). Formalized in Tau Ceti as TauCeti.geometricDegree_mul_add_degree_tameDifferent_le.

TauCeti.geometricDegree_mul_add_degree_tameDifferent_le.{u, u', v, v'} {k : Type u} {k' : Type u'}
  {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F]
  [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F'] [FiniteDimensional k k']
  [Algebra.IsSeparable k k'] (hF : TauCeti.IsFunctionField k F)
  (hF' : TauCeti.IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F)
  (hex' : IsIntegrallyClosedIn k' F') :
  ↑(TauCeti.geometricDegree F k' F') * (2 * ↑(TauCeti.genus k F) - 2) +
      TauCeti.Divisor.degree (TauCeti.Divisor.tameDifferent k' F' hF) ≤
    2 * ↑(TauCeti.genus k' F') - 2

Sources

• Tau Ceti documentation: TauCeti.hurwitz_genus_formula
• Source of TauCeti.hurwitz_genus_formula in TauCeti/FieldTheory/FunctionField/Different/Hurwitz.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.hurwitz_genus_formula · TauCeti.hurwitz_genus_formula_ratFunc · TauCeti.hurwitz_genus_formula_geometricDegree · TauCeti.two_mul_genus_sub_two_eq_iff_forall_isTame · TauCeti.geometricDegree_mul_add_degree_tameDifferent_le

Uses 6 · Used by 9

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The weak approximation theorem

Used byPerfect local Tate duality for E[m] · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · The genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3) · The Artin--Schreier genus formula, cross-multiplied for a possible constant-field extension · The Hurwitz bound (Stichtenoth, Exercise 3.18)

DefinitionThe anti-equivalence between regular proper curves and algebraic function fields over a field k#

the function-field functor X ↦ k(X) is an equivalence RegularProperCurveCat k ≌ (FunctionFieldCat k)ᵒᵖ with inverse the model functor F ↦ twoChartModel F.

TauCeti.AlgebraicGeometry.RegularProperCurveCat.equivFunctionFieldCat.{u} (k : Type u) [Field k] :
  TauCeti.AlgebraicGeometry.RegularProperCurveCat k ≌ (TauCeti.FunctionFieldCat k)ᵒᵖ

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.RegularProperCurveCat.equivFunctionFieldCat.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.RegularProperCurveCat.equivFunctionFieldCat
• Source of TauCeti.AlgebraicGeometry.RegularProperCurveCat.equivFunctionFieldCat in TauCeti/AlgebraicGeometry/Curves/TwoChartModel/AntiEquivalence.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.AlgebraicGeometry.RegularProperCurveCat.equivFunctionFieldCat

Uses 4

Proof usesKrull–Akizuki for Mathlib's integralClosure · Riemann's theorem · TauCeti.Ring.IsJapanese · The weak approximation theorem

TheoremAbhyankar's lemma (Stichtenoth, Theorem 3.9.1)#

Let E₁ and E₂ be intermediate fields of a finite separable extension F' / F of function fields, and P' a place of F' such that the residue field of the place P below it in F is perfect, for instance because k is perfect (TauCeti.Place.perfectField_residueField). If the ramification index of P' ∩ E₁ over P is nonzero in k, then the ramification index of P' ∩ E₁ E₂ over P is the least common multiple of those of P' ∩ E₁ and P' ∩ E₂.

In particular, if P' ∩ E₁ and P' ∩ E₂ have ramification index 1 over P, then so does P' ∩ E₁ E₂.

TauCeti.Place.ramificationIdx_restrict_sup.{u, v, w} {k : Type u} {F : Type v} {F' : Type w}
  [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : TauCeti.IsFunctionField k F)
  (P' : TauCeti.Place k F') [PerfectField (TauCeti.Place.restrict k F P').ResidueField]
  (E₁ E₂ : IntermediateField F F')
  (h₁ : ↑(TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥E₁) P')) ≠ 0) :
  TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥(E₁ ⊔ E₂)) P') =
    (TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥E₁) P')).lcm
      (TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥E₂) P'))

Lean

Formalized in Tau Ceti as TauCeti.Place.ramificationIdx_restrict_sup.

Other forms

Abhyankar's lemma in a Galois extension (Stichtenoth, Theorem 3.9.1). Formalized in Tau Ceti as TauCeti.Place.ramificationIdx_restrict_sup_of_isGalois.

TauCeti.Place.ramificationIdx_restrict_sup_of_isGalois.{u, v, w} {k : Type u} {F : Type v}
  {F' : Type w} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F']
  [IsScalarTower k F F'] [FiniteDimensional F F'] [IsGalois F F'] (Q : TauCeti.Place k F')
  [Algebra.IsSeparable (TauCeti.Place.restrict k F Q).ResidueField Q.ResidueField]
  (E₁ E₂ : IntermediateField F F')
  (h₁ : ↑(TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥E₁) Q)) ≠ 0) :
  TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥(E₁ ⊔ E₂)) Q) =
    (TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥E₁) Q)).lcm
      (TauCeti.Place.ramificationIdx F (TauCeti.Place.restrict k (↥E₂) Q))

Sources

• Tau Ceti documentation: TauCeti.Place.ramificationIdx_restrict_sup
• Source of TauCeti.Place.ramificationIdx_restrict_sup in TauCeti/FieldTheory/FunctionField/Place/Extension/Abhyankar.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.Place.ramificationIdx_restrict_sup · TauCeti.Place.ramificationIdx_restrict_sup_of_isGalois

Uses 5

Proof usesThe fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Galois correspondence for the inertia field · The residue action, on residues (Stichtenoth, Theorem 3.8.2) · The weak approximation theorem

TheoremThe genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3)#

let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d, with every point of G = 0 over an algebraically closed extension K of k nonsingular. Let F / k be generated by a transcendental x and an element y with G(x, y, 1) = 0. Then F has genus (d - 1)(d - 2) / 2.

Nonsingularity makes G(X₀, X₁, 1) irreducible over K, so k is the exact constant field of F (TauCeti.isIntegrallyClosedIn_of_irreducible_map).

TauCeti.genus_eq_of_isHomogeneous.{u_1, u_2, u_3} {k : Type u_1} [Field k] {F : Type u_2} [Field F]
  [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k}
  {d : ℕ} (hG : G.IsHomogeneous d)
  (hsm :
    ∀ (b : Fin 3 → K),
      b ≠ 0 →
        (MvPolynomial.aeval b) G = 0 → ∃ l, (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0)
  {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤)
  (h : (MvPolynomial.aeval ![x, y, 1]) G = 0) : TauCeti.genus k F = (d - 1) * (d - 2) / 2

Lean

Formalized in Tau Ceti as TauCeti.genus_eq_of_isHomogeneous.

Sources

• Tau Ceti documentation: TauCeti.genus_eq_of_isHomogeneous
• Source of TauCeti.genus_eq_of_isHomogeneous in TauCeti/FieldTheory/FunctionField/PlaneCurve/Projective.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.genus_eq_of_isHomogeneous

Uses 7

Proof usesThe dimension theorem at the origin · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The Jacobian criterion for a hypersurface · Riemann's theorem · The weak approximation theorem

AbbreviationTauCeti.Divisor.sectionRing#

The section ring ⨁ₙ L(nD) of a divisor D: the k-subalgebra of F[X] of polynomials ∑ fₙ Xⁿ with fₙ ∈ L(nD) for every n.

It is an abbreviation for TauCeti.coeffSubalgebra of the family n ↦ L(nD), so that the grading and its API apply to it directly.

TauCeti.Divisor.sectionRing.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k] [Field F]
  [Algebra k F] (D : TauCeti.Divisor k F) : Subalgebra k (Polynomial F)

Lean

Formalized in Tau Ceti as TauCeti.Divisor.sectionRing.

Sources

• Tau Ceti documentation: TauCeti.Divisor.sectionRing
• Source of TauCeti.Divisor.sectionRing in TauCeti/FieldTheory/FunctionField/RiemannRoch/SectionRing.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.Divisor.sectionRing

Used by 1

Used byHigh powers of a transcendental function have pole divisors whose section ring is generated in degree one

TheoremHigh powers of a transcendental function have pole divisors whose section ring is generated in degree one#

over an exact constant field, if z is transcendental over k, e ≥ 1 and e ≥ 2g, then every section of n (zᵉ)∞ is a sum of products of n sections of (zᵉ)∞.

TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k]
  [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  {z : Fˣ} (hz : Transcendental k ↑z) {e : ℕ} (he₀ : 0 < e) (he : 2 * TauCeti.genus k F ≤ e)
  (n : ℕ) :
  TauCeti.riemannRochSpace (n • TauCeti.Divisor.poles hF (z ^ e)) ≤
    TauCeti.riemannRochSpace (TauCeti.Divisor.poles hF (z ^ e)) ^ n

Lean

Formalized in Tau Ceti as TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow.

Sources

• Tau Ceti documentation: TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow
• Source of TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow in TauCeti/FieldTheory/FunctionField/RiemannRoch/Pencil.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.riemannRochSpace_nsmul_poles_pow_le_pow

Uses 3

Proof usesThe Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · TauCeti.Divisor.sectionRing · The weak approximation theorem

DefinitionThe automorphism group acting on the Weil differentials of F' / k#

the restriction of the dual of TauCeti.repartitionRepresentation to the stable subspace Ω_F, so that (σ • ω) a = ω (σ⁻¹ • a).

TauCeti.weilDifferentialRepresentation.{u, v, v'} (k : Type u) (F : Type v) (F' : Type v') [Field k]
  [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] :
  Representation k Gal(F'/F) ↥(TauCeti.weilDifferentialSpace k F')

Lean

Formalized in Tau Ceti as TauCeti.weilDifferentialRepresentation.

Sources

• Tau Ceti documentation: TauCeti.weilDifferentialRepresentation
• Source of TauCeti.weilDifferentialRepresentation in TauCeti/FieldTheory/FunctionField/Differential/Automorphism.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.weilDifferentialRepresentation

TheoremAt every place the completion is F_P((T)), separable residue field or not#

some isomorphism of the completion with the Laurent-series field over the residue field carries the valuation of P to the T-adic valuation. When F_P is inseparable over k there may be no k-linear such isomorphism (TauCeti.Place.isEmpty_completion_algEquiv_laurentSeries).

TauCeti.Place.exists_completion_ringEquiv_laurentSeries.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] (P : TauCeti.Place k F) :
  ∃ e, ∀ (x : P.Completion), Valued.v (e x) = P.completionPlace.valuation x

Lean

Formalized in Tau Ceti as TauCeti.Place.exists_completion_ringEquiv_laurentSeries.

Sources

• Tau Ceti documentation: TauCeti.Place.exists_completion_ringEquiv_laurentSeries
• Source of TauCeti.Place.exists_completion_ringEquiv_laurentSeries in TauCeti/FieldTheory/FunctionField/Place/Expansion/Laurent/CoefficientField.lean
• Tau Ceti roadmap status: Algebraic curves — function fields, divisors, and Riemann–Roch

LeanTauCeti.Place.exists_completion_ringEquiv_laurentSeries

Uses 1

Proof usesCohen's theorem: a complete local ring containing a field has a coefficient field

TheoremThe abstract residue theorem (Stichtenoth, (1.45))#

the local components of a Weil differential sum to zero on every function of F.

The constant repartition of x lies in the diagonal copy of F inside A_F, on which every Weil differential vanishes, and its entry at every place is x. Stichtenoth states the case x = 1; no hypothesis on the constant field k is needed, and no residue map has been constructed.

TauCeti.finsum_repartitionDualComponent_eq_zero.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k]
  [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  {ω : Module.Dual k ↥(TauCeti.repartitionSpace k F)} (hω : ω ∈ TauCeti.weilDifferentialSpace k F)
  (x : F) : ∑ᶠ (P : TauCeti.Place k F), (TauCeti.repartitionDualComponent ω P) x = 0

Lean

Formalized in Tau Ceti as TauCeti.finsum_repartitionDualComponent_eq_zero.

Sources

• Tau Ceti documentation: TauCeti.finsum_repartitionDualComponent_eq_zero
• Source of TauCeti.finsum_repartitionDualComponent_eq_zero in TauCeti/FieldTheory/FunctionField/Differential/LocalComponent.lean

LeanTauCeti.finsum_repartitionDualComponent_eq_zero

Uses 1 · Used by 5

Proof usesThe weak approximation theorem

Used byTauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The Riemann–Roch theorem with the sheaf of differentials · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3) · The residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x))

TheoremThe duality theorem, in dimensions#

ℓ(W - D) = dim_k Ω_F(D).

TauCeti.dim_sub_eq_finrank_weilDifferentialFiltration.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(TauCeti.repartitionSpace k F)} (hω : ω ≠ 0)
  {W : TauCeti.Divisor k F} (hW : IsGreatest {D | ω ∈ TauCeti.weilDifferentialFiltration D} W)
  (D : TauCeti.Divisor k F) : (W - D).dim = Module.finrank k ↥(TauCeti.weilDifferentialFiltration D)

Lean

Formalized in Tau Ceti as TauCeti.dim_sub_eq_finrank_weilDifferentialFiltration.

Other forms

The duality theorem (Stichtenoth, Theorem 1.5.14). Formalized in Tau Ceti as TauCeti.riemannRochSpaceEquivWeilDifferentialFiltration.

TauCeti.riemannRochSpaceEquivWeilDifferentialFiltration.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(TauCeti.repartitionSpace k F)} (hω : ω ≠ 0)
  {W : TauCeti.Divisor k F} (hW : IsGreatest {D | ω ∈ TauCeti.weilDifferentialFiltration D} W)
  (D : TauCeti.Divisor k F) :
  ↥(TauCeti.riemannRochSpace (W - D)) ≃ₗ[k] ↥(TauCeti.weilDifferentialFiltration D)

Sources

• Tau Ceti documentation: TauCeti.dim_sub_eq_finrank_weilDifferentialFiltration
• Source of TauCeti.dim_sub_eq_finrank_weilDifferentialFiltration in TauCeti/FieldTheory/FunctionField/Differential/CanonicalDivisor.lean

LeanTauCeti.dim_sub_eq_finrank_weilDifferentialFiltration · TauCeti.riemannRochSpaceEquivWeilDifferentialFiltration

Uses 2 · Used by 3

Proof usesRiemann's theorem · The weak approximation theorem

Used bySerre duality in degree zero · Serre duality, in dimensions · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself

TheoremThe residue theorem (Stichtenoth, Corollary 4.3.3)#

over an algebraically closed field, the residues of a Kähler differential ω at the places of F sum to zero, ∑_P res_P (ω) = 0. Every place is rational here, and only finitely many residues are nonzero (TauCeti.finite_support_kaehlerResidueOfPerfectField).

Over a field that is not algebraically closed the rational places do not suffice: over ℚ, the differential 2x / (x² - 2) dx of ℚ(x) has residue zero at every rational place x = a and residue -2 at infinity; the missing residue sits at the place of x² - 2, which is not rational (see TauCeti.finsum_residue_adicOfIrreducible_X_sub_C). Over a perfect field the trace residues at the places of every degree sum to zero (TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero).

TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] [IsAlgClosed k] (hF : TauCeti.IsFunctionField k F)
  (ω : Ω[F⁄k]) : ∑ᶠ (P : TauCeti.Place k F), (P.kaehlerResidueOfPerfectField ⋯ hF) ω = 0

Lean

Formalized in Tau Ceti as TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero.

Sources

• Tau Ceti documentation: TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero
• Source of TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero in TauCeti/FieldTheory/FunctionField/Differential/Independence.lean

LeanTauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero

Uses 8

Proof usesThe abstract residue theorem (Stichtenoth, (1.45)) · Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · Stichtenoth's transformation formula · The weak approximation theorem

TheoremThe residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d))#

over a perfect exact constant field, choose a prime element t_P at each place P. Then the trace residues of a Kähler differential ω sum to zero, ∑_P Tr_{F_P/k} res_{P,t_P} (ω / dt_P) = 0, a sum with finitely many nonzero terms (TauCeti.finite_support_traceResidue_kaehlerBasisOfSeparating_coord). This is the residue theorem for Weil differentials TauCeti.finsum_traceResidue_coord_eq_zero at u = 1, applied to the Weil differential attached to ω. Unlike TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero, places of every degree contribute, so this applies over finite fields.

TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero.{u_1, u_2} {k : Type u_1}
  {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k]
  (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  [∀ (P : TauCeti.Place k F), Algebra.IsSeparable k P.ResidueField] (t : TauCeti.Place k F → F)
  (ht : ∀ (P : TauCeti.Place k F), P.ord (t P) = 1)
  [∀ (P : TauCeti.Place k F), Algebra.IsSeparable (↥k⟮t P⟯) F] (ω : Ω[F⁄k]) :
  have htr := ⋯;
  ∑ᶠ (P : TauCeti.Place k F),
      (P.traceResidue ⋯) (((TauCeti.kaehlerBasisOfSeparating ⋯).coord ()) ω) =
    0

Lean

Formalized in Tau Ceti as TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero.

Sources

• Tau Ceti documentation: TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero
• Source of TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero in TauCeti/FieldTheory/FunctionField/Differential/Independence.lean

LeanTauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero

Uses 7 · Used by 1

Proof usesThe abstract residue theorem (Stichtenoth, (1.45)) · Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · Stichtenoth's transformation formula · The weak approximation theorem

Used byThe residue theorem (Stichtenoth, Corollary 4.3.3)

TheoremRiemann's theorem#

Riemann's theorem (Stichtenoth, Theorem 1.4.17), in the form that unwinds the definition of the genus: deg D + 1 - ℓ(D) ≤ g for every divisor D.

TauCeti.Divisor.degree_add_one_sub_dim_le_genus.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k]
  [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F) (D : TauCeti.Divisor k F) :
  TauCeti.Divisor.degree D + 1 - ↑D.dim ≤ ↑(TauCeti.genus k F)

Lean

Formalized in Tau Ceti as TauCeti.Divisor.degree_add_one_sub_dim_le_genus.

Other forms

Riemann's theorem (Stichtenoth, Theorem 1.4.17). Formalized in Tau Ceti as TauCeti.Divisor.degree_add_one_sub_genus_le_dim.

TauCeti.Divisor.degree_add_one_sub_genus_le_dim.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k]
  [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F) (D : TauCeti.Divisor k F) :
  TauCeti.Divisor.degree D + 1 - ↑(TauCeti.genus k F) ≤ ↑D.dim

Riemann's theorem on k(x), with the genus evaluated. Formalized in Tau Ceti as TauCeti.Divisor.degree_add_one_le_dim_ratFunc.

TauCeti.Divisor.degree_add_one_le_dim_ratFunc.{u_1} {k : Type u_1} [Field k]
  (D : TauCeti.Divisor k (RatFunc k)) : TauCeti.Divisor.degree D + 1 ≤ ↑D.dim

Sources

• Tau Ceti documentation: TauCeti.Divisor.degree_add_one_sub_dim_le_genus
• Source of TauCeti.Divisor.degree_add_one_sub_dim_le_genus in TauCeti/FieldTheory/FunctionField/RiemannRoch/Genus.lean

LeanTauCeti.Divisor.degree_add_one_sub_dim_le_genus · TauCeti.Divisor.degree_add_one_sub_genus_le_dim · TauCeti.Divisor.degree_add_one_le_dim_ratFunc

Uses 1 · Used by 33

Proof usesThe weak approximation theorem

Used byPerfect local Tate duality for E[m] · The Hurwitz genus formula for y² = x³ - x over K(x), as a numerical identity · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Serre duality in degree zero · Serre duality, in dimensions · Serre duality on X_F, in dimensions · The Riemann–Roch theorem for line bundles, in Serre-duality form · The Riemann–Roch theorem on X_F in dimension form · A curve of genus zero with a divisor of degree one has nodal reduction · TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The 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 degree-zero Picard functor Pic⁰_{X/S} · The points of an elliptic curve form Pic⁰ of its projective model · The Riemann–Roch theorem · The Riemann–Roch theorem with the sheaf of differentials · The anti-equivalence between regular proper curves and algebraic function fields over a field k · The duality theorem, in dimensions · The genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3) · The Riemann–Roch identity, read as duality · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3) · Clifford's theorem · Riemann's inequality (Stichtenoth, Corollary 3.11.4) · Strong approximation (Stichtenoth, Theorem 1.6.5) · The residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x))

TheoremThe Riemann–Roch identity, read as duality#

for a Riemann–Roch divisor W, the index of specialty of D is ℓ(W - D) (Stichtenoth, Theorem 1.5.14 in the presence of Theorem 1.5.15).

TauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] {W : TauCeti.Divisor k F} {g₀ : ℕ}
  (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  (hW : W.IsRiemannRochDivisor g₀) (D : TauCeti.Divisor k F) : D.indexOfSpecialty = ↑(W - D).dim

Lean

Formalized in Tau Ceti as TauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq.

Sources

• Tau Ceti documentation: TauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq
• Source of TauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq in TauCeti/FieldTheory/FunctionField/RiemannRoch/Uniqueness.lean

LeanTauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq

Uses 2

Proof usesRiemann's theorem · The weak approximation theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.