Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistMultiplication

Multiplication presentation of Frobenius-twist constant extensions #

Let T = S ⊗[C] N, and let F_g be a Frobenius-twist fixed field in T. The multiplication map from S ⊗[C] F_g to T is an equivalence over the original function-field base. Thus every twist becomes the same top field after extending constants from C to S.

This is the field-level transport needed to compare the differents, genera, and Riemann budgets of all twists without identifying the twist fields over C(X) themselves.

source
noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusTwistMultiplicationAlgEquiv (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional L N] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; have hExactF := ⋯; ExactConstantExtension C (↥F) S ≃ₐ[L] ExactConstantExtension C N S

Multiplication identifies the constant extension of a Frobenius-twist field with the common exact constant extension.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusTwistMultiplicationAlgEquivOverConstants (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional L N] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
    let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; have hExactF := ⋯; ExactConstantExtension C (↥F) S ≃ₐ[S] ExactConstantExtension C N S

    Multiplication also identifies the constant extension of a Frobenius-twist field with the common top field as an algebra over the enlarged constant field S. This is the scalar structure used to transport the intrinsic genus.

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