:: Free Magmas
:: by Marco Riccardi
::
:: Received October 20, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users

registration

let X be set ;
let f be sequence of X;
let n be Nat;

cluster f | n -> Sequence-like ;

correctness
coherence
f | n is Sequence-like ;

proof end;

end;

definition

let X, x be set ;

func IFXFinSequence (x,X) -> XFinSequence of X equals :Def1: :: ALGSTR_4:def 1
x if x is XFinSequence of X
otherwise <%> X;

correctness
coherence
( ( x is XFinSequence of X implies x is XFinSequence of X ) & ( x is not XFinSequence of X implies <%> X is XFinSequence of X ) );
consistency
for b₁ being XFinSequence of X holds verum;
;

end;

:: deftheorem Def1 defines IFXFinSequence ALGSTR_4:def 1 :
for X, x being set holds
( ( x is XFinSequence of X implies IFXFinSequence (x,X) = x ) & ( x is not XFinSequence of X implies IFXFinSequence (x,X) = <%> X ) );

definition

let X be non empty set ;
let f be Function of (X ^omega),X;
let c be XFinSequence of X;
:: original: .
redefine func f . c -> Element of X;
correctness
coherence
f . c is Element of X;

proof end;

end;

theorem Th1: :: 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

proof end;

scheme :: ALGSTR_4:sch 1
FuncRecursiveUniq{ F₁( set ) -> set , F₂() -> Function, F₃() -> Function } :

F₂() = F₃()

provided

A1: ( dom F₂() = NAT & ( for n being Nat holds F₂() . n = F₁((F₂() | n)) ) ) and
A2: ( dom F₃() = NAT & ( for n being Nat holds F₃() . n = F₁((F₃() | n)) ) )

proof end;

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)) ) )

proof end;

scheme :: ALGSTR_4:sch 3
FuncRecursiveUniqu2{ F₁() -> non empty set , F₂( XFinSequence of F₁()) -> Element of F₁(), F₃() -> sequence of F₁(), F₄() -> sequence of F₁() } :

F₃() = F₄()

provided

A1: for n being Nat holds F₃() . n = F₂((F₃() | n)) and
A2: for n being Nat holds F₄() . n = F₂((F₄() | n))

proof end;

scheme :: ALGSTR_4:sch 4
FuncRecursiveExist2{ F₁() -> non empty set , F₂( XFinSequence of F₁()) -> Element of F₁() } :

ex f being sequence of F₁() st
for n being Nat holds f . n = F₂((f | n))

proof end;

definition

let f, g be Function;

pred f extends g means :: ALGSTR_4:def 2
( dom g c= dom f & f tolerates g );

end;

:: deftheorem defines extends ALGSTR_4:def 2 :
for f, g being Function holds
( f extends g iff ( dom g c= dom f & f tolerates g ) );

registration

cluster empty for multMagma ;

existence
ex b₁ being multMagma st b₁ is empty

proof end;

end;

:: 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 :Def3: :: 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;

:: deftheorem Def3 defines compatible ALGSTR_4:def 3 :
for M being multMagma
for R being Equivalence_Relation of M holds
( R is compatible iff 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)) );

registration

let M be multMagma ;

cluster nabla the carrier of M -> compatible ;

correctness
coherence
nabla the carrier of M is compatible ;

proof end;

end;

registration

let M be multMagma ;

cluster Relation-like the carrier of M -defined the carrier of M -valued total quasi_total V65() V70() compatible for Element of bool [: the carrier of M, the carrier of M:];

correctness
existence
ex b₁ being Equivalence_Relation of M st b₁ is compatible ;

proof end;

end;

theorem Th2: :: ALGSTR_4:2

for M being multMagma
for 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)) )

proof end;

definition

let M be multMagma ;
let R be compatible Equivalence_Relation of M;

func ClassOp R -> BinOp of (Class R) means :Def4: :: ALGSTR_4:def 4
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
it . (x,y) = Class (R,(v * w)) if not M is empty
otherwise it = {} ;

