:: Torsion $\mathbb Z$-module and Torsion-free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama
::
:: Copyright (c) 2014-2019 Association of Mizar Users

theorem Th1V: :: ZMODUL06:1
for R being commutative Ring
for V being LeftMod of R
for W being Subspace of V holds (1. R) (*) W = (Omega). W
proof end;

theorem :: ZMODUL06:2
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Subspace of V holds W1 /\ W2 is Subspace of (W1 + W3) /\ W2
proof end;

theorem ThIS1: :: ZMODUL06:3
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Subspace of V st W1 /\ W2 <> (0). V holds
(W1 + W3) /\ W2 <> (0). V
proof end;

theorem :: ZMODUL06:4
for V being Z_Module
for I, I1 being linearly-independent Subset of V st I1 c= I holds
(Lin (I \ I1)) /\ (Lin I1) = (0). V
proof end;

definition
let R be Ring;
let V be LeftMod of R;
let v be Vector of V;
attr v is torsion means :: ZMODUL06:def 1
ex i being Element of R st
( i <> 0. R & i * v = 0. V );
end;

:: deftheorem defines torsion ZMODUL06:def 1 :
for R being Ring
for V being LeftMod of R
for v being Vector of V holds
( v is torsion iff ex i being Element of R st
( i <> 0. R & i * v = 0. V ) );

ThTV1: for V being Z_Module holds 0. V is torsion
proof end;

registration
let V be Z_Module;
cluster 0. V -> torsion ;
coherence
0. V is torsion
by ThTV1;
end;

theorem :: ZMODUL06:5
for V being Z_Module
for v, u being Vector of V st v is torsion & u is torsion holds
v + u is torsion
proof end;

theorem :: ZMODUL06:6
for V being Z_Module
for v being Vector of V st v is torsion holds
- v is torsion
proof end;

theorem :: ZMODUL06:7
for V being Z_Module
for v, u being Vector of V st v is torsion & u is torsion holds
v - u is torsion
proof end;

theorem :: ZMODUL06:8
for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring st v is torsion holds
i * v is torsion
proof end;

theorem ThTV6: :: ZMODUL06:9
for V being Z_Module
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
( v is torsion iff w is torsion )
proof end;

registration
let V be Z_Module;
cluster torsion for Element of the carrier of V;
correctness
existence
ex b1 being Vector of V st b1 is torsion
;
proof end;
end;

theorem :: ZMODUL06:10
for V being Z_Module
for v being Vector of V st not v is torsion holds
not - v is torsion
proof end;

theorem :: ZMODUL06:11
for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring st not v is torsion & i <> 0 holds
not i * v is torsion
proof end;

theorem ThnTV3: :: ZMODUL06:12
for V being Z_Module
for v being Vector of V holds
( not v is torsion iff {v} is linearly-independent )
proof end;

definition
let V be Z_Module;
attr V is torsion means :defTorsionModule: :: ZMODUL06:def 2
for v being Vector of V holds v is torsion ;
end;

:: deftheorem defTorsionModule defines torsion ZMODUL06:def 2 :
for V being Z_Module holds
( V is torsion iff for v being Vector of V holds v is torsion );

ThTZM: for V being Z_Module holds (0). V is torsion
proof end;

registration
let V be Z_Module;
coherence
(0). V is torsion
by ThTZM;
end;

registration
existence
ex b1 being Z_Module st b1 is torsion
proof end;
end;

theorem LMINTRNG1: :: ZMODUL06:13
for v being Element of INT.Ring
for v1 being Integer st v = v1 holds
for n being Nat holds . (n,v) = n * v1
proof end;

theorem LMINTRNG2: :: ZMODUL06:14
for x, v being Element of INT.Ring
for v1 being Integer st v = v1 holds
. (x,v) = x * v1
proof end;

registration
existence
not for b1 being Z_Module holds b1 is torsion
proof end;
end;

registration
let V be non torsion Z_Module;
cluster non torsion for Element of the carrier of V;
existence
not for b1 being Vector of V holds b1 is torsion
by defTorsionModule;
end;

definition
let V be Z_Module;
attr V is torsion-free means :defTorsionFree: :: ZMODUL06:def 3
for v being Vector of V st v <> 0. V holds
not v is torsion ;
end;

:: deftheorem defTorsionFree defines torsion-free ZMODUL06:def 3 :
for V being Z_Module holds
( V is torsion-free iff for v being Vector of V st v <> 0. V holds
not v is torsion );

theorem ThMCTF: :: ZMODUL06:15
for V being Z_Module holds
( V is Mult-cancelable iff V is torsion-free )
proof end;

