:: Torsion $\mathbb Z$-module and Torsion-free $\mathbb Z$-module :: by Yuichi Futa , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama :: :: Received November 29, 2014 :: Copyright (c) 2014-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies GAUSSINT, NUMBERS, SUBSET_1, RLVECT_1, STRUCT_0, PBOOLE, FUNCT_4, FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOM, RLSUB_2, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, FUNCOP_1, RLSUB_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2, INT_3, COMPLEX1, INT_2, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, MONOID_0, ZMODUL02, RLVECT_5, ZMODUL04, ZMODUL05, ZMODUL06, MOD_3, FUNCSDOM, VECTSP_2, BINOP_1, LATTICES, VECTSP10; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, ORDINAL1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1, INT_2, REALSET1, FUNCT_4, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, INT_3, VECTSP_7, VECTSP_9, VECTSP10, MATRLIN, BINOM, ZMODUL01, ZMODUL02, RANKNULL, ZMODUL03, GAUSSINT, MOD_2, ZMODUL04, ZMODUL05; constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, FUNCT_4, VECTSP_6, VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL04, ZMODUL05, INT_2, ZMODUL01, ZMODUL02, MATRLIN, MOD_2, INT_3, RANKNULL; registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, STRUCT_0, RLVECT_1, CARD_1, INT_1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_3, RELAT_1, ZMODUL02, GAUSSINT, FUNCT_4, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL05, VECTSP_4, VECTSP_7, VECTSP10, VECTSP_1, MEMBERED; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: 1. Torsion $\mathbb{Z}$-module and torsion-free $\mathbb{Z}$-module theorem :: ZMODUL06:1 for R being commutative Ring for V being LeftMod of R, W being Subspace of V holds (1.R) (*) W = (Omega).W; theorem :: ZMODUL06:2 for R being Ring for V being LeftMod of R, W1, W2, W3 being Subspace of V holds W1 /\ W2 is Subspace of (W1 + W3) /\ W2; theorem :: ZMODUL06:3 for R being Ring for V being LeftMod of R, W1, W2, W3 being Subspace of V st W1 /\ W2 <> (0).V holds (W1 + W3) /\ W2 <> (0).V; theorem :: ZMODUL06:4 for V being Z_Module, I, I1 being linearly-independent Subset of V st I1 c= I holds Lin(I \ I1) /\ Lin(I1) = (0).V; reserve V for Z_Module; reserve W for Subspace of V; reserve v, u for Vector of V; reserve i for Element of INT.Ring; definition let R be Ring; let V be LeftMod of R, 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; registration let V be Z_Module; cluster 0.V -> torsion; end; theorem :: ZMODUL06:5 v is torsion & u is torsion implies v + u is torsion; theorem :: ZMODUL06:6 v is torsion implies -v is torsion; theorem :: ZMODUL06:7 v is torsion & u is torsion implies v - u is torsion; theorem :: ZMODUL06:8 v is torsion implies i * v is torsion; theorem :: ZMODUL06:9 for v being Vector of V, w being Vector of W st v = w holds v is torsion iff w is torsion; registration let V be Z_Module; cluster torsion for Vector of V; end; theorem :: ZMODUL06:10 v is non torsion implies -v is non torsion; theorem :: ZMODUL06:11 v is non torsion & i <> 0 implies i * v is non torsion; theorem :: ZMODUL06:12 v is non torsion iff {v} is linearly-independent; definition let V be Z_Module; attr V is torsion means :: ZMODUL06:def 2 for v being Vector of V holds v is torsion; end; registration let V be Z_Module; cluster (0).V -> torsion; end; registration cluster torsion for Z_Module; end; theorem :: ZMODUL06:13 for v be Element of INT.Ring,v1 be Integer st v = v1 holds for n be Nat holds (Nat-mult-left(INT.Ring)).(n,v) = n*v1; theorem :: ZMODUL06:14 for x be Element of INT.Ring, v be Element of INT.Ring, v1 be Integer st v = v1 holds (Int-mult-left INT.Ring).(x,v) = x*v1; registration cluster non torsion for Z_Module; end; registration let V be non torsion Z_Module; cluster non torsion for Vector of V; end; definition let V be Z_Module; attr V is torsion-free means :: ZMODUL06:def 3 for v being Vector of V st v <> 0.V holds v is non torsion; end; theorem :: ZMODUL06:15 V is Mult-cancelable iff V is torsion-free; registration cluster -> torsion-free for Mult-cancelable Z_Module; end; registration cluster -> Mult-cancelable for torsion-free Z_Module; end; registration cluster -> torsion-free for free Z_Module; end; registration cluster torsion-free free for Z_Module; end; theorem :: ZMODUL06:16 for V being torsion-free Z_Module, v being Vector of V holds v is torsion iff v = 0.V; registration let V be torsion-free Z_Module; cluster -> torsion-free for Subspace of V; end; registration let R be Ring; let V be LeftMod of R; cluster (0).V -> trivial; end; registration cluster -> non torsion for non trivial torsion-free Z_Module; end; registration let R be Ring; cluster trivial for LeftMod of R; end; registration let K be Abelian add-associative right_zeroed right_complementable associative left_unital distributive non degenerated non empty doubleLoopStr; cluster Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital strict for non trivial ModuleStr over K; end; registration let R be non degenerated non empty Ring; let V be non trivial LeftMod of R; cluster non zero for Vector of V; end; theorem :: ZMODUL06:17 v is non torsion iff Lin{v} is free & v <> 0.V; registration let V be non torsion Z_Module; let v be non torsion Vector of V; cluster Lin{v} -> free; end; theorem :: ZMODUL06:18 for V being Z_Module, A being Subset of V, v being Vector of V st A is linearly-independent & v in A holds v is non torsion; theorem :: ZMODUL06:19 for u being object holds u in Lin{v} implies ex i being Element of INT.Ring st u = i*v; theorem :: ZMODUL06:20 v in Lin{v}; theorem :: ZMODUL06:21 i*v in Lin{v}; theorem :: ZMODUL06:22 for R being Ring for V being LeftMod of R holds Lin{0.V} = (0).V; registration let V be torsion-free Z_Module; let v be Vector of V; cluster Lin{v} -> free; end; theorem :: ZMODUL06:23 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; theorem :: ZMODUL06:24 for V being Z_Module, W being free Subspace of V, I being Subset of V, v being Vector of V st I is linearly-independent & Lin(I) = (Omega).W & v in I holds (Omega).W = Lin(I \ {v}) + Lin{v} & Lin(I \ {v}) /\ Lin{v} = (0).V & Lin(I \ {v}) is free & Lin{v} is free & v <> 0.V; theorem :: ZMODUL06:25 for V being Z_Module, W being free Subspace of V holds ex A being Subset of V st A is Subset of W & A is linearly-independent & Lin(A) = (Omega).W; theorem :: ZMODUL06:26 for V being Z_Module, W being finite-rank free Subspace of V holds 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); theorem :: ZMODUL06:27 for V being torsion-free Z_Module, v1, v2 being Vector of V st v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V ex u being Vector of V st u <> 0.V & Lin{v1} /\ Lin{v2} = Lin{u}; theorem :: ZMODUL06:28 for V being torsion-free Z_Module, v1, v2 being Vector of V st v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V ex u being Vector of V st u <> 0.V & Lin{v1} + Lin{v2} = Lin{u}; theorem :: ZMODUL06:29 for V being torsion-free Z_Module, W being finite-rank free Subspace of V, v, u being Vector of V st v <> 0.V & u <> 0.V & W /\ Lin{v} = (0).V & (W + Lin{u}) /\ Lin{v} <> (0).V & Lin{u} /\ Lin{v} = (0).V holds ex w1, w2 being Vector of V st w1 <> 0.V & w2 <> 0.V & (W + Lin{u}) + Lin{v} = (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 Lin{u} + Lin{v} & w2 in Lin{u} + Lin{v}; theorem :: ZMODUL06:30 for V being torsion-free Z_Module, W being finite-rank free Subspace of V, v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V holds W + Lin{v} is free; registration let V be torsion-free Z_Module; let v be Vector of V; let W be finite-rank free Subspace of V; cluster W + Lin{v} -> free; end; registration let V be Z_Module; let v be Vector of V; let W be finitely-generated Subspace of V; cluster W + Lin{v} -> finitely-generated; end; registration let V be Z_Module; let W1, W2 be finitely-generated Subspace of V; cluster W1 + W2 -> finitely-generated; end; theorem :: ZMODUL06:31 for R being Ring for V being LeftMod of R, W being Subspace of V, W1s, W2s being Subspace of W, W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds W1s + W2s = W1 + W2; registration let V be torsion-free Z_Module; let U1, U2 be finite-rank free Subspace of V; cluster U1 + U2 -> free; end; registration cluster -> free for finitely-generated torsion-free Z_Module; end; begin :: 2. Rank of finite-rank free $\mathbb{Z}$-module theorem :: ZMODUL06:32 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V st W1 /\ W2 = (0).V holds rank(W1 + W2) = rank W1 + rank W2; theorem :: ZMODUL06:33 for V being finite-rank free Z_Module, W1, W2 being finite-rank free Subspace of V st V is_the_direct_sum_of W1,W2 holds rank V = rank W1 + rank W2; theorem :: ZMODUL06:34 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V holds rank(W1 /\ W2) <= rank(W1); theorem :: ZMODUL06:35 for V being torsion-free Z_Module, v being Vector of V st v <> 0.V holds rank(Lin{v}) = 1; theorem :: ZMODUL06:36 for V being Z_Module holds rank((0).V) = 0; theorem :: ZMODUL06:37 for V being torsion-free Z_Module, v, u being Vector of V st v <> 0.V & u <> 0.V & Lin{v} /\ Lin{u} <> (0).V holds rank(Lin{v} + Lin{u}) = 1; theorem :: ZMODUL06:38 for V being torsion-free Z_Module, W being finite-rank free Subspace of V, v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V holds rank(W + Lin{v}) = rank(W); theorem :: ZMODUL06:39 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, v being Vector of V st W1 /\ Lin{v} <> (0).V & W2 /\ Lin{v} <> (0).V holds (W1 /\ W2) /\ Lin{v} <> (0).V; theorem :: ZMODUL06:40 for R being Ring for V, W being LeftMod of R, T be linear-transformation of V,W, A being Subset of V holds T.:(the carrier of Lin(A)) c= the carrier of Lin(T.: A); theorem :: ZMODUL06:41 for R being Ring for X, Y be LeftMod of R, L be linear-transformation of X, Y holds L.(0.X) = 0.Y; theorem :: ZMODUL06:42 for R being Ring for X, Y be LeftMod of R, L be linear-transformation of X, Y st L is bijective holds ex K be linear-transformation of Y, X st K = L" & K is bijective; theorem :: ZMODUL06:43 for R being Ring for X, Y be LeftMod of R, l be Linear_Combination of X, L be linear-transformation of X, Y st L is bijective holds L@*l = l*L"; theorem :: ZMODUL06:44 for R being Ring for X, Y be LeftMod of R, X0 be Subset of X, L be linear-transformation of X, Y, l be Linear_Combination of L.:X0 st X0 = the carrier of X & L is one-to-one holds L#l = l*L; theorem :: ZMODUL06:45 for R being Ring for X, Y be LeftMod of R, A be Subset of X, L be linear-transformation of X, Y st L is bijective holds A is linearly-independent iff L.:A is linearly-independent; theorem :: ZMODUL06:46 for R being Ring for X, Y be LeftMod of R, A be Subset of X, T be linear-transformation of X, Y st T is bijective holds T.:(the carrier of Lin(A)) = the carrier of Lin(T.: A); theorem :: ZMODUL06:47 for R being Ring for Y be LeftMod of R, A be Subset of Y holds Lin(A) is strict Subspace of (Omega).Y; theorem :: ZMODUL06:48 for R being Ring for X, Y be LeftMod of R, T be linear-transformation of X, Y st T is bijective holds X is free iff Y is free; theorem :: ZMODUL06:49 for X, Y be free Z_Module, T be linear-transformation of X, Y, A be Subset of X st T is bijective holds A is Basis of X iff T.: A is Basis of Y; theorem :: ZMODUL06:50 for X, Y be free Z_Module, T be linear-transformation of X, Y st T is bijective holds X is finite-rank iff Y is finite-rank; theorem :: ZMODUL06:51 for X, Y be finite-rank free Z_Module, T be linear-transformation of X, Y st T is bijective holds rank(X) = rank(Y); theorem :: ZMODUL06:52 for V being Z_Module, W being finite-rank free Subspace of V, a being Element of INT.Ring st a <> 0.INT.Ring holds rank(a (*) W) = rank(W); theorem :: ZMODUL06:53 for V being Z_Module, W1, W2, W3 being finite-rank free Subspace of V, a being Element of INT.Ring st a <> 0.INT.Ring & W3 = a (*) W1 holds rank(W3 /\ W2) = rank(W1 /\ W2); theorem :: ZMODUL06:54 for V being torsion-free Z_Module, W1, W2, W3 being finite-rank free Subspace of V, a being Element of INT.Ring st a <> 0.INT.Ring & W3 = a (*) W1 holds rank(W3 + W2) = rank(W1 + W2); theorem :: ZMODUL06:55 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, I being Basis of W1 st (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V) holds rank(W1 /\ W2) = rank(W1); theorem :: ZMODUL06:56 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, I being Basis of W1 st rank(W1 /\ W2) < rank(W1) holds ex v being Vector of V st v in I & (W1 /\ W2) /\ Lin{v} = (0).V; theorem :: ZMODUL06:57 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, 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) /\ Lin{v} <> (0).V); theorem :: ZMODUL06:58 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, I being Basis of W1 st (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V) holds rank(W1 + W2) = rank(W2); theorem :: ZMODUL06:59 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V st rank(W1 /\ W2) = rank(W1) holds rank(W1 + W2) = rank(W2); theorem :: ZMODUL06:60 for G be Field, V be VectSp of G, A being Subset of V st A is linearly-independent holds A is Basis of Lin(A); theorem :: ZMODUL06:61 for V being Mult-cancelable finite-rank free Z_Module, W1, W2 be finite-rank free Subspace of V holds rank(W1 + W2) + rank(W1 /\ W2) = rank(W1) + rank(W2); theorem :: ZMODUL06:62 for V being torsion-free Z_Module, W1, W2 be finite-rank free Subspace of V holds rank(W1 + W2) + rank(W1 /\ W2) = rank(W1) + rank(W2); theorem :: ZMODUL06:63 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V st rank(W1 + W2) = rank(W2) holds rank(W1 /\ W2) = rank(W1); theorem :: ZMODUL06:64 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, v being Vector of V st v <> 0.V & W1 /\ Lin{v} = (0).V & (W1 + W2) /\ Lin{v} = (0).V holds rank((W1 + Lin{v}) /\ W2) = rank(W1 /\ W2); theorem :: ZMODUL06:65 for V being torsion-free Z_Module, W being finite-rank free Subspace of V, v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V holds rank(W /\ Lin{v}) = 1; theorem :: ZMODUL06:66 for V being torsion-free Z_Module, W being finite-rank free Subspace of V, v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V holds ex u being Vector of V st u <> 0.V & W /\ Lin{v} = Lin{u}; theorem :: ZMODUL06:67 for V being torsion-free Z_Module, W being finite-rank free Subspace of V, u, v being Vector of V st W /\ Lin{v} = (0).V & (W + Lin{u}) /\ Lin{v} <> (0).V holds W /\ Lin{u} = (0).V; theorem :: ZMODUL06:68 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, v being Vector of V st rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V holds W2 /\ Lin{v} <> (0).V; theorem :: ZMODUL06:69 for V being torsion-free Z_Module, W1, W2, W3 being finite-rank free Subspace of V st rank(W1 + W2) = rank(W2) & W3 is Subspace of W1 holds rank(W3 + W2) = rank(W2); theorem :: ZMODUL06:70 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V, 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) /\ Lin{v} <> (0).V) ; theorem :: ZMODUL06:71 for V being torsion-free Z_Module, W1, W2 being finite-rank free Subspace of V st rank(W1 /\ W2) = rank(W1) holds ex a being Element of INT.Ring st a (*) W1 is Subspace of W2;