Riemann–Roch spaces under semilinear field isomorphisms

A field isomorphism carrying one constant field onto another identifies places and divisors, preserves residue-weighted degrees, and induces semilinear isomorphisms of Riemann–Roch spaces. Consequently it preserves the genus. Semilinearity is essential for Frobenius: over perfect constants Frobenius is an automorphism of the constants, not generally their identity.

Divisor transport uses Finsupp.domCongr along Place.equivOfRingEquiv; no additional divisor carrier is introduced. These statements do not require exact constants or a function-field hypothesis, since they identify the sets and dimensions defining the genus directly.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Sections I.4 and III.10.

@[simp]

theorem TauCeti.Divisor.degree_domCongr_equivOfRingEquiv {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) : degree ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D) = degree D

Transporting a divisor along a semilinear field isomorphism preserves its weighted degree.

@[simp]

theorem TauCeti.mem_riemannRochSpace_domCongr_equivOfRingEquiv_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) (z : F) : τ z ∈ riemannRochSpace ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D) ↔ z ∈ riemannRochSpace D

A semilinear field isomorphism preserves the valuation bounds defining a Riemann–Roch space.

noncomputable def TauCeti.riemannRochSpaceEquivOfRingEquiv {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) : ↥(riemannRochSpace D) ≃ₛₗ[↑σ] ↥(riemannRochSpace ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D))

The semilinear isomorphism of Riemann–Roch spaces induced by an isomorphism of fields and constants. Its underlying map is the restriction of τ.

Equations

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

@[simp]

theorem TauCeti.riemannRochSpaceEquivOfRingEquiv_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) (z : ↥(riemannRochSpace D)) : ↑((riemannRochSpaceEquivOfRingEquiv σ τ h D) z) = τ ↑z

Evaluation of the transported section is evaluation of the field isomorphism.

@[simp]

theorem TauCeti.riemannRochSpaceEquivOfRingEquiv_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) (z : ↥(riemannRochSpace ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D))) : ↑((riemannRochSpaceEquivOfRingEquiv σ τ h D).symm z) = τ.symm ↑z

Inverse transport of a section is given by the inverse field isomorphism.

@[simp]

theorem TauCeti.Divisor.dim_domCongr_equivOfRingEquiv {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) : dim ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D) = D.dim

Semilinear transport preserves the dimension of a Riemann–Roch space.

theorem TauCeti.genus_eq_of_ringEquiv {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)) : genus k' F' = genus k F

The genus is invariant under an isomorphism carrying the constant fields onto one another. This also preserves the junk value of the supremum when the fields are not function fields.