:: Ring of {E}ndomorphisms \& {M}odules over a {R}ing
:: by Yasushige Watase
::
:: Received September 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

definition

let M, N be AbGroup;

func ADD (M,N) -> BinOp of (Funcs ( the carrier of M, the carrier of N)) means :Def1: :: LMOD_XX1:def 1
for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds it . (f,g) = the addF of N .: (f,g);

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

proof end;

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

proof end;

end;

:: deftheorem Def1 defines ADD LMOD_XX1:def 1 :
for M, N being AbGroup
for b₃ being BinOp of (Funcs ( the carrier of M, the carrier of N)) holds
( b₃ = ADD (M,N) iff for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds b₃ . (f,g) = the addF of N .: (f,g) );

Lm1: for M, N being AbGroup
for x being Element of M
for f being Function of M,N holds x in dom f

proof end;

theorem Th1: :: LMOD_XX1:1

for M, N being AbGroup
for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (ADD (M,N)) . (f,g) iff for x being Element of the carrier of M holds h . x = (f . x) + (g . x) )

proof end;

Lm2: for M, N being AbGroup
for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((ADD (M,N)) . (g,h))) = (ADD (M,N)) . (((ADD (M,N)) . (f,g)),h)

proof end;

theorem Th2: :: LMOD_XX1:2

for M, N being AbGroup
for f, g being Homomorphism of M,N holds (ADD (M,N)) . (f,g) is Homomorphism of M,N

proof end;

definition

let M be AbGroup;

func set_End M -> non empty Subset of (Funcs ( the carrier of M, the carrier of M)) equals :: LMOD_XX1:def 2
{ f where f is Function of M,M : f is Endomorphism of M } ;

coherence
{ f where f is Function of M,M : f is Endomorphism of M } is non empty Subset of (Funcs ( the carrier of M, the carrier of M))

proof end;

end;

:: deftheorem defines set_End LMOD_XX1:def 2 :
for M being AbGroup holds set_End M = { f where f is Function of M,M : f is Endomorphism of M } ;

Lm3: for M being AbGroup
for f being object st f in set_End M holds
f is Endomorphism of M

proof end;

definition

let M be AbGroup;

func add_End M -> BinOp of (set_End M) equals :: LMOD_XX1:def 3
(ADD (M,M)) | [:(set_End M),(set_End M):];

correctness
coherence
(ADD (M,M)) | [:(set_End M),(set_End M):] is BinOp of (set_End M);

proof end;

end;

:: deftheorem defines add_End LMOD_XX1:def 3 :
for M being AbGroup holds add_End M = (ADD (M,M)) | [:(set_End M),(set_End M):];

theorem Th3: :: LMOD_XX1:3

for M being AbGroup
for f, g being Endomorphism of M holds
( f in Funcs ( the carrier of M, the carrier of M) & g in Funcs ( the carrier of M, the carrier of M) & (add_End M) . [f,g] = (ADD (M,M)) . (f,g) & (ADD (M,M)) . (f,g) is Endomorphism of M )

proof end;

definition

let M be AbGroup;
let f, g be Element of Funcs ( the carrier of M, the carrier of M);
:: original: *
redefine func g * f -> Element of Funcs ( the carrier of M, the carrier of M);
coherence
f * g is Element of Funcs ( the carrier of M, the carrier of M)

proof end;

end;

::$INSERT prepare Composition of Homomorphisms

definition

let M be AbGroup;

func FuncComp M -> BinOp of (Funcs ( the carrier of M, the carrier of M)) means :Def4: :: LMOD_XX1:def 4
for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds it . (f,g) = f * g;

existence
ex b₁ being BinOp of (Funcs ( the carrier of M, the carrier of M)) st
for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds b₁ . (f,g) = f * g

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs ( the carrier of M, the carrier of M)) st ( for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds b₁ . (f,g) = f * g ) & ( for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds b₂ . (f,g) = f * g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines FuncComp LMOD_XX1:def 4 :
for M being AbGroup
for b₂ being BinOp of (Funcs ( the carrier of M, the carrier of M)) holds
( b₂ = FuncComp M iff for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds b₂ . (f,g) = f * g );

theorem Th4: :: LMOD_XX1:4

for M, N being AbGroup
for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,g) = (ADD (M,N)) . (g,f)

proof end;

:: Endomorphism of M is closed under Composition

theorem Th5: :: LMOD_XX1:5

for M being AbGroup
for f, g being Endomorphism of M holds (FuncComp M) . (f,g) is Endomorphism of M

proof end;

definition

let M be AbGroup;

