Theory Subspaces

theory Subspaces
  imports Isomorphism
begin

section{*Subspaces*}

context vector_space
begin

definition subspace :: "'b set => bool"
  where "subspace M == ((M ⊆ carrier V) ∧ M ≠ {} 
  ∧ (∀α∈carrier K. ∀β∈carrier K. ∀x∈M. ∀y∈M. 
  α · x ⊕\<^bsub>V\<^esub> β · y ∈ M))"

lemma
  zero_in_subspace:
  assumes s: "subspace M"
  shows "\<zero>\<^bsub>V\<^esub> ∈ M"
proof -
  obtain x where x: "x ∈ M" using s
    unfolding subspace_def by fast
  hence xV: "x ∈ carrier V" 
    using s unfolding subspace_def by fast
  have one: "\<one>\<^bsub>K\<^esub> ∈ carrier K" 
    and minus_one: "\<ominus> \<one>\<^bsub>K\<^esub> ∈ carrier K" by simp+
  hence "\<one>\<^bsub>K\<^esub> · x ⊕\<^bsub>V\<^esub> (\<ominus> \<one>\<^bsub>K\<^esub> · x) ∈ M" 
    using s x unfolding subspace_def by blast
  thus ?thesis 
    unfolding mult_1 [OF xV] negate_eq [OF xV]
    unfolding V.r_neg [OF xV] .
qed

text{*In the following statement we can observe the operation of 
  field updating for records:*}

lemma
  subspace_is_vector_space:
  assumes s: "subspace M"
  shows "vector_space K (V(|carrier:= M|)),) (op ·)"
proof (unfold_locales, auto)
  show "\<zero>\<^bsub>V\<^esub> ∈ M"
    by (metis assms zero_in_subspace)
  fix x and y and z
  assume x_in_M: "x ∈ M" 
    and y_in_M: "y ∈ M" 
    and z_in_M: "z ∈ M"
  hence x_in_V: "x ∈ carrier V" 
    and y_in_V: "y ∈ carrier V" 
    and z_in_V: "z ∈ carrier V"
    by (metis assms mem_def subsetD subspace_def)+
  show "x ⊕\<^bsub>V\<^esub> y ∈ M"
  proof -
    have "x ⊕\<^bsub>V\<^esub> y = \<one>·x ⊕\<^bsub>V\<^esub> \<one>·y"
      by (metis assms insert_absorb insert_subset 
        mult_1 subspace_def x_in_M y_in_M)
    also have "... ∈ M" 
      using s one_closed x_in_M y_in_M 
      unfolding subspace_def by fast
    finally show "x ⊕\<^bsub>V\<^esub> y ∈ M" .
  qed
  show "\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> x = x"
    by (metis V.add.l_one assms mem_def 
      subsetD subspace_def x_in_M)
  show "x ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub> = x"
    by (metis V.add.r_one assms mem_def 
      subsetD subspace_def x_in_M)
  show "x ⊕\<^bsub>V\<^esub> y = y ⊕\<^bsub>V\<^esub> x"
    by (metis V.a_comm x_in_V y_in_V)
  show "x ⊕\<^bsub>V\<^esub> y ⊕\<^bsub>V\<^esub> z = x ⊕\<^bsub>V\<^esub> (y ⊕\<^bsub>V\<^esub> z)"
    using a_assoc[OF x_in_V y_in_V z_in_V] .
  show "\<one> · x = x" using mult_1[OF x_in_V] .
  show "x ∈ Units (|carrier = M, mult = op ⊕\<^bsub>V\<^esub>, one = \<zero>\<^bsub>V\<^esub>|))," 
  proof -
    have "∃y ∈ M. x ⊕\<^bsub>V\<^esub> y = \<zero>\<^bsub>V\<^esub> ∧ y ⊕\<^bsub>V\<^esub> x = \<zero>\<^bsub>V\<^esub>"
    proof (rule bexI[of _ "\<ominus>\<^bsub>V\<^esub>x"], rule conjI)
      show "x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> x = \<zero>\<^bsub>V\<^esub>" using r_neg[OF x_in_V] .
      show "\<ominus>\<^bsub>V\<^esub> x ⊕\<^bsub>V\<^esub> x = \<zero>\<^bsub>V\<^esub>"
        by (metis V.add.l_inv x_in_V)
      show " \<ominus>\<^bsub>V\<^esub> x ∈ M" 
      proof -
        have "\<ominus>\<^bsub>V\<^esub> x = \<zero>\<^bsub>K\<^esub> · x ⊕\<^bsub>V\<^esub> (\<ominus>\<^bsub>K\<^esub>\<one>)· x"
          by (metis K.a_inv_closed K.add.l_one 
            K.add.one_closed add_mult_distrib2 
            negate_eq one_closed x_in_V)
        also have "... ∈ M"
          by (metis K.add.one_closed 
            abelian_group.a_inv_closed assms is_abelian_group
            one_closed subspace_def x_in_M)
        finally show ?thesis .
      qed
    qed
    thus ?thesis using x_in_M unfolding Units_def by force
  qed
  fix a and b
  assume a_in_K: "a ∈ carrier K" and b_in_K: "b ∈ carrier K"
  show "(a ⊗ b) · x = a · b · x"
    using mult_assoc[OF x_in_V a_in_K b_in_K] .
  show "a · x ∈ M"
  proof -
    have "a · x = a · x ⊕\<^bsub>V\<^esub> a · \<zero>\<^bsub>V\<^esub>"
      by (metis V.add.one_closed V.add.r_one 
        a_in_K add_mult_distrib1 x_in_V)
    also have "... ∈ M"
      by (metis `\<zero>\<^bsub>V\<^esub> ∈ M` a_in_K assms subspace_def x_in_M)
    finally show ?thesis .
  qed
  show "a · (x ⊕\<^bsub>V\<^esub> y) = a · x ⊕\<^bsub>V\<^esub> a · y" 
    using add_mult_distrib1[OF x_in_V y_in_V a_in_K] .
  show "(a ⊕ b) · x = a · x ⊕\<^bsub>V\<^esub> b · x" 
    using add_mult_distrib2[OF x_in_V a_in_K b_in_K] .
