Grace/Cumulus/Algebra/MultiplicationMatrix.g17

Open in Workbench Download source

Imports

CoefficientMatrix · IndexedLists · Ring.Determinant

Declarations

Source

1-- Square coefficient matrices for multiplication on finite modules (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.MultiplicationMatrix8import CoefficientMatrix9import IndexedLists10import Ring.Determinant1112-- A row is a coefficient list; columns read its entries in list order.13defunique coefficientMatrixEntry (n A zero C rows p : Set) (a ∈ A) :=14  ∃ i ∈ n, ∃ j ∈ n, p = (i, j) ∧ a = listCoefficient{A}(zero, rows(i), j)15requires natural : Nat(n)16requires default : zero ∈ A17requires function : rows : n → C18requires rowTypes : ∀ cs ∈ C, List(A, cs)19requires pair : p ∈ n × n20proof21  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at22    n, n, p with pair23  have positions := natural.member at n with natural24  have jNat := positions with j, hj25  have rowIn := FunctionBetween.apply_closed at rows, n, C, i with *26  have list := rowTypes with rows(i), rowIn27  have value := listCoefficient.closed at A, zero, rows(i), j with *28  refine ⟨listCoefficient{A}(zero, rows(i), j), value, i, hi, j, hj, shape, rfl⟩29uniqueness30  intros u hu first v hv second31  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first32  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second33  have equal : (i, j) = (k, l)34    cc35  have coordinates := orderedPair.injective at i, j, k, l with equal36  cc3738defgraph coefficientMatrix (n A zero C rows : Set) (p ∈ n × n) : A := coefficientMatrixEntry(n, A, zero, C, rows, p)39requires natural : Nat(n)40requires default : zero ∈ A41requires function : rows : n → C42requires rowTypes : ∀ cs ∈ C, List(A, cs)43proof44  have selected := coefficientMatrixEntry.selected at n, A, zero, C, rows, p with *45  exact selected.left4647theorem coefficientMatrix.pair (n A zero C rows i j : Set)48  requires natural : Nat(n)49  requires default : zero ∈ A50  requires function : rows : n → C51  requires rowTypes : ∀ cs ∈ C, List(A, cs)52  requires row : i ∈ n53  requires column : j ∈ n54  shows coefficientMatrix(n, A, zero, C, rows)[i, j] = listCoefficient{A}(zero, rows(i), j)55proof56  have pair := product.pair at i, j, n, n with *57  have selected := coefficientMatrixEntry.selected at n, A, zero, C, rows, (i, j) with *58  obtain ⟨k, hk, l, hl, shape, output⟩ := selected.right59  have coordinates := orderedPair.injective with shape60  have value := coefficientMatrix.value at n, A, zero, C, rows, (i, j) with *61  cc6263-- Once the length is fixed, the matrix determines each coefficient row uniquely.64theorem coefficientMatrix.row_unique (n A zero C rows i : Set) (cs : List(A))65  requires natural : Nat(n)66  requires default : zero ∈ A67  requires function : rows : n → C68  requires rowTypes : ∀ ds ∈ C, List(A, ds)69  requires rowLengths : ∀ ds ∈ C, length{A}(ds) = n70  requires row : i ∈ n71  requires size : length{A}(cs) = n72  requires entries : ∀ j ∈ n, coefficientMatrix(n, A, zero, C, rows)[i, j] = listCoefficient{A}(zero, cs, j)73  shows rows(i) = cs74proof75  have rowIn := FunctionBetween.apply_closed with *76  have list := rowTypes with rows(i), rowIn77  have length := rowLengths with rows(i), rowIn78  have sameLength : length{A}(rows(i)) = length{A}(cs) by cc79  have agreement : ∀ j, Nat(j) → j < length{A}(rows(i)) → listCoefficient{A}(zero, rows(i), j) = listCoefficient{A}(zero, cs, j)80    intros j jNat bound81    rw length at bound82    have position : j ∈ n by exact membership.of_Less at j, n with jNat, natural, bound83    have actual := coefficientMatrix.pair at n, A, zero, C, rows, i, j with *84    have specified := entries with j, position85    cc86  exact listCoefficient.ext with *8788section Algebras89variable (A add zero neg mul one B plus z minus times unit f x : Set)90notation ring R := (A, add, zero, neg, mul, one)91notation ring S := (B, plus, z, minus, times, unit)92hypothesis source : IsCommRing(R)93hypothesis target : IsCommRing(S)94hypothesis hom : IsRingHom(f, R, S)95hypothesis element : x ∈ S9697-- No independence or distinctness assumption: repeated generators remain positions.98theorem FiniteAlgebraModule.multiplication_matrix99  requires finiteModule : FiniteAlgebraModule(f, R, S)100  shows ∃ xs, List(B, xs) ∧ linearSpan(f, R, S, listSupport{B}(xs)) = S ∧101    (∃ M, RingMatrix(length{B}(xs), R, M) ∧102      (∀ i ∈ length{B}(xs), ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧103        S[x * listCoefficient{B}(z, xs, i)] = linearCombination(R, S, f, xs, cs) ∧104        (∀ j ∈ length{B}(xs), M[i, j] = listCoefficient{A}(zero, cs, j))))105proof106  obtain ⟨xs, list, spans, C, finite, rowTypes, rows, function, equations⟩ := FiniteAlgebraModule.multiplication_rows at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x with *107  have ordinary := IsCommRing.ring with source108  have zeroIn := IsRing.zero_in_carrier with ordinary109  have entries := listEntries.function at B, z, xs with *110  have indexed := compose.function at rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C with *111  have lists : ∀ cs ∈ C, List(A, cs)112    intros cs hc113    have data := rowTypes with cs, hc114    exact data.left115  have matrix := coefficientMatrix.function at length{B}(xs), A, zero, C, compose(rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C) with *116  refine ⟨xs, list, spans, coefficientMatrix(length{B}(xs), A, zero, C, compose(rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C)), ?_⟩117  constructor118    exact matrix119  . intros i hi120    have entry := listEntries.value at B, z, xs, i with *121    have supported := FunctionBetween.apply_closed at listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), i with *122    have rowIn := FunctionBetween.apply_closed at rows, listSupport{B}(xs), C, listEntries(B, z, xs)(i) with *123    have data := rowTypes with rows(listEntries(B, z, xs)(i)), rowIn124    have equation := equations with listEntries(B, z, xs)(i), supported125    have composite := compose.apply at rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C, i with *126    refine ⟨rows(listEntries(B, z, xs)(i)), data.left, data.right, ?_⟩127    constructor128    . rw ← entry129      exact equation130    . intros j hj131      have value := coefficientMatrix.pair at length{B}(xs), A, zero, C, compose(rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C), i, j with *132      rwa composite at value133134end Algebras135