oxilean-std 0.1.2

//! Algebraic K-theory functions: computing K_0, K_1, K_2 for rings and fields.
//!
//! Implements:
//! - Grothendieck group K_0 construction
//! - Euler characteristic in K_0
//! - Steinberg relations for K_2
//! - Bass cancellation theorem
//! - Milnor symbol relations

use super::types::{
    ElementaryMatrix, K0Group, K1Group, K2Group, MatrixOverRing, MilnorK2Symbol, ProjectiveModule,
    StableIsomorphismClass, UnitGroup,
};

// ── K_0 computations ─────────────────────────────────────────────────────────

/// K_0 of a field k.
///
/// Every f.g. projective module over a field is free (since fields are local),
/// so K_0(k) ≅ Z generated by \[k\]. We represent Z as the single generator
/// class \[k\] of rank 1, with addition table reflecting Z-addition (rank sums).
pub fn k0_of_field() -> K0Group {
    // K_0(field) ≅ Z, generator = [k] = class of rank 1.
    // We represent finitely many classes: 0, [k], [k^2] = [k]+[k], ...
    // For a concrete finite representation, use classes of rank 0..=3.
    let classes = vec![
        StableIsomorphismClass::new(0, 0), // [0] = trivial class
        StableIsomorphismClass::new(1, 0), // [k] = generator
        StableIsomorphismClass::new(2, 0), // [k^2]
        StableIsomorphismClass::new(3, 0), // [k^3]
    ];
    // addition_table[i][j] = index of class of rank i + rank j
    // Saturate at rank 3 (clamp to last element) for finite representation.
    let n = classes.len();
    let addition_table = (0..n)
        .map(|i| {
            (0..n)
                .map(|j| {
                    let sum_rank = classes[i].rank + classes[j].rank;
                    // Find the class with this rank (id=0), or last one
                    classes
                        .iter()
                        .rposition(|c| c.rank == sum_rank)
                        .unwrap_or(n - 1)
                })
                .collect()
        })
        .collect();
    K0Group::new(classes, addition_table)
}

/// K_0 of the integers Z.
///
/// Every f.g. projective module over Z is free (since Z is a PID),
/// so K_0(Z) ≅ Z generated by \[Z\].
pub fn k0_of_integers() -> K0Group {
    // Identical structure to k0_of_field — Z is also a PID.
    k0_of_field()
}

/// Compute the Grothendieck group K_0(R) from a list of projective modules.
///
/// The Grothendieck group is the group completion of the monoid of isomorphism
/// classes under direct sum. We identify modules by their rank and assign
/// stable isomorphism classes accordingly.
pub fn grothendieck_group(modules: &[ProjectiveModule]) -> K0Group {
    if modules.is_empty() {
        // Empty collection: K_0 with just the zero class.
        return K0Group::new(vec![StableIsomorphismClass::new(0, 0)], vec![vec![0]]);
    }

    // Collect distinct (rank, ring) pairs to form stable classes.
    // Assign id=0 to each distinct rank (simplified: only one ring assumed).
    let mut seen_ranks: Vec<usize> = Vec::new();
    for m in modules {
        if !seen_ranks.contains(&m.rank) {
            seen_ranks.push(m.rank);
        }
    }
    seen_ranks.sort_unstable();

    // Also include rank 0 (zero module).
    if !seen_ranks.contains(&0) {
        seen_ranks.insert(0, 0);
    }

    let classes: Vec<StableIsomorphismClass> = seen_ranks
        .iter()
        .enumerate()
        .map(|(id, &rank)| StableIsomorphismClass::new(rank, id))
        .collect();

    let n = classes.len();
    let addition_table = build_addition_table(&classes, n);

    K0Group::new(classes, addition_table)
}

/// Build the addition table for a K_0 group from stable isomorphism classes.
///
/// [P_i] + [P_j] = \[P_i ⊕ P_j\], whose rank = rank(P_i) + rank(P_j).
/// If the sum rank exceeds any class rank, we saturate at the last class.
fn build_addition_table(classes: &[StableIsomorphismClass], n: usize) -> Vec<Vec<usize>> {
    (0..n)
        .map(|i| {
            (0..n)
                .map(|j| {
                    let sum_rank = classes[i].rank + classes[j].rank;
                    // Find a class with matching rank (prefer id=0), else last.
                    classes
                        .iter()
                        .position(|c| c.rank == sum_rank)
                        .unwrap_or(n - 1)
                })
                .collect()
        })
        .collect()
}