qed
  
lemma
  subspace_zero:
  shows "subspace {\<zero>\<^bsub>V\<^esub>}"
  unfolding subspace_def
  by (simp, metis mult_zero_descomposition 
    scalar_mult_zeroV_is_zeroV)

lemma subspace_V:
  shows "subspace (carrier V)"
  unfolding subspace_def
  by (simp, metis V.a_closed V.add.one_closed 
    ex_in_conv mult_closed)

text{*As one would expect, a subspace is closed under addition:*}

lemma subspace_add_closed:
  assumes s: "subspace S"
  and x: "x ∈ S" and y: "y ∈ S"
  shows "x ⊕\<^bsub>V\<^esub> y ∈ S"
proof -
  have xv: "x ∈ carrier V" and yv: "y ∈ carrier V"
    using x y s unfolding subspace_def by auto
  have "x ⊕\<^bsub>V\<^esub> y = \<one> · x ⊕\<^bsub>V\<^esub> \<one> · y" 
    using mult_1 [OF xv] mult_1 [OF yv] by simp
  thus ?thesis
    using s unfolding subspace_def by (metis one_closed x y)
qed

text{*The definition of @{term finsum} (see @{thm finsum_def}) is done in such a way
  hat for any infinite set it returns @{term undefined} and otherwise
  the result of a folding operator over the finite set. Under these 
  circumstances it seems rather hard to prove properties of subspaces considering
  infinite sums:*}
 
lemma subspace_finsum_closed:
  assumes s: "subspace S"
  and f: "finite S"
  and y: "Y ⊆ S"
  and c: "f ∈ Y -> carrier K"
  shows "finsum V (λi. f i · i) Y ∈ S"
proof -
  have fY: "finite Y" by (rule finite_subset [OF y f])
  show ?thesis
    using fY y c proof (induct Y)
    case empty
    show ?case 
      using zero_in_subspace [OF s] by simp
  next
    -- "Nice Isabelle feature: we can even interpret the locale vector space
      with the same vector space where only the carrier set has been modified.
      I thought that this may not be possible because it could produce some 
      problems, but it worked smoothly:"
    interpret S: vector_space K "V(|carrier := S|))," "op ·" 
      using subspace_is_vector_space [OF s] .
    case (insert x F)
    have finsum_S: "(\<Oplus>\<^bsub>V\<^esub>i∈F. f i · i) ∈ S"
      using insert.hyps (3) insert.prems by fast
    have fxS: "f x · x ∈ S"
      using insert.prems
      using s using S.mult_closed by auto
      have lambda: "(λi. f i · i) ∈ F -> carrier V" 
        and fx: "f x · x ∈ carrier V" 
        using insert.prems
      using insert.hyps
      using s unfolding subspace_def using mult_closed by blast+
    show ?case
      unfolding finsum_insert [OF insert.hyps (1,2) lambda, OF fx] 
      by (rule subspace_add_closed [OF s fxS finsum_S])
  qed
qed

lemma subspace_finsum_closed':
  assumes s: "subspace S"
  and f: "finite Y"
  and y: "Y ⊆ S"
  and c: "f ∈ Y -> carrier K"
  shows "finsum V (λi. f i · i) Y ∈ S"
using f y c
proof (induct Y)
  case empty
  show ?case 
    using zero_in_subspace [OF s] by simp
next
  interpret S: vector_space K "V(|carrier := S|))," "op ·" 
    using subspace_is_vector_space [OF s] .
  case (insert x F)
  have finsum_S: "(\<Oplus>\<^bsub>V\<^esub>i∈F. f i · i) ∈ S"
    using insert.hyps (3) insert.prems by fast
  have fxS: "f x · x ∈ S"
    using insert.prems
    using s using S.mult_closed by auto
  have lambda: "(λi. f i · i) ∈ F -> carrier V" 
    and fx: "f x · x ∈ carrier V" 
    using insert.prems
    using insert.hyps
    using s unfolding subspace_def using mult_closed by blast+
  show ?case
    unfolding finsum_insert [OF insert.hyps (1,2) lambda, OF fx] 
    by (rule subspace_add_closed [OF s fxS finsum_S])
qed


corollary subspace_linear_combination_closed:
  assumes s: "subspace S"
  and f: "finite Y"
  and y: "Y ⊆ S"
  and c: "f ∈ coefficients_function Y"
  shows "linear_combination f Y ∈ S"
  proof (unfold linear_combination_def, 
      rule subspace_finsum_closed')
   show "subspace S" using s .
   show "finite Y" using f .
   show "Y ⊆ S" using y .
   show "f ∈ Y -> carrier K" 
     using c unfolding coefficients_function_def by blast
qed
  

end

end