Improve code quality in the linear algebra namespace (#1544)

Author: SimonBrandner

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

@@ -146,7 +146,7 @@ is-closed-under-negation-left-submodule-Ring :
     ( subset-left-submodule-Ring R M N)
 is-closed-under-negation-left-submodule-Ring R M N x x-in-subset =
   tr
-    ( λ x' → pr1 (subset-left-submodule-Ring R M N x'))
+    ( λ x' → type-Prop (subset-left-submodule-Ring R M N x'))
     ( mul-neg-one-left-module-Ring R M x)
     ( is-closed-under-multiplication-by-scalar-left-submodule-Ring R M N
       ( neg-one-Ring R)
@@ -194,18 +194,23 @@ module _
 
   neg-left-submodule-Ring :
     type-left-submodule-Ring R M N → type-left-submodule-Ring R M N
-  pr1 (neg-left-submodule-Ring x) = neg-left-module-Ring R M (pr1 x)
+  pr1 (neg-left-submodule-Ring x) =
+    neg-left-module-Ring R M (inclusion-left-submodule-Ring R M N x)
   pr2 (neg-left-submodule-Ring x) =
-    is-closed-under-negation-left-submodule-Ring R M N (pr1 x) (pr2 x)
+    is-closed-under-negation-left-submodule-Ring R M N
+      ( inclusion-left-submodule-Ring R M N x)
+      ( pr2 x)
 
   add-left-submodule-Ring :
     (x y : type-left-submodule-Ring R M N) → type-left-submodule-Ring R M N
   pr1 (add-left-submodule-Ring x y) =
-    add-left-module-Ring R M (pr1 x) (pr1 y)
+    add-left-module-Ring R M
+      ( inclusion-left-submodule-Ring R M N x)
+      ( inclusion-left-submodule-Ring R M N y)
   pr2 (add-left-submodule-Ring x y) =
     is-closed-under-addition-left-submodule-Ring R M N
-      ( pr1 x)
-      ( pr1 y)
+      ( inclusion-left-submodule-Ring R M N x)
+      ( inclusion-left-submodule-Ring R M N y)
       ( pr2 x)
       ( pr2 y)
 
@@ -214,10 +219,10 @@ module _
     (x : type-left-submodule-Ring R M N) →
     type-left-submodule-Ring R M N
   pr1 (mul-left-submodule-Ring r x) =
-    mul-left-module-Ring R M r (pr1 x)
+    mul-left-module-Ring R M r (inclusion-left-submodule-Ring R M N x)
   pr2 (mul-left-submodule-Ring r x) =
     is-closed-under-multiplication-by-scalar-left-submodule-Ring R M N r
-      ( pr1 x)
+      ( inclusion-left-submodule-Ring R M N x)
       ( pr2 x)
 
   associative-add-left-submodule-Ring :
@@ -226,66 +231,78 @@ module _
     add-left-submodule-Ring x (add-left-submodule-Ring y z)
   associative-add-left-submodule-Ring x y z =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( associative-add-left-module-Ring R M (pr1 x) (pr1 y) (pr1 z))
+      ( associative-add-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x)
+        ( inclusion-left-submodule-Ring R M N y)
+        ( inclusion-left-submodule-Ring R M N z))
 
   left-unit-law-add-left-submodule-Ring :
     (x : type-left-submodule-Ring R M N) →
     add-left-submodule-Ring (unit-left-submodule-Ring R M N) x ＝ x
   left-unit-law-add-left-submodule-Ring x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( left-unit-law-add-left-module-Ring R M (pr1 x))
+      ( left-unit-law-add-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x))
 
   right-unit-law-add-left-submodule-Ring :
     (x : type-left-submodule-Ring R M N) →
     add-left-submodule-Ring x (unit-left-submodule-Ring R M N) ＝ x
   right-unit-law-add-left-submodule-Ring x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( right-unit-law-add-left-module-Ring R M (pr1 x))
+      ( right-unit-law-add-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x))
 
   left-inverse-law-add-left-submodule-Ring :
     (x : type-left-submodule-Ring R M N) →
     add-left-submodule-Ring (neg-left-submodule-Ring x) x ＝
     unit-left-submodule-Ring R M N
   left-inverse-law-add-left-submodule-Ring x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( left-inverse-law-add-left-module-Ring R M (pr1 x))
+      ( left-inverse-law-add-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x))
 
   right-inverse-law-add-left-submodule-Ring :
     (x : type-left-submodule-Ring R M N) →
     add-left-submodule-Ring x (neg-left-submodule-Ring x) ＝
     unit-left-submodule-Ring R M N
   right-inverse-law-add-left-submodule-Ring x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( right-inverse-law-add-left-module-Ring R M (pr1 x))
+      ( right-inverse-law-add-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x))
 
   commutative-add-left-submodule-Ring :
     (x y : type-left-submodule-Ring R M N) →
     add-left-submodule-Ring x y ＝ add-left-submodule-Ring y x
   commutative-add-left-submodule-Ring x y =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( commutative-add-left-module-Ring R M (pr1 x) (pr1 y))
