Weil differentials of an algebraic function field

A Weil differential of an algebraic function field F / k is a k-linear form on the repartition space A_F that vanishes on A_F(D) + F for some divisor D. Writing

Ω_F(D) = {ω : A_F →ₗ[k] k | ω vanishes on (A_F(D) + F) ∩ A_F},

the space of all Weil differentials is Ω_F = ⨆_D Ω_F(D), and multiplying repartitions by a function f ∈ F makes Ω_F a vector space over F itself, by (f · ω) a := ω (f · a).

This file constructs Ω_F(D), Ω_F and that F-action. It is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definitions 1.5.6 and 1.5.8. The two theorems that make the objects built here compute — dim_k Ω_F(D) = i(D) (Lemma 1.5.7) and dim_F Ω_F = 1 (Proposition 1.5.9) — rest on the quotient interpretation i(D) = dim_k (A_F ⧸ (A_F(D) + F)) of the index of specialty, and are proved in TauCeti/FieldTheory/FunctionField/Differential/Dimension.lean.

Main definitions

• TauCeti.weilDifferentialFiltration: the space Ω_F(D) of Weil differentials bounded by a divisor (Definition 1.5.6), as a k-subspace of the dual of A_F.
• TauCeti.weilDifferentialSpace: the space Ω_F of all Weil differentials.
• TauCeti.repartitionDualMul: the action of F on the k-linear forms on A_F, induced by multiplication of repartitions by a function (Definition 1.5.8).
• TauCeti.weilDifferentialSpaceMul and TauCeti.weilDifferentialSpaceModule: its restriction to Ω_F, and the resulting F-vector space structure.
• TauCeti.repartitionDualMulRight: that action with the linear form frozen, as the k-linear map F → Module.Dual k A_F, x ↦ x · ω. It restricts to a map F → Ω_F when ω is a Weil differential, by TauCeti.repartitionDualMul_mem_weilDifferentialSpace.

Main results

• TauCeti.mem_weilDifferentialFiltration_of_apply_eq_zero with TauCeti.weilDifferentialFiltration_apply_eq_zero_of_mem_adeleFiltration and TauCeti.weilDifferentialFiltration_apply_eq_zero_of_mem_diagonalRepartitions: membership in Ω_F(D) is vanishing on the repartitions bounded by D together with vanishing on the constants.
• TauCeti.weilDifferentialFiltration_antitone and TauCeti.mem_weilDifferentialSpace_iff: the filtration is antitone and directed, so a k-linear form is a Weil differential exactly when some single divisor bounds it.
• TauCeti.weilDifferentialFiltration_sup: the exact supremum rule Ω_F(D ⊔ E) = Ω_F(D) ∩ Ω_F(E).
• TauCeti.weilDifferentialFiltration_eq_bot_iff: Ω_F(D) = 0 exactly when every repartition differs from a constant by one bounded by D.
• TauCeti.repartitionDualMul_inv_repartitionDualMul: multiplying by a unit and then by its inverse restores the form, so the action of a nonzero function is invertible.
• TauCeti.repartitionDualMulRight_injective and TauCeti.repartitionDualMul_ne_zero: for a nonzero linear form ω, the map x ↦ x · ω is injective, so z · ω is again nonzero for z ≠ 0.
• TauCeti.repartitionDualMul_mem_weilDifferentialFiltration_iff: for z ∈ Fˣ, a linear form lies in Ω_F(D) exactly when z · ω lies in Ω_F(D + div z), so Ω_F is stable under the action (TauCeti.repartitionDualMul_mem_weilDifferentialSpace).

Implementation notes

Ω_F(D) is the annihilator, in the sense of Submodule.dualAnnihilator, of the subspace (A_F(D) + F) ∩ A_F of A_F, which is TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions. The intersection with A_F is not a restriction: the constants are repartitions as soon as F / k is a function field (TauCeti.diagonalRepartitions_le_repartitionSpace), and taking it means the definition of Ω_F(D) itself needs no such hypothesis. Because the definition is an annihilator — TauCeti.weilDifferentialFiltration_eq_dualAnnihilator — Submodule.dualQuotEquivDualAnnihilator identifies Ω_F(D) with the dual of the cokernel A_F ⧸ (A_F(D) + F) with no further work, which is how Lemma 1.5.7 will read dim_k Ω_F(D) off the index of specialty.

The F-vector space structure TauCeti.weilDifferentialSpaceModule is a def, not an instance: it exists only when F / k is a function field, and IsFunctionField k F is a hypothesis passed explicitly rather than a class. Consumers introduce it with letI, as TauCeti.coe_weilDifferentialSpaceModule_smul and TauCeti.isScalarTower_weilDifferentialSpace do.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5.

Weil differentials bounded by a divisor

noncomputable def TauCeti.weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : Submodule k (Module.Dual k ↥(repartitionSpace k F))

The space Ω_F(D) of Weil differentials bounded by D (Stichtenoth, Definition 1.5.6): the k-linear forms on the repartition space that vanish on A_F(D) + F.

Equations

• TauCeti.weilDifferentialFiltration D = (TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions D).dualAnnihilator

