:: Free Product of Groups
:: by Sebastian Koch
::
:: Received April 27, 2025
:: Copyright (c) 2025 Association of Mizar Users

:: into FINSEQ_1

theorem Th1: :: GR_FREE0:1

for p being FinSequence st len p <> 0 holds
p | 1 = <*(p . 1)*>

proof end;

theorem Th2: :: GR_FREE0:2

for p being FinSequence st len p <> 0 holds
p /^ ((len p) -' 1) = <*(p . (len p))*>

proof end;

:: into FUNCT_5

theorem :: GR_FREE0:3

for f being Function
for x being object st x in dom f holds
(uncurry <*f*>) . (1,x) = f . x

proof end;

:: reformulation of TOPGEN5
:: into FUNCT_6

theorem Th4: :: GR_FREE0:4

for f being Function
for x being object st x in dom f holds
(commute <*f*>) . x = <*(f . x)*>

proof end;

:: into REWRITE1

registration

let X be FinSequence-membered set ;
let R be Relation of X;

cluster non trivial -> FinSequence-yielding for RedSequence of R;

coherence
for b₁ being RedSequence of R st not b₁ is trivial holds
b₁ is FinSequence-yielding

proof end;

end;

:: generalization of GROUP_7:39
:: into GROUP_7

theorem Th6: :: GR_FREE0:5

for I being non empty set
for i being Element of I
for F being Group-Family of I st I is trivial holds
F . i, product F are_isomorphic

proof end;

:: into MONOID_0

registration

cluster {} *+^ -> trivial ;

coherence
( not {} *+^ is empty & {} *+^ is trivial ) by MONOID_0:def 34, FUNCT_7:17;

cluster {} *+^+<0> -> trivial ;

coherence
( not {} *+^+<0> is empty & {} *+^+<0> is trivial ) by MONOID_0:61, FUNCT_7:17;

end;

definition

let M0 be multMagma-yielding Function;

func FreeAtoms M0 -> Relation equals :: GR_FREE0:def 1
*graph (Carrier M0);

coherence
*graph (Carrier M0) is Relation ;

end;

:: deftheorem defines FreeAtoms GR_FREE0:def 1 :
for M0 being multMagma-yielding Function holds FreeAtoms M0 = *graph (Carrier M0);

theorem Th7: :: GR_FREE0:6

for x, y being object
for M0 being multMagma-yielding Function holds
( [x,y] in FreeAtoms M0 iff ( x in dom M0 & y in (Carrier M0) . x ) )

proof end;

theorem Th8: :: GR_FREE0:7

for x being object
for M being non empty multMagma-yielding Function
for i being Element of dom M holds
( [i,x] in FreeAtoms M iff x in the carrier of (M . i) )

proof end;

theorem Th9: :: GR_FREE0:8

for x being object
for I being non empty set
for i being Element of I
for N being multMagma-Family of I holds
( [i,x] in FreeAtoms N iff x in the carrier of (N . i) )

proof end;

theorem Th10: :: GR_FREE0:9

for M0 being multMagma-yielding Function holds
( M0 = {} iff FreeAtoms M0 = {} )

proof end;

registration

cluster FreeAtoms {} -> empty ;

coherence
FreeAtoms {} is empty by Th10;
let M be non empty multMagma-yielding Function;

cluster FreeAtoms M -> non empty ;

coherence
not FreeAtoms M is empty by Th10;

end;

registration

let I be non empty set ;
let G be Group-like multMagma-Family of I;

cluster FreeAtoms G -> non empty ;

coherence
not FreeAtoms G is empty ;

end;

theorem Th11: :: GR_FREE0:10

for M being non empty multMagma-yielding Function holds FreeAtoms M = union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum }

proof end;

theorem Th12: :: GR_FREE0:11

for M1 being non empty multMagma holds FreeAtoms <*M1*> = [:{1}, the carrier of M1:]

proof end;

theorem Th13: :: GR_FREE0:12

for M1, M2 being non empty multMagma holds FreeAtoms <*M1,M2*> = [:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]

proof end;

