Grace/Cumulus/Algebra/SpanCoefficients.g17

Open in Workbench Download source

Imports

SpanInsert · CoefficientLists · Cardinal.ListSupport

Declarations

Source

1-- Explicit finite coefficient lists for relative linear spans (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.SpanCoefficients8import SpanInsert9import CoefficientLists10import Cardinal.ListSupport1112-- Missing coefficients are zero; extra coefficients are ignored.13-- Existence results below provide exactly one coefficient per generator.14def linearCombination (A sourceZero B plus z times f : Set) (xs : List(B)) (cs : List(A)) → Set15  | A, sourceZero, B, plus, z, times, f, List.nil, cs => z16  | A, sourceZero, B, plus, z, times, f, List.cons(x, tail), cs => plus(times(f(listHeadOr{A}(sourceZero, cs)), x), linearCombination(A, sourceZero, B, plus, z, times, f, tail, listTail{A}(cs)))17  descends xs1819notation scoped linearCombination(R, S, f, xs, cs) => linearCombination(R.carrier, R.zero, S.carrier, S.add, S.zero, S.mul, f, xs, cs)2021theorem listHeadOr.closed (A zero : Set) (cs : List(A))22  requires zeroIn : zero ∈ A23  shows listHeadOr{A}(zero, cs) ∈ A24proof25  induction cs26  | List.nil =>27    rwa listHeadOr28  | List.cons(a, tail) using ih =>29    rwa listHeadOr3031section Algebras32variable (A add zero neg mul one B plus z minus times unit f : Set)33notation ring R := (A, add, zero, neg, mul, one)34notation ring S := (B, plus, z, minus, times, unit)35hypothesis source : IsCommRing(R)36hypothesis target : IsCommRing(S)37hypothesis hom : IsRingHom(f, R, S)3839theorem linearCombination.cons (x : Set) (xs : List(B)) (a : Set) (cs : List(A))40  requires element : x ∈ S41  requires coefficient : a ∈ R42  shows linearCombination(R, S, f, x :: xs, a :: cs) = S[f(a) * x + linearCombination(R, S, f, xs, cs)]43proof44  rw [linearCombination, listHeadOr, listTail]45  rfl4647theorem linearCombination.mem_span (xs : List(B))48  shows ∀ cs, List(A, cs) → linearCombination(R, S, f, xs, cs) ∈ linearSpan(f, R, S, listSupport{B}(xs))49proof50  induction xs51  | List.nil =>52    intros cs list53    rw [linearCombination, listSupport]54    have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, ∅ with *55    exact Submodule.zero_mem with source, target, hom, span56  | List.cons(x, tail) using ih =>57    intros cs list58    have element : x ∈ S by assumption59    have r := IsCommRing.ring with source60    have zeroIn := IsRing.zero_in_carrier with r61    have head := listHeadOr.closed at A, zero, cs with *62    have tailList := listTail.closed at A, cs with *63    have rest := ih with listTail{A}(cs), tailList64    have bound := listSupport.subset at B, tail with *65    have enlargedBound : insert(x, listSupport{B}(tail)) ⊆ S by simp [Subset, insert.membership]66    have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, insert(x, listSupport{B}(tail)) with *67    have contains := linearSpan.contains with source, target, hom, enlargedBound68    have xIn : x ∈ linearSpan(f, R, S, insert(x, listSupport{B}(tail))) by simp [Subset, insert.membership]69    have subset : listSupport{B}(tail) ⊆ insert(x, listSupport{B}(tail)) by simp [Subset, insert.membership]70    have included := linearSpan.mono with source, target, hom, enlargedBound, subset71    have restIn : linearCombination(R, S, f, tail, listTail{A}(cs)) ∈ linearSpan(f, R, S, insert(x, listSupport{B}(tail)))72      exact included with linearCombination(R, S, f, tail, listTail{A}(cs)), rest73    have scalar := Submodule.scalar_mul_mem with source, target, hom, span, head, xIn74    have addition := Submodule.add_closed with source, target, hom, span75    rw [linearCombination, listSupport]76    exact ClosedBinary.mem with addition, scalar, restIn7778theorem linearCombination.closed (xs : List(B)) (cs : List(A))79  shows linearCombination(R, S, f, xs, cs) ∈ S80proof81  have combinations := linearCombination.mem_span at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, xs with *82  have member := combinations with cs, assumption83  have bounded := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, listSupport{B}(xs) with *84  exact bounded with linearCombination(R, S, f, xs, cs), member8586theorem linearSpan.list_coefficients (xs : List(B))87  shows ∀ y ∈ linearSpan(f, R, S, listSupport{B}(xs)), ∃ cs, List(A, cs) ∧88    ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs)89proof90  induction xs91  | List.nil =>92    intros y hy93    rw listSupport at hy94    have empty := linearSpan.empty with *95    rw empty at hy96    have equal := singleton.membership.forward with hy97    have list : List(A, []) by typecheck98    refine ⟨[], list, ?_⟩99    constructor100    . rw [ListOps.length, ListOps.length]101      rfl102    . rw linearCombination103      exact equal104  | List.cons(x, tail) using ih =>105    intros y hy106    have element : x ∈ S by assumption107    have bounded := listSupport.subset with *108    rw listSupport at hy109    have decomposition := linearSpan.insert_membership.forward with *110    obtain ⟨a, ha, u, hu, equation⟩ := decomposition.right111    obtain ⟨cs, list, length, value⟩ := ih with u, hu112    have nextList : List(A, a :: cs) by typecheck113    refine ⟨a :: cs, nextList, ?_⟩114    constructor115    . rw [ListOps.length, ListOps.length, length]116      rfl117    . have combination := linearCombination.cons at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, tail, a, cs with *118      rw combination119      rwa value at equation120121theorem linearSpan.list_membership (xs : List(B)) (y : Set)122  shows y ∈ linearSpan(f, R, S, listSupport{B}(xs)) ↔123    (∃ cs, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs))124proof125  constructor126  . intro member127    have coefficients := linearSpan.list_coefficients with *128    exact coefficients with y, member129  . intro representation130    obtain ⟨cs, list, length, equal⟩ := representation131    have combinations := linearCombination.mem_span with *132    rw equal133    exact combinations with cs, list134135theorem FiniteAlgebraModule.coefficients136  requires finiteModule : FiniteAlgebraModule(f, R, S)137  shows ∃ xs, List(B, xs) ∧ (∀ y ∈ S, ∃ cs, List(A, cs) ∧138    ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs))139proof140  obtain ⟨G, finite, bounded, spans⟩ := finiteModule141  obtain ⟨xs, list, covers⟩ := Finite.cover_in with finite, bounded142  have supportBound := listSupport.subset with *143  have included := linearSpan.mono with source, target, hom, supportBound, covers144  rw spans at included145  have coefficients := linearSpan.list_coefficients with *146  refine ⟨xs, list, ?_⟩147  intros y hy148  have member : y ∈ linearSpan(f, R, S, listSupport{B}(xs)) by exact included with y, hy149  exact coefficients with y, member150151theorem FiniteAlgebraModule.of_coefficients (xs : List(B))152  requires representations : ∀ y ∈ S, ∃ cs, List(A, cs) ∧ y = linearCombination(R, S, f, xs, cs)153  shows FiniteAlgebraModule(f, R, S)154proof155  have finite := listSupport.finite with *156  have bounded := listSupport.subset with *157  have first := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, listSupport{B}(xs) with *158  have combinations := linearCombination.mem_span with *159  have second : S ⊆ linearSpan(f, R, S, listSupport{B}(xs))160    intros y hy161    obtain ⟨cs, list, equal⟩ := representations with y, hy162    rw equal163    exact combinations with cs, list164  have spans := Subset.antisymmetric with first, second165  unfold FiniteAlgebraModule166  refine ⟨listSupport{B}(xs), finite, bounded, spans⟩167168end Algebras169