Library LinAlg.LinAlg.vecspaces_verybasic


vecspaces_verybasic.v

Section MAIN.
Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Field_facts.
Require Export equal_syntax.
Require Export more_syntax.
Require Export Module_facts.

  • The definition of a vectorspace, and some very easy lemma's. This file is basically the book's Section 1.2

Section vecfielddef.

Definition vectorspace (F : field) : Type := MODULE F.
Definition VECSP (F : field) : category :=
  full_subcat (fun V : vectorspace F ⇒ V:MODULE F).

End vecfielddef.

Section jargon.
Variable F : field.
Variable V : vectorspace F.
Definition carrier := module_carrier.
Definition scalar_mult (a : F) (x : V) : V := a mX x.
  • Since scalar_mult is exactly the same as module_mult, ie mX, we will continue to use that notation instead
Definition scalar_mult_comp :
  ∀ (x x' : F) (y y' : carrier V),
  x =' x' in _ → y =' y' in _ → x mX y =' x' mX y' in _ :=
  MODULE_comp (R:=F) (Mod:=V).
Definition one_acts_as_unit : ∀ x : carrier V, one mX x =' x in _ :=
  MODULE_unit_l (R:=F) (Mod:=V).
Definition quasi_associativity :
  ∀ (a b : F) (x : carrier V), (a rX b) mX x =' a mX b mX x in _ :=
  MODULE_assoc (R:=F) (Mod:=V).
Definition distributivity :
  ∀ (a : F) (x y : carrier V), a mX (x +' y) =' a mX x +' a mX y in _ :=
  MODULE_dist_l (R:=F) (Mod:=V).
Definition distributivity' :
  ∀ (a b : F) (x : carrier V), (a +' b) mX x =' a mX x +' b mX x in _ :=
  MODULE_dist_r (R:=F) (Mod:=V).
End jargon.

Variable F : field.
Variable V : vectorspace F.
Hint Unfold carrier module_carrier.
Hint Resolve scalar_mult_comp distributivity distributivity': algebra.

Section Lemmas1.
  • ; the corollaries are immediate by construction/definition
Lemma vector_cancellation :
 ∀ x y z : V, x +' z =' y +' z in _ → x =' y in _.
intros.
apply GROUP_reg_right with z; auto with algebra.
Qed.

  • , split into several separate lemmas
Lemma Zero_times_a_vector_gives_zero :
 ∀ v : V, (zero F) mX v =' (zero V) in _.
auto with algebra.
Qed.

Lemma a_scalar_times_zero_gives_zero :
 ∀ f : F, f mX (zero V) =' (zero V) in _.
auto with algebra.
Qed.

Section Lemmas1_2.

Lemma Mince_minus1 :
 ∀ (f : F) (v : V), (min f) mX v =' (min f mX v) in _.
auto with algebra.
Qed.

Lemma Mince_minus2 :
 ∀ (f : F) (v : V), (min f mX v) =' f mX (min v) in _.
auto with algebra.
Qed.

Lemma Mince_minus3 :
 ∀ (f : F) (v : V), (min f) mX v =' f mX (min v) in _.
intros.
apply Trans with (min f mX v); auto with algebra.
Qed.

Lemma vecspace_op_reg_l :
 ∀ (f : F) (v : V),
 ¬ f =' (zero F) in _ → f mX v =' (zero V) in _ → v =' (zero V) in _.
intros.
apply Trans with (one mX v); auto with algebra.
apply Trans with ((field_inverse f rX f) mX v).
apply MODULE_comp; auto with algebra.
apply Sym; auto with algebra.
apply Trans with (field_inverse f mX f mX v); auto with algebra.
apply Trans with (field_inverse f mX (zero V)); auto with algebra.
Qed.

End Lemmas1_2.
End Lemmas1.

End MAIN.

Hint Resolve vector_cancellation Zero_times_a_vector_gives_zero
  a_scalar_times_zero_gives_zero Mince_minus1 Mince_minus2 Mince_minus3:
  algebra.