Restriction of rational places in a function-field tower

Place degree is multiplicative in a tower. Consequently a degree-one place of the top field restricts to a degree-one place of every intermediate field, and its relative residue degree is one. This file packages that consequence for the repository's exhaustive finite/infinity place type.

noncomputable def BGS.HasseWeil.rationalFinitePlaceUnder (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : FiniteExtensionRationalFinitePlace K L) : FiniteExtensionRationalFinitePlace K M

A degree-one finite place of the top field restricts to a degree-one finite place of the intermediate field.

Equations

• BGS.HasseWeil.rationalFinitePlaceUnder K M L Q = ⟨BGS.HasseWeil.finitePlaceUnder K M L ↑Q, ⋯⟩

noncomputable def BGS.HasseWeil.rationalInfinityPlaceUnder (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : FiniteExtensionRationalInfinityPlace K L) : FiniteExtensionRationalInfinityPlace K M

A degree-one place above infinity restricts to a degree-one place above infinity in the intermediate field.

Equations

• BGS.HasseWeil.rationalInfinityPlaceUnder K M L Q = ⟨BGS.HasseWeil.infinityPlaceUnder K M L ↑Q, ⋯⟩

noncomputable def BGS.HasseWeil.rationalPlaceUnder (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : FiniteExtensionRationalPlace K L → FiniteExtensionRationalPlace K M

Restriction of an exhaustive degree-one place through an intermediate function field.

Equations

• BGS.HasseWeil.rationalPlaceUnder K M L (Sum.inl Q) = Sum.inl (BGS.HasseWeil.rationalFinitePlaceUnder K M L Q)
• BGS.HasseWeil.rationalPlaceUnder K M L (Sum.inr Q) = Sum.inr (BGS.HasseWeil.rationalInfinityPlaceUnder K M L Q)

theorem BGS.HasseWeil.rationalFinitePlace_relativeInertiaDeg_eq_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : FiniteExtensionRationalFinitePlace K L) : finitePlaceRelativeInertiaDeg K M L ↑Q = 1

The relative residue degree of a rational finite place is one.

theorem BGS.HasseWeil.rationalInfinityPlace_relativeInertiaDeg_eq_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : FiniteExtensionRationalInfinityPlace K L) : infinityPlaceRelativeInertiaDeg K M L ↑Q = 1

The relative residue degree of a rational place above infinity is one.