The abstract of the Mizar article:

Institution of Many Sorted Algebras. Part I: Signature Reduct of an Algebra

by

Grzegorz Bancerek

Received December 30, 1996

MML identifier: INSTALG1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, PRALG_1, RELAT_1, MSUALG_3, BOOLE, AMI_1, MSUALG_1,
      ZF_REFLE, PBOOLE, MSATERM, FREEALG, MSAFREE, TDGROUP, FINSEQ_1, DTCONSTR,
      QC_LANG1, TREES_3, NATTRA_1, TREES_4, CARD_3, FUNCT_6, ALG_1, MSUALG_6,
      PUA2MSS1, FUNCT_4, REWRITE1, REALSET1, MSUALG_2, CAT_1, GROUP_6,
      INSTALG1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1,
      FINSEQ_1, STRUCT_0, FINSEQ_2, CARD_3, FINSEQ_4, LANG1, TREES_3, TREES_4,
      DTCONSTR, REWRITE1, FUNCT_7, PBOOLE, MSUALG_1, PARTFUN1, FUNCT_2,
      MSUALG_2, PRALG_2, MSUALG_3, PUA2MSS1, MSAFREE, MSATERM, AUTALG_1,
      MSUALG_6;
 constructors NAT_1, REWRITE1, MSATERM, PUA2MSS1, FUNCT_7, AUTALG_1, MSUALG_6,
      FINSEQ_4;
 clusters STRUCT_0, RELSET_1, FUNCT_1, TREES_3, PRALG_1, PBOOLE, MSUALG_1,
      MSAFREE, PRE_CIRC, MSUALG_9, MSATERM, FUNCT_2, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

canceled;

theorem :: INSTALG1:2
 for S being non empty non void ManySortedSign
 for o being OperSymbol of S
 for V being non-empty ManySortedSet of the carrier of S
 for x being set holds
   x is ArgumentSeq of Sym(o,V) iff x is Element of Args(o, FreeMSA V);

definition
 let S be non empty non void ManySortedSign;
 let V be non-empty ManySortedSet of the carrier of S;
 let o be OperSymbol of S;
 cluster -> DTree-yielding Element of Args(o, FreeMSA V);
end;

theorem :: INSTALG1:3
 for S being non empty non void ManySortedSign
 for A1,A2 being MSAlgebra over S st
   the Sorts of A1 is_transformable_to the Sorts of A2
 for o being OperSymbol of S st Args(o,A1) <> {} holds Args(o,A2) <> {};

theorem :: INSTALG1:4
 for S being non empty non void ManySortedSign
 for o being OperSymbol of S
 for V being non-empty ManySortedSet of the carrier of S
 for x being Element of Args(o, FreeMSA V) holds
   Den(o,FreeMSA V).x = [o, the carrier of S]-tree x;

definition
 let S be non empty non void ManySortedSign;
 let A be non-empty MSAlgebra over S;
 cluster the MSAlgebra of A -> non-empty;
end;

theorem :: INSTALG1:5
 for S being non empty non void ManySortedSign
 for A,B being MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B
 for o being OperSymbol of S holds Den(o,A) = Den(o,B);

theorem :: INSTALG1:6
 for S being non empty non void ManySortedSign
 for A1,A2,B1,B2 being MSAlgebra over S
  st the MSAlgebra of A1 = the MSAlgebra of B1 &
     the MSAlgebra of A2 = the MSAlgebra of B2
 for f being ManySortedFunction of A1,A2
 for g being ManySortedFunction of B1,B2 st f = g
 for o being OperSymbol of S st Args(o,A1) <> {} & Args(o,A2) <> {}
 for x being Element of Args(o,A1)
 for y being Element of Args(o,B1) st x = y
  holds f#x = g#y;

theorem :: INSTALG1:7
   for S being non empty non void ManySortedSign
 for A1,A2,B1,B2 being MSAlgebra over S
  st the MSAlgebra of A1 = the MSAlgebra of B1 &
     the MSAlgebra of A2 = the MSAlgebra of B2 &
     the Sorts of A1 is_transformable_to the Sorts of A2
 for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2
 ex h' being ManySortedFunction of B1,B2 st
   h' = h & h' is_homomorphism B1,B2;

definition
 let S be ManySortedSign;
 attr S is feasible means
:: INSTALG1:def 1

  the carrier of S = {} implies the OperSymbols of S = {};
end;

theorem :: INSTALG1:8
 for S being ManySortedSign holds S is feasible iff
  dom the ResultSort of S = the OperSymbols of S;

definition
 cluster non empty -> feasible ManySortedSign;
 cluster void -> feasible ManySortedSign;
 cluster empty feasible -> void ManySortedSign;
 cluster non void feasible -> non empty ManySortedSign;
end;

definition
 cluster non void non empty ManySortedSign;
end;

