harness_algebra/modules/
mod.rs

1// TODO: Redo these docs.
2
3//! Module theory abstractions and implementations.
4//!
5//! This module provides traits and implementations for module theory concepts,
6//! which generalize vector spaces by allowing the scalars to lie in a ring rather than a field.
7//!
8//! Semimodule abstractions and implementations.
9//!
10//! A semimodule is a generalization of vector spaces and modules where the scalars form a semiring
11//! rather than a ring or field. Like modules, semimodules support scalar multiplication and
12//! addition, but the scalars only need to form a semiring structure.
13//!
14//! # Key Concepts
15//!
16//! - **Semimodule**: A set with an additive structure and scalar multiplication by elements of a
17//!   semiring
18//! - **Semiring**: A ring-like structure but without the requirement of additive inverses
19//! - **Scalar Multiplication**: Compatible multiplication between semiring elements and semimodule
20//!   elements
21//!
22//! # Examples
23//!
24//! The tropical algebra (implemented in the `tropical` module) is a classic example of a
25//! semimodule, where addition is replaced by maximum and multiplication by regular addition.
26//!
27//! # Module Structure
28//!
29//! - [`trivial`]: Trivial semimodule
30//! - [`tropical`]: Semimodule over the tropical semiring
31
32use core::marker::PhantomData;
33
34use super::*;
35use crate::{
36  groups::{AbelianGroup, Group},
37  rings::{Field, Ring, Semiring},
38};
39
40pub mod trivial;
41pub mod tropical;
42
43/// A left semimodule over a semiring.
44///
45/// A set with commutative addition and left scalar multiplication satisfying:
46/// - Distributivity: s * (x + y) = s * x + s * y
47/// - Compatibility: (s + t) * x = s * x + t * x
48/// - Associativity: (s * t) * x = s * (t * x)
49/// - Identity: 1 * x = x
50/// - Zero: 0 * x = 0
51pub trait LeftSemimodule
52where Self: Mul<Self::Semiring> {
53  /// The Semiring that this semimodule is defined over.
54  type Semiring: Semiring;
55}
56
57/// A right semimodule over a semiring.
58///
59/// A set with commutative addition and right scalar multiplication satisfying:
60/// - Distributivity: (x + y) * s = x * s + y * s
61/// - Compatibility: x * (s + t) = x * s + x * t
62/// - Associativity: x * (s * t) = (x * s) * t
63/// - Identity: x * 1 = x
64/// - Zero: x * 0 = 0
65pub trait RightSemimodule
66where Self: Mul<Self::Semiring> {
67  /// The Semiring that this semimodule is defined over.
68  type Semiring: Semiring;
69}
70
71/// A two-sided semimodule over a semiring.
72///
73/// - **Semimodule**: A vector space generalization where scalars are elements of a semiring
74/// - **Left/Right Semimodule**: Defines scalar multiplication from left/right respectively
75/// - **Two-Sided Semimodule**: Both left and right semimodule over the same semiring
76///
77/// Combines left and right semimodule properties over the same semiring.
78/// Note: For commutative semirings, left and right actions typically coincide.
79pub trait TwoSidedSemimodule: LeftSemimodule + RightSemimodule {
80  /// The semiring over which this semimodule is defined.
81  type Semiring: Semiring;
82}
83
84/// A trait representing a left module over a ring.
85///
86/// A left module is a generalization of a vector space, where the scalars lie in a ring
87/// rather than a field. This trait combines the requirements for an Abelian group
88/// with scalar multiplication by elements of the ring on the left.
89pub trait LeftModule: AbelianGroup
90where Self::Ring: Mul<Self> {
91  /// The ring over which this module is defined.
92  type Ring: Ring;
93}
94
95/// A trait representing a right module over a ring.
96///
97/// A right module is a generalization of a vector space, where the scalars lie in a ring
98/// rather than a field. This trait combines the requirements for an Abelian group
99/// with scalar multiplication by elements of the ring on the right.
100pub trait RightModule: AbelianGroup
101where Self::Ring: Mul<Self> {
102  /// The ring over which this module is defined.
103  type Ring: Ring;
104}
105
106/// A trait representing a two-sided module over a ring.
107///
108/// A two-sided module is a generalization of a vector space, where the scalars lie in a ring
109/// rather than a field. This trait combines the requirements for an Abelian group
110/// with scalar multiplication by elements of the ring on both the left and right.
111pub trait TwoSidedModule: LeftModule + RightModule {
112  /// The ring over which this module is defined.
113  type Ring: Ring;
114}
115
116/// A trait representing a vector space over a field.
117///
118/// A vector space is a module over a field, meaning it has both addition and
119/// scalar multiplication operations, with the scalars coming from a field.
120pub trait VectorSpace: TwoSidedModule
121where <Self as TwoSidedModule>::Ring: Field {
122}
harness_algebra/modules/mod.rs

harness_algebra/modules/
mod.rs
