:: 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
::           (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, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0,
      PBOOLE, 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, VALUED_1, RLSUB_1, ZFMISC_1, INT_1,
      ORDINAL1, RLVECT_2, ZMODUL01, ZMODUL03, ORDERS_1, RLVECT_3, RMOD_2,
      RANKNULL, UNIALG_1, MSAFREE2, INT_3, VECTSP_1, XCMPLX_0, MESFUNC1, MOD_3,
      MONOID_0, VECTSP10, ZMODUL02, ZMODUL05, ZMODUL06, ZMODUL07, INT_2,
      FUNCSDOM, VECTSP_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, ORDERS_1,
      INT_2, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1,
      FINSEQ_1, FINSEQOP, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, INT_3,
      VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MOD_2, BINOM, ZMODUL01,
      ZMODUL02, VECTSP10, ZMODUL03, GAUSSINT, ZMODUL05, ZMODUL06, RANKNULL;
 constructors BINOP_2, BINOM, UPROOTS, ORDERS_1, REALSET1, FINSEQOP, ALGSTR_1,
      ZMODUL01, ZMODUL02, EC_PF_1, ZMODUL04, ZMODUL05, ZMODUL06, VECTSP10,
      RELSET_1;
 registrations SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, STRUCT_0,
      RLVECT_1, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, ORDINAL1,
      XXREAL_0, NAT_1, INT_3, RELAT_1, VECTSP_1, GAUSSINT, RAT_1, XCMPLX_0,
      ZMODUL02, ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06, GRCAT_1, VECTSP_4;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Torsion-part of $\mathbb{Z}$-module

reserve x, y, y1, y2 for object;
reserve V for Z_Module;
reserve W, W1, W2 for Submodule of V;
reserve u, v for VECTOR of V;
reserve i, j, k, n for Element of NAT;

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

registration
  cluster prime non zero for Element of INT.Ring;
end;

registration
  cluster prime -> non zero for Element of INT.Ring;
end;

theorem :: ZMODUL07:2
  for V being 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 <> 0 & a * v in Lin(B));

theorem :: ZMODUL07:3
  for V being Z_Module, I being finite Subset of V, 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
  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;

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

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

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

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

theorem :: ZMODUL07:7
  for V being torsion-free Z_Module,
  W1, W2 being finite-rank free Submodule of V,
  I1 being Basis of W1 holds
  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));

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

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

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

definition
  let V be LeftMod of INT.Ring;
  func torsion_part(V) -> strict Subspace of V means
:: ZMODUL07:def 1

  the carrier of it = { v where v is Vector of V : v is torsion };
end;

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

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

registration
  let V be Z_Module;
  cluster VectQuot(V,torsion_part(V)) -> torsion-free;
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
:: ZMODUL07:def 2

  for v being Element of V holds it.v = v + W;
end;

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

theorem :: ZMODUL07:13
  for V, W being Z_Module,
  T being linear-transformation of V,W,
  s being FinSequence of V,
  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));

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

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

begin :: 2. $\mathbb Z$-module generated the rational number field

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) #);
end;

registration
  cluster Rat-Module -> non empty;
end;

registration
  cluster Rat-Module -> Abelian add-associative
  right_zeroed right_complementable scalar-distributive vector-distributive
  scalar-associative scalar-unital;
end;

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

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

registration
  cluster Rat-Module -> torsion-free;
end;

registration
  cluster Rat-Module -> non trivial;
end;

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

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

registration
  cluster Rat-Module -> non free;
end;

theorem :: ZMODUL07:18
  for A being finite Subset of Rat-Module holds
  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;

registration
  cluster Rat-Module -> non finitely-generated;
end;

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

begin :: 3. The rank-nullity theorem

reserve V,W for finite-rank free Z_Module;
reserve T for linear-transformation of V,W;

registration
  let W be finite-rank free Z_Module, V be Z_Module;
  let T be linear-transformation of V,W;
  cluster im T -> finite-rank free;
end;

definition
  let W be finite-rank free 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);
end;

definition
  let V be finite-rank free 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);
end;

theorem :: ZMODUL07:20
  for V being finite-rank free Z_Module, A being Subset of V,
  B being linearly-independent Subset of V,
  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;

theorem :: ZMODUL07:21
  for V being finite-rank free Z_Module,
  A being Subset of V,
  B being linearly-independent Subset of V,
  T being linear-transformation of V,W,
  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);

theorem :: ZMODUL07:22
  for R being Ring
  for V, W being LeftMod of R, T being linear-transformation of V, W,
  A being Subset of V
  st A c= the carrier of (ker T)
  holds Lin(T .: A) = (0).W;

theorem :: ZMODUL07:23
  for R being Ring
  for V, W being LeftMod of R,
  T being linear-transformation of V, W,
  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);

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

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

::: 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
:: ZMODUL07:def 6
  it is bijective &
  for v being Element of V holds it.((ZQMorph(V,ker T)).v) = T.v;
end;

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

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

definition
  let R be Ring;
  let V, U, W be LeftMod of R,
  f be linear-transformation of V, U,
  g be linear-transformation of U, W;
  redefine func g*f -> linear-transformation of V, W;
end;

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

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

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

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

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

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

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

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

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

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

theorem :: ZMODUL07:38
  for R being Ring
  for V, U being LeftMod of R, V1 being Submodule of V,
      U1 being Submodule of U,
  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;

theorem :: ZMODUL07:39
  for R being Ring
  for V being LeftMod of R, W1, W2 being Submodule of V,
  U1 being Submodule of W1 + W2, 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;

theorem :: ZMODUL07:40
  for R being Ring
  for V being LeftMod of R, W1 being Submodule of V,
      W2 being Submodule of W1,
  U1 being Submodule of V, 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;

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

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

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

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

registration
  cluster non trivial for torsion Z_Module;
end;

registration
  cluster non torsion-free for Z_Module;
end;

registration
  let V be non torsion-free Z_Module;
  cluster non zero torsion for Vector of V;
end;

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

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

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

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

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

registration
  cluster finitely-generated for torsion Z_Module;
end;

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

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

registration
  let V be non torsion Z_Module;
  cluster VectQuot(V, torsion_part(V)) -> non trivial;
end;