:: Divisible $\mathbb Z$-modules
::  by Yuichi Futa and Yasunari Shidama
::
:: Received December 30, 2015
:: Copyright (c) 2015-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, FUNCT_1, RAT_1,
      XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOP_2, RLSUB_2, EQREL_1,
      PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1,
      FUNCT_2, FINSET_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01,
      ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1, MSAFREE2, INT_3,
      COMPLEX1, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, VECTSP10, ZMODUL02,
      ZMODUL04, ZMODUL06, ZMODUL07, ZMODUL08;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1,
      CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, RAT_1, BINOP_2, REALSET1,
      EQREL_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4,
      VECTSP_5, VECTSP_6, VECTSP_7, INT_3, MOD_2, ZMODUL01, ZMODUL02, ZMODUL03,
      RANKNULL, GAUSSINT, ZMODUL04, ZMODUL05, ZMODUL06, ZMODUL07, VECTSP10;
 constructors BINOP_2, UPROOTS, ZMODUL01, REALSET1, ALGSTR_1, EC_PF_1,
      ZMODUL04, ZMODUL06, ZMODUL07, ZMODUL05, RELSET_1, ZMODUL02, VECTSP10;
 registrations SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0,
      STRUCT_0, RLVECT_1, MEMBERED, CARD_1, INT_1, XBOOLE_0, ORDINAL1,
      XXREAL_0, NAT_1, INT_3, REALSET1, RELAT_1, GAUSSINT, VECTSP_7, EQREL_1,
      RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL06, ZMODUL07;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Divisible Module

definition
  let V be Z_Module, v be Vector of V;
  attr v is divisible means
:: ZMODUL08:def 1

  for a being Element of INT.Ring st a <> 0.INT.Ring holds
  ex u being Vector of V st a*u = v;
end;

registration
  let V be Z_Module;
  cluster 0.V -> divisible;
end;

registration
  let V be Z_Module;
  cluster divisible for Vector of V;
end;

theorem :: ZMODUL08:1
  for V being Z_Module, v, u being divisible Vector of V holds
  v + u is divisible;

theorem :: ZMODUL08:2
  for V being Z_Module, v being divisible Vector of V holds
  - v is divisible;

theorem :: ZMODUL08:3
  for V being Z_Module, v being divisible Vector of V,
      i being Element of INT.Ring holds
    i * v is divisible;

definition
  let V be Z_Module;
  attr V is divisible means
:: ZMODUL08:def 2

  for v being Vector of V holds v is divisible;
end;

registration
  let V be Z_Module;
  cluster (0).V -> divisible;
end;

registration
  cluster Rat-Module -> divisible;
end;

registration
  cluster divisible for Z_Module;
end;

registration
  let V be Z_Module;
  cluster divisible for Submodule of V;
end;

registration
  cluster non finitely-generated for divisible Z_Module;
end;

theorem :: ZMODUL08:4
  (Int-mult-left(F_Rat)) | [:INT, INT:] = Int-mult-left(INT.Ring);

theorem :: ZMODUL08:5
  ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring,
  the ZeroF of INT.Ring, Int-mult-left(INT.Ring) #)
  is Submodule of Rat-Module;

theorem :: ZMODUL08:6
  for V being divisible Z_Module, W be Submodule of V
  holds VectQuot(V, W) is divisible;

registration
  cluster non trivial for divisible Z_Module;
end;

theorem :: ZMODUL08:7
  for V being Z_Module holds
  V is divisible iff (Omega).V is divisible;

theorem :: ZMODUL08:8
  for V being Z_Module, v being Vector of V st v is non torsion holds
  Lin{v} is non divisible;

theorem :: ZMODUL08:9
  for V being Z_Module, v being Vector of V st v is torsion & v <> 0.V holds
  Lin{v} is non divisible;

registration
  let V be non trivial Z_Module, v be non zero Vector of V;
  cluster Lin{v} -> non divisible;
end;

registration
  let V be non trivial Z_Module;
  cluster non divisible for Submodule of V;
end;

theorem :: ZMODUL08:10
  for V being non trivial finitely-generated torsion-free Z_Module holds
  V is non divisible;

