Finite places of an exact constant extension

This file embeds the enlarged constant field into the finite normalization over the original polynomial ring. The canonical constant quotient is compatible with the resulting Galois action. Consequently, at every finite place whose residue field has degree one over the enlarged constants, the kernel of constant restriction on the decomposition group is exactly inertia.

noncomputable def BGS.HasseWeil.exactConstantExtensionConstantToFiniteIntegralClosureRingHom (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra (RatFunc C) N] [IsScalarTower C (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : S →+* ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (ExactConstantExtension C N S))

The enlarged constants map into the finite normalization.

Equations

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

@[reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionFiniteIntegralClosureConstantAlgebra (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra (RatFunc C) N] [IsScalarTower C (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : Algebra S ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (ExactConstantExtension C N S))

The S-algebra structure on the finite normalization induced by the embedded enlarged constants.

Equations

• BGS.HasseWeil.exactConstantExtensionFiniteIntegralClosureConstantAlgebra C N S hExact = (BGS.HasseWeil.exactConstantExtensionConstantToFiniteIntegralClosureRingHom C N S hExact).toAlgebra

theorem BGS.HasseWeil.exactConstantExtensionFiniteIntegralClosure_algebraMap_val (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra (RatFunc C) N] [IsScalarTower C (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (s : S) : ↑((algebraMap S ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (ExactConstantExtension C N S))) s) = Algebra.TensorProduct.includeLeft s

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_action_on_finiteNormalization (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra (RatFunc C) N] [IsScalarTower C (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra C L] [Algebra L N] [IsScalarTower C L N] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (g : ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S) (s : S) : g • (algebraMap S ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (ExactConstantExtension C N S))) s = (algebraMap S ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (ExactConstantExtension C N S))) (((exactConstantExtensionConstantQuotient C L N S hExact) g) s)

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_stabilizerRestriction_ker_eq_inertia (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra (RatFunc C) N] [IsScalarTower C (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra C L] [Algebra L N] [IsScalarTower C L N] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : Module.finrank S Q.asIdeal.ResidueField = 1 → ((exactConstantExtensionConstantQuotient C L N S hExact).comp (MulAction.stabilizer (ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S) Q.asIdeal).subtype).ker = Ideal.inertia (↥(MulAction.stabilizer (ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S) Q.asIdeal)) Q.asIdeal

On a residue-degree-one finite place, the kernel of constant restriction on the decomposition group is inertia.

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_decompositionGroup_card (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra (RatFunc C) N] [IsScalarTower C (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra C L] [Algebra L N] [IsScalarTower C L N] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] [Finite C] [DecidableEq C] [DecidableEq (RatFunc C)] (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : Module.finrank S Q.asIdeal.ResidueField = 1 → CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q) = Module.finrank C S → CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl (finitePlaceUnder C L (ExactConstantExtension C N S) Q)) = 1 → 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)

The decomposition-group cardinality required by Frobenius-coset averaging, specialized to the exact constant extension.