The different of a finite coefficient extension at infinity

For a finite Galois extension S / C, the infinity valuation ring over S is the localization of the reciprocal polynomial ring S[X] at the image of the reciprocal-origin complement from C[X]. The key denominator argument uses the product of all Galois conjugates of a polynomial.

This localization description transports finiteness and formal unramifiedness from C[X] → S[X]. Consequently the local different of the coefficient extension at infinity is the unit ideal.

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqC (C : Type u_1) : DecidableEq C

Decidable equality on C used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqC C = Classical.decEq C

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqS (S : Type u_2) : DecidableEq S

Decidable equality on S used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqS S = Classical.decEq S

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqRatFuncC (C : Type u_1) [Field C] : DecidableEq (RatFunc C)

Decidable equality on (RatFunc C) used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqRatFuncC C = Classical.decEq (RatFunc C)

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqRatFuncS (S : Type u_2) [Field S] : DecidableEq (RatFunc S)

Decidable equality on (RatFunc S) used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentDecidableEqRatFuncS S = Classical.decEq (RatFunc S)

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientPolynomialAlgebra (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 finite field infinity different construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentReciprocalPolynomialAlgebra (S : Type u_2) [Field S] : Algebra (Polynomial S) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

The algebra structure from S[X] to (RatFuncInfinityIntegers S) used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentReciprocalPolynomialAlgebra S = BGS.HasseWeil.ratFuncInfinityReciprocalPolynomialAlgebra S

theorem BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientOriginPrime (C : Type u_1) [Field C] : (Ideal.span {Polynomial.X}).IsPrime

theorem BGS.HasseWeil.finiteFieldInfinityDifferentExtensionOriginPrime (S : Type u_2) [Field S] : (Ideal.span {Polynomial.X}).IsPrime

theorem BGS.HasseWeil.ratFuncInfinityIntegers_isLocalization_coefficientPrimeCompl (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] : IsLocalization (Algebra.algebraMapSubmonoid (Polynomial S) (Ideal.span {Polynomial.X}).primeCompl) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

The infinity valuation ring over S is already obtained by localizing S[X] at the image of the reciprocal-origin complement from C[X].

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentBaseReciprocalPolynomialAlgebra (C : Type u_1) [Field C] : Algebra (Polynomial C) ↥(CorvajaZannier.RatFuncInfinityIntegers C)

The algebra structure from C[X] to (RatFuncInfinityIntegers C) used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentBaseReciprocalPolynomialAlgebra C = BGS.HasseWeil.ratFuncInfinityReciprocalPolynomialAlgebra C

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientAlgebra (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Algebra ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

The algebra structure from (RatFuncInfinityIntegers C) to (RatFuncInfinityIntegers S) used in the finite field infinity different construction.

Equations

• BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientAlgebra C S = (BGS.HasseWeil.ratFuncInfinityIntegersRingHom C S).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteFieldInfinityDifferentBasePolynomialExtensionAlgebra (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Algebra (Polynomial C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

The base polynomial algebra on the finite extension used for the infinity different.

Equations

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

theorem BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientPolynomialTower (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : IsScalarTower (Polynomial C) (Polynomial S) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

theorem BGS.HasseWeil.finiteFieldInfinityDifferentBasePolynomialCoefficientTower (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : IsScalarTower (Polynomial C) ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

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

theorem BGS.HasseWeil.ratFuncInfinityIntegers_coefficient_moduleFinite (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

The coefficient extension of infinity valuation rings is finite.

theorem BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientModuleFinite (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

theorem BGS.HasseWeil.finiteFieldInfinityDifferentCoefficientIsTorsionFree (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

theorem BGS.HasseWeil.ratFuncInfinityIntegers_coefficient_formallyUnramified (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] : Algebra.FormallyUnramified ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S)

The coefficient extension of infinity valuation rings is formally unramified.

theorem BGS.HasseWeil.ratFuncInfinityIntegers_coefficient_differentIdeal_eq_top (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] : differentIdeal ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegers S) = ⊤

A finite Galois coefficient extension has unit different at the infinity valuation ring.