:: On the Trivial Many Sorted Algebras and Many Sorted Congruences :: by Artur Korni\l owicz :: :: Received June 11, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, STRUCT_0, MSUALG_1, PBOOLE, FINSET_1, SUBSET_1, CLOSURE2, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, MARGREL1, NAT_1, PRALG_2, CARD_3, RLVECT_2, MSAFREE, PRELAMB, ZFMISC_1, PRALG_1, MCART_1, EQREL_1, FUNCOP_1, MSUALG_3, TREES_4, LANG1, NUMBERS, MSUALG_2, MEMBER_1, GROUP_6, WELLORD1, PARTFUN1, FUNCT_6, FINSEQ_4, PZFMISC1, CARD_1, MSUALG_4, MSUALG_5, SETFAM_1, FUNCT_4, RELAT_2, MSUALG_9; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, RELAT_2, STRUCT_0, SETFAM_1, FUNCT_1, PBOOLE, EQREL_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, LANG1, XTUPLE_0, MCART_1, FINSET_1, CARD_3, NAT_1, TREES_4, FUNCT_6, DTCONSTR, MSUALG_1, MSUALG_2, PRALG_1, MSUALG_3, MSAFREE, PRALG_2, FUNCOP_1, MSAFREE2, MSUALG_4, PZFMISC1, MSSUBFAM, CLOSURE2, MSUALG_5; constructors BINOP_1, PZFMISC1, MSUALG_3, MSUALG_5, CLOSURE1, CLOSURE2, PRALG_3, RELSET_1, CIRCUIT1, XTUPLE_0, NUMBERS; registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FINSET_1, EQREL_1, PRE_CIRC, PZFMISC1, MSSUBFAM, STRUCT_0, FUNCT_1, MSUALG_1, MSUALG_2, PRALG_2, MSUALG_3, MSAFREE, MSUALG_4, MSUALG_5, CLOSURE2, CARD_3, RELSET_1, PRALG_1, PBOOLE, XTUPLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve a, I for set, S for non empty non void ManySortedSign; registration let I be set, M be ManySortedSet of I; cluster finite-yielding for Element of Bool M; end; registration let I be set, M be non-empty ManySortedSet of I; cluster non-empty finite-yielding for ManySortedSubset of M; end; registration let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, o be OperSymbol of S; cluster -> FinSequence-like for Element of Args(o,A); end; registration let S be non void non empty ManySortedSign, I be set, s be SortSymbol of S, F be MSAlgebra-Family of I, S; cluster -> Function-like Relation-like for Element of (SORTS F).s; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeGen X -> free non-empty; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeMSA X -> free; end; registration let S be non empty non void ManySortedSign, A, B be non-empty MSAlgebra over S; cluster [:A,B:] -> non-empty; end; theorem :: MSUALG_9:1 for X, Y being set, f being Function st a in dom f & f.a in [:X,Y:] holds f.a = [(pr1 f).a, (pr2 f).a]; theorem :: MSUALG_9:2 for X being non empty set, Y being set, f being Function of X, {Y } holds rng f = {Y}; theorem :: MSUALG_9:3 Class(nabla I) c= {I}; theorem :: MSUALG_9:4 for I being non empty set holds Class(nabla I) = {I}; theorem :: MSUALG_9:5 ex A being ManySortedSet of I st {A} = I --> {a}; theorem :: MSUALG_9:6 for A being ManySortedSet of I ex B being non-empty ManySortedSet of I st A c= B; theorem :: MSUALG_9:7 for M being non-empty ManySortedSet of I for B being finite-yielding ManySortedSubset of M ex C being non-empty finite-yielding ManySortedSubset of M st B c= C; theorem :: MSUALG_9:8 for A, B being ManySortedSet of I for F, G being ManySortedFunction of A, {B} holds F = G; theorem :: MSUALG_9:9 for A being non-empty ManySortedSet of I, B being ManySortedSet of I for F being ManySortedFunction of A, {B} holds F is "onto"; theorem :: MSUALG_9:10 for A being ManySortedSet of I, B being non-empty ManySortedSet of I for F being ManySortedFunction of {A}, B holds F is "1-1"; theorem :: MSUALG_9:11 for X being non-empty ManySortedSet of the carrier of S holds Reverse X is "1-1"; theorem :: MSUALG_9:12 for A being non-empty finite-yielding ManySortedSet of I ex F being ManySortedFunction of I --> NAT, A st F is "onto"; 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 object holds proj(the Sorts of A,i).f = proj(the Sorts of A,i).g holds f = g; theorem :: MSUALG_9:14 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; theorem :: MSUALG_9:15 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 for h2 being ManySortedFunction of B, A st h1 = h2 holds h2 is_homomorphism B, A; theorem :: MSUALG_9:16 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; theorem :: MSUALG_9:17 for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A, B st F is "onto" for o being OperSymbol of S for x being Element of Args(o,B) holds ex y being Element of Args(o,A) st F # y = x ; theorem :: MSUALG_9:18 for A being non-empty MSAlgebra over S, 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); theorem :: MSUALG_9:19 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 for G being ManySortedFunction of B, C st G ** F1 = F2 holds G is_homomorphism B, C; reserve A, M for ManySortedSet of I, B, C for non-empty ManySortedSet of I; definition let I be set; let A be ManySortedSet of I; let B, C be non-empty ManySortedSet of I; let F be ManySortedFunction of A, [|B,C|]; func Mpr1 F -> ManySortedFunction of A, B means :: MSUALG_9:def 1 for i being set st i in I holds it.i = pr1 (F.i); func Mpr2 F -> ManySortedFunction of A, C means :: MSUALG_9:def 2 for i being set st i in I holds it.i = pr2 (F.i); end; theorem :: MSUALG_9:20 for F being ManySortedFunction of A, [| I-->{a} , I-->{a} |] holds Mpr1 F = Mpr2 F; theorem :: MSUALG_9:21 for F being ManySortedFunction of A, [|B,C|] st F is "onto" holds Mpr1 F is "onto"; theorem :: MSUALG_9:22 for F being ManySortedFunction of A, [|B,C|] st F is "onto" holds Mpr2 F is "onto"; theorem :: MSUALG_9:23 for F being ManySortedFunction of A, [|B,C|] st M in doms F holds for i be set st i in I holds (F..M).i = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i]; begin :: On the Trivial Many Sorted Algebras registration let S be non empty ManySortedSign; cluster the Sorts of Trivial_Algebra S -> finite-yielding non-empty; end; registration let S be non empty ManySortedSign; cluster Trivial_Algebra S -> finite-yielding non-empty; end; theorem :: MSUALG_9:24 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; theorem :: MSUALG_9:25 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; theorem :: MSUALG_9:26 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; begin :: On the Many Sorted Congruences theorem :: MSUALG_9:27 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|]; theorem :: MSUALG_9:28 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; theorem :: MSUALG_9:29 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}; theorem :: MSUALG_9:30 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; theorem :: MSUALG_9:31 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); theorem :: MSUALG_9:32 for A being MSAlgebra over S for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 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)); theorem :: MSUALG_9:33 for A being non-empty MSAlgebra over S, C being MSCongruence of A for s being SortSymbol of S, 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; theorem :: MSUALG_9:34 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); theorem :: MSUALG_9:35 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); theorem :: MSUALG_9:36 for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A, B st F is_homomorphism A, B for C1 being MSCongruence of A st C1 c= MSCng F ex H being ManySortedFunction of QuotMSAlg (A,C1), B st H is_homomorphism QuotMSAlg (A,C1), B & F = H ** MSNat_Hom(A,C1);