Compatibility of the two finite-place models in a constant extension

The explicit constant-extension normalization is naturally a normalization over S[X], whereas the relative Galois action is implemented on the normalization over C[X]. This file identifies the corresponding finite places and their residue fields. In particular, an S-rational place has absolute C-degree [S : C], in precisely the model used by the decomposition-group theorem.

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibilityBaseConstantAlgebra (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 place compatibility construction.

Equations

• BGS.HasseWeil.compatibilityBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibilityBasePolynomialAlgebra (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 place compatibility construction.

Equations

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

theorem BGS.HasseWeil.compatibilityBaseConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

theorem BGS.HasseWeil.compatibilityBaseConstantPolynomialTower (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.compatibilityPolynomialCoefficientAlgebra (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 place compatibility construction.

Equations

• BGS.HasseWeil.compatibilityPolynomialCoefficientAlgebra C S = (Polynomial.mapRingHom (algebraMap C S)).toAlgebra

@[instance_reducible]

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

The algebra structure from (RatFunc C) to (RatFunc S) used in the exact constant extension finite place compatibility construction.

Equations

• BGS.HasseWeil.compatibilityRatFuncCoefficientAlgebra C S = BGS.HasseWeil.ratFuncCoefficientAlgebra C S

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibilityTargetPolynomialAlgebra (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 place compatibility construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibilityTensorNormalizationPolynomialAlgebra (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 place compatibility construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibilityOldNormalizationConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C ↥(integralClosure (Polynomial C) N)

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

Equations

• BGS.HasseWeil.compatibilityOldNormalizationConstantAlgebra C N = ((algebraMap (Polynomial C) ↥(integralClosure (Polynomial C) N)).comp (algebraMap C (Polynomial C))).toAlgebra

theorem BGS.HasseWeil.finiteDimensional_exactConstantExtension_over_baseRatFunc (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 C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : FiniteDimensional (RatFunc C) (ExactConstantExtension C N S)

The exact constant extension is finite over the original rational function field. This is the finite-dimensional input needed to compare its C[X]- and S[X]-normalizations.

theorem BGS.HasseWeil.exactConstantExtension_ratFunc_polynomialCompatibility (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] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (p : Polynomial C) : (algebraMap (RatFunc C) (ExactConstantExtension C N S)) ((algebraMap (Polynomial C) (RatFunc C)) p) = (algebraMap (RatFunc S) (ExactConstantExtension C N S)) ((algebraMap (Polynomial S) (RatFunc S)) ((algebraMap (Polynomial C) (Polynomial S)) p))

Polynomial coefficient extension is compatible with the two canonical rational-function embeddings into the exact constant extension.

noncomputable def BGS.HasseWeil.exactConstantExtensionCompatibleBaseFinitePlace (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 C (ExactConstantExtension C N S)

The finite place over C corresponding to a place in the explicit S[X]-normalization. Extending its constants back to S recovers the finite place constructed in ConstantExtensionFinitePlaceBridge.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionCompatibleBaseFinitePlace_baseChange (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))) : (IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (ratFuncFiniteIntegralClosureRingEquiv C S (ExactConstantExtension C N S) ⋯)) (exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q) = exactConstantExtensionUpstairsFinitePlace C S N hExact q

noncomputable def BGS.HasseWeil.exactConstantExtensionFiniteClosureBaseChangeAlgEquiv (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] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (ExactConstantExtension C N S)) ≃ₐ[S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S (ExactConstantExtension C N S))

The identity equivalence between the C[X]- and S[X]-normalizations is linear over the enlarged constant field.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionUpstairsFinitePlace_eq_compatibleNormalizationTransport (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))) : have e := integralClosureAlgEquivRatFuncFiniteOfAlgebraMap S (ExactConstantExtension C N S) (constantExtensionTensorPolynomialAlgebra C S N) ⋯; exactConstantExtensionUpstairsFinitePlace C S N hExact q = (heightOneSpectrumEquivOfAlgEquiv e) q

The actual upstairs finite place is exactly the transport of the presented prime along the equality bridge from the compatible polynomial normalization to the canonical rational-function normalization.

noncomputable def BGS.HasseWeil.exactConstantExtensionCompatibleResidueFieldAlgEquiv (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))) : (exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q).asIdeal.ResidueField ≃ₐ[S] (exactConstantExtensionUpstairsFinitePlace C S N hExact q).asIdeal.ResidueField

Corresponding finite places have equivalent residue fields as S-algebras, even though the source place is represented in the C[X]-normalization.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionCompatibleResidueField_finrank_eq (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))) : Module.finrank S (exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q).asIdeal.ResidueField = Module.finrank S (exactConstantExtensionUpstairsFinitePlace C S N hExact q).asIdeal.ResidueField

The two representations of the upstairs place have the same residue degree over the enlarged constants.

theorem BGS.HasseWeil.exactConstantExtensionCompatibleBaseFinitePlace_degree_eq (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)) = 1 → CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl (exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q)) = Module.finrank C S

An S-rational place in the explicit normalization has absolute C-degree [S : C] in the finite-place model used by the Galois action.

theorem BGS.HasseWeil.exactConstantExtensionCompatibleBaseFinitePlace_under_original (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))) : finitePlaceUnder C N (ExactConstantExtension C N S) (exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q) = exactConstantExtensionDownstairsFinitePlace C S N hExact q

Restricting the compatible C[X]-place to the original function field recovers the downstairs place obtained by contracting the explicit constant extension ideal.

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibilityIntermediateConstantAlgebra (C : Type u_1) [Field C] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] : Algebra C L

The algebra structure from C to L used in the exact constant extension finite place compatibility construction.

Equations

• BGS.HasseWeil.compatibilityIntermediateConstantAlgebra C L = ((algebraMap (RatFunc C) L).comp (algebraMap C (RatFunc C))).toAlgebra

theorem BGS.HasseWeil.compatibilityConstantIntermediateTopTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] : IsScalarTower C L N

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_decompositionGroup_card_of_rational_base (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 (RatFunc C)] [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 = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) (hBase : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl (finitePlaceUnder C L N (exactConstantExtensionDownstairsFinitePlace C S N hExact q))) = 1) (hDegreeDiv : Module.finrank L N ∣ Module.finrank C S) : have Q := exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q; Nat.card ↥(finitePlaceDecompositionGroup C L (ExactConstantExtension C N S) Q) = Nat.card ↥((exactConstantExtensionConstantQuotient C L N S hExact).comp (finitePlaceDecompositionGroup C L (ExactConstantExtension C N S) Q).subtype).ker * Nat.card Gal(S/C)

For an actual finite place in the constant-extended normalization, a rational restriction to L and divisibility [N : L] ∣ [S : C] imply the decomposition-group cardinality identity. The residue-degree-one, absolute top-degree, and rational-base hypotheses of the generic theorem are all derived internally.