The abstract of the Mizar article:

Homomorphisms of Algebras. Quotient Universal Algebra

by

Malgorzata Korolkiewicz

Received October 12, 1993

MML identifier: ALG_1

[ Mizar article, MML identifier index ]

environ

 vocabulary UNIALG_1, UNIALG_2, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_4, BOOLE,
      CQC_SIM1, GROUP_6, WELLORD1, FINSEQ_2, EQREL_1, FUNCT_2, PARTFUN1,
      TARSKI, ZF_REFLE, RELAT_2, ALG_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, RELAT_1, RELAT_2, RELSET_1,
      FUNCT_1, STRUCT_0, FINSEQ_1, PARTFUN1, EQREL_1, FINSEQ_2, FUNCT_2,
      TOPREAL1, UNIALG_1, FINSEQOP, UNIALG_2;
 constructors RELAT_2, EQREL_1, UNIALG_2, FINSEQOP, MEMBERED, XBOOLE_0;
 clusters UNIALG_1, UNIALG_2, RELSET_1, STRUCT_0, FINSEQ_2, PARTFUN1, SUBSET_1,
      ARYTM_3, FILTER_1, MEMBERED, ZFMISC_1, FUNCT_1, FUNCT_2, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

reserve U1,U2,U3 for Universal_Algebra,
        n,m for Nat,
        o1 for operation of U1,
        o2 for operation of U2,
        o3 for operation of U3,
        x,y for set;

theorem :: ALG_1:1
for D1,D2 be non empty set, p be FinSequence of D1, f be Function of D1,D2
 holds dom(f*p) = dom p & len (f*p) = len p &
      for n st n in dom (f*p) holds (f*p).n = f.(p.n);

theorem :: ALG_1:2
for B be non empty Subset of U1 st B = the carrier of U1 holds
Opers(U1,B) = the charact of(U1);

definition
 let U1, U2 be 1-sorted;
mode Function of U1,U2 is Function of the carrier of U1,the carrier of U2;
end;

reserve a for FinSequence of U1,
        f for Function of U1,U2;

theorem :: ALG_1:3
  f*(<*>the carrier of U1) = <*>the carrier of U2;

theorem :: ALG_1:4
(id the carrier of U1)*a = a;

theorem :: ALG_1:5
for h1 be Function of U1,U2, h2 be Function of U2,U3,a be FinSequence of U1
  holds h2*(h1*a) = (h2 * h1)*a;

definition let U1,U2,f;
pred f is_homomorphism U1,U2 means
:: ALG_1:def 1
 U1,U2 are_similar &
 for n st n in dom the charact of(U1)
  for o1,o2 st o1=(the charact of U1).n & o2=(the charact of U2).n
   for x be FinSequence of U1 st x in dom o1 holds f.(o1.x) = o2.(f*x);
end;

definition let U1,U2,f;
pred f is_monomorphism U1,U2 means
:: ALG_1:def 2
 f is_homomorphism U1,U2 & f is one-to-one;
pred f is_epimorphism U1,U2 means
:: ALG_1:def 3
 f is_homomorphism U1,U2 & rng f = the carrier of U2;
end;

definition let U1,U2,f;
pred f is_isomorphism U1,U2 means
:: ALG_1:def 4
 f is_monomorphism U1,U2 & f is_epimorphism U1,U2;
end;

definition let U1,U2;
pred U1,U2 are_isomorphic means
:: ALG_1:def 5
 ex f st f is_isomorphism U1,U2;
end;

theorem :: ALG_1:6
id the carrier of U1 is_homomorphism U1,U1;

theorem :: ALG_1:7
for h1 be Function of U1,U2, h2 be Function of U2,U3 st
 h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
 h2 * h1 is_homomorphism U1,U3;

theorem :: ALG_1:8
f is_isomorphism U1,U2 iff
f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one;

theorem :: ALG_1:9
f is_isomorphism U1,U2 implies dom f = the carrier of U1 &
 rng f = the carrier of U2;

theorem :: ALG_1:10
 for h be Function of U1,U2, h1 be Function of U2,U1 st
 h is_isomorphism U1,U2 & h1=h" holds h1 is_homomorphism U2,U1;

theorem :: ALG_1:11
for h be Function of U1,U2, h1 be Function of U2,U1 st
h is_isomorphism U1,U2 & h1 = h" holds h1 is_isomorphism U2,U1;

theorem :: ALG_1:12
for h be Function of U1,U2, h1 be Function of U2,U3 st
h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3
holds h1 * h is_isomorphism U1,U3;

theorem :: ALG_1:13
  U1,U1 are_isomorphic;

theorem :: ALG_1:14
   U1,U2 are_isomorphic implies U2,U1 are_isomorphic;

theorem :: ALG_1:15
   U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic;

definition let U1,U2,f;
assume  f is_homomorphism U1,U2;
 func Image f -> strict SubAlgebra of U2 means