func mult_End M -> BinOp of (set_End M) equals :: LMOD_XX1:def 5
(FuncComp M) | [:(set_End M),(set_End M):];

correctness
coherence
(FuncComp M) | [:(set_End M),(set_End M):] is BinOp of (set_End M);

proof end;

end;

:: deftheorem defines mult_End LMOD_XX1:def 5 :
for M being AbGroup holds mult_End M = (FuncComp M) | [:(set_End M),(set_End M):];

theorem Th6: :: LMOD_XX1:6

for M being AbGroup
for f, g being Endomorphism of M holds
( f in Funcs ( the carrier of M, the carrier of M) & g in Funcs ( the carrier of M, the carrier of M) & (mult_End M) . [f,g] = (FuncComp M) . (f,g) & (FuncComp M) . (f,g) is Endomorphism of M )

proof end;

definition

let M be AbGroup;

func 0_End M -> Element of set_End M equals :: LMOD_XX1:def 6
ZeroMap (M,M);

correctness
coherence
ZeroMap (M,M) is Element of set_End M;

proof end;

func 1_End M -> Element of set_End M equals :: LMOD_XX1:def 7
id M;

correctness
coherence
id M is Element of set_End M;

proof end;

end;

:: deftheorem defines 0_End LMOD_XX1:def 6 :
for M being AbGroup holds 0_End M = ZeroMap (M,M);

:: deftheorem defines 1_End LMOD_XX1:def 7 :
for M being AbGroup holds 1_End M = id M;

definition

let M be AbGroup;
let f be Element of set_End M;

func Inv f -> Element of set_End M means :Def8: :: LMOD_XX1:def 8
for x being Element of M holds it . x = f . (- x);

existence
ex b₁ being Element of set_End M st
for x being Element of M holds b₁ . x = f . (- x)

proof end;

