Frobenius restriction over a finite constant field

Let K be a finite field and put q = #K. The map x ↦ x ^ (q ^ n) on any commutative K-algebra is the n-th iterate of the relative Frobenius. In particular it is a genuine K-algebra endomorphism: no Frobenius-twisted scalar action is needed.

This file packages that endomorphism as an algebra homomorphism and as a linear map, specializes the two tensor-restriction orientations, and records the principal-divisor and pole-budget identities needed by the Stepanov restriction argument.

def BGS.HasseWeil.powCardAlgHom (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) : A →ₐ[K] A

The n-fold relative Frobenius on a commutative algebra over the finite field K. Its underlying function is x ↦ x ^ ((#K) ^ n).

Equations

• BGS.HasseWeil.powCardAlgHom K A n = FiniteField.frobeniusAlgHom K A ^ n

@[simp]

theorem BGS.HasseWeil.powCardAlgHom_apply (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) (x : A) : (powCardAlgHom K A n) x = x ^ Fintype.card K ^ n

def BGS.HasseWeil.powCardLinearMap (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) : A →ₗ[K] A

The K-linear map underlying the n-fold relative Frobenius.

Equations

• BGS.HasseWeil.powCardLinearMap K A n = (BGS.HasseWeil.powCardAlgHom K A n).toLinearMap

@[simp]

theorem BGS.HasseWeil.powCardLinearMap_apply (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) (x : A) : (powCardLinearMap K A n) x = x ^ Fintype.card K ^ n

theorem BGS.HasseWeil.powCardLinearMap_add (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) (x y : A) : (powCardLinearMap K A n) (x + y) = (powCardLinearMap K A n) x + (powCardLinearMap K A n) y

theorem BGS.HasseWeil.powCardLinearMap_smul (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) (c : K) (x : A) : (powCardLinearMap K A n) (c • x) = c • (powCardLinearMap K A n) x

theorem BGS.HasseWeil.powCardLinearMap_mul (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) (x y : A) : (powCardLinearMap K A n) (x * y) = (powCardLinearMap K A n) x * (powCardLinearMap K A n) y

def BGS.HasseWeil.powCardTensorRestriction {K : Type u_3} {A : Type u_4} [Field K] [Fintype K] [CommRing A] [Algebra K A] {R S T : Submodule K A} (n : ℕ) (hmul : ∀ (x : ↥R) (y : ↥S), ↑x * ↑y ^ Fintype.card K ^ n ∈ T) : TensorProduct K ↥R ↥S →ₗ[K] ↥T

The tensor restriction induced by (x, y) ↦ x * y ^ ((#K) ^ n).

Equations

• BGS.HasseWeil.powCardTensorRestriction n hmul = BGS.HasseWeil.tensorRestriction (BGS.HasseWeil.powCardAlgHom K A n) ⋯

@[simp]

theorem BGS.HasseWeil.powCardTensorRestriction_tmul {K : Type u_3} {A : Type u_4} [Field K] [Fintype K] [CommRing A] [Algebra K A] {R S T : Submodule K A} (n : ℕ) (hmul : ∀ (x : ↥R) (y : ↥S), ↑x * ↑y ^ Fintype.card K ^ n ∈ T) (x : ↥R) (y : ↥S) : (powCardTensorRestriction n hmul) (x ⊗ₜ[K] y) = ⟨↑x * ↑y ^ Fintype.card K ^ n, ⋯⟩

def BGS.HasseWeil.powCardSwappedTensorRestriction {K : Type u_3} {A : Type u_4} [Field K] [Fintype K] [CommRing A] [Algebra K A] {R S T : Submodule K A} (n : ℕ) (hmul : ∀ (x : ↥R) (y : ↥S), ↑x ^ Fintype.card K ^ n * ↑y ∈ T) : TensorProduct K ↥R ↥S →ₗ[K] ↥T

The swapped tensor restriction induced by (x, y) ↦ x ^ ((#K) ^ n) * y.

Equations

• BGS.HasseWeil.powCardSwappedTensorRestriction n hmul = BGS.HasseWeil.swappedTensorRestriction (BGS.HasseWeil.powCardAlgHom K A n) ⋯

@[simp]

theorem BGS.HasseWeil.powCardSwappedTensorRestriction_tmul {K : Type u_3} {A : Type u_4} [Field K] [Fintype K] [CommRing A] [Algebra K A] {R S T : Submodule K A} (n : ℕ) (hmul : ∀ (x : ↥R) (y : ↥S), ↑x ^ Fintype.card K ^ n * ↑y ∈ T) (x : ↥R) (y : ↥S) : (powCardSwappedTensorRestriction n hmul) (x ⊗ₜ[K] y) = ⟨↑x ^ Fintype.card K ^ n * ↑y, ⋯⟩

@[instance_reducible]

noncomputable def BGS.HasseWeil.frobeniusRestrictionConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the frobenius restriction construction.

Equations

• BGS.HasseWeil.frobeniusRestrictionConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.frobeniusRestrictionConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_powCardLinearMap (K : Type u_1) [Field K] [Fintype K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (n : ℕ) : CorvajaZannier.finiteExtensionPrincipalDivisor K L ((powCardLinearMap K L n) x) = Fintype.card K ^ n • CorvajaZannier.finiteExtensionPrincipalDivisor K L x

Raising to (#K) ^ n scales every exhaustive place order by that integer.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_powCardLinearMap_apply (K : Type u_1) [Field K] [Fintype K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (n : ℕ) (v : CorvajaZannier.FiniteExtensionPlace K L) : (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((powCardLinearMap K L n) x)) v = ↑(Fintype.card K ^ n) * (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v

Pointwise form of the Frobenius order-scaling identity.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_powCardLinearMap (K : Type u_1) [Field K] [Fintype K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (n : ℕ) : finiteExtensionPoleDivisor K L ((powCardLinearMap K L n) x) = Fintype.card K ^ n • finiteExtensionPoleDivisor K L x

The pole divisor is scaled by the same power of the constant-field cardinality under iterated Frobenius.

theorem BGS.HasseWeil.powCardLinearMap_mem_scaledRiemannSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D : CorvajaZannier.FiniteExtensionDivisor K L} {x : L} (hx : x ∈ CorvajaZannier.finiteExtensionRiemannSpace K L D) (n : ℕ) : (powCardLinearMap K L n) x ∈ CorvajaZannier.finiteExtensionRiemannSpace K L (Fintype.card K ^ n • D)

Iterated Frobenius sends L(D) into L((#K)^n D).

theorem BGS.HasseWeil.mul_powCardLinearMap_mem_poleDivisor_budget (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (n : ℕ) : x * (powCardLinearMap K L n) y ∈ CorvajaZannier.finiteExtensionRiemannSpace K L (finiteExtensionPoleDivisor K L x + Fintype.card K ^ n • finiteExtensionPoleDivisor K L y)

The pole budget for (x, y) ↦ x * y ^ ((#K)^n).

theorem BGS.HasseWeil.powCardLinearMap_mul_mem_poleDivisor_budget (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (n : ℕ) : (powCardLinearMap K L n) x * y ∈ CorvajaZannier.finiteExtensionRiemannSpace K L (Fintype.card K ^ n • finiteExtensionPoleDivisor K L x + finiteExtensionPoleDivisor K L y)

The pole budget for the swapped product (x, y) ↦ x ^ ((#K)^n) * y.

noncomputable def BGS.HasseWeil.powCardRiemannTensorRestriction (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D E : CorvajaZannier.FiniteExtensionDivisor K L) (n : ℕ) : TensorProduct K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E) →ₗ[K] ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Fintype.card K ^ n • E))

Tensor restriction between Riemann spaces in the unswapped orientation.

Equations

• BGS.HasseWeil.powCardRiemannTensorRestriction K L D E n = BGS.HasseWeil.powCardTensorRestriction n ⋯

@[simp]

theorem BGS.HasseWeil.powCardRiemannTensorRestriction_tmul (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D E : CorvajaZannier.FiniteExtensionDivisor K L) (n : ℕ) (x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)) (y : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E)) : (powCardRiemannTensorRestriction K L D E n) (x ⊗ₜ[K] y) = ⟨↑x * ↑y ^ Fintype.card K ^ n, ⋯⟩

noncomputable def BGS.HasseWeil.powCardSwappedRiemannTensorRestriction (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D E : CorvajaZannier.FiniteExtensionDivisor K L) (n : ℕ) : TensorProduct K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E) →ₗ[K] ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (Fintype.card K ^ n • D + E))

Tensor restriction between Riemann spaces in the swapped orientation.

Equations

• BGS.HasseWeil.powCardSwappedRiemannTensorRestriction K L D E n = BGS.HasseWeil.powCardSwappedTensorRestriction n ⋯

@[simp]

theorem BGS.HasseWeil.powCardSwappedRiemannTensorRestriction_tmul (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D E : CorvajaZannier.FiniteExtensionDivisor K L) (n : ℕ) (x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)) (y : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E)) : (powCardSwappedRiemannTensorRestriction K L D E n) (x ⊗ₜ[K] y) = ⟨↑x ^ Fintype.card K ^ n * ↑y, ⋯⟩