Skip to content

Commit 8b6accd

Browse files
SimonBrandnerSimonBrandner
committed
Add linear combinations, linear spans and tuple concatenation
This PR adds linear combinations, linear spans and tuple concatenation. It contains a proof that a linear span has the structure of a left submodule. Signed-off-by: Šimon Brandner <[email protected]>
1 parent 961069e commit 8b6accd

File tree

6 files changed

+662
-0
lines changed

6 files changed

+662
-0
lines changed

‎src/linear-algebra.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,9 @@ open import linear-algebra.finite-sequences-in-semirings public
2323
open import linear-algebra.functoriality-matrices public
2424
open import linear-algebra.left-modules-rings public
2525
open import linear-algebra.left-submodules-rings public
26+
open import linear-algebra.linear-combinations public
2627
open import linear-algebra.linear-maps-left-modules-rings public
28+
open import linear-algebra.linear-spans public
2729
open import linear-algebra.matrices public
2830
open import linear-algebra.matrices-on-rings public
2931
open import linear-algebra.multiplication-matrices public

‎src/linear-algebra/linear-combinations.lagda.md‎

Lines changed: 282 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,282 @@
1+
# Linear combinations
2+
3+
```agda
4+
module linear-algebra.linear-combinations where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.natural-numbers
11+
12+
open import foundation.action-on-identifications-functions
13+
open import foundation.identity-types
14+
open import foundation.universe-levels
15+
16+
open import linear-algebra.left-modules-rings
17+
18+
open import lists.concatenation-tuples
19+
open import lists.functoriality-tuples
20+
open import lists.tuples
21+
22+
open import ring-theory.rings
23+
```
24+
25+
</details>
26+
27+
## Idea
28+
29+
Let `M` be a [left module](linear-algebra.left-modules-rings.md) over a
30+
[ring](ring-theory.rings.md) `R`. Given a tuple `(r_1, ..., r_n)` of elements of
31+
`R` and a tuple `(x_1, ..., x_n)` of elements of `M`, a
32+
{{#concept "linear combination" Agda=linear-combination-left-module-Ring}} of
33+
these tuples is the sum `r_1 * x_1 + ... + r_n * x_n`.
34+
35+
## Definitions
36+
37+
### Linear combinations in a left module over a ring
38+
39+
```agda
40+
linear-combination-left-module-Ring :
41+
{l1 l2 : Level}
42+
{n : ℕ} →
43+
(R : Ring l1)
44+
(M : left-module-Ring l2 R) →
45+
tuple (type-Ring R) n →
46+
tuple (type-left-module-Ring R M) n →
47+
type-left-module-Ring R M
48+
linear-combination-left-module-Ring R M empty-tuple empty-tuple =
49+
zero-left-module-Ring R M
50+
linear-combination-left-module-Ring R M (r ∷ scalars) (x ∷ vectors) =
51+
add-left-module-Ring R M
52+
( linear-combination-left-module-Ring R M scalars vectors)
53+
( mul-left-module-Ring R M r x)
54+
```
55+
56+
## Properties
57+
58+
### Left distributivity law for multiplication
59+
60+
```agda
61+
left-distributive-law-mul-linear-combination-left-module-Ring :
62+
{l1 l2 : Level}
63+
{n : ℕ} →
64+
(R : Ring l1) →
65+
(M : left-module-Ring l2 R)
66+
(r : type-Ring R) →
67+
(scalars : tuple (type-Ring R) n) →
68+
(vectors : tuple (type-left-module-Ring R M) n) →
69+
mul-left-module-Ring R M
70+
( r)
71+
( linear-combination-left-module-Ring R M scalars vectors) ＝
72+
linear-combination-left-module-Ring R M
73+
( map-tuple (mul-Ring R r) scalars)
74+
( vectors)
75+
left-distributive-law-mul-linear-combination-left-module-Ring
76+
R M r empty-tuple empty-tuple =
77+
equational-reasoning
78+
mul-left-module-Ring R M r
79+
( linear-combination-left-module-Ring R M empty-tuple empty-tuple)
80+
＝
81+
mul-left-module-Ring R M r (zero-left-module-Ring R M)
82+
by refl
83+
＝
84+
zero-left-module-Ring R M
85+
by right-zero-law-mul-left-module-Ring R M r
86+
＝
87+
linear-combination-left-module-Ring R M empty-tuple empty-tuple
88+
by refl
89+
left-distributive-law-mul-linear-combination-left-module-Ring
90+
R M r (s ∷ scalars) (x ∷ vectors) =
91+
equational-reasoning
92+
mul-left-module-Ring R M r
93+
( linear-combination-left-module-Ring R M (s ∷ scalars) (x ∷ vectors))
94+
＝
95+
mul-left-module-Ring R M r
96+
( add-left-module-Ring R M
97+
( linear-combination-left-module-Ring R M scalars vectors)
98+
( mul-left-module-Ring R M s x))
99+
by refl
100+
＝
101+
add-left-module-Ring R M
102+
( mul-left-module-Ring R M r
103+
( linear-combination-left-module-Ring R M scalars vectors))
104+
( mul-left-module-Ring R M r (mul-left-module-Ring R M s x))
105+
by left-distributive-mul-add-left-module-Ring R M r
106+
( linear-combination-left-module-Ring R M scalars vectors)
107+
( mul-left-module-Ring R M s x)
108+
＝
109+
add-left-module-Ring R M
110+
( mul-left-module-Ring R M r
111+
( linear-combination-left-module-Ring R M scalars vectors))
112+
( mul-left-module-Ring R M (mul-Ring R r s) x)
113+
by ap
114+
( λ y →
115+
add-left-module-Ring R M
116+
( mul-left-module-Ring R M r
117+
( linear-combination-left-module-Ring R M scalars vectors))
118+
( y))
119+
(inv (associative-mul-left-module-Ring R M r s x))
120+
＝
121+
add-left-module-Ring R M
122+
( linear-combination-left-module-Ring R M
123+
( map-tuple (mul-Ring R r) scalars)
124+
( vectors))
125+
( mul-left-module-Ring R M (mul-Ring R r s) x)
126+
by ap
127+
( λ y →
128+
add-left-module-Ring R M
129+
( y)
130+
( mul-left-module-Ring R M (mul-Ring R r s) x))
131+
( left-distributive-law-mul-linear-combination-left-module-Ring R M r
132+
( scalars)
133+
( vectors))
134+
＝
135+
linear-combination-left-module-Ring R M
136+
( map-tuple (mul-Ring R r) (s ∷ scalars))
137+
( x ∷ vectors)
138+
by refl
139+
```
140+
141+
### Concatenation is addition
142+
143+
```agda
144+
concatenation-is-addition-linear-combination-left-module-Ring :
145+
{l1 l2 : Level}
146+
{n m : ℕ} →
147+
(R : Ring l1) →
148+
(M : left-module-Ring l2 R)
149+
(scalars-a : tuple (type-Ring R) n) →
150+
(vectors-a : tuple (type-left-module-Ring R M) n) →
151+
(scalars-b : tuple (type-Ring R) m) →
152+
(vectors-b : tuple (type-left-module-Ring R M) m) →
153+
linear-combination-left-module-Ring R M
154+
( concat-tuple scalars-a scalars-b)
155+
( concat-tuple vectors-a vectors-b) ＝
156+
add-left-module-Ring R M
157+
( linear-combination-left-module-Ring R M scalars-a vectors-a)
158+
( linear-combination-left-module-Ring R M scalars-b vectors-b)
159+
concatenation-is-addition-linear-combination-left-module-Ring
160+
R M empty-tuple empty-tuple scalars-b vectors-b =
161+
equational-reasoning
162+
linear-combination-left-module-Ring R M
163+
( concat-tuple empty-tuple scalars-b)
164+
( concat-tuple empty-tuple vectors-b)
165+
＝
166+
linear-combination-left-module-Ring R M scalars-b vectors-b
167+
by refl
168+
＝
169+
add-left-module-Ring R M
170+
( zero-left-module-Ring R M)
171+
( linear-combination-left-module-Ring R M scalars-b vectors-b)
172+
by inv
173+
( left-unit-law-add-left-module-Ring R M
174+
( linear-combination-left-module-Ring R M scalars-b vectors-b))
175+
＝
176+
add-left-module-Ring R M
177+
( linear-combination-left-module-Ring R M empty-tuple empty-tuple)
178+
( linear-combination-left-module-Ring R M scalars-b vectors-b)
179+
by refl
180+
concatenation-is-addition-linear-combination-left-module-Ring
181+
R M (r ∷ scalars-a) (x ∷ vectors-a) scalars-b vectors-b =
182+
equational-reasoning
183+
linear-combination-left-module-Ring R M
184+
( concat-tuple (r ∷ scalars-a) scalars-b)
185+
( concat-tuple (x ∷ vectors-a) vectors-b)
186+
＝
187+
linear-combination-left-module-Ring R M
188+
( r ∷ (concat-tuple scalars-a scalars-b))
189+
( x ∷ (concat-tuple vectors-a vectors-b))
190+
by refl
191+
＝
192+
add-left-module-Ring R M
193+
( linear-combination-left-module-Ring R M
194+
( concat-tuple scalars-a scalars-b)
195+
( concat-tuple vectors-a vectors-b))
196+
( mul-left-module-Ring R M r x)
197+
by refl
198+
＝
199+
add-left-module-Ring R M
200+
( add-left-module-Ring R M
201+
( linear-combination-left-module-Ring R M
202+
( scalars-a)
203+
( vectors-a))
204+
( linear-combination-left-module-Ring R M
205+
( scalars-b)
206+
( vectors-b)))
207+
( mul-left-module-Ring R M r x)
208+
by ap
209+
(λ z → add-left-module-Ring R M z (mul-left-module-Ring R M r x))
210+
( concatenation-is-addition-linear-combination-left-module-Ring R M
211+
( scalars-a)
212+
( vectors-a)
213+
( scalars-b)
214+
( vectors-b))
215+
＝
216+
add-left-module-Ring R M
217+
( mul-left-module-Ring R M r x)
218+
( add-left-module-Ring R M
219+
( linear-combination-left-module-Ring R M
220+
( scalars-a)
221+
( vectors-a))
222+
( linear-combination-left-module-Ring R M
223+
( scalars-b)
224+
( vectors-b)))
225+
by commutative-add-left-module-Ring R M
226+
( add-left-module-Ring R M
227+
( linear-combination-left-module-Ring R M
228+
( scalars-a)
229+
( vectors-a))
230+
( linear-combination-left-module-Ring R M
231+
( scalars-b)
232+
( vectors-b)))
233+
( mul-left-module-Ring R M r x)
234+
＝
235+
add-left-module-Ring R M
236+
( add-left-module-Ring R M
237+
( mul-left-module-Ring R M r x)
238+
( linear-combination-left-module-Ring R M
239+
( scalars-a)
240+
( vectors-a)))
241+
( linear-combination-left-module-Ring R M
242+
( scalars-b)
243+
( vectors-b))
244+
by inv
245+
( associative-add-left-module-Ring R M
246+
( mul-left-module-Ring R M r x)
247+
( linear-combination-left-module-Ring R M
248+
( scalars-a)
249+
( vectors-a))
250+
( linear-combination-left-module-Ring R M
251+
( scalars-b)
252+
( vectors-b)))
253+
＝
254+
add-left-module-Ring R M
255+
( add-left-module-Ring R M
256+
( linear-combination-left-module-Ring R M
257+
( scalars-a)
258+
( vectors-a))
259+
( mul-left-module-Ring R M r x))
260+
( linear-combination-left-module-Ring R M
261+
( scalars-b)
262+
( vectors-b))
263+
by ap
264+
( λ y → add-left-module-Ring R M y
265+
( linear-combination-left-module-Ring R M
266+
( scalars-b)
267+
( vectors-b)))
268+
( commutative-add-left-module-Ring R M
269+
( mul-left-module-Ring R M r x)
270+
( linear-combination-left-module-Ring R M
271+
( scalars-a)
272+
( vectors-a)))
273+
＝
274+
add-left-module-Ring R M
275+
( linear-combination-left-module-Ring R M
276+
( r ∷ scalars-a)
277+
( x ∷ vectors-a))
278+
( linear-combination-left-module-Ring R M
279+
( scalars-b)
280+
( vectors-b))
281+
by refl
282+
```

0 commit comments

Comments
 (0)