Divisor class groups under semilinear field isomorphisms

Let τ : F ≃+* F' be an isomorphism of function fields carrying the constants k onto k' along σ : k ≃+* k'. It transports places (Place.equivOfRingEquiv) and hence divisors, by reindexing. This file shows that this transport preserves degrees and carries the divisor of a function z to the divisor of τ z. Consequently it carries principal divisors onto principal divisors, and induces isomorphisms of the divisor class groups and of the degree-zero divisor class groups Cl⁰(F) ≃+ Cl⁰(F').

Isomorphic function fields therefore have isomorphic degree-zero divisor class groups, which is how a class group computed for one model of a curve is transported to another model of it.

Main declarations

• Divisor.degree_domCongr_equivOfRingEquiv: τ preserves divisor degrees;
• Divisor.domCongr_equivOfRingEquiv_principal: τ carries div z to div (τ z);
• Divisor.classGroupEquivOfRingEquiv: the induced isomorphism Cl(F) ≃+ Cl(F');
• Divisor.degreeZeroClassGroupEquivOfRingEquiv: its restriction Cl⁰(F) ≃+ Cl⁰(F').

References

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

@[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.Divisor.domCongr_equivOfRingEquiv_principal {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ˣ) : (Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) (principal hF z) = principal hF' ((Units.map ↑τ) z)

A semilinear field isomorphism transports principal divisors: reindexing div z along the induced bijection of places gives div (τ z).

noncomputable def TauCeti.Divisor.classGroupEquivOfRingEquiv {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') : (Place.orderSystem hF).ClassGroup ≃+ (Place.orderSystem hF').ClassGroup

The divisor class groups of isomorphic function fields are isomorphic: a semilinear field isomorphism τ sends the class of D to the class of its transport along the induced bijection of places.

@[simp]

theorem TauCeti.Divisor.classGroupEquivOfRingEquiv_divisorClass {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') (D : Divisor k F) : (classGroupEquivOfRingEquiv σ τ h hF hF') ((Place.orderSystem hF).divisorClass D) = (Place.orderSystem hF').divisorClass ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D)

classGroupEquivOfRingEquiv sends the class of D to the class of its transport.

@[simp]

theorem TauCeti.Divisor.classGroupEquivOfRingEquiv_symm_divisorClass {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') (D : Divisor k' F') : (classGroupEquivOfRingEquiv σ τ h hF hF').symm ((Place.orderSystem hF').divisorClass D) = (Place.orderSystem hF).divisorClass ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h).symm) D)

The inverse of classGroupEquivOfRingEquiv sends the class of D to the class of its transport back along the induced bijection of places.

@[simp]

theorem TauCeti.Divisor.degreeClass_classGroupEquivOfRingEquiv {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') (c : (Place.orderSystem hF).ClassGroup) : (degreeClass hF') ((classGroupEquivOfRingEquiv σ τ h hF hF') c) = (degreeClass hF) c

classGroupEquivOfRingEquiv preserves the degree of a divisor class.

noncomputable def TauCeti.Divisor.degreeZeroClassGroupEquivOfRingEquiv {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') : ↥(degreeClass hF).ker ≃+ ↥(degreeClass hF').ker

The degree-zero divisor class groups of isomorphic function fields are isomorphic: Cl⁰(F) ≃+ Cl⁰(F'), the restriction of classGroupEquivOfRingEquiv.

@[simp]

theorem TauCeti.Divisor.coe_degreeZeroClassGroupEquivOfRingEquiv_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)) (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (c : ↥(degreeClass hF).ker) : ↑((degreeZeroClassGroupEquivOfRingEquiv σ τ h hF hF') c) = (classGroupEquivOfRingEquiv σ τ h hF hF') ↑c

degreeZeroClassGroupEquivOfRingEquiv is the restriction of classGroupEquivOfRingEquiv.

@[simp]

theorem TauCeti.Divisor.coe_degreeZeroClassGroupEquivOfRingEquiv_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)) (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (c : ↥(degreeClass hF').ker) : ↑((degreeZeroClassGroupEquivOfRingEquiv σ τ h hF hF').symm c) = (classGroupEquivOfRingEquiv σ τ h hF hF').symm ↑c

The inverse of degreeZeroClassGroupEquivOfRingEquiv is the restriction of the inverse of classGroupEquivOfRingEquiv.