Local different coefficients under exact constant extension

The finite and reciprocal-infinity different ideals commute with exact extension of finite constants. Since every place in a constant extension has ramification index one, their multiplicities agree place by place. This discharges the local hypothesis of the global different-degree and genus transport theorems.

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantDifferentCoefficientConstantsDecidableEq (K : Type u_4) : DecidableEq K

Classical equality on the enlarged constant field for the different-coefficient calculation.

Equations

• BGS.HasseWeil.exactConstantDifferentCoefficientConstantsDecidableEq K = BGS.HasseWeil.infinityBridgeDecidableEqConstants K

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantDifferentCoefficientRatFuncDecidableEq (K : Type u_4) [Field K] : DecidableEq (RatFunc K)

Classical equality on rational functions over the enlarged constants for the different coefficient.

Equations

• BGS.HasseWeil.exactConstantDifferentCoefficientRatFuncDecidableEq K = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants K

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantDifferentCoefficientBaseConstantAlgebra (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 different coefficient construction.

Equations

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

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

theorem BGS.HasseWeil.exactConstantExtensionPresentedFinitePlace_ramificationIdx_eq_one (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))) : let E := ExactConstantExtension C N S; let R2 := CorvajaZannier.RatFuncFiniteIntegralClosure C N; have B := integralClosure (Polynomial S) E; q.asIdeal.ramificationIdx ↥R2 = 1

A prime in the explicit S[X]-normalization is unramified over its contracted prime in the original C[X]-normalization. The proof transports the prime to the canonical C[X]-normalization used by the place tower and then invokes unramifiedness of exact constant extensions.

theorem BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlace_ramificationIdx_eq_one (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 : ExactConstantExtensionPresentedInfinityPlace C S N) : let E := ExactConstantExtension C N S; let R2 := CorvajaZannier.RatFuncInfinityIntegralClosure C N; have B := CorvajaZannier.RatFuncInfinityIntegralClosure S E; (↑(exactConstantExtensionUpstairsInfinityPlace C S N hExact ↑q ⋯)).ramificationIdx ↥R2 = 1

Every prime in the explicit extended infinity normalization is unramified over the original infinity normalization.

theorem BGS.HasseWeil.exactConstantExtension_presented_totalDifferentMultiplicity_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] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : ExactConstantExtensionPresentedPlace C S N) : let E := ExactConstantExtension C N S; let this := exactConstantExtensionField C N S hExact; let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S; have this_2 := this_1.toSMul; let this_3 := Algebra.toModule; have this_4 := ⋯; have this_5 := ⋯; let this_6 := ratFuncExactConstantExtensionAlgebra C S N hExact; let this_7 := this_6.toSMul; let this_8 := Algebra.toModule; let this_9 := constantExtensionTensorPolynomialAlgebra C S N; let this_10 := this_9.toSMul; have this_11 := Algebra.toModule; have this_12 := ⋯; have this_13 := ⋯; have this_14 := ⋯; (finiteExtensionTotalDifferentEffectiveDivisor S E) ((exactConstantExtensionPresentedUpstairsPlaceEquiv C S N hExact) q) = (finiteExtensionTotalDifferentEffectiveDivisor C N) (exactConstantExtensionPresentedDownstairsPlace C S N hExact q)

Exact constant extension preserves the total-different coefficient at every presented finite or infinity place.

theorem BGS.HasseWeil.exactConstantExtension_genus_eq (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] [Finite C] (hExact : algebraicClosure C N = ⊥) : let E := ExactConstantExtension C N S; MarkoffRiemannRoch.FunctionField.genus S E = MarkoffRiemannRoch.FunctionField.genus C N

Exact finite extension of the full constant field preserves intrinsic function-field genus.