:: An Explicit Construction of Free Modules in Mizar
:: by Yasushige Watase
::
:: Received August 2, 2026
:: Copyright (c) 2026 Association of Mizar Users

definition

let R be Ring;
let X be set ;
let N be LeftMod of R;

func 0_Funcs (X,N) -> Element of Funcs (X, the carrier of N) equals :: LMODFREE:def 1
X --> (0. N);

coherence
X --> (0. N) is Element of Funcs (X, the carrier of N) by FUNCT_2:8;

end;

:: deftheorem defines 0_Funcs LMODFREE:def 1 :
for R being Ring
for X being set
for N being LeftMod of R holds 0_Funcs (X,N) = X --> (0. N);

registration

let R be Ring;
let X be set ;
let N be LeftMod of R;

cluster Funcs (X, the carrier of N) -> non empty ;

coherence
not Funcs (X, the carrier of N) is empty ;

end;

definition

let R be Ring;
let X be set ;
let N be LeftMod of R;

func ADD (X,N) -> BinOp of (Funcs (X, the carrier of N)) means :: LMODFREE:def 2
for f, g being Element of Funcs (X, the carrier of N) holds it . (f,g) = the addF of N .: (f,g);

existence
ex b₁ being BinOp of (Funcs (X, the carrier of N)) st
for f, g being Element of Funcs (X, the carrier of N) holds b₁ . (f,g) = the addF of N .: (f,g)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (X, the carrier of N)) st ( for f, g being Element of Funcs (X, the carrier of N) holds b₁ . (f,g) = the addF of N .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of N) holds b₂ . (f,g) = the addF of N .: (f,g) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines ADD LMODFREE:def 2 :
for R being Ring
for X being set
for N being LeftMod of R
for b₄ being BinOp of (Funcs (X, the carrier of N)) holds
( b₄ = ADD (X,N) iff for f, g being Element of Funcs (X, the carrier of N) holds b₄ . (f,g) = the addF of N .: (f,g) );

definition

let R be Ring;
let X be set ;
let N be LeftMod of R;
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;
:: original: [;]
redefine func F [;] (a,f) -> Element of Funcs (X, the carrier of N);
coherence
F [;] (a,f) is Element of Funcs (X, the carrier of N)

proof 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 be Ring;
let X be set ;
let N be LeftMod of R;

func LMULT (X,N) -> Function of [: the carrier of R,(Funcs (X, the carrier of N)):],(Funcs (X, the carrier of N)) means :: LMODFREE:def 3
for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of N)
for x being object st x in X holds
(it . (a,f)) . x = the lmult of N . (a,(f . x));