theorem :: INSTALG1:9
 for S being feasible ManySortedSign holds
   id the carrier of S, id the OperSymbols of S form_morphism_between S,S;

theorem :: INSTALG1:10
 for S1,S2 being ManySortedSign
 for f,g being Function st f,g form_morphism_between S1,S2
  holds f is Function of the carrier of S1, the carrier of S2 &
   g is Function of the OperSymbols of S1, the OperSymbols of S2;

begin :: Subsignature

definition
 let S be feasible ManySortedSign;
 mode Subsignature of S -> ManySortedSign means
:: INSTALG1:def 2

  id the carrier of it, id the OperSymbols of it form_morphism_between it,S;
end;

theorem :: INSTALG1:11
 for S being feasible ManySortedSign, T being Subsignature of S holds
   the carrier of T c= the carrier of S &
   the OperSymbols of T c= the OperSymbols of S;

definition
 let S be feasible ManySortedSign;
 cluster -> feasible Subsignature of S;
end;

theorem :: INSTALG1:12
 for S being feasible ManySortedSign, T being Subsignature of S holds
   the ResultSort of T c= the ResultSort of S &
   the Arity of T c= the Arity of S;

theorem :: INSTALG1:13
 for S being feasible ManySortedSign, T being Subsignature of S holds
  the Arity of T = (the Arity of S)|the OperSymbols of T &
  the ResultSort of T = (the ResultSort of S)|the OperSymbols of T;

theorem :: INSTALG1:14
 for S,T being feasible ManySortedSign
  st the carrier of T c= the carrier of S &
     the Arity of T c= the Arity of S &
     the ResultSort of T c= the ResultSort of S
  holds T is Subsignature of S;

theorem :: INSTALG1:15
   for S,T being feasible ManySortedSign
  st the carrier of T c= the carrier of S &
     the Arity of T = (the Arity of S)|the OperSymbols of T &
     the ResultSort of T = (the ResultSort of S)|the OperSymbols of T
  holds T is Subsignature of S;

theorem :: INSTALG1:16
 for S being feasible ManySortedSign holds S is Subsignature of S;

theorem :: INSTALG1:17
   for S1 being feasible ManySortedSign
 for S2 being Subsignature of S1
 for S3 being Subsignature of S2 holds S3 is Subsignature of S1;

theorem :: INSTALG1:18
   for S1 being feasible ManySortedSign
 for S2 being Subsignature of S1 st S1 is Subsignature of S2
  holds the ManySortedSign of S1 = the ManySortedSign of S2;

definition
 let S be non empty ManySortedSign;
 cluster non empty Subsignature of S;
end;

definition
 let S be non void feasible ManySortedSign;
 cluster non void Subsignature of S;
end;

theorem :: INSTALG1:19
   for S being feasible ManySortedSign, S' being Subsignature of S
 for T being ManySortedSign, f,g being Function
  st f,g form_morphism_between S,T
  holds f|the carrier of S', g|the OperSymbols of S' form_morphism_between S',T
;

theorem :: INSTALG1:20
   for S being ManySortedSign, T being feasible ManySortedSign
 for T' being Subsignature of T, f,g being Function
  st f,g form_morphism_between S,T'
  holds f,g form_morphism_between S,T;

theorem :: INSTALG1:21
   for S being ManySortedSign, T being feasible ManySortedSign
 for T' being Subsignature of T, f,g being Function
  st f,g form_morphism_between S,T & rng f c= the carrier of T' &
     rng g c= the OperSymbols of T'
  holds f,g form_morphism_between S,T';

begin :: Signature reduct

definition
 let S1,S2 be non empty ManySortedSign;
 let A be MSAlgebra over S2;
 let f,g be Function such that
   f,g form_morphism_between S1,S2;
 func A|(S1,f,g) -> strict MSAlgebra over S1 means
:: INSTALG1:def 3

  the Sorts of it = (the Sorts of A)*f &
  the Charact of it = (the Charact of A)*g;
end;

definition
 let S2,S1 be non empty ManySortedSign;
 let A be MSAlgebra over S2;
 func A|S1 -> strict MSAlgebra over S1 equals
:: INSTALG1:def 4

   A|(S1, id the carrier of S1, id the OperSymbols of S1);
end;

theorem :: INSTALG1:22
   for S1,S2 being non empty ManySortedSign
 for A,B being MSAlgebra over S2 st the MSAlgebra of A = the MSAlgebra of B
 for f,g being Function st f,g form_morphism_between S1,S2
  holds A|(S1,f,g) = B|(S1,f,g);

theorem :: INSTALG1:23
 for S1,S2 being non empty ManySortedSign
 for A being non-empty MSAlgebra over S2
 for f,g being Function st f,g form_morphism_between S1,S2
  holds A|(S1,f,g) is non-empty;

