IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory FinSupp_ZF imports Finite_ZF Group_ZF_2

begin

Functions with finite support are those functions valued in a monoid that are equal to the neutral element everywhere except a finite number of points. They form a submonoid of the space of all functions valued in the monoid with the natural pointwise operation (or a subgroup if functions are valued in a group). Polynomials can be viewed as ring valued sequences that have finite support.

Functions with finite support

In this section we provide the definition and set up notation for formalizing the notion of finitely supported functions.

Support of a function is the subset of its domain where the values are not zero.

definition

\( \text{Supp}(f,G,A) \equiv \{x \in domain(f).\ f(x) \neq \text{ TheNeutralElement}(G,A)\} \)

A finitely supported function is such that its support is in the finite powerset of its domain.

definition

\( \text{FinSupp}(X,G,A) \equiv \{f \in X\rightarrow G.\ \text{Supp}(f,G,A) \in \text{FinPow}(X)\} \)

We will use the additive notation writing about finitely supported functions. In the finsupp context defined below we assume that \((M,A)\) is a monoid and \(X\) is some arbitrary set. We denote \( \mathcal{A} \) to be the pointwise operation on \(M\)-valued functions on \(X\) corresponding to the monoid operation \(A\), (denoted as \( + \)). \( 0 \) is the neutral element of the monoid.

locale finsupp

assumes monoidAsssum: \( \text{IsAmonoid}(M,A) \)

defines \( a + b \equiv A\langle a,b\rangle \)

defines \( \mathcal{M} \equiv \text{FinSupp}(X,M,A) \)

defines \( \mathcal{A} \equiv A \text{ lifted to function space over } X \)

defines \( a \oplus b \equiv \mathcal{A} \langle a,b\rangle \)

defines \( 0 \equiv \text{ TheNeutralElement}(M,A) \)

defines \( supp(f) \equiv \text{Supp}(f,M,A) \)

We can use theorems proven in the monoid0 context.

lemma (in finsupp) monoid0_valid:

shows \( monoid0(M,A) \) using monoidAsssum, monoid0_def

Finitely supported functions valued in a monoid

We show in Group_ZF_2 that if \((M,A)\) is a monoid, and \(X\) is an arbitrary set, then the space of functions \(X\rightarrow M\) with the natural pointwise operation is also a monoid. In this section we show that the set of finitely supported funtions is a a sub-monoid of that monoid.

The sum of monoid valued functions is a monoid valued function.

lemma (in finsupp) lifted_op_closed:

assumes \( f:X \rightarrow M \), \( g:X \rightarrow M \)

shows \( f\oplus g : X\rightarrow M \)proof

have \( \mathcal{A} : (X\rightarrow M)\times (X\rightarrow M)\rightarrow (X\rightarrow M) \) using monoid0_valid, Group_ZF_2_1_L0A

with assms show \( f\oplus g : X\rightarrow M \)

qed

What is the value of a sum of monoid-valued functions?

lemma (in finsupp) finsupp_sum_val:

assumes \( f:X \rightarrow M \), \( g:X \rightarrow M \) and \( x \in X \)

shows \( (f\oplus g)(x) = f(x) + g(x) \) using assms, monoid0_valid, lifted_val

The support of the sum of functions is contained in the union of supports.

lemma (in finsupp) supp_sum_union:

assumes \( f:X \rightarrow M \), \( g:X \rightarrow M \)

shows \( supp(f\oplus g) \subseteq supp(f) \cup supp(g) \)proof

{

fix \( x \)

assume \( x \in supp(f\oplus g) \)

from assms have \( f\oplus g : X\rightarrow M \) using lifted_op_closed

with assms, \( x \in supp(f\oplus g) \) have \( x\in X \) and \( f(x) + g(x) \neq 0 \) using func1_1_L1, Supp_def, finsupp_sum_val

with assms have \( x \in (supp(f) \cup supp(g)) \) using monoid0_valid, sum_nonzero_elmnt_nonzero, func1_1_L1, Supp_def

}

thus \( thesis \)

qed

The sum of finitely supported functions is finitely supported.

lemma (in finsupp) sum_finsupp:

assumes \( f \in \mathcal{M} \), \( g \in \mathcal{M} \)

shows \( f\oplus g \in \mathcal{M} \)proof

from assms have I: \( f: X\rightarrow M \), \( g: X\rightarrow M \) and \( supp(f) \in \text{FinPow}(X) \), \( supp(g) \in \text{FinPow}(X) \) using FinSupp_def

then have \( supp(f) \cup supp(g) \in \text{FinPow}(X) \) and \( supp(f\oplus g) \subseteq supp(f) \cup supp(g) \) using union_finpow, supp_sum_union

then have \( supp(f\oplus g) \in \text{FinPow}(X) \) by (rule subset_finpow )

with I show \( f\oplus g \in \mathcal{M} \) using lifted_op_closed, FinSupp_def

qed