+      ( commutative-add-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x)
+        ( inclusion-left-submodule-Ring R M N y))
 
-  left-distributive-law-mul-add-left-submodule-Ring :
+  left-distributive-mul-add-left-submodule-Ring :
     (r : type-Ring R)
     (x y : type-left-submodule-Ring R M N) →
     mul-left-submodule-Ring r (add-left-submodule-Ring x y) ＝
     add-left-submodule-Ring
       ( mul-left-submodule-Ring r x)
       ( mul-left-submodule-Ring r y)
-  left-distributive-law-mul-add-left-submodule-Ring r x y =
+  left-distributive-mul-add-left-submodule-Ring r x y =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( left-distributive-mul-add-left-module-Ring R M r (pr1 x) (pr1 y))
+      ( left-distributive-mul-add-left-module-Ring R M r
+        ( inclusion-left-submodule-Ring R M N x)
+        ( inclusion-left-submodule-Ring R M N y))
 
-  right-distributive-law-mul-add-left-submodule-Ring :
+  right-distributive-mul-add-left-submodule-Ring :
     (r s : type-Ring R)
     (x : type-left-submodule-Ring R M N) →
     mul-left-submodule-Ring (add-Ring R r s) x ＝
     add-left-submodule-Ring
       ( mul-left-submodule-Ring r x)
       ( mul-left-submodule-Ring s x)
-  right-distributive-law-mul-add-left-submodule-Ring r s x =
+  right-distributive-mul-add-left-submodule-Ring r s x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( right-distributive-mul-add-left-module-Ring R M r s (pr1 x))
+      ( right-distributive-mul-add-left-module-Ring R M r s
+        ( inclusion-left-submodule-Ring R M N x))
 
   associative-mul-left-submodule-Ring :
     (r s : type-Ring R)
@@ -294,14 +311,16 @@ module _
     mul-left-submodule-Ring r (mul-left-submodule-Ring s x)
   associative-mul-left-submodule-Ring r s x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( associative-mul-left-module-Ring R M r s (pr1 x))
+      ( associative-mul-left-module-Ring R M r s
+        ( inclusion-left-submodule-Ring R M N x))
 
   left-unit-law-mul-left-submodule-Ring :
     (x : type-left-submodule-Ring R M N) →
     mul-left-submodule-Ring (one-Ring R) x ＝ x
   left-unit-law-mul-left-submodule-Ring x =
     eq-left-submodule-Ring-eq-left-module-Ring R M N
-      ( left-unit-law-mul-left-module-Ring R M (pr1 x))
+      ( left-unit-law-mul-left-module-Ring R M
+        ( inclusion-left-submodule-Ring R M N x))
 
   set-left-submodule-Ring : Set (l2 ⊔ l3)
   pr1 set-left-submodule-Ring = type-left-submodule-Ring R M N
@@ -340,7 +359,7 @@ module _
     (r : type-Ring R) → hom-Ab ab-left-submodule-Ring ab-left-submodule-Ring
   pr1 (map-hom-left-submodule-Ring r) = mul-left-submodule-Ring r
   pr2 (map-hom-left-submodule-Ring r) {x} {y} =
-    left-distributive-law-mul-add-left-submodule-Ring r x y
+    left-distributive-mul-add-left-submodule-Ring r x y
 
   mul-hom-left-submodule-Ring :
     hom-Ring R endomorphism-ring-left-submodule-Ring
@@ -349,7 +368,7 @@ module _
     eq-htpy-hom-Ab
       ab-left-submodule-Ring
       ab-left-submodule-Ring
-      ( right-distributive-law-mul-add-left-submodule-Ring r s)
+      ( right-distributive-mul-add-left-submodule-Ring r s)
   pr1 (pr2 mul-hom-left-submodule-Ring) {r} {s} =
     eq-htpy-hom-Ab
       ab-left-submodule-Ring

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

@@ -138,6 +138,15 @@ module _
   generators-linear-span-left-module-Ring : subset-left-module-Ring l3 R M
   generators-linear-span-left-module-Ring = pr2 (pr1 S)
 
+  inclusion-generators-linear-span-left-module-Ring :
+    type-subset-left-module-Ring R M generators-linear-span-left-module-Ring →
+    type-left-module-Ring R M
+  inclusion-generators-linear-span-left-module-Ring = pr1
+
+  is-in-linear-span-left-module-Ring : type-left-module-Ring R M → UU l3
+  is-in-linear-span-left-module-Ring x =
+    type-Prop (subset-linear-span-left-module-Ring x)
+
   contains-all-linear-combinations-linear-span-left-module-Ring :
     contains-all-linear-combinations-subset-left-module-Ring R M
       subset-linear-span-left-module-Ring
@@ -193,50 +202,74 @@ module _
             contains-only-linear-combinations-linear-span-left-module-Ring R M S
               ( y , y-in-span)
           tr