theorem Th14: :: GR_FREE0:13

for M1, M2, M3 being non empty multMagma holds FreeAtoms <*M1,M2,M3*> = ([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) \/ [:{3}, the carrier of M3:]

proof end;

theorem :: GR_FREE0:14

for M1, M2, M3 being non empty multMagma
for x1 being Element of M1 holds
( [1,x1] in FreeAtoms <*M1*> & [1,x1] in FreeAtoms <*M1,M2*> & [1,x1] in FreeAtoms <*M1,M2,M3*> )

proof end;

theorem :: GR_FREE0:15

for M1, M2, M3 being non empty multMagma
for x2 being Element of M2 holds
( [2,x2] in FreeAtoms <*M1,M2*> & [2,x2] in FreeAtoms <*M1,M2,M3*> )

proof end;

theorem :: GR_FREE0:16

for M1, M2, M3 being non empty multMagma
for x3 being Element of M3 holds [3,x3] in FreeAtoms <*M1,M2,M3*>

proof end;

theorem :: GR_FREE0:17

for X being set
for M1 being non empty multMagma holds FreeAtoms (X --> M1) = [:X, the carrier of M1:]

proof end;

theorem Th19: :: GR_FREE0:18

for M0, N0 being multMagma-yielding Function holds FreeAtoms (M0 +* N0) c= (FreeAtoms M0) \/ (FreeAtoms N0)

proof end;

theorem :: GR_FREE0:19

for M0, N0 being multMagma-yielding Function st M0 tolerates N0 holds
FreeAtoms (M0 +* N0) = (FreeAtoms M0) \/ (FreeAtoms N0)

proof end;

theorem Th21: :: GR_FREE0:20

for I being non empty set
for G being Group-like multMagma-Family of I
for p being FinSequence of FreeAtoms G ex q being FinSequence of FreeAtoms G st
( len p = len q & ( for k being Nat
for i being Element of I
for g being Element of (G . i) st p . k = [i,g] holds
ex h being Element of (G . i) st
( g * h = 1_ (G . i) & (Rev q) . k = [i,h] ) ) )

proof end;

theorem Th22: :: GR_FREE0:21

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p being FinSequence of FreeAtoms H ex q being FinSequence of FreeAtoms H st
( len p = len q & ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) )

proof end;

theorem Th23: :: GR_FREE0:22

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> is FinSequence of FreeAtoms G

proof end;

theorem :: GR_FREE0:23

for I being non empty set
for i, j being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i)
for h being Element of (G . j) holds <*[i,g],[j,h]*> is FinSequence of FreeAtoms G

proof end;

definition

let I be set ;
let G be Group-like multMagma-Family of I;

func ReductionRel G -> Relation of ((FreeAtoms G) *+^+<0>) means :Def2: :: GR_FREE0:def 2
( ( I is empty implies it = {} ) & ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in it iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) );

existence
ex b₁ being Relation of ((FreeAtoms G) *+^+<0>) st
( ( I is empty implies b₁ = {} ) & ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in b₁ iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of ((FreeAtoms G) *+^+<0>) st ( I is empty implies b₁ = {} ) & ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in b₁ iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) & ( I is empty implies b₂ = {} ) & ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in b₂ iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ReductionRel GR_FREE0:def 2 :
for I being set
for G being Group-like multMagma-Family of I
for b₃ being Relation of ((FreeAtoms G) *+^+<0>) holds
( b₃ = ReductionRel G iff ( ( I is empty implies b₃ = {} ) & ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in b₃ iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) ) );

definition

let I be non empty set ;
let G be Group-like multMagma-Family of I;

redefine func ReductionRel G means :Def3: :: GR_FREE0:def 3
for p, q being FinSequence of FreeAtoms G holds
( [p,q] in it iff ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) );

compatibility
for b₁ being Relation of ((FreeAtoms G) *+^+<0>) holds
( b₁ = ReductionRel G iff for p, q being FinSequence of FreeAtoms G holds
( [p,q] in b₁ iff ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) )

proof end;

end;

