Finite places in an exact constant extension

Let N / C(X) be finite separable with exact constant field C, and let S / C be finite Galois. This file connects maximal ideals in the explicit normalization of S ⊗[C] N to the project's finite-place types over S and C. It proves that the upstairs residue field is finite, packages the downstairs contraction as an actual finite place of N, and expresses the constant-extension residue formula as

deg_S(Q) = deg_C(P) / gcd([S : C], deg_C(P)).

No maximality or residue-finiteness hypothesis is left to downstream users.

@[instance_reducible]

noncomputable def BGS.HasseWeil.bridgeBaseConstantAlgebra (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 constant extension finite place bridge construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.bridgeBasePolynomialAlgebra (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 constant extension finite place bridge construction.

Equations

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

theorem BGS.HasseWeil.bridgeBaseConstantPolynomialTower (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.bridgeTargetPolynomialAlgebra (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 constant extension finite place bridge construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.bridgeTensorNormalizationPolynomialAlgebra (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 constant extension finite place bridge construction.

Equations

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

@[instance_reducible]

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

The algebra structure from S to (integralClosure S[X] (ExactConstantExtension C N S)) used in the constant extension finite place bridge construction.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionTensorNormalizationHeightOne (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [Algebra C S] (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))

Pull an ideal in the explicit base-changed normalization back to the constant tensor of the original normalization.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionUpstairsFinitePlace (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : CorvajaZannier.FiniteExtensionFinitePlace S (ExactConstantExtension C N S)

Package a height-one ideal of the explicit normalization as an actual finite place over S.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionUpstairsResidueField_finite (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [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 = ⊥) [Finite C] (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : Finite q.asIdeal.ResidueField

The residue field of an upstairs height-one ideal is finite.

theorem BGS.HasseWeil.exactConstantExtensionUpstairsIdeal_isMaximal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [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 = ⊥) [Finite C] (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : q.asIdeal.IsMaximal

Every upstairs height-one ideal is maximal.

noncomputable def BGS.HasseWeil.exactConstantExtensionDownstairsFinitePlace (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [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 = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : CorvajaZannier.FiniteExtensionFinitePlace C N

Package the downstairs contraction as an actual finite place of N/C(X).

Equations

• BGS.HasseWeil.exactConstantExtensionDownstairsFinitePlace C S N hExact q = id { asIdeal := BGS.HasseWeil.finiteFieldConstantExtensionDownstairsIdeal C S N q.asIdeal, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionDownstairsFinitePlace_asIdeal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [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 = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : (exactConstantExtensionDownstairsFinitePlace C S N hExact q).asIdeal = finiteFieldConstantExtensionDownstairsIdeal C S N q.asIdeal

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_degree_eq_div_gcd (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq S] [DecidableEq (RatFunc C)] [DecidableEq (RatFunc S)] [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 = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (Sum.inl (exactConstantExtensionUpstairsFinitePlace C S N hExact q)) = CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inl (exactConstantExtensionDownstairsFinitePlace C S N hExact q)) / (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inl (exactConstantExtensionDownstairsFinitePlace C S N hExact q)))

Constant extension changes the degree of an actual finite place by the standard division-by-gcd formula.