existence
ex b₁ being Function of [: the carrier of R,(Funcs (X, the carrier of N)):],(Funcs (X, the carrier of N)) st
for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of N)
for x being object st x in X holds
(b₁ . (a,f)) . x = the lmult of N . (a,(f . x))

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of R,(Funcs (X, the carrier of N)):],(Funcs (X, the carrier of N)) st ( for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of N)
for x being object st x in X holds
(b₁ . (a,f)) . x = the lmult of N . (a,(f . x)) ) & ( for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of N)
for x being object st x in X holds
(b₂ . (a,f)) . x = the lmult of N . (a,(f . x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines LMULT LMODFREE:def 3 :
for R being Ring
for X being set
for N being LeftMod of R
for b₄ being Function of [: the carrier of R,(Funcs (X, the carrier of N)):],(Funcs (X, the carrier of N)) holds
( b₄ = LMULT (X,N) iff for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of N)
for x being object st x in X holds
(b₄ . (a,f)) . x = the lmult of N . (a,(f . x)) );

definition

let R be Ring;
let X be set ;
let N be LeftMod of R;

func Func_Mod (X,N) -> non empty ModuleStr over R equals :: LMODFREE:def 4
ModuleStr(# (Funcs (X, the carrier of N)),(ADD (X,N)),(0_Funcs (X,N)),(LMULT (X,N)) #);

coherence
ModuleStr(# (Funcs (X, the carrier of N)),(ADD (X,N)),(0_Funcs (X,N)),(LMULT (X,N)) #) is non empty ModuleStr over R ;

end;

:: deftheorem defines Func_Mod LMODFREE:def 4 :
for R being Ring
for X being set
for N being LeftMod of R holds Func_Mod (X,N) = ModuleStr(# (Funcs (X, the carrier of N)),(ADD (X,N)),(0_Funcs (X,N)),(LMULT (X,N)) #);

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Funcs(X,R)/finite Support -> R-Module
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::$INSERT Module structure on function spaces & on finitely supported functions.

definition

let R be Ring;
let X be set ;

func 0_Funcs (X,R) -> Element of Funcs (X, the carrier of R) equals :: LMODFREE:def 5
X --> (0. R);

coherence
X --> (0. R) is Element of Funcs (X, the carrier of R) by FUNCT_2:8;

end;

:: deftheorem defines 0_Funcs LMODFREE:def 5 :
for R being Ring
for X being set holds 0_Funcs (X,R) = X --> (0. R);

definition

let R be Ring;
let X be set ;

func ADD (X,R) -> BinOp of (Funcs (X, the carrier of R)) means :Def6: :: LMODFREE:def 6
for f, g being Element of Funcs (X, the carrier of R) holds it . (f,g) = the addF of R .: (f,g);

existence
ex b₁ being BinOp of (Funcs (X, the carrier of R)) st
for f, g being Element of Funcs (X, the carrier of R) holds b₁ . (f,g) = the addF of R .: (f,g)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (X, the carrier of R)) st ( for f, g being Element of Funcs (X, the carrier of R) holds b₁ . (f,g) = the addF of R .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of R) holds b₂ . (f,g) = the addF of R .: (f,g) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ADD LMODFREE:def 6 :
for R being Ring
for X being set
for b₃ being BinOp of (Funcs (X, the carrier of R)) holds
( b₃ = ADD (X,R) iff for f, g being Element of Funcs (X, the carrier of R) holds b₃ . (f,g) = the addF of R .: (f,g) );

theorem Th1: :: LMODFREE:1

for R being Ring
for X being set
for f, g, h being Element of Funcs (X, the carrier of R) 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 end;

definition

let R be Ring;
let X be set ;
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;
:: original: [;]
redefine func F [;] (a,f) -> Element of Funcs (X, the carrier of R);
coherence
F [;] (a,f) is Element of Funcs (X, the carrier of R)

proof end;

end;

definition

let R be Ring;
let X be set ;

func LMULT (X,R) -> Function of [: the carrier of R,(Funcs (X, the carrier of R)):],(Funcs (X, the carrier of R)) means :Def7: :: LMODFREE:def 7
for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R)
for x being object st x in X holds
(it . (a,f)) . x = the multF of R . (a,(f . x));

existence
ex b₁ being Function of [: the carrier of R,(Funcs (X, the carrier of R)):],(Funcs (X, the carrier of R)) st
for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R)
for x being object st x in X holds
(b₁ . (a,f)) . x = the multF of R . (a,(f . x))

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of R,(Funcs (X, the carrier of R)):],(Funcs (X, the carrier of R)) st ( for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R)
for x being object st x in X holds
(b₁ . (a,f)) . x = the multF of R . (a,(f . x)) ) & ( for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R)
for x being object st x in X holds
(b₂ . (a,f)) . x = the multF of R . (a,(f . x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines LMULT LMODFREE:def 7 :
for R being Ring
for X being set
for b₃ being Function of [: the carrier of R,(Funcs (X, the carrier of R)):],(Funcs (X, the carrier of R)) holds
( b₃ = LMULT (X,R) iff for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R)
for x being object st x in X holds
(b₃ . (a,f)) . x = the multF of R . (a,(f . x)) );

theorem Th2: :: LMODFREE:2

for R being Ring
for X being set
for a being Element of the carrier of R
for f, h being Element of Funcs (X, the carrier of R) holds
( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) )

proof end;

Lm2: for R being Ring
for X being set
for f, g being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,g) = (ADD (X,R)) . (g,f)

proof end;

Lm3: for R being Ring
for X being set
for f, g, h being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,((ADD (X,R)) . (g,h))) = (ADD (X,R)) . (((ADD (X,R)) . (f,g)),h)

proof end;

Lm4: for R being Ring
for X being set
for a being Element of the carrier of R
for f, g being Element of Funcs (X, the carrier of R) holds (LMULT (X,R)) . (a,((ADD (X,R)) . (f,g))) = (ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (a,g)))

proof end;

Lm5: for R being Ring
for X being set
for a, b being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R) holds (LMULT (X,R)) . ((a + b),f) = (ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (b,f)))

proof end;

Lm6: for R being Ring
for X being set
for a, b being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R) holds (LMULT (X,R)) . ((a * b),f) = (LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))

proof end;

Lm7: for R being Ring
for X being set
for f being Element of Funcs (X, the carrier of R) holds (LMULT (X,R)) . ((1. R),f) = f

proof end;

definition

let R be Ring;
let X be set ;

func fs_Funcs (X,R) -> Subset of (Funcs (X, the carrier of R)) equals :: LMODFREE:def 8
{ x where x is Function of X, the carrier of R : x is finite-Support } ;

coherence
{ x where x is Function of X, the carrier of R : x is finite-Support } is Subset of (Funcs (X, the carrier of R))

proof end;

end;

:: deftheorem defines fs_Funcs LMODFREE:def 8 :
for R being Ring
for X being set holds fs_Funcs (X,R) = { x where x is Function of X, the carrier of R : x is finite-Support } ;

Lm8: for R being Ring
for X being set holds
( 0_Funcs (X,R) is finite-Support & Support (0_Funcs (X,R)) = {} )

proof end;

Lm9: for R being Ring
for X being set holds 0_Funcs (X,R) in fs_Funcs (X,R)

proof end;

registration

let R be Ring;
let X be set ;

cluster fs_Funcs (X,R) -> non empty ;

coherence
not fs_Funcs (X,R) is empty by Lm9;

end;

Lm10: for R being Ring
for X being set holds Support (X --> (0. R)) = {}

proof end;

registration

let R be Ring;
let X be set ;

cluster Relation-like X -defined the carrier of R -valued Function-like total quasi_total finite-Support for Element of bool [:X, the carrier of R:];

existence
ex b₁ being Function of X, the carrier of R st b₁ is finite-Support

proof end;

end;

theorem Th3: :: LMODFREE:3

