:: Torsion-part of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


theorem LMThFRat31X: :: ZMODUL07:1
for n being Integer st n <> 0 & n <> - 1 & n <> - 2 holds
not n / (n + 1) in INT
proof end;

registration
cluster V31() integer non zero complex ext-real rational prime g_integer g_rational for Element of the carrier of INT.Ring;
existence
ex b1 being Element of INT.Ring st
( b1 is prime & not b1 is zero )
proof end;
end;

registration
cluster prime -> non zero for Element of the carrier of INT.Ring;
coherence
for b1 being Element of INT.Ring st b1 is prime holds
not b1 is zero ;
end;

LmDOMRNG: for V, W being non empty 1-sorted
for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
proof end;

theorem LmTF1: :: ZMODUL07:2
for V being Z_Module
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B ) ) )
proof end;

theorem LmTF1C: :: ZMODUL07:3
for V being Z_Module
for I being finite Subset of V
for W being Submodule of V st ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
proof end;

LmTF1B: for V being Z_Module
for I being finite Subset of V
for W being Submodule of V
for a being Element of INT.Ring st a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) holds
for v being VECTOR of V st v in Lin I holds
a * v in W
proof end;

theorem LmTF1D: :: ZMODUL07:4
for V being free finite-rank Z_Module
for I being linearly-independent Subset of V holds I is finite
proof end;

registration
let V be free finite-rank Z_Module;
cluster linearly-independent -> finite for Element of bool the carrier of V;
coherence
for b1 being Subset of V st b1 is linearly-independent holds
b1 is finite by LmTF1D;
end;

LmTF1A: for V being free finite-rank Z_Module
for A being Subset of V st A is linearly-independent holds
ex B being finite Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) )
proof end;

theorem LmRankSX11: :: ZMODUL07:5
for V being free finite-rank Z_Module
for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )
proof end;

theorem LmRankSX1: :: ZMODUL07:6
for V being free finite-rank Z_Module
for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V st
( A c= I & rank V = card I )
proof end;

theorem LmRankSX2: :: ZMODUL07:7
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V
for I1 being Basis of W1 ex I being finite linearly-independent Subset of V st
( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )
proof end;

theorem :: ZMODUL07:8
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V st W2 is Submodule of W1 holds
ex W3 being free finite-rank Submodule of V st
( rank W1 = (rank W2) + (rank W3) & W2 /\ W3 = (0). V & W3 is Submodule of W1 )
proof end;

theorem :: ZMODUL07:9
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V ex W3 being free finite-rank Submodule of V st
( rank (W1 + W2) = (rank W1) + (rank W3) & W1 /\ W3 = (0). V & W3 is Submodule of W1 + W2 )
proof end;

theorem :: ZMODUL07:10
for V being free finite-rank Z_Module
for W1, W2 being Submodule of V holds rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V)
proof end;

definition
let V be LeftMod of INT.Ring ;
func torsion_part V -> strict Subspace of V means :defTorsionPart: :: ZMODUL07:def 1
 the carrier of it = { v where v is Vector of V : v is torsion } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { v where v is Vector of V : v is torsion }
proof end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { v where v is Vector of V : v is torsion } & the carrier of b2 = { v where v is Vector of V : v is torsion } holds
b1 = b2 by ZMODUL01:45;
end;

:: deftheorem defTorsionPart defines torsion_part ZMODUL07:def 1 :
for V being LeftMod of INT.Ring
for b2 being strict Subspace of V holds
( b2 = torsion_part V iff the carrier of b2 = { v where v is Vector of V : v is torsion } );

theorem LmTP1: :: ZMODUL07:11
for V being Z_Module
for v being Vector of V holds
( v is torsion iff v in torsion_part V )
proof end;

theorem :: ZMODUL07:12
for V being Z_Module holds
( V is torsion-free iff torsion_part V = (0). V )
proof end;

ThTF1: for V being Z_Module holds VectQuot (V,(torsion_part V)) is torsion-free
proof end;

registration
let V be Z_Module;
cluster VectQuot (V,(torsion_part V)) -> torsion-free ;
coherence
VectQuot (V,(torsion_part V)) is torsion-free by ThTF1;
end;

definition
let R be Ring;
let V be LeftMod of R;
let W be Subspace of V;
func ZQMorph (V,W) -> linear-transformation of V,(VectQuot (V,W)) means :defMophVW: :: ZMODUL07:def 2
 for v being Element of V holds it . v = v + W;
existence
ex b1 being linear-transformation of V,(VectQuot (V,W)) st
for v being Element of V holds b1 . v = v + W
proof end;
uniqueness
for b1, b2 being linear-transformation of V,(VectQuot (V,W)) st ( for v being Element of V holds b1 . v = v + W ) & ( for v being Element of V holds b2 . v = v + W ) holds
b1 = b2
proof end;
end;

