The finite different after exact constant extension

This file supplies the field-theoretic input for transporting the finite different through an exact finite constant extension. Inside ExactConstantExtension C N S, the copies of S(X) and N generate the whole tensor field and are linearly disjoint over C(X). The proof uses the explicit tensor generation and the extension-degree formulas already proved for rational-function and exact constant extensions.

@[reducible]

noncomputable def BGS.HasseWeil.finiteDifferentCanonicalRatFuncPolynomialAlgebra (K : Type u_1) [Field K] : Algebra (Polynomial K) (RatFunc K)

The canonical polynomial algebra structure on the rational function field.

Equations

• BGS.HasseWeil.finiteDifferentCanonicalRatFuncPolynomialAlgebra K = inferInstance

theorem BGS.HasseWeil.finiteDifferentCanonicalRatFuncPolynomialFractionRing (K : Type u_1) [Field K] : IsFractionRing (Polynomial K) (RatFunc K)

The rational function field is the fraction field of its canonical polynomial algebra.

theorem BGS.HasseWeil.different_eq_map_of_linearlyDisjoint_fieldRanges (A : Type u_1) (R₁ : Type u_2) (R₂ : Type u_3) (B : Type u_4) (K : Type u_5) (K₁ : Type u_6) (K₂ : Type u_7) (L : Type u_8) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [CommRing R₁] [IsDedekindDomain R₁] [CommRing R₂] [IsDedekindDomain R₂] [CommRing B] [IsDedekindDomain B] [Field K] [Field K₁] [Field K₂] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K K₁] [Algebra K K₂] [Algebra K L] [Algebra K₁ L] [Algebra K₂ L] [Algebra A K₂] [IsScalarTower K K₁ L] [IsScalarTower K K₂ L] [IsScalarTower A K K₂] [Algebra A R₁] [Algebra A R₂] [Algebra A B] [Algebra A L] [Algebra R₁ K₁] [IsFractionRing R₁ K₁] [Algebra R₂ K₂] [IsFractionRing R₂ K₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [Algebra B L] [IsScalarTower A K L] [IsScalarTower A K₂ L] [IsScalarTower R₁ K₁ L] [IsScalarTower R₂ K₂ L] [IsScalarTower A R₂ K₂] [IsScalarTower A R₁ L] [IsScalarTower A R₂ L] [IsScalarTower A R₁ B] [IsScalarTower A R₂ B] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [IsScalarTower A B L] [FiniteDimensional K K₂] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Module.Finite A R₁] [Module.Finite A R₂] [Module.Free A R₂] [Module.IsTorsionFree A R₁] [Module.IsTorsionFree A R₂] [Module.IsTorsionFree R₂ L] [Module.IsTorsionFree R₁ B] [IsIntegralClosure R₂ A K₂] [IsIntegralClosure B R₁ L] (hdisjoint : (IsScalarTower.toAlgHom K K₁ L).fieldRange.LinearDisjoint ↥(IsScalarTower.toAlgHom K K₂ L).fieldRange) (hsup : (IsScalarTower.toAlgHom K K₁ L).fieldRange ⊔ (IsScalarTower.toAlgHom K K₂ L).fieldRange = ⊤) (hcoprime : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) : differentIdeal R₁ B = Ideal.map (algebraMap R₂ B) (differentIdeal A R₂)

Base change preserves the relative different when the fraction-field images are linearly disjoint, generate the ambient field, and the original differents are coprime.

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteDifferentBaseConstantAlgebra (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 exact constant extension finite different construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteDifferentBasePolynomialAlgebra (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 exact constant extension finite different construction.

Equations

• BGS.HasseWeil.finiteDifferentBasePolynomialAlgebra C N = BGS.HasseWeil.ratFuncInducedPolynomialAlgebra C N

theorem BGS.HasseWeil.finiteDifferentBaseConstantPolynomialTower (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.finiteDifferentCoefficientPolynomialAlgebra (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 exact constant extension finite different construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteDifferentTargetPolynomialAlgebra (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 exact constant extension finite different construction.

Equations

• BGS.HasseWeil.finiteDifferentTargetPolynomialAlgebra C S N = BGS.HasseWeil.constantExtensionTensorPolynomialAlgebra C S N

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteDifferentTensorNormalizationPolynomialAlgebra (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) (TensorProduct C S ↥(integralClosure (Polynomial C) N))

The algebra structure from S[X] to (S ⊗[C] integralClosure C[X] N) used in the exact constant extension finite different construction.

Equations

• BGS.HasseWeil.finiteDifferentTensorNormalizationPolynomialAlgebra C S N = BGS.HasseWeil.constantExtensionNormalizationTensorPolynomialAlgebra C S N

@[reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionFiniteNormalizationAlgebra (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] [Fintype C] [Finite S] : Algebra ↥(integralClosure (Polynomial C) N) ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))

The original finite normalization acts on the finite normalization after constant extension through the right tensor factor and the canonical normalization equivalence.

Equations

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

theorem BGS.HasseWeil.exactConstantExtension_rationalFunctionRanges_linearDisjoint (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : let L := ExactConstantExtension C N S; have f₁ := IsScalarTower.toAlgHom (RatFunc C) (RatFunc S) L; have f₂ := IsScalarTower.toAlgHom (RatFunc C) N L; have F₁ := f₁.fieldRange; let F₂ := f₂.fieldRange; F₁.LinearDisjoint ↥F₂ ∧ F₁ ⊔ F₂ = ⊤

In an exact constant extension, the embedded copies of S(X) and N are linearly disjoint over C(X) and generate the whole tensor field.

theorem BGS.HasseWeil.exactConstantExtension_finiteDifferent_eq_map (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Fintype C] [Finite S] : let L := ExactConstantExtension C N S; let R₂ := integralClosure (Polynomial C) N; let B := integralClosure (Polynomial S) L; let this := exactConstantExtensionField C N S hExact; let this_1 := constantExtensionTensorPolynomialAlgebra C S N; let this_2 := this_1.toSMul; let this_3 := Algebra.toModule; let this_4 := ratFuncExactConstantExtensionAlgebra C S N hExact; let this_5 := this_4.toSMul; let this_6 := Algebra.toModule; let this_7 := finiteDifferentCanonicalRatFuncPolynomialAlgebra S; have this_8 := ⋯; have this_9 := ⋯; have this_10 := ⋯; have this_11 := ⋯; have this_12 := ⋯; have this := ⋯; have this_13 := ⋯; let this_14 := finiteDifferentCanonicalRatFuncPolynomialAlgebra C; have this_15 := ⋯; have this_16 := ⋯; have this_17 := ⋯; have this_18 := ⋯; have this_19 := ⋯; have this_20 := exactConstantExtensionFiniteNormalizationAlgebra C S N; differentIdeal (Polynomial S) ↥B = Ideal.map (algebraMap ↥R₂ ↥B) (differentIdeal (Polynomial C) ↥R₂)

In an exact finite constant extension, the different of the extended finite normalization is the extension of the original finite different. The map on ideals is the right-factor map supplied by exactConstantExtensionFiniteNormalizationAlgebra.