uniqueness
for b₁, b₂ being Element of set_End M st ( for x being Element of M holds b₁ . x = f . (- x) ) & ( for x being Element of M holds b₂ . x = f . (- x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Inv LMOD_XX1:def 8 :
for M being AbGroup
for f, b₃ being Element of set_End M holds
( b₃ = Inv f iff for x being Element of M holds b₃ . x = f . (- x) );

theorem Th7: :: LMOD_XX1:7

for M being AbGroup
for f being Element of set_End M holds (ADD (M,M)) . (f,(Inv f)) = ZeroMap (M,M)

proof end;

::$INSERT Define the Ring of Endomorphism of M as a structure.

definition

let M be AbGroup;

func End_Ring M -> non empty strict doubleLoopStr equals :: LMOD_XX1:def 9
doubleLoopStr(# (set_End M),(add_End M),(mult_End M),(1_End M),(0_End M) #);

coherence
doubleLoopStr(# (set_End M),(add_End M),(mult_End M),(1_End M),(0_End M) #) is non empty strict doubleLoopStr ;

end;

:: deftheorem defines End_Ring LMOD_XX1:def 9 :
for M being AbGroup holds End_Ring M = doubleLoopStr(# (set_End M),(add_End M),(mult_End M),(1_End M),(0_End M) #);

Lm4: for M being AbGroup
for f being Element of Funcs ( the carrier of M, the carrier of M) holds (ADD (M,M)) . (f,(ZeroMap (M,M))) = f

proof end;

Lm5: for M being AbGroup holds End_Ring M is Abelian

proof end;

Lm6: for M being AbGroup holds End_Ring M is add-associative

proof end;

Lm7: for M being AbGroup holds End_Ring M is right_zeroed

proof end;

Lm8: for M being AbGroup holds End_Ring M is right_complementable

proof end;

Lm9: for M being AbGroup holds End_Ring M is distributive

proof end;

Lm10: for M being AbGroup holds End_Ring M is associative

proof end;

Lm11: for M being AbGroup holds End_Ring M is well-unital

proof end;

:: the structure of End_Ring(M) turns to be a Ring.

theorem :: LMOD_XX1:8

for M being AbGroup holds End_Ring M is Ring by Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;

registration

let M be AbGroup;

cluster End_Ring M -> non empty right_complementable strict well-unital distributive Abelian add-associative right_zeroed associative ;

coherence
( End_Ring M is Abelian & End_Ring M is add-associative & End_Ring M is right_zeroed & End_Ring M is right_complementable & End_Ring M is associative & End_Ring M is well-unital & End_Ring M is distributive ) by Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;

end;

registration

let M be AbGroup;

cluster End_Ring M -> non empty strict ;

coherence
End_Ring M is strict ;

end;

:: the Def. of \cite{MOD_4.abs} cannot be applied since no ring-hom. is used.

definition

let R be Ring;
let M, N be LeftMod of R;

mode Homomorphism of R,M,N -> Function of M,N means :Def10: :: LMOD_XX1:def 10
( it is additive & it is homogeneous );

existence
ex b₁ being Function of M,N st
( b₁ is additive & b₁ is homogeneous )

proof end;

end;

:: deftheorem Def10 defines Homomorphism LMOD_XX1:def 10 :
for R being Ring
for M, N being LeftMod of R
for b₄ being Function of M,N holds
( b₄ is Homomorphism of R,M,N iff ( b₄ is additive & b₄ is homogeneous ) );

theorem Th9: :: LMOD_XX1:9

for R being Ring
for M, N being LeftMod of R
for f being Homomorphism of R,M,N st f is one-to-one & f is onto holds
f " is Homomorphism of R,N,M

proof end;

definition

let R be Ring;
let M, N be LeftMod of R;

pred M ~= N means :: LMOD_XX1:def 11
ex f being Homomorphism of R,M,N st
( f is one-to-one & f is onto );

end;

:: deftheorem defines ~= LMOD_XX1:def 11 :
for R being Ring
for M, N being LeftMod of R holds
( M ~= N iff ex f being Homomorphism of R,M,N st
( f is one-to-one & f is onto ) );

definition

let R be Ring;
let M be LeftMod of R;
mode Endomorphism of R,M is Homomorphism of R,M,M;

end;

theorem Tref: :: LMOD_XX1:10

for R being Ring
for M being LeftMod of R holds M ~= M

proof end;

theorem Tsym: :: LMOD_XX1:11

for R being Ring
for M, N being LeftMod of R st M ~= N holds
N ~= M

proof end;

definition

let R be Ring;
let M, N be LeftMod of R;
:: original: ~=
redefine pred M ~= N;
reflexivity
for M being LeftMod of R holds (R,b₁,b₁) by Tref;
symmetry
for M, N being LeftMod of R st (R,b₁,b₂) holds
(R,b₂,b₁) by Tsym;

end;

theorem :: LMOD_XX1:12

for R being Ring
for L, M, N being LeftMod of R st L ~= M & M ~= N holds
L ~= N

proof end;

theorem Th13: :: LMOD_XX1:13

for R being Ring
for M, N being LeftMod of R
for f being Homomorphism of R,M,N holds
( f is one-to-one iff ker f = {(0. M)} )

proof end;

definition

let R be Ring;
let M be AbGroup;
let s be Function of R,(End_Ring M);

func LModlmult (M,s) -> Function of [: the carrier of R, the carrier of M:], the carrier of M means :Def12: :: LMOD_XX1:def 12
for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & it . (x,y) = h . y );

existence
ex b₁ being Function of [: the carrier of R, the carrier of M:], the carrier of M st
for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & b₁ . (x,y) = h . y )

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of R, the carrier of M:], the carrier of M st ( for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & b₁ . (x,y) = h . y ) ) & ( for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & b₂ . (x,y) = h . y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines LModlmult LMOD_XX1:def 12 :
for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M)
for b₄ being Function of [: the carrier of R, the carrier of M:], the carrier of M holds
( b₄ = LModlmult (M,s) iff for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & b₄ . (x,y) = h . y ) );

definition

let R be Ring;
let M be AbGroup;
let s be Function of R,(End_Ring M);

func AbGrLMod (M,s) -> non empty strict ModuleStr over R equals :: LMOD_XX1:def 13
ModuleStr(# the carrier of M, the addF of M,(0. M),(LModlmult (M,s)) #);

coherence
ModuleStr(# the carrier of M, the addF of M,(0. M),(LModlmult (M,s)) #) is non empty strict ModuleStr over R ;

end;

:: deftheorem defines AbGrLMod LMOD_XX1:def 13 :
for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M) holds AbGrLMod (M,s) = ModuleStr(# the carrier of M, the addF of M,(0. M),(LModlmult (M,s)) #);

Lm12: for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M)
for a being Element of R
for x, y being Element of (AbGrLMod (M,s)) holds a * (x + y) = (a * x) + (a * y)

proof end;

Lm13: for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M)
for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a + b) * x = (a * x) + (b * x)

proof end;

Lm14: for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M)
for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a * b) * x = a * (b * x)

proof end;

theorem Th14: :: LMOD_XX1:14

for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M) st s is RingHomomorphism holds
AbGrLMod (M,s) is LeftMod of R

proof end;

definition

let R be Ring;
let M, N be LeftMod of R;

func 0_Funcs (M,N) -> Element of Funcs ( the carrier of M, the carrier of N) equals :: LMOD_XX1:def 14
ZeroMap (M,N);