:: deftheorem defMophVW defines ZQMorph ZMODUL07:def 2 :
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for b4 being linear-transformation of V,(VectQuot (V,W)) holds
( b4 = ZQMorph (V,W) iff for v being Element of V holds b4 . v = v + W );

registration
let R be Ring;
let V be LeftMod of R;
let W be Subspace of V;
cluster ZQMorph (V,W) -> onto ;
coherence
ZQMorph (V,W) is onto
proof end;
end;

theorem :: ZMODUL07:13
for V, W being Z_Module
for T being linear-transformation of V,W
for s being FinSequence of V
for t being FinSequence of W st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being VECTOR of V st
( si = s . i & t . i = T . si ) ) holds
Sum t = T . (Sum s)
proof end;

registration
let V be finitely-generated Z_Module;
let W be Submodule of V;
cluster VectQuot (V,W) -> finitely-generated ;
coherence
VectQuot (V,W) is finitely-generated
proof end;
end;

registration
let V be finitely-generated Z_Module;
cluster VectQuot (V,(torsion_part V)) -> free ;
correctness
coherence
VectQuot (V,(torsion_part V)) is free ;
;
end;

definition
func Rat-Module -> ModuleStr over INT.Ring equals :: ZMODUL07:def 3
 ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);
coherence
ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #) is ModuleStr over INT.Ring ;
end;

:: deftheorem defines Rat-Module ZMODUL07:def 3 :
Rat-Module = ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);

registration
cluster Rat-Module -> non empty ;
coherence
not Rat-Module is empty ;
end;

registration
cluster Rat-Module -> right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;
correctness
coherence
( Rat-Module is Abelian & Rat-Module is add-associative & Rat-Module is right_zeroed & Rat-Module is right_complementable & Rat-Module is scalar-distributive & Rat-Module is vector-distributive & Rat-Module is scalar-associative & Rat-Module is scalar-unital );
proof end;
end;

theorem LMTFRat1: :: ZMODUL07:14
for v being Element of F_Rat
for v1 being Rational st v = v1 holds
for n being Nat holds (Nat-mult-left F_Rat) . (n,v) = n * v1
proof end;

theorem LMTFRat2: :: ZMODUL07:15
for x being Integer
for v being Element of F_Rat
for v1 being Rational st v = v1 holds
(Int-mult-left F_Rat) . (x,v) = x * v1
proof end;

registration
cluster Rat-Module -> torsion-free ;
correctness
coherence
Rat-Module is torsion-free ;
proof end;
end;

registration
cluster Rat-Module -> non trivial ;
correctness
coherence
not Rat-Module is trivial ;
;
end;

theorem LMThFRat31: :: ZMODUL07:16
for s being Element of Rat-Module holds Lin {s} <> Rat-Module
proof end;

theorem LMThFRat32: :: ZMODUL07:17
for s, t being Element of Rat-Module st s <> t holds
not {s,t} is linearly-independent
proof end;

registration
cluster Rat-Module -> non free ;
correctness
coherence
not Rat-Module is free ;
proof end;
end;

theorem :: ZMODUL07:18
for A being finite Subset of Rat-Module ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )
proof end;

registration
cluster Rat-Module -> non finitely-generated ;
correctness
coherence
not Rat-Module is finitely-generated ;
;
end;

theorem :: ZMODUL07:19
for A being finite Subset of Rat-Module holds rank (Lin A) <= 1
proof end;

registration
let W be free finite-rank Z_Module;
let V be Z_Module;
let T be linear-transformation of V,W;
cluster im T -> free finite-rank ;
correctness
coherence
( im T is finite-rank & im T is free );
;
end;

definition
let W be free finite-rank Z_Module;
let V be Z_Module;
let T be linear-transformation of V,W;
func rank T -> Nat equals :: ZMODUL07:def 4
 rank (im T);
coherence
rank (im T) is Nat ;
end;

:: deftheorem defines rank ZMODUL07:def 4 :
for W being free finite-rank Z_Module
for V being Z_Module
for T being linear-transformation of V,W holds rank T = rank (im T);

definition
let V be free finite-rank Z_Module;
let W be Z_Module;
let T be linear-transformation of V,W;
func nullity T -> Nat equals :: ZMODUL07:def 5
 rank (ker T);
coherence
rank (ker T) is Nat ;
end;

:: deftheorem defines nullity ZMODUL07:def 5 :
for V being free finite-rank Z_Module
for W being Z_Module
for T being linear-transformation of V,W holds nullity T = rank (ker T);

