The extension k(t)[Y] / (Y ^ n - t)

For n ≠ 0, the polynomial Y ^ n - t is irreducible over the rational function field k(t), since t has order one at the place t = 0. So k(t)[Y] / (Y ^ n - t) is a field extension of k(t) of degree n, and it is separable when n is invertible in k. It is the function field of the source of the power map u ↦ u ^ n of the projective line.

Main results

• TauCeti.irreducible_X_pow_sub_C_X: Y ^ n - t is irreducible over k(t).
• TauCeti.finrank_adjoinRoot_X_pow_sub_C_X: k(t)[Y] / (Y ^ n - t) has degree n over k(t).
• TauCeti.isSeparable_adjoinRoot_X_pow_sub_C_X: it is separable over k(t) when n is invertible in k.
• TauCeti.isTotallyRamified_adjoinRoot_X_pow_sub_C_X and TauCeti.ramificationIdx_adjoinRoot_X_pow_sub_C_X_eq_one: when n is invertible in k, it is totally ramified over t = 0 and t = ∞ and unramified elsewhere.
• TauCeti.exists_equiv_restrict_eq_adicOfIrreducible_X_sub_one: when n is invertible in k, the places over t = 1 correspond to the monic irreducible factors q of X ^ n - 1 over k, with relative degree deg q. This is Kummer's theorem (TauCeti.Place.exists_equiv_restrict_eq_of_prod_eq_map_residue): Y ^ n - t reduces to Y ^ n - 1 at t = 1, which is separable.
• TauCeti.exists_setOf_restrict_eq_adicOfIrreducible_X_sub_one_eq_pair: when X ^ 2 + X + 1 is irreducible over k, as over ℚ, the extension k(t)[Y] / (Y ^ 3 - t) has two places over t = 1, of relative degrees 1 and 2. The ramification indices over t = 1 therefore do not add up to the degree; only the ramification indices weighted by the relative degrees do.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.3.7.

theorem TauCeti.irreducible_X_pow_sub_C_X (k : Type u_1) [Field k] (n : ℕ) [NeZero n] : Irreducible (Polynomial.X ^ n - Polynomial.C RatFunc.X)

Y ^ n - t is irreducible over k(t), because t has order one at the place t = 0.

instance TauCeti.instFactIrreducibleHSubPolynomialRatFuncHPowNatXCoeRingHomCX_tauCeti (k : Type u_1) [Field k] (n : ℕ) [NeZero n] : Fact (Irreducible (Polynomial.X ^ n - Polynomial.C RatFunc.X))

instance TauCeti.instFiniteDimensionalRatFuncAdjoinRootHSubPolynomialHPowNatXCoeRingHomCX_tauCeti (k : Type u_1) [Field k] (n : ℕ) [NeZero n] : FiniteDimensional (RatFunc k) (AdjoinRoot (Polynomial.X ^ n - Polynomial.C RatFunc.X))

theorem TauCeti.finrank_adjoinRoot_X_pow_sub_C_X (k : Type u_1) [Field k] (n : ℕ) [NeZero n] : Module.finrank (RatFunc k) (AdjoinRoot (Polynomial.X ^ n - Polynomial.C RatFunc.X)) = n

k(t)[Y] / (Y ^ n - t) has degree n over k(t).

theorem TauCeti.isSeparable_adjoinRoot_X_pow_sub_C_X (k : Type u_1) [Field k] (n : ℕ) [NeZero n] (hn : ↑n ≠ 0) : Algebra.IsSeparable (RatFunc k) (AdjoinRoot (Polynomial.X ^ n - Polynomial.C RatFunc.X))

k(t)[Y] / (Y ^ n - t) is separable over k(t) when n is invertible in k.

theorem TauCeti.isTotallyRamified_adjoinRoot_X_pow_sub_C_X (k : Type u_1) [Field k] (n : ℕ) [NeZero n] (hn : ↑n ≠ 0) {P : Place k (AdjoinRoot (Polynomial.X ^ n - Polynomial.C RatFunc.X))} (hP : Place.restrict k (RatFunc k) P = Place.adicOfIrreducible ⋯ ∨ Place.restrict k (RatFunc k) P = Place.infty k) : Place.IsTotallyRamified (RatFunc k) P

