Sums in normed real vector spaces

src/linear-algebra.lagda.md

@@ -58,6 +58,7 @@ open import linear-algebra.linear-forms-left-modules-commutative-rings public
 open import linear-algebra.linear-forms-vector-spaces public
 open import linear-algebra.linear-maps-left-modules-commutative-rings public
 open import linear-algebra.linear-maps-left-modules-rings public
+open import linear-algebra.linear-maps-real-vector-spaces public
 open import linear-algebra.linear-maps-vector-spaces public
 open import linear-algebra.linear-spans-left-modules-rings public
 open import linear-algebra.matrices public
@@ -90,7 +91,10 @@ open import linear-algebra.standard-euclidean-vector-spaces public
 open import linear-algebra.subsets-left-modules-commutative-rings public
 open import linear-algebra.subsets-left-modules-rings public
 open import linear-algebra.subspaces-vector-spaces public
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-rings public
 open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public
+open import linear-algebra.sums-of-finite-sequences-of-elements-real-vector-spaces public
+open import linear-algebra.sums-of-finite-sequences-of-elements-vector-spaces public
 open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
 open import linear-algebra.transposition-matrices public
 open import linear-algebra.tuples-on-commutative-monoids public

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

@@ -90,6 +90,11 @@ module _
     (x y : type-left-module-Ring) → type-left-module-Ring
   add-left-module-Ring = add-Ab ab-left-module-Ring
 
+  ap-add-left-module-Ring :
+    {x y x' y' : type-left-module-Ring} →
+    x ＝ x' → y ＝ y' → add-left-module-Ring x y ＝ add-left-module-Ring x' y'
+  ap-add-left-module-Ring = ap-add-Ab ab-left-module-Ring
+
   zero-left-module-Ring : type-left-module-Ring
   zero-left-module-Ring = zero-Ab ab-left-module-Ring
 
@@ -102,6 +107,10 @@ module _
   neg-left-module-Ring : type-left-module-Ring → type-left-module-Ring
   neg-left-module-Ring = neg-Ab ab-left-module-Ring
 
+  diff-left-module-Ring :
+    type-left-module-Ring → type-left-module-Ring → type-left-module-Ring
+  diff-left-module-Ring = right-subtraction-Ab ab-left-module-Ring
+
   endomorphism-ring-ab-left-module-Ring : Ring l2
   endomorphism-ring-ab-left-module-Ring =
     endomorphism-ring-Ab ab-left-module-Ring

src/linear-algebra/linear-maps-real-vector-spaces.lagda.md