/// Compute the Euler characteristic χ in K_0.
///
/// For a chain complex  0 → P_n → P_{n-1} → … → P_0 → 0  of projective modules,
/// the Euler characteristic is:
///   χ = Σ (-1)^i · rank(P_i)
///
/// This is the alternating sum of ranks, which is well-defined in K_0(R).
pub fn euler_characteristic_k0(complex: &[ProjectiveModule]) -> i64 {
    complex
        .iter()
        .enumerate()
        .map(|(i, p)| {
            let sign: i64 = if i % 2 == 0 { 1 } else { -1 };
            sign * (p.rank as i64)
        })
        .sum()
}

// ── Elementary matrices and K_1 ───────────────────────────────────────────────

/// Generate the Steinberg relations for the elementary group E_n(R) ⊂ GL_n(R).
///
/// The Steinberg relations are:
/// 1. \[e_{ij}(λ), e_{kl}(μ)\] = 1 if j ≠ k and i ≠ l  (distant commutativity)
/// 2. \[e_{ij}(λ), e_{jk}(μ)\] = e_{ik}(λμ)              (Chevalley commutator)
///
/// Returns human-readable descriptions of the relations for n generators.
pub fn elementary_matrix_relations(n: usize) -> Vec<String> {
    let mut relations = Vec::new();

    for i in 0..n {
        for j in 0..n {
            if i == j {
                continue;
            }
            for k in 0..n {
                if k == j || k == i {
                    continue;
                }
                // Distant commutativity: [e_{ij}(λ), e_{kl}(μ)] = 1 when j≠k, i≠l.
                // Here j≠k is already guaranteed (k≠j above).
                if k != i {
                    relations.push(format!(
                        "[e_{{{i}{j}}}(λ), e_{{{k}{}}}(μ)] = 1  (distant commutativity)",
                        (k + 1) % n
                    ));
                }
                // Chevalley commutator: [e_{ij}(λ), e_{jk}(μ)] = e_{ik}(λμ).
                relations.push(format!(
                    "[e_{{{i}{j}}}(λ), e_{{{j}{k}}}(μ)] = e_{{{i}{k}}}(λμ)  (Chevalley)"
                ));
            }
        }
    }
    relations
}

/// Check whether a matrix over a ring is an elementary matrix.
///
/// A matrix M is elementary if it equals the identity except for exactly one
/// off-diagonal entry that is non-zero.
pub fn is_elementary_matrix(m: &MatrixOverRing) -> bool {
    let nr = m.num_rows();
    let nc = m.num_cols();
    if nr != nc || nr == 0 {
        return false;
    }
    let mut off_diag_count = 0usize;
    for i in 0..nr {
        for j in 0..nc {
            let val = m.entry(i, j).unwrap_or(0);
            if i == j {
                // Diagonal must be 1.
                if val != 1 {
                    return false;
                }
            } else if val != 0 {
                off_diag_count += 1;
                if off_diag_count > 1 {
                    return false;
                }
            }
        }
    }
    // Exactly one off-diagonal non-zero entry.
    off_diag_count == 1
}

/// Compute the commutator ABA⁻¹B⁻¹ of two invertible matrices in GL_n(R).
///
/// For integer matrices (entries in Z), computes the commutator \[A, B\].
/// This is used in computing K_1(R) = GL(R)/E(R) where E(R) = \[GL(R), GL(R)\].
///
/// **Limitation**: This implementation uses integer arithmetic and computes
/// inverses only for matrices with determinant ±1 (unimodular over Z).
pub fn commutator_in_gl(a: &MatrixOverRing, b: &MatrixOverRing) -> MatrixOverRing {
    let n = a.num_rows();
    if n == 0 || n != b.num_rows() || n != a.num_cols() || n != b.num_cols() {
        return MatrixOverRing::identity(n.max(1), &a.ring);
    }

    // Compute A*B, A⁻¹, B⁻¹, then A*B*A⁻¹*B⁻¹.
    let ab = matrix_multiply(a, b);
    let a_inv =
        matrix_inverse_unimodular(a).unwrap_or_else(|| MatrixOverRing::identity(n, &a.ring));
    let b_inv =
        matrix_inverse_unimodular(b).unwrap_or_else(|| MatrixOverRing::identity(n, &b.ring));
    let ab_a_inv = matrix_multiply(&ab, &a_inv);
    matrix_multiply(&ab_a_inv, &b_inv)
}

