The rational-function field in an exact constant extension

Let C be the exact constant field of a function field N / C(X), and let S / C be a finite Galois extension. The tensor product S ⊗[C] N is then a field. This file constructs its canonical S(X)-algebra structure and proves that it is compatible with both copies of C(X).

For finite Galois N / C(X), the tensor product is finite and separable over S(X). The final equivalence identifies the polynomial normalization after constant extension with the normalization used by the project's finite-place model.

@[instance_reducible]

noncomputable def BGS.HasseWeil.constantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the rat func exact constant extension construction.

Equations

• BGS.HasseWeil.constantAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap C (RatFunc C))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.polynomialAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra (Polynomial C) N

The algebra structure from C[X] to N used in the rat func exact constant extension construction.

Equations

• BGS.HasseWeil.polynomialAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap (Polynomial C) (RatFunc C))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.ratFuncCoefficientPolynomialAlgebra (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Algebra (Polynomial C) (Polynomial S)

The algebra structure from C[X] to S[X] used in the rat func exact constant extension construction.

Equations

• BGS.HasseWeil.ratFuncCoefficientPolynomialAlgebra C S = Polynomial.algebra C S

@[instance_reducible]

noncomputable def BGS.HasseWeil.coefficientPolynomialModule (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Module (Polynomial C) (Polynomial S)

The module structure of S[X] over C[X] used in the rat func exact constant extension construction.

Equations

• BGS.HasseWeil.coefficientPolynomialModule C S = Algebra.toModule

theorem BGS.HasseWeil.coefficientPolynomialFlat (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] : Module.Flat (Polynomial C) (Polynomial S)

theorem BGS.HasseWeil.constantPolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (Polynomial C) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.targetPolynomialAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] : Algebra (Polynomial S) (ExactConstantExtension C N S)

The algebra structure from S[X] to (ExactConstantExtension C N S) used in the rat func exact constant extension construction.

Equations

• BGS.HasseWeil.targetPolynomialAlgebra C S N = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S N

noncomputable def BGS.HasseWeil.ratFuncToExactConstantExtension (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : RatFunc S →ₐ[S] ExactConstantExtension C N S

The canonical copy of S(X) inside the exact constant extension, obtained by extending the evaluated S[X]-algebra map.

Equations

• BGS.HasseWeil.ratFuncToExactConstantExtension C S N hExact = RatFunc.liftAlgHom (Polynomial.aeval (BGS.HasseWeil.polynomialTensorCancelEvaluationPoint C S N)) ⋯

theorem BGS.HasseWeil.ratFuncToExactConstantExtension_injective (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : Function.Injective ⇑(ratFuncToExactConstantExtension C S N hExact)

theorem BGS.HasseWeil.ratFuncToExactConstantExtension_algebraMap (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (p : Polynomial S) : (ratFuncToExactConstantExtension C S N hExact) ((algebraMap (Polynomial S) (RatFunc S)) p) = (Polynomial.aeval (polynomialTensorCancelEvaluationPoint C S N)) p

theorem BGS.HasseWeil.ratFuncToExactConstantExtension_X (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : (ratFuncToExactConstantExtension C S N hExact) RatFunc.X = polynomialTensorCancelEvaluationPoint C S N

@[reducible]

noncomputable def BGS.HasseWeil.ratFuncExactConstantExtensionAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : Algebra (RatFunc S) (ExactConstantExtension C N S)

The algebra structure induced by the canonical copy of S(X).

Equations

• BGS.HasseWeil.ratFuncExactConstantExtensionAlgebra C S N hExact = (BGS.HasseWeil.ratFuncToExactConstantExtension C S N hExact).toAlgebra

theorem BGS.HasseWeil.rationalBase_algebraMap_eq (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : algebraMap (RatFunc C) (ExactConstantExtension C N S) = (algebraMap (RatFunc S) (ExactConstantExtension C N S)).comp (algebraMap (RatFunc C) (RatFunc S))

The copy of C(X) obtained through coefficient extension to S(X) agrees with the copy coming from the right tensor factor N.

theorem BGS.HasseWeil.rationalBase_scalarTower (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : IsScalarTower (RatFunc C) (RatFunc S) (ExactConstantExtension C N S)

The rational-function coefficient extension and the exact constant extension form a scalar tower.

theorem BGS.HasseWeil.finiteDimensional_over_extendedRatFunc (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [FiniteDimensional (RatFunc C) N] : FiniteDimensional (RatFunc S) (ExactConstantExtension C N S)

If N / C(X) is finite, then the exact constant extension is finite over the enlarged rational function field S(X).

theorem BGS.HasseWeil.isSeparable_exactConstantExtension_over_baseRatFunc (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Algebra.IsSeparable (RatFunc C) N] : Algebra.IsSeparable (RatFunc C) (ExactConstantExtension C N S)

For a finite separable N / C(X), the exact constant extension remains separable over the original rational function field C(X).

theorem BGS.HasseWeil.isSeparable_over_extendedRatFunc (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Algebra.IsSeparable (RatFunc C) N] : Algebra.IsSeparable (RatFunc S) (ExactConstantExtension C N S)

For a finite separable N / C(X), the exact constant extension is separable over the enlarged rational function field S(X).

theorem BGS.HasseWeil.scalarTower_constant_ratFunc_exactConstantExtension (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : IsScalarTower S (RatFunc S) (ExactConstantExtension C N S)

The constant field, its rational function field, and the exact constant extension form a scalar tower.

noncomputable def BGS.HasseWeil.exactConstantExtensionNormalizationAlgEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Fintype C] [Finite S] : TensorProduct C S ↥(integralClosure (Polynomial C) N) ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S (ExactConstantExtension C N S))

The polynomial normalization obtained after extending the constants is the normalization used by the rational-function finite-place model.

Equations

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