Basic theory of vector spaces.

The same structure is called either module or vector space
depending on whether the scalars are commutive ring or field.
Since the scalars are parameter of our definition, we call them both
vector spaces. Most (if not all) of the theorems proved here assume only
commutative ring of scalars, so they are theorems about modules.

The axiom of choice (in set theory) proves that every vector space has
basis, so every vector space is (isomorphic to) free vector space.
But that is not true constructively.

We can construct free vector spaces (and modules) with any "set" (i.e. type)
of generators and coefficents (scalars) K  (a commutative ring)
(see free-vs-property)
We can construct the free vector space without assuming that either the
generators or the scalars have decidable equality.
To make that work we need to "formally" remove zeros and combine coefficients
for the same generator using an equivalence relation.
(see bfs-equiv and bfs-reduce)..

Definition: vs-point
Point(vs) ==  vs."Point"

Definition: vector-space
VectorSpace(K) ==
  "+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
       (∀x,y,z:Point(self).  ((f (f z)) (f (f y) z) ∈ Point(self)))
       ∧ (∀x,y:Point(self).  ((f y) (f x) ∈ Point(self)))} 
  "*":{m:|K| ⟶ Point(self) ⟶ Point(self)| 
       (∀a:|K|. ∀x,y:Point(self).  ((m (self."+" y)) (self."+" (m x) (m y)) ∈ Point(self)))
       ∧ (∀x:Point(self)
            (((m x) x ∈ Point(self))
            ∧ ((m x) self."0" ∈ Point(self))
            ∧ (∀a,b:|K|.  ((m (m x)) (m (a b) x) ∈ Point(self)))
            ∧ (∀a,b:|K|.  ((m (a +K b) x) (self."+" (m x) (m x)) ∈ Point(self)))))} 

Lemma: vector-space_wf
K:RngSig. (VectorSpace(K) ∈ 𝕌')

Lemma: vs-point_wf
[K:RngSig]. ∀[vs:VectorSpace(K)].  (Point(vs) ∈ Type)

Definition: vs-0
==  vs."0"

Lemma: vs-0_wf
[K:RngSig]. ∀[vs:VectorSpace(K)].  (0 ∈ Point(vs))

Definition: vs-add
==  vs."+" y

Lemma: vs-add_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y:Point(vs)].  (x y ∈ Point(vs))

Lemma: vs-add-comm-nu
K:RngSig. ∀vs:VectorSpace(K). ∀x,y:Point(vs).  (x x ∈ Point(vs))

Lemma: vs-add-comm
K:RngSig. ∀vs:VectorSpace(K). ∀x,y:Point(vs).  (x x ∈ Point(vs))

Lemma: vs-add-assoc
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)].  (x z ∈ Point(vs))

Lemma: vs-mon_assoc
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)].  (x z ∈ Point(vs))

Lemma: vs-ac_1
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)].  (x z ∈ Point(vs))

Definition: vs-mul
==  vs."*" x

Lemma: vs-mul_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a:|K|]. ∀[y:Point(vs)].  (a y ∈ Point(vs))

Lemma: vs-mul-linear
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a:|K|]. ∀[x,y:Point(vs)].  (a y ∈ Point(vs))

Lemma: vs-mul-mul
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a,b:|K|]. ∀[x:Point(vs)].  (a x ∈ Point(vs))

Lemma: vs-mul-add
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a,b:|K|]. ∀[x:Point(vs)].  (a +K x ∈ Point(vs))

Lemma: vs-mul-one
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (1 x ∈ Point(vs))

Lemma: vs-mul-zero
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (0 0 ∈ Point(vs))

Lemma: vs-zero-add
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (0 x ∈ Point(vs))

Lemma: vs-mon_ident
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  ((x x ∈ Point(vs)) ∧ (0 x ∈ Point(vs)))

Definition: vs-neg
-(x) ==  -K x

Lemma: vs-neg_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (-(x) ∈ Point(vs))

Lemma: vs-add-neg
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (x -(x) 0 ∈ Point(vs))

Lemma: vs-neg-add
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (-(x) 0 ∈ Point(vs))

Lemma: vs-grp_inverse
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  ((x -(x) 0 ∈ Point(vs)) ∧ (-(x) 0 ∈ Point(vs)))

Lemma: vs-add-cancel
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)].  (x z ∈ Point(vs) ⇐⇒ y ∈ Point(vs))

Lemma: vs-cancel-add
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)].  (z y ∈ Point(vs) ⇐⇒ y ∈ Point(vs))

Lemma: vs-neg-zero
[K:Rng]. ∀[vs:VectorSpace(K)].  (-(0) 0 ∈ Point(vs))

Lemma: vs-neg-neg
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (-(-(x)) x ∈ Point(vs))

Lemma: vs-neg-add2
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x,y:Point(vs)].  (-(x y) -(y) -(x) ∈ Point(vs))

Lemma: vs-zero-mul
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[k:|K|].  (k 0 ∈ Point(vs))

Lemma: vs-grp_inv_assoc
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[a,b:Point(vs)].  ((a -(a) b ∈ Point(vs)) ∧ (-(a) b ∈ Point(vs)))

Definition: vs-bag-add
Σ{f[b] b ∈ bs} ==  Σ(b∈bs). f[b]

Lemma: vs-bag-add_wf
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[bs:bag(S)].  {f[b] b ∈ bs} ∈ Point(vs))

Lemma: vs_bag_add_empty_lemma
f,vs:Top.  {f b ∈ {}} 0)

Lemma: vs-bag-add-map
[vs:Top]. ∀[S:Type]. ∀[f,g:Top]. ∀[bs:bag(S)].  {f[b] b ∈ bag-map(g;bs)} ~ Σ{f[g b] b ∈ bs})

Lemma: vs-bag-add-append
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[bs,cs:bag(S)].
  {f[b] b ∈ bs cs} = Σ{f[b] b ∈ bs} + Σ{f[b] b ∈ cs} ∈ Point(vs))

