The abstract of the Mizar article:

Closure Operators and Subalgebras

by

Grzegorz Bancerek

Received January 15, 1997

MML identifier: WAYBEL10

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, CAT_1, YELLOW_0, RELAT_1, WELLORD1, BOOLE, OPPCAT_1,
      FUNCOP_1, WAYBEL_3, RELAT_2, SEQM_3, PRE_TOPC, FUNCT_1, WAYBEL_1,
      BINOP_1, GROUP_6, WAYBEL_0, ORDINAL2, YELLOW_1, FUNCT_2, GROUP_1, CARD_3,
      RLVECT_2, BHSP_3, UNIALG_2, LATTICE3, LATTICES, SUBSET_1, QUANTAL1,
      WAYBEL10;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
      PARTFUN1, FUNCT_2, CARD_3, STRUCT_0, QUANTAL1, PRE_TOPC, PRALG_1,
      PRE_CIRC, BORSUK_1, WELLORD1, ORDERS_1, LATTICE3, GRCAT_1, ORDERS_3,
      YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_7;
 constructors PRE_CIRC, TOLER_1, BORSUK_1, QUANTAL1, GRCAT_1, ORDERS_3,
      WAYBEL_1, WAYBEL_3;
 clusters STRUCT_0, RELSET_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
      WAYBEL_1, WAYBEL_3, SUBSET_1, FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

scheme SubrelstrEx {L() -> non empty RelStr, P[set], a() -> set}:
 ex S being non empty full strict SubRelStr of L() st
  for x being Element of L() holds x is Element of S iff P[x]
 provided
    P[a()] and
    a() in the carrier of L();

scheme RelstrEq {L1, L2() -> non empty RelStr, P[set], Q[set,set]}:
 the RelStr of L1() = the RelStr of L2()
  provided
  for x being set holds x is Element of L1() iff P[x] and
  for x being set holds x is Element of L2() iff P[x] and
  for a,b being Element of L1() holds a <= b iff Q[a,b] and
  for a,b being Element of L2() holds a <= b iff Q[a,b];

scheme SubrelstrEq1 {L() -> non empty RelStr,
                    S1, S2() -> non empty full SubRelStr of L(), P[set]}:
 the RelStr of S1() = the RelStr of S2()
  provided
  for x being set holds x is Element of S1() iff P[x] and
  for x being set holds x is Element of S2() iff P[x];

scheme SubrelstrEq2 {L() -> non empty RelStr,
                    S1, S2() -> non empty full SubRelStr of L(), P[set]}:
 the RelStr of S1() = the RelStr of S2()
  provided
  for x being Element of L() holds x is Element of S1() iff P[x] and
  for x being Element of L() holds x is Element of S2() iff P[x];

theorem :: WAYBEL10:1
 for R,Q being Relation holds
   (R c= Q iff R~ c= Q~) & (R~ c= Q iff R c= Q~);

canceled;

theorem :: WAYBEL10:3
 for L,S being RelStr holds
   (S is SubRelStr of L iff S opp is SubRelStr of L opp) &
   (S opp is SubRelStr of L iff S is SubRelStr of L opp);

theorem :: WAYBEL10:4
 for L,S being RelStr holds
   (S is full SubRelStr of L iff S opp is full SubRelStr of L opp) &
   (S opp is full SubRelStr of L iff S is full SubRelStr of L opp);

definition
 let L be RelStr, S be full SubRelStr of L;
 redefine func S opp -> strict full SubRelStr of L opp;
end;

definition
 let X be set, L be non empty RelStr;
 cluster X --> L -> non-Empty;
end;

definition
 let S be RelStr, T be non empty reflexive RelStr;
 cluster monotone map of S,T;
end;

definition
 let L be non empty RelStr;
 cluster projection -> monotone idempotent map of L,L;
end;

definition
 let S,T be non empty reflexive RelStr;
 let f be monotone map of S,T;
 cluster corestr f -> monotone;
end;

definition
 let L be 1-sorted;
 cluster id L -> one-to-one;
end;

definition
 let L be non empty reflexive RelStr;
 cluster id L -> sups-preserving infs-preserving;
end;

theorem :: WAYBEL10:5
   for L being RelStr, S being Subset of L
  holds id S is map of subrelstr S, L &
   for f being map of subrelstr S, L st f = id S holds f is monotone;

definition
 let L be non empty reflexive RelStr;
 cluster sups-preserving infs-preserving closure kernel one-to-one map of L,L;
