Grace/Cumulus/Algebra/CoefficientInduction.g17

Open in Workbench Download source

Imports

CoefficientSingle

Declarations

Source

1-- Induction on finitely supported coefficient maps by zero, terms, and addition.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.CoefficientInduction8import CoefficientSingle910defgraph coefficientErase (I A z f j : Set) (i ∈ I) : A := singleValue(A, f(i), z, j, i)11requires zeroIn : z ∈ A12requires function : f : I → A13proof14  have value := FunctionBetween.apply_closed at f, I, A, i with *15  exact singleValue.closed at A, f(i), z, j, i with *1617theorem coefficientErase.same (I A z f j : Set)18  requires zeroIn : z ∈ A19  requires function : f : I → A20  requires index : j ∈ I21  shows coefficientErase(I, A, z, f, j)(j) = z22proof23  have coefficient := FunctionBetween.apply_closed with *24  have value := coefficientErase.value at I, A, z, f, j, j with *25  have same : j = j by rfl26  have selected := singleValue.same at A, f(j), z, j, j with *27  cc2829theorem coefficientErase.other (I A z f j i : Set)30  requires zeroIn : z ∈ A31  requires function : f : I → A32  requires index : i ∈ I33  requires different : i ≠ j34  shows coefficientErase(I, A, z, f, j)(i) = f(i)35proof36  have coefficient := FunctionBetween.apply_closed with *37  have value := coefficientErase.value at I, A, z, f, j, i with *38  have selected := singleValue.other at A, f(i), z, j, i with *39  cc4041theorem coefficientErase.support (I A z f j : Set)42  requires zeroIn : z ∈ A43  requires function : f : I → A44  shows functionSupport(coefficientErase(I, A, z, f, j), I, z) ⊆ functionSupport(f, I, z) ∖ {j}45proof46  intros i hi47  have data := functionSupport.membership.forward with hi48  have different : i ≠ j49    intro equal50    have erased := coefficientErase.same at I, A, z, f, i with *51    have impossible : coefficientErase(I, A, z, f, j)(i) = z by cc52    exact data.right with impossible53  have value := coefficientErase.other with *54  apply difference.membership.backward55  constructor56  . apply functionSupport.membership.backward at f, I, z, i57    rwa value at data58  . settle with singleton.membership5960section Rings61variable (I A add zero neg mul one : Set)62hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)63notation ring R := (A, add, zero, neg, mul, one)6465theorem coefficientErase.restore (f j : Set)66  requires function : f : I → A67  requires index : j ∈ I68  shows coefficientAdd(I, A, add, zero, neg, mul, one, coefficientSingle(I, A, zero, f(j), j), coefficientErase(I, A, zero, f, j)) = f69proof70  have ordinary := IsCommRing.ring with ring71  have zeroIn := IsRing.zero_in_carrier with ordinary72  have coefficient := FunctionBetween.apply_closed with *73  have single := coefficientSingle.function at I, A, zero, f(j), j with *74  have erased := coefficientErase.function at I, A, zero, f, j with *75  have restored := coefficientAdd.function at I, A, add, zero, neg, mul, one, coefficientSingle(I, A, zero, f(j), j), coefficientErase(I, A, zero, f, j) with *76  apply FunctionBetween.ext with restored, function77  intros i hi78  have value := FunctionBetween.apply_closed at f, I, A, i with *79  have sum := coefficientAdd.value at I, A, add, zero, neg, mul, one, coefficientSingle(I, A, zero, f(j), j), coefficientErase(I, A, zero, f, j), i with *80  rw sum81  have alternatives : i = j ∨ i ≠ j by tauto82  cases alternatives with same | different83  . rw same84    have value1 := coefficientSingle.same at I, A, zero, f(j), j with *85    rw value186    have value2 := coefficientErase.same at I, A, zero, f, j with *87    rw value288    ring89  . have singleOther := coefficientSingle.other with zeroIn, coefficient, different90    rw singleOther91    have value3 := coefficientErase.other with zeroIn, function, different92    rw value393    ring9495theorem coefficientMaps.generated_list (S : Set) (xs : List(I))96  requires base : constantFunction(I, A, zero) ∈ S97  requires step : ∀ a ∈ A, ∀ j ∈ I, ∀ f ∈ S, coefficientAdd(I, A, add, zero, neg, mul, one, coefficientSingle(I, A, zero, a, j), f) ∈ S98  shows ∀ f, FunctionBetween(f, I, A) → functionSupport(f, I, zero) ⊆ listSupport{I}(xs) → f ∈ S99proof100  induction xs101  | List.nil =>102    intros f function covers103    have ordinary := IsCommRing.ring with ring104    have zeroIn := IsRing.zero_in_carrier with ordinary105    rw listSupport at covers106    have zeroFunction := constantFunction.function at I, A, zero with *107    have equal : f = constantFunction(I, A, zero)108      apply FunctionBetween.ext with function, zeroFunction109      intros i hi110      have absent : ¬(i ∈ functionSupport(f, I, zero))111        intro supported112        have impossible := covers with i, supported113        exact set.empty with impossible114      have vanishes := functionSupport.outside at f, I, zero, i with *115      have value := constantFunction.apply at I, A, i, zero with *116      cc117    rwa equal118  | List.cons(j, tail) using ih =>119    intros f function covers120    have ordinary := IsCommRing.ring with ring121    have zeroIn := IsRing.zero_in_carrier with ordinary122    have index : j ∈ I by assumption123    rw listSupport at covers124    have erased := coefficientErase.function at I, A, zero, f, j with *125    have support := coefficientErase.support at I, A, zero, f, j with *126    have smaller : functionSupport(coefficientErase(I, A, zero, f, j), I, zero) ⊆ listSupport{I}(tail)127      intros i hi128      have data := support with i, hi129      have difference := difference.membership.forward with data130      have covered := covers with i, difference.left131      have alternatives := insert.membership.forward with covered132      cases alternatives with equal | old133      . have singleton : i ∈ {j}134          simp135        exfalso136        exact difference.right with singleton137      . exact old138    have rest := ih with coefficientErase(I, A, zero, f, j), erased, smaller139    have coefficient := FunctionBetween.apply_closed at f, I, A, j with *140    have next := step with f(j), coefficient, j, index, coefficientErase(I, A, zero, f, j), rest141    have restore := coefficientErase.restore at I, A, add, zero, neg, mul, one, f, j with *142    rwa restore at next143144theorem coefficientMaps.induction (S f : Set)145  requires map : CoefficientMap(f, I, A, zero)146  requires base : constantFunction(I, A, zero) ∈ S147  requires step : ∀ a ∈ A, ∀ j ∈ I, ∀ p ∈ S, coefficientAdd(I, A, add, zero, neg, mul, one, coefficientSingle(I, A, zero, a, j), p) ∈ S148  shows f ∈ S149proof150  obtain ⟨xs, list, covers⟩ := CoefficientMap.support_list with ring, map151  have function := CoefficientMap.function with map152  have generated := coefficientMaps.generated_list with *153  exact generated with f, function, covers154155end Rings156