theorem TauCeti.weilDifferentialFiltration_eq_dualAnnihilator {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : weilDifferentialFiltration D = (submoduleOfAdeleFiltrationSupDiagonalRepartitions D).dualAnnihilator

Ω_F(D) is the annihilator of (A_F(D) + F) ∩ A_F, which is how Submodule.dualQuotEquivDualAnnihilator identifies it with the dual of the cokernel A_F ⧸ (A_F(D) + F).

theorem TauCeti.mem_weilDifferentialFiltration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} : ω ∈ weilDifferentialFiltration D ↔ ∀ a ∈ submoduleOfAdeleFiltrationSupDiagonalRepartitions D, ω a = 0

Membership in Ω_F(D), unfolded: the form kills every repartition in A_F(D) + F.

theorem TauCeti.weilDifferentialFiltration_apply_eq_zero_of_mem_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialFiltration D) (a : ↥(repartitionSpace k F)) (ha : ↑a ∈ adeleFiltration D) : ω a = 0

A Weil differential bounded by D kills every repartition whose poles are bounded by D.

theorem TauCeti.weilDifferentialFiltration_apply_eq_zero_of_mem_diagonalRepartitions {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialFiltration D) (a : ↥(repartitionSpace k F)) (ha : ↑a ∈ diagonalRepartitions k F) : ω a = 0

A Weil differential bounded by D kills every constant repartition.

theorem TauCeti.mem_weilDifferentialFiltration_of_apply_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} (h₁ : ∀ (a : ↥(repartitionSpace k F)), ↑a ∈ adeleFiltration D → ω a = 0) (h₂ : ∀ (a : ↥(repartitionSpace k F)), ↑a ∈ diagonalRepartitions k F → ω a = 0) : ω ∈ weilDifferentialFiltration D

The two vanishing conditions defining Ω_F(D): a k-linear form on A_F that kills the repartitions bounded by D and kills the constants is a Weil differential bounded by D.

theorem TauCeti.weilDifferentialFiltration_antitone {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : Antitone weilDifferentialFiltration

Enlarging the divisor shrinks the space of Weil differentials it bounds.

@[simp]

theorem TauCeti.weilDifferentialFiltration_sup {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) : weilDifferentialFiltration (D ⊔ E) = weilDifferentialFiltration D ⊓ weilDifferentialFiltration E

The filtration turns suprema of divisors into intersections of spaces of Weil differentials: Ω_F(D ⊔ E) = Ω_F(D) ∩ Ω_F(E).

theorem TauCeti.weilDifferentialFiltration_eq_bot_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : weilDifferentialFiltration D = ⊥ ↔ adeleFiltration D ⊔ diagonalRepartitions k F = repartitionSpace k F

Ω_F(D) vanishes exactly when A_F(D) + F is everything: the only k-linear form on A_F vanishing on A_F(D) + F is 0 precisely when every repartition already differs from a constant by one whose poles are bounded by D.

The space of all Weil differentials

noncomputable def TauCeti.weilDifferentialSpace (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] : Submodule k (Module.Dual k ↥(repartitionSpace k F))

The space Ω_F of Weil differentials of F / k (Stichtenoth, Definition 1.5.6): the k-linear forms on the repartition space that some divisor bounds.

Equations

• TauCeti.weilDifferentialSpace k F = ⨆ (D : TauCeti.Divisor k F), TauCeti.weilDifferentialFiltration D

theorem TauCeti.weilDifferentialFiltration_le_weilDifferentialSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : weilDifferentialFiltration D ≤ weilDifferentialSpace k F

Every Weil differential bounded by a divisor is a Weil differential.

theorem TauCeti.directed_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : Directed (fun (x1 x2 : Submodule k (Module.Dual k ↥(repartitionSpace k F))) => x1 ≤ x2) weilDifferentialFiltration

The filtration is directed: it is antitone, and any two divisors have a lower bound, namely their pointwise minimum, whose member then contains both.

theorem TauCeti.mem_weilDifferentialSpace_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {ω : Module.Dual k ↥(repartitionSpace k F)} : ω ∈ weilDifferentialSpace k F ↔ ∃ (D : Divisor k F), ω ∈ weilDifferentialFiltration D

A k-linear form on A_F is a Weil differential exactly when a single divisor bounds it: the supremum defining Ω_F is the union of the Ω_F(D), because they are directed.

Multiplication by a function

noncomputable def TauCeti.repartitionDualMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : F →ₐ[k] Module.End k (Module.Dual k ↥(repartitionSpace k F))

The multiplication action of F on the k-linear forms on the repartition space (Stichtenoth, Definition 1.5.8): (f · ω) a = ω (f · a). It is a k-algebra map because F is commutative, so the transposes of the multiplication maps compose in either order.

Equations

• TauCeti.repartitionDualMul hF = { toFun := fun (f : F) => LinearMap.dualMap ((TauCeti.repartitionMul hF) f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem TauCeti.repartitionDualMul_apply_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (ω : Module.Dual k ↥(repartitionSpace k F)) (a : ↥(repartitionSpace k F)) : (((repartitionDualMul hF) f) ω) a = ω (((repartitionMul hF) f) a)

The defining formula (f · ω) a = ω (f · a) of the action of F on the linear forms.

theorem TauCeti.repartitionDualMul_repartitionDualMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f g : F) (ω : Module.Dual k ↥(repartitionSpace k F)) : ((repartitionDualMul hF) f) (((repartitionDualMul hF) g) ω) = ((repartitionDualMul hF) (f * g)) ω

Multiplying twice is multiplying once by the product. It is not a simp lemma: map_mul rewrites in the opposite direction.

@[simp]

theorem TauCeti.repartitionDualMul_inv_repartitionDualMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) (ω : Module.Dual k ↥(repartitionSpace k F)) : ((repartitionDualMul hF) x⁻¹) (((repartitionDualMul hF) x) ω) = ω

Multiplying by a nonzero function and then by its inverse restores the linear form, so multiplication by a nonzero function is invertible on Ω_F.

noncomputable def TauCeti.repartitionDualMulRight {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (ω : Module.Dual k ↥(repartitionSpace k F)) : F →ₗ[k] Module.Dual k ↥(repartitionSpace k F)

Multiplication of a fixed linear form by a varying function, as a k-linear map F → Module.Dual k A_F: the map x ↦ x · ω obtained by freezing the second argument of TauCeti.repartitionDualMul. Here ω is an arbitrary k-linear form on A_F; when it is a Weil differential the map lands in Ω_F, by TauCeti.repartitionDualMul_mem_weilDifferentialSpace. For ω ≠ 0 it is injective (TauCeti.repartitionDualMulRight_injective), and Riemann–Roch is the computation of its image on a Riemann–Roch space.

Equations

• TauCeti.repartitionDualMulRight hF ω = (TauCeti.repartitionDualMul hF).toLinearMap.flip ω

@[simp]

theorem TauCeti.repartitionDualMulRight_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (ω : Module.Dual k ↥(repartitionSpace k F)) (x : F) : (repartitionDualMulRight hF ω) x = ((repartitionDualMul hF) x) ω

theorem TauCeti.repartitionDualMulRight_injective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) : Function.Injective ⇑(repartitionDualMulRight hF ω)

Multiplication by a nonzero linear form is injective: a function x with x · ω = 0 is itself zero.

theorem TauCeti.repartitionDualMul_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {z : F} (hz : z ≠ 0) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) : ((repartitionDualMul hF) z) ω ≠ 0