:: deftheorem Def3 defines ReductionRel GR_FREE0:def 3 :
for I being non empty set
for G being Group-like multMagma-Family of I
for b₃ being Relation of ((FreeAtoms G) *+^+<0>) holds
( b₃ = ReductionRel G iff for p, q being FinSequence of FreeAtoms G holds
( [p,q] in b₃ iff ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) );

theorem Th25: :: GR_FREE0:24

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q, r being FinSequence of FreeAtoms G st [p,q] in ReductionRel G holds
( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G )

proof end;

theorem Th26: :: GR_FREE0:25

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G
for g, h being Element of (G . i) holds [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G

proof end;

theorem Th27: :: GR_FREE0:26

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for g, h being Element of (G . i) holds [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel G

proof end;

theorem Th28: :: GR_FREE0:27

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G holds [((p ^ <*[i,(1_ (G . i))]*>) ^ q),(p ^ q)] in ReductionRel G

proof end;

theorem Th29: :: GR_FREE0:28

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I holds [<*[i,(1_ (G . i))]*>,{}] in ReductionRel G

proof end;

theorem Th30: :: GR_FREE0:29

for I being non empty set
for G being Group-like multMagma-Family of I holds
( dom (ReductionRel G) c= (FreeAtoms G) * & rng (ReductionRel G) = (FreeAtoms G) * & field (ReductionRel G) = (FreeAtoms G) * )

proof end;

theorem Th31: :: GR_FREE0:30

for I being non empty set
for G being Group-like multMagma-Family of I
for x, y being object st [x,y] in ReductionRel G holds
( x is FinSequence of FreeAtoms G & y is FinSequence of FreeAtoms G )

proof end;

theorem Th32: :: GR_FREE0:31

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G
for g, h being Element of (G . i) st g * h = 1_ (G . i) holds
ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q

proof end;

theorem Th33: :: GR_FREE0:32

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G st len p = len q & ( for k being Nat
for i being Element of I
for g, h being Element of (G . i) st p . k = [i,g] & g * h = 1_ (G . i) holds
(Rev q) . k = [i,h] ) holds
ReductionRel G reduces p ^ q, {}

proof end;

Lm1: for I being non empty set
for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H st ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) holds
for k being Nat
for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]

proof end;

theorem Th34: :: GR_FREE0:33

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H st len p = len q & ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) holds
( ReductionRel H reduces p ^ q, {} & ReductionRel H reduces q ^ p, {} )

proof end;

theorem Th35: :: GR_FREE0:34

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q being FinSequence st [p,q] in ReductionRel G holds
len p = (len q) + 1

proof end;

theorem Th36: :: GR_FREE0:35

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G holds
( not ReductionRel G reduces p,q or p = q or len q < len p )

proof end;

registration

let I be non empty set ;
let G be Group-like multMagma-Family of I;

cluster ReductionRel G -> strongly-normalizing ;

coherence
ReductionRel G is strongly-normalizing

proof end;

end;

theorem Th37: :: GR_FREE0:36

for I being non empty set
for G being Group-like multMagma-Family of I holds {} is_a_normal_form_wrt ReductionRel G

proof end;

theorem Th38: :: GR_FREE0:37

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i) st g <> 1_ (G . i) holds
<*[i,g]*> is_a_normal_form_wrt ReductionRel G

proof end;

Lm2: for p1, q1, r1, p2, q2, r2 being FinSequence st len p1 = len p2 & len q1 = len q2 & (p1 ^ q1) ^ r1 = (p2 ^ q2) ^ r2 holds
( p1 = p2 & q1 = q2 & r1 = r2 )

proof end;

