:: Category of Left Modules
:: by Micha{\l} Muzalewski
::
:: Received December 12, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

::
:: 2. Domains of left modules
::
definition
let R be Ring;
mode LeftMod_DOMAIN of R ->  non empty set  means :Def1: :: MODCAT_1:def 1
 for x being Element of it holds x is strict LeftMod of R;
existence
 ex b1 being non empty set st
for x being Element of b1 holds x is strict LeftMod of R
proofend;
end;

:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def_1_:_
 for R being Ring
for b2 being non empty set holds
( b2 is LeftMod_DOMAIN of R iff for x being Element of b2 holds x is strict LeftMod of R );

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
:: original:Element
redefine mode Element of V ->  LeftMod of R;
coherence
 for b1 being Element of V holds b1 is LeftMod of R by Def1;
end;

registration
let R be Ring;
let V be LeftMod_DOMAIN of R;
cluster non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) for Element of V;
existence
 ex b1 being Element of V st b1 is strict
proofend;
end;

definition
let R be Ring;
mode LModMorphism_DOMAIN of R ->  non empty set  means :Def2: :: MODCAT_1:def 2
 for x being Element of it holds x is strict LModMorphism of R;
existence
 ex b1 being non empty set st
for x being Element of b1 holds x is strict LModMorphism of R
proofend;
end;

:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def_2_:_
 for R being Ring
for b2 being non empty set holds
( b2 is LModMorphism_DOMAIN of R iff for x being Element of b2 holds x is strict LModMorphism of R );

definition
let R be Ring;
let M be LModMorphism_DOMAIN of R;
:: original:Element
redefine mode Element of M ->  LModMorphism of R;
coherence
 for b1 being Element of M holds b1 is LModMorphism of R by Def2;
end;

registration
let R be Ring;
let M be LModMorphism_DOMAIN of R;
cluster strict LModMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proofend;
end;

theorem Th1: :: MODCAT_1:1
for R being Ring
for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R
proofend;

definition
let R be Ring;
let G, H be LeftMod of R;
mode LModMorphism_DOMAIN of G,H ->  LModMorphism_DOMAIN of R means :Def3: :: MODCAT_1:def 3
 for x being Element of it holds x is strict Morphism of G,H;
existence
 ex b1 being LModMorphism_DOMAIN of R st
for x being Element of b1 holds x is strict Morphism of G,H
proofend;
end;

:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def_3_:_
 for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of R holds
( b4 is LModMorphism_DOMAIN of G,H iff for x being Element of b4 holds x is strict Morphism of G,H );

theorem Th2: :: MODCAT_1:2
for D being non empty set
for R being Ring
for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
proofend;

theorem :: MODCAT_1:3
for R being Ring
for G, H being LeftMod of R
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
proofend;

definition
let R be Ring;
let G, H be LeftMod of R;
func Morphs (G,H) ->  LModMorphism_DOMAIN of G,H means :Def4: :: MODCAT_1:def 4
 for x being set holds
( x in it iff x is strict Morphism of G,H );
existence
 ex b1 being LModMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is strict Morphism of G,H )
proofend;
uniqueness
 for b1, b2 being LModMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff x is strict Morphism of G,H ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Morphs MODCAT_1:def_4_:_
 for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of G,H holds
( b4 = Morphs (G,H) iff for x being set holds
( x in b4 iff x is strict Morphism of G,H ) );

definition
let R be Ring;
let G, H be LeftMod of R;
let M be LModMorphism_DOMAIN of G,H;
:: original:Element
redefine mode Element of M ->  Morphism of G,H;
coherence
 for b1 being Element of M holds b1 is Morphism of G,H by Def3;
end;

::
:: 4a. Category of left modules - objects
::
definition
let x, y be set ;
let R be Ring;
pred GO x,y,R means :Def5: :: MODCAT_1:def 5
 ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) );
end;

:: deftheorem Def5 defines GO MODCAT_1:def_5_:_
 for x, y being set
for R being Ring holds
( GO x,y,R iff ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) ) );

theorem Th4: :: MODCAT_1:4
for R being Ring
for x, y1, y2 being set st GO x,y1,R & GO x,y2,R holds
y1 = y2
proofend;

theorem Th5: :: MODCAT_1:5
for R being Ring
for UN being Universe ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x, TrivialLMod R,R )
proofend;

definition
let UN be Universe;
let R be Ring;
func LModObjects (UN,R) ->  set  means :Def6: :: MODCAT_1:def 6
 for y being set holds
