The left module of linear maps between left modules over commutative rings

Content created by Louis Wasserman.

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

module linear-algebra.left-module-linear-maps-left-modules-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.addition-linear-maps-left-modules-commutative-rings
open import linear-algebra.left-modules-commutative-rings
open import linear-algebra.linear-maps-left-modules-commutative-rings
open import linear-algebra.scalar-multiplication-linear-maps-left-modules-commutative-rings

Idea

The type of linear maps between two left modules over the same commutative ring R itself forms a left module over R.

Definition

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

  left-module-linear-map-left-module-Commutative-Ring :
    left-module-Commutative-Ring (l1 ⊔ l2 ⊔ l3) R
  left-module-linear-map-left-module-Commutative-Ring =
    make-left-module-Commutative-Ring
      ( R)
      ( ab-add-linear-map-left-module-Commutative-Ring R M N)
      ( mul-linear-map-left-module-Commutative-Ring R M N)
      ( left-distributive-mul-add-linear-map-left-module-Commutative-Ring R M N)
      ( right-distributive-mul-add-linear-map-left-module-Commutative-Ring
        ( R)
        ( M)
        ( N))
      ( left-unit-law-mul-linear-map-left-module-Commutative-Ring R M N)
      ( associative-mul-linear-map-left-module-Commutative-Ring R M N)

Properties

Evaluation of a linear map is a linear map

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

  is-linear-ev-linear-map-left-module-Commutative-Ring :
    is-linear-map-left-module-Commutative-Ring
      ( R)
      ( left-module-linear-map-left-module-Commutative-Ring R M N)
      ( N)
      ( ev-linear-map-left-module-Commutative-Ring R M N x)
  is-linear-ev-linear-map-left-module-Commutative-Ring =
    ( ( λ _ _ → refl) ,
      ( λ _ _ → refl))

  linear-map-ev-linear-map-left-module-Commutative-Ring :
    linear-map-left-module-Commutative-Ring
      ( R)
      ( left-module-linear-map-left-module-Commutative-Ring R M N)
      ( N)
  linear-map-ev-linear-map-left-module-Commutative-Ring =
    ( ev-linear-map-left-module-Commutative-Ring R M N x ,
      is-linear-ev-linear-map-left-module-Commutative-Ring)

See also

Recent changes