-            ( λ z → pr1 (subset-linear-span-left-module-Ring R M S z))
+            ( λ z → is-in-linear-span-left-module-Ring R M S z)
             ( equational-reasoning
               linear-combination-tuple-left-module-Ring R M
                 ( concat-tuple x-scalars y-scalars)
-                ( map-tuple pr1 (concat-tuple x-vectors y-vectors))
+                ( map-tuple
+                  ( inclusion-generators-linear-span-left-module-Ring R M S)
+                  ( concat-tuple x-vectors y-vectors))
               ＝ linear-combination-tuple-left-module-Ring R M
                   ( concat-tuple x-scalars y-scalars)
                   ( concat-tuple
-                    ( map-tuple pr1 x-vectors)
-                    ( map-tuple pr1 y-vectors))
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( x-vectors))
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( y-vectors)))
                 by
                   ap
                     ( λ z →
                       ( linear-combination-tuple-left-module-Ring R M
                         ( concat-tuple x-scalars y-scalars)
                         ( z)))
-                    ( distributive-map-concat-tuple pr1 x-vectors y-vectors)
+                    ( distributive-map-concat-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                        ( x-vectors)
+                        ( y-vectors))
               ＝ add-left-module-Ring R M
                   ( linear-combination-tuple-left-module-Ring R M
                     ( x-scalars)
-                    ( map-tuple pr1 x-vectors))
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( x-vectors)))
                   ( linear-combination-tuple-left-module-Ring R M
                     ( y-scalars)
-                    ( map-tuple pr1 y-vectors))
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( y-vectors)))
                 by
                   add-concat-linear-combination-tuple-left-module-Ring
                     ( R)
                     ( M)
                     ( x-scalars)
-                    ( map-tuple pr1 x-vectors)
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( x-vectors))
                     ( y-scalars)
-                    ( map-tuple pr1 y-vectors)
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( y-vectors))
               ＝ add-left-module-Ring R M
                   ( x)
                   ( linear-combination-tuple-left-module-Ring R M
                     ( y-scalars)
-                    ( map-tuple pr1 y-vectors))
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( y-vectors)))
                 by
                   ap
                     ( λ z → add-left-module-Ring R M
                       ( z)
                       ( linear-combination-tuple-left-module-Ring R M
                         ( y-scalars)
-                        ( map-tuple pr1 y-vectors)))
+                        ( map-tuple
+                          ( inclusion-generators-linear-span-left-module-Ring
+                            ( R)
+                            ( M)
+                            ( S))
+                          ( y-vectors))))
                     ( inv x-identity)
               ＝ add-left-module-Ring R M x y
                 by
@@ -266,24 +299,30 @@ module _
           ( contains-only-linear-combinations-linear-span-left-module-Ring R M S
             ( x , x-in-span))
         ( tr
-          ( λ y → pr1 (subset-linear-span-left-module-Ring R M S y))
+          ( λ y → is-in-linear-span-left-module-Ring R M S y)
           ( equational-reasoning
             linear-combination-tuple-left-module-Ring R M
               ( map-tuple (mul-Ring R r) scalars)
-              ( map-tuple pr1 vectors)
+              ( map-tuple
+                ( inclusion-generators-linear-span-left-module-Ring R M S)
+                ( vectors))
             ＝ mul-left-module-Ring R M
                 ( r)
                 ( linear-combination-tuple-left-module-Ring R M
                   ( scalars)
-                  ( map-tuple pr1 vectors))
+                  ( map-tuple
+                    ( inclusion-generators-linear-span-left-module-Ring R M S)
+                    ( vectors)))
               by
                 inv
                   ( left-distributive-mul-linear-combination-tuple-left-module-Ring
                     ( R)
                     ( M)
                     ( r)
                     ( scalars)
-                    ( map-tuple pr1 vectors))
+                    ( map-tuple
+                      ( inclusion-generators-linear-span-left-module-Ring R M S)
+                      ( vectors)))
             ＝ mul-left-module-Ring R M r x
               by
                 ap

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

@@ -8,6 +8,7 @@ module linear-algebra.subsets-left-modules-rings where
 
 ```agda
 open import foundation.conjunction
+open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
@@ -37,13 +38,19 @@ subset-left-module-Ring :
   (l : Level) (R : Ring l1) (M : left-module-Ring l2 R) → UU (l2 ⊔ lsuc l)
 subset-left-module-Ring l R M = subtype l (type-left-module-Ring R M)
 
-type-subset-left-module-Ring :
+module _
   {l1 l2 l3 : Level}
   (R : Ring l1)
   (M : left-module-Ring l2 R)
-  (S : subset-left-module-Ring l3 R M) →
-  UU (l2 ⊔ l3)
-type-subset-left-module-Ring R M S = type-subtype S
+  (S : subset-left-module-Ring l3 R M)
+  where
+
+  type-subset-left-module-Ring : UU (l2 ⊔ l3)
+  type-subset-left-module-Ring = type-subtype S
+
+  inclusion-subset-left-module-Ring :
+    type-subset-left-module-Ring → type-left-module-Ring R M
+  inclusion-subset-left-module-Ring = pr1
 ```
 
 ### The condition that a subset is closed under addition