/// Multiply two matrices over Z (integer arithmetic).
fn matrix_multiply(a: &MatrixOverRing, b: &MatrixOverRing) -> MatrixOverRing {
    let n = a.num_rows();
    let m = b.num_cols();
    let k = a.num_cols();
    let mut result = vec![vec![0i64; m]; n];
    for i in 0..n {
        for j in 0..m {
            for l in 0..k {
                let aij = a.entry(i, l).unwrap_or(0);
                let bjl = b.entry(l, j).unwrap_or(0);
                result[i][j] = result[i][j].saturating_add(aij.saturating_mul(bjl));
            }
        }
    }
    MatrixOverRing::new(result, &a.ring)
}

/// Compute the inverse of a unimodular integer matrix (det = ±1) via adjugate.
///
/// Only implemented for 1×1, 2×2, and 3×3 to keep the code tractable.
/// Returns None if the matrix is not square, not unimodular, or too large.
fn matrix_inverse_unimodular(m: &MatrixOverRing) -> Option<MatrixOverRing> {
    let n = m.num_rows();
    if n != m.num_cols() {
        return None;
    }
    match n {
        1 => {
            let a = m.entry(0, 0)?;
            if a == 1 || a == -1 {
                Some(MatrixOverRing::new(vec![vec![a]], &m.ring))
            } else {
                None
            }
        }
        2 => {
            let a = m.entry(0, 0)?;
            let b = m.entry(0, 1)?;
            let c = m.entry(1, 0)?;
            let d = m.entry(1, 1)?;
            let det = a * d - b * c;
            if det != 1 && det != -1 {
                return None;
            }
            // inv = (1/det) * [[d, -b], [-c, a]]
            Some(MatrixOverRing::new(
                vec![vec![det * d, det * (-b)], vec![det * (-c), det * a]],
                &m.ring,
            ))
        }
        3 => {
            // Cofactor/adjugate method for 3×3.
            let get = |i: usize, j: usize| m.entry(i, j).unwrap_or(0);
            let det = get(0, 0) * (get(1, 1) * get(2, 2) - get(1, 2) * get(2, 1))
                - get(0, 1) * (get(1, 0) * get(2, 2) - get(1, 2) * get(2, 0))
                + get(0, 2) * (get(1, 0) * get(2, 1) - get(1, 1) * get(2, 0));
            if det != 1 && det != -1 {
                return None;
            }
            let adj = [
                [
                    get(1, 1) * get(2, 2) - get(1, 2) * get(2, 1),
                    -(get(0, 1) * get(2, 2) - get(0, 2) * get(2, 1)),
                    get(0, 1) * get(1, 2) - get(0, 2) * get(1, 1),
                ],
                [
                    -(get(1, 0) * get(2, 2) - get(1, 2) * get(2, 0)),
                    get(0, 0) * get(2, 2) - get(0, 2) * get(2, 0),
                    -(get(0, 0) * get(1, 2) - get(0, 2) * get(1, 0)),
                ],
                [
                    get(1, 0) * get(2, 1) - get(1, 1) * get(2, 0),
                    -(get(0, 0) * get(2, 1) - get(0, 1) * get(2, 0)),
                    get(0, 0) * get(1, 1) - get(0, 1) * get(1, 0),
                ],
            ];
            // inv = det * adj (since det = ±1)
            let rows: Vec<Vec<i64>> = adj
                .iter()
                .map(|row| row.iter().map(|&v| det * v).collect())
                .collect();
            Some(MatrixOverRing::new(rows, &m.ring))
        }
        _ => None,
    }
}

// ── K_2 and Milnor symbols ────────────────────────────────────────────────────