theorem Th39: :: GR_FREE0:38

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q1, q2 being FinSequence of FreeAtoms G st [p,q1] in ReductionRel G & [p,q2] in ReductionRel G & q1 <> q2 & ( for s, t being FinSequence of FreeAtoms G
for i being Element of I
for f, g, h being Element of (G . i) holds
( not p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t or ( not ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) & not ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) ) holds
ex r, s, t being FinSequence of FreeAtoms G ex i, j being Element of I st
( ( p = (((r ^ <*[i,(1_ (G . i))]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (G . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (G . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t ) ) ) or ex g, h being Element of (G . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (G . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (G . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (G . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (G . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) )

proof end;

registration

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;

cluster ReductionRel H -> subcommutative ;

coherence
ReductionRel H is subcommutative

proof end;

end;

registration

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;

cluster ReductionRel H -> with_UN_property complete ;

coherence
( ReductionRel H is complete & ReductionRel H is with_UN_property ) ;

end;

theorem Th40: :: GR_FREE0:39

for I being non empty set
for i, j being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i)
for h being Element of (H . j) holds
( <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )

proof end;

theorem Th41: :: GR_FREE0:40

for I being non empty set
for G being Group-like multMagma-Family of I
for p1, p2, q1, q2 being FinSequence of FreeAtoms G st ReductionRel G reduces p1,q1 & ReductionRel G reduces p2,q2 holds
ReductionRel G reduces p1 ^ p2,q1 ^ q2

proof end;

theorem Th42: :: GR_FREE0:41

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I st I is trivial holds
for p being non empty FinSequence of FreeAtoms G ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>

proof end;

theorem Th43: :: GR_FREE0:42

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p1, p2, q1, q2 being FinSequence of FreeAtoms H st p1,q1 are_convertible_wrt ReductionRel H & p2,q2 are_convertible_wrt ReductionRel H holds
p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H

proof end;

registration

let I be set ;
let H be Group-like associative multMagma-Family of I;

cluster EqCl (ReductionRel H) -> compatible ;

coherence
EqCl (ReductionRel H) is compatible

proof end;

end;

theorem Th44: :: GR_FREE0:43

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H st p ^ q is_a_normal_form_wrt ReductionRel H & len p <> 0 & len q <> 0 holds
(p . (len p)) `1 <> (q . 1) `1

proof end;

definition

let I be set ;
let H be Group-like associative multMagma-Family of I;

func FreeProduct H -> strict multMagma equals :: GR_FREE0:def 4
((FreeAtoms H) *+^+<0>) ./. (EqCl (ReductionRel H));

coherence
((FreeAtoms H) *+^+<0>) ./. (EqCl (ReductionRel H)) is strict multMagma ;

end;

:: deftheorem defines FreeProduct GR_FREE0:def 4 :
for I being set
for H being Group-like associative multMagma-Family of I holds FreeProduct H = ((FreeAtoms H) *+^+<0>) ./. (EqCl (ReductionRel H));

theorem Th45: :: GR_FREE0:44

for I being set
for H being Group-like associative multMagma-Family of I holds 1_ (FreeProduct H) = Class ((EqCl (ReductionRel H)),{})

proof end;

theorem Th46: :: GR_FREE0:45

for I being empty set
for H being Group-like associative multMagma-Family of I holds the carrier of (FreeProduct H) = {(1_ (FreeProduct H))}

proof end;

registration

let I be set ;
let H be Group-like associative multMagma-Family of I;

cluster FreeProduct H -> non empty strict Group-like ;

coherence
( FreeProduct H is Group-like & not FreeProduct H is empty )

proof end;

end;

definition

let I be set ;
let H be Group-like associative multMagma-Family of I;
:: original: FreeProduct
redefine func FreeProduct H -> strict Group;
coherence
FreeProduct H is strict Group ;

end;

registration

let I be empty set ;
let H be Group-like associative multMagma-Family of I;

cluster FreeProduct H -> trivial strict ;

coherence
FreeProduct H is trivial

proof end;

end;

theorem Th47: :: GR_FREE0:46

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H
for s, t being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) & t = Class ((EqCl (ReductionRel H)),q) holds
s * t = Class ((EqCl (ReductionRel H)),(p ^ q))

proof end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let i be Element of I;
let g be Element of (H . i);

func [*i,g*] -> Element of (FreeProduct H) equals :: GR_FREE0:def 5
Class ((EqCl (ReductionRel H)),<*[i,g]*>);

coherence
Class ((EqCl (ReductionRel H)),<*[i,g]*>) is Element of (FreeProduct H)

proof end;

end;

:: deftheorem defines [* GR_FREE0:def 5 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for i being Element of I
for g being Element of (H . i) holds [*i,g*] = Class ((EqCl (ReductionRel H)),<*[i,g]*>);

theorem Th48: :: GR_FREE0:47

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds <*[i,g]*> in [*i,g*]

proof end;

theorem Th49: :: GR_FREE0:48

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I holds [*i,(1_ (H . i))*] = 1_ (FreeProduct H)

proof end;

theorem Th50: :: GR_FREE0:49

for I being non empty set
for i, j being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i)
for h being Element of (H . j) holds
( [*i,g*] = [*j,h*] iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )

proof end;

theorem Th51: :: GR_FREE0:50

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g, h being Element of (H . i) holds [*i,g*] * [*i,h*] = [*i,(g * h)*]

proof end;

theorem :: GR_FREE0:51

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds [*i,g*] " = [*i,(g ")*]

proof end;

Lm3: for I being non empty set
for f, g being ManySortedSet of I holds dom <:f,g:> = I

proof end;

theorem Th53: :: GR_FREE0:52

for I being non empty set
for f, g being ManySortedSet of I holds dom (commute <*<:f,g:>*>) = I

proof end;

theorem Th54: :: GR_FREE0:53

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> = (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g

proof end;

theorem Th55: :: GR_FREE0:54

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I holds rng (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) = 1 -tuples_on [:{i}, the carrier of (G . i):]

proof end;

Lm4: for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I holds 1 -tuples_on [:{i}, the carrier of (G . i):] c= (FreeAtoms G) *

proof end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let i be Element of I;

func injection (H,i) -> Function of (H . i),(FreeProduct H) equals :: GR_FREE0:def 6
(proj (Class (EqCl (ReductionRel H)))) * (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>);

coherence
(proj (Class (EqCl (ReductionRel H)))) * (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>) is Function of (H . i),(FreeProduct H)

proof end;

end;

:: deftheorem defines injection GR_FREE0:def 6 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for i being Element of I holds injection (H,i) = (proj (Class (EqCl (ReductionRel H)))) * (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>);

theorem Th56: :: GR_FREE0:55

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds (injection (H,i)) . g = [*i,g*]

proof end;

registration

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let i be Element of I;

cluster injection (H,i) -> one-to-one multiplicative ;

coherence
( injection (H,i) is multiplicative & injection (H,i) is one-to-one )

proof end;

end;

theorem Th57: :: GR_FREE0:56

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I st I is trivial holds
injection (H,i) is bijective

proof end;

theorem Th58: :: GR_FREE0:57

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I st I is trivial holds
H . i, FreeProduct H are_isomorphic

proof end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let s be Element of (FreeProduct H);

func nf s -> FinSequence of FreeAtoms H means :Def7: :: GR_FREE0:def 7
( it in s & it is_a_normal_form_wrt ReductionRel H );

existence
ex b₁ being FinSequence of FreeAtoms H st
( b₁ in s & b₁ is_a_normal_form_wrt ReductionRel H )

proof end;

uniqueness
for b₁, b₂ being FinSequence of FreeAtoms H st b₁ in s & b₁ is_a_normal_form_wrt ReductionRel H & b₂ in s & b₂ is_a_normal_form_wrt ReductionRel H holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines nf GR_FREE0:def 7 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H)
for b₄ being FinSequence of FreeAtoms H holds
( b₄ = nf s iff ( b₄ in s & b₄ is_a_normal_form_wrt ReductionRel H ) );

theorem Th59: :: GR_FREE0:58

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p being FinSequence of FreeAtoms H
for s being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) holds
nf s = nf (p,(ReductionRel H))

proof end;

theorem Th60: :: GR_FREE0:59

for I being non empty set
for H being Group-like associative multMagma-Family of I
for k being Nat
for s, t being Element of (FreeProduct H) st t = Class ((EqCl (ReductionRel H)),((nf s) | k)) holds
nf t = (nf s) | k

proof end;

theorem Th61: :: GR_FREE0:60

for I being non empty set
for H being Group-like associative multMagma-Family of I
for k being Nat
for s, t being Element of (FreeProduct H) st t = Class ((EqCl (ReductionRel H)),((nf s) /^ k)) holds
nf t = (nf s) /^ k

proof end;

theorem Th62: :: GR_FREE0:61

for I being non empty set
for H being Group-like associative multMagma-Family of I holds nf (1_ (FreeProduct H)) = {}

proof end;

theorem Th63: :: GR_FREE0:62

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) st len (nf s) = 0 holds
s = 1_ (FreeProduct H)

proof end;

theorem Th64: :: GR_FREE0:63

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) st g <> 1_ (H . i) holds
nf [*i,g*] = <*[i,g]*>

