make pre-commit

Author: lowasser

src/linear-algebra/scalar-multiplication-vectors-on-rings.lagda.md

@@ -20,8 +20,9 @@ open import group-theory.homomorphisms-abelian-groups
 open import linear-algebra.vectors
 open import linear-algebra.vectors-on-rings
 
+open import module-theory.left-modules-rings
+
 open import ring-theory.homomorphisms-rings
-open import ring-theory.left-modules-rings
 open import ring-theory.rings
 ```
 

src/module-theory.lagda.md

@@ -0,0 +1,9 @@
+# Module theory
+
+```agda
+module module-theory where
+
+open import module-theory.left-modules-rings public
+open import module-theory.linear-maps-left-modules-rings public
+open import module-theory.right-modules-rings public
+```

src/ring-theory/left-modules-rings.lagda.md renamed to src/module-theory/left-modules-rings.lagda.md

@@ -1,7 +1,7 @@
 # Left modules over rings
 
 ```agda
-module ring-theory.left-modules-rings where
+module module-theory.left-modules-rings where
 ```
 
 <details><summary>Imports</summary>
@@ -28,8 +28,11 @@ open import ring-theory.rings
 
 ## Idea
 
-A (left) module `M` over a ring `R` consists of an abelian group `M` equipped
-with an action `R → M → M` such
+A
+{{#concept "left module" WD="left module" WDID="Q120721996" Agda=left-module-Ring}}
+`M` over a [ring](ring-theory.rings.md) `R` consists of an
+[abelian group](group-theory.abelian-groups.md) `M` equipped with an action
+`R → M → M` such that
 
 ```text
   r(x+y) = rx + ry
@@ -42,10 +45,8 @@ with an action `R → M → M` such
       1x = x
 ```
 
-In other words, a left module `M` over a ring `R` consists of an abelian group
-`M` equipped with a ring homomorphism `R → endomorphism-ring-Ab M`. A right
-module over `R` consists of an abelian group `M` equipped with a ring
-homomorphism `R → opposite-Ring (endomorphism-ring-Ab M)`.
+Equivalently, a left module `M` over a ring `R` consists of an abelian group `M`
+equipped with a ring homomorphism `R → endomorphism-ring-Ab M`.
 
 ## Definitions
 

src/ring-theory/linear-maps-left-modules-rings.lagda.md renamed to src/module-theory/linear-maps-left-modules-rings.lagda.md

@@ -1,7 +1,7 @@
 # Linear maps between modules over rings
 
 ```agda
-module ring-theory.linear-maps-left-modules-rings where
+module module-theory.linear-maps-left-modules-rings where
 ```
 
 <details><summary>Imports</summary>
@@ -18,7 +18,8 @@ open import foundation.universe-levels
 
 open import group-theory.abelian-groups
 
-open import ring-theory.left-modules-rings
+open import module-theory.left-modules-rings
+
 open import ring-theory.rings
 ```
 
@@ -27,9 +28,9 @@ open import ring-theory.rings
 ## Idea
 
 A
-{{#concept "linear map" Agda=is-linear-map-left-module-Ring Disambiguation="over modules" WD="linear map" WDID=Q207643 }}
-between [left modules](ring-theory.left-modules-rings.md) is a map `f` with the
-following properties:
+{{#concept "linear map" Agda=is-linear-map-left-module-Ring Disambiguation="over left modules" WD="linear map" WDID=Q207643 }}
+between [left modules](module-theory.left-modules-rings.md) is a map `f` with
+the following properties:
 
 - Additivity: `f (a + b) = f a + f b`
 - Homogeneity: `f (c * a) = c * f a`

src/ring-theory/right-modules-rings.lagda.md renamed to src/module-theory/right-modules-rings.lagda.md

@@ -1,7 +1,7 @@
 # Right modules over rings
 
 ```agda
-module ring-theory.right-modules-rings where
+module module-theory.right-modules-rings where
 ```
 
 <details><summary>Imports</summary>
@@ -28,7 +28,9 @@ open import ring-theory.rings
 
 ## Idea
 
-A right module over a [ring](ring-theory.rings.md) `R` consists of an
+A
+{{#concept "right module" WD="right module" WDID=Q120722061 Agda=right-module-Ring}}
+over a [ring](ring-theory.rings.md) `R` consists of an
 [abelian group](group-theory.abelian-groups.md) `M` equipped with a
 [ring homomorphism](ring-theory.homomorphisms-rings.md) from `R` to the
 [opposite ring](ring-theory.opposite-rings.md) of the

src/ring-theory.lagda.md

@@ -47,8 +47,6 @@ open import ring-theory.joins-right-ideals-rings public
 open import ring-theory.kernels-of-ring-homomorphisms public
 open import ring-theory.left-ideals-generated-by-subsets-rings public
 open import ring-theory.left-ideals-rings public
-open import ring-theory.left-modules-rings public
-open import ring-theory.linear-maps-left-modules-rings public
 open import ring-theory.local-rings public
 open import ring-theory.localizations-rings public
 open import ring-theory.maximal-ideals-rings public
@@ -75,7 +73,6 @@ open import ring-theory.quotient-rings public
 open import ring-theory.radical-ideals-rings public
 open import ring-theory.right-ideals-generated-by-subsets-rings public
 open import ring-theory.right-ideals-rings public
-open import ring-theory.right-modules-rings public
 open import ring-theory.rings public
 open import ring-theory.semirings public
 open import ring-theory.subsets-rings public

src/ring-theory/algebras-rings.lagda.md

@@ -12,7 +12,8 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
-open import ring-theory.left-modules-rings
+open import module-theory.left-modules-rings
+
 open import ring-theory.rings
 ```