:: Rank of Submodule, Linear Transformations and Linearly Independent Subsets of $\mathbb Z$-module
:: by Kazuhisa Nakasho , Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received July 10, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

registration

let V be LeftMod of INT.Ring ;
let A be finite Subset of V;

cluster Lin A -> finitely-generated ;

correctness
coherence
Lin A is finitely-generated ;

proof end;

end;

theorem RL5Th33: :: ZMODUL05:1

for V being free finite-rank Z_Module holds
( rank V = 0 iff (Omega). V = (0). V )

proof end;

registration

let V be free finite-rank Z_Module;

cluster finite base for Element of K10( the carrier of V);

existence
ex b₁ being Basis of V st b₁ is finite

proof end;

end;

registration

let V be free finite-rank Z_Module;

cluster base -> finite for Element of K10( the carrier of V);

correctness
coherence
for b₁ being Basis of V holds b₁ is finite ;
;

end;

theorem RL5Th29: :: ZMODUL05:2

for V being free finite-rank Z_Module
for W being Submodule of V holds rank W <= rank V

proof end;

theorem RL5Th30: :: ZMODUL05:3

for V being Z_Module
for A being finite linearly-independent Subset of V holds card A = rank (Lin A)

proof end;

theorem :: ZMODUL05:4

for V being free finite-rank Z_Module holds rank V = rank ((Omega). V)

proof end;

theorem :: ZMODUL05:5

for V being free finite-rank Z_Module holds
( rank V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )

proof end;

theorem :: ZMODUL05:6

for V being free finite-rank Z_Module holds
( rank V = 2 iff ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

proof end;

RL5Lm2: for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat st n <= rank V holds
ex W being strict free Submodule of V st rank W = n

proof end;

theorem :: ZMODUL05:7

for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat holds
( n <= rank V iff ex W being strict free Submodule of V st rank W = n ) by RL5Lm2, RL5Th29;

definition

let V be free finite-rank Z_Module;
let n be Nat;

func n Submodules_of V -> set means :RL5Def4: :: ZMODUL05:def 1
for x being object holds
( x in it iff ex W being strict free Submodule of V st
( W = x & rank W = n ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex W being strict free Submodule of V st
( W = x & rank W = n ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) ) & ( for x being object holds
( x in b₂ iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem RL5Def4 defines Submodules_of ZMODUL05:def 1 :
for V being free finite-rank Z_Module
for n being Nat
for b₃ being set holds
( b₃ = n Submodules_of V iff for x being object holds
( x in b₃ iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) );

theorem :: ZMODUL05:8

for V being free finite-rank Z_Module
for n being Nat st n <= rank V holds
not n Submodules_of V is empty

proof end;

theorem :: ZMODUL05:9

for V being free finite-rank Z_Module
for n being Nat st rank V < n holds
n Submodules_of V = {}

proof end;

theorem :: ZMODUL05:10

for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat holds n Submodules_of W c= n Submodules_of V

proof end;

theorem :: ZMODUL05:11

for F, G being FinSequence of INT
for v being Integer st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v

proof end;

theorem RLVECT142: :: ZMODUL05:12

for F, G being FinSequence of INT st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G

proof end;

definition

let T be finite Subset of the carrier of INT.Ring;

::: what for? defined for reals, then redefine

func Sum T -> Element of INT.Ring means :: ZMODUL05:def 2
ex F being FinSequence of INT st
( rng F = T & F is one-to-one & it = Sum F );

existence
ex b₁ being Element of INT.Ring ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b₁ = Sum F )

proof end;

uniqueness
for b₁, b₂ being Element of INT.Ring st ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b₁ = Sum F ) & ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b₂ = Sum F ) holds
b₁ = b₂ by RLVECT142;

end;

:: deftheorem defines Sum ZMODUL05:def 2 :
for T being finite Subset of the carrier of INT.Ring
for b₂ being Element of INT.Ring holds
( b₂ = Sum T iff ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b₂ = Sum F ) );

theorem RF9: :: ZMODUL05:13

for K being Ring
for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds
Sum R1 = Sum R2

proof end;

theorem :: ZMODUL05:14

canceled;

