:: Lattice of Congruences in a Many Sorted Algebra
::  by Robert Milewski
::
:: Received January 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 NUMBERS, PBOOLE, RELAT_1, EQREL_1, TARSKI, XBOOLE_0, STRUCT_0,
      LATTICES, FUNCT_1, SUBSET_1, BINOP_1, MSUALG_4, ZFMISC_1, CARD_3,
      MSUALG_1, FINSEQ_1, MARGREL1, PARTFUN1, ARYTM_3, ORDINAL4, NAT_1,
      XXREAL_0, CARD_1, RELAT_2, ARYTM_1, NAT_LAT, REALSET1, XXREAL_2,
      MSUALG_5, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
      REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, FINSEQ_2, STRUCT_0, PARTFUN1,
      FUNCT_2, RELSET_1, EQREL_1, BINOP_1, PBOOLE, MSUALG_1, MSUALG_3,
      MSUALG_4, LATTICES, NAT_LAT, CARD_3, FINSEQ_1, NAT_1, XXREAL_0;
 constructors BINOP_1, XXREAL_0, NAT_1, NAT_D, EQREL_1, REALSET1, NAT_LAT,
      MSUALG_3, MSUALG_4, RELSET_1, PRALG_2, FUNCOP_1, FINSEQ_2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1,
      EQREL_1, PBOOLE, STRUCT_0, LATTICES, NAT_LAT, PRALG_1, MSUALG_1,
      MSUALG_3, MSUALG_4, ORDINAL1, CARD_1, RELAT_2;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

::                MORE  OF  EQUIVALENCE  RELATIONS

reserve I,X,x,d,i for set;
reserve M for ManySortedSet of I;

reserve EqR1,EqR2 for Equivalence_Relation of X;

definition
  let X be set, R be Relation of X;
  func EqCl R -> Equivalence_Relation of X means
:: MSUALG_5:def 1

  R c= it & for EqR2 be
  Equivalence_Relation of X st R c= EqR2 holds it c= EqR2;
end;

theorem :: MSUALG_5:1
  EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2);

theorem :: MSUALG_5:2
  EqCl EqR1 = EqR1;

begin

::               LATTICE  OF  EQUIVALENCE  RELATIONS             ::

definition
  let X be set;
  func EqRelLatt X -> strict Lattice means
:: MSUALG_5:def 2
  the carrier of it = {x where x is
  Relation of X,X : x is Equivalence_Relation of X} & for x,y being
Equivalence_Relation of X holds (the L_meet of it).(x,y) = x /\ y & (the L_join
  of it).(x,y) = x "\/" y;
end;

begin

::              MANY  SORTED  EQUIVALENCE  RELATIONS             ::

registration
  let I,M;
  cluster MSEquivalence_Relation-like for ManySortedRelation of M;
end;

definition
  let I,M;
  mode Equivalence_Relation of M is MSEquivalence_Relation-like
    ManySortedRelation of M;
end;

reserve I for non empty set;
reserve M for ManySortedSet of I;
reserve EqR,EqR1,EqR2,EqR3,EqR4 for Equivalence_Relation of M;

definition
  let I be non empty set;
  let M be ManySortedSet of I, R be ManySortedRelation of M;
  func EqCl R -> Equivalence_Relation of M means
:: MSUALG_5:def 3

  for i being Element of I holds it.i = EqCl(R.i);
end;

theorem :: MSUALG_5:3
  EqCl EqR = EqR;

begin

::       LATTICE  OF  MANY  SORTED  EQUIVALENCE  RELATIONS       ::

definition
  let I be non empty set, M be ManySortedSet of I;
  let EqR1,EqR2 be Equivalence_Relation of M;
  func EqR1 "\/" EqR2 -> Equivalence_Relation of M means
:: MSUALG_5:def 4

  ex EqR3 being
  ManySortedRelation of M st EqR3 = EqR1 (\/) EqR2 & it = EqCl EqR3;
  commutativity;
end;

theorem :: MSUALG_5:4
  EqR1 (\/) EqR2 c= EqR1 "\/" EqR2;

theorem :: MSUALG_5:5
  for EqR be Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds
  EqR1 "\/" EqR2 c= EqR;

