OSALG_4: Order Sorted Quotient Algebra

:: Order Sorted Quotient Algebra
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2011 Association of Mizar Users

begin

registration

let R be non empty Poset;
cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding order-sorted set ;
existence

proof end;

end;

definition

let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
let IT be ManySortedRelation of A,B;
attr IT is os-compatible means :Def1: :: OSALG_4:def 1
for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in IT . s1 iff [x,y] in IT . s2 );

end;

:: deftheorem Def1 defines os-compatible OSALG_4:def 1 :

registration

let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding os-compatible ManySortedRelation of A,B;
existence

proof end;

end;

definition

let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;

end;

theorem Th1: :: OSALG_4:1

for R being non empty Poset
for A, B being ManySortedSet of the carrier of R
for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R

proof end;

registration

let R be non empty Poset;
let A, B be ManySortedSet of R;
cluster os-compatible -> order-sorted ManySortedRelation of A,B;
coherence by Th1;

end;

definition

let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A is OrderSortedRelation of A,A;

end;

definition

let S be OrderSortedSign;
let U1 be OSAlgebra of S;
canceled;
mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means :Def3: :: OSALG_4:def 3
it is os-compatible ;
existence

proof end;

end;

:: deftheorem OSALG_4:def 2 :

:: deftheorem Def3 defines OrderSortedRelation OSALG_4:def 3 :

registration

let S be OrderSortedSign;
let U1 be OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like OrderSortedRelation of U1;
existence

proof end;

end;

registration

let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;
existence

proof end;

end;

definition

let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
mode OSCongruence of U1 is MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;

end;

definition

let R be non empty Poset;
func Path_Rel R -> Equivalence_Relation of the carrier of R means :Def4: :: OSALG_4:def 4
for x, y being set holds
( [x,y] in it iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Path_Rel OSALG_4:def 4 :

theorem Th2: :: OSALG_4:2

for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R

proof end;

definition

let R be non empty Poset;
let s1, s2 be Element of R;
pred s1 ~= s2 means :Def5: :: OSALG_4:def 5
[s1,s2] in Path_Rel R;
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def5 defines ~= OSALG_4:def 5 :

theorem :: OSALG_4:3

for R being non empty Poset
for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds
s1 ~= s3

proof end;

definition

let R be non empty Poset;
func Components R -> non empty Subset-Family of R equals :: OSALG_4:def 6
Class (Path_Rel R);
coherence ;

end;

:: deftheorem defines Components OSALG_4:def 6 :

registration

let R be non empty Poset;
cluster -> non empty Element of Components R;
coherence

proof end;

end;

definition

let R be non empty Poset;
mode Component of R is Element of Components R;

end;

definition

let R be non empty Poset;
let s1 be Element of R;
canceled;
func CComp s1 -> Component of R equals :: OSALG_4:def 8
Class ((Path_Rel R),s1);
correctness by EQREL_1:def 5;

end;

:: deftheorem OSALG_4:def 7 :

:: deftheorem defines CComp OSALG_4:def 8 :

theorem :: OSALG_4:4

canceled;

theorem Th5: :: OSALG_4:5

for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2

proof end;

definition

let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
let C be Component of R;
func A -carrier_of C -> set equals :: OSALG_4:def 9
union { (A . s) where s is Element of R : s in C } ;
correctness ;

end;

:: deftheorem defines -carrier_of OSALG_4:def 9 :

theorem Th6: :: OSALG_4:6

for R being non empty Poset
for A being ManySortedSet of the carrier of R
for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)

proof end;

definition

let R be non empty Poset;
attr R is locally_directed means :Def10: :: OSALG_4:def 10
for C being Component of R holds C is directed ;

end;

:: deftheorem Def10 defines locally_directed OSALG_4:def 10 :

theorem Th7: :: OSALG_4:7

for R being non empty discrete Poset
for x, y being Element of R st [x,y] in Path_Rel R holds
x = y

proof end;

theorem Th8: :: OSALG_4:8

for R being non empty discrete Poset
for C being Component of R ex x being Element of R st C = {x}

proof end;

theorem Th9: :: OSALG_4:9

for R being non empty discrete Poset holds R is locally_directed