for R being Ring
for X being set
for f, g being 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 end;

Lm11: for R being Ring
for X being set
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 end;

theorem Th4: :: LMODFREE:4

for R being Ring
for X being set
for a being Element of the carrier of R
for g being 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 end;

Lm12: for R being Ring
for X being set
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 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 :: LMODFREE:def 9
for f, g being Element of Funcs (X, the carrier of Y) holds it . (f,g) = the addF of Y .: (f,g);

existence
ex b₁ being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds b₁ . (f,g) = the addF of Y .: (f,g)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (X, the carrier of Y)) st ( for f, g being Element of Funcs (X, the carrier of Y) holds b₁ . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds b₂ . (f,g) = the addF of Y .: (f,g) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines FuncAdd LMODFREE:def 9 :
for X being non empty set
for Y being non empty addLoopStr
for b₃ being BinOp of (Funcs (X, the carrier of Y)) holds
( b₃ = FuncAdd (X,Y) iff for f, g being Element of Funcs (X, the carrier of Y) holds b₃ . (f,g) = the addF of Y .: (f,g) );

definition

let R be Ring;
let X be set ;

func fs_ADD (X,R) -> BinOp of (fs_Funcs (X,R)) equals :: LMODFREE:def 10
(ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):];

coherence
(ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):] is BinOp of (fs_Funcs (X,R))

proof end;

end;

:: deftheorem defines fs_ADD LMODFREE:def 10 :
for R being Ring
for X being set holds fs_ADD (X,R) = (ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):];

definition

let R be Ring;
let X be set ;

func fs_LMULT (X,R) -> Function of [: the carrier of R,(fs_Funcs (X,R)):],(fs_Funcs (X,R)) equals :: LMODFREE:def 11
(LMULT (X,R)) | [: the carrier of R,(fs_Funcs (X,R)):];

coherence
(LMULT (X,R)) | [: the carrier of R,(fs_Funcs (X,R)):] is Function of [: the carrier of R,(fs_Funcs (X,R)):],(fs_Funcs (X,R))

proof end;

end;

:: deftheorem defines fs_LMULT LMODFREE:def 11 :
for R being Ring
for X being set holds fs_LMULT (X,R) = (LMULT (X,R)) | [: the carrier of R,(fs_Funcs (X,R)):];

definition

let R be Ring;
let X be set ;

func 0_fs_Zero (X,R) -> Element of fs_Funcs (X,R) equals :: LMODFREE:def 12
0_Funcs (X,R);

correctness
coherence
0_Funcs (X,R) is Element of fs_Funcs (X,R);

proof end;

end;

:: deftheorem defines 0_fs_Zero LMODFREE:def 12 :
for R being Ring
for X being set holds 0_fs_Zero (X,R) = 0_Funcs (X,R);

:: The structure $\mathrm{FS\_Funcs}(X,R)$ forms a left $R$-module.

definition

let R be Ring;
let X be set ;

func FS_Funcs (X,R) -> non empty ModuleStr over R equals :: LMODFREE:def 13
ModuleStr(# (fs_Funcs (X,R)),(fs_ADD (X,R)),(0_fs_Zero (X,R)),(fs_LMULT (X,R)) #);

coherence
ModuleStr(# (fs_Funcs (X,R)),(fs_ADD (X,R)),(0_fs_Zero (X,R)),(fs_LMULT (X,R)) #) is non empty ModuleStr over R ;

end;

:: deftheorem defines FS_Funcs LMODFREE:def 13 :
for R being Ring
for X being set holds FS_Funcs (X,R) = ModuleStr(# (fs_Funcs (X,R)),(fs_ADD (X,R)),(0_fs_Zero (X,R)),(fs_LMULT (X,R)) #);

Lm13: for R being Ring
for X being set
for f being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,(0_Funcs (X,R))) = f

proof end;

Lm14: for R being Ring
for X being set
for f being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f))) = 0_Funcs (X,R)

proof end;

theorem Th5: :: LMODFREE:5

for R being Ring
for X being set
for v1, w1 being Element of Funcs (X, the carrier of R)
for v, w being Element of (FS_Funcs (X,R)) st v1 = v & w1 = w holds
v + w = (ADD (X,R)) . (v1,w1)

proof end;

Lm15: for R being Ring
for X being set
for a being Element of R
for f1 being Element of Funcs (X, the carrier of R)
for f being Element of (FS_Funcs (X,R)) st f1 = f holds
a * f = (LMULT (X,R)) . (a,f1)

proof end;

theorem Th6: :: LMODFREE:6

for R being Ring
for X being set holds FS_Funcs (X,R) is LeftMod of R

proof end;

registration

let R be Ring;
let X be set ;

cluster FS_Funcs (X,R) -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed left_zeroed ;

coherence
( FS_Funcs (X,R) is Abelian & FS_Funcs (X,R) is add-associative & FS_Funcs (X,R) is right_zeroed & FS_Funcs (X,R) is left_zeroed & FS_Funcs (X,R) is right_complementable & FS_Funcs (X,R) is vector-distributive & FS_Funcs (X,R) is scalar-distributive & FS_Funcs (X,R) is scalar-associative & FS_Funcs (X,R) is scalar-unital ) by Th6;

end;

:: The definition of Free Module $\mathcal{F}_{\mathrm{LMod}}(X)$

