Linear maps on left modules over commutative rings

Content created by Louis Wasserman.

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

module linear-algebra.linear-maps-left-modules-commutative-rings where

open import commutative-algebra.commutative-rings

open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import linear-algebra.left-modules-commutative-rings
open import linear-algebra.linear-maps-left-modules-rings

Idea

A linear map^¶ from a left module M over a commutative ring R to another left module N over R is a map f with the following properties:

• Additivity: f (a + b) = f a + f b
• Homogeneity: f (c * a) = c * f a

Definition

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (f :
    type-left-module-Commutative-Ring R V →
    type-left-module-Commutative-Ring R W)
  where

  is-additive-map-prop-left-module-Commutative-Ring : Prop (l2 ⊔ l3)
  is-additive-map-prop-left-module-Commutative-Ring =
    is-additive-map-prop-left-module-Ring
      ( ring-Commutative-Ring R)
      ( V)
      ( W)
      ( f)

  is-additive-map-left-module-Commutative-Ring : UU (l2 ⊔ l3)
  is-additive-map-left-module-Commutative-Ring =
    type-Prop is-additive-map-prop-left-module-Commutative-Ring

  is-homogeneous-map-prop-left-module-Commutative-Ring : Prop (l1 ⊔ l2 ⊔ l3)
  is-homogeneous-map-prop-left-module-Commutative-Ring =
    is-homogeneous-map-prop-left-module-Ring
      ( ring-Commutative-Ring R)
      ( V)
      ( W)
      ( f)

  is-homogeneous-map-left-module-Commutative-Ring : UU (l1 ⊔ l2 ⊔ l3)
  is-homogeneous-map-left-module-Commutative-Ring =
    type-Prop is-homogeneous-map-prop-left-module-Commutative-Ring

  is-linear-map-prop-left-module-Commutative-Ring : Prop (l1 ⊔ l2 ⊔ l3)
  is-linear-map-prop-left-module-Commutative-Ring =
    is-linear-map-prop-left-module-Ring
      ( ring-Commutative-Ring R)
      ( V)
      ( W)
      ( f)

  is-linear-map-left-module-Commutative-Ring : UU (l1 ⊔ l2 ⊔ l3)
  is-linear-map-left-module-Commutative-Ring =
    type-Prop is-linear-map-prop-left-module-Commutative-Ring

linear-map-left-module-Commutative-Ring :
  {l1 l2 l3 : Level} (R : Commutative-Ring l1) →
  left-module-Commutative-Ring l2 R → left-module-Commutative-Ring l3 R →
  UU (l1 ⊔ l2 ⊔ l3)
linear-map-left-module-Commutative-Ring R V W =
  type-subtype (is-linear-map-prop-left-module-Commutative-Ring R V W)

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (f : linear-map-left-module-Commutative-Ring R V W)
  where

  map-linear-map-left-module-Commutative-Ring :
    type-left-module-Commutative-Ring R V →
    type-left-module-Commutative-Ring R W
  map-linear-map-left-module-Commutative-Ring = pr1 f

  is-linear-map-linear-map-left-module-Commutative-Ring :
    is-linear-map-left-module-Commutative-Ring R V W
      ( map-linear-map-left-module-Commutative-Ring)
  is-linear-map-linear-map-left-module-Commutative-Ring = pr2 f

  is-additive-map-linear-map-left-module-Commutative-Ring :
    is-additive-map-left-module-Commutative-Ring R V W
      ( map-linear-map-left-module-Commutative-Ring)
  is-additive-map-linear-map-left-module-Commutative-Ring =
    pr1 is-linear-map-linear-map-left-module-Commutative-Ring

  is-homogeneous-map-linear-map-left-module-Commutative-Ring :
    is-homogeneous-map-left-module-Commutative-Ring R V W
      ( map-linear-map-left-module-Commutative-Ring)
  is-homogeneous-map-linear-map-left-module-Commutative-Ring =
    pr2 is-linear-map-linear-map-left-module-Commutative-Ring

ev-linear-map-left-module-Commutative-Ring :
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (v : type-left-module-Commutative-Ring R V) →
  linear-map-left-module-Commutative-Ring R V W →
  type-left-module-Commutative-Ring R W
ev-linear-map-left-module-Commutative-Ring R V W v f =
  map-linear-map-left-module-Commutative-Ring R V W f v

Properties

A linear map maps zero to zero

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (f : linear-map-left-module-Commutative-Ring R V W)
  where

  abstract
    is-zero-map-zero-linear-map-left-module-Commutative-Ring :
      is-zero-left-module-Commutative-Ring R W
        ( map-linear-map-left-module-Commutative-Ring R V W f
          ( zero-left-module-Commutative-Ring R V))
    is-zero-map-zero-linear-map-left-module-Commutative-Ring =
      is-zero-map-zero-linear-map-left-module-Ring
        ( ring-Commutative-Ring R)
        ( V)
        ( W)
        ( f)

A linear map maps -v to the negation of the map of v

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (f : linear-map-left-module-Commutative-Ring R V W)
  where

  abstract
    map-neg-linear-map-left-module-Commutative-Ring :
      (v : type-left-module-Commutative-Ring R V) →
      map-linear-map-left-module-Commutative-Ring R V W f
        ( neg-left-module-Commutative-Ring R V v) ＝
      neg-left-module-Commutative-Ring R W
        ( map-linear-map-left-module-Commutative-Ring R V W f v)
    map-neg-linear-map-left-module-Commutative-Ring =
      map-neg-linear-map-left-module-Ring
        ( ring-Commutative-Ring R)
        ( V)
        ( W)
        ( f)

