The automorphism group acting on repartitions

Let F' / F be an extension of fields and k a subfield of F. An F-automorphism σ of F' permutes the places of F' / k (TauCeti.Place.instMulActionAlgEquiv) and moves functions, so it moves families of functions indexed by the places: the family a goes to

(σ • a) Q = σ (a (σ⁻¹ • Q)),

whose entry at σ • P is σ (a P). This is a k-linear representation of F' ≃ₐ[F] F' on Place k F' → F'. Because σ carries the valuation at P to the valuation at σ • P, it is compatible with every piece of structure from which Weil differentials are built: it preserves the repartition space A_F, carries the filtration step A_F(D) onto A_F(σ • D), preserves the diagonal copy of F', is semilinear for multiplication by functions, and moves the repartition ι_P x supported at one place to ι_{σ • P} (σ x).

The restriction to A_F is the representation whose dual gives the action of the automorphism group on Weil differentials, in TauCeti.FieldTheory.FunctionField.Differential.Automorphism.

Main definitions

• TauCeti.placeFamilyRepresentation: the representation of F' ≃ₐ[F] F' on the families Place k F' → F', (σ • a) Q = σ (a (σ⁻¹ • Q)).
• TauCeti.repartitionRepresentation: its restriction to the repartition space A_F.

Main results

• TauCeti.placeFamilyRepresentation_mem_repartitionSpace_iff: the action preserves A_F.
• TauCeti.placeFamilyRepresentation_mem_adeleFiltration_smul_iff: it carries A_F(D) onto A_F(σ • D).
• TauCeti.placeFamilyRepresentation_mem_diagonalRepartitions_iff and TauCeti.placeFamilyRepresentation_const: it preserves the constant families, acting on their value by σ.
• TauCeti.placeFamilyRepresentation_smul and TauCeti.repartitionRepresentation_repartitionMul: it is σ-semilinear for multiplication by a function.
• TauCeti.repartitionRepresentation_singleRepartition: σ • ι_P x = ι_{σ • P} (σ x).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5 for repartitions and Section III.5 for the automorphism action on places.

The action on families indexed by the places

noncomputable def TauCeti.placeFamilyRepresentation (k : Type u) (F : Type v) (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] : Representation k Gal(F'/F) (Place k F' → F')

The automorphism group acting on families indexed by the places: σ sends a family a to the family whose entry at Q is σ (a (σ⁻¹ • Q)), so the entry a P is moved by σ to the place σ • P. It is k-linear because σ fixes F, hence k, pointwise.

@[simp]

theorem TauCeti.placeFamilyRepresentation_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (a : Place k F' → F') (Q : Place k F') : ((placeFamilyRepresentation k F F') σ) a Q = σ (a (σ⁻¹ • Q))

The defining formula (σ • a) Q = σ (a (σ⁻¹ • Q)) of the action on families.

@[simp]

theorem TauCeti.placeFamilyRepresentation_mem_adeleFiltration_smul_iff {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) {D : Divisor k F'} {a : Place k F' → F'} : ((placeFamilyRepresentation k F F') σ) a ∈ adeleFiltration (σ • D) ↔ a ∈ adeleFiltration D

The action carries A_F(D) onto A_F(σ • D): σ moves the valuation at a place to the valuation at the moved place, where the bound imposed by σ • D is the one D imposed before.

theorem TauCeti.placeFamilyRepresentation_mem_repartitionSpace_iff {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) {a : Place k F' → F'} : ((placeFamilyRepresentation k F F') σ) a ∈ repartitionSpace k F' ↔ a ∈ repartitionSpace k F'

The action preserves the repartition space: a family is integral at all but finitely many places exactly when its image is, because both are bounded by some divisor and the action moves the bounding divisor.

This is not @[simp]: TauCeti.mem_repartitionSpace_iff is, and it rewrites this left-hand side first.

@[simp]

theorem TauCeti.placeFamilyRepresentation_const {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (f : F') : ((placeFamilyRepresentation k F F') σ) (Function.const (Place k F') f) = Function.const (Place k F') (σ f)

The action on a constant family applies σ to its value.

@[simp]

theorem TauCeti.placeFamilyRepresentation_mem_diagonalRepartitions_iff {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) {a : Place k F' → F'} : ((placeFamilyRepresentation k F F') σ) a ∈ diagonalRepartitions k F' ↔ a ∈ diagonalRepartitions k F'

The action preserves the diagonal copy of F': a family is constant exactly when its image is.

theorem TauCeti.placeFamilyRepresentation_smul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (f : F') (a : Place k F' → F') : ((placeFamilyRepresentation k F F') σ) (f • a) = σ f • ((placeFamilyRepresentation k F F') σ) a

The action is σ-semilinear for multiplication by a function: σ • (f • a) is σ f • (σ • a).

The action on repartitions

noncomputable def TauCeti.repartitionRepresentation (k : Type u) (F : Type v) (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] : Representation k Gal(F'/F) ↥(repartitionSpace k F')

The automorphism group acting on the repartition space A_F of F' / k: the restriction of TauCeti.placeFamilyRepresentation to the stable subspace A_F.

@[simp]

theorem TauCeti.coe_repartitionRepresentation_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (a : ↥(repartitionSpace k F')) : ↑(((repartitionRepresentation k F F') σ) a) = ((placeFamilyRepresentation k F F') σ) ↑a

The action on repartitions is the action on the underlying families.

theorem TauCeti.repartitionRepresentation_repartitionMul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (hF : IsFunctionField k F') (f : F') (a : ↥(repartitionSpace k F')) : ((repartitionRepresentation k F F') σ) (((repartitionMul hF) f) a) = ((repartitionMul hF) (σ f)) (((repartitionRepresentation k F F') σ) a)

The action on repartitions is σ-semilinear: σ • (f · a) = σ f · (σ • a).

@[simp]

theorem TauCeti.repartitionRepresentation_singleRepartition {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (P : Place k F') (x : F') : ((repartitionRepresentation k F F') σ) ((singleRepartition P) x) = (singleRepartition (σ • P)) (σ x)

The action moves the repartition supported at a place to the moved place: σ • ι_P x = ι_{σ • P} (σ x).