theorem :: ZMODUL08:11
  for V being non trivial finitely-generated torsion Z_Module holds
  ex i being Element of INT.Ring st i <> 0 & for v being Vector of V
  holds i * v = 0.V;

theorem :: ZMODUL08:12
  for V being non trivial finitely-generated torsion Z_Module,
  i being Element of INT.Ring st i <> 0 & for v being Vector of V
  holds i * v = 0.V
  holds V is non divisible;

theorem :: ZMODUL08:13
  for V being non trivial finitely-generated torsion Z_Module holds
  V is non divisible;

registration
  cluster non divisible for non trivial finitely-generated torsion Z_Module;
end;

theorem :: ZMODUL08:14
  for V being non trivial finitely-generated Z_Module holds V is non divisible;

registration
  cluster -> non finitely-generated for non trivial divisible Z_Module;
end;

registration
  let V be non trivial non divisible Z_Module;
  cluster non divisible for non zero Vector of V;
end;

registration
  let V be non trivial finite-rank free Z_Module;
  cluster rank V -> non zero;
end;

theorem :: ZMODUL08:15
  for V being non trivial free Z_Module, v being non zero Vector of V,
  I being Basis of V holds
  ex L being Linear_Combination of I, u being Vector of V
  st v = Sum(L) & u in I & L.u <> 0;

theorem :: ZMODUL08:16
  for V being non trivial free Z_Module, v being non zero Vector of V
  holds v is non divisible;

registration
  cluster -> non divisible for non trivial free Z_Module;
end;

theorem :: ZMODUL08:17
  for V being non trivial free Z_Module, v being non zero Vector of V
  holds ex a being Element of INT.Ring
  st a in NAT & for b being Element of INT.Ring,
  u being Vector of V st b > a holds v <> b*u;

theorem :: ZMODUL08:18
  for V being non trivial free Z_Module, v being non zero Vector of V
  holds ex a being Element of INT.Ring, u being Vector of V
  st a in NAT & a <> 0 & v = a*u &
  for b being Element of INT.Ring, w being Vector of V st b > a
  holds v <> b*w;

begin :: 2. Divisible module for torsion-free $\mathbb{Z}$-module

definition
  let V be torsion-free Z_Module;
  func EMbedding(V) -> strict Z_Module means
:: ZMODUL08:def 3

  the carrier of it = rng MorphsZQ(V) &
  the ZeroF of it = zeroCoset(V) &
  the addF of it = (addCoset(V)) || ( rng MorphsZQ(V) ) &
  the lmult of it = (lmultCoset(V)) | [:INT,rng MorphsZQ(V):];
end;

theorem :: ZMODUL08:19
  for V being torsion-free Z_Module holds
  (for x being Vector of EMbedding(V) holds x is Vector of Z_MQ_VectSp(V) ) &
  0.EMbedding(V) = 0.Z_MQ_VectSp(V) &
  (for x, y being Vector of EMbedding(V), v, w being Vector of Z_MQ_VectSp(V)
  st x = v & y = w holds x+y = v+w ) &
  for i being Element of INT.Ring, j being Element of F_Rat,
  x being Vector of EMbedding(V), v being Vector of Z_MQ_VectSp(V)
  st i = j & x = v holds i*x = j*v;

theorem :: ZMODUL08:20
  for V being torsion-free Z_Module holds
  (for v, w being Vector of Z_MQ_VectSp(V)
  st v in EMbedding(V) & w in EMbedding(V)
  holds v+w in EMbedding(V) ) &
  for j being Element of F_Rat, v being Vector of Z_MQ_VectSp(V)
  st j in INT & v in EMbedding(V)
  holds j*v in EMbedding(V);

theorem :: ZMODUL08:21
  for V being torsion-free Z_Module holds
  ex T being linear-transformation of V, EMbedding(V)
  st T is bijective & T = MorphsZQ(V) &
  (for v being Vector of V holds T.v = Class(EQRZM(V),[v,1]) );

theorem :: ZMODUL08:22
  for V being torsion-free Z_Module, vv being Vector of EMbedding(V)
  holds ex v being Vector of V st (MorphsZQ(V)).v = vv;

