Automorphisms of plane-curve constant extensions

For an algebraic extension E / K, this file transports every element of Gal(E/K) to the scalar extension of a plane-curve function field. The transported automorphisms act on E in the prescribed way and fix the original function field pointwise.

When K and E are finite, the scalar-extended function field has degree [E : K], is Galois over the original function field, and its full Galois group is identified with Gal(E/K). The finite-field Frobenius therefore acts with exact order [E : K] on the base-changed function field.

This file does not identify fixed points or rational places; those are the next local-geometric layer.

noncomputable def BGS.HasseWeil.tensorConstantAlgEquiv (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [CommRing L] [Algebra K E] [Algebra K L] (σ : Gal(E/K)) : TensorProduct K E L ≃ₐ[K] TensorProduct K E L

An automorphism of the constant field acting on the left factor of a tensor product.

Equations

• BGS.HasseWeil.tensorConstantAlgEquiv K E L σ = Algebra.TensorProduct.congr σ AlgEquiv.refl

@[simp]

theorem BGS.HasseWeil.tensorConstantAlgEquiv_tmul (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [CommRing L] [Algebra K E] [Algebra K L] (σ : Gal(E/K)) (e : E) (x : L) : (tensorConstantAlgEquiv K E L σ) (e ⊗ₜ[K] x) = σ e ⊗ₜ[K] x

theorem BGS.HasseWeil.tensorConstantAlgEquiv_includeRight (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [CommRing L] [Algebra K E] [Algebra K L] (σ : Gal(E/K)) (x : L) : (tensorConstantAlgEquiv K E L σ) (Algebra.TensorProduct.includeRight x) = Algebra.TensorProduct.includeRight x

noncomputable def BGS.HasseWeil.tensorConstantAutHom (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [CommRing L] [Algebra K E] [Algebra K L] : Gal(E/K) →* TensorProduct K E L ≃ₐ[K] TensorProduct K E L

The homomorphism sending a constant-field automorphism to its tensor-product action.

Equations

• BGS.HasseWeil.tensorConstantAutHom K E L = { toFun := BGS.HasseWeil.tensorConstantAlgEquiv K E L, map_one' := ⋯, map_mul' := ⋯ }

theorem BGS.HasseWeil.tensorConstantAutHom_injective (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [CommRing L] [Algebra K E] [Algebra K L] [Nontrivial L] : Function.Injective ⇑(tensorConstantAutHom K E L)

noncomputable def BGS.HasseWeil.planeCurveConstantAlgEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] (σ : Gal(E/K)) : CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f) ≃ₐ[K] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

A constant-field automorphism transported to the base-changed plane-curve function field.

Equations

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

noncomputable def BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgHom (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : CorvajaZannier.PlaneCurveFunctionField f →ₐ[K] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

The embedding of the original plane-curve function field into its constant-field base change.

Equations

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

@[simp]

theorem BGS.HasseWeil.planeCurveConstantAlgEquiv_baseChange (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] (σ : Gal(E/K)) (x : CorvajaZannier.PlaneCurveFunctionField f) : (planeCurveConstantAlgEquiv K E f hf hfE σ) ((planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE) x) = (planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE) x

@[simp]

theorem BGS.HasseWeil.planeCurveConstantAlgEquiv_algebraMap (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] (σ : Gal(E/K)) (e : E) : (planeCurveConstantAlgEquiv K E f hf hfE σ) ((algebraMap E (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))) e) = (algebraMap E (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))) (σ e)

noncomputable def BGS.HasseWeil.planeCurveConstantAutHom (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : Gal(E/K) →* CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f) ≃ₐ[K] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

The action of constant-field automorphisms on the base-changed plane-curve function field.

Equations

• BGS.HasseWeil.planeCurveConstantAutHom K E f hf hfE = { toFun := BGS.HasseWeil.planeCurveConstantAlgEquiv K E f hf hfE, map_one' := ⋯, map_mul' := ⋯ }

theorem BGS.HasseWeil.planeCurveConstantAutHom_injective (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : Function.Injective ⇑(planeCurveConstantAutHom K E f hf hfE)

@[reducible]

noncomputable def BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgebra (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : Algebra (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))

The algebra structure on the base-changed function field induced by the canonical embedding of the original function field.

Equations

• BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgebra K E f hf hfE = (BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE).toAlgebra

noncomputable def BGS.HasseWeil.planeCurveFunctionFieldBaseChangeLinearEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : TensorProduct K (CorvajaZannier.PlaneCurveFunctionField f) E ≃ₗ[CorvajaZannier.PlaneCurveFunctionField f] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

The base-changed function field has the expected dimension over the original function field.

Equations

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

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChange_finrank (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : Module.finrank (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)) = Module.finrank K E

noncomputable def BGS.HasseWeil.planeCurveConstantAlgEquivOverBase (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] (σ : Gal(E/K)) : CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f) ≃ₐ[CorvajaZannier.PlaneCurveFunctionField f] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

A constant-field automorphism, viewed as an automorphism over the embedded original function field.

Equations

• BGS.HasseWeil.planeCurveConstantAlgEquivOverBase K E f hf hfE σ = { toEquiv := (BGS.HasseWeil.planeCurveConstantAlgEquiv K E f hf hfE σ).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.planeCurveConstantAutOverBaseHom (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : Gal(E/K) →* CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f) ≃ₐ[CorvajaZannier.PlaneCurveFunctionField f] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

The constant-field automorphism action viewed over the embedded original function field.

Equations

• BGS.HasseWeil.planeCurveConstantAutOverBaseHom K E f hf hfE = { toFun := BGS.HasseWeil.planeCurveConstantAlgEquivOverBase K E f hf hfE, map_one' := ⋯, map_mul' := ⋯ }

theorem BGS.HasseWeil.planeCurveConstantAutOverBaseHom_injective (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] : Function.Injective ⇑(planeCurveConstantAutOverBaseHom K E f hf hfE)

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChange_isGalois (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Finite K] [Finite E] : IsGalois (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))

noncomputable def BGS.HasseWeil.planeCurveConstantAutOverBaseMulEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Fintype K] [Finite E] : Gal(E/K) ≃* CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f) ≃ₐ[CorvajaZannier.PlaneCurveFunctionField f] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