theorem :: ZMODUL05:15

canceled;

::$CT 2
::theorem
::: for X be finite Subset of INT st X = {}
::: holds Sum X = 0 by Def2,GR_CY_1:3,RELAT_1:38;
::theorem
:: for v be Element of INT holds Sum {v} = v
:: proof
:: let v be Element of INT;
:: A1: Sum <*v*> = v by RVSUM_1:73;
:: rng <*v*> = {v} & <*v*> is one-to-one by FINSEQ_1:39;
:: hence Sum {v} = v by A1,Def2;
:: end;
::theorem
:: for S, T being finite Subset of INT
:: st T misses S holds
:: Sum (T \/ S) = (Sum T) + (Sum S)
:: proof
:: let S, T be finite Subset of INT;
:: consider F being FinSequence of INT such that
:: A1: rng F = T \/ S and
:: A2: F is one-to-one & Sum (T \/ S) = Sum F by Def2;
:: consider G being FinSequence of INT such that
:: A3: rng G = T and
:: A4: G is one-to-one and
:: A5: Sum T = Sum G by Def2;
:: consider H being FinSequence of INT such that
:: A6: rng H = S and
:: A7: H is one-to-one and
:: A8: Sum S = Sum H by Def2;
:: set I = G ^ H;
:: reconsider G0 = G, H0 = H as real-valued FinSequence;
::: A9: Sum (G0 ^ H0) = Sum (G) + Sum (H) by RVSUM_1:75;
:: assume T misses S; then
:: A10: G ^ H is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
:: rng (G ^ H) = rng F by A1,A3,A6,FINSEQ_1:31;
:: hence Sum (T \/ S) = (Sum T) + (Sum S) by A2,A5,A8,A9,A10,RLVECT142;
:: end;

definition

end;

:: deftheorem ZMODUL05:def 3 :
canceled;

:: deftheorem ZMODUL05:def 4 :
canceled;

:: deftheorem ZMODUL05:def 5 :
canceled;

theorem MATRLIN16: :: ZMODUL05:16

for R being Ring
for V1, V2 being LeftMod of R
for f being Function of V1,V2
for p being FinSequence of V1 st f is additive & f is homogeneous holds
f . (Sum p) = Sum (f * p)

proof end;

theorem :: ZMODUL05:17

for V being free Z_Module st [#] V is finite holds
(Omega). V = (0). V

proof end;

theorem :: ZMODUL05:18

for F being Ring
for V, W being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y) by RANKNULL:8;

theorem :: ZMODUL05:19

for V, W being Z_Module
for T being linear-transformation of V,W holds T . (0. V) = 0. W by RANKNULL:9;

theorem :: ZMODUL05:20

for V, W being Z_Module
for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W ) by RANKNULL:10;

theorem :: ZMODUL05:21

for V, W being Z_Module
for T being linear-transformation of V,W holds 0. V in ker T by RANKNULL:11;

theorem :: ZMODUL05:22

for V, W being Z_Module
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T) by RANKNULL:12;

theorem :: ZMODUL05:23

for V, W being Z_Module
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x ) by RANKNULL:13;

theorem :: ZMODUL05:24

for V, W being Z_Module
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W by RANKNULL:14;

theorem :: ZMODUL05:25

for V, W being Z_Module
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V by RANKNULL:15;

theorem :: ZMODUL05:26

for V being free finite-rank Z_Module holds rank ((0). V) = 0

proof end;

theorem Th17: :: ZMODUL05:27

for V, W being Z_Module
for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T by RANKNULL:17;

theorem Th18: :: ZMODUL05:28

for V being Z_Module
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y}) by RANKNULL:18;

:: combinations

theorem :: ZMODUL05:29

for V, W being Z_Module
for X being Subset of V st V is Submodule of W holds
X is Subset of W

proof end;

theorem ThLin4: :: ZMODUL05:30

for R being Ring
for V being LeftMod of R
for A being Subset of V holds A is Subset of (Lin A)

proof end;

theorem ThLin7: :: ZMODUL05:31

for V being LeftMod of INT.Ring
for A being linearly-independent Subset of V holds A is Basis of (Lin A)

