Grace/Cumulus/Algebra/CoefficientMatrix.g17

Open in Workbench Download source

Imports

SpanCoefficients

Declarations

• linearCombination.choose_rows theorem derivation
• FiniteAlgebraModule.multiplication_rows theorem derivation

Source

1-- Finite multiplication tables assembled from coefficient witnesses in 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.CoefficientMatrix8import SpanCoefficients910section Algebras11variable (A add zero neg mul one B plus z minus times unit f x : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis source : IsCommRing(R)15hypothesis target : IsCommRing(S)16hypothesis hom : IsRingHom(f, R, S)17hypothesis element : x ∈ S1819section Generators20variable (xs : Set)21hypothesis generators : List(B, xs)22hypothesis representations : ∀ y ∈ S, ∃ cs, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs)2324theorem linearCombination.choose_rows (ys : List(B))25  shows ∃ C, Finite(C) ∧ (∀ cs ∈ C, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)) ∧26    (∃ rows, FunctionBetween(rows, listSupport{B}(ys), C) ∧27      (∀ g ∈ listSupport{B}(ys), S[x * g] = linearCombination(R, S, f, xs, rows(g))))28proof29  induction ys30  | List.nil =>31    have rowTypes : ∀ cs ∈ ∅, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)32      intros cs impossible33      exfalso34      exact set.empty with impossible35    have function : ∅ : ∅ → ∅ by exact FunctionBetween.empty at ∅36    have equations : ∀ g ∈ ∅, S[x * g] = linearCombination(R, S, f, xs, ∅(g))37      intros g impossible38      exfalso39      exact set.empty with impossible40    refine ⟨∅, Finite.empty, rowTypes, ∅, ?_⟩41    constructor42    . rw listSupport43      exact function44    . intros g hg45      rw listSupport at hg46      exact equations with g, hg47  | List.cons(g, tail) using ih =>48    obtain ⟨C, finite, rowTypes, rows, function, equations⟩ := ih49    have alternatives : g ∈ listSupport{B}(tail) ∨ ¬(g ∈ listSupport{B}(tail)) by tauto50    cases alternatives with old | fresh51    . have same : insert(g, listSupport{B}(tail)) = listSupport{B}(tail)52        ext y53        constructor54        . intro hy55          have casesY := insert.membership.forward with hy56          cases casesY with equal | previous57          . rw equal58            exact old59          . exact previous60        . intro hy61          exact insert.contains with hy62      refine ⟨C, finite, rowTypes, rows, ?_⟩63      constructor64      . rw [listSupport, same]65        exact function66      . intros y hy67        rw [listSupport, same] at hy68        exact equations with y, hy69    . have member : g ∈ S70        assumption71      have ordinary := IsCommRing.ring with target72      have product := IsRing.mul_closed with ordinary, element, member73      obtain ⟨cs, list, length, equation⟩ := representations with S[x * g], product74      have nextFinite := Finite.insert at C, cs with finite75      have nextTypes : ∀ row ∈ insert(cs, C), List(A, row) ∧ ListOps.length{A}(row) = ListOps.length{B}(xs)76        intros row hr77        have casesRow := insert.membership.forward with hr78        cases casesRow with same | previous79        . rw same80          refine ⟨list, length⟩81        . exact rowTypes with row, previous82      have nextFunction := adjoinMap.function at rows, listSupport{B}(tail), C, g, cs with function, fresh83      have newMember := insert.self at g, listSupport{B}(tail)84      have newGraph := adjoinMap.relates_new at rows, g, cs85      have newValue := FunctionBetween.apply_value with nextFunction, newMember, newGraph86      have nextEquations : ∀ y ∈ insert(g, listSupport{B}(tail)), S[x * y] = linearCombination(R, S, f, xs, adjoinMap(rows, g, cs)(y))87        intros y hy88        have casesY := insert.membership.forward with hy89        cases casesY with same | previous90        . rw [same, newValue]91          exact equation92        . obtain ⟨value, valueIn, graph⟩ := FunctionBetween.exists_value with function, previous93          have oldValue := FunctionBetween.apply_value with function, previous, graph94          have included := adjoinMap.relates_old at rows, g, cs, y, value with graph95          have nextValue := FunctionBetween.apply_value with nextFunction, hy, included96          have oldEquation := equations with y, previous97          rw oldValue at oldEquation98          rwa nextValue99      refine ⟨insert(cs, C), nextFinite, nextTypes, adjoinMap(rows, g, cs), ?_⟩100      constructor101      . rw listSupport102        exact nextFunction103      . intros y hy104        rw listSupport at hy105        exact nextEquations with y, hy106107end Generators108109theorem FiniteAlgebraModule.multiplication_rows110  requires finiteModule : FiniteAlgebraModule(f, R, S)111  shows ∃ xs, List(B, xs) ∧ linearSpan(f, R, S, listSupport{B}(xs)) = S ∧112    (∃ C, Finite(C) ∧ (∀ cs ∈ C, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)) ∧113      (∃ rows, FunctionBetween(rows, listSupport{B}(xs), C) ∧114        (∀ g ∈ listSupport{B}(xs), S[x * g] = linearCombination(R, S, f, xs, rows(g)))))115proof116  obtain ⟨xs, list, representations⟩ := FiniteAlgebraModule.coefficients at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *117  have first := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, listSupport{B}(xs) with *118  have combinations := linearCombination.mem_span with *119  have second : S ⊆ linearSpan(f, R, S, listSupport{B}(xs))120    intros y hy121    obtain ⟨cs, coefficients, length, equal⟩ := representations with y, hy122    rw equal123    exact combinations with cs, coefficients124  have spans := Subset.antisymmetric with first, second125  have table := linearCombination.choose_rows with *126  refine ⟨xs, list, spans, table⟩127128end Algebras129