Documentation

TauCeti.FieldTheory.FunctionField.Differential.Automorphism

The automorphism group acting on Weil differentials #

Let F' / F be an extension of fields and k a subfield of F. An F-automorphism σ of F' acts on the repartition space A_F of F' / k (TauCeti.repartitionRepresentation), and hence, contragrediently, on the k-linear forms on A_F:

(σ • ω) a = ω (σ⁻¹ • a).

This is Mathlib's dual representation Representation.dual. Since the action on repartitions carries A_F(D) onto A_F(σ • D) and preserves the diagonal copy of F', it carries the Weil differentials bounded by D onto those bounded by σ • D. So it preserves the space Ω_F of Weil differentials, which becomes a k-linear representation of F' ≃ₐ[F] F'.

The action is compatible with all the structure of Ω_F. It is σ-semilinear for the F'-vector space structure: σ • (f · ω) = σ f · (σ • ω). It moves local components with the places: (σ • ω)_{σ • P} (σ x) = ω_P (x). The divisor of a Weil differential is equivariant, (σ • ω) = σ • (ω). In particular the canonical class is fixed by every automorphism.

Main definitions #

Main results #

References #

The action on linear forms on repartitions #

source
theorem TauCeti.repartitionRepresentation_dual_eq_zero_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)) {ω : Module.Dual k ↥(repartitionSpace k F')} :
((repartitionRepresentation k F F').dual σ) ω = 0 ↔ ω = 0

The action of an automorphism on linear forms is injective.

source
theorem TauCeti.repartitionRepresentation_dual_mem_weilDifferentialFiltration_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'} {ω : Module.Dual k ↥(repartitionSpace k F')} :
((repartitionRepresentation k F F').dual σ) ω ∈ weilDifferentialFiltration (σ • D) ↔ ω ∈ weilDifferentialFiltration D

The action carries Ω_F(D) onto Ω_F(σ • D): a linear form on A_F vanishes on A_F(D) + F' exactly when its image under σ vanishes on A_F(σ • D) + F'.

source
theorem TauCeti.repartitionRepresentation_dual_mem_weilDifferentialSpace_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)) {ω : Module.Dual k ↥(repartitionSpace k F')} :
((repartitionRepresentation k F F').dual σ) ω ∈ weilDifferentialSpace k F' ↔ ω ∈ weilDifferentialSpace k F'

The action preserves the space Ω_F of Weil differentials.

source
theorem TauCeti.repartitionRepresentation_dual_repartitionDualMul {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') (ω : Module.Dual k ↥(repartitionSpace k F')) :
((repartitionRepresentation k F F').dual σ) (((repartitionDualMul hF) f) ω) = ((repartitionDualMul hF) (σ f)) (((repartitionRepresentation k F F').dual σ) ω)

The action on linear forms is σ-semilinear over F': σ • (f · ω) = σ f · (σ • ω).

source
theorem TauCeti.repartitionDualComponent_repartitionRepresentation_dual {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)) (ω : Module.Dual k ↥(repartitionSpace k F')) (P : Place k F') (x : F') :
(repartitionDualComponent (((repartitionRepresentation k F F').dual σ) ω) (σ • P)) (σ x) = (repartitionDualComponent ω P) x

The action moves local components with the places: (σ • ω)_{σ • P} (σ x) = ω_P (x), because σ⁻¹ moves the repartition ι_{σ • P} (σ x) to ι_P x.

This is not @[simp]: TauCeti.repartitionDualComponent_apply and Representation.dual_apply rewrite its left-hand side first.

The action on Weil differentials #

source
noncomputable def TauCeti.weilDifferentialRepresentation (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) ↥(weilDifferentialSpace k F')

The automorphism group acting on the Weil differentials of F' / k: the restriction of the dual of TauCeti.repartitionRepresentation to the stable subspace Ω_F, so that (σ • ω) a = ω (σ⁻¹ • a).

Instances For
    source
    @[simp]
    theorem TauCeti.coe_weilDifferentialRepresentation_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)) (ω : ↥(weilDifferentialSpace k F')) :
    ↑(((weilDifferentialRepresentation k F F') σ) ω) = ((repartitionRepresentation k F F').dual σ) ↑ω

    The action on Weil differentials is the action on the underlying linear forms.

    source
    theorem TauCeti.repartitionDualComponent_weilDifferentialRepresentation {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)) (ω : ↥(weilDifferentialSpace k F')) (P : Place k F') (x : F') :
    (repartitionDualComponent (↑(((weilDifferentialRepresentation k F F') σ) ω)) (σ • P)) (σ x) = (repartitionDualComponent (↑ω) P) x

    The action on Weil differentials moves local components with the places: (σ • ω)_{σ • P} (σ x) = ω_P (x).

    source
    theorem TauCeti.weilDifferentialRepresentation_weilDifferentialSpaceMul {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') (ω : ↥(weilDifferentialSpace k F')) :
    ((weilDifferentialRepresentation k F F') σ) (((weilDifferentialSpaceMul hF) f) ω) = ((weilDifferentialSpaceMul hF) (σ f)) (((weilDifferentialRepresentation k F F') σ) ω)

    The action on Weil differentials is σ-semilinear over F', for the multiplication TauCeti.weilDifferentialSpaceMul that makes Ω_F an F'-vector space.

    The divisor of a moved Weil differential #

    source
    @[simp]
    theorem TauCeti.weilDifferentialDivisor_repartitionRepresentation_dual {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') (hex : IsIntegrallyClosedIn k F') {ω : Module.Dual k ↥(repartitionSpace k F')} (hmem : ω ∈ weilDifferentialSpace k F') (hω : ω ≠ 0) :
    weilDifferentialDivisor hF hex ⋯ ⋯ = σ • weilDifferentialDivisor hF hex hmem hω

    The divisor of a Weil differential is equivariant: (σ • ω) = σ • (ω). The action carries the divisors bounding ω bijectively onto those bounding σ • ω, preserving the order, so it carries the greatest one to the greatest one.

    source
    @[simp]
    theorem TauCeti.weilDifferentialOrder_repartitionRepresentation_dual {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') (hex : IsIntegrallyClosedIn k F') {ω : Module.Dual k ↥(repartitionSpace k F')} (hmem : ω ∈ weilDifferentialSpace k F') (hω : ω ≠ 0) (Q : Place k F') :
    weilDifferentialOrder hF hex ⋯ ⋯ Q = weilDifferentialOrder hF hex hmem hω (σ⁻¹ • Q)

    The order of σ • ω at a place Q is the order of ω at σ⁻¹ • Q. This is the coefficient form of TauCeti.weilDifferentialDivisor_repartitionRepresentation_dual.

    source
    @[simp]
    theorem TauCeti.smul_canonicalClass {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') (hex : IsIntegrallyClosedIn k F') :
    σ • canonicalClass hF hex = canonicalClass hF hex

    Automorphisms fix the canonical class: moving a nonzero Weil differential by σ gives a nonzero Weil differential, whose divisor is the moved divisor.