Repartitions and repartition cokernels under semilinear field isomorphisms

Let τ : F ≃+* F' be a field isomorphism carrying a constant subfield k onto k' along σ : k ≃+* k'. Composing valuations with τ⁻¹ identifies the places (Place.equivOfRingEquiv) and hence the divisors (Finsupp.domCongr).

Entrywise application of τ along that bijection of places gives a σ-semilinear isomorphism of repartition spaces A_F ≃ₛₗ[σ] A_{F'} (TauCeti.repartitionSpaceEquivOfRingEquiv). It moves single repartitions with the places, intertwines multiplication by functions, and carries both the divisor filtration A_F(D) and the diagonal copy of F onto their counterparts in F', descending to a σ-semilinear isomorphism of repartition cokernels A_F ⧸ (A_F(D) + F) ≃ₛₗ[σ] A_{F'} ⧸ (A_{F'}(τ_* D) + F') (TauCeti.repartitionQuotientEquivOfRingEquiv).

No exact-constant or function-field hypothesis is needed to construct the repartition and cokernel equivalences.

Main definitions

• TauCeti.repartitionSpaceEquivOfRingEquiv: the σ-semilinear isomorphism A_F ≃ₛₗ[σ] A_{F'}.
• TauCeti.repartitionQuotientEquivOfRingEquiv: the induced isomorphism of repartition cokernels A_F ⧸ (A_F(D) + F) ≃ₛₗ[σ] A_{F'} ⧸ (A_{F'}(τ_* D) + F').

Main results

• TauCeti.repartitionSpaceEquivOfRingEquiv_singleRepartition: transport moves ι_P x to ι_{τ_* P} (τ x).
• TauCeti.repartitionSpaceEquivOfRingEquiv_repartitionMul: transport is τ-semilinear for multiplication by functions.
• TauCeti.repartitionQuotientEquivOfRingEquiv_mk: the cokernel isomorphism sends the class of a to the class of its transport.

References

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

Semilinear transport of repartitions

noncomputable def TauCeti.repartitionSpaceEquivOfRingEquiv {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)) : ↥(repartitionSpace k F) ≃ₛₗ[↑σ] ↥(repartitionSpace k' F')

Semilinear transport of the repartition space: an isomorphism τ : F ≃+* F' carrying k onto k' along σ induces A_F ≃ₛₗ[σ] A_{F'} by (τ_* a)_Q = τ (a_{τ^* Q}).

@[simp]

theorem TauCeti.coe_repartitionSpaceEquivOfRingEquiv_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)) (a : ↥(repartitionSpace k F)) (Q : Place k' F') : ↑((repartitionSpaceEquivOfRingEquiv σ τ h) a) Q = τ (↑a ((Place.equivOfRingEquiv σ τ h).symm Q))

Entrywise formula for repartitionSpaceEquivOfRingEquiv.

@[simp]

theorem TauCeti.coe_repartitionSpaceEquivOfRingEquiv_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)) (b : ↥(repartitionSpace k' F')) (P : Place k F) : ↑((repartitionSpaceEquivOfRingEquiv σ τ h).symm b) P = τ.symm (↑b ((Place.equivOfRingEquiv σ τ h) P))

Entrywise formula for the inverse of repartitionSpaceEquivOfRingEquiv.

@[simp]

theorem TauCeti.repartitionSpaceEquivOfRingEquiv_singleRepartition {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)) (P : Place k F) (x : F) : (repartitionSpaceEquivOfRingEquiv σ τ h) ((singleRepartition P) x) = (singleRepartition ((Place.equivOfRingEquiv σ τ h) P)) (τ x)

repartitionSpaceEquivOfRingEquiv moves a single-place repartition ι_P x to ι_{τ_* P} (τ x).

@[simp]

theorem TauCeti.repartitionSpaceEquivOfRingEquiv_repartitionMul {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) (a : ↥(repartitionSpace k F)) : (repartitionSpaceEquivOfRingEquiv σ τ h) (((repartitionMul hF) z) a) = ((repartitionMul hF') (τ z)) ((repartitionSpaceEquivOfRingEquiv σ τ h) a)

repartitionSpaceEquivOfRingEquiv is τ-semilinear for multiplication by functions.

@[simp]

theorem TauCeti.repartitionSpaceEquivOfRingEquiv_mem_submoduleOfAdeleFiltrationSupDiagonalRepartitions_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) (a : ↥(repartitionSpace k F)) : (repartitionSpaceEquivOfRingEquiv σ τ h) a ∈ submoduleOfAdeleFiltrationSupDiagonalRepartitions ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D) ↔ a ∈ submoduleOfAdeleFiltrationSupDiagonalRepartitions D

repartitionSpaceEquivOfRingEquiv carries (A_F(D) + F) ∩ A_F onto (A_{F'}(τ_* D) + F') ∩ A_{F'}.

noncomputable def TauCeti.repartitionQuotientEquivOfRingEquiv {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) : (↥(repartitionSpace k F) ⧸ submoduleOfAdeleFiltrationSupDiagonalRepartitions D) ≃ₛₗ[↑σ] ↥(repartitionSpace k' F') ⧸ submoduleOfAdeleFiltrationSupDiagonalRepartitions ((Finsupp.domCongr (Place.equivOfRingEquiv σ τ h)) D)

Semilinear transport of repartition cokernels: A_F ⧸ (A_F(D) + F) is σ-semilinearly isomorphic to A_{F'} ⧸ (A_{F'}(τ_* D) + F').

@[simp]

theorem TauCeti.repartitionQuotientEquivOfRingEquiv_mk {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) (a : ↥(repartitionSpace k F)) : (repartitionQuotientEquivOfRingEquiv σ τ h D) (Submodule.Quotient.mk a) = Submodule.Quotient.mk ((repartitionSpaceEquivOfRingEquiv σ τ h) a)

repartitionQuotientEquivOfRingEquiv sends the class of a to the class of its transport.

@[simp]

theorem TauCeti.repartitionQuotientEquivOfRingEquiv_symm_mk {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) (b : ↥(repartitionSpace k' F')) : (repartitionQuotientEquivOfRingEquiv σ τ h D).symm (Submodule.Quotient.mk b) = Submodule.Quotient.mk ((repartitionSpaceEquivOfRingEquiv σ τ h).symm b)

The inverse of repartitionQuotientEquivOfRingEquiv sends the class of b to the class of its inverse transport.