:: Free $\mathbb Z$-module
::  by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012-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 NUMBERS, FINSEQ_1, SUBSET_1, STRUCT_0, FUNCT_1, XBOOLE_0,
      ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4, PRELAMB,
      CLASSES1, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2,
      FINSET_1, VALUED_1, RLSUB_1, ZFMISC_1, INT_1, ORDINAL1, RLVECT_2,
      ZMODUL01, ZMODUL03, ORDERS_1, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2,
      INT_3, VECTSP_1, NEWTON, MONOID_0, VECTSP10, EC_PF_1, ZMODUL02, RLVECT_5,
      INT_2, MESFUNC1, MOD_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1, FINSET_1, ORDERS_1,
      CARD_1, CLASSES1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_1, FINSEQ_1,
      FINSEQ_3, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1,
      VECTSP_2, VECTSP_4, INT_2, VECTSP_6, VECTSP_9, MATRLIN, INT_3, BINOM,
      EC_PF_1, VECTSP_7, VECTSP10, ZMODUL01, ZMODUL02;
 constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, VECTSP_2,
      RLVECT_2, REAL_1, CLASSES1, FUNCT_7, NAT_D, GR_CY_1, EUCLID, VECTSP_6,
      VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL01, ZMODUL02, BINOP_1, VECTSP_7,
      VECTSP_4, NEWTON;
 registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
      XREAL_0, STRUCT_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, XXREAL_0,
      NAT_1, INT_3, RELAT_1, ALGSTR_1, ZMODUL02, ORDINAL1, VECTSP_7;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Free Z-module

 reserve x, y, y1, y2 for set;
 reserve V for Z_Module;
 reserve u, v, w for Vector of V;
 reserve F, G, H, I for FinSequence of V;
 reserve W, W1, W2, W3 for Submodule of V;

registration
  cluster non trivial for Z_Module;
end;

registration
  let V be Z_Module;
  cluster linearly-independent for finite Subset of V;
end;

theorem :: ZMODUL03:1
  for u being Vector of V holds
  ex l being Linear_Combination of V st l.u = 1 &
  for v being Vector of V st v <> u holds l.v = 0;

theorem :: ZMODUL03:2
  for G be Z_Module, i being Element of INT.Ring,
  w be Element of INT, v be Element of G
  st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring,
    the ZeroF of INT.Ring, Int-mult-left(INT.Ring) #) & v = w
  holds i*v = i*w;

definition
::$CD
::  let IT be Z_Module;
::  attr IT is free means  :Def1:
::  ex A being Subset of IT
::  st A is linearly-independent & Lin(A) = the ModuleStr of IT;
end;

registration let V;
  cluster (0).V -> free;
end;

registration
  cluster strict free for Z_Module;
end;

registration
  let V be Z_Module;
  cluster strict free for Submodule of V;
end;

registration
  let V be free Z_Module;
  cluster base for Subset of V;
end;

definition
  let V be free Z_Module;
  mode Basis of V is base Subset of V;
::$CD
end;

registration
  cluster -> Mult-cancelable for free Z_Module;
end;

registration
  cluster free for non trivial Z_Module;
end;

 reserve KL1, KL2 for Linear_Combination of V;
 reserve X for Subset of V;

theorem :: ZMODUL03:3
  X is linearly-independent & Carrier(KL1) c= X & Carrier(KL2) c= X
  & Sum(KL1) = Sum(KL2) implies KL1 = KL2;

theorem :: ZMODUL03:4
  for V being free Z_Module, A being Subset of V st A is linearly-independent
  ex B being Subset of V st A c= B & B is linearly-independent &
  (for v being Vector of V holds ex a being Element of INT.Ring st
    a * v in Lin(B));

