Transport of places under semilinear field isomorphisms

An isomorphism of fields carrying one constant field onto another transports normalized places by composing their valuations with its inverse. The residue fields are correspondingly isomorphic, semilinearly over the constant-field isomorphism, so residue degrees are preserved. This permits coefficient automorphisms to act on places even when they do not fix the constants pointwise, as in Galois actions on base-changed curves.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Section I.1.

noncomputable def TauCeti.Place.equivOfRingEquiv {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) : Place k L ≃ Place k' L'

Transport of places under a semilinear field isomorphism. The compatibility equation says that τ carries the constants along σ; the transported valuation is v ∘ τ⁻¹.

Equations

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

@[simp]

theorem TauCeti.Place.valuation_equivOfRingEquiv {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (P : Place k L) (z : L') : ((equivOfRingEquiv σ τ h) P).valuation z = P.valuation (τ.symm z)

The defining valuation formula for transport of a place.

@[simp]

theorem TauCeti.Place.ord_equivOfRingEquiv {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (P : Place k L) (z : L') : ((equivOfRingEquiv σ τ h) P).ord z = P.ord (τ.symm z)

The order at the transported place is computed by applying the inverse field isomorphism.

@[simp]

theorem TauCeti.Place.valuation_equivOfRingEquiv_symm {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (Q : Place k' L') (z : L) : ((equivOfRingEquiv σ τ h).symm Q).valuation z = Q.valuation (τ z)

The inverse transport has valuation v ∘ τ.

noncomputable def TauCeti.Place.integersEquivOfRingEquiv {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (P : Place k L) : ↥P.integers ≃+* ↥((equivOfRingEquiv σ τ h) P).integers

Transport restricts to an isomorphism of the valuation rings.

Equations

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

@[simp]

theorem TauCeti.Place.coe_integersEquivOfRingEquiv {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (P : Place k L) (x : ↥P.integers) : ↑((integersEquivOfRingEquiv σ τ h P) x) = τ ↑x

The valuation-ring isomorphism is the restriction of the field isomorphism.

@[simp]

theorem TauCeti.Place.degree_equivOfRingEquiv {k : Type u_1} {k' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field k'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (P : Place k L) : ((equivOfRingEquiv σ τ h) P).degree = P.degree

Residue degrees are preserved by semilinear transport. The residue-field isomorphism carries constants by σ, which suffices to preserve their vector-space dimension.