The neutral element of the lifted (pointwise) operation is the function equal zero everywhere. In the next lemma we show that this is a finitely supported function.

lemma (in finsupp) const_zero_fin_supp:

shows \( \text{ TheNeutralElement}(X\rightarrow M, \mathcal{A} ) \in \mathcal{M} \) using monoidAsssum, Group_ZF_2_1_L2, monoid0_valid, unit_is_neutral, func1_3_L1, func1_3_L2, func1_1_L1, Supp_def, empty_in_finpow, FinSupp_def

Finitely supported functions form a submonoid of all functions with pointwise operation.

theorem (in finsupp) fin_supp_monoid:

shows \( \text{IsAmonoid}(\mathcal{M} ,\text{restrict}(\mathcal{A} ,\mathcal{M} \times \mathcal{M} )) \)proof

have \( monoid0(X\rightarrow M,\mathcal{A} ) \) using monoid0_valid, Group_ZF_2_1_T1, monoid0_def

moreover

have \( \mathcal{M} \text{ is closed under } \mathcal{A} \), \( \mathcal{M} \subseteq (X\rightarrow M) \), \( \text{ TheNeutralElement}(X\rightarrow M, \mathcal{A} ) \in \mathcal{M} \) using sum_finsupp, IsOpClosed_def, FinSupp_def, const_zero_fin_supp

ultimately show \( thesis \) using group0_1_T1

qed

Group valued finitely supported functions

Similarly as in the monoid case the group valued finitely supported functions form a subgroup of all functions valued in that group.

We will reuse the notation defined in the finsupp context, just adding an assumption about that the existence of the right inverse with a notation for it.

locale finsupp1 = finsupp +

assumes rinverse: \( \forall x\in M.\ \exists y\in M.\ x + y = 0 \)

defines \( ( - a) \equiv \text{GroupInv}(M,A)(a) \)

With this additional assumption \((M,A)\) becomes a group and we can use theorems proven in ine group0 context.

lemma (in finsupp1) group0_valid:

shows \( \text{IsAgroup}(M,A) \) and \( group0(M,A) \) using monoidAsssum, rinverse, IsAgroup_def, group0_def

Recall from Group_ZF_2 that the function space of \(G\) valued functions is also a group.

lemma (in finsupp1) fungroup0_valid:

shows \( \text{IsAgroup}(X\rightarrow M,\mathcal{A} ) \) and \( group0(X\rightarrow M,\mathcal{A} ) \) using group0_valid, Group_ZF_2_1_T2, group0_def

A function has the same support as its negative.

lemma (in finsupp1) finsupp_neg:

assumes A1: \( f: X\rightarrow M \)

shows \( supp(f) = supp( \text{GroupInv}(X\rightarrow M,\mathcal{A} )(f)) \)proof

let \( g = \text{GroupInv}(X\rightarrow M,\mathcal{A} )(f) \)

from A1 have I: \( g : X\rightarrow M \) using fungroup0_valid, inverse_in_group

have \( supp(g) \subseteq supp(f) \)proof

{

fix \( x \)

assume \( x \in supp(g) \)

with I have \( x\in X \) and \( g(x) \neq 0 \) using func1_1_L1, Supp_def

with A1 have \( x \in supp(f) \) using group0_valid, lift_gr_inv_val, group0_2_L8C, func1_1_L1, Supp_def

}

thus \( supp(g) \subseteq supp(f) \)

qed

moreover

from A1, I have \( supp(f) \subseteq supp(g) \) using func1_1_L1, Supp_def, group0_valid, group0_2_L8B, lift_gr_inv_val

ultimately show \( thesis \)

qed

The negative of a function with a finite support is a function with a finite support.

lemma (in finsupp1) finsupp_neg_finsupp:

assumes A1: \( f \in \mathcal{M} \)

shows \( \text{GroupInv}(X\rightarrow M,\mathcal{A} )(f) \in \mathcal{M} \)proof

let \( g = \text{GroupInv}(X\rightarrow M,\mathcal{A} )(f) \)

from A1 have I: \( f: X\rightarrow M \), \( supp(f) \in \text{FinPow}(X) \) using FinSupp_def, func1_1_L1

then have \( g \in X\rightarrow M \) using fungroup0_valid, inverse_in_group

moreover

from I have \( supp(g) \in \text{FinPow}(X) \) using finsupp_neg

ultimately show \( thesis \) using FinSupp_def

qed

Finitely supported functions form a subgroup with pointwise addition of group-valued functions.

theorem (in finsupp1) fin_sup_group:

shows \( \text{IsAsubgroup}(\mathcal{M} ,\mathcal{A} ) \)proof

have \( \mathcal{M} \neq 0 \) and \( \mathcal{M} \subseteq X\rightarrow M \) and \( \mathcal{M} \text{ is closed under } \mathcal{A} \) and \( \forall f\in \mathcal{M} .\ \text{GroupInv}(X\rightarrow M,\mathcal{A} )(f) \in \mathcal{M} \) using const_zero_fin_supp, FinSupp_def, sum_finsupp, IsOpClosed_def, finsupp_neg_finsupp