theorem :: ZMODUL03:5
  for L being Linear_Combination of V for F, G being FinSequence of V
  for P being Permutation of dom F st G = F*P holds
  Sum(L (#) F) = Sum(L (#) G);

theorem :: ZMODUL03:6
  for L being Linear_Combination of V for F being FinSequence of V st
  Carrier(L) misses rng F holds Sum(L (#) F) = 0.V;

theorem :: ZMODUL03:7
  for F being FinSequence of V st F is one-to-one
  for L being Linear_Combination of V st Carrier(L) c= rng F holds
  Sum(L (#) F) = Sum(L);

theorem :: ZMODUL03:8
  for L being Linear_Combination of V for F being FinSequence of V holds
  ex K being Linear_Combination of V st
  Carrier(K) = rng F /\ Carrier(L) & L (#) F = K (#) F;

theorem :: ZMODUL03:9
  for L being Linear_Combination of V for A being Subset of V
  for F being FinSequence of V st rng F c= the carrier of Lin(A) holds
  ex K being Linear_Combination of A st Sum(L (#) F) = Sum(K);

theorem :: ZMODUL03:10
  for L being Linear_Combination of V for A being Subset of V st
  Carrier(L) c= the carrier of Lin(A) holds
  ex K being Linear_Combination of A st Sum(L) = Sum(K);

theorem :: ZMODUL03:11
  for L being Linear_Combination of V st Carrier(L) c= the carrier
  of W for K being Linear_Combination of W st K = L|the carrier of W holds
  Carrier(L) = Carrier(K) & Sum(L) = Sum(K);

theorem :: ZMODUL03:12
  for K being Linear_Combination of W holds
  ex L being Linear_Combination of V st
  Carrier(K) = Carrier(L) & Sum(K) = Sum(L);

theorem :: ZMODUL03:13
  for L being Linear_Combination of V st
  Carrier(L) c= the carrier of W
  ex K being Linear_Combination of W
   st Carrier(K) = Carrier(L) & Sum(K) = Sum (L);

theorem :: ZMODUL03:14
  for V being free Z_Module for I being Basis of V, v being Vector of V
    holds v in Lin(I);

theorem :: ZMODUL03:15
  for A being Subset of W st A is linearly-independent holds
  A is linearly-independent Subset of V;

theorem :: ZMODUL03:16
  for A being Subset of V st A is linearly-independent &
  A c= the carrier of W holds A is linearly-independent Subset of W;

theorem :: ZMODUL03:17
  for V being Z_Module
  for A being Subset of V st A is linearly-independent
  for v being Vector of V st v in A for B being Subset of V st B = A \ {v}
  holds not v in Lin(B);

theorem :: ZMODUL03:18
  for V being free Z_Module for I being Basis of V
  for A being non empty Subset of V st A misses I
  for B being Subset of V st B = I \/ A holds B is linearly-dependent;

theorem :: ZMODUL03:19
  for A being Subset of V st A c= the carrier of W holds
  Lin(A) is Submodule of W;

theorem :: ZMODUL03:20
  for A being Subset of V, B being Subset of W st A = B holds Lin(A) = Lin(B);

registration
  let V be Z_Module, A be linearly-independent Subset of V;
  cluster Lin(A) -> free;
end;

registration
  let V be free Z_Module;
  cluster (Omega).V -> strict free;
end;

begin  :: Finite-rank free Z-module

definition
  let IT be free Z_Module;
  attr IT is finite-rank means
:: ZMODUL03:def 3
  ex A being finite Subset of IT st A is Basis of IT;
end;

registration let V;
  cluster (0).V -> finite-rank;
end;

registration
  cluster strict finite-rank for free Z_Module;
end;

registration
  let V be Z_Module;
  cluster strict finite-rank for free Submodule of V;
end;

registration
  let V be Z_Module, A be finite linearly-independent Subset of V;
  cluster Lin(A) -> finite-rank;
end;

definition
  let V be Z_Module;
  attr V is finitely-generated means
:: ZMODUL03:def 4
  ex A being finite Subset of V st Lin(A) = the ModuleStr of V;
end;

registration let V;
  cluster (0).V -> finitely-generated;
end;

registration
  cluster strict finitely-generated free for Z_Module;
end;

registration let V be finite-rank free Z_Module;
  cluster -> finite for Basis of V;
end;

begin :: Rank of a finite-rank free Z-module

theorem :: ZMODUL03:21
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Basis of V,
  u1, u2 being Vector of V
  st u1 <> u2 & u1 in I & u2 in I holds
  ZMtoMQV(V,p,u1) <> ZMtoMQV(V,p,u2);

theorem :: ZMODUL03:22
  for p being prime Element of INT.Ring, V being Z_Module,
  ZQ being VectSp of GF(p), vq being Vector of ZQ
  st ZQ = Z_MQ_VectSp(V,p)
  holds ex v being Vector of V st vq = ZMtoMQV(V,p,v);

theorem :: ZMODUL03:23
  for p being prime Element of INT.Ring, V being Z_Module,
  I being Subset of V,
  lq being Linear_Combination of Z_MQ_VectSp(V,p)
  holds ex l being Linear_Combination of I
  st for v being Vector of V st v in I holds
  ex w be Vector of V st w in I & w in ZMtoMQV(V,p,v)
  & l.w = lq.(ZMtoMQV(V,p,v));

theorem :: ZMODUL03:24
  for p being prime Element of INT.Ring, V being free Z_Module,
  I being Basis of V,
  lq being Linear_Combination of Z_MQ_VectSp(V,p)
  holds ex l being Linear_Combination of I
  st for v being Vector of V st v in I holds
  l.v = lq.(ZMtoMQV(V,p,v));

theorem :: ZMODUL03:25
  for p being prime Element of INT.Ring, V being free Z_Module,
  I being Basis of V,
  X be non empty Subset of Z_MQ_VectSp(V,p)
  st X = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
  ex F be Function of X, the carrier of V
  st (for u be Vector of V st u in I holds F.(ZMtoMQV(V,p,u)) = u)
  & F is one-to-one & dom F = X & rng F = I;

theorem :: ZMODUL03:26
  for p being prime Element of INT.Ring, V being free Z_Module,
      I being Basis of V holds
  card ( {ZMtoMQV(V,p,u) where u is Vector of V : u in I} )
  = card(I);

theorem :: ZMODUL03:27
  for p being prime Element of INT.Ring, V being free Z_Module holds
  ZMtoMQV(V,p,0. V) = 0.(Z_MQ_VectSp(V,p));

theorem :: ZMODUL03:28
  for p being prime Element of INT.Ring, V being free Z_Module,
  s,t be Element of V holds
  ZMtoMQV(V,p,s)+ZMtoMQV(V,p,t) = ZMtoMQV(V,p,s+t);

theorem :: ZMODUL03:29
  for p being prime Element of INT.Ring, V being free Z_Module,
  s be FinSequence of V,
  t be FinSequence of Z_MQ_VectSp(V,p)
  st len s = len t & for i be Element of NAT
  st i in dom s holds ex si be Vector of V
  st si = s.i & t.i = ZMtoMQV(V,p,si) holds
  Sum(t) = ZMtoMQV(V,p,Sum(s));

theorem :: ZMODUL03:30
  for p being prime Element of INT.Ring, V being free Z_Module,
  s be Element of V,
  a be Element of INT.Ring,
  b be Element of GF(p) st a = b holds
  b*ZMtoMQV(V,p,s) = ZMtoMQV(V,p,a*s);

theorem :: ZMODUL03:31
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Basis of V,
      l being Linear_Combination of I,
      IQ being Subset of Z_MQ_VectSp(V,p),
      lq being Linear_Combination of IQ
  st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} &
  (for v being Vector of V st v in I holds
  l.v = lq.(ZMtoMQV(V,p,v)) ) holds
  Sum(lq) = ZMtoMQV(V,p,Sum(l));

theorem :: ZMODUL03:32
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Basis of V,
      IQ being Subset of Z_MQ_VectSp(V,p)
  st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I}
  holds IQ is linearly-independent;

theorem :: ZMODUL03:33
  for p being prime Element of INT.Ring, V being free Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V,p)
  st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
  (for s be FinSequence of V
  st (for i be Element of NAT
  st i in dom s holds ex si be Vector of V
  st si=s.i & ZMtoMQV(V,p,si) in Lin(IQ))
  holds ZMtoMQV(V,p,Sum(s)) in Lin(IQ));

theorem :: ZMODUL03:34
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Basis of V,
  IQ being Subset of Z_MQ_VectSp(V,p),
  l be Linear_Combination of I
  st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
  ZMtoMQV(V,p,Sum(l)) in Lin(IQ);

theorem :: ZMODUL03:35
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Basis of V,
  IQ being Subset of Z_MQ_VectSp(V,p)
  st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
  IQ is Basis of Z_MQ_VectSp(V,p);

registration
  let p be prime Element of INT.Ring, V be finite-rank free Z_Module;
  cluster Z_MQ_VectSp(V,p) -> finite-dimensional;
end;

theorem :: ZMODUL03:36
  for V be finite-rank free Z_Module
  holds for A, B being Basis of V holds
  card A = card B;

definition
  let V be finite-rank free Z_Module;
  func rank(V) -> Nat means
:: ZMODUL03:def 5
  for I being Basis of V holds it = card I;
end;

theorem :: ZMODUL03:37
  for p be prime Element of INT.Ring, V be finite-rank free Z_Module holds
  rank V = dim Z_MQ_VectSp(V,p);