:: On the Trivial Many Sorted Algebras and Many Sorted Congruences
:: by Artur Korni\l owicz
::
:: Received June 11, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like I -defined Function-like total V32() for Element of Bool M;
existence
 not for b1 being Element of Bool M holds b1 is V32()
proofend;
end;

registration
let I be set ;
let M be V2() ManySortedSet of I;
cluster Relation-like V2() I -defined Function-like total V32() for ManySortedSubset of M;
existence
 ex b1 being ManySortedSubset of M st
( b1 is V2() & b1 is V32() )
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let o be OperSymbol of S;
cluster  ->  FinSequence-like for Element of Args (o,A);
coherence
 for b1 being Element of Args (o,A) holds b1 is FinSequence-like
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let I be set ;
let s be SortSymbol of S;
let F be MSAlgebra-Family of I,S;
cluster  ->  Relation-like Function-like for Element of (SORTS F) . s;
coherence
 for b1 being Element of (SORTS F) . s holds
( b1 is Function-like & b1 is Relation-like )
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeGen X -> V2() free ;
coherence
 ( FreeGen X is free & FreeGen X is non-empty ) by MSAFREE:14, MSAFREE:16;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeMSA X ->  free ;
coherence
 FreeMSA X is free by MSAFREE:17;
end;

registration
let S be non empty non void ManySortedSign ;
let A, B be non-empty MSAlgebra over S;
cluster[:A,B:] ->  non-empty ;
coherence
 [:A,B:] is non-empty
proofend;
end;

theorem :: MSUALG_9:1
for a, X, Y being set
for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
proofend;

theorem Th2: :: MSUALG_9:2
for X being non empty set
for Y being set
for f being Function of X,{Y} holds rng f = {Y}
proofend;

theorem Th3: :: MSUALG_9:3
for I being set holds Class (nabla I) c= {I}
proofend;

theorem Th4: :: MSUALG_9:4
for I being non empty set holds Class (nabla I) = {I}
proofend;

theorem Th5: :: MSUALG_9:5
for I, a being set ex A being ManySortedSet of I st {A} = I --> {a}
proofend;

theorem :: MSUALG_9:6
for I being set
for A being ManySortedSet of I ex B being V2() ManySortedSet of I st A c= B
proofend;

theorem :: MSUALG_9:7
for I being set
for M being V2() ManySortedSet of I
for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C
proofend;

theorem :: MSUALG_9:8
for I being set
for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A,{B} holds F = G
proofend;

theorem Th9: :: MSUALG_9:9
for I being set
for A being V2() ManySortedSet of I
for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
proofend;

theorem Th10: :: MSUALG_9:10
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
proofend;

theorem :: MSUALG_9:11
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1"
proofend;

theorem :: MSUALG_9:12
for I being set
for A being V2() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"
proofend;

theorem :: MSUALG_9:13
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds
f = g
proofend;

theorem :: MSUALG_9:14
for S being non empty non void ManySortedSign
for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
proofend;

theorem :: MSUALG_9:15
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
proofend;

theorem :: MSUALG_9:16
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
proofend;

theorem Th17: :: MSUALG_9:17
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
proofend;

theorem Th18: :: MSUALG_9:18
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)
proofend;

theorem Th19: :: MSUALG_9:19
for S being non empty non void ManySortedSign
for A, B, C being non-empty MSAlgebra over S
for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
proofend;

definition
let I be set ;
let A be ManySortedSet of I;
let B, C be V2() ManySortedSet of I;
let F be ManySortedFunction of A,[|B,C|];
func Mpr1 F ->  ManySortedFunction of A,B means :Def1: :: MSUALG_9:def 1
 for i being set st i in I holds
it . i = pr1 (F . i);
existence
 ex b1 being ManySortedFunction of A,B st
for i being set st i in I holds
b1 . i = pr1 (F . i)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of A,B st ( for i being set st i in I holds
b1 . i = pr1 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr1 (F . i) ) holds
b1 = b2
proofend;
func Mpr2 F ->  ManySortedFunction of A,C means :Def2: :: MSUALG_9:def 2
 for i being set st i in I holds
it . i = pr2 (F . i);
existence
 ex b1 being ManySortedFunction of A,C st