definition
  let V be torsion-free Z_Module;
  func DivisibleMod(V) -> strict Z_Module means
:: ZMODUL08:def 4

  the carrier of it = Class EQRZM(V) &
  the ZeroF of it = zeroCoset(V) &
  the addF of it = addCoset(V) &
  the lmult of it = (lmultCoset(V)) | [:INT, Class EQRZM(V):];
end;

theorem :: ZMODUL08:23
  for V being torsion-free Z_Module holds
  for v being Vector of DivisibleMod(V) holds
  for a being Element of INT.Ring st a <> 0 holds
  ex u being Vector of DivisibleMod(V) st a*u = v;

registration
  let V be torsion-free Z_Module;
  cluster DivisibleMod(V) -> divisible;
end;

theorem :: ZMODUL08:24
  for V being torsion-free Z_Module holds
  EMbedding(V) is Submodule of DivisibleMod(V);

registration
  let V be finitely-generated torsion-free Z_Module;
  cluster EMbedding(V) -> finitely-generated;
end;

registration
  let V be non trivial torsion-free Z_Module;
  cluster EMbedding(V) -> non trivial;
end;

definition
  let G be Field;
  let V be VectSp of G;
  let W be Subset of V;
  let a be Element of G;
  func a*W -> Subset of V equals
:: ZMODUL08:def 5
  {a*u where u is Vector of V: u in W};
end;

definition
  let V be torsion-free Z_Module, r be Element of F_Rat;
  func EMbedding(r,V) -> strict Z_Module means
:: ZMODUL08:def 6
  the carrier of it = r* (rng MorphsZQ(V)) &
  the ZeroF of it = zeroCoset(V) &
  the addF of it = (addCoset(V)) || ( r* (rng MorphsZQ(V)) ) &
  the lmult of it = (lmultCoset(V)) |
  [:the carrier of INT.Ring,r* (rng MorphsZQ(V)):];
end;

theorem :: ZMODUL08:25
  for V being torsion-free Z_Module, r being Element of F_Rat holds
  (for x being Vector of EMbedding(r,V)
  holds x is Vector of Z_MQ_VectSp(V)) &
  0.EMbedding(r,V) = 0.Z_MQ_VectSp(V) &
  (for x, y being Vector of EMbedding(r,V),
  v, w being Vector of Z_MQ_VectSp(V) st x = v & y = w holds x+y = v+w ) &
  for i being Element of INT.Ring, j being Element of F_Rat,
  x being Vector of EMbedding(r, V), v being Vector of Z_MQ_VectSp(V)
  st i = j & x = v holds i*x = j*v;

theorem :: ZMODUL08:26
  for V being torsion-free Z_Module,
  r being Element of F_Rat holds
  (for v, w being Vector of Z_MQ_VectSp(V)
  st v in EMbedding(r,V) & w in EMbedding(r,V)
  holds v+w in EMbedding(r,V) ) &
  for j being Element of F_Rat,
  v being Vector of Z_MQ_VectSp(V)
  st j in INT & v in EMbedding(r,V)
  holds j*v in EMbedding(r,V);

theorem :: ZMODUL08:27
  for V being torsion-free Z_Module, r being Element of F_Rat
  st r <> 0.F_Rat holds
  ex T being linear-transformation of EMbedding(V),EMbedding(r,V)
  st (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
  holds T.v = r*v) &
  T is bijective;

theorem :: ZMODUL08:28
  for V being torsion-free Z_Module, v being Vector of V holds
  Class(EQRZM(V), [v, 1]) in EMbedding(V);

theorem :: ZMODUL08:29
  for V being torsion-free Z_Module, v being Vector of DivisibleMod(V) holds
  ex a being Element of INT.Ring st a <> 0 & a * v in EMbedding(V);

registration
  let V be torsion-free Z_Module;
  cluster DivisibleMod(V) -> torsion-free;
end;

registration
  let V be torsion-free Z_Module;
  cluster EMbedding(V) -> torsion-free;
end;

registration
  let V be free Z_Module;
  cluster EMbedding(V) -> free;
end;