:: ALG_1:def 6
the carrier of it = f .: (the carrier of U1);
end;

theorem :: ALG_1:16
  for h be Function of U1,U2 st h is_homomorphism U1,U2 holds
rng h = the carrier of Image h;

theorem :: ALG_1:17
   for U2 being strict Universal_Algebra, f be Function of U1,U2
 st f is_homomorphism U1,U2 holds f is_epimorphism U1,U2 iff Image f = U2;

begin
::
:: Quotient Universal Algebra
::

definition let U1 be 1-sorted;
mode Relation of U1 is Relation of the carrier of U1;
mode Equivalence_Relation of U1 is Equivalence_Relation of the carrier of U1;
 canceled 2;
end;

definition let D be non empty set,
               R be Relation of D;
func ExtendRel(R) -> Relation of D* means
:: ALG_1:def 9
 for x,y be FinSequence of D holds
  [x,y] in it iff len x = len y & for n st n in dom x holds [x.n,y.n] in R;
end;

theorem :: ALG_1:18
for D be non empty set holds ExtendRel(id D) = id (D*);

definition let U1;
mode Congruence of U1 -> Equivalence_Relation of U1 means
:: ALG_1:def 10
 for n,o1 st n in dom the charact of(U1) & o1 = (the charact of U1).n
   for x,y be FinSequence of U1 st x in dom o1 & y in dom o1 &
   [x,y] in ExtendRel(it) holds [o1.x,o1.y] in it;
end;

reserve E for Congruence of U1;

definition let D be non empty set,
               R be Equivalence_Relation of D;
           let y be FinSequence of Class(R),
               x be FinSequence of D;
pred x is_representatives_FS y means
:: ALG_1:def 11
 len x = len y &
 for n st n in dom x holds Class(R,x.n) = y.n;
end;

theorem :: ALG_1:19
for D be non empty set, R be Equivalence_Relation of D,
    y be FinSequence of Class(R)
 ex x be FinSequence of D st x is_representatives_FS y;

definition let U1 be Universal_Algebra,
               E be Congruence of U1,
               o be operation of U1;
func QuotOp(o,E) -> homogeneous quasi_total non empty
       PartFunc of (Class E)*,(Class E) means
:: ALG_1:def 12
 dom it = (arity o)-tuples_on (Class E) &
 for y be FinSequence of (Class E) st y in dom it
  for x be FinSequence of the carrier of U1 st x is_representatives_FS y
    holds it.y = Class(E,o.x);
end;

definition let U1,E;
func QuotOpSeq(U1,E) -> PFuncFinSequence of Class E means
:: ALG_1:def 13
 len it = len the charact of(U1) &
 for n st n in dom it
  for o1 st (the charact of(U1)).n = o1 holds it.n = QuotOp(o1,E);
end;

theorem :: ALG_1:20
for U1,E holds
   UAStr (# Class(E),QuotOpSeq(U1,E) #) is strict Universal_Algebra;

definition let U1,E;
func QuotUnivAlg(U1,E) -> strict Universal_Algebra equals
:: ALG_1:def 14
  UAStr (# Class(E),QuotOpSeq(U1,E) #);
end;

definition let U1,E;
func Nat_Hom(U1,E) -> Function of U1,QuotUnivAlg(U1,E) means
:: ALG_1:def 15
 for u be Element of U1 holds it.u = Class(E,u);
end;

theorem :: ALG_1:21
for U1,E holds Nat_Hom(U1,E) is_homomorphism U1,QuotUnivAlg(U1,E);

theorem :: ALG_1:22
   for U1,E holds Nat_Hom(U1,E) is_epimorphism U1,QuotUnivAlg(U1,E);

definition let U1,U2;let f be Function of U1,U2;
 assume  f is_homomorphism U1,U2;
 func Cng(f) -> Congruence of U1 means
:: ALG_1:def 16
  for a,b be Element of U1 holds [a,b] in it iff f.a = f.b;
end;

definition
 let U1,U2 be Universal_Algebra,
     f be Function of U1,U2;
 assume  f is_homomorphism U1,U2;
func HomQuot(f) -> Function of QuotUnivAlg(U1,Cng(f)),U2 means
:: ALG_1:def 17
for a be Element of U1 holds it.(Class(Cng f,a)) = f.a;
end;

theorem :: ALG_1:23
f is_homomorphism U1,U2 implies
HomQuot(f) is_homomorphism QuotUnivAlg(U1,Cng(f)),U2 &
HomQuot(f) is_monomorphism QuotUnivAlg(U1,Cng(f)),U2;

theorem :: ALG_1:24
f is_epimorphism U1,U2 implies HomQuot(f)
   is_isomorphism QuotUnivAlg(U1,Cng(f)),U2;

theorem :: ALG_1:25
  f is_epimorphism U1,U2 implies QuotUnivAlg(U1,Cng(f)),U2 are_isomorphic;