for i being set st i in I holds
b1 . i = pr2 (F . i)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of A,C st ( for i being set st i in I holds
b1 . i = pr2 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr2 (F . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Mpr1 MSUALG_9:def_1_:_
 for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b6 being ManySortedFunction of A,B holds
( b6 = Mpr1 F iff for i being set st i in I holds
b6 . i = pr1 (F . i) );

:: deftheorem Def2 defines Mpr2 MSUALG_9:def_2_:_
 for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b6 being ManySortedFunction of A,C holds
( b6 = Mpr2 F iff for i being set st i in I holds
b6 . i = pr2 (F . i) );

theorem :: MSUALG_9:20
for I, a being set
for A being ManySortedSet of I
for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
proofend;

theorem :: MSUALG_9:21
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
proofend;

theorem :: MSUALG_9:22
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
proofend;

theorem :: MSUALG_9:23
for I being set
for A, M being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
proofend;

begin

registration
let S be non empty ManySortedSign ;
cluster the Sorts of (Trivial_Algebra S) -> V2() V32() ;
coherence
 ( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty )
proofend;
end;

registration
let S be non empty ManySortedSign ;
cluster Trivial_Algebra S ->  non-empty finite-yielding ;
coherence
 ( Trivial_Algebra S is finite-yielding & Trivial_Algebra S is non-empty )
proofend;
end;

theorem Th24: :: MSUALG_9:24
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
proofend;

theorem Th25: :: MSUALG_9:25
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
proofend;

theorem :: MSUALG_9:26
for S being non empty non void ManySortedSign
for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds
A, Trivial_Algebra S are_isomorphic
proofend;

begin

theorem :: MSUALG_9:27
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
proofend;

theorem :: MSUALG_9:28
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being Subset of (CongrLatt A)
for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
proofend;

theorem :: MSUALG_9:29
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds
the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
proofend;

theorem Th30: :: MSUALG_9:30
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F
proofend;

theorem Th31: :: MSUALG_9:31
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)
proofend;

theorem :: MSUALG_9:32
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
proofend;

theorem :: MSUALG_9:33
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
proofend;

Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_A_being_non-empty_MSAlgebra_over_S
for_C1,_C2_being_MSCongruence_of_A
for_G_being_ManySortedFunction_of_(QuotMSAlg_(A,C1)),(QuotMSAlg_(A,C2))_st_(_for_i_being_Element_of_S
for_x_being_Element_of_the_Sorts_of_(QuotMSAlg_(A,C1))_._i
for_xx_being_Element_of_the_Sorts_of_A_._i_st_x_=_Class_(C1,xx)_holds_
(G_._i)_._x_=_Class_(C2,xx)_)_holds_
G_is_"onto"
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is "onto"
let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is "onto"
let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is "onto"
let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) implies G is "onto" )
assume A1: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ; ::_thesis: G is "onto"
thus  G is "onto" ::_thesis: verum
proof
let i be set ; :: according toMSUALG_3:def_3 ::_thesis: ( not i in the carrier of S or rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i )
set sL = the Sorts of (QuotMSAlg (A,C1));
set sP = the Sorts of (QuotMSAlg (A,C2));
assume  i in the carrier of S ; ::_thesis: rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i
then reconsider s = i as SortSymbol of S ;
A2: dom (G . s) = the Sorts of (QuotMSAlg (A,C1)) . s by FUNCT_2:def_1;
 rng (G . s) c= the Sorts of (QuotMSAlg (A,C2)) . s ;
hence  rng (G . i) c= the Sorts of (QuotMSAlg (A,C2)) . i ; :: according toXBOOLE_0:def_10 ::_thesis: the Sorts of (QuotMSAlg (A,C2)) . i c= rng (G . i)
let q be set ; :: according toTARSKI:def_3 ::_thesis: ( not q in the Sorts of (QuotMSAlg (A,C2)) . i or q in rng (G . i) )
assume  q in the Sorts of (QuotMSAlg (A,C2)) . i ; ::_thesis: q in rng (G . i)
then  q in Class (C2 . s) by MSUALG_4:def_6;
then consider a being set  such that
A3: a in the Sorts of A . s and
A4: q = Class ((C2 . s),a) by EQREL_1:def_3;
reconsider a = a as Element of the Sorts of A . s by A3;
 Class ((C1 . s),a) in Class (C1 . s) by EQREL_1:def_3;
then reconsider x = Class (C1,a) as Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def_6;
(G . s) . x = Class (C2,a) by A1
.= Class ((C2 . s),a) ;
hence  q in rng (G . i) by A4, A2, FUNCT_1:def_3; ::_thesis: verum
end;
end;

theorem Th34: :: MSUALG_9:34
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)
proofend;

theorem Th35: :: MSUALG_9:35
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
proofend;

theorem :: MSUALG_9:36
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
proofend;