Lemma: vs-bag-add-mul
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[bs:bag(S)]. ∀[k:|K|].
  (k * Σ{f[b] b ∈ bs} = Σ{k f[b] b ∈ bs} ∈ Point(vs))

Lemma: vs-bag-add-add
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f,g:S ⟶ Point(vs)]. ∀[bs:bag(S)].
  {f[b] g[b] b ∈ bs} = Σ{f[b] b ∈ bs} + Σ{g[b] b ∈ bs} ∈ Point(vs))

Lemma: vs-double-bag-add
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ bag(A[x])]. ∀[h:x:T ⟶ A[x] ⟶ Point(vs)].
  {h[x;y] y ∈ f[x]} x ∈ b} = Σ{h[fst(p);snd(p)] p ∈ ⋃x∈b.bag-map(λy.<x, y>;f[x])} ∈ Point(vs))

Definition: sum-in-vs
Σ{f[i] n≤i≤m} ==  Σ{f[i] i ∈ [n, 1)}

Lemma: sum-in-vs_wf
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f:{n..m 1-} ⟶ Point(vs)].  {f[i] n≤i≤m} ∈ Point(vs))

Lemma: empty-sum-in-vs
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f:Top].  Σ{f[i] n≤i≤m} 0 ∈ Point(vs) supposing m < n

Lemma: sum-in-vs-add
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f,g:{n..m 1-} ⟶ Point(vs)].
  {f[i] g[i] n≤i≤m} = Σ{f[i] n≤i≤m} + Σ{g[i] n≤i≤m} ∈ Point(vs))

Lemma: sum-in-vs-mul
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f:{n..m 1-} ⟶ Point(vs)]. ∀[k:|K|].
  (k * Σ{f[i] n≤i≤m} = Σ{k f[i] n≤i≤m} ∈ Point(vs))

Lemma: sum-in-vs-neg
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f:{n..m 1-} ⟶ Point(vs)].
  {-(f[i]) n≤i≤m} -(Σ{f[i] n≤i≤m}) ∈ Point(vs))

Lemma: sum-in-vs-split
[n,m,k:ℤ]. ∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[f:{n..m 1-} ⟶ Point(vs)].
  Σ{f[i] n≤i≤m} = Σ{f[i] n≤i≤k} + Σ{f[i] 1≤i≤m} ∈ Point(vs) supposing (n ≤ k) ∧ (k ≤ m)

Lemma: sum-in-vs-shift
[k,n,m:ℤ]. ∀[f,vs:Top].  {f[i] n≤i≤m} ~ Σ{f[i k] k≤i≤k})

Lemma: sum-in-vs-split-shift
[k,n,m:ℤ]. ∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[f:{n..m 1-} ⟶ Point(vs)].
  Σ{f[i] n≤i≤m} = Σ{f[i] n≤i≤k} + Σ{f[k 1] 0≤i≤1} ∈ Point(vs) supposing (n ≤ k) ∧ (k ≤ m)

Lemma: sum-in-vs-single
[n:ℤ]. ∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[f:{n..n 1-} ⟶ Point(vs)].  {f[i] n≤i≤n} f[n] ∈ Point(vs))

Lemma: sum-in-vs-const
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f:{n..m 1-} ⟶ |K|]. ∀[a:Point(vs)].
  {f[i] n≤i≤m} = Σ(K) n ≤ i < 1. f[i] a ∈ Point(vs))

Lemma: double-sum-in-vs
[n,m:ℤ]. ∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[l,u:{n..m 1-} ⟶ ℤ]. ∀[h:x:{n..m 1-} ⟶ {l[x]..u[x] 1-} ⟶ Point(vs)].
  {h[x;y] l[x]≤y≤u[x]} n≤x≤m}
  = Σ{h[fst(p);snd(p)] p ∈ ⋃x∈[n, 1).bag-map(λy.<x, y>;[l[x], u[x] 1))}
  ∈ Point(vs))

Definition: vs-lin-indep
vs-lin-indep(K;vs;v.P[v]) ==
  ∀n:ℕ. ∀f:ℕ1 ⟶ {v:Point(vs)| P[v]} .
     (∀c:ℕ1 ⟶ |K|. ((Σ{c 0≤i≤n} 0 ∈ Point(vs))  (∀i:ℕ1. ((c i) 0 ∈ |K|)))))

Lemma: vs-lin-indep_wf
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  (vs-lin-indep(K;vs;v.P[v]) ∈ ℙ)

Definition: mk-vs
Point= zero= x+y= +[x; y] a*u= *[a; u] ==  λx.x["Point" := V]["0" := z]["+" := λx,y. +[x; y]]["*" := λa,u. *[a; u]]

Lemma: mk-vs_wf
[K:RngSig]. ∀[V:Type]. ∀[z:V]. ∀[+:V ⟶ V ⟶ V]. ∀[*:|K| ⟶ V ⟶ V].
  Point= V
  zero= z
  x+y= +[x;y]
  a*u= *[a;u] ∈ VectorSpace(K) 
  supposing (∀x,y,z:V.  (+[x;+[y;z]] +[+[x;y];z] ∈ V))
  ∧ (∀x,y:V.  (+[x;y] +[y;x] ∈ V))
  ∧ (∀a:|K|. ∀x,y:V.  (*[a;+[x;y]] +[*[a;x];*[a;y]] ∈ V))
  ∧ (∀x:V. (*[1;x] x ∈ V))
  ∧ (∀x:V. (*[0;x] z ∈ V))
  ∧ (∀x:V. ∀a,b:|K|.  (*[a;*[b;x]] *[a b;x] ∈ V))
  ∧ (∀x:V. ∀a,b:|K|.  (*[a +K b;x] +[*[a;x];*[b;x]] ∈ V))

Definition: trivial-vs
==  Point= Unit zero= ⋅ x+y= ⋅ a*x= ⋅

Lemma: trivial-vs_wf
[K:RngSig]. (0 ∈ VectorSpace(K))

