Unimodularity of the class bases #
Let E a ∈ ℤ[t] (a : Fin h) be such that, modulo p,
E a ≡ ∏_{c ≠ cls a} (t - γ_c)^{L_c} · (t - γ_{cls a})^{idx a},
where the γ_c ∈ 𝔽_p are distinct, idx a < L (cls a) and (cls, idx) is injective.
Then the coefficient matrix of the E a has a determinant prime to p.
theorem
Zeta5Irrational.sum_pow_X_sub_C_eq_zero
{F : Type u_1}
[Field F]
{ι : Type u_2}
(s : Finset ι)
(d : ι → ℕ)
(hd : Set.InjOn d ↑s)
(lam : ι → F)
(γ : F)
(h : ∑ a ∈ s, Polynomial.C (lam a) * (Polynomial.X - Polynomial.C γ) ^ d a = 0)
(a : ι)
:
A polynomial ∑_{i ∈ s} λ_i (X - γ)^i vanishes only if all λ_i vanish.
theorem
Zeta5Irrational.classBasis_independent
{F : Type u_1}
[Field F]
{h : ℕ}
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(γ : ι → F)
(hγ : Function.Injective γ)
(L : ι → ℕ)
(cls : Fin h → ι)
(idx : Fin h → ℕ)
(hidx : ∀ (a : Fin h), idx a < L (cls a))
(hinj : ∀ (a b : Fin h), cls a = cls b → idx a = idx b → a = b)
(v : Fin h → F)
(hv :
∑ a : Fin h,
Polynomial.C (v a) * ((∏ c ∈ Finset.univ.erase (cls a), (Polynomial.X - Polynomial.C (γ c)) ^ L c) * (Polynomial.X - Polynomial.C (γ (cls a))) ^ idx a) = 0)
:
Independence of the class bases over a field.
theorem
Zeta5Irrational.coeffMat_det_unit
{h p : ℕ}
[hp : Fact (Nat.Prime p)]
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(Ez : Fin h → Polynomial ℤ)
(hdeg : ∀ (a : Fin h), (Ez a).natDegree < h)
(γ : ι → ZMod p)
(hγ : Function.Injective γ)
(L : ι → ℕ)
(cls : Fin h → ι)
(idx : Fin h → ℕ)
(hidx : ∀ (a : Fin h), idx a < L (cls a))
(hinj : ∀ (a b : Fin h), cls a = cls b → idx a = idx b → a = b)
(hred :
∀ (a : Fin h),
Polynomial.map (Int.castRingHom (ZMod p)) (Ez a) = (∏ c ∈ Finset.univ.erase (cls a), (Polynomial.X - Polynomial.C (γ c)) ^ L c) * (Polynomial.X - Polynomial.C (γ (cls a))) ^ idx a)
:
(coeffMat fun (a : Fin h) => Polynomial.map (Int.castRingHom ℚ) (Ez a)).det ≠ 0 ∧ padicValRat p (coeffMat fun (a : Fin h) => Polynomial.map (Int.castRingHom ℚ) (Ez a)).det = 0
Unimodularity: the rational determinant of the coefficient matrix is a p-adic unit.