Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwist

Fixed fields of Frobenius twists #

Let C ⊆ L ⊆ N, let C be algebraically closed in N, and let S / C be a finite Galois extension of finite fields. The exact constant extension T = S ⊗[C] N has Galois group

Gal(T/L) ≃ Gal(S/C) × Gal(N/L).

For g ∈ Gal(N/L), this file constructs the automorphism of T represented by (Frob, g), its cyclic subgroup, and its fixed field. If |Gal(N/L)| divides [S : C], the cyclic subgroup has order [S : C] and meets the original function-field factor trivially. Consequently T is a finite Galois extension of the twist field of degree [S : C], while the twist field has degree [N : L] over L.

These are the structural assertions in the setup of Stichtenoth, Proposition 5.2.8. Exactness of the constant field of the twist requires, in addition, stability of relative algebraic closedness under finite separable base change; that separate regular-base-change lemma is not assumed here.

source
noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusTwist (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] [IsGalois C S] [Fintype C] (g : Gal(N/L)) :
ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

The automorphism of the exact constant extension represented by (Frob, g) under the direct-product description of its Galois group.

Equations
Instances For
    source
    noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusTwistSubgroup (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] [IsGalois C S] [Fintype C] (g : Gal(N/L)) :
    Subgroup (ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S)

    The cyclic subgroup generated by a Frobenius twist.

    Equations
    Instances For
      source
      noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusTwistField (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] [Fintype C] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) :
      IntermediateField L (ExactConstantExtension C N S)

      The fixed field of the cyclic subgroup generated by a Frobenius twist.

      Equations
      Instances For
        source
        noncomputable def BGS.HasseWeil.exactConstantExtensionExtendedBaseField (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] [IsGalois L N] (hExact : algebraicClosure C N = ⊥) :
        IntermediateField L (ExactConstantExtension C N S)

        The extended base inside the exact constant extension, characterized as the fixed field of the original function-field factor. In the rational function specialization this is the copy of S(X).

        Equations
        Instances For
          source
          theorem BGS.HasseWeil.orderOf_exactConstantExtensionFrobeniusTwist (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] [IsGalois C S] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
          orderOf (exactConstantExtensionFrobeniusTwist C L N S g) = Module.finrank C S

          Every Frobenius twist has order [S : C] when the order of the original function-field Galois group divides [S : C].

          source
          theorem BGS.HasseWeil.natCard_exactConstantExtensionFrobeniusTwistSubgroup (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] [IsGalois C S] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
          Nat.card ↥(exactConstantExtensionFrobeniusTwistSubgroup C L N S g) = Module.finrank C S

          The cyclic subgroup generated by a Frobenius twist has cardinality [S : C].

          source
          theorem BGS.HasseWeil.exactConstantExtensionFrobeniusTwistSubgroup_inf_quotientKer (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] [IsGalois L N] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
          exactConstantExtensionFrobeniusTwistSubgroup C L N S g ⊓ (exactConstantExtensionConstantQuotient C L N S hExact).ker = ⊥

          The twist subgroup meets the kernel of restriction to the enlarged constants trivially.

          source
          theorem BGS.HasseWeil.exactConstantExtensionFrobeniusTwistSubgroup_inf_functionRange (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] [IsGalois L N] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
          exactConstantExtensionFrobeniusTwistSubgroup C L N S g ⊓ (exactConstantExtensionFunctionAutHom C L N S).range = ⊥

          Equivalently, the twist subgroup meets the embedded original function-field Galois group trivially.

          source
          theorem BGS.HasseWeil.frobeniusTwistField_sup_extendedBaseField_eq_top (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] [IsGalois L N] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) :
          exactConstantExtensionFrobeniusTwistField C L N S hExact g ⊔ exactConstantExtensionExtendedBaseField C L N S hExact = ⊤

          A twist field and the extended base generate the entire exact constant extension. This is the fixed-field form of T = T_g S in Stichtenoth, Proposition 5.2.8(b).

          source
          theorem BGS.HasseWeil.finrank_exactConstantExtension_over_frobeniusTwistField (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) :
          Module.finrank (↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g)) (ExactConstantExtension C N S) = Module.finrank C S

          The exact constant extension has degree [S : C] over the Frobenius twist field.

          source
          theorem BGS.HasseWeil.finiteDimensional_exactConstantExtension_over_frobeniusTwistField (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] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) :
          FiniteDimensional (↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g)) (ExactConstantExtension C N S)

          The exact constant extension is finite-dimensional over every Frobenius twist field.

          source
          theorem BGS.HasseWeil.isGalois_exactConstantExtension_over_frobeniusTwistField (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] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/L)) :
          IsGalois (↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g)) (ExactConstantExtension C N S)

          The exact constant extension is Galois over every Frobenius twist field. This only uses the general theorem that a field is Galois over the fixed field of a finite group action.

          source
          theorem BGS.HasseWeil.finrank_frobeniusTwistField_over_base (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) :
          Module.finrank L ↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g) = Module.finrank L N

          Every Frobenius twist field has the same degree over L as the original function field N.

          source
          theorem BGS.HasseWeil.natCard_aut_exactConstantExtension_over_frobeniusTwistField (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) :
          Nat.card (ExactConstantExtension C N S ≃ₐ[↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g)] ExactConstantExtension C N S) = Module.finrank C S

          The Galois group over a Frobenius twist field has cardinality [S : C].