registration
coherence
for b1 being Mult-cancelable Z_Module holds b1 is torsion-free
by ThMCTF;
end;

registration
coherence
for b1 being torsion-free Z_Module holds b1 is Mult-cancelable
by ThMCTF;
end;

registration
coherence
for b1 being free Z_Module holds b1 is torsion-free
;
end;

registration
existence
ex b1 being Z_Module st
( b1 is torsion-free & b1 is free )
proof end;
end;

theorem :: ZMODUL06:16
for V being torsion-free Z_Module
for v being Vector of V holds
( v is torsion iff v = 0. V ) by defTorsionFree;

registration
let V be torsion-free Z_Module;
cluster -> torsion-free for Subspace of V;
coherence
for b1 being Subspace of V holds b1 is torsion-free
proof end;
end;

registration
let R be Ring;
let V be LeftMod of R;
coherence
(0). V is trivial
proof end;
end;

registration
coherence
for b1 being non trivial torsion-free Z_Module holds not b1 is torsion
proof end;
end;

registration
let R be Ring;
existence
ex b1 being LeftMod of R st b1 is trivial
proof end;
end;

registration
let K be non empty non degenerated right_complementable associative distributive left_unital Abelian add-associative right_zeroed doubleLoopStr ;
existence
ex b1 being non trivial ModuleStr over K st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict )
proof end;
end;

registration
let R be non degenerated Ring;
let V be non trivial LeftMod of R;
cluster non zero for Element of the carrier of V;
existence
not for b1 being Vector of V holds b1 is zero
proof end;
end;

theorem ThnTV4: :: ZMODUL06:17
for V being Z_Module
for v being Vector of V holds
( not v is torsion iff ( Lin {v} is free & v <> 0. V ) )
proof end;

registration
let V be non torsion Z_Module;
let v be non torsion Vector of V;
cluster Lin {v} -> free ;
coherence
Lin {v} is free
by ThnTV4;
end;

theorem ThLIV1: :: ZMODUL06:18
for V being Z_Module
for A being Subset of V
for v being Vector of V st A is linearly-independent & v in A holds
not v is torsion
proof end;

theorem ThLin1: :: ZMODUL06:19
for V being Z_Module
for v being Vector of V
for u being object st u in Lin {v} holds
ex i being Element of INT.Ring st u = i * v
proof end;

theorem ThLin2: :: ZMODUL06:20
for V being Z_Module
for v being Vector of V holds v in Lin {v} by ;

theorem :: ZMODUL06:21
for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring holds i * v in Lin {v} by ;

ThLin4: for V being Z_Module
for A being Subset of V holds A is Subset of (Lin A)

by ZMODUL05:30;

theorem ThLin5: :: ZMODUL06:22
for R being Ring
for V being LeftMod of R holds Lin {(0. V)} = (0). V
proof end;

registration
let V be torsion-free Z_Module;
let v be Vector of V;
cluster Lin {v} -> free ;
coherence
Lin {v} is free
proof end;
end;

theorem :: ZMODUL06:23
for V being Z_Module
for A1, A2 being Subset of V st A1 is linearly-independent & A2 is linearly-independent & A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent holds
(Lin A1) /\ (Lin A2) <> (0). V
proof end;

ThLin7: for V being Z_Module
for A being linearly-independent Subset of V holds A is Basis of (Lin A)

proof end;

theorem ThLin8: :: ZMODUL06:24
for V being Z_Module
for W being free Subspace of V
for I being Subset of V
for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + () & (Lin (I \ {v})) /\ () = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
proof end;

LmGCD1: for i1, i2 being Integer st i1,i2 are_coprime holds
ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1

proof end;

LmGCD: for i1, i2 being Element of INT.Ring st i1,i2 are_coprime holds
ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1

proof end;

theorem :: ZMODUL06:25
for V being Z_Module
for W being free Subspace of V ex A being Subset of V st
( A is Subset of W & A is linearly-independent & Lin A = (Omega). W )
proof end;

theorem LmFree2: :: ZMODUL06:26
for V being Z_Module
for W being free finite-rank Subspace of V ex A being finite Subset of V st
( A is finite Subset of W & A is linearly-independent & Lin A = (Omega). W & card A = rank W )
proof end;

theorem LmSumMod1: :: ZMODUL06:27
for V being torsion-free Z_Module
for v1, v2 being Vector of V st v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V holds
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {u} )
proof end;

theorem LmSumMod2: :: ZMODUL06:28
for V being torsion-free Z_Module
for v1, v2 being Vector of V st v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V holds
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) + (Lin {v2}) = Lin {u} )
proof end;