correctness
coherence
ZeroMap (M,N) is Element of Funcs ( the carrier of M, the carrier of N);
by FUNCT_2:8;

end;

:: deftheorem defines 0_Funcs LMOD_XX1:def 14 :
for R being Ring
for M, N being LeftMod of R holds 0_Funcs (M,N) = ZeroMap (M,N);

definition

let R be Ring;
let M, N be LeftMod of R;

func ADD (M,N) -> BinOp of (Funcs ( the carrier of M, the carrier of N)) means :Def15: :: LMOD_XX1:def 15
for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds it . (f,g) = the addF of N .: (f,g);

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

proof end;

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

proof end;

end;

:: deftheorem Def15 defines ADD LMOD_XX1:def 15 :
for R being Ring
for M, N being LeftMod of R
for b₄ being BinOp of (Funcs ( the carrier of M, the carrier of N)) holds
( b₄ = ADD (M,N) iff for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds b₄ . (f,g) = the addF of N .: (f,g) );

Lm15: for R being Ring
for M, N being LeftMod of R
for x being Element of M
for f being Function of M,N holds x in dom f

proof end;

theorem Th15: :: LMOD_XX1:15

for R being Ring
for M, N being LeftMod of R
for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (ADD (M,N)) . (f,g) iff for x being Element of the carrier of M holds h . x = (f . x) + (g . x) )

proof end;

definition

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

proof end;

end;

definition

let R be Ring;
let M, N be LeftMod of R;

func LMULT (M,N) -> Function of [: the carrier of R,(Funcs ( the carrier of M, the carrier of N)):],(Funcs ( the carrier of M, the carrier of N)) means :Def16: :: LMOD_XX1:def 16
for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (it . [a,f]) . x = a * (f . x);

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

proof end;

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

proof end;

end;

:: deftheorem Def16 defines LMULT LMOD_XX1:def 16 :
for R being Ring
for M, N being LeftMod of R
for b₄ being Function of [: the carrier of R,(Funcs ( the carrier of M, the carrier of N)):],(Funcs ( the carrier of M, the carrier of N)) holds
( b₄ = LMULT (M,N) iff for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (b₄ . [a,f]) . x = a * (f . x) );

definition

let R be Ring;
let M, N be LeftMod of R;

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

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

end;

:: deftheorem defines Func_Mod LMOD_XX1:def 17 :
for R being Ring
for M, N being LeftMod of R holds Func_Mod (R,M,N) = ModuleStr(# (Funcs ( the carrier of M, the carrier of N)),(ADD (M,N)),(0_Funcs (M,N)),(LMULT (M,N)) #);

theorem Th16: :: LMOD_XX1:16

for R being Ring
for M, N being LeftMod of R
for a being Element of the carrier of R
for f, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (LMULT (M,N)) . [a,f] iff for x being Element of M holds h . x = a * (f . x) )

proof end;

Lm16: for R being Ring
for M, N being LeftMod of R
for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,g) = (ADD (M,N)) . (g,f)

proof end;

Lm17: for R being Ring
for M, N being LeftMod of R
for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((ADD (M,N)) . (g,h))) = (ADD (M,N)) . (((ADD (M,N)) . (f,g)),h)

proof end;

Lm18: for R being Ring
for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,(0_Funcs (M,N))) = f

proof end;

Lm19: for R being Ring
for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f])) = 0_Funcs (M,N)

proof end;

Lm20: for R being Ring
for M, N being LeftMod of R
for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for a being Element of the carrier of R holds (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))

proof end;

Lm21: for R being Ring
for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for a, b being Element of the carrier of R holds (LMULT (M,N)) . [(a + b),f] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]))

proof end;

Lm22: for R being Ring
for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for a, b being Element of the carrier of R holds (LMULT (M,N)) . [(a * b),f] = (LMULT (M,N)) . [a,((LMULT (M,N)) . [b,f])]

proof end;

Lm23: for R being Ring
for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds (LMULT (M,N)) . [(1. R),f] = f

proof end;

Lm24: for R being Ring
for M, N being LeftMod of R holds Func_Mod (R,M,N) is right_complementable

proof end;

registration

let R be Ring;
let M, N be LeftMod of R;

cluster Func_Mod (R,M,N) -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;

coherence
( Func_Mod (R,M,N) is Abelian & Func_Mod (R,M,N) is add-associative & Func_Mod (R,M,N) is right_zeroed & Func_Mod (R,M,N) is right_complementable & Func_Mod (R,M,N) is vector-distributive & Func_Mod (R,M,N) is scalar-distributive & Func_Mod (R,M,N) is scalar-associative & Func_Mod (R,M,N) is scalar-unital ) by Lm16, Lm17, Lm18, Lm20, Lm21, Lm23, Lm22, Lm24;

