Up to index of Isabelle/HOL/HOL-Algebra/Vector_Spaces
theory Isomorphismtheory Isomorphism
imports Dimension
begin
section{*Isomorphism*}
text{*The @{text "types"} keyword seems to be replaced by @{text "type_synonym"}
in the Isabelle 2011 release.*}
text{*The following definition of @{text vector} has been obtained from the \emph{AFP},
where a similar one is defined over @{text real}, instead of @{typ "'a"}, for defining the
Cauchy-Schwarz Inequality \url{http://afp.sourceforge.net/entries/Cauchy.shtml}.*}
text{*22-07-2011: JE: For some time I thought that many of the proofs required the vector spaces
to be non empty (not of dimension zero). This is why one can meet a lot of
premises of the type @{term "0 < n"} or about the dimension being non zero (all
these premises are now enclosed between comments). After a closer look
I could remove each of these premises and make everything general for every finite dimension.*}
types 'a vector = "(nat => 'a) * nat"
definition
ith :: "'a vector => nat => 'a"
where "ith v i = fst v i"
definition
vlen :: "'a vector => nat"
where "vlen v = snd v"
text{*Before getting into the definition of the vector space $K_n$,
we introduce a generic lemma that states that the decomposition of
an element @{term "x ∈ carrier V"} as a linear combination of
the elements of a given basis is unique.*}
text{*The lemma requires the basis @{term X} to be finite, because otherwise
there would be a linear combination of the infinite number of elements
of the basis equal to zero, but the @{term finsum} of an infinite set
is undefined, and thus we cannot complete the proof.*}
context abelian_group
begin
text{*Some previous lemmas about addition in abelian monoids.*}
lemma
add_minus_add_minus:
assumes a: "a ∈ carrier G"
and b: "b ∈ carrier G"
and c: "c ∈ carrier G"
shows "a ⊕ b \<ominus> c = a ⊕ (b \<ominus> c)"
proof -
have "a ⊕ b \<ominus> c = a ⊕ b ⊕ \<ominus> c"
using minus_eq [OF a_closed [OF a b] c] .
also have "... = a ⊕ (b ⊕ \<ominus> c)"
using a_assoc [OF a b a_inv_closed [OF c]] .
also have "... = a ⊕ (b \<ominus> c)"
unfolding minus_eq [symmetric, OF b c] ..
finally show ?thesis .
qed
lemma
minus_add_minus_minus:
assumes a: "a ∈ carrier G"
and b: "b ∈ carrier G"
and c: "c ∈ carrier G"
shows "a \<ominus> (b ⊕ c) = a \<ominus> b \<ominus> c"
proof -
have "a \<ominus> (b ⊕ c) = a ⊕ \<ominus> (b ⊕ c)"
using minus_eq [OF a a_closed [OF b c]] .
thm minus_add
also have "... = a ⊕ (\<ominus> b ⊕ \<ominus> c)"
unfolding minus_add [OF b c] ..
also have "... = a ⊕ \<ominus> b ⊕ \<ominus> c"
using a_assoc [symmetric, OF a a_inv_closed [OF b] a_inv_closed [OF c]] .
also have "... = a \<ominus> b ⊕ \<ominus> c"
unfolding minus_eq [symmetric, OF a b] ..
also have "... = a \<ominus> b \<ominus> c"
using minus_eq [symmetric, OF minus_closed [OF a b] c] .
finally show ?thesis .
qed
lemma
add_minus_add_minus_add_minus:
assumes a: "a ∈ carrier G"
and b: "b ∈ carrier G"
and c: "c ∈ carrier G"
and d: "d ∈ carrier G"
shows "a ⊕ b \<ominus> (c ⊕ d) = a \<ominus> c ⊕ (b \<ominus> d)"
proof -
have "a ⊕ b \<ominus> (c ⊕ d) = a ⊕ b ⊕ \<ominus> (c ⊕ d)"
using minus_eq [OF a_closed [OF a b] a_closed [OF c d]] .
also have "... = a ⊕ (b ⊕ \<ominus> (c ⊕ d))"
using a_assoc [OF a b a_inv_closed [OF a_closed [OF c d]]] .
also have "... = a ⊕ (b \<ominus> (c ⊕ d))"
unfolding minus_eq [symmetric, OF b a_closed [OF c d]] ..
also have "... = a ⊕ (b \<ominus> c \<ominus> d)"
unfolding minus_add_minus_minus [OF b c d] ..
also have "... = a ⊕ (b ⊕ \<ominus> c ⊕ \<ominus> d)"
unfolding minus_eq [OF minus_closed [OF b c] d]
unfolding minus_eq [OF b c] ..
also have "... = a ⊕ (\<ominus> c ⊕ b ⊕ \<ominus> d)"
unfolding a_comm [OF b a_inv_closed [OF c]] ..
also have "... = a ⊕ (\<ominus> c ⊕ (b ⊕ \<ominus> d))"
unfolding a_assoc [OF a_inv_closed [OF c] b a_inv_closed [OF d]] ..
also have "... = a ⊕ \<ominus> c ⊕ (b ⊕ \<ominus> d)"
unfolding a_assoc [OF a a_inv_closed [OF c] a_closed [OF b a_inv_closed [OF d]]] ..
also have "... = a \<ominus> c ⊕ (b \<ominus> d)"
unfolding minus_eq [OF a c]
unfolding minus_eq [OF b d] ..
finally show ?thesis .
qed
corollary add_minus_add_minus_add_minus_comm:
assumes a: "a ∈ carrier G"
and b: "b ∈ carrier G"
and c: "c ∈ carrier G"
and d: "d ∈ carrier G"
shows "a ⊕ b \<ominus> (c ⊕ d) = b \<ominus> d ⊕ (a \<ominus> c)"
proof -
have "a ⊕ b \<ominus> (c ⊕ d) = a \<ominus> c ⊕ (b \<ominus> d)"
using add_minus_add_minus_add_minus [OF a b c d] .
also have "... = (b \<ominus> d) ⊕ (a \<ominus> c)"
unfolding a_comm [OF minus_closed [OF a c] minus_closed [OF b d]] ..
finally show ?thesis .
qed
lemma finsum_minus_eq:
assumes fin_A: "finite A"
and f_PI: "f ∈ A -> carrier G"
shows "\<ominus> finsum G f A = finsum G (λx. \<ominus> f x) A"
using fin_A f_PI proof (induct)
case empty
show ?case by simp
next
case (insert a A)
have f_PI: "f ∈ A -> carrier G"
and fa: "f a ∈ carrier G"
and minus_f_PI: "(λx. \<ominus> f x) ∈ A -> carrier G"
and minus_fa: "\<ominus> f a ∈ carrier G"
using insert (4) unfolding Pi_def by simp_all
have fG: "finsum G f A ∈ carrier G"
by (rule finsum_closed [OF insert (1) f_PI])
show ?case
unfolding finsum_insert [OF insert (1, 2) f_PI, OF fa]
unfolding finsum_insert [OF insert (1, 2) minus_f_PI, OF minus_fa]
unfolding minus_add [OF fa fG]
unfolding insert.hyps (3) [OF f_PI] ..
qed
end
context vector_space
begin
text{*The following function should replace to @{term coefficients_function};
the problem with @{term coefficients_function}
is that it does not impose any condition over functions out of their domain, @{term "carrier V"};
thus, we cannot prove that two coefficient functions which are equal over their
corresponding domain (the basis @{term X}) are equal.
We have to impose an additional restriction that the
function out of its domain is equal to @{term "\<zero>\<^bsub>K\<^esub>"}*}
(*definition coefficients_function_comp :: "'b set => ('b => 'a) set"
where "coefficients_function_comp X = {f. f ∈ X -> carrier K ∧ (∀x. x∉X --> f x = \<zero>\<^bsub>K\<^esub>)}"
lemma coefficients_function_comp_is_coefficients_function:
assumes f: "f ∈ coefficients_function_comp X"
and cbX: "good_set X"
shows "f ∈ coefficients_function"
unfolding coefficients_function_def
using f (*cbX*)
unfolding coefficients_function_comp_def
unfolding good_set_def by auto
*)
end
subsection{*Definition of $\mathbb{K}^n$*}
context field
begin
text{*The following definition represents the carrier set of the vector space.
Note that the type variable is now @{typ "'a"},
so we define only the following concepts over the field of the coefficients.*}
-- "Seleccionamos un representante canónico para cada elemento, haciendo que todas
las coordenadas sean cero por encima de la dimensión del espacio vectorial"
-- "Además, debemos asegurar que la dimensión del vector, o la longitud del mismo,
sea igual al número de componenetes en el que estamos interesados; sino perderíamos
la inyectividad de algunas operaciones"
-- "Hay que tener en cuenta que en una lista de 1 elemento (por ejemplo,
los elementos del carrier de K1) nos interesa únicamente el elemento en
la posición 0, de ahí que nos interesen los elementos con vlen = n - 1;"
text{*Para los elementos en @{term "K_n_carrier A 0"} debemos observar
que su primera componente será @{term \<zero>} y su segunda componente será
también @{term "0::nat"}, lo que nos deja con un $K_0$ cuyo único
elemento es el @{term 0} de la estructura correspondiente ($K_n$).*}
definition K_n_carrier :: "'a set => nat => ('a vector) set"
where "K_n_carrier A n = {v. ((∀i<n. ith v i ∈ A)) ∧
(∀i≥n. ith v i = \<zero>) ∧ (vlen v = (n - 1))}"
lemma ith_closed:
assumes k: "k ∈ K_n_carrier A n" and i: "i ∈ {..<n}"
shows "ith k i ∈ A"
using k
unfolding K_n_carrier_def using i by fast
lemma K_n_carrier_zero:
"K_n_carrier A 0 = {v. (ith v 0 = \<zero>) ∧ (∀i>0. ith v i = \<zero>) ∧ (vlen v = 0)}"
unfolding K_n_carrier_def
by rule (auto, case_tac "i", force+)
lemma K_n_carrier_zero_ext: "K_n_carrier A 0 = {(λi. \<zero>, 0)}"
unfolding K_n_carrier_zero ith_def vlen_def
by auto (rule ext, metis gr0I)
lemma K_n_carrier_one:
"K_n_carrier A 1 = {v. ith v 0 ∈ A ∧ (∀i≥1. ith v i = \<zero>) ∧ (vlen v = 0)}"
unfolding K_n_carrier_def by auto
definition
K_n_add :: " nat => 'a vector => 'a vector => 'a vector" (infixr "⊕\<index>" 65)
where "K_n_add n = (λv w. ((λi. ith v i ⊕\<^bsub>R\<^esub> ith w i), n - 1))"
lemma K_n_add_zero:
shows "K_n_add 0 = (λv w. ((λi. ith v i ⊕\<^bsub>R\<^esub> ith w i), 0))"
using K_n_add_def [of 0] by simp
definition K_n_mult :: "nat => 'a vector => 'a vector => 'a vector"
where "K_n_mult n = (λv w. ((λi. ith v i ⊗\<^bsub>R\<^esub> ith w i), n - 1))"
lemma K_n_mult_zero:
shows "K_n_mult 0 = (λv w. ((λi. ith v i ⊗\<^bsub>R\<^esub> ith w i), 0))"
using K_n_mult_def by auto
definition K_n_zero :: "nat => 'a vector"
where "K_n_zero n = ((λi. \<zero>\<^bsub>R\<^esub>), n - 1)"
lemma K_n_zero_zero:
shows "K_n_zero 0 = ((λi. \<zero>\<^bsub>R\<^esub>), 0)"
using K_n_zero_def by auto
definition K_n_one :: "nat => 'a vector"
where "K_n_one n = ((λi. \<one>\<^bsub>R\<^esub>), n - 1)"
text{*Actually, in the following case, one should be equal to zero*}
lemma K_n_one_zero:
shows "K_n_one 0 = ((λi. \<one>\<^bsub>R\<^esub>), 0)"
using K_n_one_def by auto
text{*We are now forced to define also operations @{text K_n_mult}
and @{text K_n_one} for our \emph{abelian group} $K^n$.
This is due to the fact that the abelian group predicate in the
Algebra Library is defined over rings, and even if we have
no interest in using that operations (they are not required to
prove that an algebraic structure is an abelian group),
they must be defined somehow. In our case this is not a major problem,
since they can be defined just following the previous
definitions of @{text K_n_zero} and @{text K_n_add}.*}
definition K_n :: "nat => 'a vector ring"
where
"K_n n = (| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
lemma abelian_group_K_n:
shows "abelian_group (K_n n)"
unfolding K_n_def
proof (intro abelian_groupI)
let ?K_n = "(| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
fix x y
assume x: "x ∈ carrier ?K_n" and y: "y ∈ carrier ?K_n"
show "x ⊕\<^bsub>?K_n\<^esub> y ∈ carrier ?K_n"
using x y
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding ith_def vlen_def by auto
next
let ?K_n = "(| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
show "\<zero>\<^bsub>?K_n\<^esub> ∈ carrier ?K_n"
unfolding K_n_carrier_def
unfolding K_n_zero_def
unfolding ith_def vlen_def by auto
next
let ?K_n = "(| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
fix x y z
assume x: "x ∈ carrier ?K_n" and y: "y ∈ carrier ?K_n" and z: "z ∈ carrier ?K_n"
show "x ⊕\<^bsub>?K_n\<^esub> y ⊕\<^bsub>?K_n\<^esub> z = x ⊕\<^bsub>?K_n\<^esub> (y ⊕\<^bsub>?K_n\<^esub> z)"
using x y z
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding ith_def vlen_def
proof (auto)
assume x1: "∀i<n. fst x i ∈ carrier R" and y1: "∀i<n. fst y i ∈ carrier R"
and z1: "∀i<n. fst z i ∈ carrier R"
assume x2: "∀i≥n. fst x i = \<zero>" and y2: "∀i≥n. fst y i = \<zero>" and z2: "∀i≥n. fst z i = \<zero>"
show "(λi. fst x i ⊕ fst y i ⊕ fst z i) = (λi. fst x i ⊕ (fst y i ⊕ fst z i))"
proof (rule ext)
fix i
show "fst x i ⊕ fst y i ⊕ fst z i = fst x i ⊕ (fst y i ⊕ fst z i)"
proof (cases "i < n")
case True
show ?thesis using x1 y1 z1 using True by (metis a_assoc)
next
case False
show ?thesis using x2 y2 z2 using False
by (metis add.one_closed cring.cring_simprules(16)
is_cring less_or_eq_imp_le linorder_neqE_nat)
qed
qed
qed
next
let ?K_n = "(| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
fix x y
assume x: "x ∈ carrier ?K_n" and y: "y ∈ carrier ?K_n"
show "x ⊕\<^bsub>?K_n\<^esub> y = y ⊕\<^bsub>?K_n\<^esub> x"
using x y
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding ith_def vlen_def apply auto
proof (rule ext)
fix i
assume x1: "∀i<n. fst x i ∈ carrier R" and y1: "∀i<n. fst y i ∈ carrier R"
assume x2: "∀i≥n. fst x i = \<zero>" and y2: "∀i≥n. fst y i = \<zero>"
show "fst x i ⊕ fst y i = fst y i ⊕ fst x i"
proof (cases "i < n")
case True
show ?thesis using x1 y1 using True by (metis a_comm)
next
case False
show ?thesis using x2 y2 using False
by (metis less_or_eq_imp_le linorder_neqE_nat)
qed
qed
next
let ?K_n = "(| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
fix x
assume x: "x ∈ carrier ?K_n"
show "\<zero>\<^bsub>?K_n\<^esub> ⊕\<^bsub>?K_n\<^esub> x = x"
using x
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding K_n_zero_def
unfolding ith_def vlen_def
apply auto
apply (subst (2) surjective_pairing [of x])
apply simp
apply (rule ext)
by (metis add.l_one add.one_closed le_eq_less_or_eq linorder_neqE_nat)
next
let ?K_n = "(| carrier = K_n_carrier (carrier R) n,
mult = (λv w. K_n_mult n v w),
one = K_n_one n,
zero = K_n_zero n,
add = (λv w. K_n_add n v w)|)),"
fix x
assume x: "x ∈ carrier ?K_n"
show "∃y∈carrier ?K_n. y ⊕\<^bsub>?K_n\<^esub> x = \<zero>\<^bsub>?K_n\<^esub>"
apply (rule bexI [of _ "((λi. \<ominus> (fst x i)), n - Suc 0)"])
using x
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding K_n_zero_def
unfolding ith_def vlen_def
apply auto
apply (rule ext)
by (metis add.l_inv add.one_closed le_eq_less_or_eq linorder_neqE_nat)
qed
corollary abelian_monoid_K_n:
shows "abelian_monoid (K_n n)"
using abelian_group_K_n [of n]
unfolding abelian_group_def ..
text{*We are later to consider @{term K_n} like one abelian group over which @{term R}
gives place to a vector space. We must define first the scalar product between both structures.*}
definition
K_n_scalar_product :: "'a => 'a vector => 'a vector"
(infixr "\<odot>" 65)
where "a \<odot> b = (λn::nat. a ⊗\<^bsub>R\<^esub> ith b n, vlen b)"
lemma K_n_scalar_product_closed:
assumes a: "a ∈ carrier R"
and b: "b ∈ carrier (K_n n)"
shows "a \<odot> b ∈ carrier (K_n n)"
unfolding K_n_scalar_product_def
using a b
unfolding ith_def vlen_def K_n_def K_n_carrier_def by simp
lemma field_R: "field R"
by (metis cring_fieldI field_Units)
lemma
vector_space_K_n:
shows "vector_space R (K_n n) (op \<odot>)"
unfolding K_n_def
proof (intro vector_spaceI)
show "field R" using field_R .
show "abelian_group (|carrier = K_n_carrier (carrier R) n,
mult = K_n_mult n, one = K_n_one n,
zero = K_n_zero n, add = K_n_add n|)),"
using abelian_group_K_n [of n]
unfolding K_n_def .
next
let ?K_n = "(|carrier = K_n_carrier (carrier R) n,
mult = K_n_mult n, one = K_n_one n,
zero = K_n_zero n, add = K_n_add n|)),"
fix x :: "'a vector" and a :: "'a"
assume x: "x ∈ carrier ?K_n"
assume a: "a ∈ carrier R"
show "a \<odot> x ∈ carrier ?K_n"
using x a
unfolding K_n_scalar_product_def
unfolding K_n_carrier_def
unfolding vlen_def ith_def by simp
next
let ?K_n = "(|carrier = K_n_carrier (carrier R) n,
mult = K_n_mult n, one = K_n_one n,
zero = K_n_zero n, add = K_n_add n|)),"
fix x a b
assume x: "x ∈ carrier ?K_n"
assume a: "a ∈ carrier R" and b: "b ∈ carrier R"
show "a ⊗ b \<odot> x = a \<odot> b \<odot> x"
using x a b
unfolding K_n_scalar_product_def
unfolding K_n_carrier_def
unfolding vlen_def ith_def apply auto apply (rule ext)
by (metis add.one_closed le_refl linorder_neqE_nat m_assoc nat_less_le)
next
let ?K_n = "(|carrier = K_n_carrier (carrier R) n,
mult = K_n_mult n, one = K_n_one n,
zero = K_n_zero n, add = K_n_add n|)),"
fix x
assume x: "x ∈ carrier ?K_n"
show "\<one> \<odot> x = x"
using x
unfolding K_n_scalar_product_def
unfolding K_n_carrier_def
unfolding vlen_def ith_def
apply (subst (3) surjective_pairing [of x])
apply auto
apply (rule ext)
by (metis add.one_closed l_one less_or_eq_imp_le linorder_neqE_nat)
next
let ?K_n = "(|carrier = K_n_carrier (carrier R) n,
mult = K_n_mult n, one = K_n_one n,
zero = K_n_zero n, add = K_n_add n|)),"
fix x y a
assume x: "x ∈ carrier ?K_n" and y: "y ∈ carrier ?K_n"
assume a: "a ∈ carrier R"
show "a \<odot> (x ⊕\<^bsub>?K_n\<^esub> y) = (a \<odot> x) ⊕\<^bsub>?K_n\<^esub> (a \<odot> y)"
using x y a
unfolding K_n_scalar_product_def
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding vlen_def ith_def
apply auto
apply (rule ext)
by (metis add.one_closed less_or_eq_imp_le linorder_neqE_nat r_distr)
next
let ?K_n = "(|carrier = K_n_carrier (carrier R) n,
mult = K_n_mult n, one = K_n_one n,
zero = K_n_zero n, add = K_n_add n|)),"
fix x a b
assume x: "x ∈ carrier ?K_n"
assume a: "a ∈ carrier R" and b: "b ∈ carrier R"
show "(a ⊕ b) \<odot> x = (a \<odot> x) ⊕\<^bsub>?K_n\<^esub> (b \<odot> x)"
using x a b
unfolding K_n_scalar_product_def
unfolding K_n_carrier_def
unfolding K_n_add_def
unfolding vlen_def ith_def apply auto apply (rule ext)
by (metis add.one_closed l_distr le_eq_less_or_eq linorder_neqE_nat)
qed
subsection{*Canonical basis of $\mathbb{K}^n$:*}
text{*In the following section we introduce the elements that generate
the canonical basis of the vector space @{term "K_n n"} and prove some
properties of them.*}
text{*The elements of the canonical basis of @{term "K_n"} are the following ones:*}
definition x_i :: "nat => nat => 'a vector"
where "x_i j n = ((λi. if i = j then \<one> else \<zero>), n - 1)"
text{*The elements @{term "x_i"} are part of the @{term "carrier (K_n n)"}.*}
lemma
x_i_closed:
assumes j_l_n: "j < n"
shows "x_i j n ∈ carrier (K_n n)"
unfolding K_n_def
unfolding K_n_carrier_def
unfolding ith_def vlen_def x_i_def using j_l_n by auto
text{*Any two elements of the basis are different:*}
lemma x_i_ne_x_j:
assumes i_ne_j: "i ≠ j"
shows "x_i i n ≠ x_i j n"
proof (rule ccontr, simp)
assume eq: "x_i i n = x_i j n"
have "fst (x_i i n) i = \<one>"
unfolding x_i_def by simp
moreover have "fst (x_i j n) i = \<zero>"
unfolding x_i_def using i_ne_j by force
ultimately show False using eq by simp
qed
text{*In the following lemma we can even omit the premise of @{term i} being
smaller than @{term n}, so the result is also true for vectors which are not
part of the canonical basis. It claims that an element of the canonical
basis is not equal to @{term "\<zero>\<^bsub>K_n n\<^esub>"}*}
lemma x_i_ne_zero:
shows "x_i i n ≠ \<zero>\<^bsub>K_n n\<^esub>"
proof (rule ccontr, simp)
assume eq: "x_i i n = \<zero>\<^bsub>K_n n\<^esub>"
have "fst (x_i i n) i = \<one>"
unfolding x_i_def by simp
moreover have "fst (\<zero>\<^bsub>K_n n\<^esub>) i = \<zero>"
unfolding K_n_def K_n_zero_def by force
ultimately show False using eq by simp
qed
end
context vector_space
begin
(*lemma
coefficients_function_Pi:
assumes x: "x ∈ carrier V"
and cf_f: "f ∈ coefficients_function"
shows "f x ∈ carrier K"
unfolding coefficients_function_def
by (metis cf_f fx_in_K x)
*)
lemma
coefficients_function_Pi:
assumes x: "x ∈ carrier V"
and cf_f: "f ∈ coefficients_function A"
shows "f x ∈ carrier K"
using cf_f
unfolding coefficients_function_def by auto
end
context abelian_group
begin
lemma
finsum_twice:
assumes f: "f ∈ {i,j} -> carrier G"
and i_ne_j: "i ≠ j"
shows "finsum G f {i, j} = f i ⊕ f j"
proof -
have "finsum G f {i, j} = f i ⊕ finsum G f {j}"
apply (rule finsum_insert) using i_ne_j f by auto
also have "... = f i ⊕ (f j ⊕ finsum G f {})"
using finsum_insert [of "{}" j f] using f by fastsimp
also have "... = f i ⊕ f j"
unfolding finsum_empty using f by force
finally show ?thesis .
qed
end
context comm_monoid
begin
lemma mult_if:
shows "(λk. x ⊗ (if k = i then y else z)) = (λk. if k = i then x ⊗ y else x ⊗ z)"
by (rule ext, auto)
end
lemma
fun_eq_contr:
assumes fg: "f = g"
and x: "f x ≠ g x"
shows False by (metis fg x)
context abelian_monoid
begin
lemma
finsum_singleton_set:
assumes f: "f a ∈ carrier G"
shows "finsum G f {a} = f a"
using finsum_insert [of "{}" a f]
using finsum_empty using f by force
end
context field
begin
lemma comm_monoid_R: "comm_monoid R" by intro_locales
lemma abelian_monoid_R: "abelian_monoid R" by intro_locales
text{*Some previous about the linear independece
of the elements of the canonical basis:*}
lemma x_i_li:
assumes j_l_n: "j < n"
shows "vector_space.linear_independent R (K_n n) (op \<odot>) {(x_i j n)}"
proof (unfold vector_space.linear_independent_def [OF vector_space_K_n], intro conjI)
interpret vector_space R "K_n n" "op \<odot>" using vector_space_K_n .
show "good_set {x_i j n}"
unfolding good_set_def
using x_i_closed [OF j_l_n] by blast
show "∀f. f ∈ coefficients_function (carrier (K_n n)) ∧
linear_combination f {x_i j n} = \<zero>\<^bsub>K_n n\<^esub> --> (∀x∈{x_i j n}. f x = \<zero>)"
proof (rule+, erule conjE)
fix f x
assume f: "f ∈ coefficients_function (carrier (K_n n))"
and f1: "linear_combination f {x_i j n} = \<zero>\<^bsub>K_n n\<^esub>"
and "x ∈ {x_i j n}"
hence x: "x = x_i j n" by fast
have " \<zero>\<^bsub>K_n n\<^esub> = linear_combination f {x_i j n}"
using f1 [symmetric] .
also have "linear_combination f {x_i j n} = f (x_i j n) \<odot> (x_i j n)"
unfolding linear_combination_def
apply (rule abelian_monoid.finsum_singleton_set [OF abelian_monoid_K_n [of n]])
apply (rule K_n_scalar_product_closed)
using f x_i_closed [OF j_l_n]
unfolding coefficients_function_def by fast+
finally have zero: "\<zero>\<^bsub>K_n n\<^esub> = f (x_i j n) \<odot> (x_i j n)" .
show "f x = \<zero>"
proof (rule mult_zero_uniq [OF x_i_closed [OF j_l_n]])
show "x_i j n ≠ \<zero>\<^bsub>K_n n\<^esub>"
by (rule x_i_ne_zero [of j n])
show "f x ∈ carrier R" unfolding x using f x_i_closed [OF j_l_n]
unfolding coefficients_function_def by fast+
show "f x \<odot> x_i j n = \<zero>\<^bsub>K_n n\<^esub>" unfolding x by (rule zero [symmetric])
qed
qed
qed
text{*Any two different elements of the canonical basis are linearly independent:*}
lemma x_i_x_j_li:
assumes j_l_n: "j < n"
and i_l_n: "i < n"
and i_ne_j: "i ≠ j"
shows "vector_space.linear_independent R (K_n n) (op \<odot>) {(x_i i n), (x_i j n)}"
proof -
interpret vector_space R "K_n n" "op \<odot>" using vector_space_K_n .
show ?thesis
proof (unfold linear_independent_def, rule)
show "vector_space.good_set (K_n n) {x_i i n, x_i j n}"
unfolding good_set_def
using x_i_closed [OF j_l_n] x_i_closed [OF i_l_n] by blast
show "∀f. f ∈ coefficients_function (carrier (K_n n)) ∧
linear_combination f {x_i i n, x_i j n} = \<zero>\<^bsub>K_n n\<^esub> --> (∀x∈{x_i i n, x_i j n}. f x = \<zero>)"
proof auto
fix f
assume f: "f ∈ coefficients_function (carrier (K_n n))"
and lc: "linear_combination f {x_i i n, x_i j n} = \<zero>\<^bsub>K_n n\<^esub>"
have fxii: "f (x_i i n) ∈ carrier R" and fxij: "f (x_i j n) ∈ carrier R"
using fx_in_K [OF x_i_closed [OF i_l_n] f]
using fx_in_K [OF x_i_closed [OF j_l_n] f] by fast+
show "f (x_i i n) = \<zero>"
proof (rule ccontr)
assume xii: "f (x_i i n) ≠ \<zero>"
have "\<zero>\<^bsub>K_n n \<^esub>= linear_combination f {x_i i n, x_i j n}"
by (rule lc [symmetric])
also have "linear_combination f {x_i i n, x_i j n} =
(f (x_i i n) \<odot> (x_i i n)) ⊕\<^bsub>K_n n\<^esub> (f (x_i j n) \<odot> (x_i j n))"
unfolding linear_combination_def
apply (rule finsum_twice [of "(λi. f i \<odot> i)" "x_i i n" "x_i j n"])
using fx_x_in_V [OF _ f]
using x_i_closed [OF i_l_n] x_i_closed [OF j_l_n]
using x_i_ne_x_j [OF i_ne_j, of n]
unfolding x_i_def by simp_all
also have "... = ((λk. if k = i then f (x_i i n) else \<zero>) , n - 1) ⊕\<^bsub>n\<^esub>
((λk. if k = j then f (x_i j n) else \<zero>), n - 1)"
apply (subst (2 4) x_i_def)
apply (unfold K_n_scalar_product_def)
unfolding ith_def vlen_def apply simp
unfolding K_n_def apply auto
unfolding comm_monoid.mult_if [OF comm_monoid_R]
unfolding r_one [OF fxii] r_one [OF fxij] r_null [OF fxii] r_null [OF fxij] ..
also have "... = ((λk. if k = i then f (x_i i n)
else if k = j then f (x_i j n) else \<zero>) , n - 1)"
unfolding K_n_add_def ith_def
unfolding fst_conv
apply rule+ using i_ne_j apply auto
unfolding abelian_monoid.r_zero [OF abelian_monoid_R fxii]
unfolding abelian_monoid.l_zero [OF abelian_monoid_R fxij] by fast+
finally have "\<zero>\<^bsub>K_n n\<^esub> = ((λk. if k = i then f (x_i i n)
else if k = j then f (x_i j n) else \<zero>) , n - 1)" by fast
thus False
unfolding K_n_def
unfolding K_n_zero_def
using xii i_ne_j
apply simp
apply (rule fun_eq_contr [of "(λi. \<zero>)" "(λk. if k = i
then f (x_i i n) else if k = j then f (x_i j n) else \<zero>)" i])
by simp_all
qed
next
fix f
assume f: "f ∈ coefficients_function (carrier (K_n n))"
and lc: "linear_combination f {x_i i n, x_i j n} = \<zero>\<^bsub>K_n n\<^esub>"
have fxii: "f (x_i i n) ∈ carrier R" and fxij: "f (x_i j n) ∈ carrier R"
using fx_in_K [OF x_i_closed [OF i_l_n] f]
using fx_in_K [OF x_i_closed [OF j_l_n] f] by fast+
show "f (x_i j n) = \<zero>"
proof (rule ccontr)
assume xii: "f (x_i j n) ≠ \<zero>"
have "\<zero>\<^bsub>K_n n \<^esub>= linear_combination f {x_i i n, x_i j n}"
by (rule lc [symmetric])
also have "linear_combination f {x_i i n, x_i j n} =
(f (x_i i n) \<odot> (x_i i n)) ⊕\<^bsub>K_n n\<^esub> (f (x_i j n) \<odot> (x_i j n))"
unfolding linear_combination_def
apply (rule finsum_twice [of "(λi. f i \<odot> i)" "x_i i n" "x_i j n"])
using fx_x_in_V [OF _ f]
using x_i_closed [OF i_l_n] x_i_closed [OF j_l_n]
using x_i_ne_x_j [OF i_ne_j, of n]
unfolding x_i_def by simp_all
also have "... = ((λk. if k = i then f (x_i i n) else \<zero>) , n - 1)
⊕\<^bsub>n\<^esub> ((λk. if k = j then f (x_i j n) else \<zero>), n - 1)"
apply (subst (2 4) x_i_def)
apply (unfold K_n_scalar_product_def)
unfolding ith_def vlen_def apply simp
unfolding K_n_def apply auto
unfolding comm_monoid.mult_if [OF comm_monoid_R]
unfolding r_one [OF fxii] r_one [OF fxij] r_null [OF fxii] r_null [OF fxij] ..
also have "... = ((λk. if k = i then f (x_i i n)
else if k = j then f (x_i j n) else \<zero>) , n - 1)"
unfolding K_n_add_def ith_def
unfolding fst_conv
apply rule+ using i_ne_j apply auto
unfolding abelian_monoid.r_zero [OF abelian_monoid_R fxii]
abelian_monoid.l_zero [OF abelian_monoid_R fxij] by fast+
finally have "\<zero>\<^bsub>K_n n\<^esub> = ((λk. if k = i then f (x_i i n)
else if k = j then f (x_i j n) else \<zero>) , n - 1)" by fast
thus False
unfolding K_n_def
unfolding K_n_zero_def
using xii i_ne_j
apply simp
apply (rule fun_eq_contr [
of "(λi. \<zero>)"
"(λk. if k = i then f (x_i i n) else if k = j then f (x_i j n) else \<zero>)" j])
by simp_all
qed
qed
qed
qed
text{*We did not find a better way to define the elements of the canonical basis
than accumulating them iteratively. In order to define them as a range,
from @{term "(x_i 0 n)"} up to @{term "(x_i (n - 1) n)"},
the underlying type, in this case @{typ "'a vector"}, should be
of sort ``order'' (which in general is not, only the elements of the basis
have some notion of order.)*}
text{*The following fuction iteratively joins all the elements of the
form @{term "x_i k n"} in order to create the canonical basis of @{term "K_n n"}.*}
text{*We have considered as a special case the situation where both indexes are
equal to @{term "0::nat"}. This case will give us the basis
of @{term "K_n 0"}, which is the empty set. Note that a linear
combination over an empty set is equal to @{term "(λi. \<zero>\<^bsub>K\<^esub>, 0::nat)"},
which is the only element in @{term "carrier (K_n 0)"}.*}
fun canonical_basis_acc :: "nat => nat => 'a vector set"
where
"canonical_basis_acc 0 0 = {}"
| "canonical_basis_acc 0 n = {x_i 0 n}"
| "canonical_basis_acc (Suc i) n
= (if (Suc i < n) then
insert (x_i (Suc i) n) (canonical_basis_acc i n) else {})"
text{*We now prove some lemmas trying to establish the relation between
the elements of the form @{term "x_i i n"} and the ones in @{term "canonical_basis_acc"}.*}
lemma
finite_canonical_basis_acc:
shows "finite (canonical_basis_acc k n)"
by (induct k, induct n, auto)
lemma
canonical_basis_acc_closed:
assumes i_l_j: "i < j"
shows "canonical_basis_acc i j ⊆ carrier (K_n j)"
using i_l_j using x_i_closed by (induct i, induct j, auto)
text{*The canonical basis in dimension @{term "n::nat"} is given
by all elements ranging from @{term "x_i 0 n"} up to
@{term "x_i (n - 1) n"}*}
definition canonical_basis_K_n :: "nat => 'a vector set" where
"canonical_basis_K_n n = canonical_basis_acc (n - 1) n"
lemma
canonical_basis_acc_insert:
assumes j_l_k: "j < k"
and k_l_n: "k < n"
shows "x_i k n ∉ canonical_basis_acc j n"
using j_l_k k_l_n proof (induct j)
case 0
show ?case
unfolding canonical_basis_acc.simps
using "0.prems" (1) using x_i_ne_x_j [of 0 k n] by (cases n, auto)
next
case (Suc j)
show ?case
proof (cases "j < k")
case True
show ?thesis
apply (subst canonical_basis_acc.simps)
using Suc.hyps [OF True Suc.prems (2)]
using Suc.prems
using x_i_ne_x_j [of "Suc j" k n]
using x_i_ne_x_j [of j k n] by force
next
case False
with Suc.prems have False by linarith
thus ?thesis by fast
qed
qed
lemma
card_canonical_basis_acc:
assumes k_le_n: "k < n"
shows "card (canonical_basis_acc k n) = Suc k"
using k_le_n
proof (induct k)
case 0
show ?case using 0 by (cases n, auto)
next
case (Suc k)
have k_l_n: "k < n" using Suc.prems by presburger
show ?case
apply (subst canonical_basis_acc.simps)
using Suc.prems
using canonical_basis_acc_insert [OF _ Suc.prems, of k]
using card.insert [OF finite_canonical_basis_acc [of k n],
of "x_i (Suc k) n"]
using Suc.hyps [OF k_l_n] by simp
qed
end
lemma
n_minus_one_l_n:
assumes n_g_0: "0 < n"
shows "n - (1::nat) < n"
by (metis assms diff_Suc_1 gr0_implies_Suc lessI)
context field
begin
text{*The following lemma is true for dimension @{term "0::nat"}
thanks to the special case
@{thm canonical_basis_acc.simps (1)} previously introduced:*}
lemma
canonical_basis_K_n_closed:
(*assumes n_g_0: "0 < n"*)
shows "canonical_basis_K_n n ⊆ carrier (K_n n)"
proof (cases n)
case 0
show ?thesis
unfolding 0
unfolding canonical_basis_K_n_def by simp
next
case (Suc n)
show ?thesis
unfolding Suc canonical_basis_K_n_def
by (rule canonical_basis_acc_closed [OF n_minus_one_l_n], fast)
qed
text{*The following lemma is true for dimension @{term "0::nat"}
thanks to the special case
@{thm canonical_basis_acc.simps (1)[no_vars]} previously introduced:*}
lemma
card_canonical_basis_K_n:
(*assumes n_g_0: "0 < n"*)
shows "card (canonical_basis_K_n n) = n"
proof (cases n)
case 0
show ?thesis unfolding 0
unfolding canonical_basis_K_n_def by simp
next
case (Suc n)
show ?thesis unfolding Suc
unfolding canonical_basis_K_n_def
using card_canonical_basis_acc [OF n_minus_one_l_n [of "Suc n"]] by fastsimp
qed
text{*The following lemma does not even require to have a dimension greater than @{term "0::nat"}.*}
lemma
finite_canonical_basis_K_n:
(*assumes n_g_0: "0 < n"*)
shows "finite (canonical_basis_K_n n)"
by (metis canonical_basis_K_n_def finite_canonical_basis_acc)
lemma
canonical_basis_acc_insert2:
assumes j_le_k: "j ≤ k"
and k_l_n: "k < n"
shows "x_i j n ∈ canonical_basis_acc k n"
using j_le_k k_l_n proof (induct k)
case 0
show ?case using "0.prems" by (cases n, auto)
next
case (Suc k)
show ?case
proof (cases "j = Suc k")
case False
hence j_le_k: "j ≤ k" using Suc.prems (1) by presburger
have k_l_n: "k < n" using Suc.prems (2) by presburger
show ?thesis
using Suc.hyps [OF j_le_k k_l_n]
using Suc.prems (2) by simp
next
case True
show ?thesis
apply (subst canonical_basis_acc.simps)
using True
using Suc.prems (2)
using x_i_ne_x_j [of k "Suc k" n] by (cases k, auto)
qed
qed
lemma
canonical_basis_K_n_elements:
assumes (*n_g_0: "0 < n"
and*) j_in_n: "j ∈ {..<n}"
shows "x_i j n ∈ canonical_basis_K_n n"
proof (cases n)
case 0
show ?thesis using j_in_n unfolding 0 by fast
next
case (Suc n)
show ?thesis
using j_in_n
unfolding Suc
unfolding canonical_basis_K_n_def
using canonical_basis_acc_insert2 [of j "Suc n - 1" "Suc n"] by simp
qed
lemma
canonical_basis_K_n_good_set:
(*assumes n_g_0: "0 < n"*)
shows "vector_space.good_set (K_n n) (canonical_basis_K_n n)"
proof (unfold vector_space.good_set_def [OF vector_space_K_n ], rule)
show "finite (canonical_basis_K_n n)"
unfolding canonical_basis_K_n_def
by (rule finite_canonical_basis_acc [of "n - 1" n])
show "canonical_basis_K_n n ⊆ carrier (K_n n)"
by (rule canonical_basis_K_n_closed)
qed
end
text{*JE: I have moved this definition to @{text Finite_Vector_Space}, so I remove
it from here. This is to be checked with the other files.*}
(*context vector_space
begin
definition span :: "'b set => 'b set"
where "span A = {x. ∃g∈ coefficients_function. x = linear_combination g A}"
end*)
subsection{*Theorem on bijection*}
context abelian_monoid
begin
text{*We need to prove the following lemma which is a generic version
of the theorem @{text finsum_cong}: *}
text{*@{thm finsum_cong[no_vars]} in the case where finite sums are
defined over sets of different type, but isomorphic (in
@{text finsum_cong} only the case where
both sets of both finite sums are equal is considered).*}
lemma finsum_cong'':
assumes fB: "finite B"
and bb: "bij_betw h B A"
and f: "f : A -> carrier G" and g: "g : B -> carrier G"
and eq: "(!!x. x ∈ B =simp=> g x = f (h x))"
shows "finsum G f A = finsum G g B"
proof -
have "finsum G g B = finsum G (f o h) B"
by (rule finsum_cong, simp_all add: g) (rule eq)
also have "... = (\<Oplus>x∈B. f (h x))"
proof (rule finsum_cong)
show "B = B" ..
show "!!i. i ∈ B =simp=> (f o h) i = f (h i)" by simp
show "(f o h ∈ B -> carrier G) = True"
using bij_betw_imp_funcset [OF bb] using f by auto
qed
also have "... = finsum G f (h ` B)"
proof (rule finsum_reindex [symmetric])
show "finite B" by fact
show "f ∈ h ` B -> carrier G"
using f using bij_betw_imp_funcset [OF bb] by auto
show "inj_on h B" using bb unfolding bij_betw_def by fast
qed
also have "... = finsum G f A"
proof (rule finsum_cong)
show "h `B = A" using bb unfolding bij_betw_def by fast
show "(f ∈ A -> carrier G) = True" using f by fast
show "!!i. i ∈ A =simp=> f i = f i" by simp
qed
finally show ?thesis by simp
qed
end
lemma n_notin_lessThan_n: "(n::nat) ∉ {..<n}"
by (metis lessThan_iff less_not_refl3)
context field
begin
lemma
snd_in_carrier:
assumes x: "x ∈ carrier (K_n n)"
shows "snd x = n - 1"
using x
unfolding K_n_def K_n_carrier_def unfolding vlen_def by auto
text{*The following lemma gives a different representation of the elements of @{term "K_n n"};
this representation will be later used to prove that the elements of @{term "K_n n"}
can be expressed as linear combinations of the elements of @{term "canonical_basis_K_n n"}.*}
lemma
x_in_carrier:
assumes x: "x ∈ carrier (K_n n)"
shows "x = (λi. if i ∈ {..<n} then fst x i else \<zero>, n - 1)"
using x
unfolding K_n_def K_n_carrier_def
unfolding ith_def vlen_def
apply (subst surjective_pairing)
unfolding snd_in_carrier [OF x] apply simp
apply (rule ext)
by (metis less_Suc_eq_le not_less_eq)
text{*The following lemma was later unused; every element can be ``embedded'' into
a smaller dimension by means of ``forgetful'' function (we forget the last
position of the vector).*}
lemma
K_n_carrier_embed:
assumes x: "x ∈ carrier (K_n (Suc k))"
shows "((λn. if n ∈ {..<k} then fst x n else \<zero>), k - 1) ∈ carrier (K_n k)"
using x
unfolding K_n_def K_n_carrier_def ith_def vlen_def by auto
text{*Functions with only a single nonzero element can be expressed as
scalar products of @{term "x_i"} elements.*}
lemma
singleton_function_x_i:
assumes x: "x ∈ carrier R"
shows "(λi. if i = j then x else \<zero>, n - 1) = x \<odot> x_i j n"
unfolding K_n_scalar_product_def
unfolding x_i_def ith_def vlen_def fst_conv snd_conv
apply (rule, rule conjI)
apply (rule ext) using x by auto
text{*The following lemma is rather important, since it shows how to express any element in
@{term "carrier (K_n k)"} in a canonical way: it proves that any element in @{term "carrier (K_n k)"}
can be expressed as a finite sum of the elements @{term "x_i j k"}.*}
text{*It is important to note that in the proof we have
introduced an extra natural variable @{term "n"}, with @{term "n≤k"},
which permits to prove the result by induction in @{term "n"} over the
field @{term "K_n k"}.*}
text{*If we do not use the extra variable @{term "n"} and we apply induction directly over @{term "k"}, the
induction step will produce two different algebraic structures, @{term "K_n k"}, where the property holds, and
@{term "K_n (Suc k)"}, where the property must be proved, but then the induction hypothesis cannot be used.*}
lemma
lambda_finsum:
assumes cl: "∀i∈{..<n}. x i ∈ carrier R"
and n_le_k: "n ≤ k"
shows "(λi. if i ∈ {..<n} then x i else \<zero>, k - 1) =
finsum (K_n k) (λi. x i \<odot> x_i i k) {..<n}"
using cl n_le_k proof (induct n)
case 0
show ?case
unfolding lessThan_0
unfolding abelian_monoid.finsum_empty [OF abelian_monoid_K_n
[of k]]
unfolding K_n_def K_n_zero_def by simp
next
case (Suc n)
have prem: "∀i∈{..<n}. x i ∈ carrier R" and prem2: "n ≤ k"
and x_n: "x n ∈ carrier R"
and hypo: "(λi. if i ∈ {..<n} then x i else \<zero>, k - 1)
= (\<Oplus>\<^bsub>K_n k\<^esub>i∈{..<n}. x i \<odot> x_i i k)"
using Suc.prems Suc.hyps by simp_all
show ?case
proof -
have "(\<Oplus>\<^bsub>K_n k\<^esub>i∈{..<Suc n}. x i \<odot> x_i i k)
= (\<Oplus>\<^bsub>K_n k\<^esub>i∈(insert n {..<n}). x i \<odot> x_i i k)"
unfolding lessThan_Suc ..
also have "... = (x n \<odot> x_i n k)
⊕\<^bsub>K_n k\<^esub> (\<Oplus>\<^bsub>K_n k\<^esub>i∈{..<n}. x i \<odot> x_i i k)"
proof (rule abelian_monoid.finsum_insert
[OF abelian_monoid_K_n])
show "finite {..<n}" by simp
show "n ∉ {..<n}" by simp
show "(λi. x i \<odot> x_i i k) ∈ {..<n} -> carrier (K_n k)"
proof
fix xa assume xa: "xa ∈ {..<n}"
show "x xa \<odot> x_i xa k ∈ carrier (K_n k)"
unfolding K_n_def K_n_carrier_def
unfolding K_n_scalar_product_def ith_def vlen_def x_i_def
using xa prem Suc.prems (2) by fastsimp
qed
show "x n \<odot> x_i n k ∈ carrier (K_n k)"
unfolding K_n_def K_n_carrier_def
unfolding K_n_scalar_product_def ith_def vlen_def x_i_def
using Suc.prems (1) Suc.prems (2) by simp
qed
also have "... = (x n \<odot> x_i n k)
⊕\<^bsub>K_n k\<^esub> (λi. if i ∈ {..<n} then x i else \<zero>, k - 1)"
unfolding Suc.hyps [symmetric, OF prem prem2] ..
also have "... = (λi. if i = n then x n else \<zero>, k - 1)
⊕\<^bsub>K_n k\<^esub> (λi. if i ∈ {..<n} then x i else \<zero>, k - 1)"
unfolding x_i_def [of n k]
unfolding K_n_scalar_product_def ith_def
vlen_def fst_conv snd_conv
unfolding mult_if unfolding r_null [OF x_n] r_one [OF x_n] ..
also have "... = (λi. (if i = n then x n else \<zero>)
⊕ (if i < n then x i else \<zero>), k - Suc 0)"
unfolding K_n_def K_n_add_def ith_def by simp
also have "... = ((λi. if i < (Suc n) then x i else \<zero>), k - 1)"
proof (rule, intro conjI)
show "k - Suc 0 = k - 1" by simp
show "(λi. (if i = n then x n else \<zero>)
⊕ (if i < n then x i else \<zero>)) =
(λi. if i < Suc n then x i else \<zero>)"
proof (rule ext)
fix i :: nat
show "(if i = n then x n else \<zero>)
⊕ (if i < n then x i else \<zero>) =
(if i < Suc n then x i else \<zero>)"
proof (cases "i < Suc n")
case False
thus ?thesis by simp
next
case True
show ?thesis using True using Suc.prems (1)
by (cases "i = n", auto)
qed
qed
qed
finally show ?thesis by simp
qed
qed
text{*Now, as a corollary of the previous result, we obtain that any
element of @{term "K_n n"} can be expressed as a finite sum of the
elements of the form @{term "x_i j n"}.*}
lemma lambda_finsum_n:
assumes cl: "∀i∈{..<n}. x i ∈ carrier R"
shows "(λi. if i ∈ {..<n} then x i else \<zero>, n - 1) =
finsum (K_n n) (λi. x i \<odot> x_i i n) {..<n}"
using lambda_finsum [OF cl, of n] by fast
text{*Finally, we get the lemma that states tha any element of the set
@{term "K_n_carrier n"} is a linear combination of elements of
@{term "canonical_basis_K_n n"}:*}
lemma
K_n_carrier_finsum_x_i:
assumes x: "x ∈ carrier (K_n n)"
shows "x = finsum (K_n n) (λj. fst x j \<odot> x_i j n) {..<n}"
apply (subst x_in_carrier [OF x])
apply (rule lambda_finsum_n)
using x unfolding K_n_def K_n_carrier_def ith_def vlen_def
by force
subsection{*Bijection between basis:*}
text{*In the following lemmas we try to establish an explicit bijection between the sets
@{term X}, which is a basis of @{term V}, and the set @{term "canonical_basis_K_n n"}. This bijection
will be later extended, by linearity, to a bijection between @{term "carrier V"} and @{term "carrier (K_n n)"}*}
lemma canonical_basis_acc_eq_x_i:
assumes x: "x ∈ canonical_basis_acc k n"
and k_l_n: "k < n"
shows "∃j∈{..<Suc k}. x_i j n = x"
using x k_l_n
proof (induct k)
case 0 thus ?case unfolding canonical_basis_acc.simps by (cases n, auto)
next
case (Suc k)
show ?case
proof (cases "x = x_i (Suc k) n")
case False
have k_l_n: "k < n" and cb: "x ∈ canonical_basis_acc k n"
and hypo: "∃j∈{..<(Suc k)}. x_i j n = x"
using Suc.prems Suc.hyps False by simp_all
thus ?thesis by fastsimp
next
case True
show ?thesis
using True by fast
qed
qed
corollary
canonical_basis_acc_isom_x_i:
assumes x: "x ∈ canonical_basis_acc k n"
and k_l_n: "k < n"
shows "∃!j∈{..<Suc k}. x = x_i j n"
proof -
obtain j :: nat where j: "j ∈ {..<Suc k}" and x: "x = x_i j n"
using canonical_basis_acc_eq_x_i [OF x k_l_n] by blast
show ?thesis
proof (rule ex1I [of _ j], rule conjI)
show "j ∈ {..<Suc k}" by fact
show "x = x_i j n" by (rule x)
fix ja
assume ja: "ja ∈ {..<Suc k} ∧ x = x_i ja n"
show "ja = j"
using x ja unfolding x_i_def
by (metis ja x x_i_ne_x_j)
qed
qed
corollary
canonical_basis_acc_isom_x_i2:
assumes x: "x ∈ canonical_basis_acc k n"
and k_l_n: "k < n"
shows "∃!j∈{..<n}. x = x_i j n"
proof -
obtain j :: nat where j: "j ∈ {..<Suc k}" and x: "x = x_i j n"
using canonical_basis_acc_eq_x_i [OF x k_l_n] by blast
show ?thesis
proof (rule ex1I [of _ j], rule conjI)
show "j ∈ {..<n}" using j k_l_n by fastsimp
show "x = x_i j n" by (rule x)
fix ja
assume ja: "ja ∈ {..<n} ∧ x = x_i ja n"
show "ja = j"
using x ja unfolding x_i_def
by (metis ja x x_i_ne_x_j)
qed
qed
lemma
canonical_basis_is_x_i:
assumes x: "x ∈ canonical_basis_K_n n"
(*and n_g_0: "0 < n"*)
shows "∃j∈{..<n}. x = x_i j n"
using x
unfolding canonical_basis_K_n_def
using canonical_basis_acc_eq_x_i [of x "n - 1" n] by (cases n, auto)
corollary
canonical_basis_isom_x_i:
assumes x: "x ∈ canonical_basis_K_n n"
(*and n_g_0: "0 < n"*)
shows "∃!j∈{..<n}. x = x_i j n"
proof -
obtain j :: nat where j: "j ∈ {..<n}" and x: "x = x_i j n"
using canonical_basis_is_x_i [OF x] by blast
show ?thesis
proof (rule ex1I [of _ j], rule conjI)
show "j ∈ {..<n}" by fact
show "x = x_i j n" by fact
fix ja
assume ja: "ja ∈ {..<n} ∧ x = x_i ja n"
show "ja = j"
using x ja unfolding x_i_def
by (metis ja x x_i_ne_x_j)
qed
qed
text{*The function @{term preim} maps vectors of the basis
@{term "canonical_basis_K_n n"} to their index.*}
definition
preim :: "'a vector => nat => nat"
where "preim x n = (THE j. j ∈ {..<n} ∧ x = x_i j n)"
lemma
preim_x_i_x_eq_x:
assumes x_l_n: "x < n"
(*and n_g_0 : "0 < n"*)
shows "preim (x_i x n) n = x"
unfolding preim_def
proof
show "x ∈ {..<n} ∧ x_i x n = x_i x n"
using x_l_n by fast
fix j :: nat
assume j: "j ∈ {..<n} ∧ x_i x n = x_i j n"
show "j = x"
using j
unfolding x_i_def by (metis j x_i_ne_x_j)
qed
lemma
preim_eq_x_i_acc:
assumes x: "x ∈ canonical_basis_acc k n"
and k_l_n: "k < n"
shows "x_i (preim x n) n = x"
unfolding preim_def
using theI' [OF canonical_basis_acc_isom_x_i2 [OF x k_l_n]] by presburger
lemma
preim_eq_x_i:
assumes x: "x ∈ canonical_basis_K_n n"
(*and n_g_0: "0 < n"*)
shows "x_i (preim x n) n = x"
unfolding preim_def
using theI' [OF canonical_basis_isom_x_i [OF x]] by presburger
lemma
preim_lessThan:
assumes x: "x ∈ canonical_basis_K_n n"
(*and n_g_0: "0 < n"*)
shows "preim x n ∈ {..<n}"
unfolding preim_def
using theI' [OF canonical_basis_isom_x_i [OF x]] by fast
subsection{*Properties of @{term "canonical_basis_K_n n"}:*}
text{*The following lemma proves that two different ways of writing down
an element of @{term "K_n n"} as a linear combination of the
elements of the basis @{term "canonical_basis_K_n n"} are equivalent.:*}
lemma
finsum_canonical_basis_acc_finsum_card:
assumes k_l_n: "k < n"
and f: "f ∈ carrier (K_n n) -> carrier R"
shows "(\<Oplus>\<^bsub>K_n n\<^esub>x∈canonical_basis_acc k n. f x \<odot> x)
= (\<Oplus>\<^bsub>K_n n\<^esub>k∈{..<Suc k}. f (x_i k n) \<odot> x_i k n)"
proof (rule abelian_monoid.finsum_cong'' [of _ _ "(λk. x_i k n)"])
show "abelian_monoid (K_n n)"
using abelian_monoid_K_n .
show "finite {..<Suc k}" using finite_lessThan .
show "bij_betw (λk. x_i k n) {..<Suc k} (canonical_basis_acc k n)"
proof (rule bij_betwI [of _ _ _ "(λj. preim j n)" ])
show "(λk. x_i k n) ∈ {..<Suc k} -> canonical_basis_acc k n"
using canonical_basis_acc_insert2 [OF _ k_l_n] by force
show "(λj. preim j n) ∈ canonical_basis_acc k n -> {..<Suc k}"
proof
fix x assume x: "x ∈ canonical_basis_acc k n"
obtain j where x_i_x: "x_i j n = x" and j_lessThan: "j < Suc k"
using canonical_basis_acc_eq_x_i [OF x k_l_n] by blast
show "preim x n ∈ {..<Suc k}"
unfolding x_i_x [symmetric]
using preim_x_i_x_eq_x [of j n] k_l_n j_lessThan by force
qed
fix x assume x: "x ∈ {..<Suc k}"
show "preim (x_i x n) n = x"
using preim_x_i_x_eq_x [of x n] k_l_n x by simp
next
fix y assume y: "y ∈ canonical_basis_acc k n"
show "x_i (preim y n) n = y"
using preim_eq_x_i_acc [OF y k_l_n] .
qed
show "(λx. f x \<odot> x) ∈ canonical_basis_acc k n -> carrier (K_n n)"
proof
fix x assume x: "x ∈ canonical_basis_acc k n"
obtain j where xi: "x_i j n = x" and j: "j ∈ {..<Suc k}"
using canonical_basis_acc_eq_x_i [OF x k_l_n] by fast
show "f x \<odot> x ∈ carrier (K_n n)"
apply (rule K_n_scalar_product_closed)
unfolding xi [symmetric] using f using x_i_closed j k_l_n by auto
qed
show "(λk. f (x_i k n) \<odot> x_i k n) ∈ {..<Suc k} -> carrier (K_n n)"
proof
fix x assume x: "x ∈ {..<Suc k}"
show "f (x_i x n) \<odot> x_i x n ∈ carrier (K_n n)"
apply (rule K_n_scalar_product_closed)
using f using x_i_closed x k_l_n by auto
qed
show "!!x. x ∈ {..<Suc k} =simp=> f (x_i x n) \<odot> x_i x n = f (x_i x n) \<odot> x_i x n"
by presburger
qed
lemma
finsum_canonical_basis_K_n_finsum_card:
assumes (*n_g_0: "0 < n"
and*) f: "f ∈ carrier (K_n n) -> carrier R"
shows "(\<Oplus>\<^bsub>K_n n\<^esub>x∈(canonical_basis_K_n n). f x \<odot> x)
= (\<Oplus>\<^bsub>K_n n\<^esub>k∈{..<n}. f (x_i k n) \<odot> x_i k n)"
proof (cases n)
case 0
interpret vector_space R "K_n 0" "op \<odot>" using vector_space_K_n .
show ?thesis
unfolding 0
unfolding canonical_basis_K_n_def by simp
next
case (Suc n)
interpret vector_space R "K_n (Suc n)" "op \<odot>" using vector_space_K_n .
show ?thesis
using f
unfolding Suc canonical_basis_K_n_def
using finsum_canonical_basis_acc_finsum_card [of "Suc n - 1" "Suc n" f]
by simp
qed
text{*The space generated by the @{term "vector_space.span"} of
@{term "canonical_basis_K_n n"} is equal to the vector space @{term "K_n n"}.*}
lemma
span_canonical_basis_K_n_carrier_K_n:
(*assumes n_g_0: "0 < n"*)
shows "vector_space.span R (K_n n) (op \<odot>) (canonical_basis_K_n n) = carrier (K_n n)"
proof
interpret vector_space R "K_n n" "op \<odot>" using vector_space_K_n .
show "span (canonical_basis_K_n n) ⊆ carrier (K_n n)"
proof
fix x
assume x: "x ∈ span (canonical_basis_K_n n)"
obtain g :: "(nat => 'a) × nat => 'a"
where g: "g ∈ coefficients_function (carrier (K_n n))"
and gx: "x = linear_combination g (canonical_basis_K_n n)"
using x unfolding span_def by blast
show "x ∈ carrier (K_n n)"
unfolding gx
by (rule linear_combination_closed,
rule canonical_basis_K_n_good_set,
rule g)
qed
show "carrier (K_n n) ⊆ span (canonical_basis_K_n n)"
proof
fix x
assume x: "x ∈ carrier (K_n n)"
def lc ≡ "finsum (K_n n) (λj. fst x j \<odot> x_i j n) {..<n}"
def reindex ≡ "(λt. if t ∈ (canonical_basis_K_n n) then fst x (preim t n) else \<zero>)"
have "x = lc"
using K_n_carrier_finsum_x_i [OF x]
unfolding lc_def .
also have "lc ∈ span (canonical_basis_K_n n)"
unfolding lc_def
unfolding span_def
unfolding coefficients_function_def
unfolding linear_combination_def
apply auto
apply (rule exI [of _ "reindex"])
apply (rule conjI3)
proof -
show "(\<Oplus>\<^bsub>K_n n\<^esub>j∈{..<n}. fst x j \<odot> x_i j n)
= (\<Oplus>\<^bsub>K_n n\<^esub>y∈canonical_basis_K_n n. reindex y \<odot> y)"
proof (rule abelian_monoid.finsum_cong'' [
symmetric, OF abelian_monoid_K_n [of n], of _ "(λj. x_i j n)"])
show "finite {..<n}" by simp
show "bij_betw (λj. x_i j n) {..<n} (canonical_basis_K_n n)"
proof (rule bij_betwI [of "(λj. x_i j n)" "{..<n}" "canonical_basis_K_n n" "(λx. preim x n)"])
show "(λj. x_i j n) ∈ {..<n} -> canonical_basis_K_n n"
using canonical_basis_K_n_elements [OF ] by fast
next
show "(λx. preim x n) ∈ canonical_basis_K_n n -> {..<n}"
using preim_lessThan [OF _ ] by blast
next
fix x assume x: "x ∈ {..<n}"
show "preim (x_i x n) n = x"
using preim_x_i_x_eq_x [OF _ , of x]
using x by fast
next
fix y assume y: "y ∈ canonical_basis_K_n n"
show "x_i (preim y n) n = y"
by (rule preim_eq_x_i [OF y])
qed
show "(λy. reindex y \<odot> y) ∈ canonical_basis_K_n n -> carrier (K_n n)"
proof
fix xa
assume xa: "xa ∈ canonical_basis_K_n n"
hence xa2: "xa ∈ carrier (K_n n)"
using canonical_basis_K_n_closed [OF ] by fast
have xa_l_n: "preim xa n ∈ {..<n}"
by (rule preim_lessThan [OF xa ])
hence f: "fst x (preim xa n) ∈ carrier R"
using x unfolding K_n_def K_n_carrier_def ith_def by auto
show "reindex xa \<odot> xa ∈ carrier (K_n n)"
unfolding reindex_def
using xa
using K_n_scalar_product_closed [OF f xa2] by presburger
qed
show "(λj. fst x j \<odot> x_i j n) ∈ {..<n} -> carrier (K_n n)"
proof
fix xa assume xa: "xa ∈ {..<n}"
hence f: "fst x xa ∈ carrier R" using x
unfolding K_n_def K_n_carrier_def ith_def by auto
have x_i: "x_i xa n ∈ carrier (K_n n)"
using x_i_closed [of xa n] xa by fast
show "fst x xa \<odot> x_i xa n ∈ carrier (K_n n)"
by (rule K_n_scalar_product_closed, rule f, rule x_i)
qed
show "!!xa. xa ∈ {..<n} =simp=>
fst x xa \<odot> x_i xa n = reindex (x_i xa n) \<odot> x_i xa n"
unfolding reindex_def
using canonical_basis_K_n_elements [of _ n]
using preim_x_i_x_eq_x [OF _, of _] by force
qed
show "reindex ∈ carrier (K_n n) -> carrier R"
proof
fix xa
assume xa: "xa ∈ carrier (K_n n)"
show "reindex xa ∈ carrier R"
unfolding reindex_def
using preim_lessThan [of xa n]
using x unfolding K_n_def K_n_carrier_def ith_def by fastsimp
qed
show "∀a b. (a, b) ∉ carrier (K_n n) --> reindex (a, b) = \<zero>"
proof (rule+)
fix a b assume notin_carrier: "(a,b) ∉ carrier (K_n n)"
have "(a,b) ∉ canonical_basis_K_n n"
using canonical_basis_K_n_closed[of n] notin_carrier
by fast
thus "reindex (a, b) = \<zero>" unfolding reindex_def by presburger
qed
qed
finally show "x ∈ span (canonical_basis_K_n n)" .
qed
qed
lemma
canonical_basis_K_n_spanning_set:
(*assumes n_g_0: "0 < n"*)
shows "vector_space.spanning_set R (K_n n) (op \<odot>) (canonical_basis_K_n n)"
apply (unfold vector_space.spanning_set_def [OF vector_space_K_n], auto)
apply (metis canonical_basis_K_n_good_set)
using span_canonical_basis_K_n_carrier_K_n [OF ]
using vector_space.span_def [OF vector_space_K_n] by force
text{*The elements of @{term "canonical_basis_acc j n"} are linearly independent.*}
lemma
canonical_basis_acc_linear_independent_ext:
assumes j_l_n: "j < n"
shows "vector_space.linear_independent_ext R (K_n n) (op \<odot>) (canonical_basis_acc j n)"
proof -
-- "We first produce the interpretation of the locale @{text vector_space}"
interpret vector_space R "(K_n n)" "(op \<odot>)"
using vector_space_K_n [of n] .
have "linear_independent_ext (canonical_basis_acc j n) =
linear_independent (canonical_basis_acc j n)"
unfolding linear_independent_ext_def
using finite_canonical_basis_acc [of j n]
by (metis independent_set_implies_independent_subset subset_refl)
also have "linear_independent (canonical_basis_acc j n)"
proof (rule ccontr)
assume n: "¬ linear_independent (canonical_basis_acc j n)"
have ld: "linear_dependent (canonical_basis_acc j n)"
proof (rule not_independent_implies_dependent)
show "¬ linear_independent (canonical_basis_acc j n)" by (rule n)
show "good_set (canonical_basis_acc j n)"
unfolding good_set_def
using finite_canonical_basis_acc [of j n]
using canonical_basis_acc_closed [OF j_l_n] by fast
qed
then obtain f where f: "f ∈ coefficients_function (carrier (K_n n))"
and lc: "linear_combination f (canonical_basis_acc j n) = \<zero>\<^bsub>K_n n\<^esub>"
and nzero: "¬ (∀x∈(canonical_basis_acc j n). f x = \<zero>)"
unfolding linear_dependent_def by fast
have "\<zero>\<^bsub>K_n n\<^esub> = linear_combination f (canonical_basis_acc j n)"
by (rule lc [symmetric])
also have "linear_combination f (canonical_basis_acc j n) =
finsum (K_n n) (λx. f x \<odot> x) (canonical_basis_acc j n)"
unfolding linear_combination_def ..
also have "... = finsum (K_n n) (λk. f (x_i k n) \<odot> x_i k n) {..<(Suc j)}"
apply (rule finsum_canonical_basis_acc_finsum_card, rule j_l_n)
using f unfolding coefficients_function_def by fast
also have "... = (λk. if k ∈ {..<Suc j} then f (x_i k n) else \<zero>, n - 1)"
apply (rule lambda_finsum [symmetric])
using f unfolding coefficients_function_def using x_i_closed [of _ n]
using j_l_n by auto
finally have "\<zero>\<^bsub>K_n n\<^esub> = (λk. if k ∈ {..<Suc j} then f (x_i k n) else \<zero>, n - 1)" .
hence p: "(λi. \<zero>) = (λk. if k ∈ {..<Suc j} then f (x_i k n) else \<zero>)"
unfolding K_n_def K_n_zero_def by auto
have j_zero: "∀k∈{..<Suc j}. f (x_i k n) = \<zero>"
using fun_cong [OF p] by metis
have "∀x∈(canonical_basis_acc (Suc j) n). f x = \<zero>"
proof
fix x assume x: "x ∈ canonical_basis_acc (Suc j) n"
obtain k where xi: "x = x_i k n" and k: "k ∈ {..<Suc j}"
by (metis assms canonical_basis_acc_eq_x_i j_zero nzero)
show "f x = \<zero>" unfolding xi using j_zero k by blast
qed
hence "∀x∈(canonical_basis_acc j n). f x = \<zero>"
by (metis assms canonical_basis_acc_eq_x_i j_zero)
thus False
using nzero by fast
qed
finally show ?thesis .
qed
end
context vector_space
begin
text {*The following lemma should be moved to the place where @{term "linear_independent_ext"}
has been defined, like a @{text simp} rule:*}
lemma linear_independent_ext_empty [simp]:
shows "linear_independent_ext {}"
unfolding linear_independent_ext_def
using empty_set_is_linearly_independent by simp
end
context field
begin
lemma
canonical_basis_K_n_linear_independent_ext:
(*assumes n_g_0: "0 < n"*)
shows "vector_space.linear_independent_ext R (K_n n) (op \<odot>) (canonical_basis_K_n n)"
unfolding canonical_basis_K_n_def
using canonical_basis_acc_linear_independent_ext [of "n - 1" n]
using vector_space.linear_independent_ext_empty [OF vector_space_K_n]
by (cases n, auto)
text{*We finally prove that @{term "canonical_basis_K_n n"} is a basis
for @{term "K_n"}.*}
lemma
canonical_basis_K_n_basis:
(*assumes n_g_0: "0 < n"*)
shows "vector_space.basis R (K_n n) (op \<odot>) (canonical_basis_K_n n)"
unfolding vector_space.basis_def [OF vector_space_K_n]
using canonical_basis_K_n_linear_independent_ext [OF ]
using canonical_basis_K_n_spanning_set [OF ]
by (metis canonical_basis_K_n_closed vector_space.spanning_imp_spanning_ext vector_space_K_n)
corollary
canonical_basis_K_n_basis_card_n:
(*assumes n_g_0: "0 < n"*)
shows "vector_space.basis R (K_n n) (op \<odot>) (canonical_basis_K_n n) ∧
card (canonical_basis_K_n n) = n"
using canonical_basis_K_n_basis [OF ]
and card_canonical_basis_K_n [OF ] by fastsimp
end
context finite_dimensional_vector_space
begin
text{*After proving the most relevant properties of @{term "K_n n"},
we fix one indexing of the basis elements (of @{term X}) that will allow us to define
later the function which given any element of the carrier set decomposes
it into the coefficients for each term if the indexation.*}
text{*The theorem @{text obtain_indexing}: @{thm obtain_indexing[no_vars]} and the
premise that the vector space is finite, and so is it basis
@{term "X::'c set"}, ensures that the following definition is sound.*}
definition indexing_X :: "nat => 'c"
where indexing_X_def: "indexing_X = (SOME f. indexing (X, f))"
text{*Relying in the fact that at least one indexing of the basis @{term "X"} exists,
we can prove that @{term indexing_X} satisfies the properties of
every @{term indexing}.*}
lemma indexing_X_is_indexing:
shows "indexing (X, indexing_X)"
using obtain_indexing [OF finite_X]
using some_eq_ex [of "(λf. indexing (X, f))"]
unfolding indexing_X_def by auto
text{*The following function is to be used as the inverse function of @{term "field.preim"};
this function and @{term "field.preim"} will be defined to prove an isomorphism between
@{term "canonical_basis_K_n (card X)"} and @{term "{..<(card X)}"}.*}
definition iso_nat_can :: "nat => 'a vector"
where "iso_nat_can n = (x_i n (dimension))"
text{*The composition of the functions @{term preim} and @{term iso_nat_can}
over the set @{term "{..<dimension}"} is equal to the identity.*}
lemma preim_iso_nat_can_id:
assumes (*X_ne: "0 < dimension"
and*) x: "x ∈ {..<dimension}"
shows "preim (iso_nat_can x) (dimension) = x"
unfolding iso_nat_can_def
using preim_x_i_x_eq_x [of x "dimension"]
unfolding x_i_def using x by blast
text{*In a very similar way, the composition of @{term preim}
and @{term iso_nat_can} over the set @{term "canonical_basis_K_n (dimension)"} is equal to the identity:*}
lemma iso_nat_can_preim_id:
assumes (*X_ne: "0 < dimension"
and*) y: "y ∈ canonical_basis_K_n (dimension)"
shows "iso_nat_can (preim y (dimension)) = y"
using preim_eq_x_i [OF y ]
unfolding x_i_def iso_nat_can_def .
lemma
bij_betw_iso_nat_can:
shows "bij_betw iso_nat_can {..<dimension}
(canonical_basis_K_n (dimension))"
proof (intro bij_betwI [of _ _ _ "(λi. preim i (dimension))"])
interpret field K by intro_locales
show "iso_nat_can
∈ {..<dimension} -> field.canonical_basis_K_n K (dimension)"
proof
fix x
assume x: "x ∈ {..<(dimension)}"
show "iso_nat_can x
∈ field.canonical_basis_K_n K (dimension)"
unfolding iso_nat_can_def
using canonical_basis_K_n_elements [OF x]
unfolding x_i_def .
qed
show "(λi. preim i (dimension))
∈ canonical_basis_K_n (dimension) -> {..<dimension}"
proof
fix x
assume x: "x ∈ canonical_basis_K_n (dimension)"
show "preim x (dimension) ∈ {..<dimension}"
by (rule preim_lessThan [OF x])
qed
fix x
assume x: "x ∈ {..<dimension}"
show "preim (iso_nat_can x) (dimension) = x"
by (rule preim_iso_nat_can_id [OF x])
next
interpret field K by intro_locales
fix y
assume y: "y ∈ canonical_basis_K_n (dimension)"
show "iso_nat_can (preim y (dimension)) = y"
by (rule iso_nat_can_preim_id [OF y])
qed
lemma
bij_betw_preim:
shows "bij_betw (λi. preim i (dimension))
(canonical_basis_K_n (dimension)) {..<dimension}"
proof (intro bij_betwI [of _ _ _ "iso_nat_can"])
interpret field K by intro_locales
show "iso_nat_can
∈ {..<dimension} -> canonical_basis_K_n (dimension)"
proof
fix x
assume x: "x ∈ {..<(dimension)}"
show "iso_nat_can x ∈ canonical_basis_K_n (dimension)"
unfolding iso_nat_can_def
using canonical_basis_K_n_elements [OF x]
unfolding x_i_def .
qed
show "(λi. preim i (dimension))
∈ canonical_basis_K_n (dimension) -> {..<dimension}"
proof
fix x
assume x: "x ∈ canonical_basis_K_n (dimension)"
show "preim x (dimension) ∈ {..<dimension}"
by (rule preim_lessThan [OF x])
qed
fix x
assume x: "x ∈ {..<dimension}"
show "preim (iso_nat_can x) (dimension) = x"
by (rule preim_iso_nat_can_id [OF x])
next
interpret field K by intro_locales
fix y
assume y: "y ∈ canonical_basis_K_n (dimension)"
show "iso_nat_can (preim y (dimension)) = y"
by (rule iso_nat_can_preim_id [OF y])
qed
text{*The following function will be used to define an isomorphism between the
sets @{term "{..<dimension}"} and @{term X}, which inverse will be the inverse
of the indexing function @{term "indexing_X"}.*}
definition
iso_nat_X :: "nat => 'c"
where "iso_nat_X n = indexing_X n"
text{*The inverse function of the previous @{term iso_nat_X} is the following function,
which properties we are to prove first:*}
definition
preim2 :: "'c => nat"
where "preim2 x = (THE j. j ∈ {..<dimension} ∧ x = indexing_X j)"
text{*The @{term preim2} function needs to be completed, since otherwise we can not ensure
for the elements out of the basis @{term X} that their value @{term "preim2 x"} is
not in the set @{term "{..<dimension}"}. If the value @{term "preim2 x"} could be
in @{term "{..<dimension}"} for elements out of @{term X}, then the function
@{term "fst x (preim2 y)"}, for @{term "y ∉ X"} could take values different from
@{term "\<zero>\<^bsub>K\<^esub>"}.*}
text{*The way to complete it is a bit artificial, since we can not
use @{term "0::nat"} to complete it, but some element @{term "a::nat"} with @{term "a ≥ dimension"},
which are the natural numbers that are mapped to @{term "\<zero>\<^bsub>K\<^esub>"} by
@{term "coefficients_function"}. In particular, we have chosen @{term "a=dimension"}.*}
definition
preim2_comp :: "'c => nat"
where "preim2_comp x = (if x ∈ X then (THE j. j ∈ {..<dimension} ∧ x = indexing_X j) else dimension)"
lemma
indexing_X_bij:
shows "bij_betw indexing_X {..<dimension} X"
proof -
have f1: "finite X" and f2: "finite {..<dimension}" by (metis finite_X, simp)
have ex: "∃f. bij_betw f {..<dimension} X"
using BIJ [OF f2 f1] unfolding dimension_def by simp
thus ?thesis
using some_eq_ex [of "(λf. bij_betw f {..<dimension} X)"]
unfolding indexing_X_def indexing_def dimension_def by simp
qed
lemma
indexing_X_preimage:
assumes x: "x ∈ X"
shows "∃j. j ∈ {..<dimension} ∧ x = indexing_X j"
proof -
obtain j where "j ∈ {..<dimension}" and "indexing_X j = x"
using x using indexing_X_bij
unfolding bij_betw_def unfolding image_def by force
thus ?thesis by fast
qed
corollary
indexing_X_preimage_unique:
assumes x: "x ∈ X"
shows "∃!j. j ∈ {..<dimension} ∧ x = indexing_X j"
proof -
obtain j :: nat where j: "j ∈ {..<dimension}" and x: "x = indexing_X j"
using indexing_X_preimage [OF x] by fast
show ?thesis
proof (rule ex1I [of _ j], rule conjI)
show "j ∈ {..<dimension}" by fact
show "x = indexing_X j" by (rule x)
fix ja
assume ja: "ja ∈ {..<dimension} ∧ x = indexing_X ja"
show "ja = j"
using x j ja indexing_X_bij
unfolding bij_betw_def
by (metis inj_onD)
qed
qed
lemma
preim2_in_dimension:
assumes x: "x ∈ X"
shows "preim2 x ∈ {..<dimension}"
unfolding preim2_def
using theI' [OF indexing_X_preimage_unique [OF x]] by fast
lemma
preim2_comp_in_dimension:
assumes x: "x ∈ X"
shows "preim2_comp x ∈ {..<dimension}"
using preim2_in_dimension [OF x] x
unfolding preim2_comp_def preim2_def by simp
lemma
preim2_is_indexing_X:
assumes x: "x ∈ X"
shows "x = indexing_X (preim2 x)"
unfolding preim2_def
using theI' [OF indexing_X_preimage_unique [OF x]] by fast
text{*The functions @{term "preim2_comp"} and @{term "iso_nat_X"} are
inverse of each other, over the sets @{term "X"} and @{term "{..<dimension}"}*}
lemma
preim2_comp_is_indexing_X:
assumes x: "x ∈ X"
shows "x = indexing_X (preim2_comp x)"
using preim2_is_indexing_X [OF x] x
unfolding preim2_def preim2_comp_def by presburger
lemma iso_nat_X_preim2_id:
assumes x: "x ∈ X"
shows "iso_nat_X (preim2 x) = x"
using theI' [OF indexing_X_preimage_unique [OF x]]
unfolding preim2_def
unfolding iso_nat_X_def by presburger
lemma iso_nat_X_preim2_comp_id:
assumes x: "x ∈ X"
shows "iso_nat_X (preim2_comp x) = x"
using iso_nat_X_preim2_id [OF x]
unfolding preim2_def preim2_comp_def using x by presburger
lemma preim2_iso_nat_X_id:
assumes n: "n ∈ {..<dimension}"
shows "preim2 (iso_nat_X n) = n"
proof -
have i: "iso_nat_X n ∈ X"
unfolding iso_nat_X_def iso_nat_X_def
using indexing_X_is_indexing using n
unfolding indexing_def dimension_def unfolding bij_betw_def image_def by auto
show ?thesis
unfolding preim2_def iso_nat_X_def
apply (rule the1_equality)
using indexing_X_preimage_unique [OF i] n
unfolding iso_nat_X_def by fast+
qed
lemma preim2_comp_iso_nat_X_id:
assumes n: "n ∈ {..<dimension}"
shows "preim2_comp (iso_nat_X n) = n"
proof -
have i: "iso_nat_X n ∈ X"
unfolding iso_nat_X_def iso_nat_X_def
using indexing_X_is_indexing using n
unfolding indexing_def dimension_def unfolding bij_betw_def image_def by auto
show ?thesis
using preim2_iso_nat_X_id [OF n] using i
unfolding preim2_comp_def preim2_def by presburger
qed
text{*Therefore, we can prove that there exists a bijection between them:*}
lemma
bij_betw_iso_nat_X:
shows "bij_betw iso_nat_X {..<dimension} X"
proof (intro bij_betwI [of _ _ _ preim2])
show "iso_nat_X ∈ {..<dimension} -> X"
proof
fix x assume x: "x ∈ {..<dimension}"
show "iso_nat_X x ∈ X"
unfolding iso_nat_X_def
using indexing_X_is_indexing using x
unfolding indexing_def bij_betw_def image_def dimension_def by auto
qed
show "preim2 ∈ X -> {..<dimension}"
proof
fix x assume x: "x ∈ X"
show "preim2 x ∈ {..<dimension}"
using theI' [OF indexing_X_preimage_unique [OF x]]
unfolding preim2_def by fast
qed
fix x assume x: "x ∈ {..<dimension}"
show "preim2 (iso_nat_X x) = x"
by (rule preim2_iso_nat_X_id [OF x])
next
fix y assume y: "y ∈ X"
show "iso_nat_X (preim2 y) = y"
by (rule iso_nat_X_preim2_id [OF y])
qed
lemma
bij_betw_preim2:
shows "bij_betw preim2 X {..<dimension}"
proof (intro bij_betwI [of _ _ _ iso_nat_X])
show "preim2 ∈ X -> {..<dimension}"
proof
fix x assume x: "x ∈ X"
show "preim2 x ∈ {..<dimension}"
using theI' [OF indexing_X_preimage_unique [OF x]]
unfolding preim2_def by fast
qed
show "iso_nat_X ∈ {..<dimension} -> X"
proof
fix x assume x: "x ∈ {..<dimension}"
show "iso_nat_X x ∈ X"
unfolding iso_nat_X_def
using indexing_X_is_indexing using x
unfolding indexing_def bij_betw_def image_def dimension_def by auto
qed
fix y assume y: "y ∈ X"
show "iso_nat_X (preim2 y) = y"
by (rule iso_nat_X_preim2_id [OF y])
next
fix x assume x: "x ∈ {..<dimension}"
show "preim2 (iso_nat_X x) = x"
by (rule preim2_iso_nat_X_id [OF x])
qed
end
subsection{*Linear maps.*}
text{*In this section we are going to introduce the notion of linear map between
vector spaces. This is a previous step for the definition of an isomorphism between
vector spaces. Then, we will have to prove the existence of an isomorphism
between the vector spaces @{term "K_n dimension"} and @{term V}.*}
text{*The definition between comments would be the expected and desired one.
Unfortunately, it introduces changes in the namespace that are really inconvenient.
The second locale hides the names of constants in vector space, demanding long names
for the first locale constanst. We do not know how to control this behaviour: thus, we
preferred the long version, in which locale interpretation has to be done later by hand:*}
(*locale linear_map = KV: vector_space K V f + KW: vector_space K W g
for K (structure) and V (structure) and W (structure) and f (infixl "·\<^bsub>V\<^esub>" 60) and g (infixl "·\<^bsub>W\<^esub>" 60)*)
locale linear_map =
fixes K :: "('a, 'b) ring_scheme"
and V :: "('c, 'd) ring_scheme"
and W :: "('e, 'f) ring_scheme"
and scalar_product1 :: "'a => 'c => 'c" (infixr "·\<^bsub>V\<^esub>" 70)
and scalar_product2 :: "'a => 'e => 'e" (infixr "·\<^bsub>W\<^esub>" 70)
assumes V: "vector_space K V (op ·\<^bsub>V\<^esub>)"
and W: "vector_space K W (op ·\<^bsub>W\<^esub>)"
context linear_map
begin
text{*Linear maps, as characterised in "Linear Algebra Done Right", have to satisfy
the additivity and homogeneity properties:*}
definition additivity :: "('c => 'e) => bool"
where "additivity T = (∀x∈carrier V. ∀y ∈ carrier V. T (x ⊕\<^bsub>V\<^esub> y) = T x ⊕\<^bsub>W\<^esub> T y)"
definition homogeneity :: "('c => 'e) => bool"
where "homogeneity T = (∀k∈carrier K. ∀x∈carrier V. T (k ·\<^bsub>V\<^esub> x) = k ·\<^bsub>W\<^esub> T x)"
definition linear_map :: "('c => 'e) => bool"
where "linear_map T = (additivity T ∧ homogeneity T)"
end
text{*We introduce a new locale for finite dimensional vector spaces, just imposing that
there is a finite basis for one ot the vector spaces.*}
locale linear_map_fin_dim = linear_map +
fixes X
assumes fin_dim: "finite_dimensional_vector_space K V (op ·\<^bsub>V\<^esub>) X"
text{*We produce two different sublocales, or interpretations,
of the locale @{text linear_map_fin_dim}
by means of the locale @{text finite_dimensional_vector_space}.
They allow us to later define
linear maps from @{term V} to @{term K_n} and also the opposite way,
from @{term K_n} to @{term V}. The system forces us to make them
\emph{named} interpretations, just to avoid colliding names.*}
sublocale finite_dimensional_vector_space <
V_K_n: linear_map_fin_dim K V "K_n dimension" "op ·" K_n_scalar_product X
proof (unfold linear_map_fin_dim_def, intro conjI)
show "linear_map K V (field.K_n K dimension) op · (field.K_n_scalar_product K)"
proof (unfold linear_map_def, intro conjI)
show "vector_space K (K_n dimension) K_n_scalar_product"
using vector_space_K_n .
show "vector_space K V op ·" by (intro_locales)
qed
next
show "linear_map_fin_dim_axioms K V op · X"
proof (unfold linear_map_fin_dim_axioms_def finite_dimensional_vector_space_def,
intro conjI)
show "vector_space K V op ·"by intro_locales
show "finite_dimensional_vector_space_axioms K V op · X"
proof
show "finite X" by (rule finite_X)
show "basis X" by (rule basis_X)
qed
qed
qed
sublocale finite_dimensional_vector_space < K_n_V: linear_map_fin_dim K "K_n dimension" V
K_n_scalar_product "op ·" "canonical_basis_K_n dimension"
proof (intro_locales)
interpret K: field K by intro_locales
interpret V: vector_space K V "op ·" by intro_locales
interpret K_n: vector_space K "K_n dimension" "K_n_scalar_product" using vector_space_K_n .
show "Isomorphism.linear_map K (K_n dimension) V (K_n_scalar_product) op ·" by unfold_locales
show "linear_map_fin_dim_axioms K (K_n dimension)
(K_n_scalar_product) (canonical_basis_K_n dimension)"
proof unfold_locales
show "finite (canonical_basis_K_n dimension)"
by (rule finite_canonical_basis_K_n)
show "K_n.basis (canonical_basis_K_n dimension)"
using canonical_basis_K_n_basis [of dimension] by fast
qed
qed
subsection{*Defining the isomorphism between $\mathbb{K}^n$ and $V$.*}
context finite_dimensional_vector_space
begin
text{*Some properties proving that there exists a unique function of coefficients
for each element in the carrier set of @{term V}; this unique function
is the one that decomposes any element into its linear combination
over the elements of the basis:*}
lemma
basis_implies_linear_combination:
assumes x: "(x::'c) ∈ carrier V"
shows "∃f. f ∈ coefficients_function (carrier V) ∧ x = linear_combination f X"
using spanning_set_X
unfolding spanning_set_def
using x by blast
text{*In order to ensure the uniqueness of the coefficients function
we have to use @{term coefficients_function}, which is mapped to
@{term "\<zero>"} out of its domain.*}
lemma
basis_implies_coeff_function_comp_linear_combination:
assumes x: "(x::'c) ∈ carrier V"
shows "∃f. f ∈ coefficients_function X ∧ x = linear_combination f X"
proof -
obtain f where f: "f ∈ coefficients_function (carrier V)"
and x: "x = linear_combination f X"
using basis_implies_linear_combination [OF x] by force
let ?g = "(λx. if x ∈ X then f x else \<zero>)"
show ?thesis
proof (rule exI [of _ ?g], intro conjI)
show "(λy. if y ∈ X then f y else \<zero>) ∈ coefficients_function X"
using f
unfolding coefficients_function_def
using good_set_X unfolding good_set_def by fastsimp
show "x = linear_combination (λy. if y ∈ X then f y else \<zero>) X"
unfolding x
unfolding linear_combination_def
proof (rule finsum_cong')
show "X = X" ..
show " (λy. (if y ∈ X then f y else \<zero>) · y) ∈ X -> carrier V"
proof
fix x assume x: "x ∈ X"
show "(if x ∈ X then f x else \<zero>) · x ∈ carrier V"
apply (cases "x ∈ X")
using fx_x_in_V [of x f]
using f x good_set_X
unfolding good_set_def by auto
qed
fix i assume i: "i ∈ X"
thus "f i · i = (if i ∈ X then f i else \<zero>) · i" by fastsimp
qed
qed
qed
text{* Firstly we prove a theorem similar to @{text unique_coordenates}: @{thm unique_coordenates[no_vars]}. It claims that the coordinates are unique in a basis.*}
lemma
linear_combination_unique:
assumes x: "x ∈ carrier V"
shows "∃!f. f ∈ coefficients_function X & linear_combination f X = x"
proof -
obtain f_cf where cf_fc: "f_cf ∈ coefficients_function (carrier V)"
and lc_cf: "linear_combination f_cf X = x"
using x using spanning_set_X
unfolding spanning_set_def by (metis mem_def)
def f == "(λx. if x ∈ X then f_cf x else \<zero>)"
have cf: "f ∈ coefficients_function X"
and lc: "linear_combination f X = x"
using cf_fc lc_cf
unfolding coefficients_function_def
unfolding linear_combination_def
unfolding f_def using good_set_X unfolding good_set_def apply auto
apply (rule finsum_cong')
apply auto by (rule mult_closed) auto
show ?thesis
proof (rule ex1I [of _ f])
show "f ∈ coefficients_function X & linear_combination f X = x" using cf lc ..
fix g
assume "g ∈ coefficients_function X & linear_combination g X = x"
hence cfg: "g ∈ coefficients_function X" and lcg: "linear_combination g X = x" by fast+
have f_y_y_Pi: "(λy. f y · y) ∈ X -> carrier V"
and f_y_Pi: "(λy. f y) ∈ X -> carrier K"
and g_y_Pi: "(λy. g y) ∈ X -> carrier K"
and g_y_y_Pi: "(λy. g y · y) ∈ X -> carrier V"
and f_minus_g_Pi: " (λy. f y · y \<ominus>\<^bsub>V\<^esub> g y · y) ∈ X -> carrier V"
(*using coefficients_function_comp_is_coefficients_function [OF cf]
and coefficients_function_comp_is_coefficients_function [OF cfg]*)
unfolding coefficients_function_def
unfolding Pi_def
using coefficients_function_Pi[OF _ cfg]
using coefficients_function_Pi[OF _ cf]
using good_set_X unfolding good_set_def by (auto simp add: mult_closed)
show "g = f"
proof -
have "\<zero>\<^bsub>V\<^esub> = linear_combination f X \<ominus>\<^bsub>V\<^esub> linear_combination g X"
unfolding lc lcg using x by (metis local.r_neg')
also have "linear_combination f X \<ominus>\<^bsub>V\<^esub> linear_combination g X =
(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) \<ominus>\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. g y · y)"
unfolding linear_combination_def ..
also have "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) \<ominus>\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. g y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. g y · y)"
unfolding minus_eq [OF finsum_closed [OF finite_X f_y_y_Pi]
finsum_closed [OF finite_X g_y_y_Pi]] ..
also have "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. g y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (g y · y))"
unfolding finsum_minus_eq [OF finite_X g_y_y_Pi]
apply (rule finsum_addf [symmetric, OF finite_X f_y_y_Pi])
using a_inv_closed g_y_y_Pi by auto
also have " (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (g y · y)) = (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y \<ominus>\<^bsub>V\<^esub> (g y · y))"
proof (rule finsum_cong', rule, rule f_minus_g_Pi)
fix i assume x: "i ∈ X"
show "f i · i ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (g i · i) = f i · i \<ominus>\<^bsub>V\<^esub> g i · i"
by (rule minus_eq [symmetric], rule funcset_mem [OF f_y_y_Pi x],
rule funcset_mem [OF g_y_y_Pi x])
qed
also have "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y \<ominus>\<^bsub>V\<^esub> g y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈X. (f y \<ominus> g y) · y)"
proof (rule finsum_cong' [symmetric], rule, rule f_minus_g_Pi)
show "!!i. i ∈ X ==> (f i \<ominus> g i) · i = f i · i \<ominus>\<^bsub>V\<^esub> g i · i"
proof -
fix i assume i: "i ∈ X"
hence iV: "i ∈ carrier V" using good_set_X unfolding good_set_def
by auto
show "(f i \<ominus> g i) · i = f i · i \<ominus>\<^bsub>V\<^esub> g i · i"
by (rule diff_mult_distrib2, fact)
(rule funcset_mem [OF f_y_Pi i], rule funcset_mem [OF g_y_Pi i])
qed
qed
also have "... = linear_combination (λx. f x \<ominus> g x) X"
unfolding linear_combination_def ..
finally have "linear_combination (λx. f x \<ominus> g x) X = \<zero>\<^bsub>V\<^esub>" ..
-- "A linear combination of elements of the basis @{term X} equal to zero
means that every coefficient must be zero:"
moreover have " (λx. f x \<ominus> g x) ∈ coefficients_function (carrier V)"
(*using coefficients_function_comp_is_coefficients_function [OF cf]
using coefficients_function_comp_is_coefficients_function [OF cfg]*)
using coefficients_function_Pi[OF _ cf]
using coefficients_function_Pi[OF _ cfg]
unfolding coefficients_function_def
apply (auto simp add: minus_closed)
proof -
fix x
assume x_notin_V: "x ∉ carrier V"
hence "f x \<ominus> g x = \<zero> \<ominus> \<zero>"
using cfg cf good_set_X unfolding coefficients_function_def good_set_def by fastsimp
also have "...=\<zero>"
by (metis K.add.inv_one K.add.one_closed a_minus_def
abelian_monoid.r_zero abelian_monoid_R insertI1 insert_absorb mem_def)
finally show "f x \<ominus> g x = \<zero>" .
qed
ultimately have lin_comb_X_eq_0: "∀x∈X. (λx. f x \<ominus> g x) x = \<zero>"
using linear_independent_X
unfolding linear_independent_def by auto
have f_eq_g_X: "∀x∈X. f x = g x"
proof (rule ballI)
fix x assume x: "x ∈ X"
have fx: "f x ∈ carrier K" and gx: "g x ∈ carrier K"
using x using good_set_X unfolding good_set_def
using cf
using cfg
unfolding coefficients_function_def by auto
have "f x \<ominus> g x ⊕ g x = g x"
using lin_comb_X_eq_0 fx gx x by simp
hence "f x = g x" using fx gx
by (metis plus_minus_cancel cring.cring_simprules(16) is_cring lin_comb_X_eq_0 x)
thus "f x = g x" .
qed
show "g = f"
proof (rule ext, case_tac "x ∈ X")
fix x assume x: "x ∈ X" show "g x = f x"
using f_eq_g_X x by simp
next
fix x assume x: "x ∉ X" show "g x = f x"
using cf cfg unfolding coefficients_function_def
using x by simp
qed
qed
qed
qed
text{*The previous lemma ensures the existence of only one function
@{term "f::'c => 'a"} satisfying to be a linear combination and a
coefficients function which generates any @{term "x::'c"} belonging
to @{term "carrier V"}*}
definition lin_comb :: "'c => ('c => 'a)"
where "lin_comb x = (THE f. f ∈ coefficients_function X
∧ linear_combination f X = x)"
lemma
lin_comb_is_coefficients_function:
assumes x: "x ∈ carrier V"
shows "lin_comb x ∈ coefficients_function X"
using theI' [OF linear_combination_unique [OF x]]
unfolding lin_comb_def by fast
(*lemma
lin_comb_is_coefficients_function_comp:
assumes x: "x ∈ carrier V"
shows "lin_comb x ∈ coefficients_function_comp X"
using theI' [OF linear_combination_unique [OF x]]
unfolding lin_comb_def by fast*)
lemma
lin_comb_is_the_linear_combination:
assumes x: "x ∈ carrier V"
shows "x = linear_combination (lin_comb x) X"
unfolding lin_comb_def
using theI' [OF linear_combination_unique [OF x]] by simp
lemma
indexing_X_n_in_X:
assumes n_dimension: "n < dimension"
shows "indexing_X n ∈ X"
using indexing_X_is_indexing
unfolding indexing_def
using bij_betw_imp_funcset
using n_dimension unfolding dimension_def by auto
corollary
indexing_X_n_in_carrier_V:
assumes n_dimension: "n < dimension"
shows "indexing_X n ∈ carrier V"
using indexing_X_n_in_X [OF n_dimension]
using good_set_X unfolding good_set_def by auto
text{*A lemma stating that every element of the carrier set
can be expressed as a finite sum over the elements of the set @{term "{..<dimension}"}
thanks to the function @{term "lin_comb"}.*}
lemma
lin_comb_is_the_linear_combination_indexing:
assumes x: "x ∈ carrier V"
shows "x = finsum V (λi. lin_comb x (indexing_X i) · indexing_X i) {..<dimension}"
proof -
have "x = linear_combination (lin_comb x) X"
by (rule lin_comb_is_the_linear_combination [OF x])
also have "... = finsum V (λy. lin_comb x y · y) X"
unfolding linear_combination_def ..
also have "... = finsum V (λi. lin_comb x (indexing_X i) · indexing_X i) {..<dimension}"
proof (rule finsum_cong'' [of _ "indexing_X"])
show "finite {..<dimension}" by fast
show "bij_betw indexing_X {..<dimension} X" by (rule indexing_X_bij)
show "(λy. lin_comb x y · y) ∈ X -> carrier V"
proof
fix xa assume xa: "xa ∈ X"
show "lin_comb x xa · xa ∈ carrier V"
apply (rule mult_closed)
using xa using good_set_X
using lin_comb_is_coefficients_function [OF x]
unfolding good_set_def coefficients_function_def by fast+
qed
show "(λi. lin_comb x (indexing_X i) · indexing_X i) ∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "lin_comb x (indexing_X xa) · indexing_X xa ∈ carrier V"
apply (rule mult_closed)
using indexing_X_n_in_carrier_V [of xa] xa
using lin_comb_is_coefficients_function [OF x]
using coefficients_function_Pi[of "indexing_X xa" "lin_comb x"]
unfolding coefficients_function_def by auto
qed
show "!!xa. xa ∈ {..<dimension} =simp=>
lin_comb x (indexing_X xa) · indexing_X xa =
lin_comb x (indexing_X xa) · indexing_X xa" by simp
qed
finally show ?thesis .
qed
text{*A lemma on how the elements of the basis are mapped by @{term "lin_comb"}:*}
lemma
lin_comb_basis:
assumes x: "x ∈ X"
shows "lin_comb x = (λi. if i = x then \<one> else \<zero>)"
unfolding lin_comb_def
proof (rule the1_equality)
have x1: "x ∈ carrier V"
using good_set_X x
unfolding good_set_def by fast
show "∃!f. f ∈ coefficients_function X ∧ linear_combination f X = x"
using linear_combination_unique [OF x1] .
show "(λi. if i = x then \<one> else \<zero>) ∈ coefficients_function X ∧
linear_combination (λi. if i = x then \<one> else \<zero>) X = x"
proof (rule conjI)
show "(λi. if i = x then \<one> else \<zero>) ∈ coefficients_function X"
unfolding coefficients_function_def using x by fastsimp
show "linear_combination (λi. if i = x then \<one> else \<zero>) X = x"
proof -
thm linear_combination_def
have "linear_combination (λi. if i = x then \<one> else \<zero>) X =
(\<Oplus>\<^bsub>V\<^esub>y∈X. (if y = x then \<one> else \<zero>) · y)" unfolding linear_combination_def ..
also have "... = (\<Oplus>\<^bsub>V\<^esub>y∈X. (if x = y then \<one> · y else \<zero>\<^bsub>V\<^esub>))"
apply (rule finsum_cong', auto)
using good_set_X
unfolding good_set_def
apply (metis mult_1 x1)
by (metis good_set_X good_set_in_carrier subsetD zeroK_mult_V_is_zeroV)
also have "... = \<one> · x"
proof (rule finsum_singleton [OF x finite_X, of "(λx. \<one> · x)"], rule)
fix x assume x: "x ∈ X" hence xx: "x ∈ carrier V"
using good_set_X
unfolding good_set_def by fast
show "\<one> · x ∈ carrier V"
by (rule mult_closed [OF xx one_closed])
qed
also have "... = x"
by (rule mult_1 [OF x1])
finally show ?thesis .
qed
qed
qed
end
context vector_space
begin
text{*The following lemma is a minor modification of @{thm finsum_aux},
but with a bit more general statement. In particular, it removes a
premise stating that @{term "X ⊆ carrier V"}, which is never used
in the proof of @{thm finsum_aux} and also generalizes the inner
expression of the finite sum. It may either replace @{thm finsum_aux}
in the file @{text Vector_Space} or added besides it in the same file.*}
lemma finsum_aux2:
"[|finite X; a ∈ carrier K; f ∈ X -> carrier K; g ∈ X -> carrier V|]
==> a · (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · g y)=(\<Oplus>\<^bsub>V\<^esub>y∈X. a · (f y · g y))"
proof (induct set: finite)
case empty thus ?case
using scalar_mult_zeroV_is_zeroV by auto
next
case (insert x X)
show ?case
proof -
have sum_closed: "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · g y) ∈ carrier V"
proof (rule finsum_closed)
show "finite X" using insert.hyps (1) .
show "(λy. f y · g y) ∈ X -> carrier V"
using insert.prems (1,2,3) and mult_closed by auto
qed
have fx_gx_in_V: "f x · g x ∈ carrier V"
using insert.prems (1,2,3) and mult_closed by auto
have "(\<Oplus>\<^bsub>V\<^esub>y∈insert x X. f y · g y)= f x · g x ⊕\<^bsub>V\<^esub>(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · g y)"
proof (rule finsum_insert)
show "finite X" using insert.hyps (1) .
show "x∉ X" using insert.hyps (2) .
show "f x · g x ∈ carrier V" using fx_gx_in_V .
show "(λy. f y · g y) ∈ X -> carrier V"
using insert.prems (1,2,3) and mult_closed by auto
qed
hence "a · (\<Oplus>\<^bsub>V\<^esub>y∈insert x X. f y · g y) = a · f x · g x ⊕\<^bsub>V\<^esub> a · (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · g y)"
using add_mult_distrib1 [
OF fx_gx_in_V sum_closed insert.prems (1)] by auto
also have "… = a · f x · g x ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. a· f y · g y)"
proof -
have f1: "f ∈ X -> carrier K" using insert.prems(2) by auto
have g1: "g ∈ X -> carrier V" using insert.prems(3) by auto
show ?thesis
unfolding insert.hyps (3) [OF insert.prems (1) f1 g1] ..
qed
also have "… = (\<Oplus>\<^bsub>V\<^esub>y∈insert x X. a · f y · g y)"
proof (rule finsum_insert[symmetric])
show "finite X" using insert.hyps(1) .
show "x ∉ X" using insert.hyps(2) .
show "(λy. a · f y · g y) ∈ X -> carrier V"
proof (unfold Pi_def, auto)
fix y
assume y_in_X: "y∈ X"
show "a · f y · g y ∈ carrier V"
proof (rule mult_closed)
show "f y · g y ∈ carrier V"
using y_in_X and insert.prems(1, 2, 3) and mult_closed
by auto
show "a ∈ carrier K" by (rule insert.prems(1))
qed
qed
show" a · f x · g x ∈ carrier V"
proof (rule mult_closed)
show "f x · g x ∈ carrier V"
using insert.prems (1, 2, 3) and mult_closed by auto
show "a ∈ carrier K" by (rule insert.prems(1))
qed
qed
finally show ?thesis .
qed
qed
end
context finite_dimensional_vector_space
begin
text{*The following functions are the candidates to be proved to define
the isomorphism between the vector spaces @{term V} and @{term "K_n dimension"}.
They have to be proved to be linear maps between the vector spaces,
and inverse one of each other.*}
definition iso_K_n_V :: "'a vector => 'c"
where "iso_K_n_V x = finsum V (λi. fst x i · indexing_X i) {..<dimension}"
definition iso_V_K_n :: "'c => 'a vector"
where "iso_V_K_n x =
finsum (K_n dimension) (λi. (K_n_scalar_product (lin_comb (x) (indexing_X i)) (x_i i dimension))) {..<dimension}"
text{*We prove that @{term "iso_K_n_V"} is a linear map, this means
both additive and homogeneous:*}
lemma linear_map_iso_K_n_V: "K_n_V.linear_map iso_K_n_V"
proof (unfold K_n_V.linear_map_def, intro conjI)
show "additivity iso_K_n_V"
proof (unfold additivity_def, rule ballI, rule ballI)
fix x y
assume x: "x ∈ carrier (K_n dimension)"
and y: "y ∈ carrier (K_n dimension)"
show "iso_K_n_V (x ⊕\<^bsub>K_n dimension\<^esub> y) =
iso_K_n_V x ⊕\<^bsub>V\<^esub> iso_K_n_V y"
proof -
have "iso_K_n_V (x ⊕\<^bsub>field.K_n K dimension\<^esub> y) =
(\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst (x ⊕\<^bsub>K_n dimension\<^esub> y) i · indexing_X i) "
unfolding iso_K_n_V_def ..
also have "... = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. (ith x i ⊕ ith y i) · indexing_X i)"
unfolding K_n_def K_n_add_def by force
also have "... = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. (ith x i) · indexing_X i ⊕\<^bsub>V\<^esub>
(ith y i) · indexing_X i)"
proof (rule finsum_cong')
show "{..<dimension} = {..<dimension}" by fastsimp
show "(λi. ith x i · indexing_X i ⊕\<^bsub>V\<^esub> ith y i · indexing_X i)
∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
find_theorems "ith ?x ?i ∈ _"
show "ith x xa · indexing_X xa ⊕\<^bsub>V\<^esub> ith y xa · indexing_X xa ∈ carrier V"
proof (rule V.a_closed)
show "ith x xa · indexing_X xa ∈ carrier V"
proof (rule mult_closed)
show "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V [of xa] xa by fastsimp
show "ith x xa ∈ carrier K"
apply (rule ith_closed [of _ _ dimension])
using x xa unfolding K_n_def by simp_all
qed
show "ith y xa · indexing_X xa ∈ carrier V"
proof (rule mult_closed)
show "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V [of xa] xa by fastsimp
show "ith y xa ∈ carrier K"
apply (rule ith_closed [of _ _ dimension])
using y xa unfolding K_n_def by simp_all
qed
qed
qed
fix xa assume xa: "xa ∈ {..<dimension}"
show "(ith x xa ⊕ ith y xa) · indexing_X xa =
ith x xa · indexing_X xa ⊕\<^bsub>V\<^esub> ith y xa · indexing_X xa"
proof (rule add_mult_distrib2)
show "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V [of xa] xa by fastsimp
show "ith x xa ∈ carrier K"
apply (rule ith_closed [of _ _ dimension])
using x xa unfolding K_n_def by simp_all
show "ith y xa ∈ carrier K"
apply (rule ith_closed [of _ _ dimension])
using y xa unfolding K_n_def by simp_all
qed
qed
also have "... = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i ⊕\<^bsub>V\<^esub> fst y i · indexing_X i)"
unfolding ith_def ..
also have "... = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i) ⊕\<^bsub>V\<^esub>
(\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst y i · indexing_X i)"
proof (cases dimension)
case 0 show ?thesis unfolding 0 by simp
next
case (Suc n)
show ?thesis
unfolding Suc
unfolding lessThan_Suc_atMost
proof (rule V.finsum_add [of "(λi. fst x i · indexing_X i)" n
"(λi. fst y i · indexing_X i)"])
show "(λi. fst x i · indexing_X i) ∈ {..n} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..n}"
show "fst x xa · indexing_X xa ∈ carrier V"
proof (rule mult_closed)
show "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V [of xa] xa using Suc by fastsimp
show "fst x xa ∈ carrier K"
apply (unfold ith_def [symmetric])
apply (rule ith_closed [of _ _ dimension])
using x xa unfolding K_n_def using Suc by simp_all
qed
qed
show "(λi. fst y i · indexing_X i) ∈ {..n} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..n}"
show "fst y xa · indexing_X xa ∈ carrier V"
proof (rule mult_closed)
show "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V [of xa] xa using Suc by fastsimp
show "fst y xa ∈ carrier K"
apply (unfold ith_def [symmetric])
apply (rule ith_closed [of _ _ dimension])
using y xa unfolding K_n_def using Suc by simp_all
qed
qed
qed
qed
also have "... = iso_K_n_V x ⊕\<^bsub>V\<^esub> iso_K_n_V y"
unfolding iso_K_n_V_def ..
finally show ?thesis .
qed
qed
show "homogeneity iso_K_n_V"
proof (unfold homogeneity_def, rule ballI, rule ballI)
fix k x
assume k: "k ∈ carrier K" and x: "x ∈ carrier (K_n dimension)"
show "iso_K_n_V (K_n_scalar_product k x) = k · iso_K_n_V x"
proof -
have "iso_K_n_V (K_n_scalar_product k x) =
(\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. (k ⊗ fst x i) · indexing_X i)"
unfolding iso_K_n_V_def K_n_scalar_product_def fst_conv ith_def ..
also have "... = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. k · (fst x i) · indexing_X i)"
proof (rule finsum_cong')
show "{..<dimension} = {..<dimension}" ..
show "(λi. k · fst x i · indexing_X i) ∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
hence fst: "fst x xa ∈ carrier K"
and i: "indexing_X xa ∈ carrier V" using x xa
using indexing_X_n_in_carrier_V [of xa] xa
unfolding K_n_def K_n_carrier_def ith_def by auto
show "k · fst x xa · indexing_X xa ∈ carrier V"
unfolding mult_assoc [symmetric, OF i k fst]
by (rule mult_closed [OF i m_closed [OF k fst]])
qed
fix xa assume xa: "xa ∈ {..<dimension}"
hence fst: "fst x xa ∈ carrier K"
and i: "indexing_X xa ∈ carrier V" using x xa
using indexing_X_n_in_carrier_V [of xa] xa
unfolding K_n_def K_n_carrier_def ith_def by auto
show "(k ⊗ fst x xa) · indexing_X xa = k · fst x xa · indexing_X xa"
by (rule mult_assoc [OF i k fst])
qed
also have "... = k · (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. (fst x i) · indexing_X i)"
proof (rule finsum_aux2 [symmetric])
show "finite {..<dimension}" by simp
show "k ∈ carrier K" by (rule k)
show "fst x ∈ {..<dimension} -> carrier K"
using x
unfolding K_n_def K_n_carrier_def ith_def by auto
show "indexing_X ∈ {..<dimension} -> carrier V"
using indexing_X_n_in_carrier_V by auto
qed
also have "... = k · iso_K_n_V x"
unfolding iso_K_n_V_def ..
finally show ?thesis .
qed
qed
qed
text{*The following lemma states that the function @{term lin_comb} satisfies
the additivity condition. It will be later used to prove that the function
@{term iso_V_K_n} is also an additive function.*}
lemma
lin_comb_additivity:
assumes x: "x ∈ carrier V"
and y: "y ∈ carrier V"
shows "lin_comb (x ⊕\<^bsub>V\<^esub> y) = (λi. lin_comb x i ⊕ lin_comb y i)"
apply (subst lin_comb_def)
proof (rule the1_equality)
show "∃!f. f ∈ coefficients_function X ∧ linear_combination f X = x ⊕\<^bsub>V\<^esub> y"
using linear_combination_unique [OF V.a_closed [OF x y]] .
next
show "(λi. lin_comb x i ⊕ lin_comb y i) ∈ coefficients_function X ∧
linear_combination (λi. lin_comb x i ⊕ lin_comb y i) X = x ⊕\<^bsub>V\<^esub> y"
proof (rule conjI)
show "(λi. lin_comb x i ⊕ lin_comb y i) ∈ coefficients_function X"
using lin_comb_is_coefficients_function [OF x]
using lin_comb_is_coefficients_function [OF y]
unfolding coefficients_function_def by auto
show "linear_combination (λi. lin_comb x i ⊕ lin_comb y i) X = x ⊕\<^bsub>V\<^esub> y"
proof -
have "linear_combination (λi. lin_comb x i ⊕ lin_comb y i) X =
(\<Oplus>\<^bsub>V\<^esub>ya∈X. (lin_comb x ya ⊕ lin_comb y ya) · ya)"
unfolding linear_combination_def ..
also have "... = (\<Oplus>\<^bsub>V\<^esub>ya∈X. (lin_comb x ya · ya) ⊕\<^bsub>V\<^esub> (lin_comb y ya · ya))"
proof (rule finsum_cong')
show "X = X" ..
show "(λya. lin_comb x ya · ya ⊕\<^bsub>V\<^esub> lin_comb y ya · ya) ∈ X -> carrier V"
using lin_comb_is_coefficients_function [OF x]
using lin_comb_is_coefficients_function [OF y]
unfolding coefficients_function_def
using mult_closed using good_set_X
unfolding good_set_def by blast
fix i
assume i: "i ∈ X"
show "(lin_comb x i ⊕ lin_comb y i) · i = lin_comb x i · i ⊕\<^bsub>V\<^esub> lin_comb y i · i"
using add_mult_distrib2
using lin_comb_is_coefficients_function [OF x]
using lin_comb_is_coefficients_function [OF y]
unfolding coefficients_function_def
using mult_closed i using good_set_X
unfolding good_set_def by blast
qed
also have "... = (\<Oplus>\<^bsub>V\<^esub>ya∈X. (lin_comb x ya · ya)) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>ya∈X. (lin_comb y ya · ya))"
using V.finsum_addf [OF finite_X,
of "(λi. lin_comb x i · i)" "(λi. lin_comb y i · i)"]
using lin_comb_is_coefficients_function [OF x]
using lin_comb_is_coefficients_function [OF y]
unfolding coefficients_function_def
using mult_closed using good_set_X
unfolding good_set_def by blast
also have "... = linear_combination (lin_comb x) X ⊕\<^bsub>V\<^esub> linear_combination (lin_comb y) X"
unfolding linear_combination_def [symmetric] ..
also have "... = x ⊕\<^bsub>V\<^esub> y"
unfolding lin_comb_is_the_linear_combination [symmetric, OF x]
unfolding lin_comb_is_the_linear_combination [symmetric, OF y] ..
finally show ?thesis .
qed
qed
qed
end
context vector_space
begin
lemma
finsum_mult_assocf:
assumes x1: "X ⊆ carrier V"
and x2: "finite X"
and k: "k ∈ carrier K"
and f: "f ∈ X -> carrier K"
and g: "g ∈ X -> carrier V"
shows "(\<Oplus>\<^bsub>V\<^esub>y∈X. (k ⊗ f y) · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · g y)"
using x2 x1 f g proof (induct X)
case empty
show ?case
using scalar_mult_zeroV_is_zeroV [OF k] by simp
next
case (insert x F)
have F: "F ⊆ carrier V" using insert.prems (1) by simp
have f: "f ∈ F -> carrier K" and g: "g ∈ F -> carrier V"
and kfg: "(λy. (k ⊗ f y) · g y) ∈ F -> carrier V"
and fg: "(λy. f y · g y) ∈ F -> carrier V"
and kfgx: "(k ⊗ f x) · g x ∈ carrier V"
and fgx: "f x · g x ∈ carrier V"
and fx: "f x ∈ carrier K" and gx: "g x ∈ carrier V"
using insert.prems (2,3) k
using mult_closed by blast+
have finsum_closed: "(\<Oplus>\<^bsub>V\<^esub>y∈F. (f y · g y)) ∈ carrier V"
by (rule finsum_closed [OF insert.hyps (1) fg])
have hypo :"(\<Oplus>\<^bsub>V\<^esub>y∈F. (k ⊗ f y) · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈F. f y · g y)"
using insert.hyps (3) [OF F f g] .
show ?case thm insert.hyps (2)
unfolding finsum_insert [OF insert.hyps (1,2) kfg, OF kfgx]
unfolding finsum_insert [OF insert.hyps (1,2) fg, OF fgx]
unfolding add_mult_distrib1 [OF fgx finsum_closed k]
unfolding mult_assoc [OF gx k fx]
unfolding hypo ..
qed
lemma
finsum_mult_assoc:
assumes k: "k ∈ carrier K"
and f: "f ∈ {..n} -> carrier K"
and g: "g ∈ {..n} -> carrier V"
shows "(\<Oplus>\<^bsub>V\<^esub>y∈{..n::nat}. (k ⊗ f y) · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. f y · g y)"
using f g proof (induct n)
case 0
show ?case
proof -
have "(\<Oplus>\<^bsub>V\<^esub>y∈{..0}. (k ⊗ f y) · g y) = (\<Oplus>\<^bsub>V\<^esub>y∈{0}. (k ⊗ f y) · g y)" by simp
also have "... = (k ⊗ f 0) · g 0 ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{}. (k ⊗ f y) · g y)"
apply (rule finsum_insert [of "{}" "0::nat" "(λi. (k ⊗ f i) · g i)"])
using "0.prems" k using mult_closed [of "g 0" "k ⊗ f 0"] by auto
also have "... = (k ⊗ f 0) · g 0"
unfolding finsum_empty
using r_zero [OF mult_closed [of "g 0" "k ⊗ f 0"]]
using "0.prems" k by auto
finally have lhs: "(\<Oplus>\<^bsub>V\<^esub>y∈{..0}. (k ⊗ f y) · g y) = (k ⊗ f 0) · g 0" .
have "k · (\<Oplus>\<^bsub>V\<^esub>y∈{..0}. f y · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈{0}. f y · g y)" by simp
also have "... = k · (f 0 · g 0 ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{}. f y · g y))"
using finsum_insert [of "{}" "0::nat" "(λi. f i · g i)"]
using "0.prems" k using mult_closed [of "g 0" "f 0"] by fastsimp
also have "... = k · (f 0 · g 0 ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>)"
unfolding finsum_empty ..
also have "... = k · (f 0 · g 0)"
using r_zero [OF mult_closed [of "g 0" "f 0"]]
using "0.prems" by force
also have "... = (k ⊗ f 0) · g 0"
using mult_assoc [symmetric]
using "0.prems" k using mult_closed [of "g 0" "f 0"] by auto
finally have rhs: "k · (\<Oplus>\<^bsub>V\<^esub>y∈{..0}. f y · g y) = (k ⊗ f 0) · g 0" .
show ?case
unfolding lhs rhs ..
qed
next
case (Suc n)
have f: "f ∈ {..n} -> carrier K" and g: "g ∈ {..n} -> carrier V"
and fSuc: "f (Suc n) ∈ carrier K" and gSuc: "g (Suc n) ∈ carrier V"
and fgSuc: "f (Suc n) · g (Suc n) ∈ carrier V"
using Suc.prems using mult_closed by auto
have fg: "(λi. f i · g i) ∈ {..n} -> carrier V"
and kfg: "(λi. (k ⊗ f i) · g i) ∈ {..n} -> carrier V"
and kfgSuc: "(k ⊗ f (Suc n)) · g (Suc n) ∈ carrier V"
using Suc.prems f g k using mult_closed by blast+
have finsum_closed: "(\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (f y · g y)) ∈ carrier V"
using finsum_closed [OF _ fg] by fast
have hypo :"(\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (k ⊗ f y) · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. f y · g y)"
by (rule Suc.hyps [OF f g ])
show ?case
proof -
have "(\<Oplus>\<^bsub>V\<^esub>y∈{..Suc n}. (k ⊗ f y) · g y) = (\<Oplus>\<^bsub>V\<^esub>y∈insert (Suc n) {..n}. (k ⊗ f y) · g y)"
unfolding atMost_Suc ..
also have "... = (k ⊗ f (Suc n)) · g (Suc n) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (k ⊗ f y) · g y)"
using finsum_insert [OF _ _ kfg, of "Suc n"] using kfgSuc by fastsimp
finally have lhs: "(\<Oplus>\<^bsub>V\<^esub>y∈{..Suc n}. (k ⊗ f y) · g y) =
(k ⊗ f (Suc n)) · g (Suc n) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (k ⊗ f y) · g y)" .
have "k · (\<Oplus>\<^bsub>V\<^esub>y∈{..Suc n}. f y · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈insert (Suc n) {..n}. (f y · g y))"
unfolding atMost_Suc ..
also have "... = k · (f (Suc n) · g (Suc n) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (f y · g y)))"
using finsum_insert [OF _ _ fg, of "Suc n"] using fgSuc by fastsimp
also have "... = k · f (Suc n) · g (Suc n) ⊕\<^bsub>V\<^esub> k · (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (f y · g y))"
unfolding add_mult_distrib1 [OF fgSuc finsum_closed k] ..
also have "... = (k ⊗ f (Suc n)) · g (Suc n) ⊕\<^bsub>V\<^esub> k · (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (f y · g y))"
unfolding mult_assoc [OF gSuc k fSuc] ..
also have "... = (k ⊗ f (Suc n)) · g (Suc n) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (k ⊗ f y) · g y)"
unfolding hypo ..
finally have rhs: "k · (\<Oplus>\<^bsub>V\<^esub>y∈{..Suc n}. f y · g y) =
(k ⊗ f (Suc n)) · g (Suc n) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈{..n}. (k ⊗ f y) · g y)" .
show ?case unfolding lhs rhs ..
qed
qed
lemma
finsum_mult_assoc_le:
assumes k: "k ∈ carrier K"
and f: "f ∈ {..<n} -> carrier K"
and g: "g ∈ {..<n} -> carrier V"
shows "(\<Oplus>\<^bsub>V\<^esub>y∈{..<n::nat}. (k ⊗ f y) · g y) = k · (\<Oplus>\<^bsub>V\<^esub>y∈{..<n}. f y · g y)"
proof (cases n)
case 0
show ?thesis unfolding 0 using scalar_mult_zeroV_is_zeroV [OF k] by simp
next
case (Suc k)
have f: "f ∈ {..k} -> carrier K" and g: "g ∈ {..k} -> carrier V"
using f g
unfolding Suc lessThan_Suc_atMost by fast+
show ?thesis
unfolding Suc
unfolding lessThan_Suc_atMost
using finsum_mult_assoc [OF k f g] .
qed
end
context finite_dimensional_vector_space
begin
text{*The following lemma states that the function @{term lin_comb} satisfies
the homogeneous property. It will be later used to prove that the function
@{term iso_V_K_n} is homogeneous:*}
lemma
lin_comb_homogeneity:
assumes k: "k ∈ carrier K"
and x: "x ∈ carrier V"
shows "lin_comb (k · x) = (λi. k ⊗ lin_comb x i)"
apply (subst lin_comb_def)
proof (rule the1_equality)
show "∃!f. f ∈ coefficients_function X ∧ linear_combination f X = k · x"
using linear_combination_unique [OF mult_closed [OF x k]] .
next
show "(λi. k ⊗ lin_comb x i) ∈ coefficients_function X ∧
linear_combination (λi. k ⊗ lin_comb x i) X = k · x"
proof (rule conjI)
show "(λi. k ⊗ lin_comb x i) ∈ coefficients_function X"
using lin_comb_is_coefficients_function [OF x]
unfolding coefficients_function_def
using k by auto
show "linear_combination (λi. k ⊗ lin_comb x i) X = k · x"
proof -
have "linear_combination (λi. k ⊗ lin_comb x i) X =
(\<Oplus>\<^bsub>V\<^esub>y∈X. (k ⊗ lin_comb x y) · y)"
unfolding linear_combination_def ..
also have "... = k · (\<Oplus>\<^bsub>V\<^esub>y∈X. (lin_comb x y) · y)"
apply (rule finsum_mult_assocf [OF _ finite_X k])
using lin_comb_is_coefficients_function [OF x]
using good_set_X
unfolding good_set_def coefficients_function_def by blast+
also have "... = k · x"
unfolding linear_combination_def [symmetric]
unfolding lin_comb_is_the_linear_combination [symmetric, OF x] ..
finally show ?thesis .
qed
qed
qed
end
context abelian_monoid
begin
lemma finsum_add':
assumes f: "f ∈ {..<n} -> carrier G"
and g: "g ∈ {..<n} -> carrier G"
shows "(\<Oplus>i∈{..<n::nat}. f i ⊕ g i) = finsum G f {..<n} ⊕ finsum G g {..<n}"
proof (cases n)
case 0
show ?thesis
unfolding 0 by force
next
case (Suc n)
show ?thesis
using f g unfolding Suc
unfolding lessThan_Suc_atMost
using finsum_add [of f n g] by fast
qed
end
context finite_dimensional_vector_space
begin
text{*The following lemma proves that the application @{term iso_V_K_n} is a linear
map between @{term V} and @{term "K_n dimension"}.*}
lemma linear_map_iso_V_K_n: "V_K_n.linear_map iso_V_K_n"
proof (unfold V_K_n.linear_map_def, intro conjI)
interpret field K by intro_locales
interpret K_n: vector_space K "K_n dimension" "K_n_scalar_product"
using vector_space_K_n .
show "V_K_n.additivity iso_V_K_n"
proof (unfold V_K_n.additivity_def, rule ballI, rule ballI)
fix x y assume x: "x ∈ carrier V" and y: "y ∈ carrier V"
show "iso_V_K_n (x ⊕\<^bsub>V\<^esub> y) = iso_V_K_n x ⊕\<^bsub>K_n dimension\<^esub> iso_V_K_n y"
proof -
have "iso_V_K_n (x ⊕\<^bsub>V\<^esub> y) =
(\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. (λn. lin_comb (x ⊕\<^bsub>V\<^esub> y) (indexing_X i) ⊗
(if n = i then \<one> else \<zero>), dimension - 1))"
unfolding iso_V_K_n_def K_n_scalar_product_def
ith_def vlen_def fst_conv snd_conv x_i_def ..
also have "... =
(\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}.
(λn. lin_comb x (indexing_X i) ⊗
(if n = i then \<one> else \<zero>), dimension - 1)
⊕\<^bsub>K_n dimension\<^esub>
(λn. lin_comb y (indexing_X i) ⊗
(if n = i then \<one> else \<zero>), dimension - 1))"
proof (rule K_n.finsum_cong')
show "{..<dimension} = {..<dimension}" ..
show "(λi. (λn. lin_comb x (indexing_X i) ⊗
(if n = i then \<one> else \<zero>), dimension - 1)
⊕\<^bsub>K_n dimension\<^esub>
(λn. lin_comb y (indexing_X i) ⊗
(if n = i then \<one> else \<zero>), dimension - 1))
∈ {..<dimension} -> carrier (K_n dimension)"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "(λn. lin_comb x (indexing_X xa) ⊗ (if n = xa then \<one> else \<zero>), dimension - 1)
⊕\<^bsub>K_n dimension\<^esub>
(λn. lin_comb y (indexing_X xa) ⊗ (if n = xa then \<one> else \<zero>), dimension - 1)
∈ carrier (K_n dimension)"
proof (rule K_n.a_closed)
have lx: "lin_comb x (indexing_X xa) ∈ carrier K"
and ly: "lin_comb y (indexing_X xa) ∈ carrier K"
using lin_comb_is_coefficients_function [OF x]
using lin_comb_is_coefficients_function [OF y]
using indexing_X_n_in_carrier_V [of xa] xa
unfolding coefficients_function_def by auto
show "(λn. lin_comb x (indexing_X xa) ⊗ (if n = xa then \<one> else \<zero>), dimension - 1)
∈ carrier (K_n dimension)"
unfolding K_n_def K_n_carrier_def ith_def vlen_def
using xa lx by auto
show "(λn. lin_comb y (indexing_X xa) ⊗ (if n = xa then \<one> else \<zero>), dimension - 1)
∈ carrier (K_n dimension)"
unfolding K_n_def K_n_carrier_def ith_def vlen_def
using xa ly by auto
qed
qed
fix i
assume i: "i ∈ {..<dimension}"
show "(λn. lin_comb (x ⊕\<^bsub>V\<^esub> y) (indexing_X i) ⊗ (if n = i then \<one> else \<zero>), dimension - 1) =
(λn. lin_comb x (indexing_X i) ⊗ (if n = i then \<one> else \<zero>), dimension - 1) ⊕\<^bsub>K_n dimension\<^esub>
(λn. lin_comb y (indexing_X i) ⊗ (if n = i then \<one> else \<zero>), dimension - 1)"
proof (unfold K_n_def K_n_add_def ith_def, simp, rule)
fix n
have lx: "lin_comb x (indexing_X i) ∈ carrier K"
and ly: "lin_comb y (indexing_X i) ∈ carrier K"
and lxy: "lin_comb (x ⊕\<^bsub>V\<^esub> y) (indexing_X i) ∈ carrier K"
using lin_comb_is_coefficients_function [OF x]
using lin_comb_is_coefficients_function [OF y]
using lin_comb_is_coefficients_function [OF V.a_closed [OF x y]]
using indexing_X_n_in_carrier_V [of i] i
unfolding coefficients_function_def by auto
show "lin_comb (x ⊕\<^bsub>V\<^esub> y) (indexing_X i) ⊗ (if n = i then \<one> else \<zero>) =
lin_comb x (indexing_X i) ⊗ (if n = i then \<one> else \<zero>) ⊕
lin_comb y (indexing_X i) ⊗ (if n = i then \<one> else \<zero>)"
proof (cases "n = i")
case False
show ?thesis using False lx ly lxy by simp
next
case True
show ?thesis using True lx ly lxy
apply simp
using lin_comb_additivity [OF x y] by presburger
qed
qed
qed
also have "... = (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}.
(λn. lin_comb x (indexing_X i) ⊗ (if n = i then \<one> else \<zero>), dimension - 1))
⊕\<^bsub>K_n dimension\<^esub>
(\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. (λn. lin_comb y (indexing_X i)
⊗ (if n = i then \<one> else \<zero>), dimension - 1))"
proof (rule K_n.finsum_add')
show "(λi. (λn. lin_comb x (indexing_X i) ⊗ (if n = i then \<one> else \<zero>), dimension - 1))
∈ {..<dimension} -> carrier (field.K_n K dimension)"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
have i: "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V xa by fast
have "lin_comb x ∈ coefficients_function (carrier V)"
using lin_comb_is_coefficients_function [OF x]
unfolding coefficients_function_def using good_set_X unfolding good_set_def by auto
thus "(λn. lin_comb x (indexing_X xa) ⊗ (if n = xa then \<one> else \<zero>), dimension - 1)
∈ carrier (field.K_n K dimension)"
using i xa
unfolding dimension_def
unfolding coefficients_function_def
unfolding K_n_def K_n_carrier_def ith_def vlen_def by force
qed
show "(λi. (λn. lin_comb y (indexing_X i) ⊗ (if n = i then \<one> else \<zero>), dimension - 1))
∈ {..<dimension} -> carrier (field.K_n K dimension)"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
have i: "indexing_X xa ∈ carrier V"
using indexing_X_n_in_carrier_V xa by fast
have cf_lc: "lin_comb x ∈ coefficients_function (carrier V)"
using lin_comb_is_coefficients_function [OF x]
unfolding coefficients_function_def using good_set_X unfolding good_set_def by auto
thus "(λn. lin_comb y (indexing_X xa) ⊗ (if n = xa then \<one> else \<zero>), dimension - 1)
∈ carrier (field.K_n K dimension)"
using i xa
unfolding dimension_def
unfolding coefficients_function_def
unfolding K_n_def K_n_carrier_def ith_def vlen_def
proof (auto)
show "lin_comb y (indexing_X xa) ⊗ \<one> ∈ carrier K"
by (metis coefficients_function_Pi i
lin_comb_is_coefficients_function m_closed one_closed y)
show "lin_comb y (indexing_X xa) ⊗ \<zero> ∈ carrier K"
by (metis K.add.one_closed coefficients_function_Pi i
lin_comb_is_coefficients_function m_closed y)
show "lin_comb y (indexing_X xa) ⊗ \<zero> = \<zero>"
by (metis coefficients_function_Pi i
lin_comb_is_coefficients_function r_null y)
qed
qed
qed
also have "... = iso_V_K_n x ⊕\<^bsub>field.K_n K dimension\<^esub> iso_V_K_n y"
unfolding iso_V_K_n_def K_n_scalar_product_def
ith_def vlen_def fst_conv snd_conv x_i_def ..
finally show ?thesis .
qed
qed
show "V_K_n.homogeneity iso_V_K_n"
proof (unfold V_K_n.homogeneity_def, rule ballI, rule ballI)
fix k x
assume k: "k ∈ carrier K" and x: "x ∈ carrier V"
show "iso_V_K_n (k · x) = K_n_scalar_product k (iso_V_K_n x)"
proof -
have "iso_V_K_n (k · x) =
(\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(lin_comb (k · x) (indexing_X i)) (x_i i dimension))"
unfolding iso_V_K_n_def ..
also have "... = (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(k ⊗ (lin_comb x (indexing_X i))) (x_i i dimension))"
proof (rule K_n.finsum_cong')
show "{..<dimension} = {..<dimension}" ..
show "(λi. K_n_scalar_product (k ⊗ lin_comb x (indexing_X i)) (x_i i dimension))
∈ {..<dimension} -> carrier (K_n dimension)"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "K_n_scalar_product (k ⊗ lin_comb x (indexing_X xa)) (x_i xa dimension)
∈ carrier (K_n dimension)"
proof (rule K_n_scalar_product_closed)
show "k ⊗ lin_comb x (indexing_X xa) ∈ carrier K"
using k lin_comb_is_coefficients_function [OF x]
unfolding coefficients_function_def
using indexing_X_n_in_carrier_V [of xa] xa by auto
show "x_i xa dimension ∈ carrier (K_n dimension)"
using x_i_closed xa by simp
qed
qed
fix i
assume i: "i ∈ {..<dimension}"
show "K_n_scalar_product (lin_comb (k · x) (indexing_X i)) (x_i i dimension) =
K_n_scalar_product (k ⊗ lin_comb x (indexing_X i)) (x_i i dimension)"
unfolding lin_comb_homogeneity [OF k x] ..
qed
also have "... = K_n_scalar_product k (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(lin_comb x (indexing_X i)) (x_i i dimension))"
apply (rule K_n.finsum_mult_assoc_le [OF k])
using k lin_comb_is_coefficients_function [OF x]
using indexing_X_n_in_carrier_V x_i_closed
unfolding coefficients_function_def by auto
also have "... = K_n_scalar_product k (iso_V_K_n x)"
unfolding iso_V_K_n_def [symmetric] ..
finally show ?thesis .
qed
qed
qed
end
lemma
lessThan_remove:
assumes i: "(i::nat) ∈ {..<k}"
shows "{..<k} = ({..<k} - {i}) ∪ {i}"
using i by blast
context finite_dimensional_vector_space
begin
text{*The functions @{term iso_K_n_V} and @{term iso_V_K_n} behave correctly
in their respective domains:*}
lemma iso_V_K_n_Pi: "iso_V_K_n ∈ carrier V -> carrier (K_n dimension)"
proof -
interpret K_n: vector_space K "K_n dimension" "K_n_scalar_product" using vector_space_K_n .
show ?thesis
proof
fix x assume x: "x ∈ carrier V"
show "iso_V_K_n x ∈ carrier (K_n dimension)"
unfolding iso_V_K_n_def
proof (rule K_n.finsum_closed)
show "finite {..<dimension}" by simp
show "(λi. K_n_scalar_product (lin_comb x (indexing_X i)) (field.x_i K i dimension))
∈ {..<dimension} -> carrier (K_n dimension)"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "K_n_scalar_product (lin_comb x (indexing_X xa)) (x_i xa dimension)
∈ carrier (K_n dimension)"
proof (rule K_n_scalar_product_closed)
show "lin_comb x (indexing_X xa) ∈ carrier K"
using lin_comb_is_coefficients_function [OF x]
using indexing_X_n_in_carrier_V xa
unfolding coefficients_function_def by auto
show "x_i xa dimension ∈ carrier (K_n dimension)"
using x_i_closed xa by simp
qed
qed
qed
qed
qed
lemma iso_K_n_V_Pi: shows "iso_K_n_V ∈ carrier (K_n dimension) -> carrier V"
proof -
interpret K_n: vector_space K "K_n dimension" "K_n_scalar_product" using vector_space_K_n .
show ?thesis
proof
fix x assume x: "x ∈ carrier (K_n dimension)"
show "iso_K_n_V x ∈ carrier V"
proof (unfold iso_K_n_V_def)
show "(\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i) ∈ carrier V"
proof (rule finsum_closed)
show "finite {..<dimension}" by simp
show "(λi. fst x i · indexing_X i) ∈ {..<dimension} -> carrier V"
using mult_closed
using indexing_X_n_in_carrier_V
using x unfolding K_n_def K_n_carrier_def ith_def vlen_def by auto
qed
qed
qed
qed
lemma
lin_comb_fimsum_candidate:
assumes x: "x ∈ carrier (K_n dimension)"
shows "(\<Oplus>\<^bsub>V\<^esub>y∈X. fst x (preim2_comp y) · y) = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i)"
proof (rule finsum_cong'' [of _ "indexing_X"])
show "finite {..<dimension}" by simp
show "bij_betw indexing_X {..<dimension} X" by (metis indexing_X_bij)
show "(λy. fst x (preim2_comp y) · y) ∈ X -> carrier V"
proof
fix xa assume xa: "xa ∈ X"
show "fst x (preim2_comp xa) · xa ∈ carrier V"
proof (rule mult_closed)
show "xa ∈ carrier V" using xa using good_set_X unfolding good_set_def by fast
show "fst x (preim2_comp xa) ∈ carrier K"
using preim2_comp_in_dimension [OF xa] x
unfolding K_n_def K_n_carrier_def ith_def vlen_def by auto
qed
qed
show "(λi. fst x i · indexing_X i) ∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "fst x xa · indexing_X xa ∈ carrier V"
proof (rule mult_closed)
show "indexing_X xa ∈ carrier V" using indexing_X_n_in_carrier_V xa by simp
show "fst x xa ∈ carrier K" using x xa
unfolding K_n_def K_n_carrier_def ith_def vlen_def by auto
qed
qed
show "!!xa. xa ∈ {..<dimension} =simp=>
fst x xa · indexing_X xa =
fst x (preim2_comp (indexing_X xa)) · indexing_X xa"
using preim2_comp_iso_nat_X_id
unfolding iso_nat_X_def by simp
qed
text{*The following lemma expresses how to write down the @{term lin_comb} of a finite sum
of the elements of the basis:*}
lemma
lin_comb_linear_combination_candidate:
assumes x: "x ∈ carrier (K_n dimension)"
shows "lin_comb (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i) = (λy. fst x (preim2_comp y))"
unfolding lin_comb_def
proof (rule the1_equality)
have finsum_closed: "(\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i) ∈ carrier V"
proof (rule finsum_closed)
show "finite {..<dimension}" by simp
show "(λi. fst x i · indexing_X i) ∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "fst x xa · indexing_X xa ∈ carrier V"
proof (rule mult_closed)
show "indexing_X xa ∈ carrier V" using indexing_X_n_in_carrier_V xa by simp
show "fst x xa ∈ carrier K" using x xa
unfolding K_n_def K_n_carrier_def ith_def vlen_def by auto
qed
qed
qed
show "∃!f. f ∈ coefficients_function X ∧
linear_combination f X = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i)"
by (rule linear_combination_unique [OF finsum_closed])
show "(λy. fst x (preim2_comp y)) ∈ coefficients_function X ∧
linear_combination (λy. fst x (preim2_comp y)) X = (\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i)"
proof (rule conjI)
show "linear_combination (λy. fst x (preim2_comp y)) X =
(\<Oplus>\<^bsub>V\<^esub>i∈{..<dimension}. fst x i · indexing_X i)"
using lin_comb_fimsum_candidate [OF x]
unfolding linear_combination_def .
show "(λy. fst x (preim2_comp y)) ∈ coefficients_function X"
unfolding coefficients_function_def
using preim2_comp_in_dimension
using x
unfolding K_n_def K_n_carrier_def ith_def vlen_def
unfolding preim2_comp_def by auto
qed
qed
text{*With the previous lemmas, we can now prove that @{term iso_V_K_n} is a bijection
between the correspoding carrier sets:*}
lemma iso_V_K_n_bij: shows "bij_betw iso_V_K_n (carrier V) (carrier (K_n dimension))"
proof (rule bij_betwI [of _ _ _ iso_K_n_V])
interpret K_n: vector_space K "K_n dimension" "K_n_scalar_product" using vector_space_K_n .
show "iso_V_K_n ∈ carrier V -> carrier (K_n dimension)" by (rule iso_V_K_n_Pi)
show "iso_K_n_V ∈ carrier (K_n dimension) -> carrier V" by (rule iso_K_n_V_Pi)
fix x assume x: "x ∈ carrier V"
show "iso_K_n_V (iso_V_K_n x) = x"
apply (subst (2) lin_comb_is_the_linear_combination_indexing [OF x])
unfolding iso_K_n_V_def
proof (rule finsum_cong')
show "{..<dimension} = {..<dimension}" by simp
show "(λi. lin_comb x (indexing_X i) · indexing_X i) ∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "lin_comb x (indexing_X xa) · indexing_X xa ∈ carrier V"
apply (rule mult_closed)
using indexing_X_n_in_carrier_V [of xa] xa
using lin_comb_is_coefficients_function [OF x]
unfolding coefficients_function_def by auto
qed
fix i assume i: "i ∈ {..<dimension}"
show "fst (iso_V_K_n x) i · indexing_X i =
lin_comb x (indexing_X i) · indexing_X i"
proof -
have "fst (iso_V_K_n x) i = fst (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(lin_comb x (indexing_X i)) (x_i i dimension)) i"
unfolding iso_V_K_n_def ..
also have "... = fst (λi. if i ∈ {..<dimension} then (lin_comb x (indexing_X i)) else \<zero>, dimension - 1) i"
proof -
have "(\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product (lin_comb x (indexing_X i)) (x_i i dimension)) =
(λi. if i ∈ {..<dimension} then (lin_comb x (indexing_X i)) else \<zero>, dimension - 1)"
apply (rule lambda_finsum [symmetric, of "dimension" "(λi. lin_comb x (indexing_X i))" "dimension"])
using lin_comb_is_coefficients_function [OF x]
using indexing_X_n_in_carrier_V
unfolding coefficients_function_def by auto
thus ?thesis by simp
qed
also have "... = (lin_comb x (indexing_X i))" using i by fastsimp
finally show ?thesis by simp
qed
qed
next
fix y
assume y: "y ∈ carrier (K_n dimension)"
show "iso_V_K_n (iso_K_n_V y) = y"
proof -
have "iso_V_K_n (iso_K_n_V y) = (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(lin_comb (iso_K_n_V y) (indexing_X i)) (x_i i dimension))" unfolding iso_V_K_n_def ..
also have "... = (λi. if i ∈ {..<dimension} then lin_comb (iso_K_n_V y) (indexing_X i) else \<zero>,
dimension - 1)"
proof (rule lambda_finsum [
symmetric, of "dimension" "(λi. (lin_comb (iso_K_n_V y) (indexing_X i)))" "dimension"])
show "dimension ≤ dimension" by fast
show "∀i∈{..<dimension}. lin_comb (iso_K_n_V y) (indexing_X i) ∈ carrier K"
proof (rule ballI)
fix i assume i: "i ∈ {..<dimension}"
have "lin_comb (iso_K_n_V y) ∈ {f. f ∈ carrier V -> carrier K}"
using lin_comb_is_coefficients_function [of "iso_K_n_V y"]
using iso_K_n_V_Pi y
unfolding coefficients_function_def
using good_set_X unfolding good_set_def by force
thus "lin_comb (iso_K_n_V y) (indexing_X i) ∈ carrier K"
using indexing_X_n_in_carrier_V i by auto
qed
qed
also have "... = (λi. if i ∈ {..<dimension} then fst y i else \<zero>, dimension - 1)"
proof (rule, rule conjI)
show "dimension - 1 = dimension - 1" by (rule refl)
show "(λi. if i ∈ {..<dimension} then lin_comb (iso_K_n_V y) (indexing_X i) else \<zero>) =
(λi. if i ∈ {..<dimension} then fst y i else \<zero>)"
proof
fix i
show "(if i ∈ {..<dimension} then lin_comb (iso_K_n_V y) (indexing_X i) else \<zero>) =
(if i ∈ {..<dimension} then fst y i else \<zero>)"
proof (cases "i ∈ {..<dimension}")
case False show ?thesis using False by simp
next
case True
have "lin_comb (iso_K_n_V y) (indexing_X i) = fst y i"
unfolding iso_K_n_V_def
unfolding lin_comb_linear_combination_candidate [OF y]
using preim2_comp_iso_nat_X_id [OF True]
unfolding iso_nat_X_def by simp
thus ?thesis by simp
qed
qed
qed
also have "... = y"
unfolding x_in_carrier [symmetric, OF y] by (rule refl)
finally show ?thesis by fast
qed
qed
lemma iso_K_n_V_bij: shows "bij_betw iso_K_n_V (carrier (K_n dimension)) (carrier V)"
proof (rule bij_betwI [of _ _ _ iso_V_K_n])
interpret K_n: vector_space K "K_n dimension" "K_n_scalar_product" using vector_space_K_n .
show "iso_V_K_n ∈ carrier V -> carrier (K_n dimension)" by (rule iso_V_K_n_Pi)
show "iso_K_n_V ∈ carrier (K_n dimension) -> carrier V" by (rule iso_K_n_V_Pi)
fix x assume x: "x ∈ carrier V"
show "iso_K_n_V (iso_V_K_n x) = x"
apply (subst (2) lin_comb_is_the_linear_combination_indexing [OF x])
unfolding iso_K_n_V_def
proof (rule finsum_cong')
show "{..<dimension} = {..<dimension}" by simp
show "(λi. lin_comb x (indexing_X i) · indexing_X i) ∈ {..<dimension} -> carrier V"
proof
fix xa assume xa: "xa ∈ {..<dimension}"
show "lin_comb x (indexing_X xa) · indexing_X xa ∈ carrier V"
apply (rule mult_closed)
using indexing_X_n_in_carrier_V [of xa] xa
using lin_comb_is_coefficients_function [OF x]
unfolding coefficients_function_def by auto
qed
fix i assume i: "i ∈ {..<dimension}"
show "fst (iso_V_K_n x) i · indexing_X i =
lin_comb x (indexing_X i) · indexing_X i"
proof -
have "fst (iso_V_K_n x) i = fst (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(lin_comb x (indexing_X i)) (x_i i dimension)) i"
unfolding iso_V_K_n_def ..
also have "... = fst (λi. if i ∈ {..<dimension} then (lin_comb x (indexing_X i)) else \<zero>, dimension - 1) i"
proof -
have "(\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product (lin_comb x (indexing_X i)) (x_i i dimension)) =
(λi. if i ∈ {..<dimension} then (lin_comb x (indexing_X i)) else \<zero>, dimension - 1)"
apply (rule lambda_finsum [symmetric, of "dimension" "(λi. lin_comb x (indexing_X i))" "dimension"])
using lin_comb_is_coefficients_function [OF x]
using indexing_X_n_in_carrier_V
unfolding coefficients_function_def by auto
thus ?thesis by simp
qed
also have "... = (lin_comb x (indexing_X i))" using i by fastsimp
finally show ?thesis by simp
qed
qed
next
fix y
assume y: "y ∈ carrier (K_n dimension)"
show "iso_V_K_n (iso_K_n_V y) = y"
proof -
have "iso_V_K_n (iso_K_n_V y) = (\<Oplus>\<^bsub>K_n dimension\<^esub>i∈{..<dimension}. K_n_scalar_product
(lin_comb (iso_K_n_V y) (indexing_X i)) (x_i i dimension))" unfolding iso_V_K_n_def ..
also have "... = (λi. if i ∈ {..<dimension} then lin_comb (iso_K_n_V y) (indexing_X i) else \<zero>,
dimension - 1)"
proof (rule lambda_finsum [
symmetric, of "dimension" "(λi. (lin_comb (iso_K_n_V y) (indexing_X i)))" "dimension"])
show "dimension ≤ dimension" by fast
show "∀i∈{..<dimension}. lin_comb (iso_K_n_V y) (indexing_X i) ∈ carrier K"
proof (rule ballI)
fix i assume i: "i ∈ {..<dimension}"
show "lin_comb (iso_K_n_V y) (indexing_X i) ∈ carrier K"
using iso_K_n_V_Pi using y
using lin_comb_is_coefficients_function [of "iso_K_n_V y"]
unfolding coefficients_function_def
using indexing_X_n_in_carrier_V i by force
qed
qed
also have "... = (λi. if i ∈ {..<dimension} then fst y i else \<zero>, dimension - 1)"
proof (rule, rule conjI)
show "dimension - 1 = dimension - 1" by (rule refl)
show "(λi. if i ∈ {..<dimension} then lin_comb (iso_K_n_V y) (indexing_X i) else \<zero>) =
(λi. if i ∈ {..<dimension} then fst y i else \<zero>)"
proof
fix i
show "(if i ∈ {..<dimension} then lin_comb (iso_K_n_V y) (indexing_X i) else \<zero>) =
(if i ∈ {..<dimension} then fst y i else \<zero>)"
proof (cases "i ∈ {..<dimension}")
case False show ?thesis using False by simp
next
case True
have "lin_comb (iso_K_n_V y) (indexing_X i) = fst y i"
unfolding iso_K_n_V_def
unfolding lin_comb_linear_combination_candidate [OF y]
using preim2_comp_iso_nat_X_id [OF True]
unfolding iso_nat_X_def by simp
thus ?thesis by simp
qed
qed
qed
also have "... = y"
unfolding x_in_carrier [symmetric, OF y] by (rule refl)
finally show ?thesis by fast
qed
qed
end
context linear_map
begin
definition vector_space_isomorphism :: "('c => 'e) => bool"
where "vector_space_isomorphism f == bij_betw f (carrier V) (carrier W) ∧ linear_map f"
end
context finite_dimensional_vector_space
begin
text{*Finally, the two following lemmas state the isomorphism
(in both directions actually) between @{term "K_n dimension"} and @{term "V"}:*}
lemma "V_K_n.vector_space_isomorphism iso_V_K_n"
using iso_V_K_n_bij using linear_map_iso_V_K_n
unfolding V_K_n.vector_space_isomorphism_def by rule
lemma "vector_space_isomorphism iso_K_n_V"
using iso_K_n_V_bij using linear_map_iso_K_n_V
unfolding vector_space_isomorphism_def by rule
end
end