Unramified finite places over Frobenius-twist fields #
The Galois group of the exact constant extension over a Frobenius-twist field is the cyclic subgroup generated by the twist. Restriction to the enlarged constants is injective on this subgroup. An inertia automorphism acts trivially on every residue class, hence in particular on the embedded constant field. It therefore lies in the kernel of constant restriction and must be the identity. Thus every finite place is unramified in the exact constant extension over a twist field.
@[instance_reducible]
noncomputable def
BGS.HasseWeil.unramifiedConstantAlgebra
(C : Type u_1)
(N : Type u_2)
[Field C]
[Field N]
[Algebra (RatFunc C) N]
:
Algebra C N
The algebra structure from C to N used in the exact constant extension frobenius
twist finite place unramified construction.
Instances For
theorem
BGS.HasseWeil.unramifiedConstantTower
(C : Type u_1)
(N : Type u_2)
[Field C]
[Field N]
[Algebra (RatFunc C) N]
:
IsScalarTower C (RatFunc C) N
theorem
BGS.HasseWeil.exactConstantExtensionFrobeniusTwistOverFixedField_zpowers_eq_top
(C : Type u_1)
(N : Type u_2)
(S : Type u_3)
[Field C]
[Fintype C]
[Field N]
[Algebra (RatFunc C) N]
[FiniteDimensional (RatFunc C) N]
[Field S]
[Algebra C S]
[FiniteDimensional C S]
[IsGalois C S]
(hExact : algebraicClosure C N = ⊥)
(g : Gal(N/RatFunc C))
:
have this := exactConstantExtensionField C N S hExact;
have this := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
Subgroup.zpowers (exactConstantExtensionFrobeniusTwistOverFixedField C N S hExact g) = ⊤
The canonical twist generates the full Galois group over its fixed field. This is a direct consequence of defining that fixed field from the cyclic subgroup generated by the ambient twist.
theorem
BGS.HasseWeil.finitePlaceUnder_degree_eq_one_of_generator_fixed
(K : Type u_4)
(M : Type u_5)
(T : Type u_6)
[Field K]
[DecidableEq K]
[DecidableEq (RatFunc K)]
[Field M]
[Algebra (RatFunc K) M]
[FiniteDimensional (RatFunc K) M]
[Algebra.IsSeparable (RatFunc K) M]
[Field T]
[Algebra (RatFunc K) T]
[FiniteDimensional (RatFunc K) T]
[Algebra.IsSeparable (RatFunc K) T]
[Algebra M T]
[IsScalarTower (RatFunc K) M T]
[FiniteDimensional M T]
[IsGalois M T]
(sigma : Gal(T/M))
(hgen : Subgroup.zpowers sigma = ⊤)
(Q : CorvajaZannier.FiniteExtensionFinitePlace K T)
(hfixed : finitePlaceGalSmul K M T sigma Q = Q)
(hunramified : finitePlaceRelativeRamificationIdx K M T Q = 1)
(htopDegree : CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q) = Module.finrank M T)
:
If one generator of a relative Galois group fixes a top finite place, then generation, unramifiedness, and maximal possible top degree force the restricted finite place to have degree one.
theorem
BGS.HasseWeil.rationalFinitePlace_lift_degree_eq_finrank_of_finrank_dvd_degree
(K : Type u_4)
(M : Type u_5)
(T : Type u_6)
[Field K]
[DecidableEq K]
[DecidableEq (RatFunc K)]
[Field M]
[Algebra (RatFunc K) M]
[FiniteDimensional (RatFunc K) M]
[Algebra.IsSeparable (RatFunc K) M]
[Field T]
[Algebra (RatFunc K) T]
[FiniteDimensional (RatFunc K) T]
[Algebra.IsSeparable (RatFunc K) T]
[Algebra M T]
[IsScalarTower (RatFunc K) M T]
[IsGalois M T]
(hdegree :
∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T),
Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q))
(P : FiniteExtensionRationalFinitePlace K M)
(Q : CorvajaZannier.FiniteExtensionFinitePlace K T)
(hQ : finitePlaceUnder K M T Q = ↑P)
:
Conversely, under the same degree-divisibility hypothesis used for the unique-lift theorem, every lift of a rational finite place has top degree equal to the relative field degree.
noncomputable def
BGS.HasseWeil.rationalFinitePlaceEquivGeneratorFixedPlace
(K : Type u_4)
(M : Type u_5)
(T : Type u_6)
[Field K]
[DecidableEq K]
[DecidableEq (RatFunc K)]
[Field M]
[Algebra (RatFunc K) M]
[FiniteDimensional (RatFunc K) M]
[Algebra.IsSeparable (RatFunc K) M]
[Field T]
[Algebra (RatFunc K) T]
[FiniteDimensional (RatFunc K) T]
[Algebra.IsSeparable (RatFunc K) T]
[Algebra M T]
[IsScalarTower (RatFunc K) M T]
[FiniteDimensional M T]
[IsGalois M T]
(hdegree :
∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T),
Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q))
(sigma : Gal(T/M))
(hgen : Subgroup.zpowers sigma = ⊤)
(hunramified : ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T), finitePlaceRelativeRamificationIdx K M T Q = 1)
:
FiniteExtensionRationalFinitePlace K M ≃ { Q : CorvajaZannier.FiniteExtensionFinitePlace K T // CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q) = Module.finrank M T ∧ finitePlaceGalSmul K M T sigma Q = Q }
Rational finite places are equivalent to generator-fixed top finite places of relative-degree-sized absolute degree, once the relative extension is unramified and every top degree is divisible by the relative degree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
BGS.HasseWeil.finitePlaceGalSmul_eq_of_apply_eq
(K : Type u_4)
(M₁ : Type u_5)
(M₂ : Type u_6)
(T : Type u_7)
[Field K]
[Field M₁]
[Algebra (RatFunc K) M₁]
[FiniteDimensional (RatFunc K) M₁]
[Field M₂]
[Algebra (RatFunc K) M₂]
[FiniteDimensional (RatFunc K) M₂]
[Field T]
[Algebra (RatFunc K) T]
[Algebra M₁ T]
[IsScalarTower (RatFunc K) M₁ T]
[IsGalois M₁ T]
[Algebra M₂ T]
[IsScalarTower (RatFunc K) M₂ T]
[IsGalois M₂ T]
(g₁ : Gal(T/M₁))
(g₂ : Gal(T/M₂))
(happly : ∀ (x : T), g₁ x = g₂ x)
(Q : CorvajaZannier.FiniteExtensionFinitePlace K T)
:
Relative automorphisms over two intermediate fields induce the same action on top finite places when their underlying top-field maps agree.
theorem
BGS.HasseWeil.frobeniusTwistField_finitePlace_ramificationIdx_eq_one
(C : Type u_1)
(N : Type u_2)
(S : Type u_3)
[Field C]
[Fintype C]
[Field N]
[Algebra (RatFunc C) N]
[FiniteDimensional (RatFunc C) N]
[Algebra.IsSeparable (RatFunc C) N]
[Field S]
[Algebra C S]
[FiniteDimensional C S]
[IsGalois C S]
[Finite S]
(hExact : algebraicClosure C N = ⊥)
(g : Gal(N/RatFunc C))
(hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S)
:
let this := exactConstantExtensionField C N S hExact;
let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
let this_2 := this_1.toSMul;
let this_3 := Algebra.toModule;
have this_4 := ⋯;
have this_5 := ⋯;
let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g;
let this_6 := SubalgebraClass.toAlgebra F.toSubalgebra;
let this_7 := this_6.toSMul;
let this_8 := Algebra.toModule;
have this_9 := ⋯;
have this_10 := ⋯;
let this_11 := F.toAlgebra;
let this_12 := this_11.toSMul;
let this_13 := Algebra.toModule;
have this_14 := ⋯;
have this_15 := ⋯;
have this_16 := ⋯;
∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)),
finitePlaceRelativeRamificationIdx C (↥F) (ExactConstantExtension C N S) Q = 1
Every finite place of the exact constant extension is unramified over a Frobenius-twist fixed field, provided the twist has the full constant-extension order.
theorem
BGS.HasseWeil.frobeniusTwistField_fixed_finitePlace_under_degree_eq_one
(C : Type u_1)
(N : Type u_2)
(S : Type u_3)
[Field C]
[Fintype C]
[DecidableEq C]
[DecidableEq (RatFunc C)]
[Field N]
[Algebra (RatFunc C) N]
[FiniteDimensional (RatFunc C) N]
[Algebra.IsSeparable (RatFunc C) N]
[Field S]
[Algebra C S]
[FiniteDimensional C S]
[IsGalois C S]
[Finite S]
(hExact : algebraicClosure C N = ⊥)
(g : Gal(N/RatFunc C))
(hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S)
:
let this := exactConstantExtensionField C N S hExact;
let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
let this_2 := this_1.toSMul;
let this_3 := Algebra.toModule;
have this_4 := ⋯;
have this_5 := ⋯;
let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g;
let this_6 := SubalgebraClass.toAlgebra F.toSubalgebra;
let this_7 := this_6.toSMul;
let this_8 := Algebra.toModule;
have this_9 := ⋯;
have this_10 := ⋯;
let this_11 := F.toAlgebra;
let this_12 := this_11.toSMul;
let this_13 := Algebra.toModule;
have this_14 := ⋯;
have this_15 := ⋯;
have this_16 := ⋯;
∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)),
CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q) = Module.finrank C S →
finitePlaceGalSmul C (↥F) (ExactConstantExtension C N S)
(exactConstantExtensionFrobeniusTwistOverFixedField C N S hExact g) Q = Q →
CorvajaZannier.finiteExtensionPlaceDegree C (↥F)
(Sum.inl (finitePlaceUnder C (↥F) (ExactConstantExtension C N S) Q)) = 1
A top finite place of degree [S : C] fixed by the canonical twist
descends to a rational finite place of the Frobenius-twist fixed field.
theorem
BGS.HasseWeil.exactConstantExtensionFrobeniusTwist_finitePlaceGalSmul_eq_overFixedField
(C : Type u_1)
(N : Type u_2)
(S : Type u_3)
[Field C]
[Fintype C]
[Field N]
[Algebra (RatFunc C) N]
[FiniteDimensional (RatFunc C) N]
[Algebra.IsSeparable (RatFunc C) N]
[Field S]
[Algebra C S]
[FiniteDimensional C S]
[IsGalois C S]
[IsGalois (RatFunc C) N]
(hExact : algebraicClosure C N = ⊥)
(g : Gal(N/RatFunc C))
:
let this := exactConstantExtensionField C N S hExact;
let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
let this_2 := this_1.toSMul;
let this_3 := Algebra.toModule;
let this_4 := this_3.toDistribMulAction;
let this_5 := this_4.toMulAction;
have this_6 := ⋯;
have this_7 := ⋯;
have this_8 := ⋯;
let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g;
let this_9 := SubalgebraClass.toAlgebra F.toSubalgebra;
let this_10 := this_9.toSMul;
let this_11 := Algebra.toModule;
have this_12 := ⋯;
have this_13 := ⋯;
let this_14 := F.toAlgebra;
let this_15 := this_14.toSMul;
let this_16 := Algebra.toModule;
have this_17 := ⋯;
have this_18 := ⋯;
have this_19 := ⋯;
∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)),
finitePlaceGalSmul C (↥F) (ExactConstantExtension C N S)
(exactConstantExtensionFrobeniusTwistOverFixedField C N S hExact g) Q = finitePlaceGalSmul C (RatFunc C) (ExactConstantExtension C N S)
(exactConstantExtensionFrobeniusTwist C (RatFunc C) N S g) Q
The canonical twist over its fixed field and the ambient twist over
C(X) induce exactly the same action on finite places.
theorem
BGS.HasseWeil.frobeniusTwistField_ambientFixed_finitePlace_under_degree_eq_one
(C : Type u_1)
(N : Type u_2)
(S : Type u_3)
[Field C]
[Fintype C]
[DecidableEq C]
[DecidableEq (RatFunc C)]
[Field N]
[Algebra (RatFunc C) N]
[FiniteDimensional (RatFunc C) N]
[Algebra.IsSeparable (RatFunc C) N]
[Field S]
[Algebra C S]
[FiniteDimensional C S]
[IsGalois C S]
[Finite S]
[IsGalois (RatFunc C) N]
(hExact : algebraicClosure C N = ⊥)
(g : Gal(N/RatFunc C))
(hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S)
:
let this := exactConstantExtensionField C N S hExact;
let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
let this_2 := this_1.toSMul;
let this_3 := Algebra.toModule;
let this_4 := this_3.toDistribMulAction;
let this_5 := this_4.toMulAction;
have this_6 := ⋯;
have this_7 := ⋯;
have this_8 := ⋯;
let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g;
let this_9 := SubalgebraClass.toAlgebra F.toSubalgebra;
let this_10 := this_9.toSMul;
let this_11 := Algebra.toModule;
have this_12 := ⋯;
have this_13 := ⋯;
let this_14 := F.toAlgebra;
let this_15 := this_14.toSMul;
let this_16 := Algebra.toModule;
have this_17 := ⋯;
have this_18 := ⋯;
have this_19 := ⋯;
∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)),
CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q) = Module.finrank C S →
finitePlaceGalSmul C (RatFunc C) (ExactConstantExtension C N S)
(exactConstantExtensionFrobeniusTwist C (RatFunc C) N S g) Q = Q →
CorvajaZannier.finiteExtensionPlaceDegree C (↥F)
(Sum.inl (finitePlaceUnder C (↥F) (ExactConstantExtension C N S) Q)) = 1
Ambient fixedness by the Frobenius twist is therefore the exact fixedness condition needed for descent to a rational twist-field place.
noncomputable def
BGS.HasseWeil.frobeniusTwistFieldRationalFinitePlaceEquivAmbientFixedFinitePlace
(C : Type u_1)
(N : Type u_2)
(S : Type u_3)
[Field C]
[Fintype C]
[DecidableEq C]
[DecidableEq (RatFunc C)]
[Field N]
[Algebra (RatFunc C) N]
[FiniteDimensional (RatFunc C) N]
[Algebra.IsSeparable (RatFunc C) N]
[Field S]
[Algebra C S]
[FiniteDimensional C S]
[IsGalois C S]
[Finite S]
[IsGalois (RatFunc C) N]
(hExact : algebraicClosure C N = ⊥)
(g : Gal(N/RatFunc C))
(hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S)
:
let this := exactConstantExtensionField C N S hExact;
let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S;
let this_2 := this_1.toSMul;
let this_3 := Algebra.toModule;
let this_4 := this_3.toDistribMulAction;
let this_5 := this_4.toMulAction;
have this_6 := ⋯;
have this_7 := ⋯;
have this_8 := ⋯;
let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g;
let this_9 := SubalgebraClass.toAlgebra F.toSubalgebra;
let this_10 := this_9.toSMul;
let this_11 := Algebra.toModule;
have this_12 := ⋯;
have this_13 := ⋯;
let this_14 := F.toAlgebra;
let this_15 := this_14.toSMul;
let this_16 := Algebra.toModule;
have this_17 := ⋯;
have this_18 := ⋯;
have this_19 := ⋯;
FiniteExtensionRationalFinitePlace C ↥F ≃ { Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S) // CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q) = Module.finrank C S ∧ finitePlaceGalSmul C (RatFunc C) (ExactConstantExtension C N S)
(exactConstantExtensionFrobeniusTwist C (RatFunc C) N S g) Q = Q }
Rational finite places of the Frobenius-twist field are exactly the
degree-[S : C] top finite places fixed by the ambient Frobenius twist.
Equations
- One or more equations did not get rendered due to their size.