The abstract of the Mizar article:

Subalgebras of the Universal Algebra. Lattices of Subalgebras

by

Ewa Burakowska

Received July 8, 1993

MML identifier: UNIALG_2

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_2, BOOLE, UNIALG_1, FUNCT_2, PARTFUN1, RELAT_1, FINSEQ_1,
      FUNCOP_1, CQC_SIM1, FUNCT_1, FINSEQ_4, TARSKI, ZF_REFLE, SETFAM_1,
      SUBSET_1, LATTICES, BINOP_1, UNIALG_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, STRUCT_0, RELAT_1,
      FUNCT_1, FINSEQ_1, SETFAM_1, FUNCOP_1, PARTFUN1, FINSEQ_2, LATTICES,
      BINOP_1, UNIALG_1;
 constructors FINSEQ_2, DOMAIN_1, FUNCOP_1, LATTICES, BINOP_1, UNIALG_1,
      MEMBERED, XBOOLE_0;
 clusters SUBSET_1, LATTICES, UNIALG_1, RELSET_1, STRUCT_0, FINSEQ_2, RLSUB_2,
      PARTFUN1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET;


begin

theorem :: UNIALG_2:1
for n be Nat, D be non empty set, D1 be non empty Subset of D holds
  n-tuples_on D /\ n-tuples_on D1 = n-tuples_on D1;

theorem :: UNIALG_2:2
for D being non empty set
for h being homogeneous quasi_total non empty PartFunc of D*,D holds
dom h = (arity(h))-tuples_on D;

reserve U0,U1,U2,U3 for Universal_Algebra,
        n,i for Nat,
        x,y for set;

definition let D be non empty set;
mode PFuncsDomHQN of D -> non empty set means
:: UNIALG_2:def 1
for x be Element of it holds
  x is homogeneous quasi_total non empty PartFunc of D*,D;
end;

definition
let D be non empty set, P be PFuncsDomHQN of D;
redefine
 mode Element of P -> homogeneous quasi_total non empty PartFunc of D*,D;
end;

definition let U1;
mode PFuncsDomHQN of U1 is PFuncsDomHQN of (the carrier of U1);
end;

definition let U1 be UAStr;
mode PartFunc of U1 is PartFunc of (the carrier of U1)*,the carrier of U1;
end;

definition let U1,U2;
 pred U1,U2 are_similar means
:: UNIALG_2:def 2
 signature (U1) = signature (U2);
  symmetry;
  reflexivity;
end;

theorem :: UNIALG_2:3
  U1,U2 are_similar implies len the charact of(U1) = len the charact of(U2);

theorem :: UNIALG_2:4
  U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar;

theorem :: UNIALG_2:5
rng the charact of(U0) is non empty Subset of
 PFuncs((the carrier of U0)*,the carrier of U0);

definition let U0;
func Operations(U0) -> PFuncsDomHQN of U0 equals
:: UNIALG_2:def 3
  rng the charact of(U0);
end;

definition let U1;
  mode operation of U1 is Element of Operations(U1);
end;

reserve A for non empty Subset of U0,
        o for operation of U0,
        x1,y1 for FinSequence of A;

theorem :: UNIALG_2:6
for n being set st n in dom the charact of U0
 holds (the charact of U0).n is operation of U0;

definition let U0 be Universal_Algebra,
                A be Subset of U0,
                o be operation of U0;
pred A is_closed_on o means
:: UNIALG_2:def 4
 for s being FinSequence of A st len s = arity o holds o.s in A;
end;

definition let U0 be Universal_Algebra,
                A be Subset of U0;
attr A is opers_closed means
:: UNIALG_2:def 5
for o be operation of U0 holds A is_closed_on o;
end;

definition let U0,A,o;
assume  A is_closed_on o;
func o/.A ->homogeneous quasi_total non empty PartFunc of A*,A equals
:: UNIALG_2:def 6
 o|((arity o)-tuples_on A);
end;

definition let U0,A;
func Opers(U0,A) -> PFuncFinSequence of A means
:: UNIALG_2:def 7
dom it = dom the charact of(U0) &
for n being set,o st n in dom it & o =(the charact of(U0)).n holds it.n = o/.A;
end;

theorem :: UNIALG_2:7
for B being non empty Subset of U0 st B=the carrier of U0 holds
 B is opers_closed & (for o holds o/.B = o);

theorem :: UNIALG_2:8
  for U1 be Universal_Algebra, A be non empty Subset of U1,
    o be operation of U1
  st A is_closed_on o holds arity (o/.A) = arity o;

definition let U0;
mode SubAlgebra of U0 -> Universal_Algebra means
:: UNIALG_2:def 8
the carrier of it is Subset of U0 &
for B be non empty Subset of U0 st B=the carrier of it holds
the charact of(it) = Opers(U0,B) & B is opers_closed;
end;

definition let U0 be Universal_Algebra;
cluster strict SubAlgebra of U0;
end;

theorem :: UNIALG_2:9
for U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be operation of U1,
 n be Nat
 st U0 is SubAlgebra of U1 & n in dom the charact of(U0) &
  o0 = (the charact of(U0)).n &
 o1 = (the charact of(U1)).n holds arity o0 = arity o1;

theorem :: UNIALG_2:10
U0 is SubAlgebra of U1 implies dom the charact of(U0)=dom the charact of(U1);

theorem :: UNIALG_2:11
  U0 is SubAlgebra of U0;

theorem :: UNIALG_2:12
  U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of
U2;

theorem :: UNIALG_2:13
U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2;