@@ -0,0 +1,69 @@
+# Linear maps between real vector spaces
+
+```agda
+module linear-algebra.linear-maps-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import linear-algebra.linear-maps-vector-spaces
+open import linear-algebra.real-vector-spaces
+
+open import real-numbers.field-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "linear map" Disambiguation="between two real vector spaces" Agda=linear-map-ℝ-Vector-Space}}
+between [real vector spaces](linear-algebra.real-vector-spaces.md) `V` and `W`
+is a map `f : V → W` such that `f (v₁ + v₂) = f v₁ + f v₂` and
+`f (c * v) ＝ c * f v`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (W : ℝ-Vector-Space l1 l3)
+  where
+
+  is-additive-map-prop-ℝ-Vector-Space :
+    subtype (l2 ⊔ l3) (type-ℝ-Vector-Space V → type-ℝ-Vector-Space W)
+  is-additive-map-prop-ℝ-Vector-Space =
+    is-additive-map-prop-Vector-Space (heyting-field-ℝ l1) V W
+
+  is-additive-map-ℝ-Vector-Space :
+    (type-ℝ-Vector-Space V → type-ℝ-Vector-Space W) → UU (l2 ⊔ l3)
+  is-additive-map-ℝ-Vector-Space =
+    is-in-subtype is-additive-map-prop-ℝ-Vector-Space
+
+  is-homogeneous-map-prop-ℝ-Vector-Space :
+    subtype (lsuc l1 ⊔ l2 ⊔ l3) (type-ℝ-Vector-Space V → type-ℝ-Vector-Space W)
+  is-homogeneous-map-prop-ℝ-Vector-Space =
+    is-homogeneous-map-prop-Vector-Space (heyting-field-ℝ l1) V W
+
+  is-homogeneous-map-ℝ-Vector-Space :
+    (type-ℝ-Vector-Space V → type-ℝ-Vector-Space W) → UU (lsuc l1 ⊔ l2 ⊔ l3)
+  is-homogeneous-map-ℝ-Vector-Space =
+    is-in-subtype is-homogeneous-map-prop-ℝ-Vector-Space
+
+  is-linear-map-prop-ℝ-Vector-Space :
+    subtype (lsuc l1 ⊔ l2 ⊔ l3) (type-ℝ-Vector-Space V → type-ℝ-Vector-Space W)
+  is-linear-map-prop-ℝ-Vector-Space =
+    is-linear-map-prop-Vector-Space (heyting-field-ℝ l1) V W
+
+  is-linear-map-ℝ-Vector-Space :
+    (type-ℝ-Vector-Space V → type-ℝ-Vector-Space W) → UU (lsuc l1 ⊔ l2 ⊔ l3)
+  is-linear-map-ℝ-Vector-Space = is-in-subtype is-linear-map-prop-ℝ-Vector-Space
+
+  linear-map-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2 ⊔ l3)
+  linear-map-ℝ-Vector-Space = type-subtype is-linear-map-prop-ℝ-Vector-Space
+```

src/linear-algebra/normed-real-vector-spaces.lagda.md

@@ -192,6 +192,11 @@ module _
   right-inverse-law-add-Normed-ℝ-Vector-Space =
     right-inverse-law-add-Ab ab-Normed-ℝ-Vector-Space
 
+  mul-Normed-ℝ-Vector-Space :
+    ℝ l1 → type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space
+  mul-Normed-ℝ-Vector-Space =
+    mul-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
   map-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ l1
   map-norm-Normed-ℝ-Vector-Space = pr1 (pr1 norm-Normed-ℝ-Vector-Space)
 

src/linear-algebra/real-vector-spaces.lagda.md

@@ -84,8 +84,7 @@ module _
 
   diff-ℝ-Vector-Space :
     type-ℝ-Vector-Space → type-ℝ-Vector-Space → type-ℝ-Vector-Space
-  diff-ℝ-Vector-Space v w =
-    add-ℝ-Vector-Space v (neg-ℝ-Vector-Space w)
+  diff-ℝ-Vector-Space = diff-Vector-Space (heyting-field-ℝ l1) V
 
   associative-add-ℝ-Vector-Space :
     (v w x : type-ℝ-Vector-Space) →

src/linear-algebra/standard-euclidean-vector-spaces.lagda.md

@@ -14,8 +14,7 @@ open import elementary-number-theory.natural-numbers
 open import foundation.sets
 open import foundation.universe-levels
 
-open import linear-algebra.dependent-products-left-modules-commutative-rings
-open import linear-algebra.left-modules-commutative-rings
+open import linear-algebra.function-real-vector-spaces
 open import linear-algebra.real-vector-spaces
 
 open import real-numbers.dedekind-real-numbers
@@ -38,12 +37,7 @@ The
 
 ```agda
 vector-space-ℝ-Fin : ℕ → (l : Level) → ℝ-Vector-Space l (lsuc l)
-vector-space-ℝ-Fin n l =
-  Π-left-module-Commutative-Ring
-    ( commutative-ring-ℝ l)
-    ( Fin n)
-    ( λ _ →
-      left-module-commutative-ring-Commutative-Ring (commutative-ring-ℝ l))
+vector-space-ℝ-Fin n l = vector-space-function-ℝ l (Fin n)
 
 set-ℝ-Fin : ℕ → (l : Level) → Set (lsuc l)
 set-ℝ-Fin n l = set-ℝ-Vector-Space (vector-space-ℝ-Fin n l)