The difference of linear maps between left modules over rings

Content created by Louis Wasserman.

Created on 2026-02-24.
Last modified on 2026-02-24.

module linear-algebra.difference-linear-maps-left-modules-rings where
Imports 
open import foundation.universe-levels

open import group-theory.abelian-groups

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

open import ring-theory.rings

Idea

The difference of two linear maps f and g between two left modules over a ring is the linear map x ↦ (f x - g x).

Definition

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

  diff-linear-map-left-module-Ring :
    linear-map-left-module-Ring R M N →
    linear-map-left-module-Ring R M N →
    linear-map-left-module-Ring R M N
  diff-linear-map-left-module-Ring =
    right-subtraction-Ab (ab-add-linear-map-left-module-Ring R M N)

Recent changes