definition
 let S2 be non empty ManySortedSign;
 let S1 be non empty Subsignature of S2;
 let A be non-empty MSAlgebra over S2;
 cluster A|S1 -> non-empty;
end;

theorem :: INSTALG1:24
 for S1,S2 being non void non empty ManySortedSign
 for f,g being Function st f,g form_morphism_between S1,S2
 for A being MSAlgebra over S2
 for o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1
  holds Den(o1,A|(S1,f,g)) = Den(o2,A);

theorem :: INSTALG1:25
 for S1,S2 being non void non empty ManySortedSign
 for f,g being Function st f,g form_morphism_between S1,S2
 for A being MSAlgebra over S2
 for o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1
  holds Args(o2,A) = Args(o1,A|(S1,f,g)) & Result(o1,A|(S1,f,g)) = Result(o2,A)
;

theorem :: INSTALG1:26
 for S being non empty ManySortedSign
 for A being MSAlgebra over S holds
  A|(S, id the carrier of S, id the OperSymbols of S) = the MSAlgebra of A;

theorem :: INSTALG1:27
   for S being non empty ManySortedSign
 for A being MSAlgebra over S holds A|S = the MSAlgebra of A;

theorem :: INSTALG1:28
 for S1,S2,S3 being non empty ManySortedSign
 for f1,g1 being Function st f1,g1 form_morphism_between S1,S2
 for f2,g2 being Function st f2,g2 form_morphism_between S2,S3
 for A being MSAlgebra over S3
  holds A|(S1,f2*f1,g2*g1) = (A|(S2,f2,g2))|(S1,f1,g1);

theorem :: INSTALG1:29
   for S1 being non empty feasible ManySortedSign
 for S2 being non empty Subsignature of S1
 for S3 being non empty Subsignature of S2
 for A being MSAlgebra over S1 holds A|S3 = (A|S2)|S3;

theorem :: INSTALG1:30
 for S1,S2 being non empty ManySortedSign
 for f being Function of the carrier of S1, the carrier of S2
 for g being Function st f,g form_morphism_between S1,S2
 for A1,A2 being MSAlgebra over S2
 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds
  h*f is ManySortedFunction of
    the Sorts of A1|(S1,f,g), the Sorts of A2|(S1,f,g);

theorem :: INSTALG1:31
   for S1 being non empty ManySortedSign
 for S2 being non empty Subsignature of S1
 for A1,A2 being MSAlgebra over S1
 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds
  h|the carrier of S2 is
   ManySortedFunction of the Sorts of A1|S2, the Sorts of A2|S2;

theorem :: INSTALG1:32
 for S1,S2 being non empty ManySortedSign
 for f,g being Function st f,g form_morphism_between S1,S2
 for A being MSAlgebra over S2 holds
  (id the Sorts of A)*f = id the Sorts of A|(S1,f,g);


theorem :: INSTALG1:33
   for S1 being non empty ManySortedSign
 for S2 being non empty Subsignature of S1
 for A being MSAlgebra over S1 holds
  (id the Sorts of A)|the carrier of S2 = id the Sorts of A|S2;

theorem :: INSTALG1:34
 for S1,S2 being non void non empty ManySortedSign
 for f,g being Function st f,g form_morphism_between S1,S2
 for A,B being MSAlgebra over S2
 for h2 being ManySortedFunction of A,B
 for h1 being ManySortedFunction of A|(S1,f,g),B|(S1,f,g) st h1 = h2*f
 for o1 being OperSymbol of S1, o2 being OperSymbol of S2
  st o2 = g.o1 & Args(o2,A) <> {} & Args(o2,B) <> {}
 for x2 being Element of Args(o2,A)
 for x1 being Element of Args(o1,A|(S1,f,g))
  st x2 = x1
  holds h1#x1 = h2#x2;

theorem :: INSTALG1:35
 for S,S' being non empty non void ManySortedSign
 for A1,A2 being MSAlgebra over S st
   the Sorts of A1 is_transformable_to the Sorts of A2
 for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2
 for f being Function of the carrier of S', the carrier of S
 for g being Function st f,g form_morphism_between S',S
 ex h' being ManySortedFunction of A1|(S',f,g), A2|(S',f,g) st
  h' = h*f & h' is_homomorphism A1|(S',f,g), A2|(S',f,g);

theorem :: INSTALG1:36
   for S being non void feasible ManySortedSign
 for S' being non void Subsignature of S
 for A1,A2 being MSAlgebra over S st
   the Sorts of A1 is_transformable_to the Sorts of A2
 for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2
 ex h' being ManySortedFunction of A1|S', A2|S' st
  h' = h|the carrier of S' & h' is_homomorphism A1|S', A2|S';

theorem :: INSTALG1:37
 for S,S' being non empty non void ManySortedSign
 for A being non-empty MSAlgebra over S
 for f being Function of the carrier of S', the carrier of S
 for g being Function st f,g form_morphism_between S',S
 for B being non-empty MSAlgebra over S' st B = A|(S',f,g)
 for s1,s2 being SortSymbol of S', t being Function
  st t is_e.translation_of B, s1, s2
  holds t is_e.translation_of A, f.s1, f.s2;