/// Check the Steinberg (Matsumoto) relation {a, 1-a} = 1 in K_2(F).
///
/// For any a ∈ F× with a ≠ 1, the symbol {a, 1-a} is trivial in K_2(F).
/// This is the fundamental relation defining K_2 (Matsumoto's theorem).
///
/// Returns true if the relation holds for the given string values a and b = 1-a.
/// The check is purely symbolic: returns true iff `a` and `b` represent
/// elements with a + b = 1 (i.e., b = "1" - a in the symbolic sense),
/// or when a = "0" or a = "1" (degenerate cases not in F×).
pub fn milnor_k2_symbol_relation(a: &str, b: &str) -> bool {
    // Degenerate: a = 0 or a = 1 means we are outside F×.
    if a == "0" || a == "1" {
        return true;
    }
    // Check symbolically: {a, 1-a} = 0 means b should equal "1-a" or "1 - a".
    // Also handle numeric cases: try to parse a, b as rationals.
    if let (Ok(af), Ok(bf)) = (a.parse::<f64>(), b.parse::<f64>()) {
        // Numerical check: b = 1 - a  AND  a ≠ 0, 1.
        let expected_b = 1.0 - af;
        return (bf - expected_b).abs() < 1e-10 && af.abs() > 1e-10 && (af - 1.0).abs() > 1e-10;
    }
    // Symbolic check: b is the string "1-a" or "(1-a)".
    let expected1 = format!("1-{a}");
    let expected2 = format!("1 - {a}");
    let expected3 = format!("(1-{a})");
    b == expected1 || b == expected2 || b == expected3
}

/// Bass cancellation theorem: checks whether P ⊕ Rⁿ ≅ Q ⊕ Rⁿ implies P ≅ Q.
///
/// Bass's theorem states: if R is a Noetherian ring of Krull dimension d,
/// and P is a projective module of rank > d, then P is cancellable
/// (stably free modules of rank > d are free).
///
/// Returns true if the module satisfies Bass's cancellation condition:
/// rank(P) > n (the Krull dimension bound).
pub fn bass_theorem_projective(module: &ProjectiveModule, n: usize) -> bool {
    // Bass cancellation: rank > n (Krull dimension of the base ring).
    module.rank > n
}

/// Build K_1(R) = R× for a commutative ring from its units.
///
/// For a commutative ring R, K_1(R) ≅ R× via the determinant map.
/// The `units` slice gives the generating units; we build the cyclic
/// multiplication table (treating the units as forming a group under multiplication).
pub fn k1_from_units(units: &[&str], _ring: &str) -> K1Group {
    let unit_names: Vec<String> = units.iter().map(|&s| s.to_string()).collect();
    let n = unit_names.len();
    // Build a cyclic multiplication table: units[i]*units[j] = units[(i+j) % n].
    // This models a cyclic unit group (e.g., (Z/pZ)×).
    let mult_table = (0..n)
        .map(|i| (0..n).map(|j| (i + j) % n).collect())
        .collect();
    let unit_group = UnitGroup::new(unit_names, mult_table);
    // No extra relations beyond commutativity (abelian group).
    K1Group::new(unit_group, vec![])
}

/// Format a K_0 group as a human-readable string.
pub fn format_k0(k0: &K0Group) -> String {
    use std::fmt::Write as FmtWrite;
    let mut s = String::new();
    let _ = writeln!(s, "K_0 group with {} classes:", k0.num_classes());
    for (i, cls) in k0.classes.iter().enumerate() {
        let _ = writeln!(s, "  [{i}] rank={}, id={}", cls.rank, cls.id);
    }
    s
}

// ── Formatting helpers ────────────────────────────────────────────────────────

/// Build a K_2 group for a field from a list of Steinberg symbols.
///
/// The group is presented by the given symbols subject to the standard relations:
/// 1. {a, b}{b, a} = 1  (anti-commutativity)
/// 2. {a, 1-a} = 1      (Steinberg relation)
/// 3. {ab, c} = {a, c}{b, c}  (bilinearity)
pub fn k2_from_symbols(symbols: Vec<MilnorK2Symbol>) -> K2Group {
    let mut relations = Vec::new();
    for sym in &symbols {
        // Steinberg relation: {a, 1-a} = 1.
        relations.push(format!("{{{}, 1-{}}} = 1", sym.a, sym.a));
        // Anti-symmetry: {a, b}{b, a} = 1.
        relations.push(format!("{{{0}, {1}}}{{{1}, {0}}} = 1", sym.a, sym.b));
        // Bilinearity (stated abstractly).
        relations.push(format!(
            "{{{}*x, {}}} = {{{0}, {1}}}{{x, {1}}} for all x in F×",
            sym.a, sym.b
        ));
    }
    // Deduplicate relations.
    relations.sort_unstable();
    relations.dedup();
    K2Group::new(symbols, relations)
}

