The different of a separable coefficient extension

Let S / C be a finite separable extension of fields. For the coefficientwise algebra structure on S[X] over C[X], the different ideal is the unit ideal.

The proof first identifies S[X] with the polynomial base change C[X] ⊗[C] S. Formal unramifiedness therefore follows from separability of S / C. After localizing both polynomial rings, the induced extension of rational function fields is finite and formally unramified, hence separable. The local characterization of the Dedekind different then excludes every maximal ideal from the support of the different.

The final corollary specializes this to arbitrary extensions of finite fields; their finiteness and separability are supplied by typeclass inference.

@[instance_reducible]

noncomputable def BGS.HasseWeil.differentCoefficientPolynomialAlgebra (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 polynomial different construction.

Equations

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

theorem BGS.HasseWeil.differentCoefficientPolynomialTower (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : IsScalarTower C (Polynomial C) (Polynomial S)

theorem BGS.HasseWeil.differentConstantPolynomialTower (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : IsScalarTower C S (Polynomial S)

theorem BGS.HasseWeil.differentCoefficientPolynomialModuleFinite (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.differentCoefficientPolynomialFormallyUnramified (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [Algebra.IsSeparable C S] : Algebra.FormallyUnramified (Polynomial C) (Polynomial S)

theorem BGS.HasseWeil.differentCoefficientRationalFunctionAlgebraic (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [Algebra.IsSeparable C S] : Algebra.IsAlgebraic (FractionRing (Polynomial C)) (FractionRing (Polynomial S))

theorem BGS.HasseWeil.differentCoefficientPolynomialIntegralClosure (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [Algebra.IsSeparable C S] : IsIntegralClosure (Polynomial S) (Polynomial C) (FractionRing (Polynomial S))

theorem BGS.HasseWeil.differentCoefficientRationalFunctionLocalization (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [Algebra.IsSeparable C S] : IsLocalization (Algebra.algebraMapSubmonoid (Polynomial S) (nonZeroDivisors (Polynomial C))) (FractionRing (Polynomial S))

theorem BGS.HasseWeil.differentCoefficientRationalFunctionFiniteDimensional (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [Algebra.IsSeparable C S] : FiniteDimensional (FractionRing (Polynomial C)) (FractionRing (Polynomial S))

theorem BGS.HasseWeil.differentCoefficientRationalFunctionFormallyUnramified (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [Algebra.IsSeparable C S] : Algebra.FormallyUnramified (FractionRing (Polynomial C)) (FractionRing (Polynomial S))

theorem BGS.HasseWeil.differentCoefficientRationalFunctionSeparable (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [Algebra.IsSeparable C S] : Algebra.IsSeparable (FractionRing (Polynomial C)) (FractionRing (Polynomial S))

theorem BGS.HasseWeil.coefficientPolynomial_formallyUnramified (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [Algebra.IsSeparable C S] : Algebra.FormallyUnramified (Polynomial C) (Polynomial S)

A finite separable extension of coefficient fields induces a formally unramified extension of polynomial rings.

theorem BGS.HasseWeil.coefficientRationalFunction_isSeparable (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [Algebra.IsSeparable C S] : Algebra.IsSeparable (FractionRing (Polynomial C)) (FractionRing (Polynomial S))

A finite separable extension of coefficient fields induces a separable extension of the corresponding rational function fields.

theorem BGS.HasseWeil.coefficientPolynomial_differentIdeal_eq_top (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] [FiniteDimensional C S] [Algebra.IsSeparable C S] : differentIdeal (Polynomial C) (Polynomial S) = ⊤

For a finite separable coefficient-field extension, the different of the coefficientwise polynomial-ring extension is the unit ideal.

theorem BGS.HasseWeil.finiteFieldPolynomial_differentIdeal_eq_top (k : Type u_3) (F : Type u_4) [Field k] [Finite k] [Field F] [Finite F] [Algebra k F] : differentIdeal (Polynomial k) (Polynomial F) = ⊤

In particular, every extension of finite fields has unit different after coefficientwise extension of polynomial rings.