Linear forms in left modules over commutative rings

Content created by Louis Wasserman.

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

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

open import foundation.universe-levels

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

Idea

A linear form in a left module M over a commutative ring R is a linear map from M to R.

Definition

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

  linear-form-left-module-Commutative-Ring : UU (l1 ⊔ l2)
  linear-form-left-module-Commutative-Ring =
    linear-map-left-module-Commutative-Ring R
      ( M)
      ( left-module-commutative-ring-Commutative-Ring R)

  map-linear-form-left-module-Commutative-Ring :
    linear-form-left-module-Commutative-Ring →
    type-left-module-Commutative-Ring R M →
    type-Commutative-Ring R
  map-linear-form-left-module-Commutative-Ring =
    map-linear-map-left-module-Commutative-Ring R
      ( M)
      ( left-module-commutative-ring-Commutative-Ring R)

See also

Recent changes