The infinity different after exact constant extension #
For an exact finite extension of constants, the old infinity normalization maps into the new infinity normalization through the canonical embedding of the original function field. The two rational-function subfields remain linearly disjoint, while the coefficient extension of infinity valuation rings has unit different. The linear-disjoint different theorem therefore identifies the new infinity different with the extension of the old one.
@[instance_reducible]
noncomputable def
BGS.HasseWeil.exactConstantExtensionInfinityDifferentBaseConstantAlgebra
(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 infinity
different construction.
Equations
Instances For
@[instance_reducible]
noncomputable def
BGS.HasseWeil.exactConstantExtensionInfinityDifferentDecidableEqBaseRatFunc
(C : Type u_1)
[Field C]
:
DecidableEq (RatFunc C)
Decidable equality on (RatFunc C) used in the exact constant extension infinity
different construction.
Equations
Instances For
@[instance_reducible]
noncomputable def
BGS.HasseWeil.exactConstantExtensionInfinityDifferentDecidableEqExtendedRatFunc
(S : Type u_2)
[Field S]
:
DecidableEq (RatFunc S)
Decidable equality on (RatFunc S) used in the exact constant extension infinity
different construction.
Equations
Instances For
noncomputable def
BGS.HasseWeil.exactConstantExtensionInfinityDifferentNormalizationRingHom
(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 = ⊥)
:
let L := ExactConstantExtension C N S;
let this := exactConstantExtensionField C N S hExact;
have this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this_2 := exactConstantExtensionAlgebra C N S;
have this_3 := ratFuncExactConstantExtensionAlgebra C S N hExact;
have this_4 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_5 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers S);
have this_6 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_7 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_8 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers S);
have this_9 := (ratFuncInfinityIntegersRingHom C S).toAlgebra;
↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N) →+* ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)
The ambient constant-extension embedding restricts to the infinity integral closures.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible]
noncomputable def
BGS.HasseWeil.exactConstantExtensionInfinityNormalizationAlgebra
(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 = ⊥)
:
let L := ExactConstantExtension C N S;
let this := exactConstantExtensionField C N S hExact;
have this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this_2 := exactConstantExtensionAlgebra C N S;
have this_3 := ratFuncExactConstantExtensionAlgebra C S N hExact;
have this_4 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_5 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers S);
have this_6 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_7 := (ratFuncInfinityIntegersRingHom C S).toAlgebra;
Algebra ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)
The original infinity normalization acts on the infinity normalization after exact constant extension through the canonical embedding of the original function field.
Equations
Instances For
theorem
BGS.HasseWeil.exactConstantExtensionInfinityNormalizationAlgebra_coe
(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 = ⊥)
(x :
let L := ExactConstantExtension C N S;
have this := exactConstantExtensionField C N S hExact;
have this := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this := exactConstantExtensionAlgebra C N S;
have this := ratFuncExactConstantExtensionAlgebra C S N hExact;
have this := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers S);
have this := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N))
:
let L := ExactConstantExtension C N S;
let this := exactConstantExtensionField C N S hExact;
have this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this_2 := exactConstantExtensionAlgebra C N S;
let this_3 := ratFuncExactConstantExtensionAlgebra C S N hExact;
have this_4 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_5 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers S);
have this_6 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
have this_7 := (ratFuncInfinityIntegersRingHom C S).toAlgebra;
have this_8 := exactConstantExtensionInfinityNormalizationAlgebra C S N hExact;
↑((algebraMap ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L))
x) = (algebraMap N L) ↑x
The infinity-normalization algebra map is the ambient embedding of the original function field into the exact constant extension.
noncomputable def
BGS.HasseWeil.exactConstantExtensionInfinityNormalizationBaseChangeRingEquiv
(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 = ⊥)
:
let L := ExactConstantExtension C N S;
let this := exactConstantExtensionField C N S hExact;
have this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this_2 := ratFuncExactConstantExtensionAlgebra C S N hExact;
↥(CorvajaZannier.RatFuncInfinityIntegralClosure C L) ≃+* ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)
Changing the infinity coefficient valuation ring from C to S does
not change the integral closure inside an exact constant extension. The
underlying ring equivalence is the identity on the ambient function field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
BGS.HasseWeil.exactConstantExtensionInfinityNormalizationBaseChangeRingEquiv_coe
(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 = ⊥)
(x :
let L := ExactConstantExtension C N S;
let this := exactConstantExtensionField C N S hExact;
have this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this_2 := ratFuncExactConstantExtensionAlgebra C S N hExact;
↥(CorvajaZannier.RatFuncInfinityIntegralClosure C L))
:
let L := ExactConstantExtension C N S;
have this := exactConstantExtensionField C N S hExact;
have this := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this := ratFuncExactConstantExtensionAlgebra C S N hExact;
↑((exactConstantExtensionInfinityNormalizationBaseChangeRingEquiv C S N hExact) x) = ↑x
The infinity-normalization base-change equivalence preserves the ambient function-field element.
theorem
BGS.HasseWeil.exactConstantExtension_infinityDifferent_eq_map
(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 = ⊥)
:
let L := ExactConstantExtension C N S;
let A := CorvajaZannier.RatFuncInfinityIntegers C;
let R₁ := CorvajaZannier.RatFuncInfinityIntegers S;
let this := exactConstantExtensionField C N S hExact;
have this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
have this_2 := exactConstantExtensionAlgebra C N S;
let this_3 := ratFuncExactConstantExtensionAlgebra C S N hExact;
let this_4 := this_3.toSMul;
let this_5 := Algebra.toModule;
let this_6 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers C);
let this_7 := this_6.toSMul;
have this_8 := Algebra.toModule;
let this_9 := Algebra.ofSubsemiring (CorvajaZannier.RatFuncInfinityIntegers S);
let this_10 := this_9.toSMul;
have this_11 := Algebra.toModule;
have this_12 := ⋯;
have this_13 := ⋯;
let this_14 := Algebra.ofSubsemiring A;
let this_15 := this_14.toSMul;
have this_16 := Algebra.toModule;
have this_17 := ⋯;
have this_18 := (ratFuncInfinityIntegersRingHom C S).toAlgebra;
let this_19 := Algebra.ofSubsemiring R₁;
let this_20 := this_19.toSMul;
have this_21 := Algebra.toModule;
have this_22 := ⋯;
let R₂ := CorvajaZannier.RatFuncInfinityIntegralClosure C N;
let B := CorvajaZannier.RatFuncInfinityIntegralClosure S L;
let this_23 := R₂.algebra;
have this_24 := this_23.toSMul;
let this_25 := Algebra.toModule;
let this_26 := B.algebra;
have this_27 := this_26.toSMul;
let this_28 := Algebra.toModule;
have this_29 := ⋯;
have this_30 := ⋯;
have this_31 := ⋯;
have this_32 := ⋯;
have this_33 := ⋯;
have this_34 := ⋯;
have this_35 := ⋯;
have this_36 := ⋯;
have this_37 := exactConstantExtensionInfinityNormalizationAlgebra C S N hExact;
differentIdeal ↥R₁ ↥B = Ideal.map (algebraMap ↥R₂ ↥B) (differentIdeal ↥A ↥R₂)
In an exact finite constant extension, the infinity different of the extended normalization is the extension of the original infinity different.