Degree-one residues over a square constant field

For a function field over a finite field S, a finite place of constant-field degree one has residue field of cardinality #S. If #S = (#K)^2, every residue therefore satisfies the half-Frobenius square identity used by the semilinear Stepanov restriction.

@[instance_reducible]

noncomputable def BGS.HasseWeil.squareFieldResiduePolynomialAlgebra (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra (Polynomial S) L

The algebra structure from S[X] to L used in the square field residue construction.

Equations

• BGS.HasseWeil.squareFieldResiduePolynomialAlgebra S L = ((algebraMap (RatFunc S) L).comp (algebraMap (Polynomial S) (RatFunc S))).toAlgebra

theorem BGS.HasseWeil.squareFieldResiduePolynomialScalarTower (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : IsScalarTower (Polynomial S) (RatFunc S) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.squareFieldResidueFiniteConstantAlgebra (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra S ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S L)

The algebra structure from S to (RatFuncFiniteIntegralClosure S L) used in the square field residue construction.

Equations

• BGS.HasseWeil.squareFieldResidueFiniteConstantAlgebra S L = ((algebraMap (Polynomial S) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure S L)).comp (algebraMap S (Polynomial S))).toAlgebra

theorem BGS.HasseWeil.squareFieldResidueFiniteConstantTower (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : IsScalarTower S (Polynomial S) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S L)

theorem BGS.HasseWeil.finiteExtensionFinitePlace_residue_squareFrobenius_of_degree_one (K : Type u_1) (S : Type u_2) [Fintype K] [Field S] [Fintype S] [DecidableEq S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] (hcard : Fintype.card S = Fintype.card K ^ 2) (q : CorvajaZannier.FiniteExtensionFinitePlace S L) (hdegree : CorvajaZannier.finiteExtensionPlaceDegree S L (Sum.inl q) = 1) (z : q.asIdeal.ResidueField) : z ^ Fintype.card K ^ 2 = z

A degree-one finite place over a square constant field has the quadratic half-Frobenius identity in its residue field.