proof end;

registration

cluster non empty reflexive transitive antisymmetric locally_directed RelStr ;
existence

proof end;

end;

registration

cluster non empty non void reflexive transitive antisymmetric order-sorted discernable locally_directed OverloadedRSSign ;
existence

proof end;

end;

registration

cluster non empty reflexive transitive antisymmetric discrete -> non empty locally_directed RelStr ;
coherence by Th9;

end;

registration

let S be non empty locally_directed Poset;
cluster -> directed Element of Components S;
coherence by Def10;

end;

theorem Th10: :: OSALG_4:10

{} is Equivalence_Relation of {} by RELSET_1:25;

definition

let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let C be Component of S;
func CompClass (E,C) -> Equivalence_Relation of ( the Sorts of A -carrier_of C) means :Def11: :: OSALG_4:def 11
for x, y being set holds
( [x,y] in it iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines CompClass OSALG_4:def 11 :

definition

let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
func OSClass (E,s1) -> Subset of (Class (CompClass (E,(CComp s1)))) means :Def12: :: OSALG_4:def 12
for z being set holds
( z in it iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines OSClass OSALG_4:def 12 :

registration

let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
cluster OSClass (E,s1) -> non empty ;
coherence

proof end;

end;

theorem Th11: :: OSALG_4:11

for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)

proof end;

definition

let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
func OSClass E -> OrderSortedSet of S means :Def13: :: OSALG_4:def 13
for s1 being Element of S holds it . s1 = OSClass (E,s1);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines OSClass OSALG_4:def 13 :

registration

let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
cluster OSClass E -> V17() ;
coherence

proof end;

end;

definition

let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of U1;
let s be Element of S;
let x be Element of the Sorts of U1 . s;
func OSClass (E,x) -> Element of OSClass (E,s) equals :: OSALG_4:def 14
Class ((CompClass (E,(CComp s))),x);
correctness by Def12;

end;

:: deftheorem defines OSClass OSALG_4:def 14 :

theorem :: OSALG_4:12

for R being non empty locally_directed Poset
for x, y being Element of R st ex z being Element of R st
( z <= x & z <= y ) holds
ex u being Element of R st
( x <= u & y <= u )

proof end;

theorem Th13: :: OSALG_4:13

for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )

proof end;

theorem :: OSALG_4:14

for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s1, s2 being Element of S
for x being Element of the Sorts of U1 . s1 st s1 <= s2 holds
for y being Element of the Sorts of U1 . s2 st y = x holds
OSClass (E,x) = OSClass (E,y) by Th5;

begin

definition

let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
let x be Element of Args (o,A);
func R #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means :Def15: :: OSALG_4:def 15
for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & it . n = OSClass (R,y) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines #_os OSALG_4:def 15 :

definition

let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes (R,o) -> Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def16: :: OSALG_4:def 16
for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass (R,x);
existence

proof end;

uniqueness

proof end;

func OSQuotArgs (R,o) -> Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) means :: OSALG_4:def 17
for x being Element of Args (o,A) holds it . x = R #_os x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines OSQuotRes OSALG_4:def 16 :

:: deftheorem defines OSQuotArgs OSALG_4:def 17 :

definition

let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes R -> ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S means :: OSALG_4:def 18
for o being OperSymbol of S holds it . o = OSQuotRes (R,o);
existence

proof end;

uniqueness

proof end;

func OSQuotArgs R -> ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S means :: OSALG_4:def 19
for o being OperSymbol of S holds it . o = OSQuotArgs (R,o);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines OSQuotRes OSALG_4:def 18 :

:: deftheorem defines OSQuotArgs OSALG_4:def 19 :

theorem Th15: :: OSALG_4:15

for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a

proof end;

definition

let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact (R,o) -> Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def20: :: OSALG_4:def 20
for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
it . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines OSQuotCharact OSALG_4:def 20 :

definition

let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact R -> ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S means :Def21: :: OSALG_4:def 21
for o being OperSymbol of S holds it . o = OSQuotCharact (R,o);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines OSQuotCharact OSALG_4:def 21 :

definition