theorem :: ZMODUL08:30
  for V being torsion-free Z_Module holds
  (for v being Vector of Z_MQ_VectSp(V) holds v is Vector of DivisibleMod(V)) &
  (for v being Vector of DivisibleMod(V) holds v is Vector of Z_MQ_VectSp(V)) &
  0.(DivisibleMod(V)) = 0.(Z_MQ_VectSp(V));

theorem :: ZMODUL08:31
  for V being torsion-free Z_Module holds
  (for x, y being Vector of DivisibleMod(V),
  v, u being Vector of Z_MQ_VectSp(V) st x = v & y = u
  holds x + y = v + u) &
  (for z being Vector of DivisibleMod(V), w being Vector of Z_MQ_VectSp(V),
  a being Element of INT.Ring, aq being Element of F_Rat
  st z = w & a = aq holds
  a * z = aq * w) &
  (for z being Vector of DivisibleMod(V),
  w being Vector of Z_MQ_VectSp(V), aq being Element of F_Rat,
  a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w
    holds z = w) &
  (for x being Vector of DivisibleMod(V), v being Vector of Z_MQ_VectSp(V),
  r being Element of F_Rat, m, n being Element of INT.Ring,
  mi,ni be Integer
  st m=mi & n=ni & x = v & r <> 0.F_Rat & n <> 0 & r = mi / ni holds
  ex y being Vector of DivisibleMod(V) st x = n * y & r * v = m * y);

theorem :: ZMODUL08:32
  for V being torsion-free Z_Module, r being Element of F_Rat holds
  EMbedding(r, V) is Submodule of DivisibleMod(V);

registration
  let V be finitely-generated torsion-free Z_Module;
  let r be Element of F_Rat;
  cluster EMbedding(r, V) -> finitely-generated;
end;

registration
  let V be non trivial torsion-free Z_Module;
  let r be non zero Element of F_Rat;
  cluster EMbedding(r, V) -> non trivial;
end;

registration
  let V be torsion-free Z_Module;
  let r be Element of F_Rat;
  cluster EMbedding(r, V) -> torsion-free;
end;

registration
  let V be free Z_Module;
  let r be non zero Element of F_Rat;
  cluster EMbedding(r, V) -> free;
end;

theorem :: ZMODUL08:33
  for V being non trivial free Z_Module,
  v being Vector of DivisibleMod(V) holds
  ex a being Element of INT.Ring st
  a in NAT & a <> 0 & a * v in EMbedding(V) &
  for b being Element of INT.Ring
  st b in NAT & b < a & b <> 0 holds not b * v in EMbedding(V);

theorem :: ZMODUL08:34
  for V being finite-rank free Z_Module holds
  rank(EMbedding(V)) = rank(V);

theorem :: ZMODUL08:35
  for V being finite-rank free Z_Module, r being non zero Element of F_Rat
  holds rank(EMbedding(r, V)) = rank(EMbedding(V));

theorem :: ZMODUL08:36
  for V being finite-rank free Z_Module, r being non zero Element of F_Rat
  holds rank(EMbedding(r, V)) = rank(V);

registration
  cluster -> infinite for non trivial torsion-free Z_Module;
end;

theorem :: ZMODUL08:37
  for V being Z_Module holds
  ex A being Subset of V st (A is linearly-independent &
  for v being Vector of V holds ex a being Element of INT.Ring
  st a in NAT & a > 0 & a * v in Lin(A));

theorem :: ZMODUL08:38
  for V being non trivial torsion-free Z_Module, v being non zero Vector of V,
      A being Subset of V, a being Element of INT.Ring
  st a in NAT & A is linearly-independent & a > 0 & a * v in Lin(A)
  holds ex L being Linear_Combination of A, u being Vector of V
  st a * v = Sum(L) & u in A & L.u <> 0;

theorem :: ZMODUL08:39
  for V being torsion-free Z_Module, i being non zero Integer,
  r1, r2 being non zero Element of F_Rat st r2 = r1/i holds
  EMbedding(r1, V) is Submodule of EMbedding(r2, V);

theorem :: ZMODUL08:40
  for V being finite-rank free Z_Module,
  Z being Submodule of DivisibleMod(V) holds
  Z is finitely-generated iff
  ex r being non zero Element of F_Rat st Z is Submodule of EMbedding(r, V);