-- Finite multiplication tables assembled from coefficient witnesses in 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.CoefficientMatrix
import SpanCoefficients

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

section Generators
variable (xs : Set)
hypothesis generators : List(B, xs)
hypothesis representations : ∀ y ∈ S, ∃ cs, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs)

theorem linearCombination.choose_rows (ys : List(B))
  shows ∃ C, Finite(C) ∧ (∀ cs ∈ C, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)) ∧
    (∃ rows, FunctionBetween(rows, listSupport{B}(ys), C) ∧
      (∀ g ∈ listSupport{B}(ys), S[x * g] = linearCombination(R, S, f, xs, rows(g))))
proof
  induction ys
  | List.nil =>
    have rowTypes : ∀ cs ∈ ∅, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)
      intros cs impossible
      exfalso
      exact set.empty with impossible
    have function : ∅ : ∅ → ∅ by exact FunctionBetween.empty at ∅
    have equations : ∀ g ∈ ∅, S[x * g] = linearCombination(R, S, f, xs, ∅(g))
      intros g impossible
      exfalso
      exact set.empty with impossible
    refine ⟨∅, Finite.empty, rowTypes, ∅, ?_⟩
    constructor
    . rw listSupport
      exact function
    . intros g hg
      rw listSupport at hg
      exact equations with g, hg
  | List.cons(g, tail) using ih =>
    obtain ⟨C, finite, rowTypes, rows, function, equations⟩ := ih
    have alternatives : g ∈ listSupport{B}(tail) ∨ ¬(g ∈ listSupport{B}(tail)) by tauto
    cases alternatives with old | fresh
    . have same : insert(g, listSupport{B}(tail)) = listSupport{B}(tail)
        ext y
        constructor
        . intro hy
          have casesY := insert.membership.forward with hy
          cases casesY with equal | previous
          . rw equal
            exact old
          . exact previous
        . intro hy
          exact insert.contains with hy
      refine ⟨C, finite, rowTypes, rows, ?_⟩
      constructor
      . rw [listSupport, same]
        exact function
      . intros y hy
        rw [listSupport, same] at hy
        exact equations with y, hy
    . have member : g ∈ S
        assumption
      have ordinary := IsCommRing.ring with target
      have product := IsRing.mul_closed with ordinary, element, member
      obtain ⟨cs, list, length, equation⟩ := representations with S[x * g], product
      have nextFinite := Finite.insert at C, cs with finite
      have nextTypes : ∀ row ∈ insert(cs, C), List(A, row) ∧ ListOps.length{A}(row) = ListOps.length{B}(xs)
        intros row hr
        have casesRow := insert.membership.forward with hr
        cases casesRow with same | previous
        . rw same
          refine ⟨list, length⟩
        . exact rowTypes with row, previous
      have nextFunction := adjoinMap.function at rows, listSupport{B}(tail), C, g, cs with function, fresh
      have newMember := insert.self at g, listSupport{B}(tail)
      have newGraph := adjoinMap.relates_new at rows, g, cs
      have newValue := FunctionBetween.apply_value with nextFunction, newMember, newGraph
      have nextEquations : ∀ y ∈ insert(g, listSupport{B}(tail)), S[x * y] = linearCombination(R, S, f, xs, adjoinMap(rows, g, cs)(y))
        intros y hy
        have casesY := insert.membership.forward with hy
        cases casesY with same | previous
        . rw [same, newValue]
          exact equation
        . obtain ⟨value, valueIn, graph⟩ := FunctionBetween.exists_value with function, previous
          have oldValue := FunctionBetween.apply_value with function, previous, graph
          have included := adjoinMap.relates_old at rows, g, cs, y, value with graph
          have nextValue := FunctionBetween.apply_value with nextFunction, hy, included
          have oldEquation := equations with y, previous
          rw oldValue at oldEquation
          rwa nextValue
      refine ⟨insert(cs, C), nextFinite, nextTypes, adjoinMap(rows, g, cs), ?_⟩
      constructor
      . rw listSupport
        exact nextFunction
      . intros y hy
        rw listSupport at hy
        exact nextEquations with y, hy

end Generators

theorem FiniteAlgebraModule.multiplication_rows
  requires finiteModule : FiniteAlgebraModule(f, R, S)
  shows ∃ xs, List(B, xs) ∧ linearSpan(f, R, S, listSupport{B}(xs)) = S ∧
    (∃ C, Finite(C) ∧ (∀ cs ∈ C, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)) ∧
      (∃ rows, FunctionBetween(rows, listSupport{B}(xs), C) ∧
        (∀ g ∈ listSupport{B}(xs), S[x * g] = linearCombination(R, S, f, xs, rows(g)))))
proof
  obtain ⟨xs, list, representations⟩ := FiniteAlgebraModule.coefficients at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *
  have first := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, listSupport{B}(xs) with *
  have combinations := linearCombination.mem_span with *
  have second : S ⊆ linearSpan(f, R, S, listSupport{B}(xs))
    intros y hy
    obtain ⟨cs, coefficients, length, equal⟩ := representations with y, hy
    rw equal
    exact combinations with cs, coefficients
  have spans := Subset.antisymmetric with first, second
  have table := linearCombination.choose_rows with *
  refine ⟨xs, list, spans, table⟩

end Algebras