The Galois group of the constant extension is exactly the Galois group of the enlarged constants.

Equations

• BGS.HasseWeil.planeCurveConstantAutOverBaseMulEquiv K E f hf hfE = MulEquiv.ofBijective (BGS.HasseWeil.planeCurveConstantAutOverBaseHom K E f hf hfE) ⋯

noncomputable def BGS.HasseWeil.planeCurveConstantFrobeniusAlgEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Fintype K] : CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f) ≃ₐ[K] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

Frobenius on the enlarged constant field, transported to the base-changed plane-curve function field.

Equations

• BGS.HasseWeil.planeCurveConstantFrobeniusAlgEquiv K E f hf hfE = BGS.HasseWeil.planeCurveConstantAlgEquiv K E f hf hfE (FiniteField.frobeniusAlgEquivOfAlgebraic K E)

@[simp]

theorem BGS.HasseWeil.planeCurveConstantFrobeniusAlgEquiv_algebraMap (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Fintype K] (e : E) : (planeCurveConstantFrobeniusAlgEquiv K E f hf hfE) ((algebraMap E (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))) e) = (algebraMap E (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))) (e ^ Fintype.card K)

@[simp]

theorem BGS.HasseWeil.planeCurveConstantFrobeniusAlgEquiv_baseChange (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Fintype K] (x : CorvajaZannier.PlaneCurveFunctionField f) : (planeCurveConstantFrobeniusAlgEquiv K E f hf hfE) ((planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE) x) = (planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE) x

theorem BGS.HasseWeil.orderOf_planeCurveConstantFrobeniusAlgEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Fintype K] [Finite E] : orderOf (planeCurveConstantFrobeniusAlgEquiv K E f hf hfE) = Module.finrank K E

theorem BGS.HasseWeil.natCard_zpowers_planeCurveConstantFrobeniusAlgEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] [Fintype K] [Finite E] : Nat.card ↥(Subgroup.zpowers (planeCurveConstantFrobeniusAlgEquiv K E f hf hfE)) = Module.finrank K E