Basic theory of vector spaces.
The same structure is called either a module or a vector space
depending on whether the scalars are a commutive ring or a field.
Since the scalars are a parameter of our definition, we call them both
vector spaces. Most (if not all) of the theorems proved here assume only
a commutative ring of scalars, so they are theorems about modules.
The axiom of choice (in set theory) proves that every vector space has
a basis, so every vector space is (isomorphic to) a 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 S and coefficents (scalars) K (a commutative ring)
(see free-vs-property)
We can construct the free vector space without assuming that either the
generators S or the scalars K 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) ==
"Point":Type
"0":Point(self)
"+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)|
(∀x,y,z:Point(self). ((f x (f y z)) = (f (f x y) z) ∈ Point(self)))
∧ (∀x,y:Point(self). ((f x y) = (f y x) ∈ Point(self)))}
"*":{m:|K| ⟶ Point(self) ⟶ Point(self)|
(∀a:|K|. ∀x,y:Point(self). ((m a (self."+" x y)) = (self."+" (m a x) (m a y)) ∈ Point(self)))
∧ (∀x:Point(self)
(((m 1 x) = x ∈ Point(self))
∧ ((m 0 x) = self."0" ∈ Point(self))
∧ (∀a,b:|K|. ((m a (m b x)) = (m (a * b) x) ∈ Point(self)))
∧ (∀a,b:|K|. ((m (a +K b) x) = (self."+" (m a x) (m b 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
0 == vs."0"
Lemma: vs-0_wf
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. (0 ∈ Point(vs))
Definition: vs-add
x + y == vs."+" x 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 + y = y + x ∈ Point(vs))
Lemma: vs-add-comm
∀K:RngSig. ∀vs:VectorSpace(K). ∀x,y:Point(vs). (x + y = y + x ∈ Point(vs))
Lemma: vs-add-assoc
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)]. (x + y + z = x + y + z ∈ Point(vs))
Lemma: vs-mon_assoc
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)]. (x + y + z = x + y + z ∈ Point(vs))
Lemma: vs-ac_1
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)]. (x + y + z = y + x + z ∈ Point(vs))
Definition: vs-mul
a * x == vs."*" a 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 * x + y = a * x + a * y ∈ Point(vs))
Lemma: vs-mul-mul
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a,b:|K|]. ∀[x:Point(vs)]. (a * b * x = a * b * x ∈ Point(vs))
Lemma: vs-mul-add
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a,b:|K|]. ∀[x:Point(vs)]. (a +K b * x = a * x + b * x ∈ Point(vs))
Lemma: vs-mul-one
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)]. (1 * x = x ∈ Point(vs))
Lemma: vs-mul-zero
∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)]. (0 * x = 0 ∈ Point(vs))
Lemma: vs-zero-add
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)]. (0 + x = x ∈ Point(vs))
Lemma: vs-mon_ident
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)]. ((x + 0 = x ∈ Point(vs)) ∧ (0 + x = x ∈ Point(vs)))
Definition: vs-neg
-(x) == -K 1 * 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) + x = 0 ∈ Point(vs))
Lemma: vs-grp_inverse
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)]. ((x + -(x) = 0 ∈ Point(vs)) ∧ (-(x) + x = 0 ∈ Point(vs)))
Lemma: vs-add-cancel
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)]. (x + z = y + z ∈ Point(vs) ⇐⇒ x = y ∈ Point(vs))
Lemma: vs-cancel-add
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[x,y,z:Point(vs)]. (z + x = z + y ∈ Point(vs) ⇐⇒ x = 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 = 0 ∈ Point(vs))
Lemma: vs-grp_inv_assoc
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[a,b:Point(vs)]. ((a + -(a) + b = b ∈ Point(vs)) ∧ (-(a) + a + b = 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)].
∀[b:bag(T)].
(Σ{Σ{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, m + 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] | k + 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] | n - k≤i≤m - 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 + i + 1] | 0≤i≤m - k + 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] * a | n≤i≤m} = Σ(K) n ≤ i < m + 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, m + 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:ℕn + 1 ⟶ {v:Point(vs)| P[v]} .
(Inj(ℕn + 1;Point(vs);f)
⇒ (∀c:ℕn + 1 ⟶ |K|. ((Σ{c i * f i | 0≤i≤n} = 0 ∈ Point(vs)) ⇒ (∀i:ℕn + 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= V zero= z 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
0 == 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= 0 a+b= a +K b a*b= a * b
Lemma: one-dim-vs_wf
∀[K:Rng]. (one-dim-vs(K) ∈ VectorSpace(K))
Definition: int-vs
ℤ == Point= ℤ zero= 0 a+b= a + b a*b= a * 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 * x + 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 * v + 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= 0 x+y= x + y a*u= a * 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])) ⊆r Point(vs))
Definition: vs-sum
Σs:S. V[s] == Point= s:S ⟶ Point(V[s]) zero= λs.0 x+y= λs.x s + y s k*u= λs.k * u 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 ⟶ B ==
{f:Point(A) ⟶ Point(B)|
(∀u,v:Point(A). ((f u + v) = f u + f v ∈ Point(B))) ∧ (∀a:|K|. ∀u:Point(A). ((f a * u) = a * f 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)].
f = g ∈ A ⟶ B supposing f = g ∈ (Point(A) ⟶ Point(B))
Lemma: vs-map-compose
∀[K:RngSig]. ∀[A,B,C:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C]. (g o f ∈ A ⟶ C)
Definition: vs-0-map
0 == λ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) == x + -K 1 * 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 x - 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) ⇐⇒ a = 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]) ⟶ B 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) ⇐⇒ a = 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 = s in is-short-exact(A;B;C;f;g)}
Definition: vs-iso
A ≅ B == ∃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 ⇒ B ≅ A)
Lemma: vs-iso-iff-kernel-0
∀[K:Rng]. ∀[A,B:VectorSpace(K)].
(A ≅ B ⇐⇒ ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f) ⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f)))
Definition: vs-hom
Hom(A;B) == Point= A ⟶ B zero= λa.0 f+g= λa.f a + g a k*f= λa.k * f a
Lemma: vs-hom_wf
∀[K:CRng]. ∀[A,B:VectorSpace(K)]. (Hom(A;B) ∈ VectorSpace(K))
Definition: eq-mod-subspace
x = y 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 = y mod (z.P[z]) ∈ ℙ)
Lemma: vs-add_functionality_eq-mod
∀K:Rng. ∀vs:VectorSpace(K). ∀P:Point(vs) ⟶ ℙ.
(vs-subspace(K;vs;z.P[z])
⇒ (∀x,y,x',y':Point(vs). (x = x' mod (z.P[z]) ⇒ y = y' mod (z.P[z]) ⇒ x + y = x' + y' mod (z.P[z]))))
Lemma: vs-mul_functionality_eq-mod
∀K:CRng. ∀vs:VectorSpace(K). ∀P:Point(vs) ⟶ ℙ.
(vs-subspace(K;vs;z.P[z])
⇒ (∀x,x':Point(vs). ∀k,k':|K|. (x = x' mod (z.P[z]) ⇒ (k = k' ∈ |K|) ⇒ k * x = 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 = y mod (z.P[z])))
Definition: vs-quotient
vs//z.P[z] == Point= x,y:Point(vs)//x = y mod (z.P[z]) zero= 0 x+y= x + y k*z= k * 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). z = 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) ⊆r 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)].
∀B: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] ⟶ B 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) ⊆r basic-formal-sum(K;T) supposing S ⊆r 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 ↓∈ b ⇒ 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
k * x == bag-map(λp.let k',s = p in <k * 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
0 * 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 + 0 * 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 a "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 K have decidable equality
and the generators S 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 + 0 * s) ∈ basic-formal-sum(K;S)))
∨ (∃cs:basic-formal-sum(K;S)
∃k,k':|K|
∃fs:basic-formal-sum(K;S)
((as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;S)) ∧ (bs = (cs + k * 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 ⊆r T
Definition: vs-lift
vs-lift(vs;f;fs) == Σ{let k,s = p in k * f s | 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 x y)))
⇒ EquivRel(basic-formal-sum(K;S);x,y.E x y)
⇒ (∀x,y:basic-formal-sum(K;S). (bfs-equiv(K;S;x;y) ⇒ (E x y))))
Lemma: bfs-equiv-implies2
∀[S:Type]. ∀[K:RngSig].
∀x,y:basic-formal-sum(K;S).
(bfs-equiv(K;S;x;y)
⇒ {∀[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) ⊆r formal-sum(K;T) supposing S ⊆r T
Definition: formal-sum-add
x + y == x + 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 + y = y + x ∈ formal-sum(K;S))
Lemma: formal-sum-add-assoc
∀[x,y,z:Top]. (x + y + z ~ x + y + 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' ∈ |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 * x = {} ∈ formal-sum(K;S))
Lemma: formal-sum-mul-linear
∀[S:Type]. ∀[K:CRng]. ∀[k:|K|]. ∀[x,y:formal-sum(K;S)]. (k * x + y = k * x + k * y ∈ formal-sum(K;S))
Lemma: formal-sum-mul-mul
∀[S:Type]. ∀[K:CRng]. ∀[k,b:|K|]. ∀[x:formal-sum(K;S)]. (k * b * x = k * b * x ∈ formal-sum(K;S))
Lemma: formal-sum-mul-1
∀[S:Type]. ∀[K:Rng]. ∀[x:formal-sum(K;S)]. (1 * x = 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) = k * 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 b * x = k * x + b * 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= x + y k*x= k * 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) = a * 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].
h = (λ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].
f = 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
strong-subtype(T;S))
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))]. x = 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 = p in k * 1, λk.{<* 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 = p 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:Type]
∀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) ⟶ ℙ].
((P[{}]
∧ (∀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])))
⇒ vs-subspace(K;free-vs(K;S);fs.P[fs]))
Lemma: free-vs-subtype
∀[S,T:Type]. ∀[K:CRng]. (Point(free-vs(K;S)) ⊆r Point(free-vs(K;T))) supposing S ⊆r 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
∀[S,T:Type].
∀[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 = p 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)) + 0 * 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 1 * 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