Theory Vector_Space

theory Vector_Space
imports Field2
begin

section{*Definition of Vector Space*}

text{*Here the definition of a vector space using locales and inherit. We need to fix
  a field, an abelian group and the scalar product relating both structures 
  (an abelian group together a field would be a vector space with
  one specific scalar product but not with another). A vector space is an 
  algebraic structure composed of a field,
  an abelian monoid and a scalar product which satisfies some properties.*}

locale vector_space = K: field K + V: abelian_group V
  for K (structure) and V (structure) +
  fixes scalar_product:: "'a => 'b => 'b" (infixr "·" 70)
  assumes mult_closed: "[|x ∈ carrier V;a ∈ carrier K|] 
  ==> a · x ∈ carrier V"
  and mult_assoc: "[|x ∈ carrier V; a ∈ carrier K; b ∈ carrier K |] 
  ==> (a ⊗\<^bsub>K\<^esub> b) · x = a · (b · x)"
  and mult_1: "[|x ∈ carrier V|] ==> \<one>\<^bsub>K\<^esub> · x = x"
  and add_mult_distrib1: 
  "[|x∈ carrier V; y ∈ carrier V; a ∈ carrier K|]
  ==> a · (x ⊕\<^bsub>V\<^esub> y)= a·x ⊕\<^bsub>V\<^esub> a·y"
  and add_mult_distrib2: 
  "[|x∈ carrier V; a ∈ carrier K; b ∈ carrier K|] 
  ==> (a ⊕\<^bsub>K\<^esub> b) · x = a·x ⊕\<^bsub>V\<^esub> b·x"

text{*Using this lemma we can check if an algebraic structure is a vector space*}
lemma vector_spaceI: 
  fixes K (structure) and V (structure) 
  and scalar_product ::"'a => 'b => 'b" (infixr "·" 70)
  assumes field_K: "field K"
  and abelian_group_V: "abelian_group V"
  and mult_closed: 
  "!!x a. [|x ∈ carrier V;a ∈ carrier K|] ==> a·x ∈ carrier V"
  and mult_assoc: 
  "!!x a b. [| x ∈ carrier V; a ∈ carrier K; b ∈ carrier K |] 
  ==> (a ⊗\<^bsub>K\<^esub> b)· x = a · (b · x)"
  and mult_1: "!!x. [|x ∈ carrier V|] ==> \<one>\<^bsub>K\<^esub> · x = x"
  and add_mult_distrib1: 
  "!!x y a. [|x∈ carrier V; y ∈ carrier V; a ∈ carrier K|]
  ==> a·(x ⊕\<^bsub>V\<^esub> y)= a·x ⊕\<^bsub>V\<^esub> a· y"
  and add_mult_distrib2: 
  "!!x a b. [|x∈ carrier V; a ∈ carrier K; b ∈ carrier K|]
  ==> (a ⊕\<^bsub>K\<^esub> b)· x = a·x ⊕\<^bsub>V\<^esub> b·x"
  shows "vector_space K V scalar_product"
proof (unfold vector_space_def, intro conjI)
  show "field K" using field_K .
  show "abelian_group V" using abelian_group_V .
next
  show "vector_space_axioms K V scalar_product"
    by (auto intro: vector_space.intro abelian_group.intro 
    field.intro vector_space_axioms.intro assms)
qed

end