Skip to content

Commit 1d3b859

Browse files
SimonBrandnerSimonBrandner
committed
Add linear independence and left modules with an ordered basis
Signed-off-by: Šimon Brandner <[email protected]>
1 parent 04645dd commit 1d3b859

File tree

6 files changed

+218
-0
lines changed

6 files changed

+218
-0
lines changed

‎src/linear-algebra.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,10 @@ open import linear-algebra.finite-sequences-in-semirings public
2424
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
27+
open import linear-algebra.left-modules-with-ordered-bases-rings public
2728
open import linear-algebra.left-submodules-rings public
2829
open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings public
30+
open import linear-algebra.linear-independence-left-modules-rings public
2931
open import linear-algebra.linear-maps-left-modules-rings public
3032
open import linear-algebra.linear-spans-left-modules-rings public
3133
open import linear-algebra.matrices public

‎src/linear-algebra/left-modules-rings.lagda.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module linear-algebra.left-modules-rings where
77
<details><summary>Imports</summary>
88

99
```agda
10+
open import elementary-number-theory.natural-numbers
1011
open import elementary-number-theory.ring-of-integers
1112
1213
open import foundation.action-on-identifications-functions
@@ -26,6 +27,8 @@ open import group-theory.endomorphism-rings-abelian-groups
2627
open import group-theory.homomorphisms-abelian-groups
2728
open import group-theory.homomorphisms-semigroups
2829
30+
open import lists.tuples
31+
2932
open import ring-theory.homomorphisms-rings
3033
open import ring-theory.opposite-rings
3134
open import ring-theory.rings
@@ -120,6 +123,11 @@ module _
120123
( endomorphism-ring-Ab ab-left-module-Ring)
121124
( mul-hom-left-module-Ring)
122125
( x))
126+
127+
trivial-tuple-left-module-Ring : (n : ℕ) → tuple (type-Ring R) n
128+
trivial-tuple-left-module-Ring zero-ℕ = empty-tuple
129+
trivial-tuple-left-module-Ring (succ-ℕ n) =
130+
zero-Ring R ∷ trivial-tuple-left-module-Ring n
123131
```
124132

125133
## Properties