A nonzero function times a nonzero linear form is nonzero.

theorem TauCeti.repartitionDualMul_mem_weilDifferentialFiltration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} : ((repartitionDualMul hF) ↑z) ω ∈ weilDifferentialFiltration (D + Divisor.principal hF z) ↔ ω ∈ weilDifferentialFiltration D

Multiplication translates the filtration by a principal divisor: for a nonzero function z, a linear form is bounded by D exactly when z · ω is bounded by D + div z, exactly as multiplication by z carries A_F(D + div z) into A_F(D).

theorem TauCeti.repartitionDualMul_mem_weilDifferentialSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialSpace k F) : ((repartitionDualMul hF) f) ω ∈ weilDifferentialSpace k F

Ω_F is stable under multiplication by a function, which is what makes it a vector space over F and not merely over k.

noncomputable def TauCeti.weilDifferentialSpaceMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : F →ₐ[k] Module.End k ↥(weilDifferentialSpace k F)

The multiplication action of F on Ω_F itself, the restriction of TauCeti.repartitionDualMul to the stable subspace of Weil differentials.

Equations

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

@[simp]

theorem TauCeti.coe_weilDifferentialSpaceMul_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (ω : ↥(weilDifferentialSpace k F)) : ↑(((weilDifferentialSpaceMul hF) f) ω) = ((repartitionDualMul hF) f) ↑ω

The action of F on Ω_F is the restriction of its action on all the linear forms.

@[instance_reducible]

noncomputable def TauCeti.weilDifferentialSpaceModule {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Module F ↥(weilDifferentialSpace k F)

The F-vector space structure on Ω_F (Stichtenoth, Definition 1.5.8): (f · ω) a is ω (f · a). It is a def and not an instance because it exists only for an algebraic function field, and TauCeti.IsFunctionField is an explicit hypothesis, not a class; introduce it with letI.

Equations

• TauCeti.weilDifferentialSpaceModule hF = Module.compHom (↥(TauCeti.weilDifferentialSpace k F)) (TauCeti.weilDifferentialSpaceMul hF).toRingHom

theorem TauCeti.coe_weilDifferentialSpaceModule_smul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (ω : ↥(weilDifferentialSpace k F)) : ↑(f • ω) = ((repartitionDualMul hF) f) ↑ω

The scalar multiplication of TauCeti.weilDifferentialSpaceModule is the multiplication action TauCeti.repartitionDualMul.

theorem TauCeti.isScalarTower_weilDifferentialSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : IsScalarTower k F ↥(weilDifferentialSpace k F)

The F-vector space structure on Ω_F extends its k-vector space structure.