:: On the Category of Posets
::  by Adam Grabowski
::
:: Received January 22, 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 ORDERS_2, NATTRA_1, RELAT_1, STRUCT_0, XBOOLE_0, ORDERS_1,
      SUBSET_1, WELLORD1, RELAT_2, XXREAL_0, TARSKI, ZFMISC_1, FUNCT_1, SEQM_3,
      FUNCT_2, CAT_5, CAT_1, ALTCAT_1, PBOOLE, FUNCOP_1, BINOP_1, ORDERS_3,
      MONOID_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDERS_1,
      CAT_5, XTUPLE_0, MCART_1, WELLORD1, MULTOP_1, PBOOLE, RELSET_1, PARTFUN1,
      FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1, STRUCT_0, ORDERS_2, CAT_1, ENS_1,
      ALTCAT_1;
 constructors RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_2, ENS_1, CAT_5,
      ALTCAT_1, MULTOP_1, PBOOLE, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      STRUCT_0, ORDERS_2, ENS_1, CAT_5, ALTCAT_1;
 requirements BOOLE, SUBSET;


begin :: Preliminaries

definition
  let IT be RelStr;
  attr IT is discrete means
:: ORDERS_3:def 1

  the InternalRel of IT = id (the carrier of IT);
end;

registration
  cluster strict discrete non empty for Poset;
end;

