Add linear independence and left modules with an ordered basis

Signed-off-by: Šimon Brandner <[email protected]>

Author: SimonBrandner

src/linear-algebra.lagda.md

@@ -24,8 +24,10 @@ open import linear-algebra.finite-sequences-in-semirings public
 open import linear-algebra.functoriality-matrices public
 open import linear-algebra.left-modules-commutative-rings public
 open import linear-algebra.left-modules-rings public
+open import linear-algebra.left-modules-with-ordered-bases-rings public
 open import linear-algebra.left-submodules-rings public
 open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings public
+open import linear-algebra.linear-independence-left-modules-rings public
 open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.linear-spans-left-modules-rings public
 open import linear-algebra.matrices public

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

@@ -7,6 +7,7 @@ module linear-algebra.left-modules-rings where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.ring-of-integers
 
 open import foundation.action-on-identifications-functions
@@ -26,6 +27,8 @@ open import group-theory.endomorphism-rings-abelian-groups
 open import group-theory.homomorphisms-abelian-groups
 open import group-theory.homomorphisms-semigroups
 
+open import lists.tuples
+
 open import ring-theory.homomorphisms-rings
 open import ring-theory.opposite-rings
 open import ring-theory.rings
@@ -120,6 +123,11 @@ module _
         ( endomorphism-ring-Ab ab-left-module-Ring)
         ( mul-hom-left-module-Ring)
         ( x))
+
+  trivial-tuple-left-module-Ring : (n : ℕ) → tuple (type-Ring R) n
+  trivial-tuple-left-module-Ring zero-ℕ = empty-tuple
+  trivial-tuple-left-module-Ring (succ-ℕ n) =
+    zero-Ring R ∷ trivial-tuple-left-module-Ring n
 ```
 
 ## Properties

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

@@ -0,0 +1,51 @@
+# Left modules over rings with ordered basis
+
+```agda
+module linear-algebra.left-modules-with-ordered-bases-rings 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-left-modules-rings
+open import linear-algebra.linear-spans-left-modules-rings
+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 bases
+
+```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-left-module-Ring 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-left-modules-rings.lagda.md

@@ -0,0 +1,90 @@
+# Linear independence
+
+```agda
+module linear-algebra.linear-independence-left-modules-rings 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-tuples-of-vectors-left-modules-rings
+
+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
+
+  is-linearly-independent-tuple-left-module-Ring-prop : Prop (l1 ⊔ l2)
+  is-linearly-independent-tuple-left-module-Ring-prop =
+    Π-Prop
+      ( tuple (type-Ring R) n)
+      λ scalars →
+        hom-Prop
+          ( Id-Prop
+            ( set-left-module-Ring R M)
+            ( linear-combination-tuple-left-module-Ring R M scalars vectors)
+            ( zero-left-module-Ring R M))
+          ( Id-Prop
+            ( tuple-Set (set-Ring R) n)
+            ( scalars)
+            ( trivial-tuple-left-module-Ring R M n))
+
+  is-linearly-independent-tuple-left-module-Ring : UU (l1 ⊔ l2)
+  is-linearly-independent-tuple-left-module-Ring =
+    type-Prop is-linearly-independent-tuple-left-module-Ring-prop
+```
+
+### Linearly independent tuple in a left-module over ring
+
+```agda
+linearly-independent-tuple-left-module-Ring :
+  {l1 l2 : Level}
+  (n : ℕ) (R : Ring l1) (M : left-module-Ring l2 R) → UU (l1 ⊔ l2)
+linearly-independent-tuple-left-module-Ring n R M =
+  Σ
+    ( tuple (type-left-module-Ring R M) n)
+    ( λ v → is-linearly-independent-tuple-left-module-Ring R M v)
+
+module _
+  {l1 l2 : Level}
+  {n : ℕ}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (v : linearly-independent-tuple-left-module-Ring 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

@@ -11,6 +11,7 @@ open import foundation.conjunction
 open import foundation.dependent-pair-types
 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
@@ -51,6 +52,11 @@ module _
   inclusion-subset-left-module-Ring :
     type-subset-left-module-Ring → type-left-module-Ring R M
   inclusion-subset-left-module-Ring = pr1
+
+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