Dependent products of vector spaces

Content created by Louis Wasserman.

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

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

Idea

Given a Heyting field K and a family of vector spaces Vᵢ over K indexed by i : I, the dependent product Πᵢ Vᵢ is a vector space over K.

Definition

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

Recent changes