Monomial bases of composita of coprime degrees

Let E / K be a finite field extension of degree ∏ᵢ mᵢ, with the mᵢ pairwise coprime, and let αᵢ ∈ E have minimal polynomials of degree mᵢ. Then the monomials ∏ᵢ αᵢ ^ Jᵢ, Jᵢ < mᵢ, form a K-basis of E (Cslib.prodPowBasis), the basis that the tensor product ⨂ᵢ K[X] / (minpoly αᵢ) would have.

The proof counts. The span of the monomials is closed under multiplication by each αᵢ, since αᵢ ^ mᵢ is a combination of lower powers, so it contains the algebra generated by the αᵢ. That algebra is a subfield whose degree is divisible by every mᵢ, hence by their product, so it is E. There are ∏ᵢ mᵢ = [E : K] monomials, so the spanning family is a basis.

Over 𝔽₂ this presents 𝔽_{2 ^ n}, n = p₁ ⋯ pₖ a product of distinct primes, through irreducible polynomials of the small degrees pᵢ, which can be found by exhaustive search.

Main definitions

• Cslib.prodPowBasis: the monomial basis J ↦ ∏ᵢ αᵢ ^ Jᵢ.

Main results

• Cslib.top_le_span_prod_pow: the monomials span E.
• Cslib.prodPowBasis_apply: the basis vectors are the monomials.
• Cslib.prodPowBasis_mul_prodPowBasis: the structure constants of the basis, from the remainders of the powers αᵢ ^ e, e < 2 mᵢ.

theorem Cslib.pow_natDegree_minpoly_mem_span {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] [FiniteDimensional K E] (α : E) : α ^ (minpoly K α).natDegree ∈ Submodule.span K (Set.range fun (e : Fin (minpoly K α).natDegree) => α ^ ↑e)

If the minimal polynomial of α has degree m, then α ^ m lies in the span of the α ^ e, e < m.

theorem Cslib.top_le_span_prod_pow {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] [FiniteDimensional K E] {ι : Type u_3} [Fintype ι] {m : ι → ℕ} {α : ι → E} (hm : Pairwise (Function.onFun Nat.Coprime m)) (hE : Module.finrank K E = ∏ i : ι, m i) (hα : ∀ (i : ι), (minpoly K (α i)).natDegree = m i) : ⊤ ≤ Submodule.span K (Set.range fun (J : (i : ι) → Fin (m i)) => ∏ i : ι, α i ^ ↑(J i))

The monomials ∏ᵢ αᵢ ^ Jᵢ, Jᵢ < mᵢ, span E when [E : K] = ∏ᵢ mᵢ with the mᵢ pairwise coprime and mᵢ the degree of the minimal polynomial of αᵢ.

noncomputable def Cslib.prodPowBasis {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] [FiniteDimensional K E] {ι : Type u_3} [Fintype ι] {m : ι → ℕ} {α : ι → E} [DecidableEq ι] (hm : Pairwise (Function.onFun Nat.Coprime m)) (hE : Module.finrank K E = ∏ i : ι, m i) (hα : ∀ (i : ι), (minpoly K (α i)).natDegree = m i) : Module.Basis ((i : ι) → Fin (m i)) K E

The monomial basis of a compositum of coprime degrees: if [E : K] = ∏ᵢ mᵢ with the mᵢ pairwise coprime and the minimal polynomial of αᵢ has degree mᵢ, then the monomials ∏ᵢ αᵢ ^ Jᵢ, Jᵢ < mᵢ, form a basis of E over K.

@[simp]

theorem Cslib.prodPowBasis_apply {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] [FiniteDimensional K E] {ι : Type u_3} [Fintype ι] {m : ι → ℕ} {α : ι → E} [DecidableEq ι] (hm : Pairwise (Function.onFun Nat.Coprime m)) (hE : Module.finrank K E = ∏ i : ι, m i) (hα : ∀ (i : ι), (minpoly K (α i)).natDegree = m i) (J : (i : ι) → Fin (m i)) : (prodPowBasis hm hE hα) J = ∏ i : ι, α i ^ ↑(J i)

The basis vector of prodPowBasis at exponents J is the monomial ∏ᵢ αᵢ ^ Jᵢ.

theorem Cslib.prodPowBasis_mul_prodPowBasis {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] [FiniteDimensional K E] {ι : Type u_3} [Fintype ι] {m : ι → ℕ} {α : ι → E} [DecidableEq ι] (hm : Pairwise (Function.onFun Nat.Coprime m)) (hE : Module.finrank K E = ∏ i : ι, m i) (hα : ∀ (i : ι), (minpoly K (α i)).natDegree = m i) (c : (i : ι) → ℕ → Fin (m i) → K) (hc : ∀ (i : ι), ∀ e < 2 * m i, α i ^ e = ∑ d : Fin (m i), c i e d • α i ^ ↑d) (J J' : (i : ι) → Fin (m i)) : (prodPowBasis hm hE hα) J * (prodPowBasis hm hE hα) J' = ∑ M : (i : ι) → Fin (m i), (∏ i : ι, c i (↑(J i) + ↑(J' i)) (M i)) • (prodPowBasis hm hE hα) M

Structure constants of the monomial basis. If each power αᵢ ^ e, e < 2 mᵢ, is the combination ∑_d c i e d • αᵢ ^ d of the powers below mᵢ, then the product of the monomial basis vectors of J and K is the combination of those of M with the coefficients ∏ᵢ c i (Jᵢ + Kᵢ) Mᵢ. The coefficients depend only on the c i, not on the αᵢ.