end;

theorem :: LMOD_XX1:17

for R being Ring
for M, N being LeftMod of R holds Func_Mod (R,M,N) is LeftMod of R ;

:: Hom(M,N) the set of all R Homomorphisms form left R-Module

theorem Th18: :: LMOD_XX1:18

for R being comRing
for M, N being LeftMod of R
for f, g being Homomorphism of R,M,N holds (ADD (M,N)) . (f,g) is Homomorphism of R,M,N

proof end;

definition

let R be comRing;
let M1, M, N be LeftMod of R;
let f be Element of Funcs ( the carrier of M1, the carrier of M);
let g be Element of Funcs ( the carrier of M, the carrier of N);
:: original: *
redefine func g * f -> Element of Funcs ( the carrier of M1, the carrier of N);
coherence
f * g is Element of Funcs ( the carrier of M1, the carrier of N) by FUNCT_2:128;

end;

Lm25: for R being comRing
for M, N, M1 being LeftMod of R
for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of M1, the carrier of M) holds ((ADD (M,N)) . (f,g)) * u = (ADD (M1,N)) . ((f * u),(g * u))

proof end;

Lm26: for R being comRing
for M, N, N1 being LeftMod of R
for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of N, the carrier of N1) st u is additive holds
u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g))

proof end;

Lm27: for R being comRing
for M, N, M1 being LeftMod of R
for a being Element of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of M1, the carrier of M) holds ((LMULT (M,N)) . [a,f]) * u = (LMULT (M1,N)) . [a,(f * u)]

proof end;

Lm28: for R being comRing
for M, N, N1 being LeftMod of R
for a being Element of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of N, the carrier of N1) st u is homogeneous holds
u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)]

proof end;

theorem Th19: :: LMOD_XX1:19

for R being comRing
for M, N, M1 being LeftMod of R
for f being Homomorphism of R,M,N
for u being Homomorphism of R,M1,M holds f * u is Homomorphism of R,M1,N

proof end;

:: commutativity matters (r*a)*g.x .= (a*r)*g.x by VECTSP_1:def 16

theorem Th20: :: LMOD_XX1:20

for R being comRing
for M, N being LeftMod of R
for a being Element of the carrier of R
for g being Homomorphism of R,M,N holds (LMULT (M,N)) . [a,g] is Homomorphism of R,M,N

proof end;

definition

let R be comRing;
let M, N be LeftMod of R;

func set_Hom (M,N) -> non empty Subset of (Funcs ( the carrier of M, the carrier of N)) equals :: LMOD_XX1:def 18
{ f where f is Function of M,N : f is Homomorphism of R,M,N } ;

coherence
{ f where f is Function of M,N : f is Homomorphism of R,M,N } is non empty Subset of (Funcs ( the carrier of M, the carrier of N))

proof end;

end;

:: deftheorem defines set_Hom LMOD_XX1:def 18 :
for R being comRing
for M, N being LeftMod of R holds set_Hom (M,N) = { f where f is Function of M,N : f is Homomorphism of R,M,N } ;

Lm29: for R being comRing
for M, N being LeftMod of R
for f being object holds
( f in set_Hom (M,N) iff f is Homomorphism of R,M,N )

proof end;

definition

let R be comRing;
let M, N be LeftMod of R;

func add_Hom (M,N) -> BinOp of (set_Hom (M,N)) equals :: LMOD_XX1:def 19
(ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):];

correctness
coherence
(ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):] is BinOp of (set_Hom (M,N));

proof end;

end;

:: deftheorem defines add_Hom LMOD_XX1:def 19 :
for R being comRing
for M, N being LeftMod of R holds add_Hom (M,N) = (ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):];

definition

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

proof end;

end;

definition

let R be comRing;
let M, N be LeftMod of R;

func lmult_Hom (M,N) -> Function of [: the carrier of R,(set_Hom (M,N)):],(set_Hom (M,N)) equals :: LMOD_XX1:def 20
(LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):];

correctness
coherence
(LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):] is Function of [: the carrier of R,(set_Hom (M,N)):],(set_Hom (M,N));

proof end;

end;

:: deftheorem defines lmult_Hom LMOD_XX1:def 20 :
for R being comRing
for M, N being LeftMod of R holds lmult_Hom (M,N) = (LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):];

definition

let R be comRing;
let M, N be LeftMod of R;

func 0_Hom (M,N) -> Element of set_Hom (M,N) equals :: LMOD_XX1:def 21
ZeroMap (M,N);

