Linear maps between left modules over rings

Created on 2025-05-18.
Last modified on 2026-03-22.

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

open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.conjunction
open import foundation.constant-maps
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.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.homomorphisms-abelian-groups

open import linear-algebra.left-modules-rings

open import ring-theory.rings

Idea

A linear map^¶ between left modules 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 : Ring l1)
  (M : left-module-Ring l2 R) (N : left-module-Ring l3 R)
  (f : type-left-module-Ring R M → type-left-module-Ring R N)
  where

  is-additive-map-prop-left-module-Ring : Prop (l2 ⊔ l3)
  is-additive-map-prop-left-module-Ring =
    Π-Prop
      ( type-left-module-Ring R M)
      ( λ x →
        Π-Prop
          ( type-left-module-Ring R M)
          ( λ y →
            Id-Prop
              ( set-left-module-Ring R N)
              ( f (add-left-module-Ring R M x y))
              ( add-left-module-Ring R N (f x) (f y))))

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

  is-homogeneous-map-prop-left-module-Ring : Prop (l1 ⊔ l2 ⊔ l3)
  is-homogeneous-map-prop-left-module-Ring =
    Π-Prop
      ( type-Ring R)
      ( λ c →
        Π-Prop
          ( type-left-module-Ring R M)
          ( λ x →
            Id-Prop
              ( set-left-module-Ring R N)
              ( f (mul-left-module-Ring R M c x))
              ( mul-left-module-Ring R N c (f x))))

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

  is-linear-map-prop-left-module-Ring : Prop (l1 ⊔ l2 ⊔ l3)
  is-linear-map-prop-left-module-Ring =
    is-additive-map-prop-left-module-Ring ∧
    is-homogeneous-map-prop-left-module-Ring

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

  is-additive-is-linear-map-left-module-Ring :
    is-linear-map-left-module-Ring →
    (x y : type-left-module-Ring R M) →
    f (add-left-module-Ring R M x y) ＝
    add-left-module-Ring R N (f x) (f y)
  is-additive-is-linear-map-left-module-Ring = pr1

  is-homogeneous-is-linear-map-left-module-Ring :
    is-linear-map-left-module-Ring →
    (c : type-Ring R) (x : type-left-module-Ring R M) →
    f (mul-left-module-Ring R M c x) ＝
    mul-left-module-Ring R N c (f x)
  is-homogeneous-is-linear-map-left-module-Ring = pr2

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

  hom-set-left-module-Ring : Set (l1 ⊔ l2 ⊔ l3)
  hom-set-left-module-Ring =
    set-subset
      ( hom-set-Set (set-left-module-Ring R M) (set-left-module-Ring R N))
      ( is-linear-map-prop-left-module-Ring R M N)

  linear-map-left-module-Ring : UU (l1 ⊔ l2 ⊔ l3)
  linear-map-left-module-Ring = type-Set hom-set-left-module-Ring

  map-linear-map-left-module-Ring :
    linear-map-left-module-Ring →
    type-left-module-Ring R M → type-left-module-Ring R N
  map-linear-map-left-module-Ring = pr1

  is-linear-map-linear-map-left-module-Ring :
    (f : linear-map-left-module-Ring) →
    is-linear-map-left-module-Ring R M N (map-linear-map-left-module-Ring f)
  is-linear-map-linear-map-left-module-Ring = pr2

  is-additive-map-linear-map-left-module-Ring :
    (f : linear-map-left-module-Ring) →
    is-additive-map-left-module-Ring R M N (map-linear-map-left-module-Ring f)
  is-additive-map-linear-map-left-module-Ring =
    is-additive-is-linear-map-left-module-Ring R M N _ ∘
    is-linear-map-linear-map-left-module-Ring

  is-homogeneous-map-linear-map-left-module-Ring :
    (f : linear-map-left-module-Ring) →
    is-homogeneous-map-left-module-Ring R M N
      ( map-linear-map-left-module-Ring f)
  is-homogeneous-map-linear-map-left-module-Ring =
    is-homogeneous-is-linear-map-left-module-Ring R M N _ ∘
    is-linear-map-linear-map-left-module-Ring

Properties

