-- Square coefficient matrices for multiplication on finite modules (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.MultiplicationMatrix
import CoefficientMatrix
import IndexedLists
import Ring.Determinant

-- A row is a coefficient list; columns read its entries in list order.
defunique coefficientMatrixEntry (n A zero C rows p : Set) (a ∈ A) :=
  ∃ i ∈ n, ∃ j ∈ n, p = (i, j) ∧ a = listCoefficient{A}(zero, rows(i), j)
requires natural : Nat(n)
requires default : zero ∈ A
requires function : rows : n → C
requires rowTypes : ∀ cs ∈ C, List(A, cs)
requires pair : p ∈ n × n
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at
    n, n, p with pair
  have positions := natural.member at n with natural
  have jNat := positions with j, hj
  have rowIn := FunctionBetween.apply_closed at rows, n, C, i with *
  have list := rowTypes with rows(i), rowIn
  have value := listCoefficient.closed at A, zero, rows(i), j with *
  refine ⟨listCoefficient{A}(zero, rows(i), j), value, i, hi, j, hj, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first
  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second
  have equal : (i, j) = (k, l)
    cc
  have coordinates := orderedPair.injective at i, j, k, l with equal
  cc

defgraph coefficientMatrix (n A zero C rows : Set) (p ∈ n × n) : A := coefficientMatrixEntry(n, A, zero, C, rows, p)
requires natural : Nat(n)
requires default : zero ∈ A
requires function : rows : n → C
requires rowTypes : ∀ cs ∈ C, List(A, cs)
proof
  have selected := coefficientMatrixEntry.selected at n, A, zero, C, rows, p with *
  exact selected.left

theorem coefficientMatrix.pair (n A zero C rows i j : Set)
  requires natural : Nat(n)
  requires default : zero ∈ A
  requires function : rows : n → C
  requires rowTypes : ∀ cs ∈ C, List(A, cs)
  requires row : i ∈ n
  requires column : j ∈ n
  shows coefficientMatrix(n, A, zero, C, rows)[i, j] = listCoefficient{A}(zero, rows(i), j)
proof
  have pair := product.pair at i, j, n, n with *
  have selected := coefficientMatrixEntry.selected at n, A, zero, C, rows, (i, j) with *
  obtain ⟨k, hk, l, hl, shape, output⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := coefficientMatrix.value at n, A, zero, C, rows, (i, j) with *
  cc

-- Once the length is fixed, the matrix determines each coefficient row uniquely.
theorem coefficientMatrix.row_unique (n A zero C rows i : Set) (cs : List(A))
  requires natural : Nat(n)
  requires default : zero ∈ A
  requires function : rows : n → C
  requires rowTypes : ∀ ds ∈ C, List(A, ds)
  requires rowLengths : ∀ ds ∈ C, length{A}(ds) = n
  requires row : i ∈ n
  requires size : length{A}(cs) = n
  requires entries : ∀ j ∈ n, coefficientMatrix(n, A, zero, C, rows)[i, j] = listCoefficient{A}(zero, cs, j)
  shows rows(i) = cs
proof
  have rowIn := FunctionBetween.apply_closed with *
  have list := rowTypes with rows(i), rowIn
  have length := rowLengths with rows(i), rowIn
  have sameLength : length{A}(rows(i)) = length{A}(cs) by cc
  have agreement : ∀ j, Nat(j) → j < length{A}(rows(i)) → listCoefficient{A}(zero, rows(i), j) = listCoefficient{A}(zero, cs, j)
    intros j jNat bound
    rw length at bound
    have position : j ∈ n by exact membership.of_Less at j, n with jNat, natural, bound
    have actual := coefficientMatrix.pair at n, A, zero, C, rows, i, j with *
    have specified := entries with j, position
    cc
  exact listCoefficient.ext with *

section Algebras
variable (A add zero neg mul one B plus z minus times unit f x : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis element : x ∈ S

-- No independence or distinctness assumption: repeated generators remain positions.
theorem FiniteAlgebraModule.multiplication_matrix
  requires finiteModule : FiniteAlgebraModule(f, R, S)
  shows ∃ xs, List(B, xs) ∧ linearSpan(f, R, S, listSupport{B}(xs)) = S ∧
    (∃ M, RingMatrix(length{B}(xs), R, M) ∧
      (∀ i ∈ length{B}(xs), ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧
        S[x * listCoefficient{B}(z, xs, i)] = linearCombination(R, S, f, xs, cs) ∧
        (∀ j ∈ length{B}(xs), M[i, j] = listCoefficient{A}(zero, cs, j))))
proof
  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 *
  have ordinary := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have entries := listEntries.function at B, z, xs with *
  have indexed := compose.function at rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C with *
  have lists : ∀ cs ∈ C, List(A, cs)
    intros cs hc
    have data := rowTypes with cs, hc
    exact data.left
  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 *
  refine ⟨xs, list, spans, coefficientMatrix(length{B}(xs), A, zero, C, compose(rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C)), ?_⟩
  constructor
    exact matrix
  . intros i hi
    have entry := listEntries.value at B, z, xs, i with *
    have supported := FunctionBetween.apply_closed at listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), i with *
    have rowIn := FunctionBetween.apply_closed at rows, listSupport{B}(xs), C, listEntries(B, z, xs)(i) with *
    have data := rowTypes with rows(listEntries(B, z, xs)(i)), rowIn
    have equation := equations with listEntries(B, z, xs)(i), supported
    have composite := compose.apply at rows, listEntries(B, z, xs), length{B}(xs), listSupport{B}(xs), C, i with *
    refine ⟨rows(listEntries(B, z, xs)(i)), data.left, data.right, ?_⟩
    constructor
    . rw ← entry
      exact equation
    . intros j hj
      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 *
      rwa composite at value

end Algebras