definition

let R be Ring;
let X be set ;

func Free_LMod (X,R) -> non empty ModuleStr over R equals :: LMODFREE:def 14
FS_Funcs (X,R);

coherence
FS_Funcs (X,R) is non empty ModuleStr over R ;

end;

:: deftheorem defines Free_LMod LMODFREE:def 14 :
for R being Ring
for X being set holds Free_LMod (X,R) = FS_Funcs (X,R);

registration

let R be Ring;
let X be set ;

cluster Free_LMod (X,R) -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed left_zeroed ;

coherence
( Free_LMod (X,R) is Abelian & Free_LMod (X,R) is add-associative & Free_LMod (X,R) is right_zeroed & Free_LMod (X,R) is left_zeroed & Free_LMod (X,R) is right_complementable & Free_LMod (X,R) is vector-distributive & Free_LMod (X,R) is scalar-distributive & Free_LMod (X,R) is scalar-associative & Free_LMod (X,R) is scalar-unital ) ;

end;

definition

let R be non degenerated Ring;
let X be non empty set ;
let f be Element of (Free_LMod (X,R));

func ~ f -> Element of fs_Funcs (X,R) equals :: LMODFREE:def 15
f;

coherence
f is Element of fs_Funcs (X,R) ;

end;

:: deftheorem defines ~ LMODFREE:def 15 :
for R being non degenerated Ring
for X being non empty set
for f being Element of (Free_LMod (X,R)) holds ~ f = f;

definition

let R be non degenerated Ring;
let X be non empty set ;
let f be Element of (Free_LMod (X,R));

func @ f -> Element of Funcs (X, the carrier of R) equals :: LMODFREE:def 16
f;

coherence
f is Element of Funcs (X, the carrier of R)

proof end;

end;

:: deftheorem defines @ LMODFREE:def 16 :
for R being non degenerated Ring
for X being non empty set
for f being Element of (Free_LMod (X,R)) holds @ f = f;

:: the canonical generator $\iota_X(x)$

definition

let X be non empty set ;
let R be non degenerated Ring;
let a be Element of X;