correctness
coherence
ZeroMap (M,N) is Element of set_Hom (M,N);

proof end;

end;

:: deftheorem defines 0_Hom LMOD_XX1:def 21 :
for R being comRing
for M, N being LeftMod of R holds 0_Hom (M,N) = ZeroMap (M,N);

definition

let R be comRing;
let M, N be LeftMod of R;

func Hom (R,M,N) -> non empty ModuleStr over R equals :: LMOD_XX1:def 22
ModuleStr(# (set_Hom (M,N)),(add_Hom (M,N)),(0_Hom (M,N)),(lmult_Hom (M,N)) #);

coherence
ModuleStr(# (set_Hom (M,N)),(add_Hom (M,N)),(0_Hom (M,N)),(lmult_Hom (M,N)) #) is non empty ModuleStr over R ;

end;

:: deftheorem defines Hom LMOD_XX1:def 22 :
for R being comRing
for M, N being LeftMod of R holds Hom (R,M,N) = ModuleStr(# (set_Hom (M,N)),(add_Hom (M,N)),(0_Hom (M,N)),(lmult_Hom (M,N)) #);

registration

let R be comRing;
let M, N be LeftMod of R;

cluster Hom (R,M,N) -> non empty ;

coherence
not Hom (R,M,N) is empty ;

end;

theorem Th21: :: LMOD_XX1:21

for R being comRing
for M, N being LeftMod of R
for f, g being Homomorphism of R,M,N holds
( f in Funcs ( the carrier of M, the carrier of N) & g in Funcs ( the carrier of M, the carrier of N) & (add_Hom (M,N)) . [f,g] = (ADD (M,N)) . (f,g) & (ADD (M,N)) . (f,g) is Homomorphism of R,M,N )

proof end;

theorem Th22: :: LMOD_XX1:22

for R being comRing
for M, N being LeftMod of R
for a being Element of the carrier of R
for f being Homomorphism of R,M,N holds
( (lmult_Hom (M,N)) . [a,f] = (LMULT (M,N)) . [a,f] & (LMULT (M,N)) . [a,f] is Homomorphism of R,M,N )

proof end;

theorem Th23: :: LMOD_XX1:23

for R being comRing
for M, N being LeftMod of R
for f1, g1 being Element of (Func_Mod (R,M,N))
for f, g being Element of (Hom (R,M,N)) st f1 = f & g1 = g holds
f + g = f1 + g1

proof end;

Lm30: for R being comRing
for M, N being LeftMod of R
for a being Element of R
for f1 being Element of (Func_Mod (R,M,N))
for f being Element of (Hom (R,M,N)) st f1 = f holds
a * f = a * f1

proof end;

theorem Th24: :: LMOD_XX1:24

for R being comRing
for M, N being LeftMod of R holds Hom (R,M,N) is LeftMod of R

proof end;

registration

let R be comRing;
let M, N be LeftMod of R;

cluster Hom (R,M,N) -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;

coherence
( Hom (R,M,N) is Abelian & Hom (R,M,N) is add-associative & Hom (R,M,N) is right_zeroed & Hom (R,M,N) is right_complementable & Hom (R,M,N) is vector-distributive & Hom (R,M,N) is scalar-distributive & Hom (R,M,N) is scalar-associative & Hom (R,M,N) is scalar-unital ) by Th24;

end;

definition

let R be comRing;
let M1, M, N be LeftMod of R;
let u be Homomorphism of R,M1,M;

func tau (N,u) -> Function of (Hom (R,M,N)),(Hom (R,M1,N)) means :Def23: :: LMOD_XX1:def 23
for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & it . f = f1 * u );

existence
ex b₁ being Function of (Hom (R,M,N)),(Hom (R,M1,N)) st
for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₁ . f = f1 * u )

proof end;

uniqueness
for b₁, b₂ being Function of (Hom (R,M,N)),(Hom (R,M1,N)) st ( for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₁ . f = f1 * u ) ) & ( for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₂ . f = f1 * u ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines tau LMOD_XX1:def 23 :
for R being comRing
for M1, M, N being LeftMod of R
for u being Homomorphism of R,M1,M
for b₆ being Function of (Hom (R,M,N)),(Hom (R,M1,N)) holds
( b₆ = tau (N,u) iff for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₆ . f = f1 * u ) );

Lm31: for R being comRing
for M1, M, N being LeftMod of R
for u being Homomorphism of R,M1,M holds
( tau (N,u) is additive & tau (N,u) is homogeneous )

proof end;

registration

let R be comRing;
let M1, M, N be LeftMod of R;
let u be Homomorphism of R,M1,M;