correctness
consistency
for b₁ being BinOp of (Class R) holds verum;
existence
( ( for b₁ being BinOp of (Class R) holds verum ) & ( not M is empty implies ex b₁ being BinOp of (Class R) st
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b₁ . (x,y) = Class (R,(v * w)) ) & ( M is empty implies ex b₁ being BinOp of (Class R) st b₁ = {} ) );
uniqueness
for b₁, b₂ being BinOp of (Class R) holds
( ( not M is empty & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b₁ . (x,y) = Class (R,(v * w)) ) & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b₂ . (x,y) = Class (R,(v * w)) ) implies b₁ = b₂ ) & ( M is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def4 defines ClassOp ALGSTR_4:def 4 :
for M being multMagma
for R being compatible Equivalence_Relation of M
for b₃ being BinOp of (Class R) holds
( ( not M is empty implies ( b₃ = ClassOp R iff for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b₃ . (x,y) = Class (R,(v * w)) ) ) & ( M is empty implies ( b₃ = ClassOp R iff b₃ = {} ) ) );

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

correctness
coherence
multMagma(# (Class R),(ClassOp R) #) is multMagma ;
;

end;

:: deftheorem defines ./. ALGSTR_4:def 5 :
for M being multMagma
for R being compatible Equivalence_Relation of M holds M ./. R = multMagma(# (Class R),(ClassOp R) #);

registration

let M be multMagma ;
let R be compatible Equivalence_Relation of M;

cluster M ./. R -> strict ;

correctness
coherence
M ./. R is strict ;
;

end;

registration

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;

cluster M ./. R -> non empty ;

correctness
coherence
not M ./. R is 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 :Def6: :: ALGSTR_4:def 6
for v being Element of M holds it . v = Class (R,v);

existence
ex b₁ being Function of M,(M ./. R) st
for v being Element of M holds b₁ . v = Class (R,v)

proof end;

uniqueness
for b₁, b₂ being Function of M,(M ./. R) st ( for v being Element of M holds b₁ . v = Class (R,v) ) & ( for v being Element of M holds b₂ . v = Class (R,v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines nat_hom ALGSTR_4:def 6 :
for M being non empty multMagma
for R being compatible Equivalence_Relation of M
for b₃ being Function of M,(M ./. R) holds
( b₃ = nat_hom R iff for v being Element of M holds b₃ . v = Class (R,v) );

registration

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;

cluster nat_hom R -> multiplicative ;

correctness
coherence
nat_hom R is multiplicative ;

proof end;

end;

registration

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;

cluster nat_hom R -> onto ;

correctness
coherence
nat_hom R is onto ;

proof end;

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
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w) } ;

correctness
coherence
meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w) } is Equivalence_Relation of M;

proof end;

end;

:: deftheorem defines equ_rel ALGSTR_4:def 7 :
for M being multMagma
for r being Relators of M holds equ_rel r = meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w) } ;

theorem Th3: :: ALGSTR_4:3

for M being multMagma
for r being Relators of M
for R being compatible Equivalence_Relation of M st ( for i being set
for 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

proof end;

registration

let M be multMagma ;
let r be Relators of M;

cluster equ_rel r -> compatible ;

coherence
equ_rel r is compatible

proof end;

end;

definition

let X, Y be set ;
let f be Function of X,Y;

func equ_kernel f -> Equivalence_Relation of X means :Def8: :: 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 ) );