Definition: one-dim-vs
one-dim-vs(K) ==  Point= |K| zero= a+b= +K a*b= b

Lemma: one-dim-vs_wf
[K:Rng]. (one-dim-vs(K) ∈ VectorSpace(K))

Definition: int-vs
ℤ ==  Point= ℤ zero= a+b= a*b= b

Lemma: one-dim-int-vs
one-dim-vs(ℤ-rng) ~ ℤ

Lemma: int-vs_wf
ℤ ∈ VectorSpace(ℤ-rng)

Definition: vs-subspace
vs-subspace(K;vs;x.P[x]) ==
  P[0] ∧ (∀x,y:Point(vs).  (P[x]  P[y]  P[x y])) ∧ (∀x:Point(vs). ∀a:|K|.  (P[x]  P[a x]))

Lemma: vs-subspace_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  (vs-subspace(K;vs;x.P[x]) ∈ ℙ)

Lemma: vs-subspace_functionality
K:RngSig. ∀vs:VectorSpace(K).
  ∀[P,Q:Point(vs) ⟶ ℙ].  ((∀x:Point(vs). (P[x] ⇐⇒ Q[x]))  {vs-subspace(K;vs;x.P[x])  vs-subspace(K;vs;x.Q[x])})

Lemma: implies-vs-subspace
K:Rng. ∀vs:VectorSpace(K).
  ∀[P:Point(vs) ⟶ ℙ]. (P[0]  (∀x,y:Point(vs).  (P[x]  P[y]  (∀k:|K|. P[k y])))  vs-subspace(K;vs;x.P[x]))

Definition: vs-tree-val
vs-tree-val(vs;t) ==  l_tree_ind(t; Leaf(p) fst(p); Node(k,l,r) v,w.k w) 

Lemma: vs-tree-val_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[t:l_tree(Point(vs) × Top;|K|)].  (vs-tree-val(vs;t) ∈ Point(vs))

Lemma: vs-tree-val_wf_subspace
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].
  ∀[t:l_tree(v:Point(vs) × P[v];|K|)]. (vs-tree-val(vs;t) ∈ {v:Point(vs)| P[v]} supposing vs-subspace(K;vs;x.P[x])

Definition: generated-subspace
Subspace(v.P[v]) ==  λw.((w 0 ∈ Point(vs)) ∨ (∃t:l_tree(v:Point(vs) × P[v];|K|). (w vs-tree-val(vs;t) ∈ Point(vs))))

Lemma: generated-subspace_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  (Subspace(x.P[x]) ∈ Point(vs) ⟶ ℙ)

Lemma: generated-subspace-is-subspace
K:Rng. ∀vs:VectorSpace(K).  ∀[P:Point(vs) ⟶ ℙ]. vs-subspace(K;vs;w.Subspace(x.P[x]) w)

Lemma: generated-subspace-contains
K:Rng. ∀vs:VectorSpace(K).  ∀[P:Point(vs) ⟶ ℙ]. ∀v:Point(vs). (P[v]  (Subspace(x.P[x]) v))

Lemma: generated-subspace-is-least
K:Rng. ∀vs:VectorSpace(K).
  ∀[P:Point(vs) ⟶ ℙ]
    ∀S:Point(vs) ⟶ ℙ
      (vs-subspace(K;vs;w.S[w])  (∀v:Point(vs). (P[v]  S[v]))  (∀v:Point(vs). ((Subspace(x.P[x]) v)  S[v])))

Definition: sub-vs
(v:vs P[v]) ==  Point= {v:Point(vs)| P[v]}  zero= x+y= a*u= u

Lemma: sub-vs_wf
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  (v:vs P[v]) ∈ VectorSpace(K) supposing vs-subspace(K;vs;x.P[x])

Lemma: sub-vs-point-subtype
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  (Point((v:vs P[v])) ⊆Point(vs))

Definition: vs-sum
Σs:S. V[s] ==  Point= s:S ⟶ Point(V[s]) zero= λs.0 x+y= λs.x k*u= λs.k s

Lemma: vs-sum_wf
[K:Rng]. ∀[S:Type]. ∀[V:S ⟶ VectorSpace(K)].  s:S. V[s] ∈ VectorSpace(K))

Definition: vs-exp
V^S ==  Σs:S. V

Lemma: vs-exp_wf
[K:Rng]. ∀[S:Type]. ∀[V:VectorSpace(K)].  (V^S ∈ VectorSpace(K))

Definition: power-vs
K^S ==  one-dim-vs(K)^S

Lemma: power-vs_wf
[K:Rng]. ∀[S:Type].  (K^S ∈ VectorSpace(K))

Lemma: power-vs-sq
[K,S:Top].  (K^S Point= S ⟶ |K| zero= λs.0 a+b= λs.((a s) +K (b s)) a*b= λs.(a (b s)))

Definition: vs-map
A ⟶ ==
  {f:Point(A) ⟶ Point(B)| 
   (∀u,v:Point(A).  ((f v) v ∈ Point(B))) ∧ (∀a:|K|. ∀u:Point(A).  ((f u) u ∈ Point(B)))} 

Lemma: vs-map_wf
[K:RngSig]. ∀[A,B:VectorSpace(K)].  (A ⟶ B ∈ Type)

Lemma: vs-map-eq
[K:RngSig]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[g:Point(A) ⟶ Point(B)].
  g ∈ A ⟶ supposing g ∈ (Point(A) ⟶ Point(B))

Lemma: vs-map-compose
[K:RngSig]. ∀[A,B,C:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C].  (g f ∈ A ⟶ C)

Definition: vs-0-map
==  λx.0

Lemma: vs-0-map_wf
[K:Rng]. ∀[vs,ws:VectorSpace(K)].  (0 ∈ ws ⟶ vs)

Definition: vs-id-map
id ==  λx.x

Lemma: vs-id-map_wf
[K:Rng]. ∀[vs:VectorSpace(K)].  (id ∈ vs ⟶ vs)