theorem LmSumMod3: :: ZMODUL06:29
for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v, u being Vector of V st v <> 0. V & u <> 0. V & W /\ () = (0). V & (W + ()) /\ () <> (0). V & () /\ () = (0). V holds
ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + ()) + () = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in () + () & w2 in () + () )
proof end;

theorem LmSumModX: :: ZMODUL06:30
for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ () <> (0). V holds
W + () is free
proof end;

registration
let V be torsion-free Z_Module;
let v be Vector of V;
let W be free finite-rank Subspace of V;
cluster W + () -> free ;
coherence
W + () is free
proof end;
end;

registration
let V be Z_Module;
let v be Vector of V;
let W be finitely-generated Subspace of V;
cluster W + () -> finitely-generated ;
coherence
W + () is finitely-generated
proof end;
end;

registration
let V be Z_Module;
let W1, W2 be finitely-generated Subspace of V;
cluster W1 + W2 -> finitely-generated ;
coherence
W1 + W2 is finitely-generated
proof end;
end;

theorem LMThSumMod2: :: ZMODUL06:31
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for W1s, W2s being Subspace of W
for W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
proof end;

registration
let V be torsion-free Z_Module;
let U1, U2 be free finite-rank Subspace of V;
cluster U1 + U2 -> free ;
correctness
coherence
U1 + U2 is free
;
proof end;
end;

registration
correctness
coherence
for b1 being finitely-generated torsion-free Z_Module holds b1 is free
;
proof end;
end;

theorem ThRankDirectSum: :: ZMODUL06:32
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st W1 /\ W2 = (0). V holds
rank (W1 + W2) = (rank W1) + (rank W2)
proof end;

theorem :: ZMODUL06:33
for V being free finite-rank Z_Module
for W1, W2 being free finite-rank Subspace of V st V is_the_direct_sum_of W1,W2 holds
rank V = (rank W1) + (rank W2)
proof end;

theorem ThISRank1: :: ZMODUL06:34
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V holds rank (W1 /\ W2) <= rank W1
proof end;

theorem LmRank0a: :: ZMODUL06:35
for V being torsion-free Z_Module
for v being Vector of V st v <> 0. V holds
rank () = 1
proof end;

theorem :: ZMODUL06:36
for V being Z_Module holds rank ((0). V) = 0
proof end;

theorem LmRank1: :: ZMODUL06:37
for V being torsion-free Z_Module
for v, u being Vector of V st v <> 0. V & u <> 0. V & () /\ () <> (0). V holds
rank (() + ()) = 1
proof end;

theorem LmRank2: :: ZMODUL06:38
for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ () <> (0). V holds
rank (W + ()) = rank W
proof end;

theorem LmISRank21: :: ZMODUL06:39
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st W1 /\ () <> (0). V & W2 /\ () <> (0). V holds
(W1 /\ W2) /\ () <> (0). V
proof end;

theorem ThTF3C: :: ZMODUL06:40
for R being Ring
for V, W being LeftMod of R
for T being linear-transformation of V,W
for A being Subset of V holds T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A))
proof end;

theorem HM0: :: ZMODUL06:41
for R being Ring
for X, Y being LeftMod of R
for L being linear-transformation of X,Y holds L . (0. X) = 0. Y
proof end;

theorem HM1: :: ZMODUL06:42
for R being Ring
for X, Y being LeftMod of R
for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
proof end;

