Weil differentials and the canonical class under semilinear field isomorphisms

Let τ : F ≃+* F' be a field isomorphism carrying a constant subfield k onto k' along σ : k ≃+* k'. Dualizing the repartition transport TauCeti.repartitionSpaceEquivOfRingEquiv (A_F ≃ₛₗ[σ] A_{F'}) sends a k-linear form ω on A_F to b ↦ σ (ω (τ⁻¹ b)) on A_{F'}.

Because repartitionSpaceEquivOfRingEquiv carries (A_F(D) + F) ∩ A_F onto (A_{F'}(τ_* D) + F') ∩ A_{F'}, this contragredient isomorphism carries Ω_F(D) onto Ω_{F'}(τ_* D) and Ω_F onto Ω_{F'} without any assumption on the constant fields. For function fields with exact constant fields, it carries the divisor (ω) of a nonzero Weil differential to τ_* (ω), so the divisor-class isomorphism Divisor.classGroupEquivOfRingEquiv carries TauCeti.canonicalClass to TauCeti.canonicalClass.

Main definitions

• TauCeti.repartitionDualEquivOfRingEquiv: the contragredient σ-semilinear isomorphism between linear forms on A_F and linear forms on A_{F'}.
• TauCeti.weilDifferentialFiltrationEquivOfRingEquiv and TauCeti.weilDifferentialSpaceEquivOfRingEquiv: its restrictions Ω_F(D) ≃ₛₗ[σ] Ω_{F'}(τ_* D) and Ω_F ≃ₛₗ[σ] Ω_{F'}.

Main results

• TauCeti.weilDifferentialDivisor_repartitionDualEquivOfRingEquiv: transport carries the divisor of a nonzero Weil differential to the reindexed divisor.
• TauCeti.Divisor.classGroupEquivOfRingEquiv_canonicalClass: Cl(F) ≃+ Cl(F') carries the canonical class of F to the canonical class of F'.

References

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

noncomputable def TauCeti.repartitionDualEquivOfRingEquiv {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) : Module.Dual k ↥(repartitionSpace k F) ≃ₛₗ[↑σ] Module.Dual k' ↥(repartitionSpace k' F')

Contragredient semilinear transport of linear forms on repartitions: ω on A_F goes to b ↦ σ (ω (τ⁻¹ b)) on A_{F'}.

@[simp]

theorem TauCeti.repartitionDualEquivOfRingEquiv_apply_apply {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (ω : Module.Dual k ↥(repartitionSpace k F)) (b : ↥(repartitionSpace k' F')) : ((repartitionDualEquivOfRingEquiv σ τ h) ω) b = σ (ω ((repartitionSpaceEquivOfRingEquiv σ τ h).symm b))

Evaluation formula for a transported linear form on repartitions.

@[simp]

theorem TauCeti.repartitionDualEquivOfRingEquiv_symm_apply_apply {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (η : Module.Dual k' ↥(repartitionSpace k' F')) (a : ↥(repartitionSpace k F)) : ((repartitionDualEquivOfRingEquiv σ τ h).symm η) a = σ.symm (η ((repartitionSpaceEquivOfRingEquiv σ τ h) a))

Evaluation formula for the inverse transport of a linear form on repartitions.

@[simp]

theorem TauCeti.repartitionDualEquivOfRingEquiv_repartitionDualMul {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (z : F) (ω : Module.Dual k ↥(repartitionSpace k F)) : (repartitionDualEquivOfRingEquiv σ τ h) (((repartitionDualMul hF) z) ω) = ((repartitionDualMul hF') (τ z)) ((repartitionDualEquivOfRingEquiv σ τ h) ω)

repartitionDualEquivOfRingEquiv is τ-semilinear for multiplication of forms by functions.

@[simp]

theorem TauCeti.repartitionDualEquivOfRingEquiv_mem_weilDifferentialFiltration_iff {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (D : Divisor k F) (ω : Module.Dual k ↥(repartitionSpace k F)) : (repartitionDualEquivOfRingEquiv σ τ h) ω ∈ weilDifferentialFiltration ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D) ↔ ω ∈ weilDifferentialFiltration D

repartitionDualEquivOfRingEquiv carries Ω_F(D) onto Ω_{F'}(τ_* D).

noncomputable def TauCeti.weilDifferentialFiltrationEquivOfRingEquiv {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (D : Divisor k F) : ↥(weilDifferentialFiltration D) ≃ₛₗ[↑σ] ↥(weilDifferentialFiltration ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D))

Semilinear transport of the Weil-differential filtration: Ω_F(D) ≃ₛₗ[σ] Ω_{F'}(τ_* D).

@[simp]

theorem TauCeti.coe_weilDifferentialFiltrationEquivOfRingEquiv_apply {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (D : Divisor k F) (ω : ↥(weilDifferentialFiltration D)) : ↑((weilDifferentialFiltrationEquivOfRingEquiv σ τ h D) ω) = (repartitionDualEquivOfRingEquiv σ τ h) ↑ω

weilDifferentialFiltrationEquivOfRingEquiv is the restriction of repartitionDualEquivOfRingEquiv.

@[simp]

theorem TauCeti.coe_weilDifferentialFiltrationEquivOfRingEquiv_symm_apply {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (D : Divisor k F) (η : ↥(weilDifferentialFiltration ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D))) : ↑((weilDifferentialFiltrationEquivOfRingEquiv σ τ h D).symm η) = (repartitionDualEquivOfRingEquiv σ τ h).symm ↑η

The inverse of weilDifferentialFiltrationEquivOfRingEquiv is the restriction of the inverse of repartitionDualEquivOfRingEquiv.

@[simp]

theorem TauCeti.repartitionDualEquivOfRingEquiv_mem_weilDifferentialSpace_iff {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (ω : Module.Dual k ↥(repartitionSpace k F)) : (repartitionDualEquivOfRingEquiv σ τ h) ω ∈ weilDifferentialSpace k' F' ↔ ω ∈ weilDifferentialSpace k F

repartitionDualEquivOfRingEquiv preserves the space of Weil differentials.

noncomputable def TauCeti.weilDifferentialSpaceEquivOfRingEquiv {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) : ↥(weilDifferentialSpace k F) ≃ₛₗ[↑σ] ↥(weilDifferentialSpace k' F')

Semilinear transport of the space of Weil differentials: Ω_F ≃ₛₗ[σ] Ω_{F'}.

@[simp]

theorem TauCeti.coe_weilDifferentialSpaceEquivOfRingEquiv_apply {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (ω : ↥(weilDifferentialSpace k F)) : ↑((weilDifferentialSpaceEquivOfRingEquiv σ τ h) ω) = (repartitionDualEquivOfRingEquiv σ τ h) ↑ω

weilDifferentialSpaceEquivOfRingEquiv is the restriction of repartitionDualEquivOfRingEquiv.

@[simp]

theorem TauCeti.coe_weilDifferentialSpaceEquivOfRingEquiv_symm_apply {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (η : ↥(weilDifferentialSpace k' F')) : ↑((weilDifferentialSpaceEquivOfRingEquiv σ τ h).symm η) = (repartitionDualEquivOfRingEquiv σ τ h).symm ↑η

The inverse of weilDifferentialSpaceEquivOfRingEquiv is the restriction of the inverse of repartitionDualEquivOfRingEquiv.

theorem TauCeti.isGreatest_weilDifferentialFiltration_repartitionDualEquivOfRingEquiv_iff {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (ω : Module.Dual k ↥(repartitionSpace k F)) (W : Divisor k F) : IsGreatest {E' : Divisor k' F' | (repartitionDualEquivOfRingEquiv σ τ h) ω ∈ weilDifferentialFiltration E'} ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) W) ↔ IsGreatest {E : Divisor k F | ω ∈ weilDifferentialFiltration E} W

repartitionDualEquivOfRingEquiv transports greatest bounding divisors of linear forms on repartitions along Place.equivOfRingEquiv.

@[simp]

theorem TauCeti.weilDifferentialDivisor_repartitionDualEquivOfRingEquiv {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : weilDifferentialDivisor hF' hex' ⋯ ⋯ = (Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) (weilDifferentialDivisor hF hex hmem hω)

Transport of the divisor of a Weil differential: transporting a nonzero Weil differential along (σ, τ) reindexes its divisor along Place.equivOfRingEquiv σ τ h.

@[simp]

theorem TauCeti.Divisor.classGroupEquivOfRingEquiv_canonicalClass {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] (σ : k ≃+* k') (τ : F ≃+* F') (h : ∀ (c : k), τ ((algebraMap k F) c) = (algebraMap k' F') (σ c)) (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : (classGroupEquivOfRingEquiv σ τ h hF hF') (canonicalClass hF hex) = canonicalClass hF' hex'

The divisor-class isomorphism Cl(F) ≃+ Cl(F') carries the canonical class to the canonical class.