Constant extensions of rational function fields

For a finite field extension S / K, this file constructs the coefficient embedding K(X) → S(X) and proves that S(X) is a finite-dimensional K(X)-vector space of dimension [S : K].

The construction is explicit. We first localize S[X] at the images of the nonzero polynomials in K[X], prove that this localization is a field, and identify it with S(X). This is the rational-function-field base-change input needed for the later constant extension of a general function field.

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.polynomialCoefficientAlgebra K S = (Polynomial.mapRingHom (algebraMap K S)).toAlgebra

theorem BGS.HasseWeil.polynomialCoefficientFaithfulSMul (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : FaithfulSMul (Polynomial K) (Polynomial S)

noncomputable def BGS.HasseWeil.ratFuncCoefficientPolynomialAlgHom (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : Polynomial K →ₐ[K] Polynomial S

The coefficient extension on polynomial rings.

Equations

• BGS.HasseWeil.ratFuncCoefficientPolynomialAlgHom K S = Polynomial.mapAlgHom (Algebra.ofId K S)

theorem BGS.HasseWeil.ratFuncCoefficientPolynomialAlgHom_injective (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : Function.Injective ⇑(ratFuncCoefficientPolynomialAlgHom K S)

noncomputable def BGS.HasseWeil.ratFuncCoefficientAlgHom (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : RatFunc K →ₐ[K] RatFunc S

The canonical coefficient extension K(X) → S(X).

Equations

• BGS.HasseWeil.ratFuncCoefficientAlgHom K S = RatFunc.mapAlgHom (BGS.HasseWeil.ratFuncCoefficientPolynomialAlgHom K S) ⋯

theorem BGS.HasseWeil.ratFuncCoefficientAlgHom_injective (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : Function.Injective ⇑(ratFuncCoefficientAlgHom K S)

theorem BGS.HasseWeil.ratFuncCoefficientAlgHom_algebraMap (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] (p : Polynomial K) : (ratFuncCoefficientAlgHom K S) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (Polynomial S) (RatFunc S)) ((algebraMap (Polynomial K) (Polynomial S)) p)

@[reducible]

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

The algebra structure on S(X) induced by coefficient extension.

Equations

• BGS.HasseWeil.ratFuncCoefficientAlgebra K S = (BGS.HasseWeil.ratFuncCoefficientAlgHom K S).toAlgebra

@[instance_reducible]

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

The algebra structure from (RatFunc K) to (RatFunc S) used in the rat func constant extension construction.

Equations

• BGS.HasseWeil.ratFuncCoefficientAlgebraInstance K S = BGS.HasseWeil.ratFuncCoefficientAlgebra K S

@[reducible, inline]

abbrev BGS.HasseWeil.RatFuncConstantLocalization (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : Type u_2

Localize S[X] by the images of all nonzero polynomials in K[X].

Equations

• BGS.HasseWeil.RatFuncConstantLocalization K S = Localization (Submonoid.map (algebraMap (Polynomial K) (Polynomial S)) (nonZeroDivisors (Polynomial K)))

theorem BGS.HasseWeil.ratFuncConstantLocalizationIsDomain (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : IsDomain (RatFuncConstantLocalization K S)

@[instance_reducible]

noncomputable def BGS.HasseWeil.ratFuncConstantLocalizationAlgebra (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : Algebra (RatFunc K) (RatFuncConstantLocalization K S)

The algebra structure on the localization used to extend rational-function constants.

Equations

• BGS.HasseWeil.ratFuncConstantLocalizationAlgebra K S = (IsLocalization.map (BGS.HasseWeil.RatFuncConstantLocalization K S) (algebraMap (Polynomial K) (Polynomial S)) ⋯).toAlgebra

theorem BGS.HasseWeil.ratFuncConstantLocalizationScalarTower (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : IsScalarTower (Polynomial K) (RatFunc K) (RatFuncConstantLocalization K S)

theorem BGS.HasseWeil.polynomialCoefficientModuleFinite (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : Module.Finite (Polynomial K) (Polynomial S)

theorem BGS.HasseWeil.ratFuncConstantLocalizationIsLocalization (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : IsLocalization (Algebra.algebraMapSubmonoid (Polynomial S) (nonZeroDivisors (Polynomial K))) (RatFuncConstantLocalization K S)

theorem BGS.HasseWeil.ratFuncConstantLocalizationFinite (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : Module.Finite (RatFunc K) (RatFuncConstantLocalization K S)

@[instance_reducible]

noncomputable def BGS.HasseWeil.ratFuncConstantLocalizationField (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : Field (RatFuncConstantLocalization K S)

The field structure on that localization.

Equations

• BGS.HasseWeil.ratFuncConstantLocalizationField K S = ⋯.toField

noncomputable def BGS.HasseWeil.ratFuncConstantLocalizationToRatFunc (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] : RatFuncConstantLocalization K S →+* RatFunc S

Map the localization at nonzero base polynomials into the rational function field.

Equations

• BGS.HasseWeil.ratFuncConstantLocalizationToRatFunc K S = IsLocalization.map (RatFunc S) (RingHom.id (Polynomial S)) ⋯

noncomputable def BGS.HasseWeil.ratFuncToConstantLocalization (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : RatFunc S →+* RatFuncConstantLocalization K S

Embed rational functions into the constant-extension localization.

Equations

• BGS.HasseWeil.ratFuncToConstantLocalization K S = IsFractionRing.lift ⋯

noncomputable def BGS.HasseWeil.ratFuncConstantLocalizationRingEquiv (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : RatFuncConstantLocalization K S ≃+* RatFunc S

The localization of S[X] at nonzero K[X] is the full rational function field S(X) when S / K is finite.

Equations

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

theorem BGS.HasseWeil.ratFuncConstantLocalizationRingEquiv_algebraMap (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] (r : RatFunc K) : (ratFuncConstantLocalizationRingEquiv K S) ((algebraMap (RatFunc K) (RatFuncConstantLocalization K S)) r) = (algebraMap (RatFunc K) (RatFunc S)) r

noncomputable def BGS.HasseWeil.ratFuncConstantLocalizationLinearEquiv (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : RatFuncConstantLocalization K S ≃ₗ[RatFunc K] RatFunc S

The localization equivalence, now linear over the canonical coefficient embedding K(X) → S(X).

Equations

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

theorem BGS.HasseWeil.ratFuncCoefficient_moduleFinite (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : Module.Finite (RatFunc K) (RatFunc S)

A finite coefficient extension induces a finite extension of rational function fields.

theorem BGS.HasseWeil.ratFuncCoefficient_finrank (K : Type u_1) (S : Type u_2) [Field K] [Field S] [Algebra K S] [FiniteDimensional K S] : Module.finrank (RatFunc K) (RatFunc S) = Module.finrank K S

Constant extension preserves the extension degree of rational function fields: [S(X) : K(X)] = [S : K].