Scalar multiplication of linear maps between vector spaces

Content created by Louis Wasserman.

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

module linear-algebra.scalar-multiplication-linear-maps-vector-spaces where
Imports 
open import commutative-algebra.heyting-fields

open import foundation.universe-levels

open import linear-algebra.linear-endomaps-vector-spaces
open import linear-algebra.linear-maps-vector-spaces
open import linear-algebra.scalar-multiplication-linear-maps-left-modules-commutative-rings
open import linear-algebra.vector-spaces

Idea

Given a linear map f from a vector space V to another vector space W and a constant c : R, the map x ↦ c * f x is a linear map.

Definition

The linear transformation of scalar multiplication

module _
  {l1 l2 : Level}
  (F : Heyting-Field l1)
  (V : Vector-Space l2 F)
  (c : type-Heyting-Field F)
  where

  is-linear-map-mul-Vector-Space :
    is-linear-endo-Vector-Space F V (mul-Vector-Space F V c)
  is-linear-map-mul-Vector-Space =
    is-linear-map-mul-left-module-Commutative-Ring
      ( commutative-ring-Heyting-Field F)
      ( V)
      ( c)

  linear-endo-mul-Vector-Space : linear-endo-Vector-Space F V
  linear-endo-mul-Vector-Space =
    linear-endo-mul-left-module-Commutative-Ring
      ( commutative-ring-Heyting-Field F)
      ( V)
      ( c)

Scalar multiplication of linear maps

module _
  {l1 l2 l3 : Level}
  (F : Heyting-Field l1)
  (V : Vector-Space l2 F)
  (W : Vector-Space l3 F)
  (c : type-Heyting-Field F)
  where

  mul-linear-map-Vector-Space :
    linear-map-Vector-Space F V W → linear-map-Vector-Space F V W
  mul-linear-map-Vector-Space =
    comp-linear-map-Vector-Space F V W W
      ( linear-endo-mul-Vector-Space F W c)

Recent changes