( y in it iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines LModObjects MODCAT_1:def_6_:_
 for UN being Universe
for R being Ring
for b3 being set holds
( b3 = LModObjects (UN,R) iff for y being set holds
( y in b3 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) );

theorem Th6: :: MODCAT_1:6
for UN being Universe
for R being Ring holds TrivialLMod R in LModObjects (UN,R)
proofend;

registration
let UN be Universe;
let R be Ring;
cluster LModObjects (UN,R) ->  non empty ;
coherence
 not LModObjects (UN,R) is empty by Th6;
end;

theorem Th7: :: MODCAT_1:7
for UN being Universe
for R being Ring
for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R
proofend;

definition
let UN be Universe;
let R be Ring;
:: original:LModObjects
redefine func LModObjects (UN,R) ->  LeftMod_DOMAIN of R;
coherence
 LModObjects (UN,R) is LeftMod_DOMAIN of R
proofend;
end;

::
:: 4b. Category of left modules - morphisms
::
definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func Morphs V ->  LModMorphism_DOMAIN of R means :Def7: :: MODCAT_1:def 7
 for x being set holds
( x in it iff ex G, H being strict Element of V st x is strict Morphism of G,H );
existence
 ex b1 being LModMorphism_DOMAIN of R st
for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proofend;
uniqueness
 for b1, b2 being LModMorphism_DOMAIN of R st ( for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Morphs MODCAT_1:def_7_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being LModMorphism_DOMAIN of R holds
( b3 = Morphs V iff for x being set holds
( x in b3 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

::
:: 4c. Category of left modules - dom,cod,id
::
definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
let F be Element of Morphs V;
func dom' F ->  Element of V equals :: MODCAT_1:def 8
 dom F;
coherence
 dom F is Element of V
proofend;
func cod' F ->  Element of V equals :: MODCAT_1:def 9
 cod F;
coherence
 cod F is Element of V
proofend;
end;

:: deftheorem  defines dom' MODCAT_1:def_8_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds dom' F = dom F;

:: deftheorem  defines cod' MODCAT_1:def_9_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds cod' F = cod F;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
let G be Element of V;
func ID G ->  strict Element of Morphs V equals :: MODCAT_1:def 10
 ID G;
coherence
 ID G is strict Element of Morphs V
proofend;
end;

:: deftheorem  defines ID MODCAT_1:def_10_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for G being Element of V holds ID G = ID G;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func dom V ->  Function of (Morphs V),V means :Def11: :: MODCAT_1:def 11
 for f being Element of Morphs V holds it . f = dom' f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = dom' f
proofend;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom' f ) & ( for f being Element of Morphs V holds b2 . f = dom' f ) holds
b1 = b2
proofend;
func cod V ->  Function of (Morphs V),V means :Def12: :: MODCAT_1:def 12
 for f being Element of Morphs V holds it . f = cod' f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = cod' f
proofend;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod' f ) & ( for f being Element of Morphs V holds b2 . f = cod' f ) holds
b1 = b2
proofend;
canceled;
end;

:: deftheorem Def11 defines dom MODCAT_1:def_11_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of (Morphs V),V holds
( b3 = dom V iff for f being Element of Morphs V holds b3 . f = dom' f );

:: deftheorem Def12 defines cod MODCAT_1:def_12_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of (Morphs V),V holds
( b3 = cod V iff for f being Element of Morphs V holds b3 . f = cod' f );

:: deftheorem  MODCAT_1:def_13_:_
canceled;

::
:: 4d. Category of left modules - superposition
::
theorem Th8: :: MODCAT_1:8
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proofend;

theorem Th9: :: MODCAT_1:9
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
g * f in Morphs V
proofend;

theorem Th10: :: MODCAT_1:10
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
proofend;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func comp V ->  PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def14: :: MODCAT_1:def 14
( ( for g, f being Element of Morphs V holds
( [g,f] in dom it iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds
it . (g,f) = g * f ) );
existence
 ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines comp MODCAT_1:def_14_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b3 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b3 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b3 holds
b3 . (g,f) = g * f ) ) );

theorem Th11: :: MODCAT_1:11
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
proofend;

::
:: 4e. Definition of Category of left modules
::
definition
let UN be Universe;
let R be Ring;
func LModCat (UN,R) ->  strict CatStr  equals :: MODCAT_1:def 15
 CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);
coherence
 CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #) is strict CatStr ;
end;

:: deftheorem  defines LModCat MODCAT_1:def_15_:_
 for UN being Universe
for R being Ring holds LModCat (UN,R) = CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);

registration
let UN be Universe;
let R be Ring;
cluster LModCat (UN,R) ->  non empty non void strict ;
coherence
 ( not LModCat (UN,R) is void & not LModCat (UN,R) is empty ) ;
end;

theorem Th12: :: MODCAT_1:12
for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
proofend;

registration
let UN be Universe;
let R be Ring;
cluster  ->  strict for Element of Morphs (LModObjects (UN,R));
coherence
 for b1 being Element of Morphs (LModObjects (UN,R)) holds b1 is strict
proofend;
end;

theorem :: MODCAT_1:13
canceled;

theorem :: MODCAT_1:14
canceled;

theorem Th15: :: MODCAT_1:15
for UN being Universe
for R being Ring
for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
proofend;

theorem Th16: :: MODCAT_1:16
for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
proofend;

Lm1:  for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
proofend;

Lm2:  for UN being Universe
for R being Ring
for f, g, h being Morphism of (LModCat (UN,R)) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proofend;

registration
let UN be Universe;
let R be Ring;
cluster LModCat (UN,R) ->  strict Category-like transitive associative reflexive ;
coherence
 ( LModCat (UN,R) is Category-like & LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
proofend;
end;