:: An Explicit Construction of Free Modules in Mizar
:: by Yasushige Watase
::
:: Received August 2, 2026
:: Copyright (c) 2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies TARSKI, FUNCSDOM, VECTSP_1, STRUCT_0, XBOOLE_0, VECTSP_2,
SUBSET_1, FUNCT_1, RELAT_1, FUNCT_2, CLASSES2, FUNCOP_1, NUMBERS, NAT_1,
ARYTM_3, ALGSTR_0, RLVECT_1, CARD_3, FINSEQ_1, XXREAL_0, SUPINF_2, MOD_3,
BINOP_1, ZFMISC_1, PARTFUN1, ARYTM_1, MESFUNC1, LMOD_7, CARD_1, FINSEQ_3,
FINSET_1, POLYNOM1, ALGSEQ_1, QC_LANG1, LOPBAN_1, UPROOTS, ORDINAL4,
RMOD_2, XCMPLX_0, GROUP_6, GROUP_4, PRELAMB, RFINSEQ, MSSUBFAM, SETWISEO,
FINSUB_1, RLVECT_3, ALGSTR_1, LMOD_XX1, RLVECT_2, FUNCT_5, MCART_1,
RLSUB_1, VALUED_1, MOD_2, LMODFREE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3,
FUNCOP_1, FINSET_1, FINSUB_1, SETWISEO, CARD_1, FUNCT_5, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_D, FINSEQ_1, FINSEQOP, FINSEQ_3, RFINSEQ,
STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, ALGSTR_1, FUNCSDOM, VECTSP_2,
VECTSP_4, VECTSP_6, VECTSP_7, MOD_2, POLYNOM1, MOD_4, ZMODUL01, PENCIL_2;
constructors FUNCT_5, RELSET_1, SETWISEO, NAT_D, FINSEQOP, FINSEQ_3, RFINSEQ,
VECTSP_6, GRCAT_1, MOD_2, MOD_4, RING_2, PENCIL_2;
registrations ORDINAL1, STRUCT_0, RELSET_1, SUBSET_1, FUNCT_2, FUNCOP_1,
VECTSP_1, VECTSP_4, NAT_1, FUNCT_1, CARD_1, FINSET_1, FINSEQ_1, RELAT_1,
XREAL_0, RLVECT_1, NEWTON04, FVSUM_1, INT_1, VECTSP_7;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, ALGSTR_0, RLVECT_1, VECTSP_1;
equalities XBOOLE_0, ALGSTR_0, STRUCT_0, BINOP_1, FUNCOP_1, VECTSP_1,
FINSEQ_1, XCMPLX_0, PENCIL_2, MOD_2;
expansions TARSKI, STRUCT_0, VECTSP_1, BINOP_1, FUNCT_2, XBOOLE_0, ALGSTR_0,
FUNCT_1, FINSEQ_1, VECTSP_7;
theorems TARSKI, FUNCT_2, FINSEQ_1, VECTSP_1, XBOOLE_0, RELAT_1, FUNCT_1,
FUNCOP_1, RLVECT_1, XBOOLE_1, ZMODUL01, ZFMISC_1, FUNCT_3, PARTFUN1,
POLYNOM1, GROUP_1, CARD_2, BINOM, FINSEQ_5, FINSEQ_2, FVSUM_1, FINSEQ_3,
ORDINAL1, MATRIX_3, CARD_1, XREAL_1, NAT_1, RFINSEQ, MOD_4, FINSEQ_4,
FINSEQOP, XXREAL_0, INT_1, NAT_D, SETWISEO, SETWOP_2, BINOP_1, FINSUB_1,
VECTSP_7, VECTSP_4, VECTSP_6, FUNCT_5;
schemes NAT_1, BINOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2;
begin :: Function spaces and free modules
reserve R for Ring;
reserve X for set;
reserve o,x for object;
reserve a,b for Element of the carrier of R;
reserve M,N for LeftMod of R;
reserve i for Nat;
definition
let R,X,N;
func 0_Funcs(X,N) -> Element of Funcs(X,the carrier of N) equals
X --> 0.N;
coherence by FUNCT_2:8;
end;
registration
let R,X,N;
cluster Funcs(X,the carrier of N) -> non empty;
coherence;
end;
definition
let R,X,N;
func ADD(X,N) -> BinOp of Funcs(X,the carrier of N) means
for f,g being Element of Funcs(X,the carrier of N) holds
it.(f,g) = (the addF of N).:(f,g);
existence
proof
deffunc F(Element of Funcs(X,the carrier of N),
Element of Funcs(X,the carrier of N))
= (the addF of N).:($1,$2);
consider F1 being BinOp of Funcs(X,the carrier of N)
such that
A1: for x,y being Element of Funcs(X,the carrier of N)
holds F1.(x,y) = F(x,y) from BINOP_1:sch 4;
take F1;
let f,g be Element of Funcs(X,the carrier of N);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(X,the carrier of N) such that
A2: for f,g being Element of Funcs(X,the carrier of N) holds
it1.(f,g) = (the addF of N).:(f,g) and
A3: for f,g being Element of Funcs(X,the carrier of N) holds
it2.(f,g) = (the addF of N).:(f,g);
now
let f,g be Element of Funcs(X,the carrier of N);
thus it1.(f,g) = (the addF of N).:(f,g) by A2
.= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
reserve f,g,h for Element of Funcs(X, the carrier of N);
definition
let R,X,N;
let F be Function of [:the carrier of R,the carrier of N:], the carrier of N;
let a be Element of the carrier of R;
let f be Function of X,N;
redefine func F[;](a,f) -> Element of Funcs(X, the carrier of N); :: redefines [;] (FUNCOP_1, definition)
coherence
proof
A1: dom f = X by FUNCT_2:def 1;
reconsider g = <:dom f --> a, f:> as Function of X,
[:the carrier of R, the carrier of N:] by FUNCT_3:58,A1;
F[;](a,f) = F * g;
hence thesis by FUNCT_2:8;
end;
end;
::for x being object st x in X holds (it.(a,f)).x = (the lmult of N).(a,f.x)
definition
let R,X,N;
func LMULT(X,N) ->
Function of [:the carrier of R,Funcs(X,the carrier of N):],
Funcs(X,the carrier of N) means
for a being Element of the carrier of R, f being Element of
Funcs(X,the carrier of N)
holds
for x being object st x in X holds (it.(a,f)).x = (the lmult of N).(a,f.x);
existence
proof
deffunc F(Element of the carrier of R,Element of
Funcs(X,the carrier of N)) = ((the lmult of N)[;]($1,$2));
consider F1 being
Function of [:the carrier of R,Funcs(X,the carrier of N):],
Funcs(X,the carrier of N) such that
A1: for a be Element of the carrier of R,
f being Element of Funcs(X,the carrier of N) holds
F1.(a,f) = F(a,f) from BINOP_1:sch 4;
take F1;
let a be Element of the carrier of R,
f be Element of Funcs(X,the carrier of N),
x be object;
assume
A3: x in X;
A2: dom (F1.(a,f)) = X by FUNCT_2:92;
F1.(a,f) = ((the lmult of N)[;](a,f)) by A1;
hence thesis by A2,A3,FUNCOP_1:32;
end;
uniqueness
proof
let it1,it2 be Function of
[:the carrier of R,Funcs(X,the carrier of N):],
Funcs(X,the carrier of N) such that
A4: for a being Element of the carrier of R,
f being Element of Funcs(X,the carrier of N) holds
for x being object st x in X holds
(it1.(a,f)).x = (the lmult of N).(a,f.x) and
A5: for a being Element of the carrier of R,
f being Element of Funcs(X,the carrier of N) holds
for x being object st x in X holds
(it2.(a,f)).x = (the lmult of N).(a,f.x);
for a being Element of the carrier of R,
f being Element of Funcs(X,the carrier of N) holds it1.(a,f) = it2.(a,f)
proof
let a be Element of the carrier of R,
f be Element of Funcs(X,the carrier of N);
A6: dom (it1.(a,f)) = X & dom (it2.(a,f))= X by FUNCT_2:92;
for x be object st x in dom (it1.(a,f)) holds
(it1.(a,f)).x = (it2.(a,f)).x
proof
let x be object;
assume x in dom (it1.(a,f)); then
A8: x in X by FUNCT_2:92;
hence (it1.(a,f)).x = (the lmult of N).(a,f.x) by A4
.= (it2.(a,f)).x by A8,A5;
end;
hence thesis by A6;
end;
hence thesis;
end;
end;
definition
let R,X,N;
func Func_Mod(X,N) -> non empty ModuleStr over R equals
ModuleStr(# Funcs(X,the carrier of N),
ADD(X,N), 0_Funcs(X,N), LMULT(X,N) #);
coherence;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Funcs(X,R)/finite Support -> R-Module
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::$INSERT Module structure on function spaces & on finitely supported functions.
definition
let R,X;
func 0_Funcs(X,R) -> Element of Funcs(X,the carrier of R) equals
X --> 0.R;
coherence by FUNCT_2:8;
end;
definition
let R,X;
func ADD(X,R) -> BinOp of Funcs(X,the carrier of R) means
:Def6:
for f,g being Element of Funcs(X,the carrier of R) holds
it.(f,g) = (the addF of R).:(f,g);
existence
proof
deffunc F(Element of Funcs(X,the carrier of R),
Element of Funcs(X,the carrier of R)) = (the addF of R).:($1,$2);
consider F1 being BinOp of Funcs(X,the carrier of R)
such that
A1: for x,y being Element of Funcs(X,the carrier of R)
holds F1.(x,y) = F(x,y) from BINOP_1:sch 4;
take F1;
let f,g be Element of Funcs(X,the carrier of R);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(X,the carrier of R) such that
A2: for f,g being Element of Funcs(X,the carrier of R) holds
it1.(f,g) = (the addF of R).:(f,g) and
A3: for f,g being Element of Funcs(X,the carrier of R) holds
it2.(f,g) = (the addF of R).:(f,g);
now
let f,g be Element of Funcs(X,the carrier of R);
thus it1.(f,g) = (the addF of R).:(f,g) by A2
.= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
reserve f,g,h for Element of Funcs(X,the carrier of R);
theorem Th1:
for R,X,f,g,h holds h = ADD(X,R).(f,g) iff
for x being object st x in X holds h.x = (the addF of R).(f.x,g.x)
proof
let R,X,f,g,h;
thus h = ADD(X,R).(f,g) implies
for x being object st x in X holds h.x = (the addF of R).(f.x,g.x)
proof
assume
A1: h = ADD(X,R).(f,g);
let x be object;
assume x in X; then
A2: x in dom ((the addF of R).:(f,g)) by FUNCT_2:def 1;
thus h.x = ((the addF of R).:(f,g)).x by A1,Def6
.= (the addF of R).(f.x,g.x) by A2,FUNCOP_1:22;
end;
assume
A3: for x being object st x in X holds h.x = (the addF of R).(f.x,g.x);
A5: dom (ADD(X,R).(f,g)) = X by FUNCT_2:def 1;
for x being object st x in dom h holds h.x = (ADD(X,R).(f,g)).x
proof
let x be object;
assume
B5: x in dom h; then
x in X; then
A7: x in dom ((the addF of R).:(f,g)) by FUNCT_2:def 1;
thus h.x = (the addF of R).(f.x,g.x) by A3,B5
.= ((the addF of R).:(f,g)).x by A7,FUNCOP_1:22
.= (ADD(X,R).(f,g)).x by Def6;
end;
hence h = ADD(X,R).(f,g) by FUNCT_2:def 1,A5;
end;
definition
let R,X;
let F be Function of [:the carrier of R,the carrier of R:],
the carrier of R;
let a be Element of the carrier of R;
let f be Function of X,R;
redefine func F[;](a,f) -> Element of Funcs(X, the carrier of R); :: redefines [;] (FUNCOP_1, definition)
coherence
proof
A1: dom f = X by FUNCT_2:def 1;
reconsider g = <:dom f --> a, f:> as Function of X,
[:the carrier of R, the carrier of R:] by A1,FUNCT_3:58;
F[;](a,f) = F * g;
hence thesis;
end;
end;
definition
let R,X;
func LMULT(X,R) ->
Function of [:the carrier of R,Funcs(X,the carrier of R):],
Funcs(X,the carrier of R) means
:Def7:
for a being Element of the carrier of R, f being Element of
Funcs(X,the carrier of R)
holds
for x being object st x in X holds
(it.(a,f)).x = (the multF of R).(a,f.x);
existence
proof
deffunc F(Element of the carrier of R,Element of
Funcs(X,the carrier of R)) = ((the multF of R)[;]($1,$2));
consider F1 being
Function of [:the carrier of R,Funcs(X,the carrier of R):],
Funcs(X,the carrier of R) such that
A1: for a be Element of the carrier of R,
f being Element of Funcs(X,the carrier of R) holds
F1.(a,f) = F(a,f) from BINOP_1:sch 4;
take F1;
let a be Element of the carrier of R,
f be Element of Funcs(X,the carrier of R),
x be object;
assume
A3: x in X;
A2: dom (F1.(a,f)) = X by FUNCT_2:92;
F1.(a,f) = ((the multF of R)[;](a,f)) by A1;
hence thesis by A2,A3,FUNCOP_1:32;
end;
uniqueness
proof
let it1,it2 be Function of
[:the carrier of R,Funcs(X,the carrier of R):],
Funcs(X,the carrier of R) such that
A4: for a being Element of the carrier of R,
f being Element of Funcs(X,the carrier of R) holds
for x being object st x in X holds
(it1.(a,f)).x = (the multF of R).(a,f.x) and
A5: for a being Element of the carrier of R,
f being Element of Funcs(X,the carrier of R) holds
for x being object st x in X holds
(it2.(a,f)).x = (the multF of R).(a,f.x);
for a being Element of the carrier of R,
f being Element of Funcs(X,the carrier of R) holds it1.(a,f) = it2.(a,f)
proof
let a be Element of the carrier of R,
f be Element of Funcs(X,the carrier of R);
A6: dom (it1.(a,f)) = X & dom (it2.(a,f))= X by FUNCT_2:92;
for x be object st x in dom (it1.(a,f)) holds
(it1.(a,f)).x = (it2.(a,f)).x
proof
let x be object;
assume x in dom (it1.(a,f)); then
A8: x in X by FUNCT_2:92;
hence (it1.(a,f)).x = (the multF of R).(a,f.x) by A4
.= (it2.(a,f)).x by A8,A5;
end;
hence thesis by A6;
end;
hence thesis;
end;
end;
theorem Th2:
for R,X holds
for a be Element of the carrier of R,
f,h be Element of Funcs(X, the carrier of R) holds
h = (LMULT(X,R)).(a,f) iff for x st x in X holds
h.x = (the multF of R).(a,f.x)
proof
let R,X;
let a be Element of the carrier of R,
f,h be Element of Funcs(X, the carrier of R);
(for x st x in X holds h.x = (the multF of R).(a,f.x)) implies
h = (LMULT(X,R)).(a,f)
proof
assume
A1: (for x st x in X holds h.x = (the multF of R).(a,f.x));
B2: dom h = X & dom ((LMULT(X,R)).(a,f)) = X by FUNCT_2:92;
for x st x in dom h holds h.x = (LMULT(X,R).(a,f)).x
proof
let x;
assume
A2: x in dom h;
hence h.x = (the multF of R).(a,f.x) by A1
.= ((LMULT(X,R)).(a,f)).x by A2,Def7;
end;
hence thesis by B2;
end;
hence thesis by Def7;
end;
Lm2:
(ADD(X,R)).(f,g) = (ADD(X,R)).(g,f)
proof
A0: dom ((ADD(X,R)).(f,g)) = X & dom ((ADD(X,R)).(g,f)) = X by FUNCT_2:92;
for x st x in X holds ((ADD(X,R)).(f,g)).x = ((ADD(X,R)).(g,f)).x
proof
let x;
assume
A1: x in X; then
reconsider fx = f.x, gx = g.x as Element of R by FUNCT_2:5;
((ADD(X,R)).(f,g)).x = fx + gx by A1,Th1
.= gx + fx
.= ((ADD(X,R)).(g,f)).x by Th1,A1;
hence thesis;
end;
hence thesis by A0;
end;
Lm3:
(ADD(X,R)).(f,(ADD(X,R)).(g,h)) = (ADD(X,R)).((ADD(X,R)).(f,g),h)
proof
set R1 = the carrier of R;
reconsider fg=(ADD(X,R)).(f,g), gh=(ADD(X,R)).(g,h) as Element of Funcs(X,R1);
set F1 = (ADD(X,R)).(f,gh);
set F2 = (ADD(X,R)).(fg,h);
B0: dom F1 = X & dom F2 = X by FUNCT_2:92;
for x st x in X holds F1.x = F2.x
proof
let x;
assume
A1: x in X; then
reconsider fx = f.x, gx = g.x, hx = h.x as Element of R by FUNCT_2:5;
F1.x = (the addF of R).(fx,gh.x) by A1,Th1
.= fx + (gx + hx) by A1,Th1
.= (fx + gx) + hx by RLVECT_1:def 3
.= (the addF of R).(fg.x,hx) by A1,Th1
.= F2.x by A1,Th1;
hence thesis;
end;
hence thesis by B0;
end;
Lm4:
LMULT(X,R).(a,(ADD(X,R)).(f,g))
= (ADD(X,R)).(LMULT(X,R).(a,f),LMULT(X,R).(a,g))
proof
set af = (LMULT(X,R)).(a,f), ag = (LMULT(X,R)).(a,g), fg = ADD(X,R).(f,g);
set F1 = ADD(X,R).(LMULT(X,R).(a,f),LMULT(X,R).(a,g)),
F2 = LMULT(X,R).(a,(ADD(X,R)).(f,g));
B0: dom F1 = X & dom F2 = X by FUNCT_2:92;
for x st x in X holds F1.x = F2.x
proof
let x;
assume
A0: x in X; then
reconsider fgx = fg.x as Element of R by FUNCT_2:5;
reconsider fx = f.x, gx = g.x as Element of R by A0,FUNCT_2:5;
A2: (the addF of R).((the multF of R).(a,f.x),(the multF of R).(a,g.x))
= a*fx + a*gx
.= a*(fx+gx) by VECTSP_1:def 7
.= a*fgx by A0,Th1;
A5: a*fx = (af).x by A0,Th2;
a*gx = (ag).x by A0,Th2; then
F1.x = a*fgx by A2,A5,A0,Th1
.= ((LMULT(X,R)).(a,fg)).x by A0,Th2;
hence thesis;
end;
hence thesis by B0;
end;
::scalar-distributive (a + b) * v = a * v + b * v
Lm5:
LMULT(X,R).(a+b,f) = (ADD(X,R)).(LMULT(X,R).(a,f),LMULT(X,R).(b,f))
proof
set af = (LMULT(X,R)).(a,f), bf =(LMULT(X,R)).(b,f);
set F1 = LMULT(X,R).(a+b,f), F2=ADD(X,R).(LMULT(X,R).(a,f),LMULT(X,R).(b,f));
B0: dom F1 = X & dom F2 = X by FUNCT_2:92;
for x st x in X holds F1.x = F2.x
proof
let x;
assume
A0: x in X; then
reconsider fx = f.x as Element of R by FUNCT_2:5;
B1: a*fx = (af).x by A0,Th2;
B2: b*fx = (bf).x by A0,Th2;
F1.x = (a+b)*fx by A0,Th2
.= a*fx + b*fx by VECTSP_1:def 7
.= ((ADD(X,R)).(af,bf)).x by A0,Th1,B1,B2;
hence thesis;
end;
hence thesis by B0;
end;
Lm6:
LMULT(X,R).(a*b,f) = LMULT(X,R).(a,LMULT(X,R).(b,f))
proof
set bf =(LMULT(X,R)).(b,f);
B0: dom (LMULT(X,R).(a*b,f)) = X & dom( LMULT(X,R).(a,LMULT(X,R).(b,f))) = X
by FUNCT_2:92;
for x st x in X holds
(LMULT(X,R).(a*b,f)).x = (LMULT(X,R).(a,LMULT(X,R).(b,f))).x
proof
let x;
assume
A0: x in X; then
reconsider fx = f.x as Element of R by FUNCT_2:5;
B1: b*fx = (bf).x by A0,Th2;
(LMULT(X,R).(a*b,f)).x = (a*b)*fx by A0,Th2
.= a*(b*fx) by GROUP_1:def 3
.= (LMULT(X,R).(a,bf)).x by B1,A0,Th2;
hence thesis;
end;
hence thesis by B0;
end;
Lm7:
LMULT(X,R).(1.R,f) = f
proof
B0: dom (LMULT(X,R).(1.R,f)) = X & dom f = X by FUNCT_2:92;
for x st x in X holds (LMULT(X,R).(1.R,f)).x = f.x
proof
let x;
assume
A0: x in X; then
reconsider fx = f.x as Element of R by FUNCT_2:5;
(LMULT(X,R).(1.R,f)).x = 1.R*(fx) by A0,Th2 .= f.x;
hence thesis;
end;
hence thesis by B0;
end;
definition
let R,X;
func fs_Funcs(X,R) -> Subset of Funcs(X,the carrier of R) equals
{x where x is Function of X,the carrier of R : x is finite-Support};
coherence
proof
set M = {x where x is Function of X,the carrier of R : x is finite-Support};
M c= Funcs(X,the carrier of R)
proof
let o be object;
assume o in M; then
consider x being Function of X,the carrier of R such that
A1: o = x & x is finite-Support;
thus thesis by A1,FUNCT_2:8;
end;
hence thesis;
end;
end;
Lm8: 0_Funcs(X,R) is finite-Support & Support 0_Funcs(X,R) = {}
proof
Support 0_Funcs(X,R) = {}
proof
assume Support 0_Funcs(X,R) <> {}; then
consider x be object such that
A2: x in Support 0_Funcs(X,R) by XBOOLE_0:def 1;
A3: x in dom 0_Funcs(X,R) by A2,POLYNOM1:def 3;
(0_Funcs(X,R)).x = 0.R by A3,FUNCOP_1:7;
hence contradiction by A2,POLYNOM1:def 3;
end;
hence thesis by POLYNOM1:def 5;
end;
Lm9:
0_Funcs(X,R) in fs_Funcs(X,R)
proof
0_Funcs(X,R) is Function of X,the carrier of R
& 0_Funcs(X,R) is finite-Support by Lm8;
hence thesis;
end;
registration
let R,X;
cluster fs_Funcs(X,R) -> non empty;
coherence by Lm9;
end;
Lm10:
Support (X --> 0.R) = {}
proof
set f = X --> 0.R;
assume Support f <> {}; then
consider x be object such that
A2: x in Support f by XBOOLE_0:def 1;
A3: x in dom f by A2,POLYNOM1:def 3;
f.x = 0.R by A3,FUNCOP_1:7;
hence contradiction by A2,POLYNOM1:def 3;
end;
registration
let R,X;
cluster finite-Support for Function of X,the carrier of R;
existence
proof
reconsider f = X --> 0.R as Function of X,the carrier of R;
take f;
Support f = {} by Lm10;
hence thesis by POLYNOM1:def 5;
end;
end;
theorem Th3:
for f,g be finite-Support Function of X,the carrier of R holds
ADD(X,R).[f,g] is finite-Support Function of X,the carrier of R
proof
let f,g be finite-Support Function of X,the carrier of R;
reconsider f1 = f, g1 = g as Element of Funcs(X, the carrier of R)
by FUNCT_2:8;
reconsider h = ADD(X,R).(f1,g1) as Element of Funcs(X, the carrier of R);
for o be object st o in Support h holds o in Support f1 \/ Support g1
proof
let o be object;
assume
A1: o in Support h;
set x = o;
A2: x in dom h by A1,POLYNOM1:def 3;
A3: dom h = X by FUNCT_2:def 1;
A4: dom f1 = X & dom g1 = X by FUNCT_2:def 1;
assume not o in Support f1 \/ Support g1; then
not x in Support f1 & not x in Support g1 by XBOOLE_0:def 3; then
A6: f1.x = 0.R & g1.x = 0.R by A2,A4,POLYNOM1:def 3;
A8: x in dom ((the addF of R).:(f1,g1)) by A2,A3,FUNCT_2:def 1;
h.x = ((the addF of R).:(f1,g1)).x by Def6
.= 0.R + 0.R by A6,A8,FUNCOP_1:22
.= 0.R;
hence contradiction by A1,POLYNOM1:def 3;
end; then
A5: Support h c= Support f1 \/ Support g1;
Support f1 is finite & Support g1 is finite by POLYNOM1:def 5;
hence thesis by A5,POLYNOM1:def 5;
end;
Lm11:
for f,g being Element of Funcs(X,the carrier of R)
st f in fs_Funcs(X,R) & g in fs_Funcs(X,R) holds
ADD(X,R).[f,g] in fs_Funcs(X,R)
proof
let f,g be Element of Funcs(X,the carrier of R);
assume
A1: f in fs_Funcs(X,R) & g in fs_Funcs(X,R); then
consider f1 be Function of X,the carrier of R such that
A2: f1 = f & f1 is finite-Support;
consider g1 be Function of X,the carrier of R such that
A3: g1 = g & g1 is finite-Support by A1;
ADD(X,R).[f,g] is finite-Support Function of X,the carrier of R
by Th3,A3,A2;
hence thesis;
end;
theorem Th4:
for a be Element of the carrier of R,
g be finite-Support Function of X,the carrier of R holds
LMULT(X,R).(a,g) is finite-Support Function of X,the carrier of R
proof
let a be Element of the carrier of R,
g be finite-Support Function of X,the carrier of R;
reconsider g as Element of Funcs(X, the carrier of R) by FUNCT_2:8;
reconsider F = LMULT(X,R).(a,g) as Element of Funcs(X, the carrier of R);
B1: dom F = X & dom g = X by FUNCT_2:def 1;
A1: Support g is finite by POLYNOM1:def 5;
for o be object st o in Support F holds o in Support g
proof
let o be object;
assume
A2: o in Support F; then
A3: o in dom F by POLYNOM1:def 3; then
reconsider x = o as Element of X;
reconsider gx = g.x as Element of R by A3,FUNCT_2:5;
F.x <> 0.R by A2,POLYNOM1:def 3; then
a*(gx) <> 0.R by A3,Th2; then
g.x <> 0.R;
hence thesis by A3,B1,POLYNOM1:def 3;
end; then
Support F c= Support g;
hence thesis by A1,POLYNOM1:def 5;
end;
reserve f,g,h for Element of fs_Funcs(X,R);
Lm12:
for a being Element of R
for f being Element of Funcs(X,the carrier of R) st f in fs_Funcs(X,R)
holds LMULT(X,R).(a,f) in fs_Funcs(X,R)
proof
let a be Element of R;
let f be Element of Funcs(X,the carrier of R);
assume f in fs_Funcs(X,R); then
consider f1 being Function of X,the carrier of R such that
A2: f1 = f & f1 is finite-Support;
LMULT(X,R).(a,f) is finite-Support Function of X,the carrier of R
by A2,Th4;
hence thesis;
end;
:: Construct the Module
definition
let X be non empty set;
let Y be non empty addLoopStr;
func FuncAdd(X,Y) -> BinOp of Funcs(X,the carrier of Y) means
for f,g being Element of Funcs(X,the carrier of Y)
holds it.(f,g) = (the addF of Y).:(f,g);
existence
proof
deffunc F(Element of Funcs(X,the carrier of Y), Element of Funcs(X,the
carrier of Y)) = (the addF of Y).:($1,$2);
thus ex ad being BinOp of Funcs(X,the carrier of Y) st
for f,g being Element of Funcs(X,the carrier of Y)
holds ad.(f,g) = F(f,g) from BINOP_1:sch 4;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(X,the carrier of Y) such that
A1: for f,g being Element of Funcs(X,the carrier of Y) holds it1.(f,g)
= (the addF of Y).:(f,g) and
A2: for f,g being Element of Funcs(X,the carrier of Y) holds it2.(f,g)
= (the addF of Y).:(f,g);
now
let f,g be Element of Funcs(X,the carrier of Y);
thus it1.(f,g) = (the addF of Y).:(f,g) by A1
.= it2.(f,g) by A2;
end;
hence thesis;
end;
end;
definition
let R,X;
func fs_ADD(X,R) -> BinOp of fs_Funcs(X,R) equals
ADD(X,R)|[:fs_Funcs(X,R), fs_Funcs(X,R):];
coherence
proof
set V = Funcs(X,the carrier of R);
set V1 = fs_Funcs(X,R);
A1: for z be object st z in [:V1,V1:] holds (ADD(X,R)|[:V1,V1:]).z in V1
proof
let z be object;
assume
A2: z in [:V1,V1:];
then consider f,g be object such that
A3: f in V1 & g in V1 and
A4: z = [f,g] by ZFMISC_1:def 2;
reconsider g1 = g,f1 = f as Element of V by A3;
[f,g] in dom(ADD(X,R)|[:V1,V1:]) by FUNCT_2:def 1,A2,A4; then
(ADD(X,R)|[:V1,V1:]).z = (ADD(X,R)).(f1,g1) by A4,FUNCT_1:47;
hence thesis by A3,Lm11;
end;
dom(ADD(X,R)|[:V1,V1:]) =[:V1,V1:] by FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let R,X;
func fs_LMULT(X,R) ->
Function of [:the carrier of R,fs_Funcs(X,R):], fs_Funcs(X,R) equals
(LMULT(X,R))|[:the carrier of R,fs_Funcs(X,R):];
coherence
proof
set CR = the carrier of R, V = Funcs(X,the carrier of R),
V1 = fs_Funcs(X,R);
A1: dom(LMULT(X,R)) = [:CR,V:] by FUNCT_2:def 1;
A2: for z be object st z in [:CR,V1:] holds ((LMULT(X,R))|[:CR,V1:]).z in V1
proof
let z be object;
assume
A3: z in [:CR,V1:];
then consider a,g be object such that
A4: a in CR & g in V1 and
A5: z=[a,g] by ZFMISC_1:def 2;
reconsider a1=a as Element of the carrier of R by A4;
reconsider g1=g as Element of V by A4;
[a1,g1] in dom((LMULT(X,R))|[:CR,V1:])
by A1,A3,A5,RELAT_1:62,ZFMISC_1:96; then
((LMULT(X,R))|[:CR,V1:]).z = (LMULT(X,R)).(a1,g1) by A5,FUNCT_1:47;
hence thesis by A4,Lm12;
end;
dom((LMULT(X,R))|[:CR,V1:]) =[:CR,V1:] by A1,RELAT_1:62,ZFMISC_1:96;
hence thesis by A2,FUNCT_2:3;
end;
end;
definition
let R,X;
func 0_fs_Zero(X,R) -> Element of fs_Funcs(X,R) equals
0_Funcs(X,R);
correctness
proof
set M = {x where x is Function of X,the carrier of R : x is finite-Support};
0_Funcs(X,R) is Function of X,the carrier of R
& 0_Funcs(X,R) is finite-Support by Lm8; then
0_Funcs(X,R) in M;
hence thesis;
end;
end;
::$N The structure $\mathrm{FS\_Funcs}(X,R)$ forms a left $R$-module.
definition
let R,X;
func FS_Funcs(X,R) -> non empty ModuleStr over R equals
ModuleStr(# fs_Funcs(X,R), fs_ADD(X,R), 0_fs_Zero(X,R), fs_LMULT(X,R) #);
coherence;
end;
Lm13:
for f be Element of Funcs(X,the carrier of R) holds
(ADD(X,R)).(f,0_Funcs(X,R)) = f
proof
let f be Element of Funcs(X,the carrier of R);
set F1 = (ADD(X,R)).(f,0_Funcs(X,R));
B1: dom F1 = X & dom f = X by FUNCT_2:def 1;
for x st x in X holds F1.x = f.x
proof
let x;
assume
A0: x in X; then
reconsider fx = f.x, y = (X --> 0.R).x as Element of R by FUNCT_2:5;
F1.x = fx + y by A0,Th1 .= fx + 0.R by A0,FUNCOP_1:7;
hence thesis;
end;
hence thesis by B1;
end;
Lm14:
for f be Element of Funcs(X,the carrier of R) holds
(ADD(X,R)).(f,LMULT(X,R).(-1.R,f)) = 0_Funcs(X,R)
proof
let f be Element of Funcs(X,the carrier of R);
set g = (LMULT(X,R)).(-1.R,f), F1 = ADD(X,R).(f,g);
B1: dom F1 = X & dom g = X by FUNCT_2:92;
for x st x in X holds F1.x = 0_Funcs(X,R).x
proof
let x;
assume
A0: x in X; then
reconsider fx = f.x as Element of R by FUNCT_2:5;
(-1.R)*fx = -(1.R*fx) by VECTSP_1:9 .= -fx; then
g.x = -fx by A0,Th2; then
F1.x = fx + (-fx) by A0,Th1
.= 0.R by RLVECT_1:5
.=(0_Funcs(X,R)).x by A0,FUNCOP_1:7;
hence thesis;
end;
hence thesis by B1;
end;
theorem Th5:
for v1,w1 be Element of Funcs(X,the carrier of R),
v,w be Element of FS_Funcs(X,R) st v1=v & w1= w holds
v + w = (ADD(X,R)).(v1,w1)
proof
let v1,w1 be Element of Funcs(X,the carrier of R),
v,w be Element of FS_Funcs(X,R);
set V1 = fs_Funcs(X,R);
assume
A1: v1=v & w1=w;
[v,w] in [:V1,V1:]; then
[v,w] in dom(ADD(X,R)|[:V1,V1:]) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:47;
end;
Lm15:
for a be Element of R, f1 be Element of Funcs(X,the carrier of R),
f be Element of FS_Funcs(X,R) st f1=f holds a*f = (LMULT(X,R)).(a,f1)
proof
let a be Element of R, f1 be Element of Funcs(X,the carrier of R),
f be Element of FS_Funcs(X,R);
set V1 = fs_Funcs(X,R);
set CR = the carrier of R;
assume
A1: f1=f;
[a,f] in [:CR,V1:];
hence thesis by A1,FUNCT_1:49;
end;
theorem Th6:
FS_Funcs(X,R) is LeftMod of R
proof
set V1 = fs_Funcs(X,R);
A1: FS_Funcs(X,R) is Abelian
proof
let v, w be Element of FS_Funcs(X,R);
v in fs_Funcs(X,R) & w in fs_Funcs(X,R); then
reconsider v1=v, w1=w as Element of Funcs(X,the carrier of R);
[v,w] in [:V1,V1:]; then
A2: [v,w] in dom(ADD(X,R)|[:V1,V1:]) by FUNCT_2:def 1;
[w,v] in [:V1,V1:]; then
A3: [w,v] in dom(ADD(X,R)|[:V1,V1:]) by FUNCT_2:def 1;
v + w = (ADD(X,R)).(v1,w1) by A2,FUNCT_1:47
.= (ADD(X,R)).(w1,v1) by Lm2
.= w + v by A3,FUNCT_1:47;
hence thesis;
end;
A4: FS_Funcs(X,R) is add-associative
proof
let f, g, h be Element of FS_Funcs(X,R);
f in fs_Funcs(X,R) & g in fs_Funcs(X,R) & h in fs_Funcs(X,R); then
reconsider f1 = f, g1 = g, h1 = h as Element of Funcs(X,the carrier of R);
A5: g + h = (ADD(X,R)).(g1,h1) by Th5;
f + g = (ADD(X,R)).(f1,g1) by Th5; then
(f + g) + h = (ADD(X,R)).((ADD(X,R)).(f1,g1), h1) by Th5
.= (ADD(X,R)).(f1,(ADD(X,R)).(g1,h1)) by Lm3
.= f + (g + h) by A5,Th5;
hence thesis;
end;
A6: FS_Funcs(X,R) is right_zeroed
proof
let f be Element of FS_Funcs(X,R);
reconsider f1 = f as Element of Funcs(X,the carrier of R) by TARSKI:def 3;
f + 0.FS_Funcs(X,R) = (ADD(X,R)).(f1, 0_Funcs(X,R)) by Th5
.= f1 by Lm13;
hence thesis;
end;
A7: FS_Funcs(X,R) is right_complementable
proof
let f be Element of FS_Funcs(X,R);
reconsider f1=f as Element of Funcs(X,the carrier of R) by TARSKI:def 3;
reconsider r = -1.R as Element of R;
r*f = (LMULT(X,R)).(r,f1) by Lm15; then
f + r*f = (ADD(X,R)).(f1, (LMULT(X,R)).(r,f1)) by Th5
.= 0.FS_Funcs(X,R) by Lm14;
hence thesis;
end;
A8: FS_Funcs(X,R) is vector-distributive
proof
let a be Element of R; let v,w be Element of FS_Funcs(X,R);
v in FS_Funcs(X,R) & w in FS_Funcs(X,R);
then
reconsider v1=v,w1=w as Element of Funcs(X,the carrier of R);
A9: v+w = (ADD(X,R)).(v1,w1) by Th5;
A10: a*v = (LMULT(X,R)).(a,v1) & a*w = (LMULT(X,R)).(a,w1) by Lm15;
a*(v+w) = (LMULT(X,R)).(a,(ADD(X,R)).(v1,w1)) by A9,Lm15
.= (ADD(X,R)).(LMULT(X,R).(a,v1),LMULT(X,R).(a,w1)) by Lm4
.= a*v + a*w by A10,Th5;
hence thesis;
end;
A11: FS_Funcs(X,R) is scalar-distributive
proof
let a,b be Element of R;
let f be Element of FS_Funcs(X,R);
f in FS_Funcs(X,R); then
reconsider f1=f as Element of Funcs(X,the carrier of R);
A12: a*f = (LMULT(X,R)).(a,f1) & b*f = (LMULT(X,R)).(b,f1) by Lm15;
(a+b)*f = (LMULT(X,R)).(a+b,f1) by Lm15
.= (ADD(X,R)).((LMULT(X,R)).(a,f1), (LMULT(X,R)).(b,f1)) by Lm5
.= a*f + b*f by A12,Th5;
hence thesis;
end;
A13: FS_Funcs(X,R) is scalar-associative
proof
let a,b be Element of R;
let f be Element of FS_Funcs(X,R);
f in FS_Funcs(X,R); then
reconsider f1=f as Element of Funcs(X,the carrier of R);
A14: (a*b)*f = (LMULT(X,R)).(a*b,f1) & b*f = (LMULT(X,R)).(b,f1) by Lm15;
(a*b)*f = (LMULT(X,R)).(a*b,f1) by Lm15
.=(LMULT(X,R)).(a,LMULT(X,R).(b,f)) by Lm6
.=a*(b*f) by A14,Lm15;
hence thesis;
end;
FS_Funcs(X,R) is scalar-unital
proof
let f be Element of FS_Funcs(X,R);
f in FS_Funcs(X,R); then
reconsider f1=f as Element of Funcs(X,the carrier of R);
1.R*f = (LMULT(X,R)).(1.R,f1) by Lm15 .= f by Lm7;
hence thesis;
end;
hence thesis by A1,A4,A6,A7,A8,A11,A13;
end;
registration
let R,X;
cluster FS_Funcs(X,R) -> Abelian add-associative right_zeroed left_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Th6;
end;
::$N The definition of Free Module $\mathcal{F}_{\mathrm{LMod}}(X)$
definition
let R,X;
func Free_LMod(X,R) -> non empty ModuleStr over R equals
FS_Funcs(X,R);
coherence;
end;
registration
let R,X;
cluster Free_LMod(X,R) ->
Abelian add-associative right_zeroed left_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence;
end;
begin :: Basis map and reconstruction
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Throughout this section, we assume that X is non empty.
:: The case X = {} is treated separately in the final section.
:: From this point onward, we also assume that R is non degenerated.
:: This assumption is essential for the basis construction below:
:: the equality Support iota(x,R) = {x} relies on
:: (iota(x,R)).x = 1.R <> 0.R.
:: Over a degenerated ring, every left module is trivial, and
:: IotaMap(X,R) is not one-to-one when card X >= 2.
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve X for non empty set;
reserve R for non degenerated Ring;
reserve M,N for LeftMod of R;
definition
let R,X;
let f be Element of Free_LMod(X,R);
func ~f -> Element of fs_Funcs(X,R) equals
f;
coherence;
end;
definition
let R,X;
let f be Element of Free_LMod(X,R);
func @f -> Element of Funcs(X,the carrier of R) equals
f;
coherence
proof
f in {x where x is Function of X,the carrier of R : x is finite-Support};
then
consider f1 be Function of X,the carrier of R such that
A1: f1 = f & f1 is finite-Support;
thus thesis by A1,FUNCT_2:8;
end;
end;
::$N the canonical generator $\iota_X(x)$
definition
let X,R;
let a be Element of X;
func iota(a,R) -> Function of X, [#]R means
:Def17:
for x being object st x in X holds
(x = a implies it.x = 1.R) & (x <> a implies it.x = 0.R);
existence
proof
defpred P[object,object] means ($1 = a implies $2 = 1.R) &
(not $1 = a implies $2 = 0.R);
A1: for x being object st x in X ex y being object st y in [#]R & P[x,y]
proof
let x be object;
assume x in X;
per cases;
suppose
A2: x = a;
take y = 1.R;
thus thesis by A2;
end;
suppose
A3: x <> a;
take y = 0.R;
thus thesis by A3;
end;
end;
consider f be Function of X, [#]R such that
A4: for x being object st x in X holds P[x,f.x] from FUNCT_2:sch 1(A1);
take f;
thus thesis by A4;
end;
uniqueness
proof
let f1,f2 be Function of X,[#]R such that
A5: for x being object st x in X holds (x = a implies f1.x = 1.R) &
(x <> a implies f1.x = 0.R) and
A6: for x being object st x in X holds (x = a implies f2.x = 1.R) &
(x <> a implies f2.x = 0.R);
for x being object st x in X holds f1.x=f2.x
proof
let x be object;
assume x in X; then
A7: x <> a implies f1.x = 0.R & f2.x = 0.R by A5,A6;
x = a implies f1.x = 1.R & f2.x = 1.R by A5,A6;
hence thesis by A7;
end;
hence thesis;
end;
end;
registration
let X,R;
let a be Element of X;
cluster iota(a,R) -> (the carrier of R)-valued;
coherence;
end;
Lm16:
for R be non degenerated Ring, X be non empty set, z be Element of X
holds Support(iota(z,R)) = {z}
proof
let R be non degenerated Ring, X be non empty set,
z be Element of X;
thus Support(iota(z,R)) c= {z}
proof
let o be object;
assume
A2: o in Support iota(z,R); then
A3: (iota(z,R)).o <> 0.R by POLYNOM1:def 3;
assume not o in {z}; then
A5: o <> z by TARSKI:def 1;
o in dom iota(z,R) by A2,POLYNOM1:def 3;
hence contradiction by A3,A5,Def17;
end;
let o be object;
assume
A7: o in {z}; then
A8: o = z by TARSKI:def 1;
A9: dom (iota(z,R)) = X by FUNCT_2:def 1;
(iota(z,R)).o = 1.R by A8,Def17; then
(iota(z,R)).o <> 0.R;
hence thesis by A7,A9,POLYNOM1:def 3;
end;
Lm17:
for R be non degenerated Ring, X be non empty set, x be Element of X holds
iota(x,R) in fs_Funcs(X,R) &
iota(x,R) is finite-Support Function of X,the carrier of R
proof
let R be non degenerated Ring, X be non empty set,
x be Element of X;
set f = iota(x,R);
Support f = {x} by Lm16; then
f is finite-Support Function of X,the carrier of R by POLYNOM1:def 5;
hence thesis;
end;
registration
let X,R;
let a be Element of X;
cluster iota(a,R) -> finite-Support;
coherence by Lm17;
end;
definition
let R,X;
let x be Element of X;
func Iota(x,R) -> Element of Free_LMod(X,R) equals
iota(x,R);
coherence by Lm17;
end;
::$N the induced injection $\iota_X : X \longrightarrow \mathcal{F}_{\mathrm{LMod}}(X)$
definition
let R,X;
func IotaMap(X,R) -> Function of X, Free_LMod(X,R) means :Def19:
for x be Element of X holds it.x = Iota(x,R);
existence
proof
defpred P[Element of X, Element of Free_LMod(X,R)] means
$2 = Iota($1,R);
A1: for x being Element of X ex y being Element of Free_LMod(X,R) st P[x,y];
consider F being Function of X,Free_LMod(X,R) such that
A2: for x being Element of X holds P[x,F.x]
from FUNCT_2:sch 3(A1);
take F;
let x be Element of X;
thus thesis by A2;
end;
uniqueness
proof
let s,t be Function of X,Free_LMod(X,R);
assume that
A3: for x be Element of X holds s.x = Iota(x,R) and
A4: for x be Element of X holds t.x = Iota(x,R);
now
let x be Element of X;
s.x = Iota(x,R) by A3;
hence s.x = t.x by A4;
end;
hence thesis;
end;
end;
registration
let R,X;
cluster IotaMap(X,R) -> one-to-one;
coherence
proof
set f = IotaMap(X,R);
for o1, o2 being object st o1 in dom f & o2 in dom f & f.o1 = f.o2 holds
o1 = o2
proof
let o1, o2 be object;
assume
A1: o1 in dom f & o2 in dom f & f.o1 = f.o2; then
reconsider x1 = o1, x2 = o2 as Element of X;
assume
A2: o1 <> o2;
A3: Iota(x1,R) = f.o2 by A1,Def19 .= Iota(x2,R) by Def19;
1.R = (iota(x2,R)).x1 by A3,Def17
.= 0.R by A2,Def17;
hence contradiction;
end;
hence thesis;
end;
end;
definition
let R,X;
let x be Element of X;
func ev_(x,R) -> Function of Free_LMod(X,R), R means :Def20:
for f be Element of Free_LMod(X,R) holds it.f = @f.x;
existence
proof
defpred P[Element of Free_LMod(X,R), Element of R] means
$2 = @($1).x;
A1: for f being Element of Free_LMod(X,R) ex y being Element of R st P[f,y];
consider F being Function of Free_LMod(X,R), R such that
A2: for f being Element of Free_LMod(X,R) holds P[f,F.f]
from FUNCT_2:sch 3(A1);
take F;
let f be Element of Free_LMod(X,R);
thus thesis by A2;
end;
uniqueness
proof
let s,t be Function of Free_LMod(X,R), R;
assume that
A3: for f be Element of Free_LMod(X,R) holds s.f = @f.x and
A4: for f be Element of Free_LMod(X,R) holds t.f = @f.x;
now
let f be Element of Free_LMod(X,R);
s.f = @f.x by A3;
hence s.f = t.f by A4;
end;
hence thesis;
end;
end;
definition
let X,R;
let f be Element of Free_LMod(X,R);
func ev_iota(f) -> Function of X, Free_LMod(X,R) means :Def21:
for x be Element of X holds it.x = (ev_(x,R).f)*(IotaMap(X,R).x);
existence
proof
defpred P[Element of X, Element of Free_LMod(X,R)] means
$2 = (ev_($1,R).f)*(IotaMap(X,R).$1);
A1: for x being Element of X ex y being Element of Free_LMod(X,R) st P[x,y];
consider F being Function of X,Free_LMod(X,R) such that
A2: for x being Element of X holds P[x,F.x]
from FUNCT_2:sch 3(A1);
take F;
let x be Element of X;
thus thesis by A2;
end;
uniqueness
proof
let s,t be Function of X,Free_LMod(X,R);
assume that
A3: for x be Element of X holds s.x = (ev_(x,R).f)*(IotaMap(X,R).x) and
A4: for x be Element of X holds t.x = (ev_(x,R).f)*(IotaMap(X,R).x);
now
let x be Element of X;
s.x = (ev_(x,R).f)*(IotaMap(X,R).x) by A3;
hence s.x = t.x by A4;
end;
hence thesis;
end;
end;
registration
let X,R;
let f be Element of Free_LMod(X,R);
cluster Support @f -> finite for set;
coherence
proof
f in {x where x is Function of X,the carrier of R : x is finite-Support};
then
consider f1 be Function of X,the carrier of R such that
A1: f1 = f & f1 is finite-Support;
thus thesis by A1,POLYNOM1:def 5;
end;
end;
registration
let X,R;
cluster 0.Free_LMod(X,R) -> zero;
coherence;
cluster non zero for Element of Free_LMod(X,R);
existence
proof
consider o be object such that
A1: o in X by XBOOLE_0:def 1;
reconsider x = o as Element of X by A1;
reconsider f = Iota(x,R) as Element of Free_LMod(X,R);
reconsider f1 = f as Function of X, the carrier of R;
A2: Support f1 = {x} by Lm16;
take f;
thus thesis by Lm10,A2;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: We introduce the indexing constructions idxseq and F_idxseq
:: to represent finite formal sums by finite sequences:
:: idxseq(f) = canFS(Support @f) the support as a finite sequence
:: F_idxseq(f) = the FinSequence with
:: F_idxseq(f).i = (ev_(x,R).f) * Iota(x,R) where x = idxseq(f).i
:: f = Sum F_idxseq(f) :: reconstruction, see Th15
:: (the numbering supports the proofs by induction on the length of
:: the sequence.)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let X,R;
let f be Element of Free_LMod(X,R);
func idxseq(f) -> FinSequence of X equals
canFS (Support @f);
coherence
proof
rng canFS(Support @f) c= X by XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
end;
Lm18:
for f be Element of Free_LMod(X,R), x be Element of X holds
x in Support @f iff ev_(x,R).f <> 0.R
proof
let f be Element of Free_LMod(X,R), x be Element of X;
A1: x in Support @f implies ev_(x,R).f <> 0.R
proof
assume
A2: x in Support @f;
ev_(x,R).f = @f.x by Def20;
hence thesis by A2,POLYNOM1:def 4;
end;
ev_(x,R).f <> 0.R implies x in Support @f
proof
assume
A3: ev_(x,R).f <> 0.R;
ev_(x,R).f = @f.x by Def20;
hence thesis by A3,POLYNOM1:def 4;
end;
hence thesis by A1;
end;
theorem
for f be Element of Free_LMod(X,R) holds
Support ev_iota(f) = Support @f
proof
let f be Element of Free_LMod(X,R);
thus Support ev_iota(f) c= Support @f
proof
let o be object;
assume
A2: o in Support ev_iota(f); then
reconsider x = o as Element of X;
assume
A3: not o in Support @f;
reconsider gx = (IotaMap(X,R)).x as Element of Free_LMod(X,R);
(ev_iota(f)).x = (ev_(x,R).f)*(IotaMap(X,R).x) by Def21
.= (@f.x)*gx by Def20
.= 0.R*gx by A3,POLYNOM1:def 4
.= 0.Free_LMod(X,R) by VECTSP_1:14;
hence contradiction by A2,POLYNOM1:def 4;
end;
let o be object;
assume
A4: o in Support @f; then
reconsider x = o as Element of X;
reconsider r = ev_(x,R).f as Element of the carrier of R;
reconsider u = Iota(x,R) as Element of Free_LMod(X,R);
reconsider v = (ev_iota(f)).x as Element of Free_LMod(X,R);
A5: @u.x = 1.R by Def17;
A6: [r,u] in [:the carrier of R,fs_Funcs(X,R):];
v = (ev_(x,R).f)*(IotaMap(X,R).x) by Def21
.= fs_LMULT(X,R).(r,u) by Def19; then
@v.x = (LMULT(X,R).(r,u)).x by A6,FUNCT_1:49 .= r*(@u.x) by Def7
.= r by A5; then
@v <> 0.Free_LMod(X,R) by A4,Lm18;
hence thesis by POLYNOM1:def 4;
end;
Lm20:
for R be non degenerated Ring, X be non empty set, x be Element of X
holds ev_(x,R).(iota(x,R)) = 1.R
proof
let R be non degenerated Ring, X be non empty set, x be Element of X;
ev_(x,R).(iota(x,R)) = @(Iota(x,R)).x by Def20
.= 1.R by Def17;
hence thesis;
end;
Lm21:
for R be non degenerated Ring, X be non empty set, x,y be Element of X
st x <> y holds ev_(x,R).(iota(y,R)) = 0.R
proof
let R be non degenerated Ring, X be non empty set, x,y be Element of X;
assume
A1: x <> y;
ev_(x,R).(iota(y,R)) = @(Iota(y,R)).x by Def20
.= 0.R by Def17,A1;
hence thesis;
end;
definition
let X,R;
let s be FinSequence of the carrier of Free_LMod(X,R), x be Element of X;
func ev_(s,x) -> FinSequence of the carrier of R means
:Def23:
dom it = dom s & for i be Nat st i in dom s holds it.i = ev_(x,R).(s/.i);
existence
proof
deffunc F(Nat) = ev_(x,R).(s/.$1);
ex z being FinSequence of the carrier of R
st len z = len s & for j being Nat st j in dom z holds
z.j = F(j) from FINSEQ_2:sch 1; then
consider z being FinSequence of the carrier of R such that
A1: len z = len s and
A2: for j being Nat st j in dom z holds z.j = F(j);
take z;
thus dom z = dom s by A1,FINSEQ_3:29;
hence thesis by A2;
end;
uniqueness
proof
let it1, it2 be FinSequence of the carrier of R such that
A3: dom it1 = dom s and
A4: for i being Nat st i in dom s holds it1.i = ev_(x,R).(s/.i) and
A5: dom it2 = dom s and
A6: for j being Nat st j in dom s holds it2.j = ev_(x,R).(s/.j);
for n being Nat st n in dom it1 holds it1.n = it2.n
proof
let n be Nat;
assume
A7: n in dom it1;
reconsider n as Element of NAT by ORDINAL1:def 12;
it1.n = ev_(x,R).(s/.n) by A3,A4,A7 .= it2.n by A3,A6,A7;
hence thesis;
end;
hence thesis by A3,A5;
end;
end;
theorem Th7:
for x be Element of X, f be Element of Free_LMod(X,R), a be Element of R
holds @(a*f).x = a*@f.x
proof
let x be Element of X, f be Element of Free_LMod(X,R), a be Element of R;
@(a*f).x = ((LMULT(X,R)).(a,@f)).x by Lm15
.= a*(@f.x) by Th2;
hence thesis;
end;
theorem Th8:
for x be Element of X, f,g be Element of Free_LMod(X,R) holds
@(f+g).x = @f.x + @g.x &
ev_(x,R).(f+g) = ev_(x,R).f + ev_(x,R).g
proof
let x be Element of X, f,g be Element of Free_LMod(X,R);
A1: @(f + g).x = ((ADD(X,R)).(@f,@g)).x by Th5
.= @f.x + @g.x by Th1;
@f.x = ev_(x,R).f & @g.x = ev_(x,R).g by Def20;
hence thesis by A1,Def20;
end;
Lm22:
for R be non degenerated Ring, X be non empty set, x be Element of X,
a be Element of R, f be Element of Free_LMod(X,R)
holds ev_(x,R).(a * f) = a * ev_(x,R).f
proof
let R be non degenerated Ring, X be non empty set, x be Element of X,
a be Element of R, f be Element of Free_LMod(X,R);
ev_(x,R).(a*f) = @(a*f).x by Def20
.= a * (@f.x) by Th7
.= a * ev_(x,R).f by Def20;
hence thesis;
end;
theorem Th9:
for x being Element of X holds ev_(x,R).(0.Free_LMod(X,R)) = 0.R
proof
let x be Element of X;
ev_(x,R).(0.Free_LMod(X,R)) = @(0.Free_LMod(X,R)).x by Def20
.= 0.R;
hence thesis;
end;
theorem Th10:
for N0 be Nat, F be FinSequence of the carrier of Free_LMod(X,R),
x be Element of X st len F = N0+1 holds
ev_(F,x) = (ev_(F|N0,x))^<*ev_(x,R).(F/.(len F))*>
proof
let N0 be Nat, F be FinSequence of the carrier of Free_LMod(X,R),
x be Element of X;
assume
A1: len F = N0+1; then
A2: dom F = Seg(N0+1) by FINSEQ_1:def 3; then
A3: Seg (N0+1) = dom ev_(F,x) by Def23
.= Seg len ev_(F,x) by FINSEQ_1:def 3;
A4: N0+1 = len((F|N0)^<*F/.(len F)*>) by A1,FINSEQ_5:21
.= len (F|N0) + 1 by FINSEQ_2:16;
A5: Seg len ev_(F|N0,x) = dom ev_(F|N0,x) by FINSEQ_1:def 3
.= dom (F|N0) by Def23 .= Seg N0 by A4,FINSEQ_1:def 3; then
A6: len ev_(F|N0,x) = N0 by FINSEQ_1:6;
len <*ev_(x,R).(F/.(len F))*> = 1 by FINSEQ_1:39; then
A7: len (ev_(F|N0,x)^<*ev_(x,R).(F/.(len F))*>) = N0+1 by A6,FINSEQ_1:22;
for k be Nat st 1 <= k <= len ev_(F,x) holds
ev_(F,x).k = (ev_(F|N0,x)^<*ev_(x,R).(F/.(len F))*>).k
proof
let k be Nat;
assume 1 <= k <= len ev_(F,x); then
A8: k in Seg (N0+1) by A3; then
A9: k in Seg N0 \/ {N0+1} by FINSEQ_1:9;
A10: Seg N0 c= Seg(N0 + 1) by FINSEQ_3:18;
per cases by A9,XBOOLE_0:def 3;
suppose
A11: k in Seg N0; then
A12: k in dom (F|N0) by A4,FINSEQ_1:def 3; then
A13: k in dom ev_(F|N0,x) by Def23;
A14: k in dom (F|Seg N0) by A11,A4,FINSEQ_1:def 3;
A15: (F|N0)/.k = (F|Seg N0).k by A12,PARTFUN1:def 6
.= F.k by A14,FUNCT_1:47 .= F/.k by A2,A11,A10,PARTFUN1:def 6;
((ev_(F|N0,x))^<* ev_(x,R).(F/.(N0+1)) *>).k
= (ev_(F|N0,x)).k by A13,FINSEQ_1:def 7
.= ev_(x,R).(F/.k) by A15,A12,Def23
.= ev_(F,x).k by Def23,A8,A2;
hence thesis by A1;
end;
suppose k in {N0+1}; then
A16: k = N0+1 by TARSKI:def 1;
N0+1 = len ev_(F|N0,x) + 1 by A5,FINSEQ_1:6;
hence thesis by A1,Def23,A2,FINSEQ_1:4,A16;
end;
end;
hence thesis by A3,A7,FINSEQ_1:6;
end;
theorem Th11:
for F be FinSequence of the carrier of Free_LMod(X,R), x be Element of X
holds ev_(x,R).(Sum F) = Sum ev_(F,x)
proof
let F be FinSequence of the carrier of Free_LMod(X,R), x be Element of X;
per cases;
suppose
A1: len F = 0; then
F = <*>(the carrier of Free_LMod(X,R)); then
Sum F = 0.Free_LMod(X,R) by RLVECT_1:43; then
A2: ev_(x,R).(Sum F) = 0.R by Th9;
Seg len F = dom F by FINSEQ_1:def 3
.= dom ev_(F,x) by Def23
.= Seg(len ev_(F,x)) by FINSEQ_1:def 3; then
ev_(F,x) = <*>(the carrier of R) by A1;
hence thesis by A2,RLVECT_1:43;
end;
suppose
A3: len F <> 0;
for k be non zero Nat holds
len F = k implies ev_(x,R).(Sum F) = Sum(ev_(F,x))
proof
let k be non zero Nat;
defpred P[non zero Nat] means
for F be FinSequence of the carrier of Free_LMod(X,R) st
len F = $1 holds ev_(x,R).(Sum F) = Sum(ev_(F,x));
A4: P[ 1 ]
proof
for F be FinSequence of the carrier of Free_LMod(X,R) st
len F = 1 holds ev_(x,R).(Sum F) = Sum(ev_(F,x))
proof
let F be FinSequence of the carrier of Free_LMod(X,R);
assume
A5: len F = 1; then
dom F = Seg 1 by FINSEQ_1:def 3; then
A6: 1 in dom F; then
F.1 in rng F by FUNCT_1:3; then
reconsider o = F.1 as Element of Free_LMod(X,R);
F = <*o*> by A5,FINSEQ_1:40; then
A7: Sum F = F.1 by RLVECT_1:44 .= F/.1 by A6,PARTFUN1:def 6;
set o1 = ev_(F,x).1;
set o = ev_(F,x)/.1;
A8: dom ev_(F,x) = dom F by Def23 .= Seg 1 by A5,FINSEQ_1:def 3;
then
A9: 1 in dom ev_(F,x);
A10: dom ev_(F,x) = dom F by Def23;
ev_(F,x) = <* o1 *> by A8,FINSEQ_1:def 8 .= <* o *>
by A9,PARTFUN1:def 6; then
Sum ev_(F,x) = (ev_(F,x)).1 by BINOM:3
.= ev_(x,R).(Sum F) by A7,A9,A10,Def23;
hence thesis;
end;
hence thesis;
end;
A11: for k be non zero Nat holds P[k] implies P[k+1]
proof
let k be non zero Nat;
assume
A12: P[k];
for F be FinSequence of the carrier of Free_LMod(X,R)
st len F = k+1 holds ev_(x,R).(Sum F) = Sum ev_(F,x)
proof
let F be FinSequence of the carrier of Free_LMod(X,R);
assume
A13: len F = k+1; then
consider G be FinSequence of Free_LMod(X,R),
d be Element of Free_LMod(X,R) such that
A14: F = G^<*d*> by FINSEQ_2:19;
(F|k)^<* F/.len F *> = G^<*d*> by A14,A13,FINSEQ_5:21; then
A15: G = (F|k) & d = F/.len F by FINSEQ_2:17;
A16: k + 1 = len G + 1 by FINSEQ_2:16,A14,A13;
Sum F = Sum G + d by A14,FVSUM_1:71; then
ev_(x,R).(Sum F) = ev_(x,R).(Sum G) + ev_(x,R).d by Th8
.= Sum(ev_(F|k,x)) + ev_(x,R).(F/.len F) by A16,A12,A15
.= Sum(ev_(F|k,x)^<* ev_(x,R).(F/.len F) *>) by FVSUM_1:71
.= Sum(ev_(F,x)) by A13,Th10;
hence thesis;
end;
hence P[k + 1];
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A4,A11);
hence thesis;
end;
hence thesis by A3;
end;
end;
definition
let X,R;
let f be Element of Free_LMod(X,R);
func F_idxseq(f) -> FinSequence of the carrier of Free_LMod(X,R) means
:Def24:
len it = len idxseq(f) & for i be Nat st i in dom it holds
it.i = (ev_iota(f)).((idxseq(f)).i);
existence
proof
deffunc F(Nat) = (ev_iota(f)).((idxseq(f)).$1);
consider z being FinSequence such that
A1: len z = len idxseq(f) & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of the carrier of Free_LMod(X,R)
proof
rng z c= the carrier of Free_LMod(X,R)
proof
let o be object;
assume o in rng z; then
consider i be object such that
A3: i in dom z and
A4: o = z.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
i in dom idxseq(f) by A1, A3,FINSEQ_3:29; then
reconsider x9 = (idxseq(f)).i as Element of X by FINSEQ_2:11;
z.i = (ev_iota(f)).x9 by A1,A3;
hence thesis by A4;
end;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of the carrier of Free_LMod(X,R) such that
A5: len z1 = len idxseq(f) and
A6: for i be Nat st i in dom z1 holds
z1.i = (ev_iota(f)).((idxseq(f)).i) and
A7: len z2 = len idxseq(f) and
A8: for j be Nat st j in dom z2 holds
z2.j = (ev_iota(f)).((idxseq(f)).j);
A9: dom z1 = Seg (len idxseq(f)) by A5,FINSEQ_1:def 3
.= dom z2 by A7,FINSEQ_1:def 3;
for q be Nat st q in dom z1 holds z1.q = z2.q
proof
let q be Nat;
assume
A10: q in dom z1; then
reconsider q9 = q as Element of NAT;
z1.q9 =(ev_iota(f)).((idxseq f).q9) by A6,A10
.= z2.q9 by A8,A9,A10;
hence thesis;
end;
hence thesis by A9;
end;
end;
theorem Th12:
for f be Element of Free_LMod(X,R),x be Element of X
st not x in Support @f holds 0.R = @(Sum(F_idxseq(f))).x
proof
let f be Element of Free_LMod(X,R), x be Element of X;
assume
A1: not x in Support @f;
A2: dom F_idxseq f = Seg len F_idxseq f by FINSEQ_1:def 3
.= Seg len idxseq f by Def24
.= dom idxseq f by FINSEQ_1:def 3;
A3: dom ev_(F_idxseq(f),x) = dom F_idxseq f by Def23;
A4: for i be Nat st i in dom ev_(F_idxseq(f),x) holds
ev_(F_idxseq(f),x).i = 0.R
proof
let i be Nat;
assume
A5: i in dom ev_(F_idxseq(f),x); then
A6: i in dom(F_idxseq(f)) by Def23;
i in dom idxseq(f) by A2,Def23,A5; then
A8: (canFS (Support @f)).i in rng (canFS (Support @f)) by FUNCT_1:3;
then (canFS (Support @f)).i in Support @f; then
reconsider x1 = (canFS (Support @f)).i as Element of X;
reconsider r = ev_(x1,R).f as Element of the carrier of R;
reconsider u = Iota(x1,R) as Element of Free_LMod(X,R);
reconsider v = (ev_iota(f)).x1 as Element of Free_LMod(X,R);
x <> x1 by A1,A8; then
A9: 0.R = @u.x by Def17;
A10: [r,u] in [:the carrier of R,fs_Funcs(X,R):];
v = (ev_(x1,R).f)*(IotaMap(X,R).x1) by Def21
.= fs_LMULT(X,R).(r,u) by Def19; then
A11: @v.x
= (LMULT(X,R).(r,u)).x by A10,FUNCT_1:49 .= r*(@u.x) by Def7
.= 0.R by A9;
ev_(F_idxseq(f),x).i = ev_(x,R).((F_idxseq(f))/.i) by A3,A5,Def23
.= ev_(x,R).((F_idxseq(f)).i) by A6,PARTFUN1:def 6
.= ev_(x,R).((ev_iota(f)).((idxseq(f)).i)) by A6,Def24
.= 0.R by A11,Def20;
hence thesis;
end;
reconsider p = ev_(F_idxseq(f),x) as FinSequence of R;
for k be Element of NAT st k in dom p holds p.k=0.R by A4; then
0.R = (Sum ev_(F_idxseq(f),x)) by MATRIX_3:35
.= ev_(x,R).Sum(F_idxseq(f)) by Th11
.= @(Sum(F_idxseq(f))).x by Def20;
hence thesis;
end;
theorem Th13:
for f be Element of Free_LMod(X,R),x be Element of X st x in Support @f
holds
ex k be Nat st x = (canFS (Support @f)).k & k in dom (canFS (Support @f)) &
ev_(F_idxseq(f),x).k = @f.x
proof
let f be Element of Free_LMod(X,R), x be Element of X;
assume
A1: x in Support @f;
rng canFS Support @f = Support @f by FUNCT_2:def 3; then
consider o being object such that
A2: o in dom canFS (Support @f) & x = (canFS (Support @f)).o
by A1,FUNCT_1:def 3;
reconsider n1 = o as Nat by A2;
A3: dom F_idxseq(f) = Seg len F_idxseq f by FINSEQ_1:def 3
.= Seg len idxseq f by Def24
.= dom idxseq f by FINSEQ_1:def 3;
A4: ev_(F_idxseq(f),x).n1 = @f.x
proof
reconsider i = n1 as Nat;
reconsider r = ev_(x,R).f as Element of the carrier of R;
reconsider u = Iota(x,R) as Element of Free_LMod(X,R);
reconsider v = (ev_iota(f)).x as Element of Free_LMod(X,R);
A5: 1.R = @u.x by Def17;
A6: [r,u] in [:the carrier of R,fs_Funcs(X,R):];
v = (ev_(x,R).f)*(IotaMap(X,R).x) by Def21
.= fs_LMULT(X,R).(r,u) by Def19; then
A7: @v.x = (LMULT(X,R).(r,u)).x by A6,FUNCT_1:49 .= r*(@u.x) by Def7
.= r by A5;
ev_(F_idxseq(f),x).i = ev_(x,R).((F_idxseq(f))/.i) by A3,A2,Def23
.= ev_(x,R).((F_idxseq(f)).i) by A3,A2,PARTFUN1:def 6
.= ev_(x,R).v by A3,A2,Def24
.= r by A7,Def20
.= @f.x by Def20;
hence thesis;
end;
take n1;
thus thesis by A4,A2;
end;
theorem Th14:
for f be Element of Free_LMod(X,R),x be Element of X st x in Support @f
holds @f.x = (@Sum(F_idxseq(f))).x
proof
let f be Element of Free_LMod(X,R), x be Element of X;
assume
A1: x in Support @f;
rng canFS (Support @f) = Support @f by FUNCT_2:def 3; then
consider o being object such that
A2: o in dom canFS (Support @f) & x = (canFS (Support @f)).o
by A1,FUNCT_1:def 3;
reconsider n1 = o as Nat by A2;
A3: dom F_idxseq f = Seg len F_idxseq f by FINSEQ_1:def 3
.= Seg len idxseq f by Def24
.= dom idxseq f by FINSEQ_1:def 3;
A4: dom ev_(F_idxseq(f),x) = dom F_idxseq f by Def23;
A5: n1 in dom ev_(F_idxseq(f),x) by A3,A2,Def23;
A6: for i be Nat st i in dom ev_(F_idxseq(f),x) & i <> n1 holds
ev_(F_idxseq(f),x).i = 0.R
proof
let i be Nat;
assume
A7: i in dom ev_(F_idxseq(f),x) & i <> n1; then
A8: i in dom F_idxseq(f) by Def23;
A9: i in dom idxseq(f) by A3,Def23,A7; then
(canFS (Support @f)).i in rng canFS (Support @f) by FUNCT_1:3;
then
(canFS Support @f).i in Support @f; then
reconsider x1 = (canFS (Support @f)).i as Element of X;
reconsider r = ev_(x1,R).f as Element of the carrier of R;
reconsider u = Iota(x1,R) as Element of Free_LMod(X,R);
reconsider v = (ev_iota(f)).x1 as Element of Free_LMod(X,R);
x <> x1 by A2,A7,A9,FUNCT_1:def 4; then
A10: 0.R = @u.x by Def17;
A11: [r,u] in [:the carrier of R,fs_Funcs(X,R):];
v = (ev_(x1,R).f)*(IotaMap(X,R).x1) by Def21
.= fs_LMULT(X,R).(r,u) by Def19; then
A12: @v.x
= (LMULT(X,R).(r,u)).x by A11,FUNCT_1:49 .= r*(@u.x) by Def7
.= 0.R by A10;
ev_(F_idxseq(f),x).i = ev_(x,R).((F_idxseq(f))/.i) by A4,A7,Def23
.= ev_(x,R).((F_idxseq(f)).i) by A8,PARTFUN1:def 6
.= ev_(x,R).((ev_iota(f)).((idxseq(f)).i)) by A8,Def24
.= 0.R by Def20,A12;
hence thesis;
end;
consider k be Nat such that
A13: x = (canFS (Support @f)).k & k in dom (canFS (Support @f)) &
ev_(F_idxseq(f),x).k = @f.x by A1,Th13;
A14: ev_(F_idxseq(f),x).n1 = @f.x by A2,A13,FUNCT_1:def 4;
Sum ev_(F_idxseq(f),x) = ev_(x,R).Sum(F_idxseq(f)) by Th11
.= (@Sum(F_idxseq(f))).x by Def20;
hence thesis by A14,A5,A6,MATRIX_3:12;
end;
::$MR Every element of $\mathrm{Free\_LMod}(X,R)$ is the sum of its canonical finite decomposition.
theorem Th15:
for f be Element of Free_LMod(X,R) holds f = Sum(F_idxseq(f))
proof
let f be Element of Free_LMod(X,R);
A1: dom @f = X by FUNCT_2:def 1 .= dom @(Sum(F_idxseq(f))) by FUNCT_2:def 1;
for o being object st o in dom @f holds
@f.o = @(Sum(F_idxseq(f))).o
proof
let o be object;
assume o in dom @f; then
reconsider x = o as Element of X;
per cases;
suppose o in Support @f;
hence thesis by Th14;
end;
suppose
A4: not o in Support @f;
@f.x = ev_(x,R).f by Def20
.= 0.R by A4,Lm18 .= @(Sum(F_idxseq(f))).x by A4,Th12;
hence thesis;
end;
end; then
@f = @(Sum(F_idxseq(f))) by A1;
hence thesis;
end;
Lm23:
for x be Element of X, r be Element of R st r <> 0.R holds
Support @(r*Iota(x,R)) = {x}
proof
let x be Element of X, r be Element of R;
assume
A1: r <> 0.R;
thus Support @(r*Iota(x,R)) c= {x}
proof
let o be object;
assume
A2: o in Support @(r*Iota(x,R)); then
reconsider x1 = o as Element of X;
A3: @(r*Iota(x,R)).x1 = r*@Iota(x,R).x1 by Th7;
per cases;
suppose
o = x;
hence thesis by TARSKI:def 1;
end;
suppose
o <> x; then
@Iota(x,R).o = 0.R by A2,Def17;
hence thesis by A2,A3,POLYNOM1:def 4;
end;
end;
@Iota(x,R).x = 1.R by Def17; then
@(r*Iota(x,R)).x = r*1.R by Th7 .= r; then
x in Support @(r*Iota(x,R)) by A1,POLYNOM1:def 4;
hence thesis by ZFMISC_1:31;
end;
Lm24:
for f be Element of Free_LMod(X,R), i be Nat st i in dom idxseq(f) holds
Support @((F_idxseq(f))/.i) = { (idxseq f).i }
proof
let f be Element of Free_LMod(X,R), i be Nat;
assume
A1: i in dom idxseq f;
A2: dom F_idxseq f = Seg len F_idxseq f by FINSEQ_1:def 3
.= Seg len idxseq f by Def24
.= dom idxseq f by FINSEQ_1:def 3;
reconsider x9 = (idxseq(f)).i as Element of X by A1,FINSEQ_2:11;
rng canFS Support @f = Support @f by FUNCT_2:def 3; then
x9 in Support @f by A1,FUNCT_1:3; then
@f.x9 <> 0.R by POLYNOM1:def 4; then
A6: ev_(x9,R).f <> 0.R by Def20;
reconsider r = ev_(x9,R).f as Element of the carrier of R;
(F_idxseq(f))/.i = (F_idxseq(f)).i by A1,A2,PARTFUN1:def 6
.= (ev_iota(f)).x9 by A1,A2,Def24
.= (ev_(x9,R).f)*(IotaMap(X,R).x9) by Def21
.= r*Iota(x9,R) by Def19;
hence thesis by A6,Lm23;
end;
Lm25:
for f be Element of Free_LMod(X,R) holds
(ex x be Element of X st Support @f = {x}) iff len idxseq(f) = 1
proof
let f be Element of Free_LMod(X,R);
thus (ex x be Element of X st Support @f = {x}) implies len idxseq(f) = 1
proof
given x be Element of X such that
A1: Support @f = {x};
card canFS(Support @f) = card Support @f by FINSEQ_1:93
.= 1 by A1,CARD_1:30;
hence len idxseq(f) = 1;
end;
assume len idxseq(f) = 1; then
card(Support @f) = 1 by FINSEQ_1:93;
then consider a being object such that
A4: Support @f = {a} by CARD_2:42;
reconsider x = a as Element of X by A4,ZFMISC_1:31;
take x;
thus Support @f = {x} by A4;
end;
Lm26:
for x be Element of X, f be Element of Free_LMod(X,R) st
Support @f = {x} holds f = (@f.x)*(IotaMap(X,R).x) & f = (F_idxseq(f)).1
& F_idxseq(f) = <* (F_idxseq(f)).1 *> & idxseq(f) = <* x *>
proof
let x be Element of X, f be Element of Free_LMod(X,R);
assume
A1: Support @f = {x}; then
consider x0 be Element of X such that
A2: Support @f = {x0};
A4: x = x0 by A1,A2,ZFMISC_1:3;
A5: len idxseq(f) = 1 by A2,Lm25;
dom F_idxseq(f) = Seg len F_idxseq(f) by FINSEQ_1:def 3
.= Seg 1 by A5,Def24; then
A6: 1 in dom F_idxseq(f);
A7: idxseq(f) = <* x0 *> by A2,FINSEQ_1:94;
A8: (F_idxseq(f)).1 = (ev_iota(f)).((idxseq(f)).1) by A6,Def24
.= (ev_(x0,R).f)*(IotaMap(X,R).x0) by A7,Def21
.= (@f.x)*(IotaMap(X,R).x) by A4,Def20; then
F_idxseq(f) = <* (@f.x)*(IotaMap(X,R).x) *> by A5,Def24,FINSEQ_1:40;
then
f = Sum <* (@f.x)*(IotaMap(X,R).x) *> by Th15;
hence thesis by RLVECT_1:44, A8,A5,Def24,FINSEQ_1:40,94, A1;
end;
theorem Th16:
for f,g be Element of Free_LMod(X,R)
st Support @f misses Support @g holds
Support @(f+g) = (Support @f) \/ (Support @g)
proof
let f,g be Element of Free_LMod(X,R);
assume
A1: Support @f misses Support @g;
thus Support @(f+g) c= (Support @f) \/ (Support @g)
proof
let o be object;
assume
A3: o in Support @(f+g); then
reconsider x = o as Element of X;
x in (Support @f) \/ (Support @g)
proof
assume not (x in (Support @f) \/ (Support @g)); then
not x in (Support @f) & not x in (Support @g) by XBOOLE_0:def 3;
then
A5: @f.x = 0.R & @g.x = 0.R by POLYNOM1:def 4;
@(f+g).x = @f.x + @g.x by Th8 .= 0.R by A5;
hence contradiction by A3,POLYNOM1:def 4;
end;
hence thesis;
end;
let o be object;
assume o in (Support @f) \/ (Support @g); then
per cases by XBOOLE_0:def 3;
suppose
A7: o in Support @f; then
reconsider x = o as Element of X;
A8: @(f+g).x = @f.x + @g.x by Th8;
not x in Support @g by A1,A7,XBOOLE_0:def 4; then
@g.x = 0.R by POLYNOM1:def 4; then
0.R <> @f.x + @g.x by A7,POLYNOM1:def 4;
hence thesis by A8,POLYNOM1:def 4;
end;
suppose
A10: o in Support @g; then
reconsider x = o as Element of X;
A11: @(f+g).x = @f.x + @g.x by Th8;
not x in Support @f by A1,A10,XBOOLE_0:def 4; then
@f.x = 0.R by POLYNOM1:def 4; then
0.R <> @f.x + @g.x by A10,POLYNOM1:def 4;
hence thesis by A11,POLYNOM1:def 4;
end;
end;
definition
let X,R,N;
let u be Function of X,N;
func @u -> Element of Funcs(X,[#]N) equals
u;
coherence by FUNCT_2:8;
end;
definition
let X,R,N;
let u be Function of X,N;
func ^u -> Element of Func_Mod(X,N) equals
u;
coherence by FUNCT_2:8;
end;
definition
let X,R,N;
let u be Element of Func_Mod(X,N);
func ^u -> Function of X,N equals
u;
coherence by FUNCT_2:66;
end;
begin :: Universal Mapping Property
reserve B,B1,B2 for Element of Fin X;
reserve f for Element of Free_LMod(X,R);
reserve v for Function of X, the carrier of N;
definition
let R be non degenerated Ring, X be non empty set, N be LeftMod of R;
let v be Function of X, the carrier of N;
let f be Element of Free_LMod(X,R);
func TermFS(f,v) -> Function of X, the carrier of N means
:Def28:
for x being Element of X holds it.x = (@f.x) * (v.x);
existence
proof
deffunc F(Element of X) = (@f.$1) * (v.$1);
consider g being Function of X, the carrier of N such that
A1: for x being Element of X holds g.x = F(x) from FUNCT_2:sch 4;
take g;
thus thesis by A1;
end;
uniqueness
proof
let g1,g2 be Function of X, the carrier of N;
assume that
A2: for x being Element of X holds g1.x = (@f.x) * (v.x) and
A3: for x being Element of X holds g2.x = (@f.x) * (v.x);
now let x be Element of X;
thus g1.x = (@f.x) * (v.x) by A2
.= g2.x by A3;
end;
hence g1 = g2;
end;
end;
definition
let R be non degenerated Ring, X be non empty set, N be LeftMod of R;
let v be Function of X, the carrier of N;
let f be Element of Free_LMod(X,R);
let B be Element of Fin X;
func PhiSet(v,f,B) -> Element of N equals
(the addF of N) $$ (B, TermFS(f,v));
coherence;
end;
theorem Th17:
for x being Element of X holds PhiSet(v,f,{.x.}) = (@f.x) * (v.x)
proof
let x be Element of X;
PhiSet(v,f,{.x.}) = TermFS(f,v).x by SETWISEO:17
.= (@f.x) * (v.x) by Def28;
hence thesis;
end;
Th18: ::: SETWOP_2:7 in other words
for X,Y be non empty set
for F be BinOp of Y
for t1,t2 be Function of X,Y
for B be Element of Fin X
st F is commutative & F is associative & F is having_a_unity &
(for x be Element of X st x in B holds t1.x = t2.x)
holds F $$ (B,t1) = F $$ (B,t2)
proof
let X,Y be non empty set;
let F be BinOp of Y;
let t1,t2 be Function of X,Y;
let B be Element of Fin X;
assume that
A1: F is commutative & F is associative & F is having_a_unity and
A2: for x be Element of X st x in B holds t1.x = t2.x;
A4: B is Subset of X by FINSUB_1:16;
A5: dom (t1|B) = (dom t1) /\ B by RELAT_1:61
.= X /\ B by FUNCT_2:def 1
.= B by XBOOLE_1:28,A4;
A6: dom (t2|B) = (dom t2) /\ B by RELAT_1:61
.= X /\ B by FUNCT_2:def 1
.= B by XBOOLE_1:28,A4;
t1|B = t2|B
proof
for x be object st x in dom (t1|B) holds (t1|B).x = (t2|B).x
proof
let x be object;
assume
A7: x in dom (t1|B); then
reconsider x1 = x as Element of X;
(t1|B).x = t1.x1 by A7,FUNCT_1:47
.= t2.x1 by A2,A7,A5
.= (t2|B).x by A7,A5,A6,FUNCT_1:47;
hence thesis;
end;
hence thesis by A5,A6;
end;
hence thesis by A1,SETWOP_2:7;
end;
definition
let R be non degenerated Ring, X be non empty set;
let f be Element of Free_LMod(X,R);
func SuppFin(f) -> Element of Fin X equals
Support @f;
coherence by FINSUB_1:def 5;
end;
::$INSERT we define the induced homomorphism $\Phi(v):\mathrm{FS\_Funcs}(X,R)\to N$.
definition
let R be non degenerated Ring, X be non empty set, N be LeftMod of R;
let v be Function of X, the carrier of N;
func Phi(v) -> Function of Free_LMod(X,R), the carrier of N means
:Def31:
for f being Element of Free_LMod(X,R) holds
it.f = PhiSet(v,f,SuppFin(f));
existence
proof
deffunc F(Element of Free_LMod(X,R)) = PhiSet(v,$1,SuppFin($1));
consider h being Function of Free_LMod(X,R), the carrier of N such that
A1: for f being Element of Free_LMod(X,R) holds h.f = F(f)
from FUNCT_2:sch 4;
take h;
thus thesis by A1;
end;
uniqueness
proof
let h1,h2 be Function of Free_LMod(X,R), the carrier of N;
assume that
A2: for f being Element of Free_LMod(X,R) holds h1.f = PhiSet(v,f,SuppFin(f))
and
A3: for f being Element of Free_LMod(X,R) holds h2.f = PhiSet(v,f,SuppFin(f));
now let f be Element of Free_LMod(X,R);
thus h1.f = PhiSet(v,f,SuppFin(f)) by A2
.= h2.f by A3;
end;
hence h1 = h2;
end;
end;
theorem Th19:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, x be Element of X holds
(Phi(v)).(Iota(x,R)) = v.x
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, x be Element of X;
set fx = Iota(x,R);
SuppFin(fx) = {.x.} by Lm16; then
(Phi(v)).fx = PhiSet(v,fx,{.x.}) by Def31; then
(Phi(v)).(Iota(x,R))
= (@fx.x) * (v.x) by Th17
.= 1.R * (v.x) by Def17
.= v.x;
hence thesis;
end;
:: Additivity of Phi(v) can be intuitively understood
:: by reducing to the disjoint-support case.
theorem :::: Th20:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R)
st Support @f misses Support @g
holds (Phi(v)).(f+g) = (Phi(v)).f + (Phi(v)).g
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R);
assume
A1: Support @f misses Support @g;
set F = the addF of N;
set Bf = SuppFin(f), Bg = SuppFin(g);
set tf = TermFS(f,v),tg = TermFS(g,v),th = TermFS(f+g,v);
A2: for x be Element of X st x in Bf holds th.x = tf.x
proof
let x be Element of X;
assume x in Bf; then
A4: not x in Support @g by A1,XBOOLE_0:3;
th.x = (@(f+g).x) * (v.x) by Def28
.= (@f.x + @g.x) * (v.x) by Th8
.= (@f.x + 0.R) * (v.x) by A4,POLYNOM1:def 4
.= tf.x by Def28;
hence thesis;
end;
A5: for x be Element of X st x in Bg holds th.x = tg.x
proof
let x be Element of X;
assume x in Bg; then
A7: not x in Support @f by A1,XBOOLE_0:3;
th.x = (@(f+g).x) * (v.x) by Def28
.= (@f.x + @g.x) * (v.x) by Th8
.= (0.R + @g.x) * (v.x) by A7,POLYNOM1:def 4
.= tg.x by Def28;
hence thesis;
end;
A8: PhiSet(v,f+g,Bg) = PhiSet(v,g,Bg) by FVSUM_1:8,A5,Th18;
(Phi(v)).(f+g)
= PhiSet(v,f+g,SuppFin(f+g)) by Def31
.= PhiSet(v,f+g,Bf \/ Bg) by A1,Th16
.= F.(PhiSet(v,f+g,Bf), PhiSet(v,f+g,Bg)) by A1,FVSUM_1:8,SETWOP_2:4
.= F.(PhiSet(v,f,Bf), PhiSet(v,g,Bg)) by FVSUM_1:8,A2,Th18,A8
.= F.((Phi(v)).f, PhiSet(v,g,Bg)) by Def31
.= (Phi(v)).f + (Phi(v)).g by Def31;
hence thesis;
end;
Lm27:
for R be non degenerated Ring, N be LeftMod of R holds
the_unity_wrt the addF of N = 0.N
proof
let R be non degenerated Ring, N be LeftMod of R;
set F = the addF of N;
for a be Element of N holds F.(0.N,a) = a & F.(a,0.N) = a
proof
let a be Element of N;
A1: F.(0.N,a) = 0.N + a .= a;
F.(a,0.N) = a + 0.N .= a;
hence thesis by A1;
end; then
0.N is_a_unity_wrt F by BINOP_1:3;
hence the_unity_wrt F = 0.N by BINOP_1:def 8;
end;
Lm28:
for R be non degenerated Ring, X be non empty set,
N be LeftMod of R, v be Function of X, the carrier of N,
f be Element of Free_LMod(X,R), B,C be Element of Fin X st B c= C &
(for x be Element of X st x in C \ B holds TermFS(f,v).x = 0.N) holds
PhiSet(v,f,B) = PhiSet(v,f,C)
proof
let R be non degenerated Ring, X be non empty set,
N be LeftMod of R, v be Function of X, the carrier of N,
f be Element of Free_LMod(X,R), B,C be Element of Fin X;
assume that
A1: B c= C and
A2: for x be Element of X st x in C \ B holds TermFS(f,v).x = 0.N;
set F = the addF of N;
set t = TermFS(f,v);
reconsider D = C \ B as Element of Fin X;
A5: C = B \/ D by A1,XBOOLE_1:45;
A6: B misses D by XBOOLE_1:79;
per cases;
suppose
D = {}; then
C = B by A1,XBOOLE_1:37;
hence thesis;
end;
suppose
A8: D <> {};
A9: t.:D = {0.N}
proof
thus t.:D c= {0.N}
proof
let y be object;
assume y in t.:D; then
consider x being object such that
A12: x in dom t & x in D & y = t.x by FUNCT_1:def 6;
reconsider x1 = x as Element of X by A12;
t.x1 = 0.N by A2,A12;
hence thesis by A12,TARSKI:def 1;
end;
A14: D is Subset of X by FINSUB_1:16;
consider x being object such that
A15: x in D by A8,XBOOLE_0:def 1;
reconsider x1 = x as Element of X by A15,A14;
ex u being object st u in dom t & u in D & 0.N = t.u
proof
take x1;
dom t = X by FUNCT_2:def 1;
hence thesis by A15,A2;
end; then
A17: 0.N in t.:D by FUNCT_1:def 6;
let y be object;
assume y in {0.N};
hence thesis by A17,TARSKI:def 1;
end;
A19: F $$ (D,t) = 0.N
proof
set e = the_unity_wrt F;
t.:D = {e} by A9,Lm27; then
F $$ (D,t) = e by FVSUM_1:8,SETWOP_2:8
.= 0.N by Lm27;
hence thesis;
end;
PhiSet(v,f,C)
= (F $$ (B,t)) + 0.N by A19,A6,FVSUM_1:8,A5,SETWOP_2:4
.= PhiSet(v,f,B);
hence PhiSet(v,f,B) = PhiSet(v,f,C);
end;
end;
Lm29:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N,
f be Element of Free_LMod(X,R), x be Element of X
st not x in Support @f
holds TermFS(f,v).x = 0.N
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N,
f be Element of Free_LMod(X,R), x be Element of X;
assume not x in Support @f; then
@f.x = 0.R by POLYNOM1:def 4;
hence TermFS(f,v).x = (0.R) * (v.x) by Def28
.= 0.N by VECTSP_1:14;
end;
Lm30:
for R be non degenerated Ring, X be non empty set,
f,g be Element of Free_LMod(X,R), x be Element of X
st x in Support @(f+g)
holds x in (Support @f) \/ (Support @g)
proof
let R be non degenerated Ring, X be non empty set,
f,g be Element of Free_LMod(X,R), x be Element of X;
assume
A1: x in Support @(f+g);
assume not x in (Support @f) \/ (Support @g); then
not x in Support @f & not x in Support @g by XBOOLE_0:def 3; then
A3: @f.x = 0.R & @g.x = 0.R by POLYNOM1:def 4;
@(f+g).x = @f.x + @g.x by Th8
.= 0.R by A3;
hence contradiction by A1,POLYNOM1:def 4;
end;
Lm31:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R),
x be Element of X holds TermFS(f+g,v).x = TermFS(f,v).x + TermFS(g,v).x
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R),
x be Element of X;
TermFS(f+g,v).x = (@(f+g).x) * (v.x) by Def28
.= (@f.x + @g.x) * (v.x) by Th8
.= (@f.x) * (v.x) + (@g.x) * (v.x) by VECTSP_1:def 15
.= TermFS(f,v).x + (@g.x) * (v.x) by Def28
.= TermFS(f,v).x + TermFS(g,v).x by Def28;
hence thesis;
end;
Lm32:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R),
B be Element of Fin X holds PhiSet(v,f,B) + PhiSet(v,g,B) = PhiSet(v,f+g,B)
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R),
B be Element of Fin X;
set F = the addF of N;
set th = TermFS(f+g,v);
A1: for x be Element of X st x in B holds
TermFS(f+g,v).x = (F.: (TermFS(f,v),TermFS(g,v))).x
proof
let x be Element of X;
th.x = TermFS(f,v).x + TermFS(g,v).x by Lm31
.= (F.: (TermFS(f,v),TermFS(g,v))).x by FUNCOP_1:37;
hence thesis;
end;
PhiSet(v,f,B) + PhiSet(v,g,B)
= F $$ (B, F.: (TermFS(f,v),TermFS(g,v))) by FVSUM_1:8,SETWOP_2:10
.= PhiSet(v,f+g,B) by FVSUM_1:8,A1,Th18;
hence thesis;
end;
theorem Th21:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R)
holds (Phi(v)).(f+g) = (Phi(v)).f + (Phi(v)).g
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f,g be Element of Free_LMod(X,R);
set Bf = SuppFin(f), Bg = SuppFin(g), Bh = SuppFin(f+g);
set B = Bf \/ Bg;
A1: Bh c= B by Lm30;
A2: PhiSet(v,f,Bf) = PhiSet(v,f,B)
proof
for x be Element of X st x in B \ Bf holds TermFS(f,v).x = 0.N
proof
let x be Element of X;
assume x in B \ Bf;
then not x in Bf by XBOOLE_0:def 5;
hence thesis by Lm29;
end;
hence thesis by XBOOLE_1:7,Lm28;
end;
A4: PhiSet(v,g,Bg) = PhiSet(v,g,B)
proof
for x be Element of X st x in B \ Bg holds TermFS(g,v).x = 0.N
proof
let x be Element of X;
assume x in B \ Bg;
then not x in Bg by XBOOLE_0:def 5;
hence thesis by Lm29;
end;
hence thesis by XBOOLE_1:7,Lm28;
end;
A6: PhiSet(v,f+g,Bh) = PhiSet(v,f+g,B)
proof
for x be Element of X st x in B \ Bh holds TermFS(f+g,v).x = 0.N
proof
let x be Element of X;
assume x in B \ Bh; then
not x in Bh by XBOOLE_0:def 5;
hence thesis by Lm29;
end;
hence thesis by A1,Lm28;
end;
(Phi(v)).(f+g) = PhiSet(v,f+g,B) by A6,Def31
.= PhiSet(v,f,Bf) + PhiSet(v,g,Bg) by A4,A2,Lm32
.= (Phi(v)).f + PhiSet(v,g,Bg) by Def31
.= (Phi(v)).f + (Phi(v)).g by Def31;
hence thesis;
end;
Lm33:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f be Element of Free_LMod(X,R),
a be Element of R, x be Element of X
holds TermFS(a*f,v).x = a * (TermFS(f,v).x)
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f be Element of Free_LMod(X,R),
a be Element of R, x be Element of X;
TermFS(a*f,v).x = (@(a*f).x) * (v.x) by Def28
.= (a * (@f.x)) * (v.x) by Th7
.= a * ((@f.x) * (v.x)) by VECTSP_1:def 16
.= a * (TermFS(f,v).x) by Def28;
hence thesis;
end;
Lm34:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f be Element of Free_LMod(X,R),
a be Element of R, B be Element of Fin X
holds PhiSet(v,a*f,B) = a * PhiSet(v,f,B)
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f be Element of Free_LMod(X,R),
a be Element of R, B be Element of Fin X;
set F = the addF of N, t = TermFS(f,v);
deffunc H(Element of N) = a * $1;
consider h being Function of the carrier of N, the carrier of N such that
A1: for y being Element of N holds h.y = H(y) from FUNCT_2:sch 4;
A2: F is commutative & F is associative & F is having_a_unity by FVSUM_1:8;
set e = the_unity_wrt F;
e = 0.N by Lm27; then
A4: h.e = a * (0.N) by A1
.= 0.N by VECTSP_1:14
.= e by Lm27;
A5: for d1, d2 being Element of N holds h.(F.(d1,d2)) = F.(h.d1, h.d2)
proof
let d1, d2 be Element of N;
h.(F.(d1,d2)) = a * (d1 + d2) by A1
.= a*d1 + a*d2 by VECTSP_1:def 14
.= (h.d1) + a*d2 by A1
.= F.(h.d1, h.d2) by A1;
hence thesis;
end;
h*t = TermFS(a*f,v)
proof
for x being Element of X holds (h*t).x = TermFS(a*f,v).x
proof
let x be Element of X;
(h*t).x = h.(t.x) by FUNCT_2:15
.= a * (t.x) by A1
.= TermFS(a*f,v).x by Lm33;
hence thesis;
end;
hence thesis;
end; then
PhiSet(v,a*f,B)
= h.(PhiSet(v,f,B)) by A2,A4,A5,SETWOP_2:16
.= a * PhiSet(v,f,B) by A1;
hence thesis;
end;
theorem Th22:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f be Element of Free_LMod(X,R),
a be Element of R holds (Phi(v)).(a*f) = a * ((Phi(v)).f)
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N, f be Element of Free_LMod(X,R),
a be Element of R;
set Bf = SuppFin(f), Baf = SuppFin(a*f), B = Bf \/ Baf;
A1: PhiSet(v,f,Bf) = PhiSet(v,f,B)
proof
for x be Element of X st x in B \ Bf holds TermFS(f,v).x = 0.N
proof
let x be Element of X;
assume x in B \ Bf; then
not x in Bf by XBOOLE_0:def 5;
hence TermFS(f,v).x = 0.N by Lm29;
end;
hence thesis by XBOOLE_1:7,Lm28;
end;
A4: PhiSet(v,a*f,Baf) = PhiSet(v,a*f,B)
proof
for x be Element of X st x in B \ Baf holds TermFS(a*f,v).x = 0.N
proof
let x be Element of X;
assume x in B \ Baf; then
not x in Baf by XBOOLE_0:def 5;
hence TermFS(a*f,v).x = 0.N by Lm29;
end;
hence thesis by XBOOLE_1:7,Lm28;
end;
(Phi(v)).(a*f) = PhiSet(v,a*f,B) by A4, Def31
.= a * PhiSet(v,f,Bf) by A1,Lm34
.= a * ((Phi(v)).f) by Def31;
hence thesis;
end;
theorem ::::::: PENCIL_2?
for M be non empty addLoopStr
for p be FinSequence of the carrier of M, k be Nat
st k in dom p holds Del(p,k,k) = Del(p,k)
proof
let M be non empty addLoopStr;
let p be FinSequence of the carrier of M, k be Nat;
assume
A1: k in dom p; then
Seg len p <> {} by FINSEQ_1:def 3; then
A2: len p <> 0;
reconsider p0 = p as FinSequence of the carrier of M;
reconsider m = len p0 - 1 as Nat by A2;
A3: len p0 = m + 1;
A4: len p0 = m + 1 & k in dom p0 by A1;
A5: 1 <= k <= len p0 by A1,FINSEQ_3:25; then
A6: len (p0|(k-'1)) = k-'1 by NAT_D:44,FINSEQ_1:59;
A7: len (p0/^k) = len p0 - k by A5,RFINSEQ:def 1;
A8: len Del(p,k,k) = len (p0|(k-'1)) + len (p0/^k) by FINSEQ_1:22
.= (k-'1) + (len p0 - k) by A6,A5,RFINSEQ:def 1
.= (k - 1) + (len p0 - k) by A5,XREAL_1:233
.= len p0 - 1;
A9: for i be Nat st i in dom Del(p,k,k) holds (Del(p,k,k)).i = (Del(p0,k)).i
proof
let i be Nat;
assume
A10: i in dom Del(p,k,k); then
i in Seg len Del(p0,k) by A8,A4,FINSEQ_3:109,FINSEQ_1:def 3; then
A12: 1 <= i <= len Del(p0,k) by FINSEQ_1:1;
per cases;
suppose
A13: i < k; then
A14: i <= k-'1 by NAT_D:49;
1 <= i by A10,FINSEQ_3:25; then
i in Seg len (p0|(k-'1)) by A14,A6; then
i in dom (p0|(k-'1)) by FINSEQ_1:def 3; then
(Del(p,k,k)).i = (p0|(k-'1)).i by FINSEQ_1:def 7
.= p0.i by A14,FINSEQ_3:112;
hence (Del(p,k,k)).i = (Del(p0,k)).i by A13,FINSEQ_3:110;
end;
suppose
A16: k <= i; then
A17: k <= i <= m by A4,FINSEQ_3:109,A12;
A18: k-'1 = k - 1 by A1,FINSEQ_3:25,XREAL_1:233;
k-1 < k by XREAL_1:30; then
k-'1 < i by A16,A18,XXREAL_0:2; then
len (p0|(k-'1)) < i by A5,NAT_D:44,FINSEQ_1:59; then
i - len (p0|(k-'1)) > 0 by XREAL_1:50; then
i - len (p0|(k-'1)) in NAT by INT_1:3; then
reconsider j = i - len (p0|(k-'1)) as Nat;
k <= m by A17,XXREAL_0:2; then
m - k >= 0 by XREAL_1:48; then
(m-k) +1 > 0; then
(len p0) -k in NAT by INT_1:3; then
reconsider s = (len p0) -k as Nat;
A23: dom (p0/^k) = Seg s by A7,FINSEQ_1:def 3;
A24: j = i - (k-'1) by A5,NAT_D:44,FINSEQ_1:59; then
A25: i = j + (k-'1);
A26: (len p0) -k -(i - (k-'1)) = (len p0) -i -1 by A18;
m -i >= 0 by A17,XREAL_1:48; then
A28: j <= s by A24,A26,XREAL_1:49;
A29: i - k >= k-k by A16,XREAL_1:6;
i - (k-'1) - 1 = i -(k - 1) - 1 by A1,FINSEQ_3:25,XREAL_1:233
.= i - k; then
i - (k-'1) -1+1 >= 0 + 1 by A29,XREAL_1:6; then
1 <= j by A5,NAT_D:44,FINSEQ_1:59; then
A32: j in Seg s by A28; then
A33: (Del(p,k,k)).i = (p0/^k).j by FINSEQ_1:def 7,A23,A25;
j in dom (p0/^k) by A32,A7,FINSEQ_1:def 3; then
A35: (p0/^k).j = p0.(k+j) by FINSEQ_5:27;
A36: j = i - (k-'1) by A5,NAT_D:44,FINSEQ_1:59;
k-'1 = k - 1 by A1,FINSEQ_3:25,XREAL_1:233; then
k+j = i+1 by A36;
hence thesis by A17,A1,A3,FINSEQ_3:111,A33,A35;
end;
end;
dom Del(p,k,k)
= Seg len Del(p0,k) by A8,A4,FINSEQ_3:109,FINSEQ_1:def 3
.= dom Del(p0,k) by FINSEQ_1:def 3;
hence thesis by A9;
end;
Lm37:
for N be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, p be FinSequence of the carrier of N,
k be Nat st k in dom p holds
Sum p = Sum (Del(p,k,k)) + p/.k
proof
let N be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr,
p be FinSequence of the carrier of N,
k be Nat;
set a = p|(k-'1), b = p/^k, c = <* p/.k *>;
assume
A1: k in dom p; then
1 <= k <= len p by FINSEQ_3:25; then
p = (p|(k-'1))^<*p.k*>^(p/^k) by FINSEQ_5:84
.= a^c^b by A1,PARTFUN1:def 6; then
Sum p = Sum (a^c) + Sum b by RLVECT_1:41
.= (Sum a + Sum c) + Sum b by RLVECT_1:41
.= (Sum a + Sum b) + Sum c by RLVECT_1:def 3
.= Sum (Del(p,k,k)) + Sum c by RLVECT_1:41;
hence thesis by RLVECT_1:44;
end;
definition
let R be Ring, X be set, M be LeftMod of R;
let u be Function of X, the carrier of M;
attr u is universal means
for N be LeftMod of R, v be Function of X, the carrier of N
holds
ex F be Homomorphism of (id R), M,N st F*u = v &
for f1,f2 be Homomorphism of (id R), M,N st f1*u = v & f2*u = v
holds f1 = f2;
end;
theorem Th23:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N
holds Phi(v) is Homomorphism of (id R), Free_LMod(X,R), N
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N;
set F = Phi(v);
A1: for x,y being Vector of Free_LMod(X,R) holds
F.(x+y) = (F.x) + (F.y) by Th21;
for a being Scalar of R for x being Vector of Free_LMod(X,R) holds
F.(a*x) = ((id R).a) * (F.x) by Th22;
hence thesis by A1,MOD_4:def 17;
end;
theorem Th24:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N
holds (Phi(v)) * (IotaMap(X,R)) = v
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N;
for x be Element of X holds ((Phi(v)) * (IotaMap(X,R))).x = v.x
proof
let x be Element of X;
((Phi(v)) * (IotaMap(X,R))).x
= (Phi(v)).((IotaMap(X,R)).x) by FUNCT_2:15
.= (Phi(v)).(Iota(x,R)) by Def19
.= v.x by Th19;
hence thesis;
end;
hence thesis;
end;
Lm38:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
h be Homomorphism of (id R), Free_LMod(X,R), N
holds h.(0.Free_LMod(X,R)) = 0.N
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
h be Homomorphism of (id R),Free_LMod(X,R), N;
set J = id R;
h.(0.Free_LMod(X,R)) = h.((0.R) * (0.Free_LMod(X,R))) by VECTSP_1:14
.= (J.(0.R)) * (h.(0.Free_LMod(X,R))) by MOD_4:def 17
.= 0.N by VECTSP_1:14;
hence thesis;
end;
registration
let R be Ring, M,N be LeftMod of R;
let h be Function of the carrier of M, the carrier of N;
let s be FinSequence of the carrier of M;
cluster h*s -> FinSequence-like (the carrier of N)-valued;
coherence;
end;
theorem Th25:
for D,E be non empty set, h be Function of D,E, p be FinSequence of D,
d be Element of D holds h*(p^<*d*>) = (h*p)^<*h.d*>
proof
let D,E be non empty set, h be Function of D,E, p be FinSequence of D,
d be Element of D;
set q = h*(p^<*d*>), r = (h*p)^<*h.d*>, i = len p + 1;
A1: len q = len(p^<*d*>) by FINSEQ_2:33;
A2: len(h*p) = len p by FINSEQ_2:33;
A3: len(p^<*d*>) = i by FINSEQ_2:16; then
A4: dom q = Seg i by A1,FINSEQ_1:def 3;
reconsider p1 = p^<*d*> as FinSequence of D;
A5: dom p1 = Seg i by A3, FINSEQ_1:def 3;
A6: for j be object st j in dom q holds (h*p1).j = r.j
proof
let j be object;
A7: Seg len p = dom p by FINSEQ_1:def 3;
A8: Seg len(h*p) = dom(h*p) by FINSEQ_1:def 3;
assume
A9: j in dom q; then
per cases by A4,A7,FINSEQ_2:7;
suppose
A10: j in dom p;
(h*(p^<*d*>)).j = h.(p1.j) by A5,A4,A9,FUNCT_1:13
.= h.(p.j) by A10,FINSEQ_1:def 7
.= (h*p).j by A2,A7,A8,A10,FUNCT_1:12
.= r.j by A2,A7,A8,A10,FINSEQ_1:def 7;
hence thesis;
end;
suppose
A11: j = i;
(h*(p^<*d*>)).j = h.(p1.j) by A5,A4,A9,FUNCT_1:13 .= r.j by A2,A11;
hence thesis;
end;
end;
len q = len (p^<*d*>) by FINSEQ_2:33 .= len p + 1 by FINSEQ_2:16
.= len(h*p) + 1 by FINSEQ_2:33 .= len r by FINSEQ_2:16;
hence thesis by A6,FINSEQ_3:29;
end;
Lm39:
for V being non empty right_zeroed addLoopStr,
W being non empty add-associative right_zeroed right_complementable
addLoopStr,
h being Function of the carrier of V, the carrier of W
st h is additive holds h.(0.V) = 0.W
proof
let V be non empty right_zeroed addLoopStr,
W be non empty add-associative right_zeroed right_complementable
addLoopStr,
h be Function of the carrier of V, the carrier of W;
set z = 0.V;
assume
A1: h is additive;
h.z = h.(z+z) by RLVECT_1:def 4
.= h.z + h.z by A1;
hence thesis by RLVECT_1:9;
end;
theorem Th26:
for M,N being non empty add-associative right_zeroed right_complementable
addLoopStr,
h being Function of the carrier of M, the carrier of N,
s being FinSequence of the carrier of M
st h is additive
holds h.(Sum s) = Sum(h*s)
proof
let M,N be non empty add-associative right_zeroed right_complementable
addLoopStr,
h be Function of the carrier of M, the carrier of N,
s be FinSequence of the carrier of M;
assume
A1: h is additive;
defpred P[Nat] means
for s being FinSequence of the carrier of M
st len s = $1 holds h.(Sum s) = Sum(h*s);
A2: P[0]
proof
let s be FinSequence of the carrier of M;
assume
A3: len s = 0; then
Sum s = 0.M by RLVECT_1:75; then
A5: h.(Sum s) = 0.N by A1, Lm39;
s = <*>the carrier of M by A3; then
h*s = <*>the carrier of N;
hence thesis by A5, RLVECT_1:43;
end;
A6: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A7: P[n];
let s be FinSequence of the carrier of M;
set s0 = s|n;
assume
A8: len s = n+1; then
A9: len s0 = n by FINSEQ_1:59, NAT_1:11;
A10: 1 <= n+1 <= len s by A8, NAT_1:11; then
A11: s/.(n+1) = s.(n+1) by FINSEQ_4:15;
n+1 in Seg len s by A10; then
n+1 in dom s by FINSEQ_1:def 3; then
reconsider v = s.(n+1) as Element of M by FINSEQ_2:11;
A12: h*s = h*(s0^<*v*>) by A8, A11, FINSEQ_5:21
.= (h*s0)^<*h.v*> by FINSEQOP:8;
h.(Sum s) = h.(Sum(s0^<*v*>)) by A8, A11, FINSEQ_5:21
.= h.(Sum s0 + v) by FVSUM_1:71
.= h.(Sum s0) + h.v by A1
.= Sum(h*s0) + h.v by A7, A9
.= Sum(h*s) by A12,FVSUM_1:71;
hence thesis;
end;
A13: for n be Nat holds P[n] from NAT_1:sch 2(A2, A6);
len s is Nat;
hence thesis by A13;
end;
Lm40:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
h be Homomorphism of (id R), Free_LMod(X,R), N,
s be FinSequence of the carrier of Free_LMod(X,R)
holds h.(Sum s) = Sum(h*s)
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
h be Homomorphism of id R, Free_LMod(X,R), N,
s be FinSequence of the carrier of Free_LMod(X,R);
defpred P[Nat] means
for s be FinSequence of the carrier of Free_LMod(X,R) st len s = $1 holds
h.(Sum s) = Sum(h*s);
A1: P[0]
proof
let s be FinSequence of the carrier of Free_LMod(X,R);
assume
A2: len s = 0; then
s = <*>(the carrier of Free_LMod(X,R)); then
A3: Sum s = 0.Free_LMod(X,R) by RLVECT_1:43;
h*s = <*>(the carrier of N) by A2,FINSEQ_2:33; then
Sum(h*s) = 0.N by RLVECT_1:43;
hence thesis by A3,Lm38;
end;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
let s be FinSequence of the carrier of Free_LMod(X,R);
assume
A6: len s = k+1; then
consider t be FinSequence of the carrier of Free_LMod(X,R),
d be Element of Free_LMod(X,R) such that
A7: s = t^<*d*> by FINSEQ_2:19;
A8: k+1 = len t +1 by A6,A7,FINSEQ_2:16;
Sum s = Sum t + d by A7,FVSUM_1:71; then
A9: h.(Sum s) = h.(Sum t) + h.d by MOD_4:def 17;
A10: h*(t^<*d*>) = (h*t)^<*h.d*> by Th25;
thus h.(Sum s) = Sum(h*t) + h.d by A9,A5,A8
.= Sum(h*s) by A7,A10,FVSUM_1:71;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A4); then
P[len s];
hence thesis;
end;
Lm41:
for R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N,
f1,f2 be Homomorphism of (id R),Free_LMod(X,R), N
st f1 * (IotaMap(X,R)) = v & f2 * (IotaMap(X,R)) = v
holds f1 = f2
proof
let R be non degenerated Ring, X be non empty set, N be LeftMod of R,
v be Function of X, the carrier of N,
f1,f2 be Homomorphism of (id R),Free_LMod(X,R), N;
assume that
A1: f1 * (IotaMap(X,R)) = v and
A2: f2 * (IotaMap(X,R)) = v;
for a being Element of Free_LMod(X,R) holds f1.a = f2.a
proof
let a be Element of Free_LMod(X,R);
set s = F_idxseq(a);
dom f1 = the carrier of Free_LMod(X,R) by FUNCT_2:def 1; then
A5: rng s c= dom f1;
dom f2 = the carrier of Free_LMod(X,R) by FUNCT_2:def 1; then
A6: rng s c= dom f2;
A7: f1*s = f2*s
proof
A8: dom (f1*s) = dom s by A5,RELAT_1:27
.= dom (f2*s) by A6,RELAT_1:27;
for i be object st i in dom (f1*s) holds (f1*s).i = (f2*s).i
proof
let i be object;
assume
A9: i in dom (f1*s); then
reconsider k = i as Nat;
A10: k in dom s by A9,FUNCT_1:11;
reconsider ak = s/.k as Element of Free_LMod(X,R);
A11: dom s = Seg len s by FINSEQ_1:def 3
.= Seg len idxseq a by Def24
.= dom idxseq a by FINSEQ_1:def 3; then
reconsider xk = (idxseq a).k as Element of X
by A9,FUNCT_1:11,FINSEQ_2:11;
A12: Support @ak = {xk} by A11,A9,FUNCT_1:11,Lm24;
reconsider r = @ak.xk as Element of R;
f1.(r * ((IotaMap(X,R)).xk)) = ((id R).r) * (f1.((IotaMap(X,R)).xk))
by MOD_4:def 17; then
A13: f1.ak = r * (f1.((IotaMap(X,R)).xk)) by A12,Lm26;
f2.(r * ((IotaMap(X,R)).xk)) = ((id R).r) * (f2.((IotaMap(X,R)).xk))
by MOD_4:def 17; then
A14: f2.ak = r * (f2.((IotaMap(X,R)).xk)) by A12,Lm26;
(f1*s).i = f1.(s.k) by A9,FUNCT_1:12
.= f1.ak by A10,PARTFUN1:def 6
.= r * (v.xk) by A13,A1,FUNCT_2:15
.= f2.ak by A14,A2,FUNCT_2:15
.= f2.(s.k) by A10,PARTFUN1:def 6
.= (f2*s).i by A8,A9,FUNCT_1:12;
hence thesis;
end;
hence thesis by A8;
end;
f1.a = f1.(Sum s) by Th15
.= Sum(f2*s) by A7,Lm40
.= f2.(Sum s) by Lm40
.= f2.a by Th15;
hence thesis;
end;
hence thesis;
end;
::$MR The map $\mathrm{IotaMap}(X,R)$ satisfies the universal mapping property of the free module on $X$.
theorem
for R be non degenerated Ring, X be non empty set
holds IotaMap(X,R) is universal
proof
let R be non degenerated Ring, X be non empty set;
let N be LeftMod of R, v be Function of X, the carrier of N;
reconsider F = Phi(v) as Homomorphism of (id R),Free_LMod(X,R), N by Th23;
take F;
thus F * (IotaMap(X,R)) = v by Th24;
let f1,f2 be Homomorphism of (id R),Free_LMod(X,R), N;
assume f1 * (IotaMap(X,R)) = v & f2 * (IotaMap(X,R)) = v;
hence thesis by Lm41;
end;
Lm42:
for R be non degenerated Ring, X be non empty set,
f be Element of Free_LMod(X,R),i be Nat st i in dom F_idxseq(f)
holds (F_idxseq(f))/.i in Lin(rng IotaMap(X,R))
proof
let R be non degenerated Ring, X be non empty set,
f be Element of Free_LMod(X,R), i be Nat;
assume
A1: i in dom F_idxseq(f);
set g = (F_idxseq(f))/.i;
A2: dom F_idxseq f = Seg len F_idxseq(f) by FINSEQ_1:def 3
.= Seg len idxseq(f) by Def24
.= dom idxseq(f) by FINSEQ_1:def 3;
reconsider x = (idxseq(f)).i as Element of X by A1,A2,FINSEQ_2:11;
A3: Support @g = {x} by A1,A2, Lm24;
set W = Lin(rng IotaMap(X,R));
IotaMap(X,R).x in W by FUNCT_2:4, VECTSP_7:8; then
(@g.x) * (IotaMap(X,R).x) in W by VECTSP_4:21;
hence thesis by A3, Lm26;
end;
begin :: Linear Independence and Basis
reserve a for Nat, p for FinSequence;
theorem Th28:
for R be non degenerated Ring, X be non empty set,
f be Element of Free_LMod(X,R) holds f in Lin(rng IotaMap(X,R))
proof
let R be non degenerated Ring, X be non empty set,
f be Element of Free_LMod(X,R);
set s = F_idxseq(f);
set W = Lin rng IotaMap(X,R);
A1: for i be Nat st i in dom s holds s/.i in W by Lm42;
Sum s in W
proof
defpred P[Nat] means
for t be FinSequence of the carrier of Free_LMod(X,R) st
len t = $1 &
(for j be Nat st j in dom t holds t/.j in W) holds Sum t in W;
A3: P[0]
proof
let t be FinSequence of the carrier of Free_LMod(X,R);
assume that
A4: len t = 0 and
for j be Nat st j in dom t holds t/.j in W;
Sum t = 0.(Free_LMod(X,R)) by A4, RLVECT_1:75;
hence thesis by VECTSP_4:17;
end;
A5: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A6: P[n];
let t be FinSequence of the carrier of Free_LMod(X,R);
assume that
A7: len t = n+1 and
A8: for j be Nat st j in dom t holds t/.j in W;
set g0 = t | Seg n;
A9: g0 is FinSequence by FINSEQ_1:15;
A10: rng g0 c= the carrier of Free_LMod(X,R);
reconsider g = g0 as FinSequence of the carrier of Free_LMod(X,R)
by A9, A10, FINSEQ_1:def 4;
A11: n <= len t by A7, NAT_1:11; then
A12: len g = n by FINSEQ_1:17;
A13: for j be Nat st j in dom g holds g/.j in W
proof
let j be Nat;
assume
A14: j in dom g; then
A15: j in Seg n by FINSEQ_1:17, A11;
Seg n c= Seg(n+1) by NAT_1:11,FINSEQ_1:5; then
j in Seg(n+1) by A15; then
A16: j in dom t by A7, FINSEQ_1:def 3;
g/.j = g.j by A14, PARTFUN1:def 6
.= t.j by A15, FUNCT_1:49
.= t/.j by A16, PARTFUN1:def 6;
hence thesis by A16, A8;
end;
A17: Sum g in W by A6, A12, A13;
n+1 in Seg len t by A7,FINSEQ_1:4; then
A18: n+1 in dom t by FINSEQ_1:def 3; then
t/.(n+1) in W by A8; then
A20: t.(n+1) in W by A18, PARTFUN1:def 6;
Seg(n+1) = dom t by A7,FINSEQ_1:def 3; then
A21: t = t | Seg(n+1);
t.(n+1) in rng t by FUNCT_1:3,A18; then
reconsider tn = t.(n+1) as Element of Free_LMod(X,R);
t = g^<* t.(n+1) *> by A18, FINSEQ_5:10, A21; then
Sum t = Sum g + tn by FVSUM_1:71;
hence Sum t in W by A17, A20, VECTSP_4:20;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A3, A5); then
P[len s];
hence thesis by A1;
end;
hence thesis by Th15;
end;
theorem Th29:
for R be non degenerated Ring, X be non empty set holds
Lin rng IotaMap(X,R) = the ModuleStr of Free_LMod(X,R)
proof
let R be non degenerated Ring, X be non empty set;
reconsider V = Free_LMod(X,R) as strict LeftMod of R;
reconsider W = Lin(rng IotaMap(X,R)) as strict Submodule of V;
for v being Vector of V holds v in W iff v in V by Th28;
hence thesis by ZMODUL01:48;
end;
Lm43:
for M be non empty addLoopStr, p be FinSequence of the carrier of M,
n,i be Nat st n in dom p & i in dom ((p|(n-'1))^(p/^n)) holds
(i <= n-'1 implies ((p|(n-'1))^(p/^n)).i = p.i) &
(i > n-'1 implies ((p|(n-'1))^(p/^n)).i = p.(i+1)) &
i+1 in dom p & len ((p|(n-'1))^(p/^n)) = len p -1
proof
let M be non empty addLoopStr, p be FinSequence of the carrier of M,
n,i be Nat;
set a = p|(n-'1), b = p/^n, q = a^b;
assume that
A1: n in dom p and
A2: i in dom ((p|(n-'1))^(p/^n));
dom p = Seg len p by FINSEQ_1:def 3; then
A4: 1 <= n <= len p by A1,FINSEQ_1:1;
A5: n <= len p by A1,FINSEQ_3:25; then
A6: len a = n-'1 by FINSEQ_1:59,NAT_D:44;
A7: len p -'n = len p - n by A5,XREAL_1:233;
A8: len b = (len p) - n by A5,RFINSEQ:def 1
.= len p -'n by A5,XREAL_1:233; then
A9: dom b = Seg (len p -' n) by FINSEQ_1:def 3;
A10: len q = len a + len b by FINSEQ_1:22
.= n -'1 + (len p - n) by A6,A8,A5,XREAL_1:233
.= (n - 1) + (len p - n) by A4,XREAL_1:233
.= len p - 1;
A11: dom q = Seg len q by FINSEQ_1:def 3; then
1 <= i <= len p -1 by A10,A2,FINSEQ_1:1; then
A12: 1+1 <= i+1 <= (len p -1) + 1 by XREAL_1:6;
1 <= i+1 by NAT_1:14; then
A13: i+1 in Seg len p by A12; then
A14: i+1 in dom p by FINSEQ_1:def 3;
A15: i <= n-'1 implies q.i = p.i
proof
assume
A16: i <= n-'1;
1 <= i by A2,FINSEQ_3:25; then
i in Seg(n-'1) by A16; then
i in dom a by A6,FINSEQ_1:def 3; then
q.i = a.i by FINSEQ_1:def 7
.= p.i by A16,FINSEQ_3:112;
hence thesis;
end;
i > n-'1 implies q.i = p.(i+1)
proof
assume
A18: i > n-'1; then
reconsider j = i - (n-'1) as Nat by NAT_1:21;
A19: i - (n-'1) > (n -' 1)-(n -' 1) by A18,XREAL_1:14; then
A20: j >= 1 by NAT_1:14;
A21: i <= len p -1 by A11,A10,A2,FINSEQ_1:1;
A22: len a + 0 < len a + j by A19,XREAL_1:8;
A23: i <= len (a^b) by A11,A2,FINSEQ_1:1;
A24: j + n = i -(n-1) + n by A4,XREAL_1:233 .= i +1;
len p -1 - (n-'1) = len p -1 - (n-1) by A4,XREAL_1:233
.= len p - n; then
j <= len p - n by A21,XREAL_1:6; then
A25: j in dom b by A20,A9,A7; then
(p/^n).j = (p/^n)/.j by PARTFUN1:def 6
.= p/.(i+1) by A24,FINSEQ_5:27,A25
.= p.(i+1) by A14,PARTFUN1:def 6;
hence thesis by FINSEQ_1:24,A6,A22,A23;
end;
hence thesis by A15,A13,FINSEQ_1:def 3, A10;
end;
Lm45:
for N be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, p be FinSequence of the carrier of N, k be Nat
st k in dom p & (for i be Nat st i in dom p & i <> k holds p.i = 0.N)
holds Sum p = p/.k
proof
let N be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr,
p be FinSequence of the carrier of N,
k be Nat;
assume that
A1: k in dom p and
A2: for i be Nat st i in dom p & i <> k holds p.i = 0.N;
A3: dom p = Seg len p by FINSEQ_1:def 3;
A6: 1 <= k <= len p by A3,A1,FINSEQ_1:1;
Seg len p <> {} by A1,FINSEQ_1:def 3; then
len p <> 0; then
A7: len p -'1 = len p - 1 by NAT_1:14,XREAL_1:233;
A8: Sum p = Sum (Del(p,k,k)) + p/.k by A1, Lm37;
A9: for i be Element of NAT st i in dom Del(p,k,k) holds
(Del(p,k,k)).i = 0.N
proof
let i be Element of NAT;
assume
A10: i in dom Del(p,k,k);
A11: dom Del(p,k,k) = Seg len Del(p,k,k) by FINSEQ_1:def 3
.= Seg ((len p) -' 1) by A1,A10,Lm43,A7;
per cases;
suppose
A12: i <= k-'1; then
A13: (Del(p,k,k)).i = p.i by A1,A10,Lm43;
k <= len p by A1,FINSEQ_3:25; then
A14: k-'1 <= len p by NAT_D:44;
1 <= i <= len p by A11,FINSEQ_1:1,A10,A14,A12,XXREAL_0:2;
then
i in Seg len p; then
A15: i in dom p by FINSEQ_1:def 3;
A16: k-1 < k by XREAL_1:30;
i <= k -1 by A12,A6,XREAL_1:233;
hence (Del(p,k,k)).i = 0.N by A13,A2,A15,A16;
end;
suppose
A18: i > k-'1; then
A19: (Del(p,k,k)).i = p.(i+1) by A1,A10,Lm43;
A20: i+1 in dom p by A1,A10,Lm43;
k -1 < i by A6,XREAL_1:233,A18; then
i+1 <> k;
hence (Del(p,k,k)).i = 0.N by A19,A2,A20;
end;
end;
Sum Del(p,k,k) = 0.N by A9,MATRIX_3:35;
hence Sum p = p/.k by A8;
end;
theorem Th30:
for R be non degenerated Ring, X be non empty set holds
rng IotaMap(X,R) is linearly-independent
proof
let R be non degenerated Ring, X be non empty set;
set V = Free_LMod(X,R);
set A = rng IotaMap(X,R);
for l being Linear_Combination of A st Sum l = 0.V holds Carrier l = {}
proof
let l be Linear_Combination of A;
assume
A1: Sum l = 0.V;
assume Carrier l <> {}; then
consider y being object such that
A3: y in Carrier l by XBOOLE_0:def 1;
reconsider v0 = y as Element of V by A3;
A4: Carrier l c= A by VECTSP_6:def 4;
consider x0 being object such that
A5: x0 in dom IotaMap(X,R) & IotaMap(X,R).x0 = v0 by A3,A4,FUNCT_1:def 3;
reconsider x = x0 as Element of X by A5;
consider F being FinSequence of the carrier of V such that
A6: F is one-to-one and
A7: rng F = Carrier l and
A8: Sum l = Sum (l (#) F) by VECTSP_6:def 6;
set s = l (#) F;
set h = ev_(x,R);
A9: rng s c= dom h
proof
let y be object;
assume y in rng s; then
consider t being object such that
A11: t in dom s & s.t = y by FUNCT_1:def 3;
y in the carrier of V by A11,FINSEQ_2:11;
hence thesis by FUNCT_2:def 1;
end;
len s = len F by VECTSP_6:def 5; then
A12: dom s = dom F by FINSEQ_3:29;
A13: h is additive by Th8;
A14: h.(Sum s) = 0.R by Th9,A8,A1;
consider k being object such that
A15: k in dom F & F.k = v0 by A3,A7,FUNCT_1:def 3;
len s = len F by VECTSP_6:def 5; then
A16: dom s = Seg len F by FINSEQ_1:def 3 .= dom F by FINSEQ_1:def 3;
A17: v0 = Iota(x,R) by A5,Def19;
A18: (F/.k) = v0 by A15,PARTFUN1:def 6;
A19: (h*s).k = h.(s.k) by A15,A16,FUNCT_1:13
.= h.(l.(F/.k) * F/.k) by A15,A16,VECTSP_6:def 5
.= l.v0 * h.v0 by A18,Lm22
.= l.v0 * 1.R by Lm20,A17
.= l.v0;
A20: for i be Nat st i in dom (h*s) & i <> k holds (h*s).i = 0.R
proof
let i be Nat;
assume that
A21: i in dom (h*s) and
A22: i <> k;
A23: i in dom F by A21,A9,RELAT_1:27,A12; then
reconsider w = F.i as Element of V by FINSEQ_2:11;
w in Carrier l by A7,A23,FUNCT_1:3; then
consider z being object such that
A25: z in dom IotaMap(X,R) & IotaMap(X,R).z = w by A4,FUNCT_1:def 3;
reconsider x1 = z as Element of X by A25;
A26: x1 <> x by A5,A6,A23,A15,A22,A25;
w = Iota(x1,R) by A25,Def19; then
A27: h.w = 0.R by A26, Lm21;
len (h*s) = len s by FINSEQ_2:33; then
i in dom s by A21,FINSEQ_3:29; then
(h*s).i = h.(s.i) by FUNCT_1:13
.= h.((l.w) * w) by A23, VECTSP_6:8
.= (l.w) *(h.w) by Lm22
.= 0.R by A27;
hence thesis;
end;
A30: k in dom (h*s) by A15,A16,A9,RELAT_1:27; then
A31: Sum(h*s) = (h*s)/.k by A20, Lm45
.= (h*s).k by A30,PARTFUN1:def 6;
l.v0 <> 0.R by A3,VECTSP_6:2;
hence contradiction by A13,Th26,A14,A19,A31;
end;
hence thesis;
end;
theorem Th31:
for R be non degenerated Ring, X be non empty set holds
rng IotaMap(X,R) is base by Th29,Th30;
::$N as a corollary of Th34, using the basis-theoretic definition of free modules.
theorem Th32:
for R be non degenerated Ring, X be non empty set
holds Free_LMod(X,R) is free
proof
let R be non degenerated Ring, X be non empty set;
reconsider S = rng IotaMap(X,R) as Subset of Free_LMod(X,R);
S is base by Th31;
hence thesis;
end;
begin :: The free module generated by the empty set
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The empty set generates the trivial left module.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
LmTriv:
fs_Funcs({},R) = {{}} & 0_Funcs({},R) = {}
proof
A0: Funcs({},the carrier of R) = {{}} by FUNCT_5:57;
0_Funcs({},R) is finite-Support & Support 0_Funcs({},R) = {} by Lm8; then
0_Funcs({},R) in fs_Funcs({},R); then
{{}} c= fs_Funcs({},R) by TARSKI:def 1;
hence thesis by A0;
end;
LmTriv2:
fs_ADD({},R) = op2 & fs_LMULT({},R) = pr2(the carrier of R,{0})
proof
fs_Funcs({},R) = {{}} by LmTriv;
hence thesis by FUNCT_2:51;
end;
theorem ThTriv1:
FS_Funcs({},R) = TrivialLMod(R)
proof
A1: the carrier of FS_Funcs({},R) = the carrier of TrivialLMod(R) by LmTriv;
the addF of FS_Funcs({},R) = op2 by LmTriv2;
hence thesis by A1,LmTriv2;
end;
theorem Th33:
Free_LMod({},R) is free
proof
set V = TrivialLMod(R);
B0: Free_LMod({},R) = TrivialLMod(R) by ThTriv1;
reconsider W1 = V as strict Subspace of V by VECTSP_4:24;
reconsider W2 = (0).V as strict Subspace of V;
the carrier of W2 = {0.V} by VECTSP_4:def 3
.= {0}; then
W1 = W2 by VECTSP_4:29; then
{}(the carrier of V) is base by VECTSP_7:9;
hence thesis by B0;
end;
theorem Th34:
for R be non degenerated Ring, X be set
holds Free_LMod(X,R) is free
proof
let R be non degenerated Ring, X be set;
per cases;
suppose X <> {};
hence thesis by Th32;
end;
suppose X = {};
hence thesis by Th33;
end;
end;
registration
let R be non degenerated Ring, X be set;
cluster Free_LMod(X,R) -> free;
coherence by Th34;
end;