existence
ex b₁ being Equivalence_Relation of X st
for x, y being object holds
( [x,y] in b₁ iff ( x in X & y in X & f . x = f . y ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of X st ( for x, y being object holds
( [x,y] in b₁ iff ( x in X & y in X & f . x = f . y ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ( x in X & y in X & f . x = f . y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines equ_kernel ALGSTR_4:def 8 :
for X, Y being set
for f being Function of X,Y
for b₄ being Equivalence_Relation of X holds
( b₄ = equ_kernel f iff for x, y being object holds
( [x,y] in b₄ iff ( x in X & y in X & f . x = f . y ) ) );

theorem Th4: :: ALGSTR_4:4

for M, N being non empty multMagma
for f being Function of M,N st f is multiplicative holds
equ_kernel f is compatible

proof end;

theorem Th5: :: ALGSTR_4:5

for M, N being non empty multMagma
for f being Function of M,N st f is multiplicative holds
ex r being Relators of M st equ_kernel f = equ_rel r

proof end;

definition

let M be multMagma ;

mode multSubmagma of M -> multMagma means :Def9: :: 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 );

existence
ex b₁ being multMagma st
( the carrier of b₁ c= the carrier of M & the multF of b₁ = the multF of M || the carrier of b₁ )

proof end;

end;

:: deftheorem Def9 defines multSubmagma ALGSTR_4:def 9 :
for M, b₂ being multMagma holds
( b₂ is multSubmagma of M iff ( the carrier of b₂ c= the carrier of M & the multF of b₂ = the multF of M || the carrier of b₂ ) );

registration

let M be multMagma ;

cluster strict for multSubmagma of M;

existence
ex b₁ being multSubmagma of M st b₁ is strict

proof end;

end;

registration

let M be non empty multMagma ;

cluster non empty for multSubmagma of M;

existence
not for b₁ being multSubmagma of M holds b₁ is empty

proof end;

end;

:: like GROUP_2:64

theorem Th6: :: ALGSTR_4:6

for M being multMagma
for N, K being multSubmagma of M st N is multSubmagma of K & K is multSubmagma of N holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #)

proof end;

theorem Th7: :: ALGSTR_4:7

for M being multMagma
for N being multSubmagma of M st the carrier of N = the carrier of M holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of M, the multF of M #)

proof end;

:: 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 :Def10: :: ALGSTR_4:def 10
for v, w being Element of M st v in A & w in A holds
v * w in A;

end;

:: deftheorem Def10 defines stable ALGSTR_4:def 10 :
for M being multMagma
for A being Subset of M holds
( A is stable iff for v, w being Element of M st v in A & w in A holds
v * w in A );

registration

let M be multMagma ;

cluster stable for Element of bool the carrier of M;

correctness
existence
ex b₁ being Subset of M st b₁ is stable ;

proof end;

end;

theorem Th8: :: ALGSTR_4:8

for M being multMagma
for N being multSubmagma of M holds the carrier of N is stable Subset of M

proof end;

registration

let M be multMagma ;
let N be multSubmagma of M;

cluster the carrier of N -> stable for Subset of M;

correctness
coherence
for b₁ being Subset of M st b₁ = the carrier of N holds
b₁ is stable ;
by Th8;

end;

theorem Th9: :: ALGSTR_4:9

for M being multMagma
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

proof end;

theorem :: ALGSTR_4:10

for M being non empty multMagma
for A being Subset of M holds
( A is stable iff A * A c= A )

proof end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki

theorem Th11: :: ALGSTR_4:11

for M, N being non empty multMagma
for f being Function of M,N
for X being stable Subset of M st f is multiplicative holds
f .: X is stable Subset of N

proof end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki

theorem Th12: :: ALGSTR_4:12

for M, N being non empty multMagma
for f being Function of M,N
for Y being stable Subset of N st f is multiplicative holds
f " Y is stable Subset of M

proof end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki

theorem :: ALGSTR_4:13

for M, N being non empty multMagma
for f, g being Function of M,N st f is multiplicative & g is multiplicative holds
{ v where v is Element of M : f . v = g . v } is stable Subset of M

proof end;

:: 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;

correctness
coherence
the multF of M || A is BinOp of A;

proof end;

end;

:: deftheorem defines the_mult_induced_by ALGSTR_4:def 11 :
for M being multMagma
for A being stable Subset of M holds the_mult_induced_by A = the multF of M || A;

:: 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 :Def12: :: 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 ) );

existence
ex b₁ being strict multSubmagma of M st
( A c= the carrier of b₁ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₁ is multSubmagma of N ) )

proof end;

uniqueness
for b₁, b₂ being strict multSubmagma of M st A c= the carrier of b₁ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₁ is multSubmagma of N ) & A c= the carrier of b₂ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₂ is multSubmagma of N ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines the_submagma_generated_by ALGSTR_4:def 12 :
for M being multMagma
for A being Subset of M
for b₃ being strict multSubmagma of M holds
( b₃ = the_submagma_generated_by A iff ( A c= the carrier of b₃ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₃ is multSubmagma of N ) ) );