proof end;

theorem Th65: :: GR_FREE0:64

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) st len (nf s) = 1 holds
ex i being Element of I ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] )

proof end;

theorem Th66: :: GR_FREE0:65

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
nf (s * t) = (nf s) ^ (nf t)

proof end;

theorem Th67: :: GR_FREE0:66

for I being non empty set
for H being Group-like associative multMagma-Family of I
for k being Nat
for s being Element of (FreeProduct H) st k <= len (nf s) holds
ex s1, s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )

proof end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let G be Group;

mode Homomorphism-Family of H,G -> Function-yielding ManySortedSet of I means :Def8: :: GR_FREE0:def 8
for i being Element of I holds it . i is Homomorphism of (H . i),G;

existence
ex b₁ being Function-yielding ManySortedSet of I st
for i being Element of I holds b₁ . i is Homomorphism of (H . i),G

proof end;

end;

:: deftheorem Def8 defines Homomorphism-Family GR_FREE0:def 8 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for G being Group
for b₄ being Function-yielding ManySortedSet of I holds
( b₄ is Homomorphism-Family of H,G iff for i being Element of I holds b₄ . i is Homomorphism of (H . i),G );

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;

func injection H -> Homomorphism-Family of H, FreeProduct H means :Def9: :: GR_FREE0:def 9
for i being Element of I holds it . i = injection (H,i);

