The precategory of left modules over commutative rings

Content created by Louis Wasserman.

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

module linear-algebra.precategory-of-left-modules-commutative-rings where
Imports 
open import category-theory.large-precategories

open import commutative-algebra.commutative-rings

open import foundation.universe-levels

open import linear-algebra.left-modules-commutative-rings
open import linear-algebra.precategory-of-left-modules-rings

Idea

Left modules over a given commutative ring and linear maps between them form a large precategory.

Definition

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

  large-precategory-left-module-Commutative-Ring :
    Large-Precategory (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  large-precategory-left-module-Commutative-Ring =
    large-precategory-left-module-Ring (ring-Commutative-Ring R)

Recent changes