Dependent products of real vector spaces (#1943)

Broken out of #1940 .

Author: lowasser

src/linear-algebra.lagda.md

@@ -19,6 +19,8 @@ open import linear-algebra.constant-matrices public
 open import linear-algebra.constant-tuples public
 open import linear-algebra.dependent-products-left-modules-commutative-rings public
 open import linear-algebra.dependent-products-left-modules-rings public
+open import linear-algebra.dependent-products-real-vector-spaces public
+open import linear-algebra.dependent-products-vector-spaces public
 open import linear-algebra.diagonal-matrices-on-rings public
 open import linear-algebra.difference-linear-maps-left-modules-commutative-rings public
 open import linear-algebra.difference-linear-maps-left-modules-rings public
@@ -35,6 +37,9 @@ open import linear-algebra.finite-sequences-in-monoids public
 open import linear-algebra.finite-sequences-in-rings public
 open import linear-algebra.finite-sequences-in-semigroups public
 open import linear-algebra.finite-sequences-in-semirings public
+open import linear-algebra.function-left-modules-rings public
+open import linear-algebra.function-real-vector-spaces public
+open import linear-algebra.function-vector-spaces public
 open import linear-algebra.functoriality-matrices public
 open import linear-algebra.kernels-linear-maps-left-modules-commutative-rings public
 open import linear-algebra.kernels-linear-maps-left-modules-rings public

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

@@ -0,0 +1,33 @@
+# Dependent products of real vector spaces
+
+```agda
+module linear-algebra.dependent-products-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import linear-algebra.dependent-products-vector-spaces
+open import linear-algebra.real-vector-spaces
+
+open import real-numbers.field-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+Given a family of [real vector spaces](linear-algebra.real-vector-spaces.md)
+`Vᵢ` indexed by `i : I`, the dependent product `Πᵢ Vᵢ` is a real vector space.
+
+## Definition
+
+```agda
+Π-ℝ-Vector-Space :
+  {l1 l2 l3 : Level} (I : UU l1) (V : I → ℝ-Vector-Space l2 l3) →
+  ℝ-Vector-Space l2 (l1 ⊔ l3)
+Π-ℝ-Vector-Space {l2 = l2} =
+  Π-Vector-Space (heyting-field-ℝ l2)
+```

src/linear-algebra/dependent-products-vector-spaces.lagda.md

@@ -0,0 +1,38 @@
+# Dependent products of vector spaces
+
+```agda
+module linear-algebra.dependent-products-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.heyting-fields
+
+open import foundation.universe-levels
+
+open import linear-algebra.dependent-products-left-modules-rings
+open import linear-algebra.vector-spaces
+```
+
+</details>
+
+## Idea
+
+Given a [Heyting field](commutative-algebra.heyting-fields.md) `K` and a family
+of [vector spaces](linear-algebra.vector-spaces.md) `Vᵢ` over `K` indexed by
+`i : I`, the dependent product `Πᵢ Vᵢ` is a vector space over `K`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (K : Heyting-Field l1)
+  (I : UU l2)
+  (V : I → Vector-Space l3 K)
+  where
+
+  Π-Vector-Space : Vector-Space (l2 ⊔ l3) K
+  Π-Vector-Space = Π-left-module-Ring (ring-Heyting-Field K) I V
+```

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

@@ -0,0 +1,49 @@
+# Function left modules on rings
+
+```agda
+module linear-algebra.function-left-modules-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import linear-algebra.dependent-products-left-modules-rings
+open import linear-algebra.left-modules-rings
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+Given a type `X` and a [left module](linear-algebra.left-modules-rings.md) `M`
+over a [ring](ring-theory.rings.md) `R`, the functions `X → M` form a left
+module over `R`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (X : UU l3)
+  where
+
+  function-left-module-Ring : left-module-Ring (l2 ⊔ l3) R
+  function-left-module-Ring = Π-left-module-Ring R X (λ _ → M)
+```
+
+## Properties
+
+### The functions `X → R` form a left module over `R`
+
+```agda
+function-left-module-ring-Ring :
+  {l1 l2 : Level} (R : Ring l1) → UU l2 → left-module-Ring (l1 ⊔ l2) R
+function-left-module-ring-Ring R =
+  function-left-module-Ring R (left-module-ring-Ring R)
+```

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

@@ -0,0 +1,43 @@
+# Function real vector spaces
+
+```agda
+module linear-algebra.function-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import linear-algebra.function-vector-spaces
+open import linear-algebra.real-vector-spaces
+
+open import real-numbers.field-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+Given a type `X` and a [real vector space](linear-algebra.real-vector-spaces.md)
+`V`, the functions `X → V` form a real vector space.
+
+## Definition
+
+```agda
+function-ℝ-Vector-Space :
+  {l1 l2 l3 : Level} (V : ℝ-Vector-Space l1 l2) → UU l3 →
+  ℝ-Vector-Space l1 (l2 ⊔ l3)
+function-ℝ-Vector-Space {l1 = l1} = function-Vector-Space (heyting-field-ℝ l1)
+```
+
+## Properties
+
+### The functions `X → ℝ` form a real vector space
+
+```agda
+vector-space-function-ℝ :
+  {l1 : Level} (l2 : Level) → UU l1 → ℝ-Vector-Space l2 (l1 ⊔ lsuc l2)
+vector-space-function-ℝ l2 =
+  function-vector-space-Heyting-Field (heyting-field-ℝ l2)
+```

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

@@ -0,0 +1,49 @@
+# Function vector spaces
+
+```agda
+module linear-algebra.function-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.heyting-fields
+
+open import foundation.universe-levels
+
+open import linear-algebra.function-left-modules-rings
+open import linear-algebra.vector-spaces
+```
+
+</details>
+
+## Idea
+
+Given a type `X` and a [vector space](linear-algebra.vector-spaces.md) `V` over
+a [Heyting field](commutative-algebra.heyting-fields.md) `K`, the functions
+`X → V` form a vector space over `K`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (K : Heyting-Field l1)
+  (V : Vector-Space l2 K)
+  (X : UU l3)
+  where
+
+  function-Vector-Space : Vector-Space (l2 ⊔ l3) K
+  function-Vector-Space = function-left-module-Ring (ring-Heyting-Field K) V X
+```
+
+## Properties
+
+### The functions `X → K` form a vector space over `K`
+
+```agda
+function-vector-space-Heyting-Field :
+  {l1 l2 : Level} (K : Heyting-Field l1) → UU l2 → Vector-Space (l1 ⊔ l2) K
+function-vector-space-Heyting-Field K =
+  function-left-module-ring-Ring (ring-Heyting-Field K)
+```