// ── Tests ─────────────────────────────────────────────────────────────────────

#[cfg(test)]
mod tests {
    use super::*;

    // ── k0_of_field tests ─────────────────────────────────────────────────────

    #[test]
    fn test_k0_of_field_num_classes() {
        let k0 = k0_of_field();
        assert!(
            k0.num_classes() >= 2,
            "K_0(field) should have at least 2 classes"
        );
    }

    #[test]
    fn test_k0_of_field_generator_rank() {
        let k0 = k0_of_field();
        // The generator [k] should have rank 1.
        let has_rank_one = k0.classes.iter().any(|c| c.rank == 1);
        assert!(has_rank_one, "K_0(field) should have a class of rank 1");
    }

    #[test]
    fn test_k0_of_field_addition_table_square() {
        let k0 = k0_of_field();
        let n = k0.num_classes();
        assert_eq!(k0.addition_table.len(), n);
        for row in &k0.addition_table {
            assert_eq!(row.len(), n);
        }
    }

    #[test]
    fn test_k0_of_field_zero_element() {
        let k0 = k0_of_field();
        // Class 0 should have rank 0 (zero element).
        assert_eq!(k0.classes[0].rank, 0);
    }

    // ── k0_of_integers tests ──────────────────────────────────────────────────

    #[test]
    fn test_k0_of_integers_matches_field() {
        let k0z = k0_of_integers();
        let k0f = k0_of_field();
        // Both K_0(Z) ≅ K_0(field) ≅ Z.
        assert_eq!(k0z.num_classes(), k0f.num_classes());
    }

    // ── grothendieck_group tests ──────────────────────────────────────────────

    #[test]
    fn test_grothendieck_group_empty() {
        let k0 = grothendieck_group(&[]);
        assert_eq!(k0.num_classes(), 1, "Empty module list gives trivial K_0");
    }

    #[test]
    fn test_grothendieck_group_single_module() {
        let modules = vec![ProjectiveModule::free(2, "Z")];
        let k0 = grothendieck_group(&modules);
        // Should have classes for rank 0 and rank 2.
        assert!(k0.classes.iter().any(|c| c.rank == 2));
    }

    #[test]
    fn test_grothendieck_group_multiple_modules() {
        let modules = vec![
            ProjectiveModule::free(1, "Z"),
            ProjectiveModule::free(2, "Z"),
            ProjectiveModule::free(3, "Z"),
        ];
        let k0 = grothendieck_group(&modules);
        // Distinct ranks: 0, 1, 2, 3.
        assert!(k0.classes.len() >= 3);
    }

    #[test]
    fn test_grothendieck_group_addition_table_valid() {
        let modules = vec![
            ProjectiveModule::free(1, "Z"),
            ProjectiveModule::free(2, "Z"),
        ];
        let k0 = grothendieck_group(&modules);
        let n = k0.num_classes();
        for row in &k0.addition_table {
            assert_eq!(row.len(), n);
            for &v in row {
                assert!(v < n, "Addition table index out of range");
            }
        }
    }

    // ── euler_characteristic_k0 tests ─────────────────────────────────────────

    #[test]
    fn test_euler_characteristic_empty() {
        let chi = euler_characteristic_k0(&[]);
        assert_eq!(chi, 0);
    }

    #[test]
    fn test_euler_characteristic_single() {
        let complex = vec![ProjectiveModule::free(3, "Z")];
        assert_eq!(euler_characteristic_k0(&complex), 3);
    }

    #[test]
    fn test_euler_characteristic_two_term() {
        // 0 → Z^3 → Z^2 → 0 : χ = 3 - 2 = 1
        let complex = vec![
            ProjectiveModule::free(3, "Z"),
            ProjectiveModule::free(2, "Z"),
        ];
        assert_eq!(euler_characteristic_k0(&complex), 1);
    }

