Splitting multiplicity in an exact extension of constants

This file proves the finite-place multiplicity in the standard splitting law for an exact extension of constants. The proof does not assume the splitting law: it proves that inertia is trivial by restricting an inertia element to the embedded enlarged constant field, computes the relative residue degree from the already established absolute degree formula, and applies the Galois fiber identity.

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingBaseConstantAlgebra (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 place splitting multiplicity construction.

Equations

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingBasePolynomialAlgebra (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 place splitting multiplicity construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingTargetPolynomialAlgebra (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 place splitting multiplicity construction.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_ramificationIdx_eq_one (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 = ⊥) [Finite C] (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : finitePlaceRelativeRamificationIdx C N (ExactConstantExtension C N S) Q = 1

Every finite place is unramified in an exact extension of constants.

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_fiber_card_eq_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 (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 = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : Fintype.card (FinitePlaceUnderFiber C N (ExactConstantExtension C N S) (exactConstantExtensionDownstairsFinitePlace C S N hExact q)) = (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inl (exactConstantExtensionDownstairsFinitePlace C S N hExact q)))

A downstairs finite place of degree d has exactly gcd([S : C], d) finite places above it in the exact extension of constants.

The chosen explicit normalization prime supplies one point of the fiber; the cardinality is that of the entire actual restriction fiber, not merely a cardinality of a selected presentation.

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedFinitePlaceEquiv (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 = ⊥) : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S)) ≃ CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)

The explicit S[X]-normalization presentation exhausts the actual finite places of the constant extension, viewed over the original constant field C.

Equations

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

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionPresentedFinitePlaceEquiv_apply (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))) : (exactConstantExtensionPresentedFinitePlaceEquiv C S N hExact) q = exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedFinitePlaceFiberEquiv (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 = ⊥) (P : CorvajaZannier.FiniteExtensionFinitePlace C N) : { q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S)) // exactConstantExtensionDownstairsFinitePlace C S N hExact q = P } ≃ FinitePlaceUnderFiber C N (ExactConstantExtension C N S) P

Restricting the global presentation equivalence to a fixed downstairs place identifies the presented contraction fiber with the entire actual place-restriction fiber.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionPresentedFinitePlaceFiber_natCard_eq_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 (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 = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : Nat.card { q' : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S)) // exactConstantExtensionDownstairsFinitePlace C S N hExact q' = exactConstantExtensionDownstairsFinitePlace C S N hExact q } = (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inl (exactConstantExtensionDownstairsFinitePlace C S N hExact q)))

The presented finite contraction fiber itself has the standard gcd cardinality. This is the presentation-level exhaustiveness form of the constant-extension splitting law.

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingInfinityBaseConstantAlgebra (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] : Algebra C ↥(CorvajaZannier.RatFuncInfinityIntegers C)

The algebra structure from C to (RatFuncInfinityIntegers C) used in the constant extension place splitting multiplicity construction.

Equations

• BGS.HasseWeil.splittingInfinityBaseConstantAlgebra C = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom C).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingInfinityBaseRatFuncAlgebra (C : Type u_1) [Field C] [DecidableEq (RatFunc C)] : Algebra (↥(CorvajaZannier.RatFuncInfinityIntegers C)) (RatFunc C)

The algebra structure from (RatFuncInfinityIntegers C) to (RatFunc C) used in the constant extension place splitting multiplicity construction.

Equations

• BGS.HasseWeil.splittingInfinityBaseRatFuncAlgebra C = (SubringClass.subtype (RatFunc.inftyValuation C).integer).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingInfinityExactBaseAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] : Algebra (↥(CorvajaZannier.RatFuncInfinityIntegers C)) (ExactConstantExtension C N S)

The algebra from the infinity valuation ring to the exact constant extension, using its chosen field and rational function structures.

Equations

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

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

The enlarged constants map into the infinity normalization over the original constant field.

Equations

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

@[reducible]

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

The enlarged-constant algebra structure on the infinity normalization.

Equations

• BGS.HasseWeil.exactConstantExtensionInfinityIntegralClosureConstantAlgebra C S N hExact = (BGS.HasseWeil.exactConstantExtensionConstantToInfinityIntegralClosureRingHom C S N hExact).toAlgebra