Total different degree under exact constant extension

This file separates the global weighted-degree cancellation from the local normalization compatibility needed for invariance of the different under an exact extension of finite constants.

The theorem below assumes only pointwise equality of the total-different multiplicity on a presented upstairs place and its contracted downstairs place. The exhaustive presented-place equivalence, the division-by-gcd degree formula, and the matching gcd fiber cardinality then prove equality of the total finite-plus-infinity different degrees. The remaining pointwise hypothesis is intended to be discharged branchwise by the finite and reciprocal-infinity different-map theorems.

@[instance_reducible]

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

Classical equality on the enlarged constants for the total different-degree calculation.

Equations

• BGS.HasseWeil.exactConstantTotalDifferentConstantsDecidableEq K = BGS.HasseWeil.infinityBridgeDecidableEqConstants K

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.exactConstantTotalDifferentRatFuncDecidableEq K = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants K

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantTotalDifferentBaseConstantAlgebra (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 total different degree construction.

Equations

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

theorem BGS.HasseWeil.exactConstantTotalDifferentBaseConstantTower (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.exactConstantTotalDifferentBasePolynomialAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra (Polynomial C) N

The polynomial algebra on the base extension field used to compare different degrees.

Equations

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

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

theorem BGS.HasseWeil.exactConstantExtension_totalDifferentDegree_eq_of_presentedMultiplicity (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 = ⊥) : let E := ExactConstantExtension C N S; (∀ (q : ExactConstantExtensionPresentedPlace C S N), (finiteExtensionTotalDifferentEffectiveDivisor S E) ((exactConstantExtensionPresentedUpstairsPlaceEquiv C S N hExact) q) = (finiteExtensionTotalDifferentEffectiveDivisor C N) (exactConstantExtensionPresentedDownstairsPlace C S N hExact q)) → CorvajaZannier.finiteExtensionFiniteDifferentDegree S E ⋯ + CorvajaZannier.infinityDifferentDegree S E = CorvajaZannier.finiteExtensionFiniteDifferentDegree C N ⋯ + CorvajaZannier.infinityDifferentDegree C N

If the total-different multiplicity is preserved at every presented place, then an exact extension of finite constants preserves the total finite-plus-infinity different degree.