    #[test]
    fn test_euler_characteristic_three_term() {
        // 0 → Z^4 → Z^6 → Z^3 → 0 : χ = 4 - 6 + 3 = 1
        let complex = vec![
            ProjectiveModule::free(4, "Z"),
            ProjectiveModule::free(6, "Z"),
            ProjectiveModule::free(3, "Z"),
        ];
        assert_eq!(euler_characteristic_k0(&complex), 1);
    }

    // ── elementary_matrix_relations tests ────────────────────────────────────

    #[test]
    fn test_elementary_matrix_relations_n2() {
        // For n=2 there are only 2 elementary matrices e_{01} and e_{10}.
        // No Chevalley or distant commutativity relations exist (no third index).
        // The function documents n≥3 for non-trivial relations.
        let rels = elementary_matrix_relations(2);
        // Result may be empty — just check it doesn't panic.
        let _ = rels;
    }

    #[test]
    fn test_elementary_matrix_relations_n3() {
        let rels = elementary_matrix_relations(3);
        // Should include both distant commutativity and Chevalley relations.
        let has_chevalley = rels.iter().any(|r| r.contains("Chevalley"));
        assert!(has_chevalley);
    }

    #[test]
    fn test_elementary_matrix_relations_n1() {
        // n=1: no off-diagonal positions.
        let rels = elementary_matrix_relations(1);
        assert_eq!(rels.len(), 0, "n=1 has no elementary matrix relations");
    }

    // ── is_elementary_matrix tests ────────────────────────────────────────────

    #[test]
    fn test_is_elementary_matrix_identity_not_elementary() {
        let id = MatrixOverRing::identity(3, "Z");
        // Identity has zero off-diagonal non-zero entries, so NOT elementary.
        assert!(!is_elementary_matrix(&id));
    }

    #[test]
    fn test_is_elementary_matrix_valid() {
        let e = ElementaryMatrix::new(3, 0, 1, 5);
        let m = e.to_matrix("Z");
        assert!(is_elementary_matrix(&m));
    }

    #[test]
    fn test_is_elementary_matrix_two_off_diag_not_elementary() {
        // Two off-diagonal entries: not elementary.
        let rows = vec![vec![1i64, 3, 0], vec![0, 1, 7], vec![0, 0, 1]];
        let m = MatrixOverRing::new(rows, "Z");
        assert!(!is_elementary_matrix(&m));
    }

    #[test]
    fn test_is_elementary_matrix_wrong_diagonal() {
        // Diagonal not all 1: not elementary.
        let rows = vec![vec![2i64, 1], vec![0, 1]];
        let m = MatrixOverRing::new(rows, "Z");
        assert!(!is_elementary_matrix(&m));
    }

    // ── commutator_in_gl tests ────────────────────────────────────────────────

    #[test]
    fn test_commutator_identity_matrices() {
        // [I, I] = I.
        let a = MatrixOverRing::identity(2, "Z");
        let b = MatrixOverRing::identity(2, "Z");
        let comm = commutator_in_gl(&a, &b);
        let id = MatrixOverRing::identity(2, "Z");
        assert_eq!(comm, id);
    }

    #[test]
    fn test_commutator_elementary_matrices() {
        // e_{01}(1) and e_{10}(1) are elementary; their commutator is computable.
        let a_rows = vec![vec![1i64, 1], vec![0, 1]];
        let b_rows = vec![vec![1i64, 0], vec![1, 1]];
        let a = MatrixOverRing::new(a_rows, "Z");
        let b = MatrixOverRing::new(b_rows, "Z");
        let comm = commutator_in_gl(&a, &b);
        assert_eq!(comm.num_rows(), 2);
    }

    // ── milnor_k2_symbol_relation tests ──────────────────────────────────────

    #[test]
    fn test_milnor_k2_trivial_a_zero() {
        assert!(milnor_k2_symbol_relation("0", "1"));
    }

    #[test]
    fn test_milnor_k2_trivial_a_one() {
        assert!(milnor_k2_symbol_relation("1", "0"));
    }

    #[test]
    fn test_milnor_k2_numeric_relation() {
        // {2, -1} ≠ {2, 1-2} = {2, -1}. Indeed 1-2 = -1.
        assert!(milnor_k2_symbol_relation("2", "-1"));
    }

