:: Inverse Limits of Many Sorted Algebras
::  by Adam Grabowski
::
:: 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, ORDERS_2, SUBSET_1, STRUCT_0, MSUALG_1, PRALG_2,
      FUNCT_1, RELAT_1, CARD_3, RLVECT_2, PBOOLE, XXREAL_0, MEMBER_1, MSUALG_3,
      FUNCOP_1, RELAT_2, MCART_1, MSUALG_2, TARSKI, UNIALG_2, MARGREL1,
      FUNCT_6, FINSEQ_1, FUNCT_2, COMPLEX1, PARTFUN1, FINSEQ_4, NAT_1, FUNCT_5,
      NATTRA_1, PUA2MSS1, ZFMISC_1, MSALIMIT;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XTUPLE_0, MCART_1,
      RELAT_1, FUNCT_1, STRUCT_0, RELAT_2, FUNCT_2, FINSEQ_1, FINSEQ_2,
      ORDERS_2, FUNCOP_1, RELSET_1, PARTFUN1, CARD_3, BINOP_1, FUNCT_5,
      FUNCT_6, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, PRALG_2,
      PUA2MSS1, ORDERS_3;
 constructors PRALG_1, PRALG_2, MSUALG_3, PUA2MSS1, ORDERS_3, RELSET_1,
      FUNCT_5, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE,
      STRUCT_0, ORDERS_2, MSUALG_1, MSUALG_2, PRALG_2, MSUALG_3, ORDERS_3,
      PRALG_3, ORDINAL1, CARD_3, RELSET_1, FINSEQ_1;
 requirements SUBSET, BOOLE;


begin :: Inverse Limits of Many Sorted Algebras

reserve P for non empty Poset,
  i, j, k for Element of P;
reserve S for non void non empty ManySortedSign;

registration
  let I be non empty set, S;
  let AF be MSAlgebra-Family of I,S;
  let i be Element of I;
  let o be OperSymbol of S;
  cluster ((OPER AF).i).o -> Function-like Relation-like;
end;

registration
  let I be non empty set, S;
  let AF be MSAlgebra-Family of I,S;
  let s be SortSymbol of S;
  cluster (SORTS AF).s -> functional;
end;

definition
  let P, S;
  mode OrderedAlgFam of P,S -> MSAlgebra-Family of the carrier of P,S means
:: MSALIMIT:def 1

     ex
 F be ManySortedFunction of the InternalRel of P st for i,j,k st i >= j
& j >= k ex f1 be ManySortedFunction of it.i, it.j, f2 be ManySortedFunction of
    it.j, it.k st f1 = F.(j,i) & f2 = F.(k,j) & F.(k,i) = f2 ** f1 & f1
    is_homomorphism it.i, it.j;
end;

reserve OAF for OrderedAlgFam of P, S;

definition
  let P, S, OAF;
  mode Binding of OAF -> ManySortedFunction of the InternalRel of P means
:: MSALIMIT:def 2

     for
 i,j,k st i >= j & j >= k ex f1 be ManySortedFunction of OAF.i, OAF.j,
f2 be ManySortedFunction of OAF.j, OAF.k st f1 = it.(j,i) & f2 = it.(k,j) & it.
    (k,i) = f2 ** f1 & f1 is_homomorphism OAF.i, OAF.j;
end;

definition
  let P, S, OAF;
  let B be Binding of OAF, i,j;
  assume
 i >= j;
  func bind (B,i,j) -> ManySortedFunction of OAF.i, OAF.j equals
:: MSALIMIT:def 3

  B.(j,i
  );
end;

reserve B for Binding of OAF;

theorem :: MSALIMIT:1
  i >= j & j >= k implies bind (B,j,k) ** bind (B,i,j) = bind (B,i, k);

definition
  let P, S, OAF;
  let IT be Binding of OAF;
  attr IT is normalized means
:: MSALIMIT:def 4

  for i holds IT.(i,i) = id (the Sorts of OAF.i);
end;

theorem :: MSALIMIT:2
  for P,S,OAF,B,i,j st i >= j for f be ManySortedFunction of OAF.i,
  OAF.j st f = bind (B,i,j) holds f is_homomorphism OAF.i,OAF.j;

definition
  let P, S, OAF, B;
  func Normalized B -> Binding of OAF means
:: MSALIMIT:def 5

  for i, j st i >= j holds it
.(j,i) = IFEQ (j, i, id (the Sorts of OAF.i), bind (B,i,j) ** id (the Sorts of
  OAF.i) );
end;

theorem :: MSALIMIT:3
  for i, j st i >= j & i <> j holds B.(j,i) = (Normalized B).(j,i);

registration
  let P, S, OAF, B;
  cluster Normalized B -> normalized;
end;

registration
  let P, S, OAF;
  cluster normalized for Binding of OAF;
end;

theorem :: MSALIMIT:4
  for NB be normalized Binding of OAF for i, j st i >= j holds (
  Normalized NB).(j,i) = NB.(j,i);

definition
  let P, S, OAF;
  let B be Binding of OAF;
  func InvLim B -> strict MSSubAlgebra of product OAF means
:: MSALIMIT:def 6

  for s be
SortSymbol of S for f be Element of (SORTS OAF).s holds f in (the Sorts of it).
  s iff for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f.j;
end;

theorem :: MSALIMIT:5
  for DP be discrete non empty Poset, S for OAF be OrderedAlgFam of DP,S
  for B be normalized Binding of OAF holds InvLim B = product OAF;

begin  :: Sets and Morphisms of Many Sorted Signatures

reserve x for set,
  A for non empty set;

definition
  let X be set;
  attr X is MSS-membered means
:: MSALIMIT:def 7

  x in X implies x is strict non empty non void ManySortedSign;
end;

registration
  cluster non empty MSS-membered for set;
end;

registration
  cluster strict empty void for ManySortedSign;
end;

theorem :: MSALIMIT:6
  for S be void ManySortedSign holds id the carrier of S, id the
  carrier' of S form_morphism_between S,S;

definition
::$CD
  let A;
  func MSS_set A -> set means
:: MSALIMIT:def 9

  for x being object holds x in it iff ex S be strict non empty non void
  ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A;
end;

registration
  let A;
  cluster MSS_set A -> non empty MSS-membered;
end;

definition
  let A be non empty MSS-membered set;
  redefine mode Element of A -> strict non empty non void ManySortedSign;
end;

definition
  let S1,S2 be ManySortedSign;
  func MSS_morph (S1,S2) -> set means
:: MSALIMIT:def 10
  x in it iff ex f,g be Function st x = [f,g] & f
  ,g form_morphism_between S1,S2;
end;