‎src/linear-algebra/left-modules-with-ordered-bases-rings.lagda.md‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
# Left modules over rings with ordered basis
2+
3+
```agda
4+
module linear-algebra.left-modules-with-ordered-bases-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.dependent-pair-types
13+
open import foundation.universe-levels
14+
15+
open import foundation-core.cartesian-product-types
16+
17+
open import linear-algebra.left-modules-rings
18+
open import linear-algebra.linear-independence-left-modules-rings
19+
open import linear-algebra.linear-spans-left-modules-rings
20+
open import linear-algebra.subsets-left-modules-rings
21+
22+
open import lists.tuples
23+
24+
open import ring-theory.rings
25+
```
26+
27+
</details>
28+
29+
## Idea
30+
31+
A
32+
{{#concept "left module over a ring with an ordered basis" Agda=left-module-with-ordered-basis-Ring}}
33+
is a [left module](linear-algebra.left-modules-rings.md) `M` over a
34+
[ring](ring-theory.rings.md) `R` with a linearly independent tuple whose linear
35+
span is the whole of `M`.
36+
37+
## Definitions
38+
39+
### Left modules over rings with ordered bases
40+
41+
```agda
42+
left-module-with-ordered-basis-Ring :
43+
{l1 : Level} (n : ℕ) (l : Level) (R : Ring l1) → UU (l1 ⊔ lsuc l)
44+
left-module-with-ordered-basis-Ring {l1} n l R =
45+
Σ
46+
( Σ ( left-module-Ring l R)
47+
( λ M → linearly-independent-tuple-left-module-Ring n R M))
48+
( λ (M , b) → is-linear-span-subset-left-module-Ring R M
49+
( whole-subset-left-module-Ring R M)
50+
( subset-tuple (tuple-linearly-independent-tuple R M b)))
51+
```

‎src/linear-algebra/linear-independence-left-modules-rings.lagda.md‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
# Linear independence
2+
3+
```agda
4+
module linear-algebra.linear-independence-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.dependent-pair-types
13+
open import foundation.identity-types
14+
open import foundation.propositions
15+
open import foundation.universe-levels
16+
17+
open import foundation-core.sets
18+
19+
open import linear-algebra.left-modules-rings
20+
open import linear-algebra.subsets-left-modules-rings
21+
open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings
22+
23+
open import lists.tuples
24+
open import lists.functoriality-tuples
25+
26+
open import ring-theory.rings
27+
```
28+
29+
</details>
30+
31+
## Idea
32+
33+
Let `M` be a [left module](linear-algebra.left-modules-rings.md) over a
34+
[ring](ring-theory.rings.md) `R`.
35+
36+
A tuple `x_1, ..., x_n` of elements of `M` is a
37+
{{#concept "linearly independent tuple" Agda=is-linearly-independent-tuple-left-module-prop-Ring Agda=linearly-independent-tuple-left-module-Ring}},
38+
if `r_1 * x_1 + ... + r_n * x_n = 0` implies `r_1 = ... = r_n = 0`.
39+
40+
A subset `S` of `M` is a
41+
{{#concept "linearly independent subset" Agda=is-linearly-independent-subset-left-module-prop-Ring Agda=linearly-independent-subset-left-module-Ring}}
42+
if any tuple `x_1, ..., x_n` of elements of `S` is linearly independent.
43+
44+
## Definitions
45+
46+
### The condition of a tuple being linearly independent
47+
48+
```agda
49+
module _
50+
{l1 l2 : Level}
51+
{n : ℕ}
52+
(R : Ring l1)
53+
(M : left-module-Ring l2 R)
54+
(vectors : tuple (type-left-module-Ring R M) n)
55+
where
56+
57+
is-linearly-independent-tuple-left-module-prop-Ring : Prop (l1 ⊔ l2)
58+
is-linearly-independent-tuple-left-module-prop-Ring =
59+
Π-Prop
60+
( tuple (type-Ring R) n)
61+
λ scalars →
62+
hom-Prop
63+
( Id-Prop
64+
( set-left-module-Ring R M)
65+
( linear-combination-tuple-left-module-Ring R M scalars vectors)
66+
( zero-left-module-Ring R M))
67+
( Id-Prop
68+
( tuple-Set (set-Ring R) n)
69+
( scalars)
70+
( trivial-tuple-left-module-Ring R M n))
71+
72+
is-linearly-independent-tuple-left-module-Ring : UU (l1 ⊔ l2)
73+
is-linearly-independent-tuple-left-module-Ring =
74+
type-Prop is-linearly-independent-tuple-left-module-prop-Ring
75+
```
76+
77+
### Linearly independent tuple in a left-module over a ring
78+
79+
```agda
80+
linearly-independent-tuple-left-module-Ring :
81+
{l1 l2 : Level}
82+
(n : ℕ) (R : Ring l1) (M : left-module-Ring l2 R) → UU (l1 ⊔ l2)
83+
linearly-independent-tuple-left-module-Ring n R M =
84+
Σ ( tuple (type-left-module-Ring R M) n)
85+
( λ v → is-linearly-independent-tuple-left-module-Ring R M v)
86+
87+
module _
88+
{l1 l2 : Level}
89+
{n : ℕ}
90+
(R : Ring l1)
91+
(M : left-module-Ring l2 R)
92+
(vectors : linearly-independent-tuple-left-module-Ring n R M)
93+
where
94+
95+
tuple-linearly-independent-tuple : tuple (type-left-module-Ring R M) n
96+
tuple-linearly-independent-tuple = pr1 vectors
97+
```
98+
99+
### The condition of a subset being linearly independent
100+
101+
```agda
102+
module _
103+
{l1 l2 l3 : Level}
104+
(R : Ring l1)
105+
(M : left-module-Ring l2 R)
106+
(S : subset-left-module-Ring l3 R M)
107+
where
108+
109+
is-linearly-independent-subset-left-module-prop-Ring : Prop (l1 ⊔ l2 ⊔ l3)
110+
is-linearly-independent-subset-left-module-prop-Ring =
111+
Π-Prop
112+
( ℕ)
113+
( λ n →
114+
Π-Prop
115+
( tuple (type-subset-left-module-Ring R M S) n)
116+
( λ vectors → is-linearly-independent-tuple-left-module-prop-Ring R M
117+
( map-tuple (inclusion-subset-left-module-Ring R M S) vectors)))
118+
119+
is-linearly-independent-subset-left-module-Ring : UU (l1 ⊔ l2 ⊔ l3)
120+
is-linearly-independent-subset-left-module-Ring =
121+
type-Prop is-linearly-independent-subset-left-module-prop-Ring
122+
```
123+
124+
### Linearly independent subset of a left module over a ring
125+
126+
```agda
127+
linearly-independent-subset-left-module-Ring :
128+
{l1 l2 : Level}
129+
(l3 : Level) (R : Ring l1) (M : left-module-Ring l2 R) →
130+
UU (l1 ⊔ l2 ⊔ lsuc l3)
131+
linearly-independent-subset-left-module-Ring l3 R M =
132+
Σ ( subset-left-module-Ring l3 R M)
133+
( λ S → is-linearly-independent-subset-left-module-Ring R M S)
134+
135+
module _
136+
{l1 l2 l3 : Level}
137+
(R : Ring l1)
138+
(M : left-module-Ring l2 R)
139+
(S : linearly-independent-subset-left-module-Ring l3 R M)
140+
where
141+
142+
subset-linearly-independent-tuple : subset-left-module-Ring l3 R M
143+
subset-linearly-independent-tuple = pr1 S
144+
```

‎src/linear-algebra/subsets-left-modules-rings.lagda.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ open import foundation.conjunction
1111
open import foundation.dependent-pair-types
1212
open import foundation.propositions
1313
open import foundation.subtypes
14+
open import foundation.unit-type
1415
open import foundation.universe-levels
1516
1617
open import linear-algebra.left-modules-rings
@@ -51,6 +52,11 @@ module _
5152
inclusion-subset-left-module-Ring :
5253
type-subset-left-module-Ring → type-left-module-Ring R M
5354
inclusion-subset-left-module-Ring = pr1
55+
56+
whole-subset-left-module-Ring :
57+
{l1 l2 l3 : Level}
58+
(R : Ring l1) (M : left-module-Ring l2 R) → subset-left-module-Ring l3 R M
59+
whole-subset-left-module-Ring R M _ = raise-unit-Prop _
5460
```
5561

5662
### The condition that a subset is closed under addition

‎src/lists/tuples.lagda.md‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,15 +18,19 @@ open import foundation.equality-dependent-pair-types
1818
open import foundation.equivalences
1919
open import foundation.homotopies
2020
open import foundation.identity-types
21+
open import foundation.propositional-truncations
2122
open import foundation.raising-universe-levels
2223
open import foundation.sets
24+
open import foundation.subtypes
2325
open import foundation.transport-along-identifications
2426
open import foundation.truncated-types
2527
open import foundation.truncation-levels
2628
open import foundation.unit-type
2729
open import foundation.universe-levels
2830
open import foundation.whiskering-higher-homotopies-composition
2931
32+
open import foundation-core.empty-types
33+
3034
open import univalent-combinatorics.standard-finite-types
3135
```
3236

@@ -96,6 +100,9 @@ module _
96100
eq-component-tuple-index-in-tuple
97101
(succ-ℕ n) a (x ∷ v) (is-in-tail .a .x .v I) =
98102
eq-component-tuple-index-in-tuple n a v I
103+
104+
subset-tuple : {n : ℕ} (v : tuple A n) → subtype l A
105+
subset-tuple v a = trunc-Prop (a ∈-tuple v)
99106
```
100107

101108
## Properties

0 commit comments

Comments
 (0)