cluster tau (N,u) -> additive homogeneous ;

coherence
( tau (N,u) is additive & tau (N,u) is homogeneous ) by Lm31;

end;

theorem :: LMOD_XX1:25

for R being comRing
for M1, M, N being LeftMod of R
for u being Homomorphism of R,M1,M holds tau (N,u) is Homomorphism of R, Hom (R,M,N), Hom (R,M1,N) by Def10;

definition

let R be comRing;
let M, N, N1 be LeftMod of R;
let u be Homomorphism of R,N,N1;

func phi (M,u) -> Function of (Hom (R,M,N)),(Hom (R,M,N1)) means :Def24: :: LMOD_XX1:def 24
for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & it . f = u * f1 );

existence
ex b₁ being Function of (Hom (R,M,N)),(Hom (R,M,N1)) st
for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₁ . f = u * f1 )

proof end;

uniqueness
for b₁, b₂ being Function of (Hom (R,M,N)),(Hom (R,M,N1)) st ( for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₁ . f = u * f1 ) ) & ( for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₂ . f = u * f1 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def24 defines phi LMOD_XX1:def 24 :
for R being comRing
for M, N, N1 being LeftMod of R
for u being Homomorphism of R,N,N1
for b₆ being Function of (Hom (R,M,N)),(Hom (R,M,N1)) holds
( b₆ = phi (M,u) iff for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₆ . f = u * f1 ) );

Lm32: for R being comRing
for M, N, N1 being LeftMod of R
for u being Homomorphism of R,N,N1 holds
( phi (M,u) is additive & phi (M,u) is homogeneous )

proof end;

registration

let R be comRing;
let M, N, N1 be LeftMod of R;
let u be Homomorphism of R,N,N1;

cluster phi (M,u) -> additive homogeneous ;

coherence
( phi (M,u) is additive & phi (M,u) is homogeneous ) by Lm32;

end;

theorem :: LMOD_XX1:26

for R being comRing
for M, N, N1 being LeftMod of R
for u being Homomorphism of R,N,N1 holds phi (M,u) is Homomorphism of R, Hom (R,M,N), Hom (R,M,N1) by Def10;

:: A formal proof of Hom(R,M) ~= M.

theorem :: LMOD_XX1:27

for R being comRing
for M being LeftMod of R holds Hom (R,(LeftModule R),M) ~= M

proof end;

:: Correspondence between Abelian Group and Left R-Module

definition

let R be comRing;
let M be LeftMod of R;

func AbGr M -> strict AbGroup equals :: LMOD_XX1:def 25
addLoopStr(# the carrier of M, the addF of M,(0. M) #);

coherence
addLoopStr(# the carrier of M, the addF of M,(0. M) #) is strict AbGroup

proof end;

end;

:: deftheorem defines AbGr LMOD_XX1:def 25 :
for R being comRing
for M being LeftMod of R holds AbGr M = addLoopStr(# the carrier of M, the addF of M,(0. M) #);

definition

let R be comRing;
let M, N be LeftMod of R;
let f be Homomorphism of R,M,N;

func AbGr f -> Function of (AbGr M),(AbGr N) means :Def26: :: LMOD_XX1:def 26
for x being object st x in the carrier of (AbGr M) holds
it . x = f . x;

existence
ex b₁ being Function of (AbGr M),(AbGr N) st
for x being object st x in the carrier of (AbGr M) holds
b₁ . x = f . x

proof end;

uniqueness
for b₁, b₂ being Function of (AbGr M),(AbGr N) st ( for x being object st x in the carrier of (AbGr M) holds
b₁ . x = f . x ) & ( for x being object st x in the carrier of (AbGr M) holds
b₂ . x = f . x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def26 defines AbGr LMOD_XX1:def 26 :
for R being comRing
for M, N being LeftMod of R
for f being Homomorphism of R,M,N
for b₅ being Function of (AbGr M),(AbGr N) holds
( b₅ = AbGr f iff for x being object st x in the carrier of (AbGr M) holds
b₅ . x = f . x );

theorem Th28: :: LMOD_XX1:28

for R being comRing
for M, N being LeftMod of R
for f being Homomorphism of R,M,N holds AbGr f is Homomorphism of (AbGr M),(AbGr N)

proof end;

theorem Th29: :: LMOD_XX1:29

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M holds
( AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x )

proof end;

theorem Lm33: :: LMOD_XX1:30

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M st h = f * g holds
AbGr h = (AbGr f) * (AbGr g)

proof end;

theorem Th30: :: LMOD_XX1:31

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M holds
( AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x) )

proof end;

theorem Th31: :: LMOD_XX1:32

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M st h = (ADD (M,M)) . (f,g) holds
AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))

proof end;

theorem :: LMOD_XX1:33

for R being Ring
for M being LeftMod of R
for a being Element of R
for m being Element of M holds ((curry the lmult of M) . a) . m = a * m by LOPBAN_8:7;

theorem Th33: :: LMOD_XX1:34

for R being comRing
for M being LeftMod of R
for a being Element of R holds (curry the lmult of M) . a is Endomorphism of R,M

proof end;

theorem Th34: :: LMOD_XX1:35

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M st h = f * g holds
AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g))

