Skip to content

Commit ebc4d50

Browse files
SimonBrandnerSimonBrandner
authored
Add linear combinations, linear spans and tuple concatenation (#1537)
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.
1 parent 8b7575d commit ebc4d50

6 files changed

+665
-0
lines changed

‎src/linear-algebra.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ open import linear-algebra.functoriality-matrices public
2525
open import linear-algebra.left-modules-commutative-rings public
2626
open import linear-algebra.left-modules-rings public
2727
open import linear-algebra.left-submodules-rings public
28+
open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings public
2829
open import linear-algebra.linear-maps-left-modules-rings public
30+
open import linear-algebra.linear-spans-left-modules-rings public
2931
open import linear-algebra.matrices public
3032
open import linear-algebra.matrices-on-rings public
3133
open import linear-algebra.multiplication-matrices public

‎src/linear-algebra/linear-combinations-tuples-of-vectors-left-modules-rings.lagda.md‎

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

0 commit comments

Comments
 (0)