theorem :: INSTALG1:38
   for S,S' being non empty non void ManySortedSign
 for f being Function of the carrier of S', the carrier of S
 for g being Function st f,g form_morphism_between S',S
 for s1,s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2
  holds TranslationRel S reduces f.s1, f.s2;

theorem :: INSTALG1:39
   for S,S' being non void non empty ManySortedSign
 for A being non-empty MSAlgebra over S
 for f being Function of the carrier of S', the carrier of S
 for g being Function st f,g form_morphism_between S',S
 for B being non-empty MSAlgebra over S' st B = A|(S',f,g)
 for s1,s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2
 for t being Translation of B, s1, s2 holds
     t is Translation of A, f.s1, f.s2;

begin :: Translating homomorphism

scheme GenFuncEx{S() -> non empty non void ManySortedSign,
  A() -> non-empty MSAlgebra over S(),
  X() -> non-empty ManySortedSet of the carrier of S(),
  F(set,set) -> set}:
 ex h being ManySortedFunction of FreeMSA X(), A() st
  h is_homomorphism FreeMSA X(), A() &
  for s being SortSymbol of S() for x being Element of X().s holds
    h.s.root-tree [x,s] = F(x,s)
 provided
  for s being SortSymbol of S() for x being Element of X().s holds
   F(x,s) in (the Sorts of A()).s;

theorem :: INSTALG1:40
 for I being set, A,B being ManySortedSet of I
 for C being ManySortedSubset of A
 for F being ManySortedFunction of A,B
 for i being set st i in I
 for f,g being Function st f = F.i & g = (F||C).i
 for x being set st x in C.i holds g.x = f.x;

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

definition
 let S1,S2 be non empty non void ManySortedSign;
 let X be non-empty ManySortedSet of the carrier of S2;
 let f be Function of the carrier of S1, the carrier of S2;
 let g be Function such that
   f,g form_morphism_between S1,S2;
 func hom(f,g,X,S1,S2) ->
      ManySortedFunction of FreeMSA(X*f), (FreeMSA X)|(S1,f,g) means
:: INSTALG1:def 5

  it is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) &
  for s being SortSymbol of S1, x being Element of (X*f).s holds
   it.s.root-tree [x,s] = root-tree [x,f.s];
end;

theorem :: INSTALG1:41
 for S1,S2 being non void non empty ManySortedSign
 for X being non-empty ManySortedSet of the carrier of S2
 for f being Function of the carrier of S1, the carrier of S2
 for g being Function st f,g form_morphism_between S1,S2
 for o being OperSymbol of S1, p being Element of Args(o,FreeMSA(X*f))
 for q being FinSequence st q = hom(f,g,X,S1,S2)#p
  holds
   (hom(f,g,X,S1,S2).the_result_sort_of o).([o,the carrier of S1]-tree p) =
    [g.o,the carrier of S2]-tree q;

theorem :: INSTALG1:42
 for S1,S2 being non void non empty ManySortedSign
 for X being non-empty ManySortedSet of the carrier of S2
 for f being Function of the carrier of S1, the carrier of S2
 for g being Function st f,g form_morphism_between S1,S2
 for t being Term of S1, X*f holds
  (hom(f,g,X,S1,S2).the_sort_of t).t is CompoundTerm of S2, X iff
  t is CompoundTerm of S1, X*f;

theorem :: INSTALG1:43
   for S1,S2 being non void non empty ManySortedSign
 for X being non-empty ManySortedSet of the carrier of S2
 for f being Function of the carrier of S1, the carrier of S2
 for g being one-to-one Function st f,g form_morphism_between S1,S2
  holds hom(f,g,X,S1,S2) is_monomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g);

theorem :: INSTALG1:44
   for S being non void non empty ManySortedSign
 for X being non-empty ManySortedSet of the carrier of S holds
  hom(id the carrier of S, id the OperSymbols of S, X, S, S)
   = id the Sorts of FreeMSA X;

theorem :: INSTALG1:45
   for S1,S2,S3 being non void non empty ManySortedSign
 for X being non-empty ManySortedSet of the carrier of S3
 for f1 being Function of the carrier of S1, the carrier of S2
 for g1 being Function st f1,g1 form_morphism_between S1,S2
 for f2 being Function of the carrier of S2, the carrier of S3
 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
  hom(f2*f1,g2*g1,X,S1,S3) = (hom(f2,g2,X,S2,S3)*f1)**hom(f1,g1,X*f2,S1,S2);