MultiplicationMatrices

A finite module supplies a square multiplication matrix, without a basis or Choice

Open in Workbench View on GitHub

1-- A finite module supplies a square multiplication matrix, without a basis or Choice.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module MultiplicationMatrices8import Grace.Cumulus.Algebra.MultiplicationMatrix910theorem lists_are_determined_by_entries (A z : Set) (xs ys : List(A))11  requires sameLength : length{A}(xs) = length{A}(ys)12  requires entries : ∀ n, Nat(n) → n < length{A}(xs) → listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)13  shows xs = ys14proof15  exact listCoefficient.ext with *1617theorem positions_cover_the_support (A z : Set) (xs : List(A))18  shows SurjectiveBetween(listEntries(A, z, xs), length{A}(xs), listSupport{A}(xs))19proof20  exact listEntries.surjective with *2122theorem repeated_generators_keep_both_positions (A z a : Set)23  requires element : a ∈ A24  shows length{A}([a, a]) = 2 ∧ listCoefficient{A}(z, [a, a], 0) = a ∧ listCoefficient{A}(z, [a, a], 1) = a25proof26  have nil : List(A, []) by typecheck27  have single : List(A, [a]) by typecheck28  have double : List(A, [a, a]) by typecheck29  constructor30  . rw length.cons31    rw length.cons32    rw length.nil33    rfl34  . constructor35    . exact listCoefficient.zero with *36    . rw listCoefficient.succ37      exact listCoefficient.zero with *3839theorem empty_list_has_no_positions (A z : Set)40  shows listEntries(A, z, []) : ∅ → ∅41proof42  have list : List(A, []) by typecheck43  have function := listEntries.function at A, z, [] with *44  rw length.nil at function45  rw nat.zero at function46  rw listSupport.nil at function47  exact function4849theorem recover_a_coefficient_row (n A zero C rows i : Set) (cs : List(A))50  requires natural : Nat(n)51  requires default : zero ∈ A52  requires function : rows : n → C53  requires rowTypes : ∀ ds ∈ C, List(A, ds)54  requires rowLengths : ∀ ds ∈ C, length{A}(ds) = n55  requires row : i ∈ n56  requires size : length{A}(cs) = n57  requires coefficients : ∀ j ∈ n, coefficientMatrix(n, A, zero, C, rows)[i, j] = listCoefficient{A}(zero, cs, j)58  shows rows(i) = cs59proof60  exact coefficientMatrix.row_unique with *6162section Algebras63variable (A add zero neg mul one B plus z minus times unit f x : Set)64notation ring R := (A, add, zero, neg, mul, one)65notation ring S := (B, plus, z, minus, times, unit)66hypothesis source : IsCommRing(R)67hypothesis target : IsCommRing(S)68hypothesis hom : IsRingHom(f, R, S)69hypothesis element : x ∈ S7071theorem square_multiplication_matrix72  requires finiteModule : FiniteAlgebraModule(f, R, S)73  shows ∃ xs, List(B, xs) ∧ linearSpan(f, R, S, listSupport{B}(xs)) = S ∧74    (∃ M, RingMatrix(length{B}(xs), R, M) ∧75      (∀ i ∈ length{B}(xs), ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧76        S[x * listCoefficient{B}(z, xs, i)] = linearCombination(R, S, f, xs, cs) ∧77        (∀ j ∈ length{B}(xs), M[i, j] = listCoefficient{A}(zero, cs, j))))78proof79  exact FiniteAlgebraModule.multiplication_matrix with *8081end Algebras82