The precategory of vector spaces

Content created by Louis Wasserman.

Created on 2026-03-22.
Last modified on 2026-03-22.

module linear-algebra.precategory-of-vector-spaces where
Imports 
open import category-theory.large-precategories

open import commutative-algebra.heyting-fields

open import foundation.universe-levels

open import linear-algebra.precategory-of-left-modules-rings
open import linear-algebra.vector-spaces

Idea

Vector spaces over a given Heyting field and linear maps form a large precategory.

Definition

module _
  {l1 : Level}
  (K : Heyting-Field l1)
  where

  large-precategory-Vector-Space :
    Large-Precategory (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  large-precategory-Vector-Space =
    large-precategory-left-module-Ring (ring-Heyting-Field K)

Recent changes