The abstract of the Mizar article:

On the Trivial Many Sorted Algebras and Many Sorted Congruences

by

Artur Kornilowicz

Received June 11, 1996

MML identifier: MSUALG_9

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_1, MSUALG_1, PBOOLE, FUNCT_1, PRE_CIRC, CLOSURE2, CAT_4,
      MSUALG_2, ZF_REFLE, FINSET_1, FINSEQ_1, RELAT_1, QC_LANG1, PRALG_2,
      CARD_3, RLVECT_2, MSAFREE, PRELAMB, PRALG_1, FUNCT_3, MCART_1, EQREL_1,
      FUNCOP_1, BOOLE, MSUALG_3, TREES_4, LANG1, BORSUK_1, ALG_1, GROUP_6,
      WELLORD1, TDGROUP, FINSEQ_4, NATTRA_1, FUNCT_6, MSUALG_4, MSUALG_5,
      SETFAM_1, FUNCT_4, CANTOR_1, RELAT_2, MSUALG_9;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1,
      RELAT_2, STRUCT_0, SETFAM_1, RELSET_1, FUNCT_1, EQREL_1, FUNCT_2,
      FINSEQ_1, LANG1, MCART_1, FINSET_1, CARD_3, FINSEQ_4, CANTOR_1, TREES_4,
      DTCONSTR, PBOOLE, MSUALG_1, MSUALG_2, PRALG_3, MSUALG_3, MSAFREE,
      PRALG_2, PRE_CIRC, MSAFREE2, MSUALG_4, AUTALG_1, EXTENS_1, PZFMISC1,
      MSSUBFAM, CLOSURE1, CLOSURE2, MSUALG_5;
 constructors AUTALG_1, BINOP_1, CANTOR_1, CLOSURE1, CLOSURE2, EXTENS_1,
      MSAFREE2, MSUALG_5, PRALG_3, PRE_CIRC, PZFMISC1, FINSEQ_4;
 clusters CANTOR_1, CLOSURE2, EQREL_1, FINSET_1, MSAFREE, MSSUBFAM, MSUALG_1,
      MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5, PRALG_1, PRALG_2, PRE_CIRC,
      PZFMISC1, RELSET_1, STRUCT_0, ARYTM_3, XBOOLE_0, MEMBERED, PARTFUN1,
      NUMBERS, ORDINAL2;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

reserve a, I for set,
        S for non empty non void ManySortedSign;

scheme MSSExD { I() -> non empty set, P[set,set] }:
 ex f being ManySortedSet of I() st for i being Element of I() holds P[i,f.i]
  provided
 for i being Element of I() ex j being set st P[i,j];

definition let I be set,
               M be ManySortedSet of I;
 cluster locally-finite Element of Bool M;
end;

definition let I be set,
               M be non-empty ManySortedSet of I;
 cluster non-empty locally-finite ManySortedSubset of M;
end;

definition let S be non empty non void ManySortedSign,
               A be non-empty MSAlgebra over S,
               o be OperSymbol of S;
 cluster -> FinSequence-like Element of Args(o,A);
end;

definition 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 Element of (SORTS F).s;
end;

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

definition let S be non void non empty ManySortedSign,
               X be non-empty ManySortedSet of the carrier of S;
 cluster FreeMSA X -> free;
end;

definition 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
for A being non empty finite set ex f being Function of NAT, A st rng f = A;

theorem :: MSUALG_9:4
Class(nabla I) c= {I};

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

theorem :: MSUALG_9:6
ex A being ManySortedSet of I st {A} = I --> {a};

theorem :: MSUALG_9:7
  for A being ManySortedSet of I
 ex B being non-empty ManySortedSet of I st A c= B;

theorem :: MSUALG_9:8
  for M being non-empty ManySortedSet of I
 for B being locally-finite ManySortedSubset of M
  ex C being non-empty locally-finite ManySortedSubset of M st B c= C;

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

theorem :: MSUALG_9:10
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:11
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:12
  for X being non-empty ManySortedSet of the carrier of S
 holds Reverse X is "1-1";

theorem :: MSUALG_9:13
  for A being non-empty locally-finite ManySortedSet of I
 ex F being ManySortedFunction of I --> NAT, A st F is "onto";

theorem :: MSUALG_9:14
  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;

theorem :: MSUALG_9:15
  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:16
  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:17
  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:18
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:19
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:20
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:21
  for F being ManySortedFunction of A, [| I-->{a} , I-->{a} |]
 holds Mpr1 F = Mpr2 F;

theorem :: MSUALG_9:22
  for F being ManySortedFunction of A, [|B,C|] st F is "onto"
 holds Mpr1 F is "onto";

theorem :: MSUALG_9:23
  for F being ManySortedFunction of A, [|B,C|] st F is "onto"
 holds Mpr2 F is "onto";

theorem :: MSUALG_9:24
  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

definition let S be non empty ManySortedSign;
 cluster the Sorts of Trivial_Algebra S -> locally-finite non-empty;
end;

definition let S be non empty ManySortedSign;
 cluster Trivial_Algebra S -> locally-finite non-empty;
end;

theorem :: MSUALG_9:25
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:26
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:27
  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:28
  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:29
  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:30
  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:31
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:32
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:33
  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:34
  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: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 ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2);

theorem :: MSUALG_9:36
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:37
  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);