Lemma: vs-map-0
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B].  ((f 0) 0 ∈ Point(B))

Lemma: vs-map-bag-add
[K:Rng]. ∀[vs,ws:VectorSpace(K)]. ∀[g:vs ⟶ ws]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[bs:bag(S)].
  ((g Σ{f[b] b ∈ bs}) = Σ{g f[b] b ∈ bs} ∈ Point(ws))

Lemma: unique-one-dim-vs-map
K:CRng. ∀vs:VectorSpace(K). ∀v:Point(vs).  ∃!h:one-dim-vs(K) ⟶ vs. ((h 1) v ∈ Point(vs))

Definition: vs-subtract
(x y) ==  -K y

Lemma: vs-subtract_wf
[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y:Point(vs)].  ((x y) ∈ Point(vs))

Lemma: vs-subtract-self
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  ((x x) 0 ∈ Point(vs))

Lemma: equal-iff-vs-subtract-is-0
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x,y:Point(vs)].  (x y ∈ Point(vs) ⇐⇒ (x y) 0 ∈ Point(vs))

Lemma: vs-map-subtract
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[x,y:Point(A)].  ((f (x y)) (f y) ∈ Point(B))

Definition: vs-map-kernel
a ∈ Ker(f) ==  (f a) 0 ∈ Point(B)

Lemma: vs-map-kernel_wf
[K:RngSig]. ∀[B:VectorSpace(K)]. ∀[T:Type]. ∀[f:T ⟶ Point(B)]. ∀[a:T].  (a ∈ Ker(f) ∈ ℙ)

Lemma: vs-map-kernel-is-subspace
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B].  vs-subspace(K;A;a.a ∈ Ker(f))

Lemma: vs-map-kernel-zero
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B].
  (∀a:Point(A). (a ∈ Ker(f) ⇐⇒ 0 ∈ Point(A)) ⇐⇒ Inj(Point(A);Point(B);f))

Definition: vs-map-image
b ∈ Img(f) ==  ∃a:Point(A). ((f a) b ∈ Point(B))

Lemma: vs-map-image_wf
[K:RngSig]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[b:Point(B)].  (b ∈ Img(f) ∈ ℙ)

Lemma: vs-map-image-is-subspace
[K:Rng]. ∀A:VectorSpace(K). ∀[B:VectorSpace(K)]. ∀[f:A ⟶ B].  vs-subspace(K;B;b.b ∈ Img(f))

Lemma: vs-map-image-iff-surject
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B].  (∀b:Point(B). b ∈ Img(f) ⇐⇒ Surj(Point(A);Point(B);f))

Lemma: vs-map-into-subspace
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[P:Point(B) ⟶ ℙ].
  (f ∈ A ⟶ (b:B P[b])) supposing ((∀a:Point(A). P[f a]) and vs-subspace(K;B;b.P[b]))

Lemma: vs-map-from-subspace
[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[P:Point(A) ⟶ ℙ].
  f ∈ (a:A P[a]) ⟶ supposing vs-subspace(K;A;a.P[a])

Definition: is-short-exact
is-short-exact(A;B;C;f;g) ==
  (∀a:Point(A). (a ∈ Ker(f) ⇐⇒ 0 ∈ Point(A)))
  ∧ (∀b:Point(B). (b ∈ Img(f) ⇐⇒ b ∈ Ker(g)))
  ∧ (∀c:Point(C). c ∈ Img(g))

Lemma: is-short-exact_wf
[K:Rng]. ∀[A,B,C:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C].  (is-short-exact(A;B;C;f;g) ∈ ℙ)

Definition: short-exact
short-exact{i:l}(K) ==
  {s:A:VectorSpace(K) × B:VectorSpace(K) × C:VectorSpace(K) × A ⟶ B × B ⟶ C| 
   let A,B,C,f,g in is-short-exact(A;B;C;f;g)} 

Definition: vs-iso
A ≅ ==  ∃f:A ⟶ B. ∃g:B ⟶ A. ((∀a:Point(A). ((g (f a)) a ∈ Point(A))) ∧ (∀b:Point(B). ((f (g b)) b ∈ Point(B))))

Lemma: vs-iso_wf
[K:RngSig]. ∀[A,B:VectorSpace(K)].  (A ≅ B ∈ ℙ)

Lemma: vs-iso_inversion
[K:RngSig]. ∀[A,B:VectorSpace(K)].  (A ≅  B ≅ A)

Lemma: vs-iso-iff-kernel-0
[K:Rng]. ∀[A,B:VectorSpace(K)].
  (A ≅ ⇐⇒ ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f) ⇐⇒ 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f)))

Definition: vs-hom
Hom(A;B) ==  Point= A ⟶ zero= λa.0 f+g= λa.f k*f= λa.k a

Lemma: vs-hom_wf
[K:CRng]. ∀[A,B:VectorSpace(K)].  (Hom(A;B) ∈ VectorSpace(K))

Definition: eq-mod-subspace
mod (z.P[z]) ==  P[x -(y)]

Lemma: eq-mod-subspace_wf
[K:RngSig]. ∀[vs:VectorSpace(K)].  ∀P:Point(vs) ⟶ ℙ. ∀[x,y:Point(vs)].  (x mod (z.P[z]) ∈ ℙ)

Lemma: vs-add_functionality_eq-mod
K:Rng. ∀vs:VectorSpace(K). ∀P:Point(vs) ⟶ ℙ.
   (∀x,y,x',y':Point(vs).  (x x' mod (z.P[z])  y' mod (z.P[z])  x' y' mod (z.P[z]))))

Lemma: vs-mul_functionality_eq-mod
K:CRng. ∀vs:VectorSpace(K). ∀P:Point(vs) ⟶ ℙ.
   (∀x,x':Point(vs). ∀k,k':|K|.  (x x' mod (z.P[z])  (k k' ∈ |K|)  k' x' mod (z.P[z]))))