    #[test]
    fn test_milnor_k2_symbolic_relation() {
        // {a, 1-a}: symbolic check.
        assert!(milnor_k2_symbol_relation("a", "1-a"));
    }

    #[test]
    fn test_milnor_k2_non_relation() {
        // {2, 3} is NOT the Steinberg relation (1-2 = -1 ≠ 3).
        assert!(!milnor_k2_symbol_relation("2", "3"));
    }

    // ── bass_theorem_projective tests ─────────────────────────────────────────

    #[test]
    fn test_bass_cancellation_rank_exceeds_dim() {
        let m = ProjectiveModule::free(5, "Z");
        // Krull dim of Z = 1; rank 5 > 1 satisfies Bass.
        assert!(bass_theorem_projective(&m, 1));
    }

    #[test]
    fn test_bass_cancellation_rank_equal_dim() {
        let m = ProjectiveModule::free(2, "Z[x]");
        // rank 2 = n=2: NOT strictly greater, so Bass fails.
        assert!(!bass_theorem_projective(&m, 2));
    }

    // ── format_k0 tests ───────────────────────────────────────────────────────

    #[test]
    fn test_format_k0_contains_classes() {
        let k0 = k0_of_field();
        let s = format_k0(&k0);
        assert!(s.contains("K_0"), "format_k0 should mention K_0");
        assert!(s.contains("rank"), "format_k0 should mention rank");
    }

    #[test]
    fn test_format_k0_nonempty() {
        let k0 = k0_of_integers();
        assert!(!format_k0(&k0).is_empty());
    }

    // ── ProjectiveModule helper tests ─────────────────────────────────────────

    #[test]
    fn test_projective_module_free() {
        let m = ProjectiveModule::free(3, "Q");
        assert_eq!(m.rank, 3);
        assert_eq!(m.generators.len(), 3);
    }

    #[test]
    fn test_projective_module_direct_sum() {
        let p = ProjectiveModule::free(2, "Z");
        let q = ProjectiveModule::free(3, "Z");
        let pq = p.direct_sum(&q);
        assert_eq!(pq.rank, 5);
        assert_eq!(pq.generators.len(), 5);
    }

    // ── ElementaryMatrix tests ────────────────────────────────────────────────

    #[test]
    fn test_elementary_matrix_valid() {
        let e = ElementaryMatrix::new(3, 1, 2, 7);
        assert!(e.is_valid());
        let m = e.to_matrix("Z");
        assert_eq!(m.entry(1, 2), Some(7));
        assert_eq!(m.entry(0, 0), Some(1));
    }

    #[test]
    fn test_elementary_matrix_invalid_same_ij() {
        let e = ElementaryMatrix::new(3, 1, 1, 5);
        assert!(!e.is_valid());
    }

    // ── MilnorK2Symbol tests ──────────────────────────────────────────────────

    #[test]
    fn test_milnor_symbol_display() {
        let sym = MilnorK2Symbol::new("a", "b");
        let s = format!("{sym}");
        assert!(s.contains("a"));
        assert!(s.contains("b"));
    }

    #[test]
    fn test_milnor_symbol_trivially_one() {
        let sym = MilnorK2Symbol::new("a", "1");
        assert!(sym.is_trivially_one_right());
        let sym2 = MilnorK2Symbol::new("1", "b");
        assert!(sym2.is_trivially_one_left());
    }

    // ── k2_from_symbols tests ─────────────────────────────────────────────────

    #[test]
    fn test_k2_from_symbols_relations_generated() {
        let syms = vec![MilnorK2Symbol::new("2", "-1")];
        let k2 = k2_from_symbols(syms);
        assert!(!k2.relations.is_empty());
    }

    #[test]
    fn test_k2_group_num_symbols() {
        let syms = vec![MilnorK2Symbol::new("a", "b"), MilnorK2Symbol::new("c", "d")];
        let k2 = k2_from_symbols(syms);
        assert_eq!(k2.num_symbols(), 2);
    }

    // ── k1_from_units test ────────────────────────────────────────────────────

    #[test]
    fn test_k1_from_units_cyclic() {
        let k1 = k1_from_units(&["1", "-1"], "Z");
        assert_eq!(k1.num_generators(), 2);
    }
}