then show \( \text{IsAsubgroup}(\mathcal{M} ,\mathcal{A} ) \) using fungroup0_valid, group0_3_T3

qed

end

lemma (in finsupp) monoid0_valid: shows \( monoid0(M,A) \)

lemma (in monoid0) Group_ZF_2_1_L0A:

assumes \( F = f \text{ lifted to function space over } X \)

shows \( F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G) \)

lemma (in monoid0) lifted_val:

assumes \( F = f \text{ lifted to function space over } X \) and \( s:X\rightarrow G \), \( r:X\rightarrow G \) and \( x\in X \)

shows \( (F\langle s,r\rangle )(x) = s(x) \oplus r(x) \)

lemma (in finsupp) lifted_op_closed:

assumes \( f:X \rightarrow M \), \( g:X \rightarrow M \)

shows \( f\oplus g : X\rightarrow M \)

lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)

Definition of Supp: \( \text{Supp}(f,G,A) \equiv \{x \in domain(f).\ f(x) \neq \text{ TheNeutralElement}(G,A)\} \)

lemma (in finsupp) finsupp_sum_val:

assumes \( f:X \rightarrow M \), \( g:X \rightarrow M \) and \( x \in X \)

shows \( (f\oplus g)(x) = f(x) + g(x) \)

lemma (in monoid0) sum_nonzero_elmnt_nonzero:

assumes \( a \oplus b \neq \text{ TheNeutralElement}(G,f) \)

shows \( a \neq \text{ TheNeutralElement}(G,f) \vee b \neq \text{ TheNeutralElement}(G,f) \)

Definition of FinSupp: \( \text{FinSupp}(X,G,A) \equiv \{f \in X\rightarrow G.\ \text{Supp}(f,G,A) \in \text{FinPow}(X)\} \)

lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)

lemma (in finsupp) supp_sum_union:

assumes \( f:X \rightarrow M \), \( g:X \rightarrow M \)

shows \( supp(f\oplus g) \subseteq supp(f) \cup supp(g) \)

lemma subset_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \subseteq A \)

shows \( B \in \text{FinPow}(X) \)

lemma Group_ZF_2_1_L2:

assumes \( \text{IsAmonoid}(G,f) \) and \( F = f \text{ lifted to function space over } X \) and \( E = \text{ConstantFunction}(X,\text{ TheNeutralElement}(G,f)) \)

shows \( E = \text{ TheNeutralElement}(X\rightarrow G,F) \)

lemma (in monoid0) unit_is_neutral:

assumes \( e = \text{ TheNeutralElement}(G,f) \)

shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)

lemma func1_3_L1:

assumes \( c\in Y \)

shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \)

lemma func1_3_L2:

assumes \( x\in X \)

shows \( \text{ConstantFunction}(X,c)(x) = c \)

lemma empty_in_finpow: shows \( 0 \in \text{FinPow}(X) \)

lemma (in monoid0) Group_ZF_2_1_T1:

assumes \( F = f \text{ lifted to function space over } X \)

shows \( \text{IsAmonoid}(X\rightarrow G,F) \)

lemma (in finsupp) sum_finsupp:

assumes \( f \in \mathcal{M} \), \( g \in \mathcal{M} \)

shows \( f\oplus g \in \mathcal{M} \)

Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)

lemma (in finsupp) const_zero_fin_supp: shows \( \text{ TheNeutralElement}(X\rightarrow M, \mathcal{A} ) \in \mathcal{M} \)

theorem (in monoid0) group0_1_T1:

assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)

shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \)

Definition of IsAgroup: \( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)

lemma (in finsupp1) group0_valid: shows \( \text{IsAgroup}(M,A) \) and \( group0(M,A) \)

theorem (in group0) Group_ZF_2_1_T2:

assumes \( F = P \text{ lifted to function space over } X \)

shows \( \text{IsAgroup}(X\rightarrow G,F) \)

lemma (in finsupp1) fungroup0_valid: shows \( \text{IsAgroup}(X\rightarrow M,\mathcal{A} ) \) and \( group0(X\rightarrow M,\mathcal{A} ) \)

lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)

corollary (in group0) lift_gr_inv_val:

assumes \( F = P \text{ lifted to function space over } X \) and \( s : X\rightarrow G \) and \( x\in X \)

shows \( ( \text{GroupInv}(X\rightarrow G,F)(s))(x) = (s(x))^{-1} \)

lemma (in group0) group0_2_L8C:

assumes \( a\in G \) and \( a^{-1} \neq 1 \)

shows \( a\neq 1 \)

lemma (in group0) group0_2_L8B:

assumes \( a\in G \) and \( a \neq 1 \)

shows \( a^{-1} \neq 1 \)