Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosureConstants

Constants and restriction for the function-field Galois closure #

Equip the chosen normal closure of L / K(t) with its induced K-algebra structure, take the algebraic constant field, and restrict every K(t)-automorphism to those constants. Over a finite base field the constant field is finite Galois and its automorphism group is cyclic, generated by Frobenius. The restriction map is surjective: a constant fixed by its image is fixed by the full Galois group over K(t), hence lies in K(t); because it is algebraic over K, the exact constant-field theorem for K(t) puts it in K.

source
@[instance_reducible]
noncomputable instance BGS.HasseWeil.functionFieldNormalClosureConstantAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
Algebra K ↥(FunctionFieldNormalClosure K L)
Equations
source
instance BGS.HasseWeil.functionFieldNormalClosureConstantTower (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
IsScalarTower K (RatFunc K) ↥(FunctionFieldNormalClosure K L)
source
@[reducible, inline]
noncomputable abbrev BGS.HasseWeil.FunctionFieldNormalClosureConstantField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
IntermediateField K ↥(FunctionFieldNormalClosure K L)

The algebraic constant field of the chosen Galois closure.

Equations
Instances For
    source
    noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantRestriction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Gal(↥(FunctionFieldNormalClosure K L)/RatFunc K) →* Gal(↥(FunctionFieldNormalClosureConstantField K L)/K)

    Restriction of a K(t)-automorphism of the normal closure to its algebraic constant field.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.HasseWeil.functionFieldNormalClosureConstantRestriction_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (g : Gal(↥(FunctionFieldNormalClosure K L)/RatFunc K)) (c : ↥(FunctionFieldNormalClosureConstantField K L)) :
      ((functionFieldNormalClosureConstantRestriction K L) g) c = ⟨g ↑c, ⋯⟩
      source
      theorem BGS.HasseWeil.mem_functionFieldNormalClosureConstantRestriction_ker_iff (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (g : Gal(↥(FunctionFieldNormalClosure K L)/RatFunc K)) :
      g ∈ (functionFieldNormalClosureConstantRestriction K L).ker ↔ ∀ (c : ↥(FunctionFieldNormalClosureConstantField K L)), g ↑c = ↑c

      The kernel consists exactly of automorphisms fixing every algebraic constant.

      source
      theorem BGS.HasseWeil.functionFieldNormalClosureConstantRestriction_surjective (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] :
      Function.Surjective ⇑(functionFieldNormalClosureConstantRestriction K L)

      Every automorphism of the algebraic constant field extends to an automorphism of the normal closure over K(t).

      The proof uses fixed fields rather than constructing a constant compositum. If an algebraic constant is fixed by the image of the restriction map, then it is fixed by every automorphism of the normal closure over K(t), so the Galois fixed-field theorem puts it in K(t). The rational function field has no elements algebraic over K except K itself. Thus the image has trivial fixed field and is the full constant-field Galois group.

      source
      theorem BGS.HasseWeil.functionFieldNormalClosureConstantField_isExact (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
      algebraicClosure ↥(FunctionFieldNormalClosureConstantField K L) ↥(FunctionFieldNormalClosure K L) = ⊥

      After enlarging the base constants to the algebraic constants of the normal closure, that field is the exact constant field: no further element of the normal closure is algebraic over it.

      source
      @[instance_reducible]
      noncomputable def BGS.HasseWeil.normalClosureConstantModule (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
      Module K ↥(FunctionFieldNormalClosureConstantField K L)

      The module structure of (FunctionFieldNormalClosureConstantField K L) over K used in the function field normal closure constants construction.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.orderOf_functionFieldNormalClosureConstantFrobenius (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Fintype K] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
        orderOf (FiniteField.frobeniusAlgEquivOfAlgebraic K ↥(FunctionFieldNormalClosureConstantField K L)) = Module.finrank K ↥(FunctionFieldNormalClosureConstantField K L)

        Frobenius on the finite algebraic constant field has order equal to its degree over K.