theorem Th14: :: ALGSTR_4:14

for M being multMagma
for A being Subset of M holds
( A is empty iff the_submagma_generated_by A is empty )

proof end;

registration

let M be multMagma ;
let A be empty Subset of M;

cluster the_submagma_generated_by A -> empty strict ;

correctness
coherence
the_submagma_generated_by A is empty ;
by Th14;

end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki

theorem Th15: :: ALGSTR_4:15

for M, N being non empty multMagma
for f being Function of M,N
for 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))

proof end;

:: Ch I ?7.1 Algebra I Bourbaki

definition

let X be set ;
defpred S₁[ object , object ] means for fs being XFinSequence of bool (the_universe_of (X \/ NAT)) st $1 = fs holds
( ( dom fs = 0 implies $2 = {} ) & ( dom fs = 1 implies $2 = X ) & ( for n being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs1 . p = [:(fs . p),(fs . (n - p)):] ) & $2 = Union (disjoin fs1) ) ) );
A1: for e being object st e in (bool (the_universe_of (X \/ NAT))) ^omega holds
ex u being object st S₁[e,u]

proof end;

consider F being Function such that
A10: ( dom F = (bool (the_universe_of (X \/ NAT))) ^omega & ( for e being object st e in (bool (the_universe_of (X \/ NAT))) ^omega holds
S₁[e,F . e] ) ) from CLASSES1:sch 1(A1);
A11: for e being object st e in (bool (the_universe_of (X \/ NAT))) ^omega holds
F . e in bool (the_universe_of (X \/ NAT))

proof end;

func free_magma_seq X -> sequence of (bool (the_universe_of (X \/ NAT))) means :Def13: :: 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) ) ) );

existence
ex b₁ being sequence of (bool (the_universe_of (X \/ NAT))) st
( b₁ . 0 = {} & b₁ . 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 = [:(b₁ . p),(b₁ . (n - p)):] ) & b₁ . n = Union (disjoin fs) ) ) )

proof end;

uniqueness
for b₁, b₂ being sequence of (bool (the_universe_of (X \/ NAT))) st b₁ . 0 = {} & b₁ . 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 = [:(b₁ . p),(b₁ . (n - p)):] ) & b₁ . n = Union (disjoin fs) ) ) & b₂ . 0 = {} & b₂ . 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 = [:(b₂ . p),(b₂ . (n - p)):] ) & b₂ . n = Union (disjoin fs) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines free_magma_seq ALGSTR_4:def 13 :
for X being set
for b₂ being sequence of (bool (the_universe_of (X \/ NAT))) holds
( b₂ = free_magma_seq X iff ( b₂ . 0 = {} & b₂ . 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 = [:(b₂ . p),(b₂ . (n - p)):] ) & b₂ . n = Union (disjoin fs) ) ) ) );

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;

correctness
coherence
(free_magma_seq X) . n is set ;
;

end;

:: deftheorem defines free_magma ALGSTR_4:def 14 :
for X being set
for n being Nat holds free_magma (X,n) = (free_magma_seq X) . n;

registration

let X be non empty set ;
let n be non zero Nat;

cluster free_magma (X,n) -> non empty ;

correctness
coherence
not free_magma (X,n) is empty ;

proof end;

end;

theorem :: ALGSTR_4:16

for X being set holds free_magma (X,0) = {} by Def13;

theorem :: ALGSTR_4:17

for X being set holds free_magma (X,1) = X by Def13;

theorem Th18: :: ALGSTR_4:18

for X being set holds free_magma (X,2) = [:[:X,X:],{1}:]

proof end;

theorem :: ALGSTR_4:19

for X being set holds free_magma (X,3) = [:[:X,[:[:X,X:],{1}:]:],{1}:] \/ [:[:[:[:X,X:],{1}:],X:],{2}:]