The composition of linear maps is linear

module _
  {l1 l2 l3 l4 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (X : left-module-Commutative-Ring l4 R)
  (g :
    type-left-module-Commutative-Ring R W →
    type-left-module-Commutative-Ring R X)
  (f :
    type-left-module-Commutative-Ring R V →
    type-left-module-Commutative-Ring R W)
  where

  abstract
    is-linear-map-comp-left-module-Commutative-Ring :
      is-linear-map-left-module-Commutative-Ring R W X g →
      is-linear-map-left-module-Commutative-Ring R V W f →
      is-linear-map-left-module-Commutative-Ring R V X (g ∘ f)
    is-linear-map-comp-left-module-Commutative-Ring =
      is-linear-map-comp-left-module-Ring
        ( ring-Commutative-Ring R)
        ( V)
        ( W)
        ( X)
        ( g)
        ( f)

The linear composition of linear maps between left modules

module _
  {l1 l2 l3 l4 : Level}
  (R : Commutative-Ring l1)
  (V : left-module-Commutative-Ring l2 R)
  (W : left-module-Commutative-Ring l3 R)
  (X : left-module-Commutative-Ring l4 R)
  (g : linear-map-left-module-Commutative-Ring R W X)
  (f : linear-map-left-module-Commutative-Ring R V W)
  where

  comp-linear-map-left-module-Commutative-Ring :
    linear-map-left-module-Commutative-Ring R V X
  comp-linear-map-left-module-Commutative-Ring =
    comp-linear-map-left-module-Ring
      ( ring-Commutative-Ring R)
      ( V)
      ( W)
      ( X)
      ( g)
      ( f)

The identity linear map

module _
  {l1 l2 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  where

  id-linear-map-left-module-Commutative-Ring :
    linear-map-left-module-Commutative-Ring R M M
  id-linear-map-left-module-Commutative-Ring =
    id-linear-map-left-module-Ring (ring-Commutative-Ring R) M

If two linear maps are homotopic, they are equal

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (N : left-module-Commutative-Ring l3 R)
  where

  htpy-linear-map-left-module-Commutative-Ring :
    Relation (l2 ⊔ l3) (linear-map-left-module-Commutative-Ring R M N)
  htpy-linear-map-left-module-Commutative-Ring =
    htpy-linear-map-left-module-Ring (ring-Commutative-Ring R) M N

  abstract
    eq-htpy-linear-map-left-module-Commutative-Ring :
      (f g : linear-map-left-module-Commutative-Ring R M N) →
      htpy-linear-map-left-module-Commutative-Ring f g →
      f ＝ g
    eq-htpy-linear-map-left-module-Commutative-Ring =
      eq-htpy-linear-map-left-module-Ring (ring-Commutative-Ring R) M N

Associativity of composition of linear maps

module _
  {l1 l2 l3 l4 l5 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (N : left-module-Commutative-Ring l3 R)
  (P : left-module-Commutative-Ring l4 R)
  (Q : left-module-Commutative-Ring l5 R)
  where

  abstract
    associative-comp-linear-map-left-module-Commutative-Ring :
      (f : linear-map-left-module-Commutative-Ring R P Q)
      (g : linear-map-left-module-Commutative-Ring R N P)
      (h : linear-map-left-module-Commutative-Ring R M N) →
      comp-linear-map-left-module-Commutative-Ring R M N Q
        ( comp-linear-map-left-module-Commutative-Ring R N P Q f g)
        ( h) ＝
      comp-linear-map-left-module-Commutative-Ring R M P Q
        ( f)
        ( comp-linear-map-left-module-Commutative-Ring R M N P g h)
    associative-comp-linear-map-left-module-Commutative-Ring =
      associative-comp-linear-map-left-module-Ring
        ( ring-Commutative-Ring R)
        ( M)
        ( N)
        ( P)
        ( Q)

Unit laws of composition of linear maps

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (N : left-module-Commutative-Ring l3 R)
  where

  abstract
    left-unit-law-comp-linear-map-left-module-Commutative-Ring :
      (f : linear-map-left-module-Commutative-Ring R M N) →
      comp-linear-map-left-module-Commutative-Ring R M N N
        ( id-linear-map-left-module-Commutative-Ring R N)
        ( f) ＝
      f
    left-unit-law-comp-linear-map-left-module-Commutative-Ring =
      left-unit-law-comp-linear-map-left-module-Ring
        ( ring-Commutative-Ring R)
        ( M)
        ( N)

    right-unit-law-comp-linear-map-left-module-Commutative-Ring :
      (f : linear-map-left-module-Commutative-Ring R M N) →
      comp-linear-map-left-module-Commutative-Ring R M M N
        ( f)
        ( id-linear-map-left-module-Commutative-Ring R M) ＝
      f
    right-unit-law-comp-linear-map-left-module-Commutative-Ring =
      right-unit-law-comp-linear-map-left-module-Ring
        ( ring-Commutative-Ring R)
        ( M)
        ( N)

See also

• Linear maps between left modules over rings
• Linear maps between vector spaces
• Scalar multiplication of linear maps between left modules over commutative rings
• The left module of linear maps between left modules over commutative rings

Recent changes

• 2026-03-22. Louis Wasserman. The large precategory of vector spaces (#1919).
• 2026-03-22. Louis Wasserman. Duals of left modules over commutative rings (#1907).
• 2026-01-30. Louis Wasserman. Linear algebra concepts (#1764).