theorem ZM05Th35: :: ZMODUL07:20
for W, V being free finite-rank Z_Module
for A being Subset of V
for B being linearly-independent Subset of V
for T being linear-transformation of V,W st rank V = card B & A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
proof end;

theorem ZM05Th59: :: ZMODUL07:21
for W, V being free finite-rank Z_Module
for A being Subset of V
for B being linearly-independent Subset of V
for T being linear-transformation of V,W
for l being Linear_Combination of B \ A st rank V = card B & A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @* l)
proof end;

theorem LMTh441: :: ZMODUL07:22
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 st A c= the carrier of (ker T) holds
Lin (T .: A) = (0). W
proof end;

theorem LMTh44: :: ZMODUL07:23
for R being Ring
for V, W being LeftMod of R
for T being linear-transformation of V,W
for A, B, X being Subset of V st A c= the carrier of (ker T) & X = B \/ A holds
Lin (T .: X) = Lin (T .: B)
proof end;

:: Rank-nullity theorem
theorem Th44: :: ZMODUL07:24
for V, W being free finite-rank Z_Module
for T being linear-transformation of V,W holds rank V = (rank T) + (nullity T)
proof end;

theorem :: ZMODUL07:25
for V, W being free finite-rank Z_Module
for T being linear-transformation of V,W st T is one-to-one holds
rank V = rank T
proof end;

::: canonical decomposition
definition
let R be Ring;
let V, W be LeftMod of R;
let T be linear-transformation of V,W;
func Zdecom T -> linear-transformation of (VectQuot (V,(ker T))),(im T) means :defdecom: :: ZMODUL07:def 6
( it is bijective & ( for v being Element of V holds it . ((ZQMorph (V,(ker T))) . v) = T . v ) );
existence
ex b1 being linear-transformation of (VectQuot (V,(ker T))),(im T) st
( b1 is bijective & ( for v being Element of V holds b1 . ((ZQMorph (V,(ker T))) . v) = T . v ) )
proof end;
uniqueness
for b1, b2 being linear-transformation of (VectQuot (V,(ker T))),(im T) st b1 is bijective & ( for v being Element of V holds b1 . ((ZQMorph (V,(ker T))) . v) = T . v ) & b2 is bijective & ( for v being Element of V holds b2 . ((ZQMorph (V,(ker T))) . v) = T . v ) holds
b1 = b2
proof end;
end;

:: deftheorem defdecom defines Zdecom ZMODUL07:def 6 :
for R being Ring
for V, W being LeftMod of R
for T being linear-transformation of V,W
for b5 being linear-transformation of (VectQuot (V,(ker T))),(im T) holds
( b5 = Zdecom T iff ( b5 is bijective & ( for v being Element of V holds b5 . ((ZQMorph (V,(ker T))) . v) = T . v ) ) );

theorem :: ZMODUL07:26
for R being Ring
for V, W being LeftMod of R
for T being linear-transformation of V,W holds T = (Zdecom T) * (ZQMorph (V,(ker T)))
proof end;

theorem LMFirst1: :: ZMODUL07:27
for R being Ring
for V, U, W being LeftMod of R
for f being linear-transformation of V,U
for g being linear-transformation of U,W holds g * f is linear-transformation of V,W
proof end;