end;

theorem :: WAYBEL10:6
 for L being non empty reflexive RelStr, c being closure map of L,L
 for x being Element of L holds c.x >= x;

definition
 let S,T be 1-sorted;
 let f be Function of the carrier of S, the carrier of T;
 let R be 1-sorted such that
   the carrier of R c= the carrier of S;
 func f|R -> map of R,T equals
:: WAYBEL10:def 1

   f|the carrier of R;
end;

theorem :: WAYBEL10:7
 for S,T being RelStr, R being SubRelStr of S
 for f being Function of the carrier of S, the carrier of T
  holds f|R = f|the carrier of R &
   for x being set st x in the carrier of R holds (f|R).x = f.x;

theorem :: WAYBEL10:8
 for S,T being RelStr, f being map of S,T st f is one-to-one
 for R being SubRelStr of S holds f|R is one-to-one;

definition
 let S,T be non empty reflexive RelStr;
 let f be monotone map of S,T;
 let R be SubRelStr of S;
 cluster f|R -> monotone;
end;

theorem :: WAYBEL10:9
 for S,T being non empty RelStr, R being non empty SubRelStr of S
 for f being map of S,T, g being map of T,S st f is one-to-one & g = f"
  holds g|Image (f|R) is map of Image (f|R), R & g|Image (f|R) = (f|R)";

begin :: The lattice of closure operators

definition
 let S be RelStr, T be non empty reflexive RelStr;
 cluster MonMaps(S,T) -> non empty;
end;

theorem :: WAYBEL10:10
 for S being RelStr, T being non empty reflexive RelStr, x being set holds
   x is Element of MonMaps(S,T) iff x is monotone map of S,T;

definition
 let L be non empty reflexive RelStr;
 func ClOpers L -> non empty full strict SubRelStr of MonMaps(L,L) means
:: WAYBEL10:def 2

  for f being map of L,L holds f is Element of it iff f is closure;
end;

theorem :: WAYBEL10:11
 for L being non empty reflexive RelStr, x being set holds
   x is Element of ClOpers L iff x is closure map of L,L;

theorem :: WAYBEL10:12
 for X being set, L being non empty RelStr
 for f,g being Function of X, the carrier of L
 for x,y being Element of L|^X st x = f & y = g
  holds x <= y iff f <= g;

theorem :: WAYBEL10:13
 for L being complete LATTICE
 for c1,c2 being map of L,L for x,y being Element of ClOpers L
  st x = c1 & y = c2 holds x <= y iff c1 <= c2;

theorem :: WAYBEL10:14
 for L being reflexive RelStr, S1, S2 being full SubRelStr of L
  st the carrier of S1 c= the carrier of S2
  holds S1 is SubRelStr of S2;

theorem :: WAYBEL10:15
 for L being complete LATTICE
 for c1,c2 being closure map of L,L holds
  c1 <= c2 iff Image c2 is SubRelStr of Image c1;

begin :: The lattice of closure systems

definition
 let L be RelStr;
 func Sub L -> strict non empty RelStr means
:: WAYBEL10:def 3

  (for x being set holds x is Element of it iff x is strict SubRelStr of L) &
  for a,b being Element of it holds a <= b iff
   ex R being RelStr st b = R & a is SubRelStr of R;
end;

theorem :: WAYBEL10:16
 for L,R being RelStr
 for x,y being Element of Sub L st y = R holds
   x <= y iff x is SubRelStr of R;

definition
 let L be RelStr;
 cluster Sub L -> reflexive antisymmetric transitive;
end;

definition
 let L be RelStr;
 cluster Sub L -> complete;
end;

definition
 let L be complete LATTICE;
 cluster infs-inheriting -> non empty SubRelStr of L;
 cluster sups-inheriting -> non empty SubRelStr of L;
end;

definition
 let L be RelStr;
 mode System of L is full SubRelStr of L;
end;

definition
 let L be non empty RelStr;
 let S be System of L;
 redefine attr S is infs-inheriting;
 synonym S is closure;
end;