The power map is totally ramified over 0 and ∞: if n is invertible in k, every place of k(t)[Y] / (Y ^ n - t) over t = 0 or t = ∞ has ramification index n, so it is the only place over that point and has relative degree one.

theorem TauCeti.ramificationIdx_adjoinRoot_X_pow_sub_C_X_eq_one (k : Type u_1) [Field k] (n : ℕ) [NeZero n] (hn : ↑n ≠ 0) {P : Place k (AdjoinRoot (Polynomial.X ^ n - Polynomial.C RatFunc.X))} (hP0 : Place.restrict k (RatFunc k) P ≠ Place.adicOfIrreducible ⋯) (hPinf : Place.restrict k (RatFunc k) P ≠ Place.infty k) : Place.ramificationIdx (RatFunc k) P = 1

The power map is unramified away from 0 and ∞: if n is invertible in k, every place of k(t)[Y] / (Y ^ n - t) over a place of k(t) other than t = 0 and t = ∞, in particular over t = 1, has ramification index 1.

The places over t = 1

theorem TauCeti.exists_equiv_restrict_eq_adicOfIrreducible_X_sub_one (k : Type u_1) [Field k] (n : ℕ) [NeZero n] (hn : ↑n ≠ 0) : ∃ (e : ↥(UniqueFactorizationMonoid.normalizedFactors (Polynomial.X ^ n - 1)).toFinset ≃ { P : Place k (AdjoinRoot (Polynomial.X ^ n - Polynomial.C RatFunc.X)) // Place.restrict k (RatFunc k) P = Place.adicOfIrreducible ⋯ }), ∀ (q : ↥(UniqueFactorizationMonoid.normalizedFactors (Polynomial.X ^ n - 1)).toFinset), Place.relativeDegree k (RatFunc k) ↑(e q) = (↑q).natDegree

The places of the power map over t = 1: if n is invertible in k, the places of k(t)[Y] / (Y ^ n - t) over t = 1 correspond to the monic irreducible factors q of X ^ n - 1 in k[X], the place attached to q having relative degree deg q. They are unramified (TauCeti.ramificationIdx_adjoinRoot_X_pow_sub_C_X_eq_one), so the local data of the power map over t = 1 is {(1, deg q)}.

In particular all the places over t = 1 have relative degree one exactly when X ^ n - 1 splits over k. When it does not, as for k = ℚ and n = 3, there are fewer places than the degree (TauCeti.exists_setOf_restrict_eq_adicOfIrreducible_X_sub_one_eq_pair).

theorem TauCeti.exists_setOf_restrict_eq_adicOfIrreducible_X_sub_one_eq_pair (k : Type u_1) [Field k] (hq : Irreducible (Polynomial.X ^ 2 + Polynomial.X + 1)) : ∃ (P₁ : Place k (AdjoinRoot (Polynomial.X ^ 3 - Polynomial.C RatFunc.X))) (P₂ : Place k (AdjoinRoot (Polynomial.X ^ 3 - Polynomial.C RatFunc.X))), P₁ ≠ P₂ ∧ {P : Place k (AdjoinRoot (Polynomial.X ^ 3 - Polynomial.C RatFunc.X)) | Place.restrict k (RatFunc k) P = Place.adicOfIrreducible ⋯} = {P₁, P₂} ∧ Place.relativeDegree k (RatFunc k) P₁ = 1 ∧ Place.relativeDegree k (RatFunc k) P₂ = 2

A cube map with two places over t = 1: if X ^ 2 + X + 1 is irreducible over k, as it is over ℚ, where it is the cyclotomic polynomial Φ₃ (Polynomial.cyclotomic.irreducible_rat), then k(t)[Y] / (Y ^ 3 - t) has exactly two places over t = 1, of relative degrees 1 and 2, the factors of X ^ 3 - 1 = (X - 1) (X ^ 2 + X + 1). Both are unramified, so the ramification indices over t = 1 add up to 2 rather than to the degree 3, while the ramification indices weighted by the relative degrees add up to 1 · 1 + 1 · 2 = 3.