theorem :: ZMODUL06:43
for R being Ring
for X, Y being LeftMod of R
for l being Linear_Combination of X
for L being linear-transformation of X,Y st L is bijective holds
L @* l = l * (L ")
proof end;

theorem :: ZMODUL06:44
for R being Ring
for X, Y being LeftMod of R
for X0 being Subset of X
for L being linear-transformation of X,Y
for l being Linear_Combination of L .: X0 st X0 = the carrier of X & L is one-to-one holds
L # l = l * L
proof end;

HM4: for R being Ring
for X, Y being LeftMod of R
for A being Subset of X
for L being linear-transformation of X,Y st L is bijective & A is linearly-independent holds
L .: A is linearly-independent

proof end;

theorem HM6: :: ZMODUL06:45
for R being Ring
for X, Y being LeftMod of R
for A being Subset of X
for L being linear-transformation of X,Y st L is bijective holds
( A is linearly-independent iff L .: A is linearly-independent )
proof end;

theorem HM7: :: ZMODUL06:46
for R being Ring
for X, Y being LeftMod of R
for A being Subset of X
for T being linear-transformation of X,Y st T is bijective holds
T .: the carrier of (Lin A) = the carrier of (Lin (T .: A))
proof end;

theorem HM8: :: ZMODUL06:47
for R being Ring
for Y being LeftMod of R
for A being Subset of Y holds Lin A is strict Subspace of (Omega). Y
proof end;

HM9: for R being Ring
for X, Y being LeftMod of R
for T being linear-transformation of X,Y st T is bijective & X is free holds
Y is free

proof end;

theorem :: ZMODUL06:48
for R being Ring
for X, Y being LeftMod of R
for T being linear-transformation of X,Y st T is bijective holds
( X is free iff Y is free )
proof end;

HM11: for X, Y being free Z_Module
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y

proof end;

theorem HM12: :: ZMODUL06:49
for X, Y being free Z_Module
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective holds
( A is Basis of X iff T .: A is Basis of Y )
proof end;

HM13: for X, Y being free Z_Module
for T being linear-transformation of X,Y st T is bijective & X is finite-rank holds
Y is finite-rank

proof end;

theorem :: ZMODUL06:50
for X, Y being free Z_Module
for T being linear-transformation of X,Y st T is bijective holds
( X is finite-rank iff Y is finite-rank )
proof end;

theorem HM15: :: ZMODUL06:51
for X, Y being free finite-rank Z_Module
for T being linear-transformation of X,Y st T is bijective holds
rank X = rank Y
proof end;

theorem ThRankS1: :: ZMODUL06:52
for V being Z_Module
for W being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring holds
rank (a (*) W) = rank W
proof end;

theorem :: ZMODUL06:53
for V being Z_Module
for W1, W2, W3 being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 /\ W2) = rank (W1 /\ W2)
proof end;

theorem :: ZMODUL06:54
for V being torsion-free Z_Module
for W1, W2, W3 being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 + W2) = rank (W1 + W2)
proof end;

theorem ThISRank2: :: ZMODUL06:55
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ () <> (0). V ) holds
rank (W1 /\ W2) = rank W1
proof end;

theorem :: ZMODUL06:56
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st rank (W1 /\ W2) < rank W1 holds
ex v being Vector of V st
( v in I & (W1 /\ W2) /\ () = (0). V ) by ThISRank2;

theorem LmISRank41: :: ZMODUL06:57
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st rank (W1 /\ W2) = rank W1 holds
for v being Vector of V st v in I holds
(W1 /\ W2) /\ () <> (0). V
proof end;

theorem LmISRank42: :: ZMODUL06:58
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ () <> (0). V ) holds
rank (W1 + W2) = rank W2
proof end;

theorem ThISRank4: :: ZMODUL06:59
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 holds
rank (W1 + W2) = rank W2
proof end;

theorem VECT9Th26: :: ZMODUL06:60
for G being Field
for V being VectSp of G
for A being Subset of V st A is linearly-independent holds
A is Basis of (Lin A)
proof end;

theorem LmISRank501: :: ZMODUL06:61
for V being free finite-rank Mult-cancelable Z_Module
for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)
proof end;

theorem LmISRank51X: :: ZMODUL06:62
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)
proof end;

theorem :: ZMODUL06:63
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st rank (W1 + W2) = rank W2 holds
rank (W1 /\ W2) = rank W1
proof end;

theorem :: ZMODUL06:64
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W1 /\ () = (0). V & (W1 + W2) /\ () = (0). V holds
rank ((W1 + ()) /\ W2) = rank (W1 /\ W2)
proof end;

theorem LmRank41: :: ZMODUL06:65
for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ () <> (0). V holds
rank (W /\ ()) = 1
proof end;

theorem LmSumMod4: :: ZMODUL06:66
for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ () <> (0). V holds
ex u being Vector of V st
( u <> 0. V & W /\ () = Lin {u} )
proof end;

theorem LmRank421: :: ZMODUL06:67
for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for u, v being Vector of V st W /\ () = (0). V & (W + ()) /\ () <> (0). V holds
W /\ () = (0). V
proof end;

theorem :: ZMODUL06:68
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ () <> (0). V holds
W2 /\ () <> (0). V
proof end;

theorem ThRankS5: :: ZMODUL06:69
for V being torsion-free Z_Module
for W1, W2, W3 being free finite-rank Subspace of V st rank (W1 + W2) = rank W2 & W3 is Subspace of W1 holds
rank (W3 + W2) = rank W2
proof end;

theorem :: ZMODUL06:70
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st rank (W1 + W2) = rank W2 holds
for v being Vector of V st v in I holds
(W1 /\ W2) /\ () <> (0). V
proof end;

theorem :: ZMODUL06:71
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 holds
ex a being Element of INT.Ring st a (*) W1 is Subspace of W2
proof end;