registration
  cluster RelStr (#{},id {}#) -> empty;
  let P be empty RelStr;
  cluster the InternalRel of P -> empty;
end;

registration
  cluster empty -> discrete for RelStr;
end;

definition
  let P be RelStr;
  let IT be Subset of P;
  attr IT is disconnected means
:: ORDERS_3:def 2

  ex A,B be Subset of P st A <> {} & B <>
  {} & IT = A \/ B & A misses B & the InternalRel of P = (the InternalRel of P)
  |_2 A \/ (the InternalRel of P) |_2 B;
end;

notation
  let P be RelStr;
  let IT be Subset of P;
  antonym IT is connected for IT is disconnected;
end;

definition
  let IT be RelStr;
  attr IT is disconnected means
:: ORDERS_3:def 3

  [#] IT is disconnected;
end;

notation
  let IT be RelStr;
  antonym IT is connected for IT is disconnected;
end;

reserve T for non empty RelStr,
  a for Element of T;

theorem :: ORDERS_3:1
  for DP be discrete non empty RelStr, x,y be Element of DP holds x <= y
  iff x = y;

theorem :: ORDERS_3:2
  for R be Relation, a be set st R is Order of {a} holds R = id {a};

theorem :: ORDERS_3:3
  T is reflexive & [#] T = {a} implies T is discrete;

reserve a for set;

theorem :: ORDERS_3:4
  [#] T = {a} implies T is connected;

theorem :: ORDERS_3:5
  for DP be discrete non empty Poset st (ex a,b be Element of DP st
  a <> b) holds DP is disconnected;

registration
  cluster strict connected for non empty Poset;
  cluster strict disconnected discrete for non empty Poset;
end;

begin  :: Category of Posets

definition
  let IT be set;
  attr IT is POSet_set-like means
:: ORDERS_3:def 4

  for a be set st a in IT holds a is non empty Poset;
end;

registration
  cluster non empty POSet_set-like for set;
end;

definition
  mode POSet_set is POSet_set-like set;
end;

definition
  let P be non empty POSet_set;
  redefine mode Element of P -> non empty Poset;
end;

definition
  let L1,L2 be RelStr;
  let f be Function of L1, L2;
  attr f is monotone means
:: ORDERS_3:def 5

  for x,y being Element of L1 st x <= y for a,
  b being Element of L2 st a = f.x & b = f.y holds a <= b;
end;

reserve P for non empty POSet_set,
  A,B for Element of P;

definition
  let A,B be RelStr;
  func MonFuncs (A,B) -> set means
:: ORDERS_3:def 6

  a in it iff ex f be Function of A, B st a =
  f & f in Funcs (the carrier of A, the carrier of B) & f is monotone;
end;

theorem :: ORDERS_3:6
  for A,B,C be non empty RelStr for f,g be Function st f in
  MonFuncs (A,B) & g in MonFuncs (B,C) holds (g*f) in MonFuncs (A,C);

theorem :: ORDERS_3:7
  id the carrier of T in MonFuncs (T,T);

registration
  let T;
  cluster MonFuncs (T,T) -> non empty;
end;

definition
  let X be set;
  func Carr X -> set means
:: ORDERS_3:def 7

  a in it iff ex s be 1-sorted st s in X & a = the carrier of s;
end;

registration
  let P;
  cluster Carr P -> non empty;
end;

theorem :: ORDERS_3:8
  for f be 1-sorted holds Carr {f} = {the carrier of f};

theorem :: ORDERS_3:9
  for f,g be 1-sorted holds Carr {f,g} = {the carrier of f, the carrier of g };

theorem :: ORDERS_3:10
  MonFuncs (A,B) c= Funcs Carr P;

theorem :: ORDERS_3:11
  for A,B be RelStr holds MonFuncs (A,B) c= Funcs (the carrier of
  A,the carrier of B);

registration
  let A,B be non empty Poset;
  cluster MonFuncs (A,B) -> functional;
end;

definition
  let P be non empty POSet_set;
  func POSCat P -> strict with_triple-like_morphisms Category means
:: ORDERS_3:def 8
  the
carrier of it = P & (for a,b be Element of P, f be Element of Funcs Carr P st f
in MonFuncs (a,b) holds [[a,b],f] is Morphism of it) & (for m be Morphism of it
ex a,b be Element of P, f be Element of Funcs (Carr P) st m = [[a,b],f] & f in
MonFuncs (a,b)) & for m1,m2 be (Morphism of it), a1,a2,a3 be Element of P, f1,
f2 be Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
  m2(*)m1 = [[a1,a3], f2*f1];
end;

begin   :: Alternative Category of Posets

scheme :: ORDERS_3:sch 1
  AltCatEx {A() -> non empty set, F(object,object) -> functional set }:
ex C be
strict AltCatStr st the carrier of C = A() & for i,j be Element of A() holds (
the Arrows of C).(i,j) = F (i,j) & for i,j,k be Element of A() holds (the Comp
  of C).(i,j,k) = FuncComp ( F(i,j) , F(j,k) )
provided
 for i,j,k be Element of A() for f,g be Function st f in F(i,j) & g
in F(j,k) holds g * f in F (i,k);

scheme :: ORDERS_3:sch 2
  AltCatUniq {A() -> non empty set, F(object,object) -> functional set } :
for C1,C2
  be strict AltCatStr st ( the carrier of C1 = A() & for i,j be Element of A()
holds (the Arrows of C1).(i,j) = F (i,j) & for i,j,k be Element of A() holds (
the Comp of C1).(i,j,k) = FuncComp ( F(i,j) , F(j,k) ) ) & ( the carrier of C2
  = A() & for i,j be Element of A() holds (the Arrows of C2).(i,j) = F (i,j) &
for i,j,k be Element of A() holds (the Comp of C2).(i,j,k) = FuncComp ( F(i,j)
  , F(j,k) ) ) holds C1 = C2;

definition
  let P be non empty POSet_set;
  func POSAltCat P -> strict AltCatStr means
:: ORDERS_3:def 9

  the carrier of it = P &
for i,j be Element of P holds (the Arrows of it).(i,j) = MonFuncs (i,j) & for i
,j,k be Element of P holds (the Comp of it).(i,j,k) = FuncComp ( MonFuncs (i,j)
  , MonFuncs (j,k) );
end;

registration
  let P be non empty POSet_set;
  cluster POSAltCat P -> transitive non empty;
end;

registration
  let P be non empty POSet_set;
  cluster POSAltCat P -> associative with_units;
end;

theorem :: ORDERS_3:12
  for o1,o2 be Object of POSAltCat P, A,B be Element of P st o1 = A & o2
  = B holds <^ o1, o2 ^> c= Funcs (the carrier of A, the carrier of B);