Theory Unimodular_Determinants
theory Unimodular_Determinants
imports Rational_Padic_Valuations
begin
section ‹Determinants of ‹p›-integral matrices and a unimodularity
criterion›
text ‹The determinant of a matrix with ‹p›-integral entries is
‹p›-integral; modulo ‹p› the
determinant of a matrix that is lower triangular modulo ‹p› is the product of its
diagonal;
hence if ‹M V = T› with ‹M›,
‹V› ‹p›-integral and ‹T› lower triangular modulo
‹p› with unit
diagonal, then ‹det M› is a ‹p›-adic unit. This is the tool behind the
unimodularity of the
inner and outer bases of the irrationality proof, but it is stated for arbitrary matrices.›
text ‹The determinant of a matrix with @{text p}-integral entries is
@{text p}-integral.›
lemma vge_det_integral:
assumes "prime p" "A ∈ carrier_mat n n" "⋀i j. i < n ⟹
j < n ⟹ vge p (A $$ (i, j)) 0"
shows "vge p (Determinant.det A) 0"
proof -
have p: "prime p" and A: "A ∈ carrier_mat n n" and Ai: "⋀i j. i < n ⟹
j < n ⟹ vge p (A $$ (i, j)) 0"
using assms by auto
have d: "Determinant.det A = (∑ σ ∈
{σ. σ permutes {0..<n}}. signof σ * (∏ i =
0..<n. A $$ (i, σ i)))"
using det_def'[OF A] by simp
have "vge p (∑ σ ∈ {σ. σ permutes {0..<n}}. signof σ *
(∏ i = 0..<n. A $$ (i, σ i))) 0"
proof (rule vge_sum[OF p])
show "finite {σ. σ permutes {0..<n}}" using finite_permutations by blast
fix σ assume "σ ∈ {σ. σ permutes {0..<n}}"
hence s: "σ permutes {0..<n}" by simp
have sg: "vge p (signof σ) 0" using vge_of_int[OF p] by simp
have pr: "vge p (∏ i = 0..<n. A $$ (i, σ i)) 0"
using vge_prod0[OF p, of "{0..<n}" "λi. A $$ (i,
σ i)"] Ai permutes_in_image[OF s] by simp
show "vge p (signof σ * (∏ i = 0..<n. A $$ (i, σ i))) 0"
using vge_mul[OF p sg pr] by simp
qed
thus ?thesis using d by simp
qed
text ‹A permutation of @{text "{0..<n}"} that is not the identity moves some @{text i}
downwards
(stated for @{text nat}; a version with an unaxiomatised @{text ord} type would be false).›
lemma permutes_not_id_exists_lt_nat:
fixes σ :: "nat ⇒ nat"
assumes "σ permutes {0..<n}" "σ ≠ id"
shows "∃i < n. σ i < i"
proof (rule ccontr)
assume nl: "¬ (∃i < n. σ i < i)"
have s: "σ permutes {0..<n}" using assms(1) .
have le: "∀i ∈ {0..<n}. i ≤ σ i" using nl by force
have sm: "(∑ i ∈ {0..<n}. i) = (∑ i ∈ {0..<n}. σ i)"
using sum.permute[OF s, of "λi. i"] by (simp add: o_def)
have eq: "∀i ∈ {0..<n}. σ i = i"
proof (rule ccontr)
assume "¬ (∀i ∈ {0..<n}. σ i = i)"
then obtain j where j: "j ∈ {0..<n}" "σ j ≠ j" by blast
have "∃a ∈ {0..<n}. a < σ a" using j le by force
hence "(∑ i ∈ {0..<n}. i) < (∑ i ∈ {0..<n}. σ i)"
using sum_strict_mono_ex1[of "{0..<n}" "λi. i" σ] le by blast
thus False using sm by linarith
qed
have "σ = id"
proof (rule ext)
fix i
show "σ i = id i" using eq permutes_not_in[OF s, of i] by auto
qed
thus False using assms(2) by simp
qed
text ‹Modulo @{text p}, the determinant of a matrix whose entries below the diagonal are
divisible by @{text p}
is the product of the diagonal.›
lemma det_cong_diag:
assumes p: "prime p" and T: "T ∈ carrier_mat n n"
and int: "⋀i j. i < n ⟹ j < n ⟹ vge p (T $$ (i, j)) 0"
and low: "⋀i j. j < i ⟹ i < n ⟹ vge p (T $$ (i, j)) 1"
shows "vge p (Determinant.det T - (∏ i < n. T $$ (i, i))) 1"
proof -
let ?S = "{σ. σ permutes {0..<n}}"
let ?f = "λσ. signof σ * (∏ i = 0..<n. T $$ (i, σ i))"
have fS: "finite ?S" using finite_permutations by blast
have idS: "id ∈ ?S" using permutes_id by simp
have "Determinant.det T = ?f id + (∑ σ ∈ ?S - {id}. ?f σ)"
using det_def'[OF T] sum.remove[OF fS idS, of ?f] by simp
moreover have "?f id = (∏ i < n. T $$ (i, i))" using sign_id atLeast0LessThan
by (simp add: atLeast0LessThan)
moreover have "vge p (∑ σ ∈ ?S - {id}. ?f σ) 1"
proof (rule vge_sum[OF p])
show "finite (?S - {id})" using fS by simp
fix σ assume "σ ∈ ?S - {id}"
hence s: "σ permutes {0..<n}" and ns: "σ ≠ id" by auto
obtain i where i: "i < n" "σ i < i" using permutes_not_id_exists_lt_nat[OF s ns] by blast
have si: "⋀j. j < n ⟹ σ j < n" using permutes_in_image[OF s]
by simp
have pr: "(∏ j = 0..<n. T $$ (j, σ j)) = T $$ (i, σ i) * (∏ j ∈
{0..<n} - {i}. T $$ (j, σ j))"
using prod.remove[of "{0..<n}" i "λj. T $$ (j, σ j)"] i by simp
have v1: "vge p (T $$ (i, σ i)) 1" using low[OF i(2) i(1)] by simp
have "vge p (∏ j ∈ {0..<n} - {i}. T $$ (j, σ j)) 0"
using vge_prod0[OF p, of "{0..<n} - {i}" "λj. T $$ (j, σ j)"] int si by simp
hence v: "vge p (T $$ (i, σ i) * (∏ j ∈
{0..<n} - {i}. T $$ (j, σ j))) (1 + 0)" by (rule vge_mul[OF p v1])
have sg: "vge p (signof σ) 0" using vge_of_int[OF p] by simp
have "vge p (signof σ * (∏ j = 0..<n. T $$ (j, σ j))) (0 + (1 + 0))"
unfolding pr by (rule vge_mul[OF p sg v])
thus "vge p (signof σ * (∏ i = 0..<n. T $$ (i, σ i))) 1" by simp
qed
ultimately show ?thesis by simp
qed
text ‹The unimodularity criterion:
if @{text "M V = T"} with @{text M}, @{text V} @{text p}-integral and @{text T} upper triangular
modulo @{text p} with unit diagonal, then @{text "det M"} is a @{text p}-adic unit.›
lemma unimodular_criterion:
assumes p: "prime p" and M: "M ∈ carrier_mat n n" and V: "V ∈ carrier_mat n n"
and Mi: "⋀i j. i < n ⟹ j < n ⟹ vge p (M $$ (i, j)) 0"
and Vi: "⋀i j. i < n ⟹ j < n ⟹ vge p (V $$ (i, j)) 0"
and low: "⋀i j. j < i ⟹ i < n ⟹
vge p ((M * V) $$ (i, j)) 1"
and diag: "⋀i. i < n ⟹ (M * V) $$ (i, i) ≠ 0 ∧
vp p ((M * V) $$ (i, i)) = 0"
shows "Determinant.det M ≠ 0 ∧ vp p (Determinant.det M) = 0"
proof -
define T where "T = M * V"
have Tc: "T ∈ carrier_mat n n" using M V by (simp add: T_def)
have Ti: "⋀i j. i < n ⟹ j < n ⟹ vge p (T $$ (i, j)) 0"
proof -
fix i j assume i: "i < n" and j: "j < n"
have e: "T $$ (i, j) = (∑ k ∈ {0..<n}. M $$ (i, k) * V $$ (k, j))"
using i j M V unfolding T_def by (simp add: index_mult_mat scalar_prod_def)
have "vge p (∑ k ∈ {0..<n}. M $$ (i, k) * V $$ (k, j)) 0"
proof (rule vge_sum[OF p])
show "finite {0..<n}" by simp
fix k assume "k ∈ {0..<n}"
hence k: "k < n" by simp
have "vge p (M $$ (i, k) * V $$ (k, j)) (0 + 0)" by (rule vge_mul[OF p Mi[OF i k] Vi[OF k j]])
thus "vge p (M $$ (i, k) * V $$ (k, j)) 0" by simp
qed
thus "vge p (T $$ (i, j)) 0" using e by simp
qed
have detT: "Determinant.det T = Determinant.det M * Determinant.det V"
unfolding T_def by (rule det_mult[OF M V])
have dprod: "(∏ i < n. T $$ (i, i)) ≠ 0 ∧ vp p (∏ i < n. T $$ (i, i)) = 0"
proof -
have dg: "⋀i. i < n ⟹ T $$ (i, i) ≠ 0 ∧
vp p (T $$ (i, i)) = 0" using diag unfolding T_def by simp
have ne: "(∏ i < n. T $$ (i, i)) ≠ 0" using dg by simp
have "vp p (∏ i < n. T $$ (i, i)) = (∑ i < n. vp p (T $$ (i, i)))"
using vp_prod_rat[OF p, of "{..<n}" "λi. T $$ (i, i)"] dg by simp
also have "… = 0" using dg by simp
finally show ?thesis using ne by simp
qed
have cong: "vge p (Determinant.det T - (∏ i < n. T $$ (i, i))) 1"
using det_cong_diag[OF p Tc Ti] T_def low by blast
have dT: "Determinant.det T ≠ 0 ∧ vp p (Determinant.det T) = 0"
proof -
define w where "w = (∏ i < n. T $$ (i, i))"
define u where "u = Determinant.det T - w"
have du: "Determinant.det T = w + u" unfolding u_def by simp
have w: "w ≠ 0" "vp p w = 0" using dprod unfolding w_def by auto
show ?thesis
proof (cases "u = 0")
case True
thus ?thesis using du w by simp
next
case False
have "1 ≤ vp p u" using cong False unfolding u_def w_def vge_def by simp
hence "vp p w < vp p u" using w by simp
hence "w + u ≠ 0 ∧ vp p (w + u) = vp p w"
by (rule vp_add_eq_of_lt[OF p w(1) False])
thus ?thesis using du w by simp
qed
qed
have vM: "vge p (Determinant.det M) 0" by (rule vge_det_integral[OF p M Mi])
have vV: "vge p (Determinant.det V) 0" by (rule vge_det_integral[OF p V Vi])
have dM: "Determinant.det M ≠ 0" and dV: "Determinant.det V ≠ 0" using dT detT
by auto
have pe: "prime_elem (int p)" using p prime_nat_int_transfer by simp
have s: "vp p (Determinant.det T) = vp p (Determinant.det M) + vp p (Determinant.det V)"
unfolding detT vp_def using qmultiplicity_mult[OF pe dM dV] by simp
have gM: "0 ≤ vp p (Determinant.det M)" using vM dM unfolding vge_def by simp
have gV: "0 ≤ vp p (Determinant.det V)" using vV dV unfolding vge_def by simp
show ?thesis using dM s gM gV dT by simp
qed
end