definition
 let L be non empty RelStr;
 cluster subrelstr [#]L -> infs-inheriting sups-inheriting;
end;

definition
 let L be non empty RelStr;
 func ClosureSystems L -> full strict non empty SubRelStr of Sub L means
:: WAYBEL10:def 4

  for R being strict SubRelStr of L holds
   R is Element of it iff R is infs-inheriting full;
end;

theorem :: WAYBEL10:17
 for L being non empty RelStr, x being set holds
   x is Element of ClosureSystems L iff x is strict closure System of L;

theorem :: WAYBEL10:18
 for L being non empty RelStr, R being RelStr
 for x,y being Element of ClosureSystems L st y = R holds
  x <= y iff x is SubRelStr of R;

begin :: Isomorphism between closure operators and closure systems

definition
 let L be non empty Poset;
 let h be closure map of L,L;
 cluster Image h -> infs-inheriting;
end;

definition
 let L be non empty Poset;
 func ClImageMap L -> map of ClOpers L, (ClosureSystems L) opp means
:: WAYBEL10:def 5

  for c being closure map of L,L holds it.c = Image c;
end;

definition
 let L be non empty RelStr;
 let S be SubRelStr of L;
 func closure_op S -> map of L,L means
:: WAYBEL10:def 6

  for x being Element of L holds it.x = "/\"((uparrow x) /\
 the carrier of S,L);
end;

definition
 let L be complete LATTICE;
 let S be closure System of L;
 cluster closure_op S -> closure;
end;

theorem :: WAYBEL10:19
 for L being complete LATTICE
 for S being closure System of L holds
  Image closure_op S = the RelStr of S;

theorem :: WAYBEL10:20
 for L being complete LATTICE
 for c being closure map of L,L holds closure_op Image c = c;

definition
 let L be complete LATTICE;
 cluster ClImageMap L -> one-to-one;
end;

theorem :: WAYBEL10:21
 for L being complete LATTICE holds
  (ClImageMap L)" is map of (ClosureSystems L) opp, ClOpers L;

theorem :: WAYBEL10:22
 for L being complete LATTICE
 for S being strict closure System of L holds
   (ClImageMap L)".S = closure_op S;

definition
 let L be complete LATTICE;
 cluster ClImageMap L -> isomorphic;
end;

theorem :: WAYBEL10:23
   for L being complete LATTICE holds
  ClOpers L, (ClosureSystems L) opp are_isomorphic;

begin :: Isomorphism between closure operators preserving directed sups
      :: and subalgebras

theorem :: WAYBEL10:24
 for L being RelStr, S being full SubRelStr of L
 for X being Subset of S holds
   (X is directed Subset of L implies X is directed) &
   (X is filtered Subset of L implies X is filtered);

:: Corollary 3.14, p. 24
theorem :: WAYBEL10:25
 for L being complete LATTICE
 for S being closure System of L holds
   closure_op S is directed-sups-preserving
  iff
   S is directed-sups-inheriting;

theorem :: WAYBEL10:26
   for L being complete LATTICE
 for h being closure map of L,L holds
   h is directed-sups-preserving
  iff
   Image h is directed-sups-inheriting;

definition
 let L be complete LATTICE;
 let S be directed-sups-inheriting closure System of L;
 cluster closure_op S -> directed-sups-preserving;
end;

definition
 let L be complete LATTICE;
 let h be directed-sups-preserving closure map of L,L;
 cluster Image h -> directed-sups-inheriting;
end;

definition
 let L be non empty reflexive RelStr;
 func DsupClOpers L -> non empty full strict SubRelStr of ClOpers L means
:: WAYBEL10:def 7

  for f being closure map of L,L holds
    f is Element of it iff f is directed-sups-preserving;
end;

theorem :: WAYBEL10:27
 for L being non empty reflexive RelStr, x being set holds
   x is Element of DsupClOpers L iff
   x is directed-sups-preserving closure map of L,L;

definition
 let L be non empty RelStr;
 func Subalgebras L -> full strict non empty SubRelStr of ClosureSystems L
 means
:: WAYBEL10:def 8

  for R being strict closure System of L holds
   R is Element of it iff R is directed-sups-inheriting;
end;

theorem :: WAYBEL10:28
 for L being non empty RelStr, x being set holds
   x is Element of Subalgebras L iff
   x is strict directed-sups-inheriting closure System of L;

theorem :: WAYBEL10:29
 for L being complete LATTICE holds
  Image ((ClImageMap L)|DsupClOpers L) = (Subalgebras L) opp;

definition
 let L be complete LATTICE;
 cluster corestr ((ClImageMap L)|DsupClOpers L) -> isomorphic;
end;

theorem :: WAYBEL10:30
   for L being complete LATTICE holds
  DsupClOpers L, (Subalgebras L) opp are_isomorphic;