existence
ex b₁ being Homomorphism-Family of H, FreeProduct H st
for i being Element of I holds b₁ . i = injection (H,i)

proof end;

uniqueness
for b₁, b₂ being Homomorphism-Family of H, FreeProduct H st ( for i being Element of I holds b₁ . i = injection (H,i) ) & ( for i being Element of I holds b₂ . i = injection (H,i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines injection GR_FREE0:def 9 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for b₃ being Homomorphism-Family of H, FreeProduct H holds
( b₃ = injection H iff for i being Element of I holds b₃ . i = injection (H,i) );

Lm5: for I being non empty set
for H being Group-like associative multMagma-Family of I
for G being Group
for F being Homomorphism-Family of H,G holds uncurry F is ManySortedSet of FreeAtoms H

proof end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let G be Group;
let F be Homomorphism-Family of H,G;
:: original: uncurry
redefine func uncurry F -> Function of (FreeAtoms H),G;
coherence
uncurry F is Function of (FreeAtoms H),G

proof end;

end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let G be Group;
let p be FinSequence of FreeAtoms H;
let F be Function of (FreeAtoms H),G;
:: original: *
redefine func F * p -> FinSequence of G;
coherence
p * F is FinSequence of G

proof end;

end;

definition

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let s be Element of (FreeProduct H);

func factorization s -> FinSequence of (FreeProduct H) equals :: GR_FREE0:def 10
(uncurry (injection H)) * (nf s);

coherence
(uncurry (injection H)) * (nf s) is FinSequence of (FreeProduct H) ;

end;

:: deftheorem defines factorization GR_FREE0:def 10 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) holds factorization s = (uncurry (injection H)) * (nf s);

theorem Th68: :: GR_FREE0:67

for I being non empty set
for H being Group-like associative multMagma-Family of I holds factorization (1_ (FreeProduct H)) = {}

proof end;

theorem Th69: :: GR_FREE0:68

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) st g <> 1_ (H . i) holds
factorization [*i,g*] = <*[*i,g*]*>