proof end;

theorem Th20: :: ALGSTR_4:20

for X being set
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 = [:(free_magma (X,p)),(free_magma (X,(n -' p))):] ) & free_magma (X,n) = Union (disjoin fs) )

proof end;

theorem Th21: :: ALGSTR_4:21

for X, x being set
for n being Nat st n >= 2 & x in free_magma (X,n) holds
ex p, m being Nat 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}:] )

proof end;

theorem Th22: :: ALGSTR_4:22

for X, x, y being set
for n, m being Nat st x in free_magma (X,n) & y in free_magma (X,m) holds
[[x,y],n] in free_magma (X,(n + m))

proof end;

theorem Th23: :: ALGSTR_4:23

for X, Y being set
for n being Nat st X c= Y holds
free_magma (X,n) c= free_magma (Y,n)

proof end;

definition

let X be set ;

func free_magma_carrier X -> set equals :: ALGSTR_4:def 15
Union (disjoin ((free_magma_seq X) | NATPLUS));

correctness
coherence
Union (disjoin ((free_magma_seq X) | NATPLUS)) is set ;
;

end;

:: deftheorem defines free_magma_carrier ALGSTR_4:def 15 :
for X being set holds free_magma_carrier X = Union (disjoin ((free_magma_seq X) | NATPLUS));

Lm1: for X being set
for n being Nat st n > 0 holds
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X

proof end;

theorem Th24: :: ALGSTR_4:24

for X being set holds
( X = {} iff free_magma_carrier X = {} )

proof end;

registration

let X be empty set ;

cluster free_magma_carrier X -> empty ;

correctness
coherence
free_magma_carrier X is empty ;
by Th24;

end;

registration

let X be non empty set ;

cluster free_magma_carrier X -> non empty ;

correctness
coherence
not free_magma_carrier X is empty ;
by Th24;
let w be Element of free_magma_carrier X;

cluster w `2 -> natural non zero for number ;

correctness
coherence
for b₁ being number st b₁ = w `2 holds
( not b₁ is zero & b₁ is natural );

proof end;

end;

theorem Th25: :: ALGSTR_4:25

for X being non empty set
for w being Element of free_magma_carrier X holds w in [:(free_magma (X,(w `2))),{(w `2)}:]

proof end;

theorem Th26: :: ALGSTR_4:26

for X being non empty set
for 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

proof end;

theorem Th27: :: ALGSTR_4:27

for X, Y being set st X c= Y holds
free_magma_carrier X c= free_magma_carrier Y

proof end;

theorem :: ALGSTR_4:28

for X being set
for n being Nat st n > 0 holds
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X by Lm1;

definition

let X be set ;

func free_magma_mult X -> BinOp of (free_magma_carrier X) means :Def16: :: ALGSTR_4:def 16
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
it . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] if not X is empty
otherwise it = {} ;

correctness
consistency
for b₁ being BinOp of (free_magma_carrier X) holds verum;
existence
( ( for b₁ being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₁ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st b<sub>1</sub> = {} ) );
uniqueness
for b<sub>1</sub>, b<sub>2</sub> being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>1</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₂ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b₁ = b₂ ) & ( X is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def16 defines free_magma_mult ALGSTR_4:def 16 :
for X being set
for b₂ being BinOp of (free_magma_carrier X) holds
( ( not X is empty implies ( b₂ = free_magma_mult X iff for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₂ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) ) & ( X is empty implies ( b₂ = free_magma_mult X iff b₂ = {} ) ) );

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

correctness
coherence
multMagma(# (free_magma_carrier X),(free_magma_mult X) #) is multMagma ;
;

end;

:: deftheorem defines free_magma ALGSTR_4:def 17 :
for X being set holds free_magma X = multMagma(# (free_magma_carrier X),(free_magma_mult X) #);

registration

let X be set ;

cluster free_magma X -> strict ;

correctness
coherence
free_magma X is strict ;
;

end;

registration

let X be empty set ;

cluster free_magma X -> empty ;

correctness
coherence
free_magma X is empty ;
;

end;

registration

let X be non empty set ;

cluster free_magma X -> non empty ;

correctness
coherence
not free_magma X is empty ;
;
let w be Element of (free_magma X);

cluster w `2 -> natural non zero for number ;

correctness
coherence
for b₁ being number st b₁ = w `2 holds
( not b₁ is zero & b₁ is natural );
;

end;

theorem :: ALGSTR_4:29

for X being set
for S being Subset of X holds free_magma S is multSubmagma of free_magma X

proof end;

definition

let X be set ;
let w be Element of (free_magma X);

func length w -> Nat equals :Def18: :: ALGSTR_4:def 18
w `2 if not X is empty
otherwise 0 ;

correctness
coherence
( ( not X is empty implies w `2 is Nat ) & ( X is empty implies 0 is Nat ) );
consistency
for b₁ being Nat holds verum;
;

end;

:: deftheorem Def18 defines length ALGSTR_4:def 18 :
for X being set
for w being Element of (free_magma X) holds
( ( not X is empty implies length w = w `2 ) & ( X is empty implies length w = 0 ) );

theorem Th30: :: ALGSTR_4:30

for X being set holds X = { (w `1) where w is Element of (free_magma X) : length w = 1 }

proof end;

theorem Th31: :: ALGSTR_4:31

for X being set
for v, w being Element of (free_magma X) st not X is empty holds
v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))]

