Weil differentials and the duality theorem

This file defines Weil differentials, the canonical divisor class, and the duality theorem that identifies L(W − D) with Ω(D).

Main definitions

• FunctionField.WeilDifferential
• FunctionField.WeilDifferential.differentialSpace
• FunctionField.WeilDifferential.divOmega
• FunctionField.IsCanonical

Main results

• FunctionField.WeilDifferential.finrank_weilDifferential_eq_one
• FunctionField.isCanonical_unique_up_to_principal
• FunctionField.duality

@[instance_reducible]

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncWeil (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

The classical decidable equality on k(X) used by the coordinate places.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncWeil k = Classical.decEq (RatFunc k)

instance MarkoffRiemannRoch.FunctionField.Chart.instIsScalarTowerAdeleSpace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : IsScalarTower k K ↥(AdeleSpace k K)

The k- and K-scalar actions on the adele space are compatible.

theorem MarkoffRiemannRoch.FunctionField.Chart.finite_adeleFilt_sub_quotient (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (hle : D ≤ D') : Module.Finite k (↥(adeleFilt k K D') ⧸ Submodule.comap (adeleFilt k K D').subtype (adeleFilt k K D + diagonalSubmodule k K))

The sandwich quotient A(D') ⧸ (A(D) + diag(K)) ⊓ A(D') is finite-dimensional.

instance MarkoffRiemannRoch.FunctionField.Chart.finiteDimensional_adeleQuotient (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : DivisorA k K) : FiniteDimensional k (↥(AdeleSpace k K) ⧸ adeleFilt k K D + diagonalSubmodule k K)

The adele class space 𝒜_K ⧸ (A(D) + diag(K)) is finite-dimensional over k.

theorem MarkoffRiemannRoch.FunctionField.Chart.eq_of_le_of_deg_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') (hdeg : deg k K D' ≤ deg k K D) : D = D'

If D ≤ D' and deg D' ≤ deg D, the divisors are equal.

structure MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Type (max u_1 u_2)

A Weil differential: a k-linear functional on adeles vanishing on some A(D)+diag(K).

• toFun : ↥(AdeleSpace k K) →ₗ[k] k

  The underlying k-linear functional on adeles.

• vanishes_on : ∃ (D : DivisorA k K), ∀ α ∈ adeleFilt k K D + diagonalSubmodule k K, self.toFun α = 0

  The functional vanishes on A(D) + diag(K) for some divisor D.

def MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.IsNonzero {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω : WeilDifferential k K) : Prop

A Weil differential is nonzero.

Equations

• ω.IsNonzero = (ω.toFun ≠ 0)

def MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.differentialSpace {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : Submodule k (↥(AdeleSpace k K) →ₗ[k] k)

The space Ω(D) of k-linear functionals vanishing on A(D)+diag(K).

Equations

• One or more equations did not get rendered due to their size.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.finrank_differentialSpace {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : DivisorA k K) : Module.finrank k ↥(differentialSpace D) = indexOfSpecialty k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.exists_nontrivial_omega {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ∃ (D : DivisorA k K), differentialSpace D ≠ ⊥

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.mul_mem_adeleFilt_add_diagonal {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) (D : DivisorA k K) {a : ↥(AdeleSpace k K)} (ha : a ∈ adeleFilt k K (D + (principalDivisorA k K) (Additive.ofMul x)) + diagonalSubmodule k K) : ↑x • a ∈ adeleFilt k K D + diagonalSubmodule k K

Multiplication by a unit sends A(D + (x)) + diag(K) into A(D) + diag(K).

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulWeil {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : K) (ω : WeilDifferential k K) : WeilDifferential k K

Scalar multiplication of a Weil differential by x ∈ K.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulWeil_toFun_apply {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : K) (ω : WeilDifferential k K) (a : ↥(AdeleSpace k K)) : (smulWeil x ω).toFun a = ω.toFun (x • a)

@[instance_reducible]

instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instZero {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Zero (WeilDifferential k K)

Equations

• MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instZero = { zero := { toFun := 0, vanishes_on := ⋯ } }

@[instance_reducible]

instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instAdd {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Add (WeilDifferential k K)

Equations

• One or more equations did not get rendered due to their size.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.ext {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {ω η : WeilDifferential k K} (h : ω.toFun = η.toFun) : ω = η

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.ext_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {ω η : WeilDifferential k K} : ω = η ↔ ω.toFun = η.toFun

@[instance_reducible]

instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instNeg {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Neg (WeilDifferential k K)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instAddCommGroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : AddCommGroup (WeilDifferential k K)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instSMul {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : SMul K (WeilDifferential k K)

Equations

• MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instSMul = { smul := MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulWeil }

@[instance_reducible]

noncomputable instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instModule {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Module K (WeilDifferential k K)

Equations

• MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instModule = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulWeil_algebraMap {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (c : k) (ω : WeilDifferential k K) (a : ↥(AdeleSpace k K)) : (smulWeil ((algebraMap k K) c) ω).toFun a = c • ω.toFun a

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulWeil_eq_zero_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : K) (hx : x ≠ 0) (ω : WeilDifferential k K) : smulWeil x ω = 0 ↔ ω = 0

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.differentialSpace_eq_dualAnnihilator {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : differentialSpace D = (adeleFilt k K D + diagonalSubmodule k K).dualAnnihilator

Ω(D) is the dual annihilator of A(D) + diag(K).

instance MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.instFiniteDimensionalDifferentialSpace {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : DivisorA k K) : FiniteDimensional k ↥(differentialSpace D)

def MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.vanishingDivisors {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω : WeilDifferential k K) : Set (DivisorA k K)

Divisors D for which ω vanishes on A(D)+diag(K).

Equations

• One or more equations did not get rendered due to their size.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.mem_vanishingDivisors_of_le {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {ω : WeilDifferential k K} {D D' : DivisorA k K} (hle : D' ≤ D) (hD : D ∈ ω.vanishingDivisors) : D' ∈ ω.vanishingDivisors

vanishingDivisors is downward closed.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.add_toFun {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω η : WeilDifferential k K) : (ω + η).toFun = ω.toFun + η.toFun

Underlying functional of a sum of differentials.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulWeil_toFun_mem_differentialSpace {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω : WeilDifferential k K) {D₀ : DivisorA k K} (h : D₀ ∈ ω.vanishingDivisors) {E : DivisorA k K} (f : ↥(RRspace k K E)) : (smulWeil (↑f) ω).toFun ∈ differentialSpace (D₀ - E)

If ω vanishes on A(D₀)+diag(K) and f ∈ L(E), then f•ω vanishes on A(D₀−E)+diag(K).

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulIntoOmega {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω : WeilDifferential k K) {D₀ : DivisorA k K} (h : D₀ ∈ ω.vanishingDivisors) (E : DivisorA k K) : ↥(RRspace k K E) →ₗ[k] ↥(differentialSpace (D₀ - E))

For D₀ ∈ M_ω, multiplication into ω maps L(E) into Ω(D₀ − E).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulIntoOmega_coe {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω : WeilDifferential k K) {D₀ : DivisorA k K} (h : D₀ ∈ ω.vanishingDivisors) (E : DivisorA k K) (f : ↥(RRspace k K E)) : ↑((ω.smulIntoOmega h E) f) = (smulWeil (↑f) ω).toFun

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.smulIntoOmega_injective {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (ω : WeilDifferential k K) {D₀ : DivisorA k K} (h : D₀ ∈ ω.vanishingDivisors) (E : DivisorA k K) (hω : ω.toFun ≠ 0) : Function.Injective ⇑(ω.smulIntoOmega h E)

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.finrank_weilDifferential_eq_one {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : Module.finrank K (WeilDifferential k K) = 1

S2: the space of Weil differentials is one-dimensional over K.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.add_principal_mem_vanishingDivisors_smul_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) (ω : WeilDifferential k K) (D : DivisorA k K) : D + (principalDivisorA k K) (Additive.ofMul x) ∈ (↑x • ω).vanishingDivisors ↔ D ∈ ω.vanishingDivisors

Vanishing divisors translate by the principal divisor under scalar multiplication.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.sup_mem_vanishingDivisors {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {ω : WeilDifferential k K} {D₁ D₂ : DivisorA k K} (hD₁ : D₁ ∈ ω.vanishingDivisors) (hD₂ : D₂ ∈ ω.vanishingDivisors) : D₁ ⊔ D₂ ∈ ω.vanishingDivisors

Directedness of the vanishing set: it is closed under ⊔.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.deg_le_of_mem_vanishingDivisors {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {ω : WeilDifferential k K} (hω : ω.toFun ≠ 0) {D : DivisorA k K} (hD : D ∈ ω.vanishingDivisors) : deg k K D ≤ 2 * ↑(genus k K) - 1

Degree bound (duality-free): a vanishing divisor of a nonzero ω has degree ≤ 2g − 1.

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.exists_max_vanishingDivisor {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {ω : WeilDifferential k K} (hω : ω.IsNonzero) : ∃! W : DivisorA k K, W ∈ ω.vanishingDivisors ∧ ∀ D ∈ ω.vanishingDivisors, D ≤ W

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.divOmega {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (ω : WeilDifferential k K) (hω : ω.IsNonzero) : DivisorA k K

The divisor of a nonzero Weil differential.

Equations

• ω.divOmega hω = Classical.choose ⋯

theorem MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential.divOmega_smul {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (x : Kˣ) (ω : WeilDifferential k K) (hω : ω.IsNonzero) (hxω : (↑x • ω).IsNonzero) : (↑x • ω).divOmega hxω = ω.divOmega hω + (principalDivisorA k K) (Additive.ofMul x)

def MarkoffRiemannRoch.FunctionField.Chart.IsCanonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (W : DivisorA k K) : Prop

A divisor is canonical when it is the divisor of a nonzero Weil differential.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.IsCanonical k K W = ∃ (ω : MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential k K) (hω : ω.IsNonzero), ω.divOmega hω = W

theorem MarkoffRiemannRoch.FunctionField.Chart.exists_isCanonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ∃ (W : DivisorA k K), IsCanonical k K W

A function field admits a canonical divisor.

theorem MarkoffRiemannRoch.FunctionField.Chart.isCanonical_unique_up_to_principal (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W₁ W₂ : DivisorA k K} (h₁ : IsCanonical k K W₁) (h₂ : IsCanonical k K W₂) : ∃ (f : Kˣ), W₁ - W₂ = (principalDivisorA k K) (Additive.ofMul f)

theorem MarkoffRiemannRoch.FunctionField.Chart.duality (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) : ell k K (W - D) = indexOfSpecialty k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.indexOfSpecialty_eq_ell_sub (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) : ↑(indexOfSpecialty k K D) = ↑(ell k K (W - D))