A linear map is an abelian group homomorphism on the abelian groups of the left modules

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

  hom-ab-linear-map-left-module-Ring :
    linear-map-left-module-Ring R M N →
    hom-Ab (ab-left-module-Ring R M) (ab-left-module-Ring R N)
  hom-ab-linear-map-left-module-Ring (f , H , _) = (f , H _ _)

A linear map maps zero to zero

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

  abstract
    is-zero-map-zero-linear-map-left-module-Ring :
      (f : linear-map-left-module-Ring R M N) →
      map-linear-map-left-module-Ring R M N f (zero-left-module-Ring R M) ＝
      zero-left-module-Ring R N
    is-zero-map-zero-linear-map-left-module-Ring f =
      preserves-zero-hom-Ab
        ( ab-left-module-Ring R M)
        ( ab-left-module-Ring R N)
        ( hom-ab-linear-map-left-module-Ring R M N f)

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

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

  abstract
    map-neg-linear-map-left-module-Ring :
      (f : linear-map-left-module-Ring R M N) →
      (x : type-left-module-Ring R M) →
      map-linear-map-left-module-Ring R M N f (neg-left-module-Ring R M x) ＝
      neg-left-module-Ring R N (map-linear-map-left-module-Ring R M N f x)
    map-neg-linear-map-left-module-Ring f _ =
      preserves-negatives-hom-Ab
        ( ab-left-module-Ring R M)
        ( ab-left-module-Ring R N)
        ( hom-ab-linear-map-left-module-Ring R M N f)

The composition of linear maps is linear

module _
  {lr l1 l2 l3 : Level} (R : Ring lr)
  (M : left-module-Ring l1 R)
  (N : left-module-Ring l2 R)
  (K : left-module-Ring l3 R)
  (g : type-left-module-Ring R N → type-left-module-Ring R K)
  (f : type-left-module-Ring R M → type-left-module-Ring R N)
  where

  abstract
    is-additive-map-comp-left-module-Ring :
      is-additive-map-left-module-Ring R N K g →
      is-additive-map-left-module-Ring R M N f →
      is-additive-map-left-module-Ring R M K (g ∘ f)
    is-additive-map-comp-left-module-Ring Hg Hf x y =
      ap g (Hf x y) ∙ Hg (f x) (f y)

    is-homogeneous-map-comp-left-module-Ring :
      is-homogeneous-map-left-module-Ring R N K g →
      is-homogeneous-map-left-module-Ring R M N f →
      is-homogeneous-map-left-module-Ring R M K (g ∘ f)
    is-homogeneous-map-comp-left-module-Ring Hg Hf c x =
      ap g (Hf c x) ∙ Hg c (f x)

    is-linear-map-comp-left-module-Ring :
      is-linear-map-left-module-Ring R N K g →
      is-linear-map-left-module-Ring R M N f →
      is-linear-map-left-module-Ring R M K (g ∘ f)
    is-linear-map-comp-left-module-Ring Hg Hf =
      ( is-additive-map-comp-left-module-Ring
        ( is-additive-is-linear-map-left-module-Ring R N K g Hg)
        ( is-additive-is-linear-map-left-module-Ring R M N f Hf)) ,
      ( is-homogeneous-map-comp-left-module-Ring
        ( is-homogeneous-is-linear-map-left-module-Ring R N K g Hg)
        ( is-homogeneous-is-linear-map-left-module-Ring R M N f Hf))

The linear composition of linear maps between left modules

module _
  {lr l1 l2 l3 : Level} (R : Ring lr)
  (M : left-module-Ring l1 R)
  (N : left-module-Ring l2 R)
  (K : left-module-Ring l3 R)
  (g : linear-map-left-module-Ring R N K)
  (f : linear-map-left-module-Ring R M N)
  where

  comp-linear-map-left-module-Ring : linear-map-left-module-Ring R M K
  comp-linear-map-left-module-Ring =
    ( map-linear-map-left-module-Ring R N K g ∘
      map-linear-map-left-module-Ring R M N f) ,
    ( is-linear-map-comp-left-module-Ring R M N K
      ( map-linear-map-left-module-Ring R N K g)
      ( map-linear-map-left-module-Ring R M N f)
      ( is-linear-map-linear-map-left-module-Ring R N K g)
      ( is-linear-map-linear-map-left-module-Ring R M N f))