proof end;

theorem Th32: :: ALGSTR_4:32

for X being set
for v being Element of (free_magma X) st not X is empty holds
( v = [(v `1),(v `2)] & length v >= 1 )

proof end;

theorem :: ALGSTR_4:33

for X being set
for v, w being Element of (free_magma X) holds length (v * w) = (length v) + (length w)

proof end;

theorem Th34: :: ALGSTR_4:34

for X being set
for w being Element of (free_magma X) st length w >= 2 holds
ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )

proof end;

theorem :: ALGSTR_4:35

for X being set
for v1, v2, w1, w2 being Element of (free_magma X) st v1 * v2 = w1 * w2 holds
( v1 = w1 & v2 = w2 )

proof end;

definition

let X be set ;
let n be Nat;

func canon_image (X,n) -> Function of (free_magma (X,n)),(free_magma X) means :Def19: :: ALGSTR_4:def 19
for x being set st x in dom it holds
it . x = [x,n] if n > 0
otherwise it = {} ;

correctness
consistency
for b₁ being Function of (free_magma (X,n)),(free_magma X) holds verum;
existence
( ( for b₁ being Function of (free_magma (X,n)),(free_magma X) holds verum ) & ( n > 0 implies ex b₁ being Function of (free_magma (X,n)),(free_magma X) st
for x being set st x in dom b₁ holds
b₁ . x = [x,n] ) & ( not n > 0 implies ex b₁ being Function of (free_magma (X,n)),(free_magma X) st b₁ = {} ) );
uniqueness
for b₁, b₂ being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 & ( for x being set st x in dom b₁ holds
b₁ . x = [x,n] ) & ( for x being set st x in dom b₂ holds
b₂ . x = [x,n] ) implies b₁ = b₂ ) & ( not n > 0 & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def19 defines canon_image ALGSTR_4:def 19 :
for X being set
for n being Nat
for b₃ being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 implies ( b₃ = canon_image (X,n) iff for x being set st x in dom b₃ holds
b₃ . x = [x,n] ) ) & ( not n > 0 implies ( b₃ = canon_image (X,n) iff b₃ = {} ) ) );

Lm2: for X being set
for n being Nat holds canon_image (X,n) is one-to-one

proof end;

registration

let X be set ;
let n be Nat;

cluster canon_image (X,n) -> one-to-one ;

correctness
coherence
canon_image (X,n) is one-to-one ;
by Lm2;

end;

Lm3: for X being non empty set holds
( dom (canon_image (X,1)) = X & ( for x being set st x in X holds
(canon_image (X,1)) . x = [x,1] ) )

proof end;

theorem Th36: :: ALGSTR_4:36

