Add submodules of left modules over rings (#1511)

This PR adds subsets of left modules over rings. If such a subset
contains the zero element/vector, is closed under addition and
multiplication by a scalar from the ring, we call this subset a
submodule. The PR contains a proof that the intersection of a family of
submodules forms a submodule and a proof that a submodule has the
structure of a module.

Thanks to @VojtechStep for some help along the way!

Author: SimonBrandner

CONTRIBUTORS.toml

@@ -275,3 +275,9 @@ github = "arnoudvanderleer"
 displayName = "Ben Connors"
 usernames = [ "Ben Connors" ]
 github = "ben-connors"
+
+[[contributors]]
+displayName = "Šimon Brandner"
+usernames = ["Šimon Brandner"]
+github = "SimonBrandner"
+homepage = "https://simonbrandner.cz/"

src/linear-algebra.lagda.md

@@ -20,6 +20,7 @@ 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-submodules-rings public
 open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.matrices public
 open import linear-algebra.matrices-on-rings public
@@ -30,6 +31,7 @@ open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public
 open import linear-algebra.scalar-multiplication-tuples public
 open import linear-algebra.scalar-multiplication-tuples-on-rings public
+open import linear-algebra.subsets-left-modules-rings public
 open import linear-algebra.transposition-matrices public
 open import linear-algebra.tuples-on-commutative-monoids public
 open import linear-algebra.tuples-on-commutative-rings public

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

@@ -83,6 +83,9 @@ module _
   type-left-module-Ring : UU l2
   type-left-module-Ring = type-Ab ab-left-module-Ring
 
+  is-set-type-left-module-Ring : is-set type-left-module-Ring
+  is-set-type-left-module-Ring = pr2 set-left-module-Ring
+
   add-left-module-Ring :
     (x y : type-left-module-Ring) → type-left-module-Ring
   add-left-module-Ring = add-Ab ab-left-module-Ring
@@ -133,6 +136,16 @@ module _
     associative-add-Ab ab-left-module-Ring
 ```
 
+### Commutativity of addition
+
+```agda
+  commutative-add-left-module-Ring :
+    (x y : type-left-module-Ring) →
+    add-left-module-Ring x y ＝ add-left-module-Ring y x
+  commutative-add-left-module-Ring =
+    commutative-add-Ab ab-left-module-Ring
+```
+
 ### Unit laws for addition
 
 ```agda