The constant map to zero is a linear map

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

  abstract
    is-additive-const-zero-map-left-module-Ring :
      is-additive-map-left-module-Ring R M N
        ( const (type-left-module-Ring R M) (zero-left-module-Ring R N))
    is-additive-const-zero-map-left-module-Ring _ _ =
      inv (left-unit-law-add-left-module-Ring R N _)

    is-homogeneous-const-zero-map-left-module-Ring :
      is-homogeneous-map-left-module-Ring R M N
        ( const (type-left-module-Ring R M) (zero-left-module-Ring R N))
    is-homogeneous-const-zero-map-left-module-Ring _ _ =
      inv (right-zero-law-mul-left-module-Ring R N _)

  is-linear-const-zero-map-left-module-Ring :
    is-linear-map-left-module-Ring R M N
      ( const (type-left-module-Ring R M) (zero-left-module-Ring R N))
  is-linear-const-zero-map-left-module-Ring =
    ( is-additive-const-zero-map-left-module-Ring ,
      is-homogeneous-const-zero-map-left-module-Ring)

  const-zero-linear-map-left-module-Ring : linear-map-left-module-Ring R M N
  const-zero-linear-map-left-module-Ring =
    ( const (type-left-module-Ring R M) (zero-left-module-Ring R N) ,
      is-linear-const-zero-map-left-module-Ring)

If two linear maps are homotopic, they are equal

module _
  {l1 l2 l3 : Level}
  (R : Ring l1)
  (M : left-module-Ring l2 R)
  (N : left-module-Ring l3 R)
  (f g : linear-map-left-module-Ring R M N)
  where

  htpy-linear-map-left-module-Ring : UU (l2 ⊔ l3)
  htpy-linear-map-left-module-Ring =
    map-linear-map-left-module-Ring R M N f ~
    map-linear-map-left-module-Ring R M N g

  abstract
    eq-htpy-linear-map-left-module-Ring :
      htpy-linear-map-left-module-Ring → f ＝ g
    eq-htpy-linear-map-left-module-Ring f~g =
      eq-type-subtype
        ( is-linear-map-prop-left-module-Ring R M N)
        ( eq-htpy f~g)

The identity linear map from a left module to itself

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

  id-linear-map-left-module-Ring :
    linear-map-left-module-Ring R M M
  id-linear-map-left-module-Ring =
    ( id , (λ _ _ → refl) , (λ _ _ → refl))

Associativity of composition of linear maps

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

  abstract
    associative-comp-linear-map-left-module-Ring :
      (f : linear-map-left-module-Ring R P Q)
      (g : linear-map-left-module-Ring R N P)
      (h : linear-map-left-module-Ring R M N) →
      comp-linear-map-left-module-Ring R M N Q
        ( comp-linear-map-left-module-Ring R N P Q f g)
        ( h) ＝
      comp-linear-map-left-module-Ring R M P Q
        ( f)
        ( comp-linear-map-left-module-Ring R M N P g h)
    associative-comp-linear-map-left-module-Ring f g h =
      eq-htpy-linear-map-left-module-Ring R M Q _ _ refl-htpy

Unit laws of composition of linear maps

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

  abstract
    left-unit-law-comp-linear-map-left-module-Ring :
      (f : linear-map-left-module-Ring R M N) →
      comp-linear-map-left-module-Ring R M N N
        ( id-linear-map-left-module-Ring R N)
        ( f) ＝
      f
    left-unit-law-comp-linear-map-left-module-Ring f =
      eq-htpy-linear-map-left-module-Ring R M N _ _ refl-htpy

    right-unit-law-comp-linear-map-left-module-Ring :
      (f : linear-map-left-module-Ring R M N) →
      comp-linear-map-left-module-Ring R M M N
        ( f)
        ( id-linear-map-left-module-Ring R M) ＝
      f
    right-unit-law-comp-linear-map-left-module-Ring f =
      eq-htpy-linear-map-left-module-Ring R M N _ _ refl-htpy

See also

• Linear maps between left modules over commutative rings
• Linear maps between vector spaces
• Addition of linear maps on left modules
• Negation of linear maps on left modules

External links

• Linear map at Wikidata

Recent changes

• 2026-03-22. Louis Wasserman. The large precategory of vector spaces (#1919).
• 2026-01-30. Louis Wasserman. Linear algebra concepts (#1764).
• 2025-05-18. Louis Wasserman and malarbol. Linear maps over modules (#1395).