MSUALG_3: Homomorphisms of Many Sorted Algebras

definition

let I be non empty set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
let i be Element of I;
:: original: .
redefine func F . i -> Function of (A . i),(B . i);
coherence by PBOOLE:def 15;

end;

definition

let S be non empty ManySortedSign ;
let U1, U2 be MSAlgebra over S;
mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2;

end;

definition

let I be set ;
let A be ManySortedSet of I;

func id A -> ManySortedFunction of A,A means :Def1: :: MSUALG_3:def 1
for i being set st i in I holds
it . i = id (A . i);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines id MSUALG_3:def 1 :

definition

let IT be Function;

attr IT is "1-1" means :Def2: :: MSUALG_3:def 2
for i being set
for f being Function st i in dom IT & IT . i = f holds
f is one-to-one ;

end;

:: deftheorem Def2 defines "1-1" MSUALG_3:def 2 :

registration

let I be set ;

cluster Relation-like I -defined Function-like total V41() V42() "1-1" for set ;

existence

proof end;

end;

theorem Th1: :: MSUALG_3:1

for I being set
for F being ManySortedFunction of I holds
( F is "1-1" iff for i being set st i in I holds
F . i is one-to-one )

proof end;

definition

let I be set ;
let A, B be ManySortedSet of I;
let IT be ManySortedFunction of A,B;

attr IT is "onto" means :Def3: :: MSUALG_3:def 3
for i being set st i in I holds
rng (IT . i) = B . i;

end;

:: deftheorem Def3 defines "onto" MSUALG_3:def 3 :

theorem Th2: :: MSUALG_3:2

for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )

proof end;

definition

let I be set ;
let A be ManySortedSet of I;
let B, C be V2() ManySortedSet of I;
let F be ManySortedFunction of A,B;
let G be ManySortedFunction of B,C;
:: original: **
redefine func G ** F -> ManySortedFunction of A,C;
coherence

proof end;

end;

theorem :: MSUALG_3:3

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds F ** (id A) = F

proof end;

theorem Th4: :: MSUALG_3:4

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds (id B) ** F = F

proof end;

definition

let I be set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
assume that
A1: F is "1-1" and
A2: F is "onto" ;

func F "" -> ManySortedFunction of B,A means :Def4: :: MSUALG_3:def 4
for i being set st i in I holds
it . i = (F . i) " ;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines "" MSUALG_3:def 4 :

theorem Th5: :: MSUALG_3:5

for I being set
for A, B being V2() ManySortedSet of I
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )

proof end;

registration

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let o be OperSymbol of S;

cluster Args (o,U1) -> functional ;

coherence

proof end;

end;

theorem Th6: :: MSUALG_3:6

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let o be OperSymbol of S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args (o,U1);
assume that
A1: Args (o,U1) <> {} and
A2: Args (o,U2) <> {} ;

func F # x -> Element of Args (o,U2) equals :Def5: :: MSUALG_3:def 5
(Frege (F * (the_arity_of o))) . x;

coherence

proof end;

correctness ;

end;

:: deftheorem Def5 defines # MSUALG_3:def 5 :

Lm1: now :: thesis:

let S be non empty non void ManySortedSign ; :: thesis:
let U1, U2 be MSAlgebra over S; :: thesis:
let o be OperSymbol of S; :: thesis:
let F be ManySortedFunction of U1,U2; :: thesis:
let x be Element of Args (o,U1); :: thesis:
let f, u be Function; :: thesis:
assume that
A1: x = f and
A2: x in Args (o,U1) and
A3: u in Args (o,U2) ; :: thesis:
A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then A5: rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def 2;
A6: F # x = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5;
A7: dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let e be set ; :: thesis:
A8: (F * (the_arity_of o)) . e is Function ;
assume A9: e in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis:
then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11;
then (the_arity_of o) . e in the carrier of S by PARTFUN1:def 2;
then A10: (the_arity_of o) . e in dom F by PARTFUN1:def 2;
e in dom (the_arity_of o) by A9, FUNCT_1:11;
then e in dom (F * (the_arity_of o)) by A10, FUNCT_1:11;
hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A8, FUNCT_6:19; :: thesis:

end;

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; :: thesis:
then e in dom (F * (the_arity_of o)) by FUNCT_6:19;
then A11: e in dom (the_arity_of o) by FUNCT_1:11;
then reconsider f = e as Element of NAT ;
(the_arity_of o) . f in the carrier of S by A11, FINSEQ_2:11;
then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def 2;
hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A11, FUNCT_1:11; :: thesis:

end;

A12: Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3;
then A13: dom u = dom ( the Sorts of U2 * (the_arity_of o)) by A3, CARD_3:9;
A14: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A15: dom f = dom ( the Sorts of U1 * (the_arity_of o)) by A1, A2, CARD_3:9
.= dom (the_arity_of o) by A5, RELAT_1:27 ;
rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def 2;
then A16: dom u = dom (the_arity_of o) by A13, RELAT_1:27;

now :: thesis:

let e be set ; :: thesis:
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; :: thesis:
then e in dom (F * (the_arity_of o)) by FUNCT_6:19;
then A17: e in dom (the_arity_of o) by FUNCT_1:11;
then reconsider Foe = F . ((the_arity_of o) . e) as Function of ( the Sorts of U1 . ((the_arity_of o) . e)),( the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:11, PBOOLE:def 15;
( the Sorts of U2 * (the_arity_of o)) . e in rng ( the Sorts of U2 * (the_arity_of o)) by A13, A16, A17, FUNCT_1:def 3;
then A18: ( the Sorts of U2 * (the_arity_of o)) . e <> {} by A3, A12, CARD_3:26;
( ( the Sorts of U1 * (the_arity_of o)) . e = the Sorts of U1 . ((the_arity_of o) . e) & ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) ) by A17, FUNCT_1:13;
hence ( the Sorts of U1 * (the_arity_of o)) . e = dom Foe by A18, FUNCT_2:def 1
.= proj1 Foe
.= proj1 ((F * (the_arity_of o)) . e) by A17, FUNCT_1:13 ;
:: thesis:

