Add linear independence and left modules with an ordered basis

Signed-off-by: Šimon Brandner <simon.bra.ag@gmail.com>

Author: SimonBrandner

src/linear-algebra.lagda.md

@@ -22,8 +22,10 @@ open import linear-algebra.finite-sequences-in-semigroups public
 open import linear-algebra.finite-sequences-in-semirings public
 open import linear-algebra.functoriality-matrices public
 open import linear-algebra.left-modules-rings public
+open import linear-algebra.left-modules-rings-with-ordered-basis public
 open import linear-algebra.left-submodules-rings public
 open import linear-algebra.linear-combinations public
+open import linear-algebra.linear-independence public
 open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.linear-spans public
 open import linear-algebra.matrices public

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

@@ -0,0 +1,50 @@
+# Left modules over rings with ordered basis
+
+```agda
+module linear-algebra.left-modules-rings-with-ordered-basis where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.linear-independence
+open import linear-algebra.linear-spans
+open import linear-algebra.subsets-left-modules-rings
+
+open import lists.tuples
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "left module over a ring with an ordered basis" Agda=left-module-with-ordered-basis-Ring}}
+is a [left module](linear-algebra.left-modules-rings.md) `M` over a
+[ring](ring-theory.rings.md) `R` with a linearly independent tuple whose linear
+span is the whole of `M`.
+
+## Definitions
+
+### Left modules over rings with ordered basis
+
+```agda
+left-module-with-ordered-basis-Ring :
+  {l1 : Level} (n : ℕ) (l : Level) (R : Ring l1) → UU (l1 ⊔ lsuc l)
+left-module-with-ordered-basis-Ring {l1} n l R =
+  Σ
+    ( Σ (left-module-Ring l R) (λ M → linearly-independent-tuple n R M))
+    ( λ (M , b) → is-linear-span-subset-left-module-Ring R M
+      ( whole-subset-left-module-Ring R M)
+      ( subset-tuple (tuple-linearly-independent-tuple R M b)))
+```

src/linear-algebra/linear-independence.lagda.md

@@ -0,0 +1,93 @@
+# Linear independence
+
+```agda
+module linear-algebra.linear-independence where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import foundation-core.sets
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.linear-combinations
+
+open import lists.tuples
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+Let `M` be a [left module](linear-algebra.left-modules-rings.md) over a
+[ring](ring-theory.rings.md) `R`. A tuple `x_1, ..., x_n` of elements of `M` is
+{{#concept "linearly independent" Agda=is-linearly-independent-tuple-prop Agda=linearly-independent-tuple}},
+if `r_1 * x_1 + ... + r_n * x_n = 0` implies `r_1 = ... = r_n = 0`.
+
+## Definitions
+
+### The condition of a tuple being linearly independent
+
+```agda
+module _
+  {l1 l2 : Level}
+  {n : ℕ}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (vectors : tuple (type-left-module-Ring R M) n)
+  where
+
+  trivial-tuple : (n : ℕ) → tuple (type-Ring R) n
+  trivial-tuple zero-ℕ = empty-tuple
+  trivial-tuple (succ-ℕ n) = zero-Ring R ∷ trivial-tuple n
+
+  is-linearly-independent-tuple-prop : Prop (l1 ⊔ l2)
+  is-linearly-independent-tuple-prop =
+    Π-Prop
+      ( tuple (type-Ring R) n)
+      λ scalars →
+        hom-Prop
+          ( Id-Prop
+            ( set-left-module-Ring R M)
+            ( linear-combination-left-module-Ring R M scalars vectors)
+            ( zero-left-module-Ring R M))
+          ( Id-Prop
+            ( tuple-Set (set-Ring R) n)
+            ( scalars)
+            ( trivial-tuple n))
+
+  is-linearly-independent-tuple : UU (l1 ⊔ l2)
+  is-linearly-independent-tuple = type-Prop is-linearly-independent-tuple-prop
+```
+
+### Linearly independent tuple in a left-module over ring
+
+```agda
+linearly-independent-tuple :
+  {l1 l2 : Level}
+  (n : ℕ) (R : Ring l1) (M : left-module-Ring l2 R) → UU (l1 ⊔ l2)
+linearly-independent-tuple n R M =
+  Σ
+    ( tuple (type-left-module-Ring R M) n)
+    ( λ v → is-linearly-independent-tuple R M v)
+
+module _
+  {l1 l2 : Level}
+  {n : ℕ}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (v : linearly-independent-tuple n R M)
+  where
+
+  tuple-linearly-independent-tuple : tuple (type-left-module-Ring R M) n
+  tuple-linearly-independent-tuple = pr1 v
+```

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

@@ -10,6 +10,7 @@ module linear-algebra.subsets-left-modules-rings where
 open import foundation.conjunction
 open import foundation.propositions
 open import foundation.subtypes
+open import foundation.unit-type
 open import foundation.universe-levels
 
 open import linear-algebra.left-modules-rings
@@ -44,6 +45,11 @@ type-subset-left-module-Ring :
   (S : subset-left-module-Ring l3 R M) →
   UU (l2 ⊔ l3)
 type-subset-left-module-Ring R M S = type-subtype S
+
+whole-subset-left-module-Ring :
+  {l1 l2 l3 : Level}
+  (R : Ring l1) (M : left-module-Ring l2 R) → subset-left-module-Ring l3 R M
+whole-subset-left-module-Ring R M _ = raise-unit-Prop _
 ```
 
 ### The condition that a subset is closed under addition

src/lists/tuples.lagda.md

@@ -18,15 +18,19 @@ open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.sets
+open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.truncated-types
 open import foundation.truncation-levels
 open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-higher-homotopies-composition
 
+open import foundation-core.empty-types
+
 open import univalent-combinatorics.standard-finite-types
 ```
 
@@ -96,6 +100,9 @@ module _
   eq-component-tuple-index-in-tuple
     (succ-ℕ n) a (x ∷ v) (is-in-tail .a .x .v I) =
     eq-component-tuple-index-in-tuple n a v I
+
+  subset-tuple : {n : ℕ} (v : tuple A n) → subtype l A
+  subset-tuple v a = trunc-Prop (a ∈-tuple v)
 ```
 
 ## Properties