Lemma: eq-mod-subspace-equiv
K:CRng. ∀vs:VectorSpace(K). ∀P:Point(vs) ⟶ ℙ.
  (vs-subspace(K;vs;z.P[z])  EquivRel(Point(vs);x,y.x mod (z.P[z])))

Definition: vs-quotient
vs//z.P[z] ==  Point= x,y:Point(vs)//x mod (z.P[z]) zero= x+y= k*z= z

Lemma: vs-quotient_wf
[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  vs//z.P[z] ∈ VectorSpace(K) supposing vs-subspace(K;vs;z.P[z])

Lemma: eq-0-in-vs-quotient
[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].
  ∀z:Point(vs). 0 ∈ Point(vs//z.P[z]) supposing ↓P[z] supposing vs-subspace(K;vs;z.P[z])

Lemma: subtype-vs-quotient
[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  Point(vs) ⊆Point(vs//z.P[z]) supposing vs-subspace(K;vs;z.P[z])

Lemma: vs-map-quotient-kernel
[K:CRng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B].  (f ∈ A//z.z ∈ Ker(f) ⟶ B)

Lemma: implies-iso-vs-quotient
[K:CRng]. ∀[A:VectorSpace(K)].
    ((∃f:A ⟶ B. Surj(Point(A);Point(B);f))  (∃P:Point(A) ⟶ ℙ(vs-subspace(K;A;z.P[z]) ∧ B ≅ A//z.P[z])))

Lemma: vs-map-quotients
[K:CRng]. ∀[A,B:VectorSpace(K)]. ∀[P:Point(A) ⟶ ℙ]. ∀[Q:Point(B) ⟶ ℙ].
  ∀[f:A ⟶ B]. f ∈ A//z.P[z] ⟶ B//z.Q[z] supposing ∀a:Point(A). (P[a]  Q[f a]) 
  supposing vs-subspace(K;A;z.P[z]) ∧ vs-subspace(K;B;z.Q[z])

Lemma: vs-map-quotient
[K:CRng]. ∀[A,B:VectorSpace(K)]. ∀[P:Point(A) ⟶ ℙ].
  ∀[f:A ⟶ B]. f ∈ A//z.P[z] ⟶ supposing ∀a:Point(A). (P[a]  ((f a) 0 ∈ Point(B))) 
  supposing vs-subspace(K;A;z.P[z])

Definition: relative-vs
v.A[v]//z.B[z] ==  (v:vs A[v])//z.B[z]

Lemma: relative-vs_wf
[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[A,B:Point(vs) ⟶ ℙ].
  a.A[a]//b.B[b] ∈ VectorSpace(K) 
  supposing vs-subspace(K;vs;a.A[a]) ∧ vs-subspace(K;vs;b.B[b]) ∧ (∀v:Point(vs). (B[v]  A[v]))

Definition: basic-formal-sum
basic-formal-sum(K;S) ==  bag(|K| × S)

Lemma: basic-formal-sum_wf
[K:RngSig]. ∀[S:Type].  (basic-formal-sum(K;S) ∈ Type)

Lemma: basic-formal-sum-subtype
[K:RngSig]. ∀[S,T:Type].  basic-formal-sum(K;S) ⊆basic-formal-sum(K;T) supposing S ⊆T

Lemma: basic-formal-sum-strong-subtype
[K:RngSig]. ∀[S,T:Type].  strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T)) supposing strong-subtype(S;T)

Definition: bfs-predicate
bfs-predicate(K;S;p.P[p];b) ==  ∀p:|K| × S. (p ↓∈  P[p])

Lemma: bfs-predicate_wf
[K:RngSig]. ∀[S:Type]. ∀[P:(|K| × S) ⟶ ℙ]. ∀[b:basic-formal-sum(K;S)].  (bfs-predicate(K;S;p.P[p];b) ∈ ℙ)

Definition: formal-sum-mul
==  bag-map(λp.let k',s in <k', s>;x)

Lemma: formal-sum-mul_wf1
[S:Type]. ∀[K:RngSig]. ∀[x:basic-formal-sum(K;S)]. ∀[k:|K|].  (k x ∈ basic-formal-sum(K;S))

Definition: zero-bfs
ss ==  bag-map(λs.<0, s>;ss)

Lemma: zero-bfs_wf
[S:Type]. ∀[K:RngSig]. ∀[ss:bag(S)].  (0 ss ∈ basic-formal-sum(K;S))

Lemma: zero-bfs-append
[S:Type]. ∀[K:RngSig]. ∀[ss1,ss2:bag(S)].  (0 ss1 ss2 (0 ss1 ss2) ∈ basic-formal-sum(K;S))

Definition: bfs-reduce
Formal sums, as and bs, should be equivalent if one can be obtained
from the other by either "removing zeros" or "combining coefficients".

This relation states "single step" of that relation, without assuming that
it is decidable. We don't need to be able to decide which coefficients are
zero, or which "elements" in the formal sum have the same "generator".
(To do that would require that the scalars have decidable equality
and the generators have decidable equality.)

We then define bfs-equiv to be the least equivalence relation
containing this relation (i.e. the transitive-reflexive-symmetric closure
of this relation).⋅

bfs-reduce(K;S;as;bs) ==
  (∃s:bag(S). (as (bs s) ∈ basic-formal-sum(K;S)))
  ∨ (∃cs:basic-formal-sum(K;S)
        ((as (cs +K k' fs) ∈ basic-formal-sum(K;S)) ∧ (bs (cs fs k' fs) ∈ basic-formal-sum(K;S))))

Lemma: bfs-reduce_wf
[K:RngSig]. ∀[S:Type]. ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;S;as;bs) ∈ ℙ)

Lemma: bfs-reduce-subtype1
[K:RngSig]. ∀[S,T:Type].
  ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;S;as;bs)  bfs-reduce(K;T;as;bs)) supposing S ⊆T

Definition: vs-lift
vs-lift(vs;f;fs) ==  Σ{let k,s in p ∈ fs}

Lemma: vs-lift_wf
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[fs:bag(|K| × S)].  (vs-lift(vs;f;fs) ∈ Point(vs))

Lemma: vs-lift-append
[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[fs,fs':bag(|K| × S)].
  (vs-lift(vs;f;fs fs') vs-lift(vs;f;fs) vs-lift(vs;f;fs') ∈ Point(vs))

Lemma: vs-lift-zero-bfs
[K:Rng]. ∀[S:Type]. ∀[ss:bag(S)]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;0 ss) 0 ∈ Point(vs))

Lemma: vs-lift-bfs-reduce
[K:Rng]. ∀[S:Type]. ∀[as,bs:basic-formal-sum(K;S)].
  ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;as) vs-lift(vs;f;bs) ∈ Point(vs)) 
  supposing bfs-reduce(K;S;as;bs)

Definition: bfs-equiv
bfs-equiv(K;S;fs1;fs2) ==  least-equiv(basic-formal-sum(K;S);λas,bs. bfs-reduce(K;S;as;bs)) fs1 fs2

Lemma: bfs-equiv_wf
[K:RngSig]. ∀[S:Type]. ∀[a,b:basic-formal-sum(K;S)].  (bfs-equiv(K;S;a;b) ∈ ℙ)

Lemma: bfs-equiv-rel
K:RngSig. ∀S:Type.  EquivRel(basic-formal-sum(K;S);a,b.bfs-equiv(K;S;a;b))

Lemma: bfs-equiv-implies
[S:Type]. ∀[K:RngSig]. ∀[E:basic-formal-sum(K;S) ⟶ basic-formal-sum(K;S) ⟶ ℙ].
  ((∀x,y:basic-formal-sum(K;S).  (bfs-reduce(K;S;x;y)  (E y)))
   EquivRel(basic-formal-sum(K;S);x,y.E y)
   (∀x,y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;y)  (E y))))