func iota (a,R) -> Function of X,([#] R) means :Def17: :: LMODFREE:def 17
for x being object st x in X holds
( ( x = a implies it . x = 1. R ) & ( x <> a implies it . x = 0. R ) );

existence
ex b₁ being Function of X,([#] R) st
for x being object st x in X holds
( ( x = a implies b₁ . x = 1. R ) & ( x <> a implies b₁ . x = 0. R ) )

proof end;

uniqueness
for b₁, b₂ being Function of X,([#] R) st ( for x being object st x in X holds
( ( x = a implies b₁ . x = 1. R ) & ( x <> a implies b₁ . x = 0. R ) ) ) & ( for x being object st x in X holds
( ( x = a implies b₂ . x = 1. R ) & ( x <> a implies b₂ . x = 0. R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines iota LMODFREE:def 17 :
for X being non empty set
for R being non degenerated Ring
for a being Element of X
for b₄ being Function of X,([#] R) holds
( b₄ = iota (a,R) iff for x being object st x in X holds
( ( x = a implies b₄ . x = 1. R ) & ( x <> a implies b₄ . x = 0. R ) ) );

registration

let X be non empty set ;
let R be non degenerated Ring;
let a be Element of X;

cluster iota (a,R) -> the carrier of R -valued ;

coherence
iota (a,R) is the carrier of R -valued ;

end;

Lm16: for R being non degenerated Ring
for X being non empty set
for z being Element of X holds Support (iota (z,R)) = {z}

proof end;

Lm17: for R being non degenerated Ring
for X being non empty set
for x being 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 end;

registration

let X be non empty set ;
let R be non degenerated Ring;
let a be Element of X;

cluster iota (a,R) -> finite-Support ;

coherence
iota (a,R) is finite-Support by Lm17;

end;

definition

let R be non degenerated Ring;
let X be non empty set ;
let x be Element of X;

func Iota (x,R) -> Element of (Free_LMod (X,R)) equals :: LMODFREE:def 18
iota (x,R);

coherence
iota (x,R) is Element of (Free_LMod (X,R)) by Lm17;

end;

:: deftheorem defines Iota LMODFREE:def 18 :
for R being non degenerated Ring
for X being non empty set
for x being Element of X holds Iota (x,R) = iota (x,R);

:: the induced injection $\iota_X : X \longrightarrow \mathcal{F}_{\mathrm{LMod}}(X)$

definition

let R be non degenerated Ring;
let X be non empty set ;

func IotaMap (X,R) -> Function of X,(Free_LMod (X,R)) means :Def19: :: LMODFREE:def 19
for x being Element of X holds it . x = Iota (x,R);

existence
ex b₁ being Function of X,(Free_LMod (X,R)) st
for x being Element of X holds b₁ . x = Iota (x,R)

proof end;

uniqueness
for b₁, b₂ being Function of X,(Free_LMod (X,R)) st ( for x being Element of X holds b₁ . x = Iota (x,R) ) & ( for x being Element of X holds b₂ . x = Iota (x,R) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines IotaMap LMODFREE:def 19 :
for R being non degenerated Ring
for X being non empty set
for b₃ being Function of X,(Free_LMod (X,R)) holds
( b₃ = IotaMap (X,R) iff for x being Element of X holds b₃ . x = Iota (x,R) );

registration

let R be non degenerated Ring;
let X be non empty set ;

cluster IotaMap (X,R) -> one-to-one ;

coherence
IotaMap (X,R) is one-to-one

proof end;

end;

definition

let R be non degenerated Ring;
let X be non empty set ;
let x be Element of X;

func ev_ (x,R) -> Function of (Free_LMod (X,R)),R means :Def20: :: LMODFREE:def 20
for f being Element of (Free_LMod (X,R)) holds it . f = (@ f) . x;

existence
ex b₁ being Function of (Free_LMod (X,R)),R st
for f being Element of (Free_LMod (X,R)) holds b₁ . f = (@ f) . x

proof end;

uniqueness
for b₁, b₂ being Function of (Free_LMod (X,R)),R st ( for f being Element of (Free_LMod (X,R)) holds b₁ . f = (@ f) . x ) & ( for f being Element of (Free_LMod (X,R)) holds b₂ . f = (@ f) . x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines ev_ LMODFREE:def 20 :
for R being non degenerated Ring
for X being non empty set
for x being Element of X
for b₄ being Function of (Free_LMod (X,R)),R holds
( b₄ = ev_ (x,R) iff for f being Element of (Free_LMod (X,R)) holds b₄ . f = (@ f) . x );

definition

let X be non empty set ;
let R be non degenerated Ring;
let f be Element of (Free_LMod (X,R));

func ev_iota f -> Function of X,(Free_LMod (X,R)) means :Def21: :: LMODFREE:def 21
for x being Element of X holds it . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x);

existence
ex b₁ being Function of X,(Free_LMod (X,R)) st
for x being Element of X holds b₁ . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,(Free_LMod (X,R)) st ( for x being Element of X holds b₁ . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) ) & ( for x being Element of X holds b₂ . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines ev_iota LMODFREE:def 21 :
for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for b₄ being Function of X,(Free_LMod (X,R)) holds
( b₄ = ev_iota f iff for x being Element of X holds b₄ . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) );

registration

let X be non empty set ;
let R be non degenerated Ring;
let f be Element of (Free_LMod (X,R));

cluster Support (@ f) -> finite for set ;

coherence
for b₁ being set st b₁ = Support (@ f) holds
b₁ is finite

proof end;

end;

registration

let X be non empty set ;
let R be non degenerated Ring;

cluster 0. (Free_LMod (X,R)) -> zero ;

coherence
0. (Free_LMod (X,R)) is zero ;

cluster non zero for Element of the carrier of (Free_LMod (X,R));

existence
not for b₁ being Element of (Free_LMod (X,R)) holds b₁ is zero

proof 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 be non empty set ;
let R be non degenerated Ring;
let f be Element of (Free_LMod (X,R));

func idxseq f -> FinSequence of X equals :: LMODFREE:def 22
canFS (Support (@ f));

coherence
canFS (Support (@ f)) is FinSequence of X

proof end;

end;

:: deftheorem defines idxseq LMODFREE:def 22 :
for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds idxseq f = canFS (Support (@ f));

Lm18: for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for x being Element of X holds
( x in Support (@ f) iff (ev_ (x,R)) . f <> 0. R )

proof end;

theorem :: LMODFREE:7

for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds Support (ev_iota f) = Support (@ f)

proof end;

Lm20: for R being non degenerated Ring
for X being non empty set
for x being Element of X holds (ev_ (x,R)) . (iota (x,R)) = 1. R

proof end;

Lm21: for R being non degenerated Ring
for X being non empty set
for x, y being Element of X st x <> y holds
(ev_ (x,R)) . (iota (y,R)) = 0. R

proof end;

definition

let X be non empty set ;
let R be non degenerated Ring;
let s be FinSequence of the carrier of (Free_LMod (X,R));
let x be Element of X;

func ev_ (s,x) -> FinSequence of the carrier of R means :Def23: :: LMODFREE:def 23
( dom it = dom s & ( for i being Nat st i in dom s holds
it . i = (ev_ (x,R)) . (s /. i) ) );

existence
ex b₁ being FinSequence of the carrier of R st
( dom b₁ = dom s & ( for i being Nat st i in dom s holds
b₁ . i = (ev_ (x,R)) . (s /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of R st dom b₁ = dom s & ( for i being Nat st i in dom s holds
b₁ . i = (ev_ (x,R)) . (s /. i) ) & dom b₂ = dom s & ( for i being Nat st i in dom s holds
b₂ . i = (ev_ (x,R)) . (s /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines ev_ LMODFREE:def 23 :
for X being non empty set
for R being non degenerated Ring
for s being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X
for b₅ being FinSequence of the carrier of R holds
( b₅ = ev_ (s,x) iff ( dom b₅ = dom s & ( for i being Nat st i in dom s holds
b₅ . i = (ev_ (x,R)) . (s /. i) ) ) );

theorem Th7: :: LMODFREE:8

for X being non empty set
for R being non degenerated Ring
for x being Element of X
for f being Element of (Free_LMod (X,R))
for a being Element of R holds (@ (a * f)) . x = a * ((@ f) . x)

proof end;

theorem Th8: :: LMODFREE:9

for X being non empty set
for R being non degenerated Ring
for x being Element of X
for f, g being 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 end;

Lm22: for R being non degenerated Ring
for X being non empty set
for x being Element of X
for a being Element of R
for f being Element of (Free_LMod (X,R)) holds (ev_ (x,R)) . (a * f) = a * ((ev_ (x,R)) . f)

proof end;

theorem Th9: :: LMODFREE:10

for X being non empty set
for R being non degenerated Ring
for x being Element of X holds (ev_ (x,R)) . (0. (Free_LMod (X,R))) = 0. R

proof end;

theorem Th10: :: LMODFREE:11

for X being non empty set
for R being non degenerated Ring
for N0 being Nat
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X st len F = N0 + 1 holds
ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>

proof end;

theorem Th11: :: LMODFREE:12

for X being non empty set
for R being non degenerated Ring
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X holds (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

proof end;

definition

let X be non empty set ;
let R be non degenerated Ring;
let f be Element of (Free_LMod (X,R));

func F_idxseq f -> FinSequence of the carrier of (Free_LMod (X,R)) means :Def24: :: LMODFREE:def 24
( len it = len (idxseq f) & ( for i being Nat st i in dom it holds
it . i = (ev_iota f) . ((idxseq f) . i) ) );

existence
ex b₁ being FinSequence of the carrier of (Free_LMod (X,R)) st
( len b₁ = len (idxseq f) & ( for i being Nat st i in dom b₁ holds
b₁ . i = (ev_iota f) . ((idxseq f) . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of (Free_LMod (X,R)) st len b₁ = len (idxseq f) & ( for i being Nat st i in dom b₁ holds
b₁ . i = (ev_iota f) . ((idxseq f) . i) ) & len b₂ = len (idxseq f) & ( for i being Nat st i in dom b₂ holds
b₂ . i = (ev_iota f) . ((idxseq f) . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def24 defines F_idxseq LMODFREE:def 24 :
for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for b₄ being FinSequence of the carrier of (Free_LMod (X,R)) holds
( b₄ = F_idxseq f iff ( len b₄ = len (idxseq f) & ( for i being Nat st i in dom b₄ holds
b₄ . i = (ev_iota f) . ((idxseq f) . i) ) ) );

theorem Th12: :: LMODFREE:13

for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for x being Element of X st not x in Support (@ f) holds
0. R = (@ (Sum (F_idxseq f))) . x

proof end;

theorem Th13: :: LMODFREE:14

for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for x being Element of X st x in Support (@ f) holds
ex k being Nat st
( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ f) . x )

proof end;

theorem Th14: :: LMODFREE:15

for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for x being Element of X st x in Support (@ f) holds
(@ f) . x = (@ (Sum (F_idxseq f))) . x

proof end;

::$MR Every element of $\mathrm{Free\_LMod}(X,R)$ is the sum of its canonical finite decomposition.

theorem Th15: :: LMODFREE:16

for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds f = Sum (F_idxseq f)

proof end;

Lm23: for X being non empty set
for R being non degenerated Ring
for x being Element of X
for r being Element of R st r <> 0. R holds
Support (@ (r * (Iota (x,R)))) = {x}

proof end;

Lm24: for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for i being Nat st i in dom (idxseq f) holds
Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)}

proof end;

Lm25: for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds
( ex x being Element of X st Support (@ f) = {x} iff len (idxseq f) = 1 )

proof end;

Lm26: for X being non empty set
for R being non degenerated Ring
for x being Element of X
for f being 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 end;

theorem Th16: :: LMODFREE:17

for X being non empty set
for R being non degenerated Ring
for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
Support (@ (f + g)) = (Support (@ f)) \/ (Support (@ g))

proof end;

definition

let X be non empty set ;
let R be non degenerated Ring;
let N be LeftMod of R;
let u be Function of X,N;

func @ u -> Element of Funcs (X,([#] N)) equals :: LMODFREE:def 25
u;

coherence
u is Element of Funcs (X,([#] N)) by FUNCT_2:8;

end;

:: deftheorem defines @ LMODFREE:def 25 :
for X being non empty set
for R being non degenerated Ring
for N being LeftMod of R
for u being Function of X,N holds @ u = u;

definition

let X be non empty set ;
let R be non degenerated Ring;
let N be LeftMod of R;
let u be Function of X,N;

func ^ u -> Element of (Func_Mod (X,N)) equals :: LMODFREE:def 26
u;

coherence
u is Element of (Func_Mod (X,N)) by FUNCT_2:8;

end;

:: deftheorem defines ^ LMODFREE:def 26 :
for X being non empty set
for R being non degenerated Ring
for N being LeftMod of R
for u being Function of X,N holds ^ u = u;

definition

let X be non empty set ;
let R be non degenerated Ring;
let N be LeftMod of R;
let u be Element of (Func_Mod (X,N));

func ^ u -> Function of X,N equals :: LMODFREE:def 27
u;

coherence
u is Function of X,N by FUNCT_2:66;

end;

:: deftheorem defines ^ LMODFREE:def 27 :
for X being non empty set
for R being non degenerated Ring
for N being LeftMod of R
for u being Element of (Func_Mod (X,N)) holds ^ u = u;

definition

let R be non degenerated Ring;
let X be non empty set ;
let 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: :: LMODFREE:def 28
for x being Element of X holds it . x = ((@ f) . x) * (v . x);

existence
ex b₁ being Function of X, the carrier of N st
for x being Element of X holds b₁ . x = ((@ f) . x) * (v . x)

proof end;

uniqueness
for b₁, b₂ being Function of X, the carrier of N st ( for x being Element of X holds b₁ . x = ((@ f) . x) * (v . x) ) & ( for x being Element of X holds b₂ . x = ((@ f) . x) * (v . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def28 defines TermFS LMODFREE:def 28 :
for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for b₆ being Function of X, the carrier of N holds
( b₆ = TermFS (f,v) iff for x being Element of X holds b₆ . x = ((@ f) . x) * (v . x) );

definition

let R be non degenerated Ring;
let X be non empty set ;
let 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 :: LMODFREE:def 29
the addF of N $$ (B,(TermFS (f,v)));

coherence
the addF of N $$ (B,(TermFS (f,v))) is Element of N ;

end;

:: deftheorem defines PhiSet LMODFREE:def 29 :
for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for B being Element of Fin X holds PhiSet (v,f,B) = the addF of N $$ (B,(TermFS (f,v)));

theorem Th17: :: LMODFREE:18

for X being non empty set
for R being non degenerated Ring
for N being LeftMod of R
for f being Element of (Free_LMod (X,R))
for v being Function of X, the carrier of N
for x being Element of X holds PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)

proof end;

Th18: for X, Y being non empty set
for F being BinOp of Y
for t1, t2 being Function of X,Y
for B being Element of Fin X st F is commutative & F is associative & F is having_a_unity & ( for x being Element of X st x in B holds
t1 . x = t2 . x ) holds
F $$ (B,t1) = F $$ (B,t2)

proof end;

definition

let R be non degenerated Ring;
let X be non empty set ;
let f be Element of (Free_LMod (X,R));

func SuppFin f -> Element of Fin X equals :: LMODFREE:def 30
Support (@ f);

coherence
Support (@ f) is Element of Fin X by FINSUB_1:def 5;

end;

:: deftheorem defines SuppFin LMODFREE:def 30 :
for R being non degenerated Ring
for X being non empty set
for f being Element of (Free_LMod (X,R)) holds SuppFin f = Support (@ f);

::$INSERT we define the induced homomorphism $\Phi(v):\mathrm{FS\_Funcs}(X,R)\to N$.

definition

let R be non degenerated Ring;
let X be non empty set ;
let 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: :: LMODFREE:def 31
for f being Element of (Free_LMod (X,R)) holds it . f = PhiSet (v,f,(SuppFin f));

existence
ex b₁ being Function of (Free_LMod (X,R)), the carrier of N st
for f being Element of (Free_LMod (X,R)) holds b₁ . f = PhiSet (v,f,(SuppFin f))

proof end;

uniqueness
for b₁, b₂ being Function of (Free_LMod (X,R)), the carrier of N st ( for f being Element of (Free_LMod (X,R)) holds b₁ . f = PhiSet (v,f,(SuppFin f)) ) & ( for f being Element of (Free_LMod (X,R)) holds b₂ . f = PhiSet (v,f,(SuppFin f)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def31 defines Phi LMODFREE:def 31 :
for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for b₅ being Function of (Free_LMod (X,R)), the carrier of N holds
( b₅ = Phi v iff for f being Element of (Free_LMod (X,R)) holds b₅ . f = PhiSet (v,f,(SuppFin f)) );

theorem Th19: :: LMODFREE:19

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for x being Element of X holds (Phi v) . (Iota (x,R)) = v . x

proof end;

:: Additivity of Phi(v) can be intuitively understood
:: by reducing to the disjoint-support case.

theorem :: LMODFREE:20

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
(Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)

proof end;

Lm27: for R being non degenerated Ring
for N being LeftMod of R holds the_unity_wrt the addF of N = 0. N

proof end;

Lm28: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for B, C being Element of Fin X st B c= C & ( for x being 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 end;

Lm29: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for x being Element of X st not x in Support (@ f) holds
(TermFS (f,v)) . x = 0. N

proof end;

Lm30: for R being non degenerated Ring
for X being non empty set
for f, g being Element of (Free_LMod (X,R))
for x being Element of X st x in Support (@ (f + g)) holds
x in (Support (@ f)) \/ (Support (@ g))

proof end;

Lm31: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R))
for x being Element of X holds (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x)

proof end;

Lm32: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R))
for B being Element of Fin X holds (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)

proof end;

theorem Th21: :: LMODFREE:21

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R)) holds (Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)

proof end;

Lm33: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R
for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)

proof end;

Lm34: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R
for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))

proof end;

theorem Th22: :: LMODFREE:22

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)

proof end;

theorem :: LMODFREE:23

for M being non empty addLoopStr
for p being FinSequence of the carrier of M
for k being Nat st k in dom p holds
Del (p,k,k) = Del (p,k)

proof end;

Lm37: for N being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of N
for k being Nat st k in dom p holds
Sum p = (Sum (Del (p,k,k))) + (p /. k)

proof end;

definition

let R be Ring;
let X be set ;
let M be LeftMod of R;
let u be Function of X, the carrier of M;

attr u is universal means :: LMODFREE:def 32
for N being LeftMod of R
for v being Function of X, the carrier of N ex F being Homomorphism of id R,M,N st
( F * u = v & ( for f1, f2 being Homomorphism of id R,M,N st f1 * u = v & f2 * u = v holds
f1 = f2 ) );

end;

:: deftheorem defines universal LMODFREE:def 32 :
for R being Ring
for X being set
for M being LeftMod of R
for u being Function of X, the carrier of M holds
( u is universal iff for N being LeftMod of R
for v being Function of X, the carrier of N ex F being Homomorphism of id R,M,N st
( F * u = v & ( for f1, f2 being Homomorphism of id R,M,N st f1 * u = v & f2 * u = v holds
f1 = f2 ) ) );

theorem Th23: :: LMODFREE:24

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N holds Phi v is Homomorphism of id R, Free_LMod (X,R),N

proof end;

theorem Th24: :: LMODFREE:25

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N holds (Phi v) * (IotaMap (X,R)) = v

proof end;

Lm38: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for h being Homomorphism of id R, Free_LMod (X,R),N holds h . (0. (Free_LMod (X,R))) = 0. N

proof end;

registration

let R be Ring;
let 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 s (#) h -> the carrier of N -valued FinSequence-like ;

coherence
( h * s is FinSequence-like & h * s is the carrier of N -valued ) ;

end;

theorem Th25: :: LMODFREE:26

for D, E being non empty set
for h being Function of D,E
for p being FinSequence of D
for d being Element of D holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>

proof end;

Lm39: for V being non empty right_zeroed addLoopStr
for W being non empty right_complementable add-associative right_zeroed addLoopStr
for h being Function of the carrier of V, the carrier of W st h is additive holds
h . (0. V) = 0. W

proof end;

theorem Th26: :: LMODFREE:27

for M, N being non empty right_complementable add-associative right_zeroed addLoopStr
for h being Function of the carrier of M, the carrier of N
for s being FinSequence of the carrier of M st h is additive holds
h . (Sum s) = Sum (h * s)

proof end;

Lm40: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for h being Homomorphism of id R, Free_LMod (X,R),N
for s being FinSequence of the carrier of (Free_LMod (X,R)) holds h . (Sum s) = Sum (h * s)

proof end;

Lm41: for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f1, f2 being Homomorphism of id R, Free_LMod (X,R),N st f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v holds
f1 = f2

proof end;

::$MR The map $\mathrm{IotaMap}(X,R)$ satisfies the universal mapping property of the free module on $X$.

theorem :: LMODFREE:28

for R being non degenerated Ring
for X being non empty set holds IotaMap (X,R) is universal

proof end;

Lm42: for R being non degenerated Ring
for X being non empty set
for f being Element of (Free_LMod (X,R))
for i being Nat st i in dom (F_idxseq f) holds
(F_idxseq f) /. i in Lin (rng (IotaMap (X,R)))

proof end;

theorem Th28: :: LMODFREE:29

for R being non degenerated Ring
for X being non empty set
for f being Element of (Free_LMod (X,R)) holds f in Lin (rng (IotaMap (X,R)))

proof end;

theorem Th29: :: LMODFREE:30

for R being non degenerated Ring
for X being non empty set holds Lin (rng (IotaMap (X,R))) = ModuleStr(# the carrier of (Free_LMod (X,R)), the addF of (Free_LMod (X,R)), the ZeroF of (Free_LMod (X,R)), the lmult of (Free_LMod (X,R)) #)

proof end;

Lm43: for M being non empty addLoopStr
for p being FinSequence of the carrier of M
for n, i being 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 end;

Lm45: for N being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of N
for k being Nat st k in dom p & ( for i being Nat st i in dom p & i <> k holds
p . i = 0. N ) holds
Sum p = p /. k

proof end;

theorem Th30: :: LMODFREE:31

for R being non degenerated Ring
for X being non empty set holds rng (IotaMap (X,R)) is linearly-independent

proof end;

theorem Th31: :: LMODFREE:32

for R being non degenerated Ring
for X being non empty set holds rng (IotaMap (X,R)) is base by Th29, Th30;

:: as a corollary of Th34, using the basis-theoretic definition of free modules.

theorem Th32: :: LMODFREE:33

for R being non degenerated Ring
for X being non empty set holds Free_LMod (X,R) is free

proof end;

LmTriv: for R being non degenerated Ring holds
( fs_Funcs ({},R) = {{}} & 0_Funcs ({},R) = {} )

proof end;

LmTriv2: for R being non degenerated Ring holds
( fs_ADD ({},R) = op2 & fs_LMULT ({},R) = pr2 ( the carrier of R,{0}) )

proof end;

theorem ThTriv1: :: LMODFREE:34

for R being non degenerated Ring holds FS_Funcs ({},R) = TrivialLMod R

proof end;

theorem Th33: :: LMODFREE:35

for R being non degenerated Ring holds Free_LMod ({},R) is free

proof end;

theorem Th34: :: LMODFREE:36

for R being non degenerated Ring
for X being set holds Free_LMod (X,R) is free

proof end;

registration

let R be non degenerated Ring;
let X be set ;

cluster Free_LMod (X,R) -> non empty free ;

coherence
Free_LMod (X,R) is free by Th34;

end;