proof end;

:: Adjoining an element x to A that is already in its linear span
:: results in a linearly dependent set.

theorem Th21: :: ZMODUL05:32

for V being free finite-rank Z_Module
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent

proof end;

registration

let V be free finite-rank Z_Module;
let W be Z_Module;
let T be linear-transformation of V,W;

cluster ker T -> free finite-rank ;

correctness
coherence
( ker T is finite-rank & ker T is free );
;

end;

theorem Th22: :: ZMODUL05:33

for W being Z_Module
for V being free finite-rank Z_Module
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one

proof end;

theorem :: ZMODUL05:34

for R being Ring
for V being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

proof end;

registration

let R be non degenerated Ring;
let V be LeftMod of R;

cluster linearly-dependent for Element of K10( the carrier of V);

existence
ex b₁ being Subset of V st b₁ is linearly-dependent

proof end;

end;

:: Restricting a linear combination to a given set

definition

let R be Ring;
let V be LeftMod of R;
let l be Linear_Combination of V;
let A be Subset of V;

func l ! A -> Linear_Combination of A equals :: ZMODUL05:def 6
(l | A) +* ((A `) --> (0. R));

coherence
(l | A) +* ((A `) --> (0. R)) is Linear_Combination of A

proof end;

end;

:: deftheorem defines ! ZMODUL05:def 6 :
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((A `) --> (0. R));

theorem Th24: :: ZMODUL05:35

for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V holds l = l ! (Carrier l)

proof end;

Lm1: for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite

proof end;

theorem Th25: :: ZMODUL05:36

for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v

proof end;

theorem Th26: :: ZMODUL05:37

for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. R

proof end;

theorem Th27: :: ZMODUL05:38

for R being Ring
for V being LeftMod of R
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))

proof end;

registration

let R be Ring;
let V be LeftMod of R;
let l be Linear_Combination of V;
let X be Subset of V;

cluster l .: X -> finite ;

coherence
l .: X is finite by Lm1;

end;

theorem Th28: :: ZMODUL05:39

for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. R)}

proof end;

definition

let K be Ring;
let V, W be VectSp of K;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;
let w be Element of W;

func lCFST (l,T,w) -> the carrier of K -valued FinSequence equals :: ZMODUL05:def 7
l * (canFS ((T " {w}) /\ (Carrier l)));

correctness
coherence
l * (canFS ((T " {w}) /\ (Carrier l))) is the carrier of K -valued FinSequence;

proof end;

end;

:: deftheorem defines lCFST ZMODUL05:def 7 :
for K being Ring
for V, W being VectSp of K
for l being Linear_Combination of V
for T being linear-transformation of V,W
for w being Element of W holds lCFST (l,T,w) = l * (canFS ((T " {w}) /\ (Carrier l)));

theorem ThTF3C0: :: ZMODUL05:40

for V, W being non empty set
for f being FinSequence
for l being Function of V,W st rng f c= V holds
( l * f is W -valued & l * f is FinSequence-like )

proof end;

registration

let V, W be non empty set ;
let f be V -valued FinSequence;
let l be Function of V,W;

cluster f (#) l -> W -valued FinSequence-like ;

coherence
( l * f is W -valued & l * f is FinSequence-like )

proof end;

end;

ThTF3C1: for V, W being non empty set
for A being finite Subset of V
for l being Function of V,W holds
( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

proof end;

registration

let V, W be non empty set ;
let A be finite Subset of V;
let l be Function of V,W;

cluster (canFS A) (#) l -> W -valued FinSequence-like ;

coherence
( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like ) by ThTF3C1;

end;

registration

let R be Ring;
let V be LeftMod of R;
let A be finite Subset of V;
let l be Linear_Combination of V;

cluster (canFS A) (#) l -> the carrier of R -valued FinSequence-like ;

coherence
( l * (canFS A) is the carrier of R -valued & l * (canFS A) is FinSequence-like ) ;

end;

theorem ThTF3C3: :: ZMODUL05:41

for V, W being non empty set
for f, g being b₁ -valued FinSequence
for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)

proof end;

theorem ThTF3C2: :: ZMODUL05:42

for R being Ring
for V being LeftMod of R
for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)

proof end;

theorem ThTF3C3: :: ZMODUL05:43

for R being Ring
for V being LeftMod of R
for A being finite Subset of V
for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds
Sum (l * (canFS A)) = Sum (l0 * (canFS A))

proof end;

definition

let R be Ring;
let V, W be LeftMod of R;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;

func T @* l -> Linear_Combination of W means :LDef5: :: ZMODUL05:def 8
( Carrier it c= T .: (Carrier l) & ( for w being Element of W holds it . w = Sum (lCFST (l,T,w)) ) );

existence
ex b₁ being Linear_Combination of W st
( Carrier b₁ c= T .: (Carrier l) & ( for w being Element of W holds b₁ . w = Sum (lCFST (l,T,w)) ) )

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of W st Carrier b₁ c= T .: (Carrier l) & ( for w being Element of W holds b₁ . w = Sum (lCFST (l,T,w)) ) & Carrier b₂ c= T .: (Carrier l) & ( for w being Element of W holds b₂ . w = Sum (lCFST (l,T,w)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem LDef5 defines @* ZMODUL05:def 8 :
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for b₆ being Linear_Combination of W holds
( b₆ = T @* l iff ( Carrier b₆ c= T .: (Carrier l) & ( for w being Element of W holds b₆ . w = Sum (lCFST (l,T,w)) ) ) );

theorem LTh29: :: ZMODUL05:44

for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

proof end;

theorem ThTF3B2: :: ZMODUL05:45

for K being Ring
for V, W being LeftMod of K
for T being linear-transformation of V,W
for s being Vector of W
for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s

proof end;

theorem :: ZMODUL05:46

for K being Ring
for V, W being LeftMod of K
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl

proof end;

::: same as ZMODUL04:25

theorem Th31: :: ZMODUL05:47

for R being Ring
for V being LeftMod of R
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)

proof end;

theorem Th32: :: ZMODUL05:48

for R being Ring
for V being LeftMod of R
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)

proof end;

theorem :: ZMODUL05:49

for R being Ring
for V being LeftMod of R
for A being Subset of V
for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds
Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

proof end;

theorem :: ZMODUL05:50

for V being free Z_Module
for A, B being Subset of V st A c= B & B is Basis of V holds
V is_the_direct_sum_of Lin A, Lin (B \ A)

proof end;

theorem :: ZMODUL05:51

for R being Ring
for V, W being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )

proof end;

theorem :: ZMODUL05:52

for R being Ring
for V being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. R)}

proof end;

theorem Th36: :: ZMODUL05:53

for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l

proof end;

theorem Th37: :: ZMODUL05:54

for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @* l) . (T . v) = l . v

proof end;

theorem Th38: :: ZMODUL05:55

for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @* l) (#) (T * G)

proof end;

theorem Th39: :: ZMODUL05:56

for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @* l)

proof end;

theorem :: ZMODUL05:57

for W being Z_Module
for V being free finite-rank Z_Module
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @* l)

proof end;

theorem :: ZMODUL05:58

for V being Z_Module
for X being Subset of V st X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) ;

:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.

definition

let R be Ring;
let V, W be LeftMod of R;
let X be Subset of V;
let T be linear-transformation of V,W;
let l be Linear_Combination of T .: X;
assume A1: T | X is one-to-one ;

func T # l -> Linear_Combination of X equals :Def6: :: ZMODUL05:def 9
(l * T) +* ((X `) --> (0. R));

coherence
(l * T) +* ((X `) --> (0. R)) is Linear_Combination of X

proof end;

end;

:: deftheorem Def6 defines # ZMODUL05:def 9 :
for R being Ring
for V, W being LeftMod of R
for X being Subset of V
for T being linear-transformation of V,W
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T # l = (l * T) +* ((X `) --> (0. R));

theorem Th42: :: ZMODUL05:59

for R being Ring
for V, W being LeftMod of R
for X being Subset of V
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)

proof end;

:: # is a right inverse of @*

theorem :: ZMODUL05:60

for R being Ring
for V, W being LeftMod of R
for X being Subset of V
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @* (T # l) = l

proof end;