Lemma: bfs-equiv-implies2
[S:Type]. ∀[K:RngSig].
     {∀[P:basic-formal-sum(K;S) ⟶ ℙ]
          ((∀x,y:basic-formal-sum(K;S).  (bfs-reduce(K;S;x;y)  (P[x] ⇐⇒ P[y])))  P[x]  P[y])})

Lemma: vs-lift-bfs-equiv
[K:Rng]. ∀[S:Type]. ∀[as,bs:basic-formal-sum(K;S)].
  ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;as) vs-lift(vs;f;bs) ∈ Point(vs)) 
  supposing bfs-equiv(K;S;as;bs)

Lemma: implies-bfs-equiv
[K:RngSig]. ∀[S:Type].  ∀as,bs:basic-formal-sum(K;S).  (bfs-reduce(K;S;as;bs)  bfs-equiv(K;S;as;bs))

Definition: bfs-rm0
bfs-rm0(K;eq;b) ==  [p∈b|¬b(eq (fst(p)) 0)]

Lemma: bfs-rm0_wf
[K:RngSig]. ∀[S:Type]. ∀[b:basic-formal-sum(K;S)]. ∀[eq:EqDecider(|K|)].  (bfs-rm0(K;eq;b) ∈ basic-formal-sum(K;S))

Definition: formal-sum
formal-sum(K;S) ==  a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b)

Lemma: formal-sum_wf
[K:RngSig]. ∀[S:Type].  (formal-sum(K;S) ∈ Type)

Lemma: formal-sum-subtype
[K:RngSig]. ∀[S,T:Type].  formal-sum(K;S) ⊆formal-sum(K;T) supposing S ⊆T

Definition: formal-sum-add
==  y

Lemma: formal-sum-add_wf1
[S:Type]. ∀[K:RngSig]. ∀[x,y:basic-formal-sum(K;S)].  (x y ∈ basic-formal-sum(K;S))

Lemma: formal-sum-add_functionality
S:Type. ∀K:RngSig. ∀x,x',y,y':basic-formal-sum(K;S).
  (bfs-equiv(K;S;y;y')  bfs-equiv(K;S;x;x')  bfs-equiv(K;S;x y;x' y'))

Lemma: formal-sum-add_wf
[S:Type]. ∀[K:RngSig]. ∀[x,y:formal-sum(K;S)].  (x y ∈ formal-sum(K;S))

Lemma: formal-sum-add-comm
[S:Type]. ∀[K:RngSig]. ∀[x,y:formal-sum(K;S)].  (x x ∈ formal-sum(K;S))

Lemma: formal-sum-add-assoc
[x,y,z:Top].  (x z)