proof end;

theorem Th70: :: GR_FREE0:69

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
factorization (s * t) = (factorization s) ^ (factorization t)

proof end;

Lm6: for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds (uncurry (injection H)) . [i,g] = [*i,g*]

proof end;

theorem :: GR_FREE0:70

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H)
for k being Nat st 1 <= k & k <= len (factorization s) holds
ex i being Element of I ex g being Element of (H . i) st (factorization s) . k = [*i,g*]

proof end;

theorem Th72: :: GR_FREE0:71

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) holds Product (factorization s) = s

proof end;

registration

let I be non empty set ;
let H be Group-like associative multMagma-Family of I;
let s be Element of (FreeProduct H);

reduce Product (factorization s) to s;

reducibility
Product (factorization s) = s by Th72;

end;

registration

let G1, G2 be Group;

cluster <%G1,G2%> -> Group-like associative for multMagma-Family of 2;

coherence
for b₁ being multMagma-Family of 2 st b₁ = <%G1,G2%> holds
( b₁ is Group-like & b₁ is associative )

proof end;

end;

definition

let G1, G2 be Group;

func G1 ^* G2 -> strict Group means :: GR_FREE0:def 11
ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & it = FreeProduct H );

existence
ex b₁ being strict Group ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & b₁ = FreeProduct H )

proof end;

uniqueness
for b₁, b₂ being strict Group st ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & b₁ = FreeProduct H ) & ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & b₂ = FreeProduct H ) holds
b₁ = b₂ ;

end;

:: deftheorem defines ^* GR_FREE0:def 11 :
for G1, G2 being Group
for b₃ being strict Group holds
( b₃ = G1 ^* G2 iff ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & b₃ = FreeProduct H ) );

definition

let G be Group;

attr G is free means :: GR_FREE0:def 12
ex c being Cardinal st G, FreeProduct (c --> INT.Group) are_isomorphic ;

end;

:: deftheorem defines free GR_FREE0:def 12 :
for G being Group holds
( G is free iff ex c being Cardinal st G, FreeProduct (c --> INT.Group) are_isomorphic );

registration

cluster non empty trivial Group-like associative -> free for multMagma ;

coherence
for b₁ being Group st b₁ is trivial holds
b₁ is free

proof end;

cluster K286() -> free ;

coherence
INT.Group is free

proof end;

let c be Cardinal;

cluster FreeProduct (c --> INT.Group) -> free for Group;

coherence
for b₁ being Group st b₁ = FreeProduct (c --> INT.Group) holds
b₁ is free ;

end;

theorem :: GR_FREE0:72

for G, H being Group st G,H are_isomorphic holds
( G is free iff H is free ) by GROUP_6:67;

registration

cluster non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable cancelable free for multMagma ;

existence
ex b₁ being Group st b₁ is free

proof end;

end;

definition

let G be Group;

attr G is free-abelian means :: GR_FREE0:def 13
ex c being Cardinal st G, sum (c --> INT.Group) are_isomorphic ;

end;

:: deftheorem defines free-abelian GR_FREE0:def 13 :
for G being Group holds
( G is free-abelian iff ex c being Cardinal st G, sum (c --> INT.Group) are_isomorphic );

registration

cluster non empty trivial Group-like associative -> free-abelian for multMagma ;

coherence
for b₁ being Group st b₁ is trivial holds
b₁ is free-abelian

proof end;

cluster K286() -> free-abelian ;

coherence
INT.Group is free-abelian

proof end;

let c be Cardinal;

cluster sum (c --> INT.Group) -> free-abelian for Group;

coherence
for b₁ being Group st b₁ = sum (c --> INT.Group) holds
b₁ is free-abelian ;

end;

theorem :: GR_FREE0:73

for G, H being Group st G,H are_isomorphic holds
( G is free-abelian iff H is free-abelian ) by GROUP_6:67;

registration

cluster non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable cancelable free-abelian for multMagma ;

existence
ex b₁ being Group st b₁ is free-abelian

proof end;

end;