Subspaces of vector spaces

Content created by Louis Wasserman.

Created on 2026-01-30.
Last modified on 2026-01-30.

module linear-algebra.subspaces-vector-spaces where
Imports 
open import commutative-algebra.heyting-fields

open import foundation.subtypes
open import foundation.universe-levels

open import linear-algebra.left-submodules-rings
open import linear-algebra.vector-spaces

Idea

A subspace of a vector space V over a Heyting field F is a submodule of V as a left module over the underlying ring of F.

Definition

subspace-Vector-Space :
  (l1 : Level) {l2 l3 : Level} (F : Heyting-Field l2) → Vector-Space l3 F →
  UU (lsuc l1 ⊔ l2 ⊔ l3)
subspace-Vector-Space l F = left-submodule-Ring l (ring-Heyting-Field F)

module _
  {l1 l2 l3 : Level}
  (F : Heyting-Field l1)
  (V : Vector-Space l2 F)
  (S : subspace-Vector-Space l3 F V)
  where

  subset-subspace-Vector-Space : subtype l3 (type-Vector-Space F V)
  subset-subspace-Vector-Space =
    subset-left-submodule-Ring (ring-Heyting-Field F) V S

  type-subspace-Vector-Space : UU (l2 ⊔ l3)
  type-subspace-Vector-Space = type-subtype subset-subspace-Vector-Space

  vector-space-subspace-Vector-Space : Vector-Space (l2 ⊔ l3) F
  vector-space-subspace-Vector-Space =
    left-module-left-submodule-Ring (ring-Heyting-Field F) V S

Recent changes