Theory Dual_Spaces

theory Dual_Spaces
  imports Dimension_of_a_Subspace
begin

section{*Dual Spaces*}

context vector_space
begin

text{*This definition can be found also on Bauer's development,
  taking as the scalar field the set of real numbers, and with the 
  name of linear form. We follow linear functional as Halmos' text*}

text{*We split the definition of linear form into its multiplicative
  and additive components:*}

definition additive_functional :: "('b => 'a) => bool"
  where "additive_functional f 
  ≡ (∀x∈carrier V. ∀y∈carrier V. f (x ⊕\<^bsub>V\<^esub> y) = f x ⊕\<^bsub>K\<^esub> f y)"

definition multiplicative_functional :: "('b => 'a) => bool"
  where "multiplicative_functional f 
  ≡ (∀k∈carrier K. ∀x∈carrier V. f (k · x) = k ⊗\<^bsub>K\<^esub> (f x))"

definition linear_functional :: "('b => 'a) => bool"
  where "linear_functional f ≡ additive_functional f 
  ∧ multiplicative_functional f"

text{*The following lemma appears in Halmos (as the homogeneous property) 
  and also in Bauer's files; in Bauer there are also some properties about the 
  difference anf lineal functionals.*}

lemma linear_functional_zero:
  assumes "linear_functional f"
  shows "f \<zero>\<^bsub>V\<^esub> = \<zero>"
  sorry

text{*We introduce the definition of the dual space of the vector space @{text V}.
  We have to provide a carrier set, a zero operation and an addition. As the definition
  of abelian groups in Isabelle is done omver the ring type, we also have
  to provide some definition of unit and multiplication, that will be useless.*}

text{*The dual space is also denoted in Halmos  @{term V'}*}

definition dual_space :: "('b => 'a) ring" ("V'")
  where "dual_space = (| carrier = linear_functional,
                        mult = undefined,
                        one = undefined,
                        zero = (λx. \<zero>),
                        add = (λy1.λy2.λx. y1 x ⊕ y2 x)|)),"

text{*We create a synonim for the previous definition to ease
  readability:*}

lemmas V'_def = dual_space_def

term "vector_space K V'"

term "(λx f y. x ⊗ f y)"

text{*I guess it is not necessary to go down to finite dimensional vector spaces
  to prove the following lemma. If it is necessary, the context should be changed
  accordingly:*}

lemma vector_space_V': "vector_space K V' (λx f y. x ⊗ f y)"
(*The following command might be a good beginning:
  proof (unfold dual_space_def, unfold_locales, auto)*)
  sorry

end

end