:: Free Magmas
:: by Marco Riccardi
::
:: Received October 20, 2009
:: Copyright (c) 2009-2016 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, FUNCT_1, ORDINAL1, RELAT_1, XBOOLE_0, TARSKI, AFINSQ_1,
SUBSET_1, YELLOW_6, ZFMISC_1, CLASSES1, PARTFUN1, ALGSTR_0, BINOP_1,
EQREL_1, MSUALG_6, STRUCT_0, GROUP_6, MSSUBFAM, FUNCT_2, SETFAM_1,
REALSET1, CIRCUIT2, CARD_1, XXREAL_0, FINSEQ_1, ARYTM_1, CARD_3, ARYTM_3,
NAT_1, XCMPLX_0, MCART_1, NAT_LAT, ALGSTR_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, XCMPLX_0,
XFAMILY, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_6, FUNCT_2,
XXREAL_0, NAT_1, CLASSES1, FINSEQ_1, CARD_3, AFINSQ_1, NAT_D, YELLOW_6,
BINOP_1, STRUCT_0, ALGSTR_0, RELSET_1, GROUP_6, MCART_1, NAT_LAT,
PARTFUN1, REALSET1, EQREL_1, ALG_1, GROUP_2;
constructors NAT_1, CLASSES1, AFINSQ_1, NAT_D, YELLOW_6, BINOP_1, RELSET_1,
FACIRC_1, GROUP_6, NAT_LAT, REALSET1, EQREL_1, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, CARD_1, FUNCT_2, INT_1, STRUCT_0, RELSET_1,
NAT_LAT, REALSET1, EQREL_1, GROUP_2, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
registration
let X be set;
let f be sequence of X;
let n be Nat;
cluster f|n -> Sequence-like;
end;
definition
let X,x be set;
func IFXFinSequence(x,X) -> XFinSequence of X equals
:: ALGSTR_4:def 1
x if x is XFinSequence of X
otherwise <%>X;
end;
definition
let X be non empty set;
let f be Function of X^omega, X;
let c be XFinSequence of X;
redefine func f.c -> Element of X;
end;
theorem :: ALGSTR_4:1
for X,Y,Z being set st Y c= the_universe_of X & Z c= the_universe_of X
holds [:Y,Z:] c= the_universe_of X;
scheme :: ALGSTR_4:sch 1
FuncRecursiveUniq { F(set) -> set, F1,F2() -> Function }:
F1() = F2()
provided
dom F1() = NAT & for n being Nat holds F1().n = F(F1()|n) and
dom F2() = NAT & for n being Nat holds F2().n = F(F2()|n);
scheme :: ALGSTR_4:sch 2
FuncRecursiveExist { F(set) -> set }:
ex f being Function st dom f = NAT &
for n being Nat holds f.n = F(f|n);
scheme :: ALGSTR_4:sch 3
FuncRecursiveUniqu2
{ X() -> non empty set, F(XFinSequence of X()) -> Element of X(),
F1,F2() -> sequence of X()}:
F1() = F2()
provided
for n being Nat holds F1().n = F(F1()|n) and
for n being Nat holds F2().n = F(F2()|n);
scheme :: ALGSTR_4:sch 4
FuncRecursiveExist2
{ X() -> non empty set, F(XFinSequence of X()) -> Element of X() }:
ex f being sequence of X() st
for n being Nat holds f.n = F(f|n);
definition
let f,g be Function;
pred f extends g means
:: ALGSTR_4:def 2
dom g c= dom f & f tolerates g;
end;
registration
cluster empty for multMagma;
end;
begin :: Equivalence Relations and Relators
:: Ch I §1.6 Def.11 Algebra I Bourbaki
definition
let M be multMagma;
let R be Equivalence_Relation of M;
attr R is compatible means
:: ALGSTR_4:def 3
for v,v9,w,w9 being Element of M st v in Class(R,v9) & w in Class(R,w9)
holds v*w in Class(R,v9*w9);
end;
registration
let M be multMagma;
cluster nabla the carrier of M -> compatible;
end;
registration
let M be multMagma;
cluster compatible for Equivalence_Relation of M;
end;
theorem :: ALGSTR_4:2
for M being multMagma, R being Equivalence_Relation of M holds
R is compatible iff for v,v9,w,w9 being Element of M
st Class(R,v) = Class(R,v9) & Class(R,w) = Class(R,w9)
holds Class(R,v*w) = Class(R,v9*w9);
definition
let M be multMagma;
let R be compatible Equivalence_Relation of M;
func ClassOp R -> BinOp of Class R means
:: ALGSTR_4:def 4
for x,y being Element of Class R, v,w being Element of M
st x = Class(R,v) & y = Class(R,w) holds it.(x,y) = Class(R,v*w)
if M is non empty otherwise it = {};
end;
:: Ch I §1.6 Def.11 Algebra I Bourbaki
definition
let M be multMagma;
let R be compatible Equivalence_Relation of M;
func M ./. R -> multMagma equals
:: ALGSTR_4:def 5
multMagma(# Class R, ClassOp R #);
end;
registration
let M be multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> strict;
end;
registration
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> non empty;
end;
definition
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
func nat_hom R -> Function of M, M ./. R means
:: ALGSTR_4:def 6
for v being Element of M holds it.v = Class(R,v);
end;
registration
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> multiplicative;
end;
registration
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> onto;
end;
definition
let M be multMagma;
mode Relators of M is [:the carrier of M,the carrier of M:]-valued Function;
end;
:: Ch I §1.6 Algebra I Bourbaki
definition
let M be multMagma;
let r be Relators of M;
func equ_rel r -> Equivalence_Relation of M equals
:: ALGSTR_4:def 7
meet {R where R is compatible Equivalence_Relation of M:
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w)};
end;
theorem :: ALGSTR_4:3
for M being multMagma, r being Relators of M,
R being compatible Equivalence_Relation of M
st (for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w))
holds equ_rel r c= R;
registration
let M be multMagma;
let r be Relators of M;
cluster equ_rel r -> compatible;
end;
definition
let X,Y be set;
let f be Function of X,Y;
func equ_kernel f -> Equivalence_Relation of X means
:: ALGSTR_4:def 8
for x,y being object holds [x,y] in it iff x in X & y in X & f.x = f.y;
end;
reserve M,N for non empty multMagma,
f for Function of M, N;
theorem :: ALGSTR_4:4
f is multiplicative implies equ_kernel f is compatible;
theorem :: ALGSTR_4:5
f is multiplicative implies
ex r being Relators of M st equ_kernel f = equ_rel r;
begin :: Submagmas and Stable Subsets
definition
let M be multMagma;
mode multSubmagma of M -> multMagma means
:: ALGSTR_4:def 9
the carrier of it c= the carrier of M &
the multF of it = (the multF of M)||the carrier of it;
end;
registration
let M be multMagma;
cluster strict for multSubmagma of M;
end;
registration
let M be non empty multMagma;
cluster non empty for multSubmagma of M;
end;
reserve M for multMagma;
reserve N,K for multSubmagma of M;
:: like GROUP_2:64
theorem :: ALGSTR_4:6
N is multSubmagma of K & K is multSubmagma of N
implies the multMagma of N = the multMagma of K;
theorem :: ALGSTR_4:7
the carrier of N = the carrier of M
implies the multMagma of N = the multMagma of M;
:: Ch I §1.4 Def.6 Algebra I Bourbaki
definition
let M be multMagma;
let A be Subset of M;
attr A is stable means
:: ALGSTR_4:def 10
for v,w being Element of M st v in A & w in A holds v*w in A;
end;
registration
let M be multMagma;
cluster stable for Subset of M;
end;
theorem :: ALGSTR_4:8
the carrier of N is stable Subset of M;
registration
let M be multMagma;
let N be multSubmagma of M;
cluster the carrier of N -> stable for Subset of M;
end;
theorem :: ALGSTR_4:9
for F being Function st
(for i being set st i in dom F holds F.i is stable Subset of M) holds
meet F is stable Subset of M;
reserve M,N for non empty multMagma,
A for Subset of M,
f,g for Function of M,N,
X for stable Subset of M,
Y for stable Subset of N;
theorem :: ALGSTR_4:10
A is stable iff A * A c= A;
:: Ch I §1.4 Pro.1 Algebra I Bourbaki
theorem :: ALGSTR_4:11
f is multiplicative implies f.:X is stable Subset of N;
:: Ch I §1.4 Pro.1 Algebra I Bourbaki
theorem :: ALGSTR_4:12
f is multiplicative implies f"Y is stable Subset of M;
:: Ch I §1.4 Pro.1 Algebra I Bourbaki
theorem :: ALGSTR_4:13
f is multiplicative & g is multiplicative
implies {v where v is Element of M: f.v=g.v} is stable Subset of M;
:: Ch I §1.4 Def.6 Algebra I Bourbaki
definition
let M be multMagma;
let A be stable Subset of M;
func the_mult_induced_by A -> BinOp of A equals
:: ALGSTR_4:def 11
(the multF of M) || A;
end;
:: like GROUP_4:def 5
definition
let M be multMagma;
let A be Subset of M;
func the_submagma_generated_by A -> strict multSubmagma of M means
:: ALGSTR_4:def 12
A c= the carrier of it & for N being strict multSubmagma of M
st A c= the carrier of N holds it is multSubmagma of N;
end;
theorem :: ALGSTR_4:14
for M being multMagma, A being Subset of M
holds A is empty iff the_submagma_generated_by A is empty;
registration
let M be multMagma;
let A be empty Subset of M;
cluster the_submagma_generated_by A -> empty;
end;
:: Ch I §1.4 Pro.1 Algebra I Bourbaki
theorem :: ALGSTR_4:15
for M,N being non empty multMagma, f being Function of M,N,
X being Subset of M st f is multiplicative holds
f.:the carrier of the_submagma_generated_by X =
the carrier of the_submagma_generated_by f.:X;
begin :: Free Magmas
:: Ch I §7.1 Algebra I Bourbaki
definition
let X be set;
func free_magma_seq X ->
sequence of bool the_universe_of(X \/ NAT) means
:: ALGSTR_4:def 13
it.0 = {} & it.1 = X & for n being Nat st n>=2 holds
ex fs being FinSequence st len fs = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
fs.p = [: it.p, it.(n-p) :] ) & it.n = Union disjoin fs;
end;
definition
let X be set;
let n be Nat;
func free_magma(X,n) -> set equals
:: ALGSTR_4:def 14
(free_magma_seq X).n;
end;
registration
let X be non empty set;
let n be non zero Nat;
cluster free_magma(X,n) -> non empty;
end;
reserve X for set;
theorem :: ALGSTR_4:16
free_magma(X,0) = {};
theorem :: ALGSTR_4:17
free_magma(X,1) = X;
theorem :: ALGSTR_4:18
free_magma(X,2) = [:[:X,X:],{1}:];
theorem :: ALGSTR_4:19
free_magma(X,3) = [:[:X,[:[:X,X:],{1}:]:],{1}:] \/
[:[:[:[:X,X:],{1}:],X:],{2}:];
reserve x,y,Y for set;
reserve n,m,p for Nat;
theorem :: ALGSTR_4:20
n >= 2 implies ex fs being FinSequence st len fs = n-1 &
(for p st p>=1 & p<=n-1 holds
fs.p = [: free_magma(X,p), free_magma(X,n-'p) :] ) &
free_magma(X,n) = Union disjoin fs;
theorem :: ALGSTR_4:21
n >= 2 & x in free_magma(X,n) implies ex p,m st x`2 = p & 1<=p & p<=n-1 &
x`1`1 in free_magma(X,p) & x`1`2 in free_magma(X,m) & n = p + m &
x in [:[:free_magma(X,p),free_magma(X,m):],{p}:];
theorem :: ALGSTR_4:22
x in free_magma(X,n) & y in free_magma(X,m) implies
[[x,y],n] in free_magma(X,n+m);
theorem :: ALGSTR_4:23
X c= Y implies free_magma(X,n) c= free_magma(Y,n);
definition
let X be set;
func free_magma_carrier X -> set
equals
:: ALGSTR_4:def 15
Union disjoin((free_magma_seq X)|NATPLUS);
end;
theorem :: ALGSTR_4:24
X = {} iff free_magma_carrier X = {};
registration
let X be empty set;
cluster free_magma_carrier X -> empty;
end;
registration
let X be non empty set;
cluster free_magma_carrier X -> non empty;
let w be Element of free_magma_carrier X;
cluster w`2 -> non zero natural for number;
end;
theorem :: ALGSTR_4:25
for X being non empty set, w being Element of free_magma_carrier X
holds w in [:free_magma(X,w`2),{w`2}:];
theorem :: ALGSTR_4:26
for X being non empty set, v,w being Element of free_magma_carrier X
holds [[[v`1,w`1],v`2],v`2+w`2] is Element of free_magma_carrier X;
theorem :: ALGSTR_4:27
X c= Y implies free_magma_carrier X c= free_magma_carrier Y;
theorem :: ALGSTR_4:28
n>0 implies [:free_magma(X,n),{n}:] c= free_magma_carrier X;
definition
let X be set;
func free_magma_mult X -> BinOp of free_magma_carrier X means
:: ALGSTR_4:def 16
for v,w being Element of free_magma_carrier X, n,m st n = v`2 & m = w`2
holds it.(v,w) = [[[v`1,w`1],v`2],n+m]
if X is non empty otherwise it = {};
end;
:: Ch I §7.1 Algebra I Bourbaki
definition
let X be set;
func free_magma X -> multMagma equals
:: ALGSTR_4:def 17
multMagma(# free_magma_carrier X, free_magma_mult X #);
end;
registration
let X be set;
cluster free_magma X -> strict;
end;
registration
let X be empty set;
cluster free_magma X -> empty;
end;
registration
let X be non empty set;
cluster free_magma X -> non empty;
let w be Element of free_magma X;
cluster w`2 -> non zero natural for number;
end;
theorem :: ALGSTR_4:29
for X being set, S being Subset of X
holds free_magma S is multSubmagma of free_magma X;
definition
let X be set;
let w be Element of free_magma X;
func length w -> Nat equals
:: ALGSTR_4:def 18
w`2 if X is non empty otherwise 0;
end;
theorem :: ALGSTR_4:30
X = {w`1 where w is Element of free_magma X: length w = 1};
reserve v,v1,v2,w,w1,w2 for Element of free_magma X;
theorem :: ALGSTR_4:31
X is non empty implies v*w = [[[v`1,w`1],v`2],length v + length w];
theorem :: ALGSTR_4:32
X is non empty implies v = [v`1,v`2] & length v >= 1;
theorem :: ALGSTR_4:33
length(v*w) = length v + length w;
theorem :: ALGSTR_4:34
length w >= 2 implies
ex w1,w2 st w = w1*w2 & length w1 < length w & length w2 < length w;
theorem :: ALGSTR_4:35
v1*v2 = w1*w2 implies v1 = w1 & v2 = w2;
definition
let X be set;
let n be Nat;
func canon_image(X,n) -> Function of free_magma(X,n),free_magma X means
:: ALGSTR_4:def 19
for x st x in dom it holds it.x = [x,n] if n > 0 otherwise it = {};
end;
registration
let X be set;
let n be Nat;
cluster canon_image(X,n) -> one-to-one;
end;
reserve X,Y,Z for non empty set;
theorem :: ALGSTR_4:36
for A being Subset of free_magma X st A = canon_image(X,1) .: X
holds free_magma X = the_submagma_generated_by A;
theorem :: ALGSTR_4:37
for R being compatible Equivalence_Relation of free_magma(X) holds
(free_magma X)./.R =
the_submagma_generated_by (nat_hom R).: (canon_image(X,1) .: X);
theorem :: ALGSTR_4:38
for f being Function of X,Y
holds canon_image(Y,1)*f is Function of X, free_magma Y;
definition
let X be non empty set;
let M be non empty multMagma;
let n,m be non zero Nat;
let f be Function of free_magma(X,n),M;
let g be Function of free_magma(X,m),M;
func [:f,g:] ->
Function of [:[:free_magma(X,n),free_magma(X,m):],{n}:], M means
:: ALGSTR_4:def 20
for x being Element of [:[:free_magma(X,n),free_magma(X,m):],{n}:],
y being Element of free_magma(X,n), z being Element of free_magma(X,m)
st y = x`1`1 & z = x`1`2 holds it.x = f.y * g.z;
end;
reserve M for non empty multMagma;
:: Ch I §7.1 Pro.1 Algebra I Bourbaki
theorem :: ALGSTR_4:39
for f being Function of X,M holds
ex h being Function of free_magma X, M st h is multiplicative &
h extends f*(canon_image(X,1)");
theorem :: ALGSTR_4:40
for f being Function of X,M, h,g being Function of free_magma X, M
st h is multiplicative & h extends f*(canon_image(X,1)") &
g is multiplicative & g extends f*(canon_image(X,1)") holds h = g;
reserve M,N for non empty multMagma,
f for Function of M, N,
H for non empty multSubmagma of N,
R for compatible Equivalence_Relation of M;
theorem :: ALGSTR_4:41
f is multiplicative & the carrier of H = rng f & R = equ_kernel f implies
ex g being Function of M./.R, H st f = g * nat_hom R &
g is bijective & g is multiplicative;
theorem :: ALGSTR_4:42
for g1,g2 being Function of M./.R, N st g1 * nat_hom R = g2 * nat_hom R
holds g1 = g2;
theorem :: ALGSTR_4:43
for M being non empty multMagma holds ex X being non empty set,
r being Relators of free_magma X,
g being Function of (free_magma X) ./. equ_rel r, M
st g is bijective & g is multiplicative;
definition
let X,Y be non empty set;
let f be Function of X,Y;
func free_magmaF f -> Function of free_magma X, free_magma Y means
:: ALGSTR_4:def 21
it is multiplicative & it extends (canon_image(Y,1)*f)*(canon_image(X,1)");
end;
registration
let X,Y be non empty set;
let f be Function of X,Y;
cluster free_magmaF f -> multiplicative;
end;
reserve f for Function of X,Y;
reserve g for Function of Y,Z;
theorem :: ALGSTR_4:44
free_magmaF(g*f) = free_magmaF(g)*free_magmaF(f);
theorem :: ALGSTR_4:45
for g being Function of X,Z st Y c= Z & f=g
holds free_magmaF f = free_magmaF g;
theorem :: ALGSTR_4:46
free_magmaF id X = id dom free_magmaF f;
:: Ch I §7.1 Pro.2 Algebra I Bourbaki
theorem :: ALGSTR_4:47
f is one-to-one implies free_magmaF f is one-to-one;
:: Ch I §7.1 Pro.2 Algebra I Bourbaki
theorem :: ALGSTR_4:48
f is onto implies free_magmaF f is onto;