Lemma: formal-sum-mul_functionality
S:Type. ∀K:CRng. ∀x,x':basic-formal-sum(K;S). ∀k,k':|K|.
  bfs-equiv(K;S;x;x')  bfs-equiv(K;S;k x;k' x') supposing k' ∈ |K|

Lemma: formal-sum-mul_wf
[S:Type]. ∀[K:CRng]. ∀[x:formal-sum(K;S)]. ∀[k:|K|].  (k x ∈ formal-sum(K;S))

Lemma: formal-sum-mul-0
[S:Type]. ∀[K:Rng]. ∀[x:formal-sum(K;S)].  (0 {} ∈ formal-sum(K;S))

Lemma: formal-sum-mul-linear
[S:Type]. ∀[K:CRng]. ∀[k:|K|]. ∀[x,y:formal-sum(K;S)].  (k y ∈ formal-sum(K;S))

Lemma: formal-sum-mul-mul
[S:Type]. ∀[K:CRng]. ∀[k,b:|K|]. ∀[x:formal-sum(K;S)].  (k x ∈ formal-sum(K;S))

Lemma: formal-sum-mul-1
[S:Type]. ∀[K:Rng]. ∀[x:formal-sum(K;S)].  (1 x ∈ formal-sum(K;S))

Lemma: bfs-rm0-equiv
K:RngSig. ∀S:Type. ∀b:basic-formal-sum(K;S). ∀eq:EqDecider(|K|).  (↓bfs-equiv(K;S;bfs-rm0(K;eq;b);b))

Definition: fs-predicate
fs-predicate(K;S;p.P[p];f) ==  ↓∃b:basic-formal-sum(K;S). ((f b ∈ formal-sum(K;S)) ∧ bfs-predicate(K;S;p.P[p];b))

Lemma: fs-predicate_wf
[K:RngSig]. ∀[S:Type]. ∀[P:(|K| × S) ⟶ ℙ]. ∀[f:formal-sum(K;S)].  (fs-predicate(K;S;p.P[p];f) ∈ ℙ)

Definition: fs-in-subtype
fs-in-subtype(K;S;T;f) ==  fs-predicate(K;S;p.snd(p) ∈ T;f)

Lemma: fs-in-subtype_wf
[K:RngSig]. ∀[S,T:Type].  ∀[f:formal-sum(K;S)]. (fs-in-subtype(K;S;T;f) ∈ ℙsupposing strong-subtype(T;S)

Lemma: sq_stable__fs-in-subtype
[K:RngSig]. ∀[S,T:Type].  ∀[f:formal-sum(K;S)]. SqStable(fs-in-subtype(K;S;T;f)) supposing strong-subtype(T;S)

Lemma: fs-in-subtype-basic
[K:RngSig]. ∀[S,T:Type].
  ∀[f:formal-sum(K;S)]. ↓∃b:basic-formal-sum(K;T). (f b ∈ formal-sum(K;S)) supposing fs-in-subtype(K;S;T;f) 
  supposing strong-subtype(T;S)

Lemma: vs-lift-formal-sum-mul
[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[k:|K|]. ∀[x:basic-formal-sum(K;S)].
  (vs-lift(vs;f;k x) vs-lift(vs;f;x) ∈ Point(vs))

Lemma: formal-sum-mul-add
[S:Type]. ∀[K:CRng]. ∀[k,b:|K|]. ∀[x:formal-sum(K;S)].  (k +K x ∈ formal-sum(K;S))

Lemma: bfs-reduce-strong-subtype
[K:RngSig]. ∀[S,T:Type].
  ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;T;as;bs)  bfs-reduce(K;S;as;bs)) supposing strong-subtype(S;T)

Lemma: bfs-reduce-strong-subtype-iff
[K:RngSig]. ∀[S,T:Type].
  ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;T;as;bs) ⇐⇒ bfs-reduce(K;S;as;bs)) supposing strong-subtype(S;T)

Definition: free-vs
free-vs(K;S) ==  Point= formal-sum(K;S) zero= {} x+y= k*x= x

Lemma: free-vs_wf
[S:Type]. ∀[K:CRng].  (free-vs(K;S) ∈ VectorSpace(K))

Lemma: vs-lift_wf2
[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[fs:formal-sum(K;S)].  (vs-lift(vs;f;fs) ∈ Point(vs))

Definition: free-vs-inc
<s> ==  {<1, s>}

Lemma: free-vs-inc_wf
[S:Type]. ∀[K:RngSig]. ∀[s:S].  (<s> ∈ Point(free-vs(K;S)))

Lemma: vs-lift-inc
[S:Type]. ∀[K:Rng]. ∀[s:S]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;<s>(f s) ∈ Point(vs))

Lemma: vs-lift-add
[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)]. ∀[u,v:Point(free-vs(K;S))].
  (vs-lift(vs;f;u v) vs-lift(vs;f;u) vs-lift(vs;f;v) ∈ Point(vs))

Lemma: vs-lift-mul
[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)]. ∀[a:|K|]. ∀[u:Point(free-vs(K;S))].
  (vs-lift(vs;f;a u) vs-lift(vs;f;u) ∈ Point(vs))

Lemma: vs-lift_wf-vs-map
[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  x.vs-lift(vs;f;x) ∈ free-vs(K;S) ⟶ vs)

