Function vector spaces

Content created by Louis Wasserman.

Created on 2026-04-26.
Last modified on 2026-04-26.

module linear-algebra.function-vector-spaces where
Imports 
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

Idea

Given a type X and a vector space V over a Heyting field K, the functions X → V form a vector space over K.

Definition

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

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)

Recent changes