proof end;

definition

let R be comRing;
let M be LeftMod of R;

func canHom M -> Function of R,(End_Ring (AbGr M)) means :Def27: :: LMOD_XX1:def 27
for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & it . x = AbGr f );

existence
ex b₁ being Function of R,(End_Ring (AbGr M)) st
for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & b₁ . x = AbGr f )

proof end;

uniqueness
for b₁, b₂ being Function of R,(End_Ring (AbGr M)) st ( for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & b₁ . x = AbGr f ) ) & ( for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & b₂ . x = AbGr f ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def27 defines canHom LMOD_XX1:def 27 :
for R being comRing
for M being LeftMod of R
for b₃ being Function of R,(End_Ring (AbGr M)) holds
( b₃ = canHom M iff for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & b₃ . x = AbGr f ) );

Lm34: for R being comRing
for M being LeftMod of R holds canHom M is additive

proof end;

registration

let R be comRing;
let M be LeftMod of R;

cluster canHom M -> additive ;

coherence
canHom M is additive by Lm34;

end;

theorem :: LMOD_XX1:36

for R being comRing
for M being LeftMod of R
for a being Element of R holds (canHom M) . a is Homomorphism of (AbGr M),(AbGr M)

proof end;

Lm36: for R being comRing
for M being LeftMod of R holds canHom M is multiplicative

proof end;

Lm37: for R being comRing
for M being LeftMod of R
for f being Endomorphism of R,M st f = 1_End M holds
AbGr f = 1_End (AbGr M)

proof end;

Lm38: for R being comRing
for M being LeftMod of R holds canHom M is unity-preserving

proof end;

registration

let R be comRing;
let M be LeftMod of R;

cluster canHom M -> linear ;

coherence
canHom M is linear by Lm36, Lm38;

end;

registration

let R be comRing;
let M be LeftMod of R;

cluster AbGrLMod ((AbGr M),(canHom M)) -> non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;

coherence
( not AbGrLMod ((AbGr M),(canHom M)) is empty & AbGrLMod ((AbGr M),(canHom M)) is Abelian & AbGrLMod ((AbGr M),(canHom M)) is add-associative & AbGrLMod ((AbGr M),(canHom M)) is right_zeroed & AbGrLMod ((AbGr M),(canHom M)) is right_complementable & AbGrLMod ((AbGr M),(canHom M)) is vector-distributive & AbGrLMod ((AbGr M),(canHom M)) is scalar-distributive & AbGrLMod ((AbGr M),(canHom M)) is scalar-associative & AbGrLMod ((AbGr M),(canHom M)) is scalar-unital ) by Th14;

end;

theorem Th35: :: LMOD_XX1:37

for R being comRing
for M being LeftMod of R holds LModlmult ((AbGr M),(canHom M)) = the lmult of M

proof end;

theorem :: LMOD_XX1:38

for R being comRing
for M being strict LeftMod of R holds AbGrLMod ((AbGr M),(canHom M)) = M

proof end;

definition

let R be comRing;
let M be LeftMod of R;

func rho M -> Function of M,(AbGrLMod ((AbGr M),(canHom M))) equals :: LMOD_XX1:def 28
id M;

coherence
id M is Function of M,(AbGrLMod ((AbGr M),(canHom M))) ;

end;

:: deftheorem defines rho LMOD_XX1:def 28 :
for R being comRing
for M being LeftMod of R holds rho M = id M;

theorem Th37: :: LMOD_XX1:39

for R being comRing
for M being LeftMod of R holds
( rho M is additive & rho M is homogeneous )

proof end;

registration

let R be comRing;
let M be LeftMod of R;

cluster rho M -> additive homogeneous ;

coherence
( rho M is additive & rho M is homogeneous ) by Th37;

end;

theorem Th38: :: LMOD_XX1:40

for R being comRing
for M being LeftMod of R holds
( rho M is one-to-one & rho M is onto )

proof end;

theorem :: LMOD_XX1:41

for R being comRing
for M being LeftMod of R holds M ~= AbGrLMod ((AbGr M),(canHom M))

proof end;