Lemma: vs-lift-unique
[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)]. ∀[h:free-vs(K;S) ⟶ vs].
  x.vs-lift(vs;f;x)) ∈ free-vs(K;S) ⟶ vs supposing ∀s:S. ((h <s>(f s) ∈ Point(vs))

Lemma: free-vs-property
[S:Type]. ∀K:CRng. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:free-vs(K;S) ⟶ vs. ∀s:S. ((h <s>(f s) ∈ Point(vs))

Lemma: free-vs-maps-eq
[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f,g:free-vs(K;S) ⟶ vs].
  g ∈ free-vs(K;S) ⟶ vs supposing ∀s:S. ((f <s>(g <s>) ∈ Point(vs))

Lemma: free-vs-unique
S:Type. ∀K:CRng. ∀V:VectorSpace(K).
  (∃i:S ⟶ Point(V). ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) (f s) ∈ Point(vs))
  ⇐⇒ V ≅ free-vs(K;S))

Lemma: fs-in-subtype-subspace
[K:CRng]. ∀[S,T:Type].  vs-subspace(K;free-vs(K;S);f.fs-in-subtype(K;S;T;f)) supposing strong-subtype(T;S)

Definition: sub-free-vs
sub-free-vs(K;S;T) ==  (f:free-vs(K;S) fs-in-subtype(K;S;T;f))

Lemma: sub-free-vs_wf
[K:CRng]. ∀[S,T:Type].  sub-free-vs(K;S;T) ∈ VectorSpace(K) supposing strong-subtype(T;S)

Lemma: sub-free-dim-1
[K:CRng]. ∀[S,T:Type].
  (∀s:T. ∀x:Point(sub-free-vs(K;S;T)).  (↓∃k:|K|. (x {<k, s>} ∈ Point(sub-free-vs(K;S;T))))) supposing 
     ((∀x,y:T.  (x y ∈ T)) and 

Definition: relative-free-vs
relative-free-vs(K;S;T) ==  free-vs(K;S)//f.fs-in-subtype(K;S;T;f)

Lemma: relative-free-vs_wf
[K:CRng]. ∀[S,T:Type].  relative-free-vs(K;S;T) ∈ VectorSpace(K) supposing strong-subtype(T;S)

Lemma: eq-0-in-relative-free-vs
[K:CRng]. ∀[S,T:Type].
  ∀[x:Point(free-vs(K;S))]. 0 ∈ Point(relative-free-vs(K;S;T)) supposing ↓fs-in-subtype(K;S;T;x) 
  supposing strong-subtype(T;S)

Lemma: free-vs-dim-1
S:Type. (S  (∀K:CRng. free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S.  (x y ∈ S)))

Lemma: free-vs-dim-0
S:Type. ((¬S)  (∀K:CRng. free-vs(K;S) ≅ 0))

Lemma: free-vs-dim-1-ext
S:Type. (S  (∀K:CRng. free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S.  (x y ∈ S)))

Definition: free-1-iso
free-1-iso(s;K) ==  <λx.Σ(p∈x). let k,s in 1, λk.{<1, s>}, λb.Ax, λa.Ax>

Lemma: free-1-iso_wf
[S:Type]. ∀[s:S]. ∀[K:CRng].  free-1-iso(s;K) ∈ free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S.  (x y ∈ S)

Definition: free-iso-int
free-iso-int(s) ==  <λx.Σ(p∈x). let k,s in k, λk.{<k, s>}, λb.Ax, λa.Ax>

Lemma: free-iso-int_wf
[S:Type]. ∀[s:S].  free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ supposing ∀x,y:S.  (x y ∈ S)

Lemma: free-1-normal-form
  ∀s:S. ∀x:Point(free-vs(ℤ-rng;S)).  ∃k:ℤ(x {<k, s>} ∈ Point(free-vs(ℤ-rng;S))) supposing ∀x,y:S.  (x y ∈ S)

Lemma: all-vs-quotient-of-free
K:CRng. ∀V:VectorSpace(K).
  ∃S:Type. ∃P:Point(free-vs(K;S)) ⟶ ℙ(vs-subspace(K;free-vs(K;S);x.P[x]) ∧ V ≅ free-vs(K;S)//a.P[a])

Lemma: free-vs-subspace
[S:Type]. ∀[K:CRng]. ∀[P:formal-sum(K;S) ⟶ ℙ].
  ∧ (∀fs,y:formal-sum(K;S).  (P[fs]  P[y]  P[fs y]))
  ∧ (∀fs:formal-sum(K;S). ∀a:|K|.  (P[fs]  P[a fs])))

Lemma: free-vs-subtype
[S,T:Type].  ∀[K:CRng]. (Point(free-vs(K;S)) ⊆Point(free-vs(K;T))) supposing S ⊆T

Lemma: free-vs-bag-add
[G:Type]. ∀[K:CRng]. ∀[S:Type]. ∀[f:S ⟶ bag(|K| × G)]. ∀[bs:bag(S)].
  {f[b] b ∈ bs} = ⋃b∈bs.f[b] ∈ Point(free-vs(K;G)))

Lemma: free-vs-map-into-subspace
[K:CRng]. ∀[S:Type]. ∀[v:VectorSpace(K)]. ∀[f:free-vs(K;S) ⟶ v]. ∀[P:Point(v) ⟶ ℙ].
  (f ∈ free-vs(K;S) ⟶ (x:v P[x])) supposing ((∀s:S. (↓P[f <s>])) and vs-subspace(K;v;x.P[x]))

Lemma: vs-lift_wf-relative
  ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].
    λx.vs-lift(vs;f;x) ∈ relative-free-vs(K;S;T) ⟶ vs supposing ∀t:T. (↓(f t) 0 ∈ Point(vs)) 
  supposing strong-subtype(T;S)

Definition: neg-bfs
-(fs) ==  bag-map(λp.let k,s in <-K k, s>;fs)

Lemma: neg-bfs_wf
[S:Type]. ∀[K:RngSig]. ∀[fs:basic-formal-sum(K;S)].  (-(fs) ∈ basic-formal-sum(K;S))

Lemma: neg-bfs-append
[S:Type]. ∀[K:RngSig]. ∀[fs1,fs2:basic-formal-sum(K;S)].  (-(fs1 fs2) (-(fs1) -(fs2)) ∈ basic-formal-sum(K;S))

Definition: null-formal-sum
null-formal-sum(K;S;fs) ==  ∃b:bag(|K| × S). ∃ss:bag(S). (fs ((b -(b)) ss) ∈ bag(|K| × S))

Lemma: null-formal-sum_wf
[K:RngSig]. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)].  (null-formal-sum(K;S;fs) ∈ ℙ)

Lemma: null-formal-sum-append
[K:RngSig]. ∀[S:Type]. ∀[fs1,fs2:basic-formal-sum(K;S)].
  (null-formal-sum(K;S;fs1)  null-formal-sum(K;S;fs2)  null-formal-sum(K;S;fs1 fs2))

Lemma: null-formal-sum-neg
K:Rng. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)].  (null-formal-sum(K;S;fs)  null-formal-sum(K;S;-(fs)))

Lemma: trivial-null-formal-sum
K:Rng. ∀[S:Type]. ∀fs:basic-formal-sum(K;S). null-formal-sum(K;S;fs -(fs))

Lemma: vs-lift-neg-bfs
[K:CRng]. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].
  (vs-lift(vs;f;-(fs)) -K vs-lift(vs;f;fs) ∈ Point(vs))

Lemma: vs-lift-null-formal-sum
[K:CRng]. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)].
  ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;fs) 0 ∈ Point(vs)) supposing null-formal-sum(K;S;fs)

Lemma: null-formal-sum-mul
[S:Type]. ∀K:CRng. ∀[x:basic-formal-sum(K;S)]. ∀k:|K|. (null-formal-sum(K;S;x)  null-formal-sum(K;S;k x))

Home Index