for X being non empty set
for A being Subset of (free_magma X) st A = (canon_image (X,1)) .: X holds
free_magma X = the_submagma_generated_by A

proof end;

theorem :: ALGSTR_4:37

for X being non empty set
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))

proof end;

theorem Th38: :: ALGSTR_4:38

for X, Y being non empty set
for f being Function of X,Y holds (canon_image (Y,1)) * f is Function of X,(free_magma Y)

proof end;

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 :Def20: :: ALGSTR_4:def 20
for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
it . x = (f . y) * (g . z);

existence
ex b₁ being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M st
for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b₁ . x = (f . y) * (g . z)

proof end;

uniqueness
for b₁, b₂ being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M st ( for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b₁ . x = (f . y) * (g . z) ) & ( for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b₂ . x = (f . y) * (g . z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines [: ALGSTR_4:def 20 :
for X being non empty set
for M being non empty multMagma
for n, m being non zero Nat
for f being Function of (free_magma (X,n)),M
for g being Function of (free_magma (X,m)),M
for b₇ being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M holds
( b₇ = [:f,g:] iff for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b₇ . x = (f . y) * (g . z) );

:: Ch I ?7.1 Pro.1 Algebra I Bourbaki

theorem Th39: :: ALGSTR_4:39

for X being non empty set
for M being non empty multMagma
for f being Function of X,M ex h being Function of (free_magma X),M st
( h is multiplicative & h extends f * ((canon_image (X,1)) ") )

proof end;

theorem Th40: :: ALGSTR_4:40

for X being non empty set
for M being non empty multMagma
for f being Function of X,M
for 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

proof end;

theorem Th41: :: ALGSTR_4:41

for M, N being non empty multMagma
for f being Function of M,N
for H being non empty multSubmagma of N
for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )

proof end;

theorem :: ALGSTR_4:42

for M, N being non empty multMagma
for R being compatible Equivalence_Relation of M
for g1, g2 being Function of (M ./. R),N st g1 * (nat_hom R) = g2 * (nat_hom R) holds
g1 = g2

proof end;

theorem :: ALGSTR_4:43

for M being non empty multMagma ex X being non empty set ex r being Relators of (free_magma X) ex g being Function of ((free_magma X) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )

proof end;

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 :Def21: :: ALGSTR_4:def 21
( it is multiplicative & it extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") );

existence
ex b₁ being Function of (free_magma X),(free_magma Y) st
( b₁ is multiplicative & b₁ extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") )

proof end;

uniqueness
for b₁, b₂ being Function of (free_magma X),(free_magma Y) st b₁ is multiplicative & b₁ extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") & b₂ is multiplicative & b₂ extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines free_magmaF ALGSTR_4:def 21 :
for X, Y being non empty set
for f being Function of X,Y
for b₄ being Function of (free_magma X),(free_magma Y) holds
( b₄ = free_magmaF f iff ( b₄ is multiplicative & b₄ extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") ) );

registration

let X, Y be non empty set ;
let f be Function of X,Y;

cluster free_magmaF f -> multiplicative ;

coherence
free_magmaF f is multiplicative by Def21;

end;

theorem Th44: :: ALGSTR_4:44

for X, Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z holds free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f)

proof end;

theorem Th45: :: ALGSTR_4:45

for X, Y, Z being non empty set
for f being Function of X,Y
for g being Function of X,Z st Y c= Z & f = g holds
free_magmaF f = free_magmaF g

proof end;

theorem Th46: :: ALGSTR_4:46

for X, Y being non empty set
for f being Function of X,Y holds free_magmaF (id X) = id (dom (free_magmaF f))

proof end;

:: Ch I ?7.1 Pro.2 Algebra I Bourbaki

theorem :: ALGSTR_4:47

for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
free_magmaF f is one-to-one

proof end;

:: Ch I ?7.1 Pro.2 Algebra I Bourbaki

theorem :: ALGSTR_4:48

for X, Y being non empty set
for f being Function of X,Y st f is onto holds
free_magmaF f is onto

proof end;