definition
let R be Ring;
let V, U, W be LeftMod of R;
let f be linear-transformation of V,U;
let g be linear-transformation of U,W;
:: original: (#)
redefine func g * f -> linear-transformation of V,W;
correctness
coherence
f (#) g is linear-transformation of V,W;
by LMFirst1;
end;

theorem LMFirst2: :: ZMODUL07:28
for R being Ring
for V, W being LeftMod of R
for f being linear-transformation of V,W holds the carrier of (ker f) = f " {(0. W)}
proof end;

theorem LMFirst3: :: ZMODUL07:29
for R being Ring
for V, U, W being LeftMod of R
for f being linear-transformation of V,U
for g being linear-transformation of U,W holds the carrier of (ker (g * f)) = f " the carrier of (ker g)
proof end;

theorem LMFirst4: :: ZMODUL07:30
for R being Ring
for V, W being LeftMod of R
for f being linear-transformation of V,W st f is onto holds
im f = (Omega). W
proof end;

theorem LMFirst5: :: ZMODUL07:31
for R being Ring
for V being LeftMod of R
for W being Subspace of V holds ker (ZQMorph (V,W)) = (Omega). W
proof end;

theorem LmStrict11a: :: ZMODUL07:32
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V
for v being Vector of V st Ws = (Omega). W holds
v + W = v + Ws
proof end;

theorem LmStrict11: :: ZMODUL07:33
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V
for A being object st Ws = (Omega). W holds
( A is Coset of W iff A is Coset of Ws )
proof end;

theorem LmStrict1: :: ZMODUL07:34
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
CosetSet (V,W) = CosetSet (V,Ws)
proof end;

theorem LmStrict2: :: ZMODUL07:35
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
addCoset (V,W) = addCoset (V,Ws)
proof end;

theorem LmStrict3: :: ZMODUL07:36
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
lmultCoset (V,W) = lmultCoset (V,Ws)
proof end;

theorem ThStrict1: :: ZMODUL07:37
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
VectQuot (V,W) = VectQuot (V,Ws)
proof end;

theorem :: ZMODUL07:38
for R being Ring
for V, U being LeftMod of R
for V1 being Submodule of V
for U1 being Submodule of U
for f being linear-transformation of V,U st f is onto & the carrier of V1 = f " the carrier of U1 holds
ex F being linear-transformation of (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective
proof end;

theorem :: ZMODUL07:39
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for U1 being Submodule of W1 + W2
for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds
ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective
proof end;

theorem :: ZMODUL07:40
for R being Ring
for V being LeftMod of R
for W1 being Submodule of V
for W2 being Submodule of W1
for U1 being Submodule of V
for U2 being Submodule of VectQuot (V,U1) st U1 = W2 & U2 = VectQuot (W1,W2) holds
ex F being linear-transformation of (VectQuot ((VectQuot (V,U1)),U2)),(VectQuot (V,W1)) st F is bijective
proof end;

registration
let V be Z_Module;
let a be non zero Element of INT.Ring;
cluster VectQuot (V,(a (*) V)) -> torsion ;
correctness
coherence
VectQuot (V,(a (*) V)) is torsion ;
proof end;
end;

theorem ThTrivial1: :: ZMODUL07:41
for R being Ring
for V being trivial LeftMod of R holds (Omega). V = (0). V
proof end;

theorem ThTrivial2: :: ZMODUL07:42
for R being Ring
for V being LeftMod of R
for v being Vector of V st v <> 0. V holds
not Lin {v} is trivial
proof end;

theorem LMCLUS1: :: ZMODUL07:43
ex V being Z_Module ex p being Element of INT.Ring st
( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial )
proof end;

registration
cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() torsion for ModuleStr over INT.Ring ;
correctness
existence
not for b1 being torsion Z_Module holds b1 is trivial ;
proof end;
end;

registration
cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() non torsion-free for ModuleStr over INT.Ring ;
correctness
existence
not for b1 being Z_Module holds b1 is torsion-free ;
proof end;
end;

registration
let V be non torsion-free Z_Module;
cluster non zero torsion for Element of the carrier of V;
correctness
existence
ex b1 being Vector of V st
( not b1 is zero & b1 is torsion );
proof end;
end;

registration
cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() finitely-generated for ModuleStr over INT.Ring ;
correctness
existence
not for b1 being finitely-generated Z_Module holds b1 is trivial ;
proof end;
end;

theorem ThTFX: :: ZMODUL07:44
for V being Z_Module holds
( V is torsion-free iff (Omega). V is torsion-free )
proof end;

registration
cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed non torsion-free -> non trivial non torsion-free for ModuleStr over INT.Ring ;
correctness
coherence
for b1 being non torsion-free Z_Module holds not b1 is trivial ;
proof end;
end;

registration
cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() Mult-cancelable free finite-rank finitely-generated torsion-free for ModuleStr over INT.Ring ;
correctness
existence
not for b1 being finitely-generated torsion-free Z_Module holds b1 is trivial ;
proof end;
end;

registration
let V be non trivial finitely-generated torsion-free Z_Module;
let p be prime Element of INT.Ring;
cluster VectQuot (V,(p (*) V)) -> non trivial ;
coherence
not VectQuot (V,(p (*) V)) is trivial
proof end;
end;

registration
cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() finitely-generated torsion for ModuleStr over INT.Ring ;
correctness
existence
ex b1 being torsion Z_Module st b1 is finitely-generated ;
proof end;
end;

registration
cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() finitely-generated torsion for ModuleStr over INT.Ring ;
correctness
existence
not for b1 being finitely-generated torsion Z_Module holds b1 is trivial ;
proof end;
end;

registration
let V be non trivial finitely-generated torsion-free Z_Module;
let p be prime Element of INT.Ring;
cluster VectQuot (V,(p (*) V)) -> finitely-generated torsion ;
correctness
coherence
( VectQuot (V,(p (*) V)) is finitely-generated & VectQuot (V,(p (*) V)) is torsion );
;
end;

registration
let V be non torsion Z_Module;
cluster VectQuot (V,(torsion_part V)) -> non trivial ;
correctness
coherence
not VectQuot (V,(torsion_part V)) is trivial ;
proof end;
end;