let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func QuotOSAlg (U1,R) -> OSAlgebra of S equals :: OSALG_4:def 22
MSAlgebra(# (OSClass R),(OSQuotCharact R) #);
coherence by OSALG_1:17;

end;

:: deftheorem defines QuotOSAlg OSALG_4:def 22 :

registration

let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
cluster QuotOSAlg (U1,R) -> strict non-empty ;
coherence by MSUALG_1:def 8;

end;

definition

let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
let s be Element of S;
func OSNat_Hom (U1,R,s) -> Function of ( the Sorts of U1 . s),(OSClass (R,s)) means :Def23: :: OSALG_4:def 23
for x being Element of the Sorts of U1 . s holds it . x = OSClass (R,x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines OSNat_Hom OSALG_4:def 23 :

definition

let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func OSNat_Hom (U1,R) -> ManySortedFunction of U1,(QuotOSAlg (U1,R)) means :Def24: :: OSALG_4:def 24
for s being Element of S holds it . s = OSNat_Hom (U1,R,s);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines OSNat_Hom OSALG_4:def 24 :

theorem :: OSALG_4:16

for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )

proof end;

theorem Th17: :: OSALG_4:17

for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
MSCng F is OSCongruence of U1

proof end;

definition

let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
assume A1: ( F is_homomorphism U1,U2 & F is order-sorted ) ;
func OSCng F -> OSCongruence of U1 equals :Def25: :: OSALG_4:def 25
MSCng F;
correctness by A1, Th17;

end;

:: deftheorem Def25 defines OSCng OSALG_4:def 25 :

definition

let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let s be Element of S;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ;
func OSHomQuot (F,s) -> Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) means :Def26: :: OSALG_4:def 26
for x being Element of the Sorts of U1 . s holds it . (OSClass ((OSCng F),x)) = (F . s) . x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def26 defines OSHomQuot OSALG_4:def 26 :

definition

let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
func OSHomQuot F -> ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 means :Def27: :: OSALG_4:def 27
for s being Element of S holds it . s = OSHomQuot (F,s);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines OSHomQuot OSALG_4:def 27 :

theorem Th18: :: OSALG_4:18

proof end;

theorem Th19: :: OSALG_4:19

for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2

proof end;

theorem :: OSALG_4:20

proof end;

definition

let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be MSEquivalence-like OrderSortedRelation of U1;
attr R is monotone means :Def28: :: OSALG_4:def 28
for o1, o2 being OperSymbol of S st o1 <= o2 holds
for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2);

end;

:: deftheorem Def28 defines monotone OSALG_4:def 28 :

theorem Th21: :: OSALG_4:21

for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1

proof end;

theorem Th22: :: OSALG_4:22

for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds
R is monotone

proof end;

registration

proof end;

end;

registration

proof end;

end;

theorem Th23: :: OSALG_4:23

for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like

proof end;

registration

let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster MSEquivalence-like monotone -> MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;
coherence by Th23;

end;

theorem Th24: :: OSALG_4:24

for S being OrderSortedSign
for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone

proof end;

registration

let S be OrderSortedSign;
let U1 be non-empty monotone OSAlgebra of S;
cluster MSEquivalence-like MSCongruence-like -> monotone OrderSortedRelation of U1;
coherence by Th24;

end;

registration

let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be monotone OSCongruence of U1;
cluster QuotOSAlg (U1,R) -> monotone ;
coherence

proof end;

end;

theorem :: OSALG_4:25

canceled;

theorem :: OSALG_4:26

for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone

proof end;

definition

let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
let s be Element of S;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted and
A3: R c= OSCng F ;
func OSHomQuot (F,R,s) -> Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) means :Def29: :: OSALG_4:def 29
for x being Element of the Sorts of U1 . s holds it . (OSClass (R,x)) = (F . s) . x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines OSHomQuot OSALG_4:def 29 :

definition

let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
func OSHomQuot (F,R) -> ManySortedFunction of (QuotOSAlg (U1,R)),U2 means :Def30: :: OSALG_4:def 30
for s being Element of S holds it . s = OSHomQuot (F,R,s);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def30 defines OSHomQuot OSALG_4:def 30 :

theorem :: OSALG_4:27

for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )

proof end;