Theory Determinant_Linear_Function
theory Determinant_Linear_Function
imports Determinants
begin
subsection ‹Determinants of linear functions between Euclidean spaces›
text ‹
\<^const>‹Determinants.det› is the determinant of a square matrix. In the following, we define
the equivalent notion of the determinant of an endomorphism (in a finite-dimensional vector
space).
›
abbreviation matrix_det :: "(('a :: comm_ring_1, 'b :: finite) vec, 'b) vec ⇒ 'a"
where "matrix_det ≡ Determinants.det"
lemmas matrix_det_def = Determinants.det_def
context finite_dimensional_vector_space
begin
definition det :: "('b ⇒ 'b) ⇒ 'a" where
"det f = (∑p | p permutes Basis. of_int (sign p) *
(∏b∈Basis. representation Basis (f (p b)) b))"
lemma det_cong:
assumes "⋀b. b ∈ Basis ⟹ f b = g b"
shows "local.det f = local.det g"
unfolding local.det_def
by (intro sum.cong arg_cong2[of _ _ _ _ "(*)"] refl prod.cong)
(simp_all add: permutes_in_image assms)
lemma det_id [simp]: "local.det id = 1"
proof -
have "local.det id =
(∑p | p permutes Basis. of_int (sign p) * (∏b∈Basis. representation Basis (p b) b))"
by (simp add: det_def)
also have "(∑p | p permutes Basis. of_int (sign p) * (∏b∈Basis. representation Basis (p b) b)) =
(∑p | p permutes Basis. of_int (sign p) * (if p = id then 1 else 0))"
using finite_Basis representation_basis[OF independent_Basis]
proof (intro sum.cong, goal_cases)
case (2 p)
show ?case
proof (cases "p = id")
case False
then obtain b where "p b ≠ b"
by (auto simp: fun_eq_iff)
with 2 have "b ∈ Basis"
using permutes_not_in[of p Basis b] by auto
with ‹p b ≠ b› show ?thesis using finite_Basis 2
by (auto simp: representation_basis[OF independent_Basis] permutes_in_image)
qed (auto simp: representation_basis[OF independent_Basis])
qed auto
also have "… = (∑p ∈ {id :: 'b ⇒ 'b}. 1)"
by (rule sum.mono_neutral_cong_right) (auto simp: finite_permutations finite_Basis)
finally show ?thesis
by simp
qed
lemma det_ident [simp]: "local.det (λx. x) = 1"
using det_id unfolding id_def by simp
lemma det_scale:
"local.det (λx. scale c (f x)) = c ^ dimension * local.det f"
proof -
define r where "r = representation Basis"
interpret r: Vector_Spaces.linear scale "(*)" "λx. r x b" for b
unfolding r_def by (intro linear_representation independent_Basis span_Basis)
have "local.det (λx. scale c (f x)) =
(∑p | p permutes Basis. of_int (sign p) * (∏b∈Basis. r (c *s f (p b)) b))"
unfolding local.det_def r_def by simp
also have "… = c ^ card Basis * (∑p | p permutes Basis. of_int (sign p) * (∏b∈Basis. r (f (p b)) b))"
by (simp add: r.scale sum_distrib_left sum_distrib_right mult_ac prod.distrib)
also have "… = c ^ dimension * local.det f"
by (simp add: local.det_def r_def dimension_def)
finally show ?thesis .
qed
lemma det_scale': "local.det (scale c) = c ^ dimension"
by (simp add: det_scale)
lemma det_minus: "local.det (λx. -f x) = (-1) ^ dimension * local.det f"
using det_scale[of "-1" f] by simp
lemma det_minus': "local.det (λx. -x) = (-1) ^ dimension"
using det_scale[of "-1" id] by simp
text ‹
The determinant commutes with function composition.
›
theorem det_compose:
assumes f: "Vector_Spaces.linear scale scale f" and g: "Vector_Spaces.linear scale scale g"
shows "local.det (f ∘ g) = local.det f * local.det g"
proof -
define r where "r = representation Basis"
interpret f: Vector_Spaces.linear scale scale f
by fact
interpret g: Vector_Spaces.linear scale scale g
by fact
interpret r: Vector_Spaces.linear scale "(*)" "λx. r x b" for b
unfolding r_def by (intro linear_representation independent_Basis span_Basis)
define s :: "('b ⇒ 'b) ⇒ 'a" where "s = of_int ∘ sign"
define P where "P = {p. p permutes Basis}"
define P' where "P' = (Basis →⇩E Basis) ∩ {f. inj_on f Basis}"
define P_bad where "P_bad = (Basis →⇩E Basis) - {f. inj_on f Basis}"
define R where "R = (λp. (∑q∈P_bad. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b)))"
have r: "(∑b∈Basis. r v b *s b) = v" for v unfolding r_def
by (rule sum_representation_eq) (use finite_Basis span_Basis independent_Basis in auto)
have [simp]: "q b ∈ Basis ⟷ b ∈ Basis" if "q ∈ P" for q b
using that by (simp add: permutes_in_image P_def)
have [simp]: "inv p ∈ P" if "p ∈ P" for p
using that unfolding P_def by (auto simp: permutes_inv)
have [simp]: "p ∘ q ∈ P" if "p ∈ P" "q ∈ P" for p q
using that unfolding P_def by (auto simp: permutes_compose)
have [simp]: "p (inv p x) = x" "inv p (p x) = x" "p ∘ inv p = id" "inv p ∘ p = id"
if "p ∈ P" for p x
proof -
interpret p: bijection p
by unfold_locales (use that in ‹auto simp: P_def permutes_bij›)
show "p (inv p x) = x" "inv p (p x) = x" "p ∘ inv p = id" "inv p ∘ p = id"
by simp_all
qed
have [simp]: "s (p ∘ q) = s p * s q" if "p ∈ P" "q ∈ P" for p q
unfolding s_def o_apply[of of_int] using that
by (subst sign_compose) (auto simp: P_def sign_compose intro: permutes_imp_permutation finite_Basis)
have [simp]: "f ∘ p ∈ P_bad ⟷ f ∈ P_bad" if "p ∈ P" for f p
proof -
have "f ∘ p ∈ P_bad" if "f ∈ P_bad" "p ∈ P" for f p
proof -
have p: "p permutes Basis"
using that by (auto simp: P_def)
from that have "¬inj_on f Basis"
unfolding P_bad_def by blast
hence "inj_on (f ∘ p) Basis ⟷ inj_on f Basis"
using comp_inj_on_iff[OF permutes_inj_on[OF p], of f Basis] permutes_image[OF p] by simp
thus "f ∘ p ∈ P_bad"
using that by (auto simp: P_bad_def PiE_def extensional_def Pi_def permutes_in_image[OF p])
qed
from this[of f p] this[of "f ∘ p" "inv p"] show ?thesis
using that by (auto simp flip: o_assoc)
qed
have "local.det (f ∘ g) = (∑p∈P. s p * (∏b∈Basis. r (f (g (p b))) b))"
unfolding det_def r_def s_def P_def by simp
also have "… = (∑p∈P. s p * (∑q∈P. (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p (inv q b))) b)) + s p * R p)"
proof (intro sum.cong refl, goal_cases)
case p: (1 p)
define restr :: "('b ⇒ 'b) ⇒ 'b ⇒ 'b" where "restr = (λp. restrict p Basis)"
define unrestr :: "('b ⇒ 'b) ⇒ 'b ⇒ 'b" where "unrestr = (λp x. if x ∈ Basis then p x else x)"
have "(∏b∈Basis. r (f (g (p b))) b) = (∏b∈Basis. r (f (∑b'∈Basis. r (g (p b)) b' *s b')) b)"
by (subst r) auto
also have "… = (∏b∈Basis. ∑b'∈Basis. r (f b') b * r (g (p b)) b')"
by (simp add: f.sum r.sum f.scale r.scale mult_ac)
also have "… = (∑q∈Basis →⇩E Basis. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b))"
by (subst prod_sum_PiE) (auto simp: finite_Basis)
also have "Basis →⇩E Basis = P' ∪ P_bad"
unfolding P'_def P_bad_def by blast
have "(∑q∈Basis →⇩E Basis. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b)) =
(∑q∈P'. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b)) + R p"
unfolding ‹Basis →⇩E Basis = P' ∪ P_bad›
by (subst sum.union_disjoint) (auto simp: P'_def P_bad_def R_def intro: finite_PiE finite_Basis)
also have "(∑q∈P'. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b)) =
(∑q∈P. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b))"
proof (rule sum.reindex_bij_witness[of _ restr unrestr], goal_cases)
case (2 q)
hence "inj_on q Basis" "q ∈ Basis → Basis"
by (auto simp: P'_def)
hence "q ` Basis = Basis"
by (meson Pi_mem endo_inj_surj image_subset_iff finite_Basis)
with ‹inj_on q Basis› have "bij_betw q Basis Basis"
unfolding bij_betw_def by blast
hence "bij_betw (unrestr q) (Basis ∪ -Basis) (Basis ∪ -Basis)"
unfolding unrestr_def by (rule bij_betw_disjoint_Un) (auto simp: bij_betw_def)
hence "bij (unrestr q)"
by simp
moreover have "unrestr q x = x" if "x ∉ Basis" for x
using that by (auto simp: unrestr_def)
ultimately have "unrestr q permutes Basis"
unfolding permutes_def bij_iff by blast
thus ?case
by (auto simp: P_def unrestr_def)
qed (auto simp: unrestr_def restr_def fun_eq_iff P_def permutes_not_in P'_def permutes_inj_on)
also have "… = (∑q∈P. (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p b)) (q b)))"
by (simp add: prod.distrib)
also have "… = (∑q∈P. (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p (inv q b))) b))"
proof (intro sum.cong refl arg_cong2[of _ _ _ _ "(*)"], goal_cases)
case q: (1 q)
interpret bijection q
by unfold_locales (use q permutes_bij[of q] in ‹auto simp: P_def›)
show "(∏b∈Basis. r (g (p b)) (q b)) = (∏b∈Basis. r (g (p (inv q b))) b)"
by (rule prod.reindex_bij_witness[of _ "inv q" q]) (use q in simp_all)
qed
finally show ?case
by (simp add: algebra_simps)
qed
also have "… = (∑p∈P. ∑q∈P. s p * (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p (inv q b))) b)) +
(∑p∈P. s p * R p)"
by (simp add: sum_distrib_left mult.assoc sum.distrib)
also have "(∑p∈P. ∑q∈P. s p * (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p (inv q b))) b)) =
(∑(p,q)∈P×P. s p * (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p (inv q b))) b))"
by (subst sum.cartesian_product) auto
also have "… = (∑(p,q)∈P×P. s (p ∘ q) * (∏b∈Basis. r (f (q b)) b) * (∏b∈Basis. r (g (p b)) b))"
by (rule sum.reindex_bij_witness[of _ "λ(p,q). (p ∘ q, q)" "λ(p,q). (p ∘ inv q, q)"])
(auto simp: fun_eq_iff simp flip: o_assoc)
also have "… = (∑q∈P. s q * (∏b∈Basis. r (f (q b)) b)) * (∑p∈P. s p * (∏b∈Basis. r (g (p b)) b))"
unfolding sum_distrib_left unfolding sum_distrib_right
by (simp add: algebra_simps flip: sum.cartesian_product)
also have "… = local.det f * local.det g"
by (simp add: det_def P_def s_def r_def)
also have "(∑p∈P. s p * R p) = 0"
proof -
define R' where "R' = (λp q. ∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b))"
have "(∑p∈P. s p * R p) = (∑p∈P. ∑q∈P_bad. s p * (∏b∈Basis. r (f (q b)) b * r (g (p b)) (q b)))"
by (simp add: R_def sum_distrib_left)
also have "… = (∑p∈P. ∑q∈P_bad. s p * (∏b∈Basis. r (f ((q ∘ p) b)) b * r (g (p b)) ((q ∘ p) b)))"
proof (rule sum.cong[OF refl], goal_cases)
case (1 p)
show ?case
by (rule sum.reindex_bij_witness[of _ "λq. q ∘ p" "λq. q ∘ inv p"]) (use 1 in auto)
qed
also have "… = (∑q∈P_bad. ∑p∈P. s p * (∏b∈Basis. r (f (q (p b))) b * r (g (p b)) (q (p b))))"
by (subst sum.swap) (simp_all add: mult_ac)
also have "… = (∑q∈P_bad. 0)"
proof (intro sum.cong refl, goal_cases)
case (1 q)
from 1 obtain b1 b2 where b12: "b1 ∈ Basis" "b2 ∈ Basis" "b1 ≠ b2" "q b1 = q b2"
unfolding P_bad_def inj_on_def by blast
define t where "t = Transposition.transpose b1 b2"
have [simp]: "t ∘ t = id" "s t = -1"
using b12 by (auto simp: t_def s_def sign_swap_id)
have [simp]: "t ∈ P"
using b12 by (auto simp: P_def t_def permutes_swap_id)
have s: "s (t ∘ p) = -s p" if "p ∈ P" for p
using that by simp
define h where "h = (λp. ((∏b∈Basis. r (f (q (p b))) b) * (∏b∈Basis. r (g b) (q b))))"
have "(∑p∈P. s p * (∏b∈Basis. r (f (q (p b))) b * r (g (p b)) (q (p b)))) = (∑p∈P. s p * h p)"
unfolding prod.distrib h_def
proof (intro sum.cong arg_cong2[of _ _ _ _ "(*)"] refl, goal_cases)
case (1 p)
show "(∏b∈Basis. r (g (p b)) (q (p b))) = (∏b∈Basis. r (g b) (q b))"
by (rule prod.reindex_bij_witness[of _ "inv p" p]) (use 1 in simp_all)
qed
also have "(∑p∈P. s p * h p) = 0"
proof (rule sum_involution_eq_0)
fix p assume p: "p ∈ P"
have "permutation p"
using P_def finite_Basis p permutes_imp_permutation by auto
hence "evenperm (t ∘ p) ⟷ ¬evenperm p"
using b12 by (subst evenperm_comp) (auto simp: t_def evenperm_swap permutation_swap_id)
thus "t ∘ p ≠ p"
by metis
have "s (t ∘ p) = -s p"
using p by auto
moreover have "h (t ∘ p) = h p" unfolding h_def using b12
by (intro arg_cong2[of _ _ _ _ "(*)"] refl prod.cong)
(auto simp: h_def t_def Transposition.transpose_def)
ultimately show "s (t ∘ p) * h (t ∘ p) + s p * h p = 0"
by simp
qed (auto simp: o_assoc)
finally show ?case .
qed
finally show ?thesis
by simp
qed
finally show ?thesis
by (simp add: o_def)
qed
lemma det_permute:
assumes "q permutes Basis"
shows "local.det (f ∘ q) = of_int (sign q) * local.det f"
proof -
have "local.det (f ∘ q) = (∑p | p permutes Basis.
of_int (sign p) * (∏b∈Basis. representation Basis (f ((q ∘ p) b)) b))"
unfolding det_def by (simp add: o_def)
also have "… = (∑p | p permutes Basis. of_int (sign q) * (of_int (sign (q ∘ p)) *
(∏b∈Basis. representation Basis (f ((q ∘ p) b)) b)))"
by (intro sum.cong refl, subst sign_compose)
(use assms in ‹auto simp flip: of_int_mult intro: permutes_imp_permutation finite_Basis›)
also have "… = (∑p | p permutes Basis. of_int (sign q) * (of_int (sign p) *
(∏b∈Basis. representation Basis (f (p b)) b)))"
by (rule sum.reindex_bij_witness[of _ "λp. inv q ∘ p" "λp. q ∘ p"])
(use assms in ‹simp_all add: permutes_compose permutes_inv permutes_inv_o o_assoc›)
also have "… = of_int (sign q) * local.det f"
by (simp only: det_def sum_distrib_left)
finally show ?thesis .
qed
lemma det_permute':
assumes "q permutes Basis"
shows "local.det q = of_int (sign q)"
using det_permute[OF assms, of id] by simp
lemma det_bij_betw_Basis:
assumes "bij_betw q Basis Basis"
shows "local.det q = of_int (sign_on Basis q)"
proof -
have "local.det q = local.det (restrict_id q Basis)"
by (rule det_cong) auto
also have "… = of_int (sign_on Basis q)"
by (subst det_permute') (auto simp: sign_on_def intro!: permutes_restrict_id assms)
finally show ?thesis .
qed
corollary det_inv:
assumes "Vector_Spaces.linear scale scale f" "inj f"
shows "local.det (inv f) = inverse (local.det f)"
proof -
have "bij f"
using assms by (simp add: bijI linear_inj_imp_surj)
interpret f: bijection f
by standard fact
have "local.det (f ∘ inv f) = 1"
by simp
also have "local.det (f ∘ inv f) = local.det f * local.det (inv f)"
using assms ‹inj f› by (subst det_compose) (auto simp: inj_linear_imp_inv_linear)
finally show ?thesis
by (auto simp: divide_simps mult_ac)
qed
lemma inj_imp_det_nonzero:
assumes "Vector_Spaces.linear scale scale f" "inj f"
shows "local.det f ≠ 0"
proof
assume [simp]: "local.det f = 0"
hence "bij f"
using assms by (simp add: bijI linear_inj_imp_surj)
interpret f: bijection f
by standard fact
have "local.det (f ∘ inv f) = 1"
by simp
also have "local.det (f ∘ inv f) = 0"
using assms ‹inj f› by (subst local.det_compose) (auto simp: inj_linear_imp_inv_linear)
finally show False
by simp
qed
text ‹
The determinant vanishes if and only if the function is not a bijection.
›
theorem det_eq_0_iff:
assumes "Vector_Spaces.linear scale scale f"
shows "local.det f = 0 ⟷ ¬inj f"
proof (cases "Basis = {}")
case True
hence "(∀x::'b. x = 0)" using span_Basis
by auto
hence "inj f"
unfolding inj_def by metis
moreover have "local.det f = 1"
unfolding det_def by (subst (2 3) True) auto
ultimately show ?thesis
by simp
next
case False
then obtain b where b: "b ∈ Basis"
by blast
have "local.det f = 0" if "¬inj f"
proof -
from ‹¬inj f› obtain x where x: "x ≠ 0" "f x = 0"
by (meson assms module_hom.inj_iff_eq_0 module_hom_eq_linear)
from b have "independent {b}"
by auto
then obtain g where g: "Vector_Spaces.linear scale scale g" "inj g" "g b = x"
using linear_independent_extend_inj[of "{b}" "λ_. x"] x by auto
interpret g: bijection g
by unfold_locales (use g in ‹simp add: bijI linear_inj_imp_surj›)
have "local.det f = local.det (inv g ∘ f ∘ g)"
using assms g
by (auto simp: Vector_Spaces.linear_compose inj_linear_imp_inv_linear
det_compose det_inv inj_imp_det_nonzero)
also have "… = (∑p | p permutes Basis. 0)"
unfolding det_def
proof (rule sum.cong, goal_cases)
case (2 p)
interpret p: bijection p
using 2 by (simp add: bijection_def permutes_bij)
interpret invg: Vector_Spaces.linear scale scale "inv g"
using g(1,2) by (intro inj_linear_imp_inv_linear)
have "inv p b ∈ Basis"
using b 2 permutes_in_image by fastforce
hence "(∃a∈Basis. representation Basis (inv g (f (g (p a)))) a = 0)"
by (intro bexI[of _ "inv p b"]) (auto simp: g(3) x representation_zero)
thus ?case
using finite_Basis by simp
qed auto
finally show "local.det f = 0"
by simp
qed
thus ?thesis
using inj_imp_det_nonzero[OF assms] by auto
qed
end
text ‹
The determinant is invariant under basis changes:
›
theorem (in finite_dimensional_vector_space_pair) det_basis_change:
assumes "Vector_Spaces.linear (*a) (*b) h" "bij_betw h B1 B2"
shows "vs1.det f = vs2.det (h ∘ f ∘ inv h)"
proof -
define r1 where "r1 = vs1.representation B1"
define r2 where "r2 = vs2.representation B2"
interpret r1: Vector_Spaces.linear "(*a)" "(*)" "λx. r1 x b" for b
unfolding r1_def
by (rule vs1.linear_representation) (auto simp: vs1.independent_Basis vs1.span_Basis)
interpret r2: Vector_Spaces.linear "(*b)" "(*)" "λx. r2 x b" for b
unfolding r2_def
by (rule vs2.linear_representation) (auto simp: vs2.independent_Basis vs2.span_Basis)
have "bij h"
by (metis assms bijI bij_betw_finite bij_betw_iff_card bij_betw_imp_surj_on
local.linear_span_image local.linear_surjective_imp_injective vs1.dim_UNIV
vs1.finite_Basis vs1.span_Basis vs2.dim_UNIV vs2.span_Basis)
note h = this assms(2)
interpret h: Vector_Spaces.linear "(*a)" "(*b)" h
by fact
interpret inv_h: Vector_Spaces.linear "(*b)" "(*a)" "inv h"
by (meson h(1) h.module_hom_axioms local.bij_module_hom_imp_inv_module_hom module_hom_eq_linear)
have bij_betw_inv_h: "bij_betw (inv h) B2 B1"
using h by (metis bij_betw_def inj_imp_bij_betw_inv)
have [simp]: "h x = h y ⟷ x = y" for x y
using h(1) by (auto simp: bij_def inj_def)
have [simp]: "inv h ∘ h = id"
by (simp add: bij_is_inj h(1))
hence [simp]: "inv h (h x) = x" for x
unfolding fun_eq_iff o_def id_def by blast
have [simp]: "h ∘ inv h = id"
by (meson bij_betw_def h(1) surj_iff)
hence [simp]: "h (inv h x) = x" for x
unfolding fun_eq_iff o_def id_def by blast
define map1 where "map1 = map_permutation B1 h"
define map2 where "map2 = map_permutation B2 (inv h)"
have r1_conv_r2: "r1 x b = r2 (h x) (h b)" for x b
proof -
have *: "r1 b' b = r2 (h b') (h b)" if "b' ∈ B1" for b'
proof -
have *: "h b' ∈ B2"
using h(2) that by (auto simp: bij_betw_def)
show ?thesis
unfolding r1_def r2_def
by (subst vs1.representation_basis[OF vs1.independent_Basis that(1)],
subst vs2.representation_basis[OF vs2.independent_Basis *(1)]) auto
qed
obtain c where x: "x = (∑v∈B1. c v *a v)"
using vs1.span_Basis unfolding vs1.span_finite[OF vs1.finite_Basis] by blast
show ?thesis
by (simp add: x r1.sum r2.sum r1.scale r2.scale h.sum h.scale *)
qed
have "vs1.det f = (∑p | p permutes B1. of_int (sign p) * (∏b∈B1. r1 (f (p b)) b))"
unfolding vs1.det_def r1_def ..
also have "… = (∑p | p permutes B2. of_int (sign p) * (∏b∈B1. r1 (f (map2 p b)) b))"
using h bij_betw_imp_inj_on[OF bij_betw_inv_h] vs1.finite_Basis bij_betw_imp_inj_on[OF h(2)]
by (intro sum.reindex_bij_witness[of _ map2 map1])
(auto simp: map1_def map2_def sign_map_permutation
map_permutation_compose[OF h(2)]
map_permutation_compose[OF bij_betw_inv_h] bij_is_inj
intro!: map_permutation_permutes bij_betw_inv_h h)
also have "… = (∑p | p permutes B2. of_int (sign p) * (∏b∈B2. r2 ((h ∘ f ∘ inv h) (p b)) b))"
proof (intro sum.cong arg_cong2[of _ _ _ _ "(*)"] refl, goal_cases)
case p: (1 p)
have "(∏b∈B1. r1 (f (map2 p b)) b) = (∏b∈B2. r1 (f (inv h (p b))) (inv h b))"
using bij_betw_inv_h p
by (intro prod.reindex_bij_witness[of _ "inv h" h])
(auto simp: bij_betw_def map2_def map_permutation_apply[OF bij_betw_imp_inj_on[OF bij_betw_inv_h]])
also have "… = (∏b∈B2. r2 ((h ∘ f ∘ inv h) (p b)) b)"
by (intro prod.cong refl) (auto simp: r1_conv_r2)
finally show ?case .
qed
also have "… = vs2.det (h ∘ f ∘ inv h)"
unfolding vs2.det_def r2_def ..
finally show ?thesis .
qed
text ‹
To compute the determinant of a linear function, we can choose whichever basis is
most convenient for us.
›
corollary (in finite_dimensional_vector_space) det_eq:
assumes f: "Vector_Spaces.linear scale scale f" and B: "independent B" "span B = UNIV"
shows "local.det f =
(∑p | p permutes B. of_int (sign p) * (∏b∈B. representation B (f (p b)) b))"
proof -
have [simp, intro]: "finite B"
by (rule finiteI_independent) fact
interpret B: finite_dimensional_vector_space scale B
by standard (use B in auto)
interpret pair: finite_dimensional_vector_space_pair scale Basis scale B ..
have "local.dimension = B.dimension"
using B B.dim_UNIV local.dim_UNIV unfolding local.dimension_def B.dimension_def by simp
then obtain h where h: "Vector_Spaces.linear scale scale h" "bij h" "bij_betw h Basis B"
using pair.basis_change_exists by blast
have h_inv: "Vector_Spaces.linear scale scale (inv h)"
by (rule inj_linear_imp_inv_linear) (use h in ‹auto simp: bij_is_inj›)
have "local.det f = B.det (h ∘ f ∘ inv h)"
by (rule pair.det_basis_change) fact+
also have "… = B.det f"
using h h_inv bij_is_inj[of h] B.det_eq_0_iff[of h]
by (simp add: f h B.det_compose B.det_inv Vector_Spaces.linear_compose[of _ scale] field_simps)
finally show ?thesis
by (simp add: B.det_def)
qed
text ‹
In particular, this gives us a notion of determinant for linear maps in a Euclidean space
(in the sence of the \<^class>‹euclidean_space› type class).
›
lemma eucl_det_def:
"eucl.det f = (∑p | p permutes Basis. of_int (sign p) * (∏b∈Basis. f (p b) ∙ b))"
by (simp add: eucl.det_def representation_euclidean_space)
text ‹
The determinant of an endomorphism of $\mathbb{R}^n$ is equal to the determinant
of the matrix representing it.
›
lemma eucl_det_conv_matrix_det:
fixes f :: "real ^ 'n ⇒ real ^ 'n"
assumes "linear f"
shows "eucl.det f = matrix_det (matrix f)"
proof -
define g where "g = (λi. axis i 1 :: real ^ 'n)"
define g' where "g' = inv g"
define h where "h = map_permutation UNIV g"
define h' where "h' = map_permutation Basis g'"
have "inj g"
unfolding g_def by (auto intro!: injI simp: axis_eq_axis)
hence [simp]: "g' (g i) = i" for i
by (simp add: inj_iff g'_def)
have [simp]: "g (g' b) = b" if "b ∈ Basis" for b
using that inv_f_f[of g] ‹inj g› by (auto simp: Basis_vec_def g_def g'_def)
have bij_g: "bij_betw g UNIV Basis"
using ‹inj g› unfolding bij_betw_def Basis_vec_def by (auto simp: g_def)
have [intro]: "h p permutes Basis" if "p permutes UNIV" for p
unfolding h_def by (intro map_permutation_permutes that bij_g)
have [intro]: "h' p permutes UNIV" if "p permutes Basis" for p
unfolding h'_def g'_def
by (intro map_permutation_permutes that bij_g bij_betw_inv_into)
have [simp]: "h' (h p) = p" if "p permutes UNIV" for p
unfolding h'_def h_def g'_def
by (subst map_permutation_compose_inv) (use bij_g that in ‹auto simp flip: g'_def›)
have [simp]: "h (h' p) = p" if "p permutes Basis" for p
unfolding h'_def h_def g'_def using bij_betw_inv_into[OF bij_g]
by (subst map_permutation_compose_inv) (use bij_g that in ‹auto simp flip: g'_def›)
have [simp]: "g b ∈ Basis" for b
unfolding Basis_vec_def g_def by auto
have "matrix_det (matrix f) = (∑p | p permutes UNIV. of_int (sign p) * (∏i∈UNIV. matrix f $ i $ p i))"
unfolding matrix_det_def ..
also have "… = (∑p | p permutes Basis. of_int (sign p) * (∏b∈Basis. f (p b) ∙ b))"
proof (intro sum.reindex_bij_witness[of _ h' h] arg_cong2[of _ _ _ _ "(*)"]
arg_cong[of _ _ of_int] prod.reindex_bij_witness[of _ g g'])
fix p :: "'n ⇒ 'n" and b :: "real ^ 'n"
assume p: "p ∈ {p. p permutes UNIV}" and b: "b ∈ Basis"
from b obtain i where [simp]: "b = axis i 1"
unfolding Basis_vec_def by auto
have "matrix f $ g' b $ p (g' b) = f (g (p (g' (g i)))) $ g' (g i)"
unfolding matrix_def g_def by (auto simp: h_def)
also have "… = f (g (p i)) $ i"
by simp
also have "… = f (map_permutation UNIV g p (g i)) $ i"
by (subst map_permutation_apply) (use ‹inj g› in auto)
also have "… = f (h p b) ∙ b"
by (simp add: h_def g_def inner_axis)
finally show "matrix f $ g' b $ p (g' b) = f (h p b) ∙ b" .
next
fix p :: "'n ⇒ 'n"
assume p: "p ∈ {p. p permutes UNIV}"
thus "sign (h p) = sign p"
unfolding h_def using ‹inj g› by (subst sign_map_permutation) auto
qed auto
also have "… = eucl.det f"
unfolding eucl_det_def ..
finally show ?thesis ..
qed
subsection ‹Absolute determinant of a multiset›
text ‹
For the ``normal'' determinant of a list of vectors, the order of the vectors matters insofar
as it determines the sign. If we look at the absolute value of the determinant, however, the
order does not matter and we can therefore define the absolute determinant of a (finite) multiset
of vectors.
This can e.g.\ be useful to check whether a multiset of vectors is dependent or not.
›
definition abs_det :: "('a :: euclidean_space) multiset ⇒ real" where
"abs_det X = (if size X ≠ DIM('a) then 0
else (THE d. ∀f. image_mset f (mset_set Basis) = X ⟶ ¦eucl.det f¦ = d))"
lemma abs_det_eq_0 [simp]:
"size (X :: 'a multiset) ≠ DIM('a :: euclidean_space) ⟹ abs_det X = 0"
by (simp add: abs_det_def)
lemma abs_det_conv_det:
assumes "image_mset f (mset_set (Basis :: 'a :: euclidean_space set)) = (X :: 'a multiset)"
shows "abs_det X = ¦eucl.det f¦"
proof -
have size_eq: "size X = DIM('a)"
by (subst assms [symmetric]) auto
hence abs_det_eq:
"abs_det X = (THE d. ∀f'. image_mset f' (mset_set Basis) =
image_mset f (mset_set Basis) ⟶ ¦eucl.det f'¦ = d)"
by (simp add: abs_det_def flip: assms)
fix X :: "'a multiset"
have "¦eucl.det f¦ = ¦eucl.det g¦"
if eq: "image_mset f (mset_set Basis) = image_mset g (mset_set Basis)" for f g :: "'a ⇒ 'a"
proof -
obtain p where p: "p permutes Basis" "⋀x. x ∈ Basis ⟹ f x = g (p x)"
using image_mset_eq_implies_permutes[OF finite_Basis eq] by metis
have "eucl.det f = eucl.det (g ∘ p)"
by (rule eucl.det_cong) (auto simp: p)
also have "… = sign p * eucl.det g"
by (rule eucl.det_permute) fact
finally show "¦eucl.det f¦ = ¦eucl.det g¦"
by (simp add: abs_mult sign_def flip: of_int_abs)
qed
hence "∃!d. ∀g::'a ⇒ 'a. image_mset g (mset_set Basis) =
image_mset f (mset_set Basis) ⟶ ¦eucl.det g¦ = d"
by blast
from theI'[OF this, folded abs_det_eq] show ?thesis
by simp
qed
lemma abs_det: "abs_det (image_mset f (mset_set Basis)) = ¦eucl.det f¦"
by (rule abs_det_conv_det) auto
lemma abs_det_empty [simp]: "abs_det {#} = 0"
by simp
lemma representation_real: "representation {1} x = (λb. if b = 1 then x else 0)"
using representation_euclidean_space[of x] by (auto split: if_splits)
lemma det_real [simp]: "eucl.det (f :: real ⇒ real) = f 1"
unfolding eucl.det_def representation_euclidean_space by (auto simp: sign_id)
lemma det_real' [simp]: "finite_dimensional_vector_space.det scaleR {1} f = f 1"
using det_real[of f] by (simp del: det_real)
lemma det_complex: "eucl.det f = Re (f 1) * Im (f 𝗂) - Re (f 𝗂) * Im (f 1)"
proof -
have [simp]: "id ≠ Transposition.transpose 1 𝗂"
by (auto simp: Transposition.transpose_def fun_eq_iff)
have "eucl.det (f :: complex ⇒ complex) =
(∑p | p permutes {1, 𝗂}. real_of_int (sign p) * (Re (f (p 1)) * Im (f (p 𝗂))))"
unfolding eucl.det_def representation_euclidean_space
by (simp add: representation_euclidean_space Basis_complex_def )
also have "{p. p permutes {1, 𝗂}} = {id, Transposition.transpose 1 𝗂}"
by (auto simp: permutes_doubleton_iff)
also have "(∑p∈…. real_of_int (sign p) * (Re (f (p 1)) * Im (f (p 𝗂)))) =
Re (f 1) * Im (f 𝗂) - Re (f 𝗂) * Im (f 1)"
by (subst sum.insert) (auto simp: sign_id sign_swap_id fun_eq_iff intro!: exI[of _ 1])
finally show ?thesis .
qed
lemma det_pair_real:
"eucl.det f = fst (f (1, 0)) * snd (f (0, 1)) - fst (f (0, 1)) * snd (f (1, 0))" (is "_ = ?rhs")
proof -
have *: "{p. p permutes Basis} = {id, Transposition.transpose (0,1) (1::real,0::real)}"
by (auto simp: permutes_doubleton_iff Basis_pair_def)
have neq: "id ≠ Transposition.transpose (0, 1) (1::real, 0::real)"
by (auto simp: fun_eq_iff Transposition.transpose_def)
show ?thesis
unfolding eucl_det_def * neq
by (simp add: Basis_pair_def permutes_doubleton_iff neq sign_id sign_swap_id inner_prod_def)
qed
lemma abs_det_real:
"abs_det {# x::real #} = ¦x¦"
using abs_det_conv_det[of "λ_. x" "{#x#}"] unfolding det_real by simp
lemma abs_det_complex:
"abs_det {# u, v :: complex #} = ¦Re u * Im v - Re v * Im u¦"
proof (subst abs_det_conv_det[of "λb. if b = 1 then u else v"])
show "{#if b = 1 then u else v. b ∈# mset_set (Basis :: complex set)#} = {# u, v #}"
by (auto simp: Basis_complex_def)
qed (auto simp: det_complex)
end