theorem :: MSUALG_5:6
  ( EqR1 (\/) EqR2 c= EqR3 & for EqR be Equivalence_Relation of M st
  EqR1 (\/) EqR2 c= EqR holds EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2;

theorem :: MSUALG_5:7
  EqR "\/" EqR = EqR;

theorem :: MSUALG_5:8
  (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3);

theorem :: MSUALG_5:9
  EqR1 (/\) (EqR1 "\/" EqR2) = EqR1;

theorem :: MSUALG_5:10
  for EqR be Equivalence_Relation of M st EqR = EqR1 (/\) EqR2 holds
  EqR1 "\/" EqR = EqR1;

theorem :: MSUALG_5:11
  for EqR1,EqR2 be Equivalence_Relation of M holds EqR1 (/\) EqR2 is
  Equivalence_Relation of M;

definition
  let I be non empty set;
  let M be ManySortedSet of I;
  func EqRelLatt M -> strict Lattice means
:: MSUALG_5:def 5

  (for x being set holds x in
  the carrier of it iff x is Equivalence_Relation of M) &
  for x,y being Equivalence_Relation of M
    holds (the L_meet of it).(x,y) = x (/\) y &
          (the L_join of it).(x,y) = x "\/" y;
end;

begin

::    LATTICE  OF  CONGRUENCES  IN  A  MANY  SORTED  ALGEBRA     ::

registration
  let S be non empty ManySortedSign;
  let A be MSAlgebra over S;
  cluster MSEquivalence-like -> MSEquivalence_Relation-like for
ManySortedRelation
    of A;
end;

reserve S for non void non empty ManySortedSign;
reserve A for non-empty MSAlgebra over S;

theorem :: MSUALG_5:12
  for o be OperSymbol of S for C1,C2 being MSCongruence of A for
x1,y1 be set for a1,b1 be FinSequence holds [x1,y1] in C1.((the_arity_of o)/.(
len a1 + 1)) \/ C2.((the_arity_of o)/.(len a1 + 1)) implies for x,y be Element
of Args(o,A) st x = (a1 ^ <*x1*> ^ b1) & y = (a1 ^ <*y1*> ^ b1) holds [Den(o,A)
  .x,Den(o,A).y] in C1.(the_result_sort_of o) \/ C2.(the_result_sort_of o);

theorem :: MSUALG_5:13
  for o be OperSymbol of S for C1,C2 being MSCongruence of A for C
being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2
 for x1,y1 be object
 for n be Element of NAT for a1,a2,b1 being FinSequence st len a1 = n & len
a1 = len a2 & for k be Element of NAT st k in dom a1 holds [a1.k,a2.k] in C.((
the_arity_of o)/.k) holds ( [Den(o,A).(a1 ^ <*x1*> ^ b1),Den(o,A).(a2 ^ <*x1*>
  ^ b1)] in C.(the_result_sort_of o) & [x1,y1] in C.((the_arity_of o)/.(n+1))
implies for x be Element of Args(o,A) st x = a1 ^ <*x1*> ^ b1 holds [Den(o,A).x
  ,Den(o,A).(a2 ^ <*y1*> ^ b1)] in C.(the_result_sort_of o));

theorem :: MSUALG_5:14
  for o be OperSymbol of S for C1,C2 being MSCongruence of A for C
  being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 for x,y be
Element of Args(o,A) holds (( for n be Nat st n in dom x holds [x.n,y.n] in C.(
(the_arity_of o)/.n)) implies [Den(o,A).x,Den(o,A).y] in C.(the_result_sort_of
  o));

theorem :: MSUALG_5:15
  for C1,C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A;

theorem :: MSUALG_5:16
  for C1,C2 being MSCongruence of A holds C1 (/\) C2 is MSCongruence of A;

definition
  let S;
  let A be non-empty MSAlgebra over S;
  func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means
:: MSUALG_5:def 6

   for
 x being set holds x in the carrier of it iff x is MSCongruence of A;
end;

theorem :: MSUALG_5:17
  id (the Sorts of A) is MSCongruence of A;

theorem :: MSUALG_5:18
  [|the Sorts of A,the Sorts of A|] is MSCongruence of A;

registration
  let S, A;
  cluster CongrLatt A -> bounded;
end;

theorem :: MSUALG_5:19
  Bottom CongrLatt A = id (the Sorts of A);

theorem :: MSUALG_5:20
  Top CongrLatt A = [|the Sorts of A,the Sorts of A|];

:: from MSUALG_7, 2010.02.21, A.T

theorem :: MSUALG_5:21
  for X be set holds x in the carrier of EqRelLatt X iff x is
  Equivalence_Relation of X;