end;

then A19: the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o)) by A7, FUNCT_6:def 2;

hereby :: thesis:

assume u = F # x ; :: thesis:
then A20: u = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5;
let n be Nat; :: thesis:
assume A21: n in dom f ; :: thesis:
then (the_arity_of o) . n in the carrier of S by A15, FINSEQ_2:11;
then (the_arity_of o) . n in dom F by PARTFUN1:def 2;
then A22: n in dom (F * (the_arity_of o)) by A15, A21, FUNCT_1:11;
then A23: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12
.= F . ((the_arity_of o) /. n) by A15, A21, PARTFUN1:def 6 ;
thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A2, A14, A19, A20, PRALG_2:def 2
.= (F . ((the_arity_of o) /. n)) . (f . n) by A22, A23, PRALG_1:def 17 ; :: thesis:

end;

F # x is Element of product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3;
then reconsider g = F # x as Function ;
A24: rng (the_arity_of o) c= dom F by A4, PARTFUN1:def 2;
assume A25: for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; :: thesis:

A26: now :: thesis:

let e be set ; :: thesis:
assume A27: e in dom f ; :: thesis:
then reconsider n = e as Nat by A15;
(the_arity_of o) . n in the carrier of S by A15, A27, FINSEQ_2:11;
then (the_arity_of o) . n in dom F by PARTFUN1:def 2;
then A28: n in dom (F * (the_arity_of o)) by A15, A27, FUNCT_1:11;
then A29: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12
.= F . ((the_arity_of o) /. n) by A15, A27, PARTFUN1:def 6 ;
thus u . e = (F . ((the_arity_of o) /. n)) . (f . n) by A25, A27
.= ((F * (the_arity_of o)) .. f) . n by A28, A29, PRALG_1:def 17
.= g . e by A1, A2, A14, A19, A6, PRALG_2:def 2 ; :: thesis:

end;

F # x = (F * (the_arity_of o)) .. f by A1, A2, A14, A19, A6, PRALG_2:def 2;
then dom g = dom (F * (the_arity_of o)) by PRALG_1:def 17
.= dom f by A15, A24, RELAT_1:27 ;
hence u = F # x by A15, A16, A26, FUNCT_1:2; :: thesis:

end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let o be OperSymbol of S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args (o,U1);

redefine func F # x means :Def6: :: MSUALG_3:def 6
for n being Nat st n in dom x holds
it . n = (F . ((the_arity_of o) /. n)) . (x . n);

compatibility by Lm1;

end;

:: deftheorem Def6 defines # MSUALG_3:def 6 :

theorem Th7: :: MSUALG_3:7

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x

proof end;

theorem Th8: :: MSUALG_3:8

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;

pred F is_homomorphism U1,U2 means :Def7: :: MSUALG_3:def 7
for o being OperSymbol of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x);

end;

:: deftheorem Def7 defines is_homomorphism MSUALG_3:def 7 :

theorem Th9: :: MSUALG_3:9

for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1

proof end;

theorem Th10: :: MSUALG_3:10

for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;

pred F is_epimorphism U1,U2 means :Def8: :: MSUALG_3:def 8
( F is_homomorphism U1,U2 & F is "onto" );

end;

:: deftheorem Def8 defines is_epimorphism MSUALG_3:def 8 :

theorem Th11: :: MSUALG_3:11

for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;

pred F is_monomorphism U1,U2 means :Def9: :: MSUALG_3:def 9
( F is_homomorphism U1,U2 & F is "1-1" );

end;

:: deftheorem Def9 defines is_monomorphism MSUALG_3:def 9 :

theorem Th12: :: MSUALG_3:12

for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;

pred F is_isomorphism U1,U2 means :Def10: :: MSUALG_3:def 10
( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 );

end;

:: deftheorem Def10 defines is_isomorphism MSUALG_3:def 10 :

theorem Th13: :: MSUALG_3:13

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S
for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

proof end;

theorem Th14: :: MSUALG_3:14

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1

proof end;

theorem Th15: :: MSUALG_3:15

for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;

pred U1,U2 are_isomorphic means :Def11: :: MSUALG_3:def 11
ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;

end;

:: deftheorem Def11 defines are_isomorphic MSUALG_3:def 11 :

theorem Th16: :: MSUALG_3:16

for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S holds
( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
:: original: are_isomorphic
redefine pred U1,U2 are_isomorphic ;
reflexivity by Th16;

end;

theorem :: MSUALG_3:17

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic

proof end;

theorem :: MSUALG_3:18

for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 ;

func Image F -> strict non-empty MSSubAlgebra of U2 means :Def12: :: MSUALG_3:def 12
the Sorts of it = F .:.: the Sorts of U1;

existence

proof end;

uniqueness by MSUALG_2:9;

end;

:: deftheorem Def12 defines Image MSUALG_3:def 12 :

theorem :: MSUALG_3:19

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )

proof end;

theorem Th20: :: MSUALG_3:20

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F

proof end;

theorem :: MSUALG_3:21

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F )

proof end;

theorem Th22: :: MSUALG_3:22

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for U2 being non-empty MSSubAlgebra of U1
for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1

proof end;

theorem :: MSUALG_3:23

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )

proof end;

theorem :: MSUALG_3:24

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds
( u = F # x iff for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) by Lm1;