theorem :: UNIALG_2:14
for U1,U2 be SubAlgebra of U0 st the carrier of U1 c= the carrier of U2
  holds U1 is SubAlgebra of U2;

theorem :: UNIALG_2:15
for U1,U2 be strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2
  holds U1 = U2;

theorem :: UNIALG_2:16
  U1 is SubAlgebra of U2 implies U1,U2 are_similar;

theorem :: UNIALG_2:17
for A be non empty Subset of U0 holds
  UAStr (#A,Opers(U0,A)#) is strict Universal_Algebra;

definition let U0 be Universal_Algebra,
   A be non empty Subset of U0;
assume  A is opers_closed;
func UniAlgSetClosed(A) -> strict SubAlgebra of U0 equals
:: UNIALG_2:def 9
  UAStr (# A, Opers(U0,A) #);
end;

definition let U0; let U1,U2 be SubAlgebra of U0;
assume  the carrier of U1 meets the carrier of U2;
func U1 /\ U2 -> strict SubAlgebra of U0 means
:: UNIALG_2:def 10
 the carrier of it = (the carrier of U1) /\ (the carrier of U2) &
for B be non empty Subset of U0 st B=the carrier of it holds
the charact of(it) = Opers(U0,B) & B is opers_closed;
end;

definition let U0;
func Constants(U0) -> Subset of U0 equals
:: UNIALG_2:def 11
   { a where a is Element of U0:
        ex o be operation of U0 st arity o=0 & a in rng o};
end;

definition let IT be Universal_Algebra;
attr IT is with_const_op means
:: UNIALG_2:def 12
ex o being operation of IT st arity o=0;
end;

definition
cluster with_const_op strict Universal_Algebra;
end;

definition let U0 be with_const_op Universal_Algebra;
 cluster Constants(U0) -> non empty;
end;

theorem :: UNIALG_2:18
for U0 be Universal_Algebra, U1 be SubAlgebra of U0 holds
Constants(U0) is Subset of U1;

theorem :: UNIALG_2:19
 for U0 be with_const_op Universal_Algebra, U1 be SubAlgebra of U0 holds
Constants(U0) is non empty Subset of U1;

theorem :: UNIALG_2:20
for U0 be with_const_op Universal_Algebra,U1,U2 be SubAlgebra of U0 holds
 the carrier of U1 meets the carrier of U2;

definition let U0 be Universal_Algebra, A be Subset of U0;
assume  Constants(U0) <> {} or A <> {};
func GenUnivAlg(A) -> strict SubAlgebra of U0 means
:: UNIALG_2:def 13
A c= the carrier of it &
for U1 be SubAlgebra of U0 st A c= the carrier of U1 holds
  it is SubAlgebra of U1;
end;

theorem :: UNIALG_2:21
  for U0 be strict Universal_Algebra holds GenUnivAlg([#]
(the carrier of U0)) = U0;

theorem :: UNIALG_2:22
for U0 be Universal_Algebra, U1 be strict SubAlgebra of U0,
B be non empty Subset of U0 st B = the carrier of U1
 holds GenUnivAlg(B) = U1;

definition let U0 be Universal_Algebra,
               U1,U2 be SubAlgebra of U0;
func U1 "\/" U2 -> strict SubAlgebra of U0 means
:: UNIALG_2:def 14
 for A be non empty Subset of U0 st
  A = (the carrier of U1) \/ (the carrier of U2) holds it = GenUnivAlg(A);
end;

theorem :: UNIALG_2:23
for U0 be Universal_Algebra, U1 be SubAlgebra of U0,
    A,B be Subset of U0 st
(A <> {} or Constants(U0) <> {}) & B = A \/ the carrier of U1 holds
GenUnivAlg(A) "\/" U1 = GenUnivAlg(B);

theorem :: UNIALG_2:24
for U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0 holds
U1 "\/" U2 = U2 "\/" U1;

theorem :: UNIALG_2:25
for U0 be with_const_op Universal_Algebra,U1,U2 be strict SubAlgebra of U0
holds U1 /\ (U1"\/"U2) = U1;

theorem :: UNIALG_2:26
for U0 be with_const_op Universal_Algebra,U1,U2 be strict SubAlgebra of U0
holds (U1 /\ U2)"\/"U2 = U2;

definition let U0 be Universal_Algebra;
func Sub(U0) -> set means
:: UNIALG_2:def 15
for x holds x in it iff x is strict SubAlgebra of U0;
end;

definition let U0 be Universal_Algebra;
cluster Sub(U0) -> non empty;
end;

definition let U0 be Universal_Algebra;
func UniAlg_join(U0) -> BinOp of Sub(U0) means
:: UNIALG_2:def 16
for x,y be Element of Sub(U0) holds
  for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds
  it.(x,y) = U1 "\/" U2;
end;

definition let U0 be Universal_Algebra;
func UniAlg_meet(U0) -> BinOp of Sub(U0) means
:: UNIALG_2:def 17
for x,y be Element of Sub(U0) holds
  for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds
  it.(x,y) = U1 /\ U2;
end;

theorem :: UNIALG_2:27
UniAlg_join(U0) is commutative;

theorem :: UNIALG_2:28
UniAlg_join(U0) is associative;

theorem :: UNIALG_2:29
for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0) is commutative;

theorem :: UNIALG_2:30
for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0) is associative;

definition let U0 be with_const_op Universal_Algebra;
func UnSubAlLattice(U0) -> strict Lattice equals
:: UNIALG_2:def 18
    LattStr (# Sub(U0), UniAlg_join(U0), UniAlg_meet(U0) #);
end;