:: Basic Properties of Functor Structures
:: by Claus Zinn and Wolfgang Jaksch
::
:: Received April 24, 1996
:: Copyright (c) 1996-2026 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 XBOOLE_0, RELAT_2, ALTCAT_1, ALTCAT_2, MSUALG_6, FUNCTOR0,
RELAT_1, FUNCT_2, FUNCT_1, SUBSET_1, FUNCT_3, ZFMISC_1, STRUCT_0, TARSKI,
MEMBER_1, MSUALG_3, ENS_1, CAT_1, PBOOLE, REALSET1, PZFMISC1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
PARTFUN1, FUNCT_2, BINOP_1, REALSET1, PZFMISC1, STRUCT_0, MSUALG_3,
ALTCAT_1, ALTCAT_2, FUNCT_3, FUNCTOR0;
constructors REALSET1, PZFMISC1, MSUALG_3, FUNCTOR0, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE,
STRUCT_0, ALTCAT_2, FUNCTOR0, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, PBOOLE, MSUALG_3, ALTCAT_2, FUNCTOR0, PZFMISC1;
equalities FUNCTOR0, BINOP_1, REALSET1;
expansions PBOOLE, MSUALG_3, ALTCAT_2, FUNCTOR0, PZFMISC1;
theorems ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCT_1, FUNCT_2, ZFMISC_1, PBOOLE,
RELAT_1, MSUALG_3, XBOOLE_1, PARTFUN1;
begin
reserve X,Y for set;
reserve Z for non empty set;
registration
cluster transitive with_units reflexive for non empty AltCatStr;
existence
proof
set C = the category;
take C;
thus thesis;
end;
end;
registration
let A be non empty reflexive AltCatStr;
cluster non empty reflexive for SubCatStr of A;
existence
proof
reconsider B = A as SubCatStr of A by ALTCAT_2:20;
take B;
thus thesis;
end;
end;
registration
let C1,C2 be non empty reflexive AltCatStr;
let F be feasible FunctorStr over C1,C2, A be non empty reflexive SubCatStr
of C1;
cluster F|A -> feasible;
coherence;
end;
begin
registration
let X be set;
cluster id X -> onto;
coherence
proof
reconsider f = id X as Function of X,X;
rng f = X;
hence thesis by FUNCT_2:def 3;
end;
end;
theorem
for A being non empty set, B,C being non empty Subset of A, D being
non empty Subset of B st C=D holds incl C = incl B * incl D
proof
let A be non empty set, B,C be non empty Subset of A, D be non empty Subset
of B such that
A1: C=D;
incl B * incl D = id (B /\ D) by FUNCT_1:22
.= incl C by A1,XBOOLE_1:28;
hence thesis;
end;
theorem Th2:
for f being Function of X,Y st f is bijective holds f" is Function of Y,X
proof
let f be Function of X,Y;
assume
A1: f is bijective;
then rng f = Y by FUNCT_2:def 3;
hence thesis by A1,FUNCT_2:25;
end;
theorem
for f being Function of X,Y, g being Function of Y,Z st f is bijective
& g is bijective holds ex h being Function of X,Z st h=g*f & h is bijective
proof
let f be Function of X,Y, g be Function of Y,Z;
assume that
A1: f is bijective and
A2: g is bijective;
A3: rng g = Z by A2,FUNCT_2:def 3;
then Y = {} iff Z = {};
then reconsider h=g*f as Function of X,Z;
take h;
rng f = Y by A1,FUNCT_2:def 3;
then rng(g*f) = Z by A3,FUNCT_2:14;
then h is onto by FUNCT_2:def 3;
hence thesis by A1,A2;
end;
begin
theorem Th4:
for A being non empty reflexive AltCatStr, B being non empty
reflexive SubCatStr of A, C being non empty SubCatStr of A, D being non empty
SubCatStr of B st C = D holds incl C = incl B * incl D
proof
let A be non empty reflexive AltCatStr, B be non empty reflexive SubCatStr
of A, C be non empty SubCatStr of A, D be non empty SubCatStr of B such that
A1: C = D;
set X = [: the carrier of B, the carrier of B :], Y = [: the carrier of D,
the carrier of D :];
A2: the carrier of D c= the carrier of B by ALTCAT_2:def 11;
then
A3: Y c= X by ZFMISC_1:96;
for i being object st i in Y holds (the MorphMap of incl C).i = (((the
MorphMap of incl B)*the ObjectMap of incl D)** the MorphMap of incl D).i
proof
set dom2 = dom (the MorphMap of incl D);
set dom1 = dom ((the MorphMap of incl B)*the ObjectMap of incl D);
set XX = the Arrows of B, YY = the Arrows of D;
let i be object;
A4: (the MorphMap of incl C).i = (id the Arrows of C).i by FUNCTOR0:def 28;
A5: dom (((the MorphMap of incl B)*the ObjectMap of incl D)** the
MorphMap of incl D) = dom2 /\ dom1 & dom (the MorphMap of incl D) = Y by
PARTFUN1:def 2,PBOOLE:def 19;
A6: dom ((the MorphMap of incl B)*the ObjectMap of incl D) = dom ((the
MorphMap of incl B)*(id Y)) by FUNCTOR0:def 28
.= (dom (the MorphMap of incl B)) /\ Y by FUNCT_1:19
.= X /\ Y by PARTFUN1:def 2
.= Y by A2,XBOOLE_1:28,ZFMISC_1:96;
assume
A7: i in Y;
then
A8: i in dom id Y;
YY cc= XX by ALTCAT_2:def 11;
then
A9: YY.i c= XX.i by A7;
A10: ((the MorphMap of incl B)*the ObjectMap of incl D).i = ((the MorphMap
of incl B)*id Y).i by FUNCTOR0:def 28
.= ((the MorphMap of incl B).((id Y).i)) by A8,FUNCT_1:13
.= ((the MorphMap of incl B).i) by A7,FUNCT_1:18;
(the MorphMap of incl B).i = (id the Arrows of B).i & (the MorphMap
of incl D).i = (id the Arrows of D).i by FUNCTOR0:def 28;
then
(the MorphMap of incl B).i * (the MorphMap of incl D).i = (id XX).i *
id (YY.i) by A7,MSUALG_3:def 1
.= id (XX.i) * id (YY.i) by A3,A7,MSUALG_3:def 1
.= id (XX.i /\ YY.i) by FUNCT_1:22
.= id ((the Arrows of D).i) by A9,XBOOLE_1:28
.= (the MorphMap of incl C).i by A1,A7,A4,MSUALG_3:def 1;
hence thesis by A7,A10,A5,A6,PBOOLE:def 19;
end;
then
A11: the MorphMap of incl C = ((the MorphMap of incl B)*the ObjectMap of
incl D)** the MorphMap of incl D by A1,PBOOLE:3;
the ObjectMap of incl C = id Y by A1,FUNCTOR0:def 28
.= id(X /\ Y) by A2,XBOOLE_1:28,ZFMISC_1:96
.= (id X)*(id Y) by FUNCT_1:22
.= (id X)*the ObjectMap of incl D by FUNCTOR0:def 28
.= (the ObjectMap of incl B)*the ObjectMap of incl D by FUNCTOR0:def 28;
hence thesis by A1,A11,FUNCTOR0:def 36;
end;
theorem Th5:
for A,B being non empty AltCatStr, F being FunctorStr over A,B st
F is bijective holds the ObjectMap of F is bijective & the MorphMap of F is
"1-1"
proof
let A,B be non empty AltCatStr, F be FunctorStr over A,B;
assume
A1: F is bijective;
then
A2: F is injective;
then F is one-to-one;
then
A3: the ObjectMap of F is one-to-one;
F is surjective by A1;
then F is onto;
then
A4: (the ObjectMap of F) is onto;
F is faithful by A2;
hence thesis by A3,A4;
end;
:: ===================================================================
:: Lemmata about properties of G*F, where G,F are FunctorStr
:: ===================================================================
theorem Th6:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is one-to-one & G is one-to-one holds G*F is one-to-one
proof
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be
feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3;
assume F is one-to-one & G is one-to-one;
then
A1: the ObjectMap of F is one-to-one & the ObjectMap of G is one-to-one;
the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by
FUNCTOR0:def 36;
hence the ObjectMap of (G*F) is one-to-one by A1;
end;
theorem Th7:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is faithful & G is faithful holds G*F is faithful
proof
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be
feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3 such that
A1: F is faithful and
A2: G is faithful;
set MMG = the MorphMap of G;
A3: MMG is "1-1" by A2;
set MMF = the MorphMap of F;
set CC2 = [:the carrier of C2,the carrier of C2:];
set CC1 = [:the carrier of C1,the carrier of C1:];
reconsider MMGF = the MorphMap of G*F as ManySortedFunction of CC1;
reconsider OMF = the ObjectMap of F as Function of CC1,CC2;
A4: MMGF = (MMG*OMF)**MMF by FUNCTOR0:def 36;
A5: MMF is "1-1" by A1;
for i be set st i in CC1 holds (MMGF.i) is one-to-one
proof
let i be set;
assume
A6: i in CC1;
then i in dom ((MMG*OMF)**MMF) by PARTFUN1:def 2;
then
A7: MMGF.i = ((MMG*OMF).i)*(MMF.i) by A4,PBOOLE:def 19
.= (MMG.(OMF.i))*(MMF.i) by A6,FUNCT_2:15;
OMF.i in CC2 by A6,FUNCT_2:5;
then
A8: MMG.(OMF.i) is one-to-one by A3,MSUALG_3:1;
MMF.i is one-to-one by A5,A6,MSUALG_3:1;
hence thesis by A7,A8;
end;
hence the MorphMap of G*F is "1-1" by MSUALG_3:1;
end;
theorem Th8:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is onto & G is onto holds G*F is onto
proof
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be
feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3 such that
A1: F is onto and
A2: G is onto;
set CC3 = [:the carrier of C3,the carrier of C3:];
set CC2 = [:the carrier of C2,the carrier of C2:];
reconsider OMG = the ObjectMap of G as Function of CC2,CC3;
OMG is onto by A2;
then
A3: rng OMG = CC3 by FUNCT_2:def 3;
set CC1 = [:the carrier of C1,the carrier of C1:];
reconsider OMF = the ObjectMap of F as Function of CC1,CC2;
OMF is onto by A1;
then rng OMF = CC2 by FUNCT_2:def 3;
then rng (OMG*OMF) = CC3 by A3,FUNCT_2:14;
then OMG*OMF is onto by FUNCT_2:def 3;
hence the ObjectMap of (G*F) is onto by FUNCTOR0:def 36;
end;
theorem Th9:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is full & G is full holds G*F is full
proof
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be
feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3 such that
A1: F is full and
A2: G is full;
set CC3 = [:the carrier of C3,the carrier of C3:];
set CC2 = [:the carrier of C2,the carrier of C2:];
set CC1 = [:the carrier of C1,the carrier of C1:];
reconsider OMF = the ObjectMap of F as Function of CC1,CC2;
reconsider OMG = the ObjectMap of G as Function of CC2,CC3;
consider MMF being ManySortedFunction of (the Arrows of C1), (the Arrows of
C2)*the ObjectMap of F such that
A3: MMF = the MorphMap of F and
A4: MMF is "onto" by A1;
consider MMG being ManySortedFunction of (the Arrows of C2), (the Arrows of
C3)*the ObjectMap of G such that
A5: MMG = the MorphMap of G and
A6: MMG is "onto" by A2;
ex f being ManySortedFunction of (the Arrows of C1), (the Arrows of C3)*
the ObjectMap of (G*F) st f = the MorphMap of G*F & f is "onto"
proof
reconsider MMGF = the MorphMap of G*F as ManySortedFunction of (the Arrows
of C1), (the Arrows of C3)*the ObjectMap of (G*F) by FUNCTOR0:def 4;
take MMGF;
A7: MMGF = (MMG*OMF)**MMF by A3,A5,FUNCTOR0:def 36;
for i be set st i in CC1 holds rng(MMGF.i) = ((the Arrows of C3)*the
ObjectMap of (G*F)).i
proof
let i be set;
assume
A8: i in CC1;
then reconsider
MMGI = MMG.(OMF.i) as Function of (the Arrows of C2).(OMF.i),
((the Arrows of C3)*the ObjectMap of G).(OMF.i) by FUNCT_2:5,PBOOLE:def 15;
A9: OMF.i in CC2 by A8,FUNCT_2:5;
A10: rng ((MMG.(OMF.i))*(MMF.i)) = rng (MMG.(OMF.i))
proof
per cases;
suppose
A11: rng MMGI = {};
rng ({}*(MMF.i)) = {};
hence thesis by A11,RELAT_1:41;
end;
suppose
A12: rng MMGI<>{};
rng MMGI = ((the Arrows of C3)*the ObjectMap of G).(OMF.i) by A6,A9;
then dom MMGI = (the Arrows of C2).(OMF.i) by A12,FUNCT_2:def 1;
then dom MMGI = ((the Arrows of C2)*OMF).i by A8,FUNCT_2:15
.= rng (MMF.i) by A4,A8;
hence thesis by RELAT_1:28;
end;
end;
i in dom ((MMG*OMF)**MMF) by A8,PARTFUN1:def 2;
then rng (MMGF.i) = rng (((MMG*OMF).i)*(MMF.i)) by A7,PBOOLE:def 19
.= rng (MMG.(OMF.i)) by A8,A10,FUNCT_2:15
.= ((the Arrows of C3)*the ObjectMap of G).(OMF.i) by A6,A9
.= (the Arrows of C3).(OMG.(OMF.i)) by A8,FUNCT_2:5,15
.= (the Arrows of C3).((OMG*OMF).i) by A8,FUNCT_2:15
.= (the Arrows of C3).((the ObjectMap of (G*F)).i) by FUNCTOR0:def 36
.= ((the Arrows of C3)*the ObjectMap of (G*F)).i by A8,FUNCT_2:15;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th10:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is injective & G is injective holds G*F is injective
by Th7,Th6;
theorem Th11:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is surjective & G is surjective holds G*F is surjective
by Th8,Th9;
theorem Th12:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive
AltGraph, F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3
st F is bijective & G is bijective holds G*F is bijective
by Th11,Th10;
begin :: Theorems about the restriction ans inclusion operator
theorem
for A,I being non empty reflexive AltCatStr, B being non empty
reflexive SubCatStr of A, C being non empty SubCatStr of A, D being non empty
SubCatStr of B st C = D for F being FunctorStr over A,I holds F|C = F|B|D
proof
let A,I be non empty reflexive AltCatStr, B be non empty reflexive SubCatStr
of A, C be non empty SubCatStr of A, D be non empty SubCatStr of B such that
A1: C = D;
let F be FunctorStr over A,I;
thus F|C = F * (incl B * incl D) by A1,Th4
.= F|B|D by FUNCTOR0:32;
end;
theorem
for A being non empty AltCatStr, B being non empty SubCatStr of A
holds B is full iff incl B is full
proof
let A be non empty AltCatStr, B be non empty SubCatStr of A;
hereby
ex I29 being non empty set, B9 being ManySortedSet of I29, f9 being
Function of [:the carrier of B,the carrier of B:],I29 st the ObjectMap of incl
B = f9 & (the Arrows of A) = B9 & the MorphMap of incl B is ManySortedFunction
of (the Arrows of B), B9*f9 by FUNCTOR0:def 3;
then reconsider
f = the MorphMap of incl B as ManySortedFunction of (the Arrows
of B), (the Arrows of A)*the ObjectMap of incl B;
set I = [:the carrier of B, the carrier of B:];
the carrier of B c= the carrier of A & dom(the Arrows of A) = [:the
carrier of A, the carrier of A:] by ALTCAT_2:def 11,PARTFUN1:def 2;
then
A1: dom(the Arrows of A) /\ I = I by XBOOLE_1:28,ZFMISC_1:96;
assume
A2: B is full;
f is "onto"
proof
let i be set such that
A3: i in I;
(the Arrows of B) = (the Arrows of A)||the carrier of B by A2;
then
A4: (the Arrows of B).i = (the Arrows of A).i by A3,FUNCT_1:49;
rng (f.i) = rng ((id the Arrows of B).i) by FUNCTOR0:def 28
.= rng (id ((the Arrows of B).i)) by A3,MSUALG_3:def 1
.= (the Arrows of A).i by A4
.= ((the Arrows of A)*id I).i by A1,A3,FUNCT_1:20
.= ((the Arrows of A)*the ObjectMap of incl B).i by FUNCTOR0:def 28;
hence thesis;
end;
hence incl B is full;
end;
set I = [:the carrier of B, the carrier of B:];
A5: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
then
A6: I c= [:the carrier of A, the carrier of A:] by ZFMISC_1:96;
dom(the Arrows of A) = [:the carrier of A, the carrier of A:] by
PARTFUN1:def 2;
then
A7: dom(the Arrows of A) /\ I = I by A5,XBOOLE_1:28,ZFMISC_1:96;
then dom((the Arrows of A)|(I qua set)) = I by RELAT_1:61;
then reconsider
XX = ((the Arrows of A)||the carrier of B) as ManySortedSet of I
by PARTFUN1:def 2;
assume
A8: incl B is full;
A9: XX c= the Arrows of B
proof
let i be object such that
A10: i in I;
let x be object;
assume
A11: x in XX.i;
x in (the Arrows of B).i
proof
consider f being ManySortedFunction of (the Arrows of B), (the Arrows of
A)*the ObjectMap of incl B such that
A12: f = the MorphMap of incl B and
A13: f is "onto" by A8;
f = id the Arrows of B by A12,FUNCTOR0:def 28;
then
A14: rng ((id the Arrows of B).i) = ((the Arrows of A)*the ObjectMap of
incl B).i by A10,A13
.= ((the Arrows of A)*id I).i by FUNCTOR0:def 28
.= (the Arrows of A).i by A7,A10,FUNCT_1:20;
consider y,z being object such that
y in the carrier of A and
z in the carrier of A and
A15: i = [y,z] by A6,A10,ZFMISC_1:84;
y in (the carrier of B) & z in (the carrier of B) by A10,A15,ZFMISC_1:87;
then
A16: XX.(y,z) = (the Arrows of A).(y,z) by A5,ALTCAT_1:5;
rng ((id the Arrows of B).i) = rng (id ((the Arrows of B).i)) by A10,
MSUALG_3:def 1
.= (the Arrows of B).i;
hence thesis by A11,A15,A16,A14;
end;
hence thesis;
end;
the Arrows of B c= XX
proof
let i be object;
assume
A17: i in I;
then consider y,z being object such that
y in the carrier of A and
z in the carrier of A and
A18: i = [y,z] by A6,ZFMISC_1:84;
y in the carrier of B & z in the carrier of B by A17,A18,ZFMISC_1:87;
then
A19: XX.(y,z) = (the Arrows of A).(y,z) by A5,ALTCAT_1:5;
let x be object;
assume
A20: x in (the Arrows of B).i;
the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
then (the Arrows of B).(y,z) c= (the Arrows of A).(y,z) by A17,A18;
hence thesis by A18,A20,A19;
end;
hence the Arrows of B = (the Arrows of A)||the carrier of B by A9,PBOOLE:146;
end;
begin :: Theorems about 'full' and 'faithful' of Functor Structures
theorem
for C1, C2 being non empty AltCatStr, F being Covariant FunctorStr
over C1,C2 holds F is full iff for o1,o2 being Object of C1 holds Morph-Map(F,
o1,o2) is onto
proof
let C1, C2 be non empty AltCatStr, F be Covariant FunctorStr over C1,C2;
set I = [:the carrier of C1, the carrier of C1:];
hereby
assume F is full;
then consider
f being ManySortedFunction of (the Arrows of C1), (the Arrows of
C2)*the ObjectMap of F such that
A1: f = the MorphMap of F and
A2: f is "onto";
let o1,o2 be Object of C1;
A3: [o1,o2] in I by ZFMISC_1:87;
then
A4: [o1,o2] in dom(the ObjectMap of F) by FUNCT_2:def 1;
rng(f.[o1,o2]) = ((the Arrows of C2)*the ObjectMap of F).[o1,o2] by A2,A3;
then
rng(Morph-Map(F,o1,o2)) = (the Arrows of C2).((the ObjectMap of F).(o1
,o2)) by A1,A4,FUNCT_1:13
.= (the Arrows of C2).(F.o1,F.o2) by FUNCTOR0:22
.= <^F.o1,F.o2^> by ALTCAT_1:def 1;
hence Morph-Map(F,o1,o2) is onto by FUNCT_2:def 3;
end;
ex I29 being non empty set, B9 being ManySortedSet of I29, f9 being
Function of I,I29 st the ObjectMap of F = f9 & (the Arrows of C2) = B9 & the
MorphMap of F is ManySortedFunction of (the Arrows of C1), B9* f9 by
FUNCTOR0:def 3;
then reconsider
f = the MorphMap of F as ManySortedFunction of (the Arrows of C1)
, (the Arrows of C2)*the ObjectMap of F;
assume
A5: for o1,o2 being Object of C1 holds Morph-Map(F,o1,o2) is onto;
f is "onto"
proof
let i be set;
assume i in I;
then consider o1,o2 being object such that
A6: o1 in the carrier of C1 & o2 in the carrier of C1 and
A7: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C1 by A6;
[o1,o2] in I by ZFMISC_1:87;
then
A8: [o1,o2] in dom(the ObjectMap of F) by FUNCT_2:def 1;
Morph-Map(F,o1,o2) is onto by A5;
then rng(Morph-Map(F,o1,o2)) = <^F.o1,F.o2^> by FUNCT_2:def 3
.= (the Arrows of C2).(F.o1,F.o2) by ALTCAT_1:def 1
.= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by FUNCTOR0:22
.= ((the Arrows of C2)*the ObjectMap of F).(o1,o2) by A8,FUNCT_1:13;
hence thesis by A7;
end;
hence
ex f being ManySortedFunction of (the Arrows of C1), (the Arrows of C2)
*the ObjectMap of F st f = the MorphMap of F & f is "onto";
end;
theorem
for C1, C2 being non empty AltCatStr, F being Covariant FunctorStr
over C1,C2 holds F is faithful iff for o1,o2 being Object of C1 holds Morph-Map
(F,o1,o2) is one-to-one
proof
let C1, C2 be non empty AltCatStr, F be Covariant FunctorStr over C1,C2;
set I = [:the carrier of C1, the carrier of C1:];
hereby
assume F is faithful;
then
A1: (the MorphMap of F) is "1-1";
let o1,o2 be Object of C1;
[o1,o2] in I & dom(the MorphMap of F) = I by PARTFUN1:def 2,ZFMISC_1:87;
hence Morph-Map(F,o1,o2) is one-to-one by A1;
end;
assume
A2: for o1,o2 being Object of C1 holds Morph-Map(F,o1,o2) is one-to-one;
let i be set, f be Function such that
A3: i in dom(the MorphMap of F) and
A4: (the MorphMap of F).i = f;
dom(the MorphMap of F) = I by PARTFUN1:def 2;
then consider o1,o2 being object such that
A5: o1 in the carrier of C1 & o2 in the carrier of C1 and
A6: i = [o1,o2] by A3,ZFMISC_1:84;
reconsider o1, o2 as Object of C1 by A5;
(the MorphMap of F).(o1,o2) = Morph-Map(F,o1,o2);
hence thesis by A2,A4,A6;
end;
begin :: Theorems about the inversion of Functor Structures
theorem
for A being transitive with_units non empty AltCatStr holds (id A)" = id A
proof
let A be transitive with_units non empty AltCatStr;
set CCA = [:the carrier of A, the carrier of A:];
consider f being ManySortedFunction of (the Arrows of A), (the Arrows of A)*
the ObjectMap of (id A) such that
A1: f = the MorphMap of (id A) and
A2: the MorphMap of (id A)" = f""*(the ObjectMap of (id A))" by FUNCTOR0:def 38
;
A3: for i be set st i in CCA holds (id (the Arrows of A)).i is one-to-one
proof
let i be set such that
A4: i in CCA;
id ((the Arrows of A).i) is one-to-one;
hence thesis by A4,MSUALG_3:def 1;
end;
the MorphMap of (id A) = id (the Arrows of A) by FUNCTOR0:def 29;
then
A5: the MorphMap of (id A) is "1-1" by A3,MSUALG_3:1;
for i be set st i in CCA holds rng(f.i) = ((the Arrows of A)*the
ObjectMap of (id A)).i
proof
dom (the Arrows of A) = CCA by PARTFUN1:def 2;
then
A6: (dom (the Arrows of A)) /\ CCA = CCA;
let i be set such that
A7: i in CCA;
rng(f.i) = rng ((id (the Arrows of A)).i) by A1,FUNCTOR0:def 29
.= rng (id ((the Arrows of A).i)) by A7,MSUALG_3:def 1
.= (the Arrows of A).i
.= ((the Arrows of A)*(id CCA)).i by A7,A6,FUNCT_1:20
.= ((the Arrows of A)*the ObjectMap of (id A)).i by FUNCTOR0:def 29;
hence thesis;
end;
then
A8: f is "onto";
for i being object st i in CCA holds (f"").i = f.i
proof
let i be object;
assume
A9: i in CCA;
then (f"").i = ((the MorphMap of (id A)).i)" by A1,A5,A8,MSUALG_3:def 4
.= ((id (the Arrows of A)).i)" by FUNCTOR0:def 29
.= ((id ((the Arrows of A).i)))" by A9,MSUALG_3:def 1
.= id ((the Arrows of A).i) by FUNCT_1:45
.= ((id (the Arrows of A)).i) by A9,MSUALG_3:def 1
.= f.i by A1,FUNCTOR0:def 29;
hence thesis;
end;
then
A10: f"" = f;
for i being object st i in CCA holds ((the MorphMap of (id A))*(id CCA)).i
= (the MorphMap of (id A)).i
proof
dom (the MorphMap of (id A)) = CCA by PARTFUN1:def 2;
then
A11: (dom (the MorphMap of (id A))) /\ CCA = CCA;
let i be object;
assume i in CCA;
hence thesis by A11,FUNCT_1:20;
end;
then
A12: (the MorphMap of (id A))*(id CCA) = the MorphMap of (id A);
A13: the ObjectMap of (id A)" = (the ObjectMap of (id A))" by FUNCTOR0:def 38;
then the ObjectMap of (id A)" = (id CCA)" by FUNCTOR0:def 29
.= (id CCA) by FUNCT_1:45
.= the ObjectMap of (id A) by FUNCTOR0:def 29;
hence thesis by A13,A1,A2,A10,A12,FUNCTOR0:def 29;
end;
:: ===================================================================
theorem
for A, B being transitive with_units reflexive non empty AltCatStr
for F being feasible FunctorStr over A,B st F is bijective for G being feasible
FunctorStr over B,A st the FunctorStr of G=F" holds F * G = id B
proof
let A,B be transitive with_units reflexive non empty AltCatStr;
set I1 = [:the carrier of A,the carrier of A:];
set I2 = [:the carrier of B,the carrier of B:];
let F be feasible FunctorStr over A,B such that
A1: F is bijective;
consider k being ManySortedFunction of (the Arrows of A), (the Arrows of B)*
the ObjectMap of F such that
A2: k = the MorphMap of F and
A3: the MorphMap of F" = k""*(the ObjectMap of F)" by A1,FUNCTOR0:def 38;
F is injective by A1;
then F is one-to-one;
then
A4: (the ObjectMap of F) is one-to-one;
set OM = the ObjectMap of F;
F is surjective by A1;
then F is onto;
then (the ObjectMap of F) is onto;
then
A5: rng OM = I2 by FUNCT_2:def 3;
F is injective by A1;
then
A6: F is faithful;
then
A7: (the MorphMap of F) is "1-1";
F is surjective by A1;
then F is full onto;
then consider
f being ManySortedFunction of (the Arrows of A), (the Arrows of B)*
the ObjectMap of F such that
A8: f = the MorphMap of F and
A9: f is "onto";
let G be feasible FunctorStr over B,A such that
A10: the FunctorStr of G=F";
A11: (the ObjectMap of G) = (the ObjectMap of F)" by A1,A10,FUNCTOR0:def 38;
the FunctorStr of G is bijective by A1,A10,FUNCTOR0:35;
then the FunctorStr of G is surjective;
then the FunctorStr of G is full onto;
then
A12: the ObjectMap of G is onto;
set OMG = the ObjectMap of G;
A13: dom OM = I1 by FUNCT_2:def 1;
reconsider OM as bifunction of the carrier of A, the carrier of B;
A14: I2 = dom((f * OMG) ** (k"" * OMG)) by PARTFUN1:def 2;
A15: for i be object st i in I2 holds ((f * OMG) ** (k""* OMG)).i = (id (the
Arrows of B)).i
proof
let i be object such that
A16: i in I2;
A17: dom(OMG) = I2 by FUNCT_2:def 1;
then
A18: (f * OMG).i = k.(OMG.i) by A2,A8,A16,FUNCT_1:13;
rng(OMG) = I1 by A12,FUNCT_2:def 3;
then
A19: OMG.i in I1 by A16,A17,FUNCT_1:def 3;
then
A20: rng (f.(OMG.i)) = ((the Arrows of B)*the ObjectMap of F).(OMG.i) by A9
.= (the Arrows of B).((the ObjectMap of F).(OMG.i)) by A13,A19,FUNCT_1:13
;
A21: (the ObjectMap of F).(OMG.i) = (OM*OM").i by A11,A16,A17,FUNCT_1:13
.= (id I2).i by A4,A5,FUNCT_1:39
.= i by A16,FUNCT_1:18;
f is "1-1" & dom(f) = I1 by A6,A8,PARTFUN1:def 2;
then
A22: (f.(OMG.i)) is one-to-one by A19;
(k"" * OMG).i = k"".(OMG.i) by A16,A17,FUNCT_1:13
.= (k.(OMG.i))" by A7,A2,A8,A9,A19,MSUALG_3:def 4;
then ( (f * OMG) ** (k"" * OMG) ).i = f.(OMG.i) * (f.(OMG.i))" by A2,A8,A14
,A16,A18,PBOOLE:def 19
.= id ((the Arrows of B).i) by A22,A20,A21,FUNCT_1:39
.= (id (the Arrows of B)).i by A16,MSUALG_3:def 1;
hence thesis;
end;
the MorphMap of F*G = (f * OMG) ** (k""* OMG) by A10,A3,A8,A11,
FUNCTOR0:def 36;
then
A23: the MorphMap of F*G = id (the Arrows of B) by A15;
the ObjectMap of F*G = (the ObjectMap of F)*the ObjectMap of G by
FUNCTOR0:def 36;
then
the ObjectMap of F*G = (the ObjectMap of F)*(the ObjectMap of F)" by A1,A10,
FUNCTOR0:def 38;
then the ObjectMap of F*G = id [:the carrier of B,the carrier of B:] by A4,A5
,FUNCT_1:39;
hence thesis by A23,FUNCTOR0:def 29;
end;
Lm1: for I be set, A,B be ManySortedSet of I st A is_transformable_to B for H
be ManySortedFunction of A,B, H1 be ManySortedFunction of B,A st H is "1-1"
"onto" & H1 = H"" holds H**H1 = id B & H1**H = id A
proof
let I be set, A,B be ManySortedSet of I such that
A1: A is_transformable_to B;
let H be ManySortedFunction of A,B, H1 be ManySortedFunction of B,A;
assume that
A2: H is "1-1" "onto" and
A3: H1 = H"";
reconsider F1 = H**H1 as ManySortedFunction of I;
A4: now
let i be set;
assume
A5: i in I;
then reconsider h = H.i as Function of A.i,B.i by PBOOLE:def 15;
reconsider h1 = H1.i as Function of B.i,A.i by A5,PBOOLE:def 15;
i in dom H by A5,PARTFUN1:def 2;
then
A6: h is one-to-one by A2;
h1 = h" by A2,A3,A5,MSUALG_3:def 4;
then h*h1 = id rng h by A6,FUNCT_1:39;
then h*h1 = id (B.i) by A2,A5;
hence (H**H1).i = id (B.i) by A5,MSUALG_3:2;
end;
now
let i be object;
assume i in I;
then F1.i = id (B.i) by A4;
hence F1.i is Function of B.i, B.i;
end;
then
A7: F1 is ManySortedFunction of B,B by PBOOLE:def 15;
reconsider F = H1**H as ManySortedFunction of I;
A8: for i be set st i in I holds (H1**H).i = id (A.i)
proof
let i be set;
assume
A9: i in I;
then reconsider h = H.i as Function of A.i,B.i by PBOOLE:def 15;
reconsider h1 = H1.i as Function of B.i,A.i by A9,PBOOLE:def 15;
i in dom H by A9,PARTFUN1:def 2;
then
A10: h is one-to-one by A2;
B.i = {} implies A.i = {} by A1,A9;
then
A11: dom h = A.i by FUNCT_2:def 1;
h1 = h" by A2,A3,A9,MSUALG_3:def 4;
then h1*h = id (A.i) by A10,A11,FUNCT_1:39;
hence thesis by A9,MSUALG_3:2;
end;
now
let i be object;
assume i in I;
then (H1**H).i = id (A.i) by A8;
hence (H1**H).i is Function of A.i, A.i;
end;
then reconsider F as ManySortedFunction of A,A by PBOOLE:def 15;
F = id A by A8,MSUALG_3:def 1;
hence thesis by A4,A7,MSUALG_3:def 1;
end;
:: ===================================================================
theorem
for A, B being transitive with_units reflexive non empty AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds (F") * F = id
A
proof
let A,B be transitive with_units reflexive non empty AltCatStr;
set I1 = [:the carrier of A,the carrier of A:];
let F be feasible FunctorStr over A,B such that
A1: F is bijective;
consider f being ManySortedFunction of (the Arrows of A), (the Arrows of B)*
the ObjectMap of F such that
A2: f = the MorphMap of F and
A3: the MorphMap of F" = f""*(the ObjectMap of F)" by A1,FUNCTOR0:def 38;
set OM = the ObjectMap of F;
A4: dom OM = I1 by FUNCT_2:def 1;
A5: (the Arrows of A) is_transformable_to (the Arrows of B)*the ObjectMap of F
proof
let i be set;
assume
A6: i in I1;
then consider o1,o2 being object such that
A7: o1 in the carrier of A & o2 in the carrier of A and
A8: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of A by A7;
A9: (the Arrows of A).i = (the Arrows of A).(o1,o2) by A8
.= <^o1,o2^> by ALTCAT_1:def 1;
assume ((the Arrows of B)*the ObjectMap of F).i = {};
then (the Arrows of B).((the ObjectMap of F).(o1,o2)) = {} by A6,A8,
FUNCT_2:15;
hence thesis by A9,FUNCTOR0:def 11;
end;
F is injective by A1;
then F is faithful;
then
A10: (the MorphMap of F) is "1-1";
for i being object st i in I1 holds (f""*(id I1)).i = f"".i
proof
let i be object;
assume
A11: i in I1;
then (f""*(id I1)).i = f"".((id I1).i) by FUNCT_2:15
.= f"".i by A11,FUNCT_1:18;
hence thesis;
end;
then
A12: (f""*(id I1)) = f"";
F is injective by A1;
then F is one-to-one;
then
A13: (the ObjectMap of F) is one-to-one;
the ObjectMap of F"*F = (the ObjectMap of F")*the ObjectMap of F by
FUNCTOR0:def 36;
then
the ObjectMap of F"*F = (the ObjectMap of F)"*the ObjectMap of F by A1,
FUNCTOR0:def 38;
then
A14: the ObjectMap of F"*F = id [:the carrier of A,the carrier of A:] by A13,A4
,FUNCT_1:39;
F is surjective by A1;
then F is full onto;
then
A15: ex k being ManySortedFunction of (the Arrows of A), (the Arrows of B)*
the ObjectMap of F st k = the MorphMap of F & k is "onto";
the MorphMap of F"*F = (f""*(the ObjectMap of F)"*the ObjectMap of F)**
f by A2,A3,FUNCTOR0:def 36
.= (f""*((the ObjectMap of F)"*the ObjectMap of F))**f by RELAT_1:36;
then the MorphMap of F"*F = (f""*(id I1))**f by A13,A4,FUNCT_1:39;
then the MorphMap of F"*F = id the Arrows of A by A5,A2,A10,A15,A12,Lm1;
hence thesis by A14,FUNCTOR0:def 29;
end;
:: ===================================================================
theorem
for A, B being transitive with_units reflexive non empty AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds (F")" = the
FunctorStr of F
proof
let A,B be transitive with_units reflexive non empty AltCatStr;
set CCA = [:the carrier of A, the carrier of A:];
set CCB = [:the carrier of B, the carrier of B:];
let F be feasible FunctorStr over A,B such that
A1: F is bijective;
A2: F is injective by A1;
then F is one-to-one;
then
A3: the ObjectMap of F is one-to-one;
A4: F" is bijective by A1,FUNCTOR0:35;
then F" is surjective;
then
A5: F" is full;
F" is injective by A4;
then
A6: F" is faithful;
A7: (the ObjectMap of F")" = ((the ObjectMap of F)")" by A1,FUNCTOR0:def 38
.= the ObjectMap of F by A3,FUNCT_1:43;
F is faithful by A2;
then
A8: the MorphMap of F is "1-1";
A9: F is surjective by A1;
then F is onto;
then (the ObjectMap of F) is onto;
then
A10: rng (the ObjectMap of F) = CCB by FUNCT_2:def 3;
A11: F is full by A9;
the MorphMap of (F")" = the MorphMap of F
proof
A12: ex kk being ManySortedFunction of (the Arrows of B), (the Arrows of A)
*the ObjectMap of (F") st kk = the MorphMap of (F") & kk is "onto" by A5;
A13: ex k being ManySortedFunction of (the Arrows of A), (the Arrows of B)*
the ObjectMap of F st k = the MorphMap of F & k is "onto" by A11;
consider f being ManySortedFunction of (the Arrows of B), (the Arrows of A
)*the ObjectMap of (F") such that
A14: f = the MorphMap of (F") and
A15: the MorphMap of (F")" = f""*(the ObjectMap of F")" by A4,FUNCTOR0:def 38;
consider g being ManySortedFunction of (the Arrows of A), (the Arrows of B
)*the ObjectMap of F such that
A16: g = the MorphMap of F and
A17: the MorphMap of (F") = g""*(the ObjectMap of F)" by A1,FUNCTOR0:def 38;
A18: f is "1-1" by A6,A14;
for i being object st i in CCA holds (f""*(the ObjectMap of F")").i = (
the MorphMap of F).i
proof
A19: (the ObjectMap of F)" is Function of CCB,CCA by A3,A10,FUNCT_2:25;
let i be object;
assume
A20: i in CCA;
then
A21: (the ObjectMap of F).i in CCB by FUNCT_2:5;
(the ObjectMap of F)" is Function of CCB,CCA by A3,A10,FUNCT_2:25;
then
A22: (the ObjectMap of F)".((the ObjectMap of F).i) in CCA by A21,FUNCT_2:5;
A23: g.i is one-to-one by A8,A16,A20,MSUALG_3:1;
(f""*((the ObjectMap of F")")).i = f"".((the ObjectMap of F).i) by A7,A20
,FUNCT_2:15
.= ((the MorphMap of (F")).((the ObjectMap of F).i))" by A14,A12,A18
,A21,MSUALG_3:def 4
.= ((g"".((the ObjectMap of F)".((the ObjectMap of F).i))))" by A17,A20
,A19,FUNCT_2:5,15
.= (((g.((the ObjectMap of F)".((the ObjectMap of F).i)))"))" by A8,A16
,A13,A22,MSUALG_3:def 4
.= (((g.i)"))" by A3,A20,FUNCT_2:26
.= (the MorphMap of F).i by A16,A23,FUNCT_1:43;
hence thesis;
end;
hence thesis by A15;
end;
hence thesis by A4,A7,FUNCTOR0:def 38;
end;
theorem
for A, B, C being transitive with_units reflexive non empty AltCatStr
, G being feasible FunctorStr over A,B, F being feasible FunctorStr over B,C,
GI being feasible FunctorStr over B,A, FI being feasible FunctorStr over C,B st
F is bijective & G is bijective & the FunctorStr of GI=G" & the FunctorStr of
FI=F" holds (F*G)" = (GI*FI)
proof
let A, B, C be transitive with_units reflexive non empty AltCatStr, G be
feasible FunctorStr over A,B, F be feasible FunctorStr over B,C, GI be feasible
FunctorStr over B,A, FI be feasible FunctorStr over C,B such that
A1: F is bijective and
A2: G is bijective and
A3: the FunctorStr of GI=G" and
A4: the FunctorStr of FI=F";
reconsider MF = the MorphMap of F as ManySortedFunction of (the Arrows of B)
, (the Arrows of C)*the ObjectMap of F by FUNCTOR0:def 4;
A5: MF is "1-1" by A1,Th5;
set OG = the ObjectMap of G;
set CB = [:the carrier of B, the carrier of B:];
set CA = [:the carrier of A, the carrier of A:];
reconsider OGI=OG" as Function of CB,CA by A2,Th2,Th5;
set CC = [:the carrier of C, the carrier of C:];
set OF = the ObjectMap of F;
reconsider OFI=OF" as Function of CC,CB by A1,Th2,Th5;
reconsider MFG = the MorphMap of (F*G) as ManySortedFunction of (the Arrows
of A), (the Arrows of C)*the ObjectMap of (F*G) by FUNCTOR0:def 4;
reconsider OG as Function of CA,CB;
reconsider OFG = the ObjectMap of (F*G) as Function of CA,CC;
reconsider MG = the MorphMap of G as ManySortedFunction of (the Arrows of A)
, (the Arrows of B)*the ObjectMap of G by FUNCTOR0:def 4;
A6: MG is "1-1" by A2,Th5;
F is surjective by A1;
then F is full;
then
A7: ex mf being ManySortedFunction of (the Arrows of B), (the Arrows of C)*
the ObjectMap of F st mf = the MorphMap of F & mf is "onto";
F is injective by A1;
then F is one-to-one;
then
A8: the ObjectMap of F is one-to-one;
A9: G is surjective by A2;
then G is onto;
then
A10: the ObjectMap of G is onto;
G is full by A9;
then
A11: ex mg being ManySortedFunction of (the Arrows of A), (the Arrows of B)*
the ObjectMap of G st mg = the MorphMap of G & mg is "onto";
G is injective by A2;
then G is one-to-one;
then
A12: the ObjectMap of G is one-to-one;
A13: F*G is bijective by A1,A2,Th12;
then F*G is surjective;
then F*G is full;
then
A14: ex mfg being ManySortedFunction of (the Arrows of A), (the Arrows of C)*
the ObjectMap of (F*G) st mfg = the MorphMap of (F*G) & mfg is "onto";
A15: MFG is "1-1" by A13,Th5;
A16: the MorphMap of (F*G)" = the MorphMap of (GI*FI)
proof
consider f being ManySortedFunction of (the Arrows of A), (the Arrows of C
)*the ObjectMap of (F*G) such that
A17: f = the MorphMap of (F*G) and
A18: the MorphMap of (F*G)" = f""*(the ObjectMap of (F*G))" by A13,
FUNCTOR0:def 38;
A19: rng(the ObjectMap of G) = CB by A10,FUNCT_2:def 3;
for i being object st i in CC holds (f""*(the ObjectMap of (F*G))").i =
(((the MorphMap of G")*the ObjectMap of F")**the MorphMap of F").i
proof
A20: (ex x1 being ManySortedFunction of (the Arrows of B), (the Arrows
of C)*the ObjectMap of F st x1 = the MorphMap of F & the MorphMap of F" = x1""*
(the ObjectMap of F)" )& ex x1 being ManySortedFunction of (the Arrows of A), (
the Arrows of B)*the ObjectMap of G st x1 = the MorphMap of G & the MorphMap of
G" = x1""*(the ObjectMap of G)" by A1,A2,FUNCTOR0:def 38;
A21: OF" = the ObjectMap of F" & dom (((MG""*OGI)*OFI)**(MF""*OFI)) = CC
by A1,FUNCTOR0:def 38,PARTFUN1:def 2;
A22: OG*OG" = id CB by A12,A19,FUNCT_2:29;
A23: OFG" = (OF*OG)" by FUNCTOR0:def 36
.= OG"*OF" by A8,A12,FUNCT_1:44;
let i be object such that
A24: i in CC;
A25: ( MF.(OG.((OG"*OF").i)) *(MG.((OFG)".i)) )" = ( MF.(OG.(OGI.(OFI.i)
)) *(MG.((OFG)".i)) )" by A24,FUNCT_2:15
.= ( MF.((OG*OGI).(OFI.i)) *(MG.((OFG)".i)) )" by A24,FUNCT_2:5,15
.= ( MF.(((id CB)*OFI).i) *(MG.((OFG)".i)) )" by A24,A22,FUNCT_2:15
.= ( MF.(OF".i) *(MG.((OGI*OFI).i)) )" by A23,FUNCT_2:17;
OFG" is Function of CC,CA by A13,Th2,Th5;
then
A26: dom (((MF)*OG)**MG) = CA & ((OFG)".i) in CA by A24,FUNCT_2:5
,PARTFUN1:def 2;
A27: (the ObjectMap of (F*G))" is Function of CC,CA by A13,Th2,Th5;
then
A28: ((the ObjectMap of (F*G))".i) in CA by A24,FUNCT_2:5;
i in dom ((the ObjectMap of (F*G))") by A24,A27,FUNCT_2:def 1;
then
A29: (f""*(the ObjectMap of (F*G))").i = MFG"".((the ObjectMap of (F*G))
".i) by A17,FUNCT_1:13
.= (MFG.((the ObjectMap of (F*G))".i))" by A14,A15,A28,MSUALG_3:def 4
.= ((((MF)*OG)**MG).((OFG)".i))" by FUNCTOR0:def 36
.= ( (((MF)*OG).((OFG)".i))*(MG.((OFG)".i)) )" by A26,PBOOLE:def 19
.= ( MF.(OG.((OG"*OF").i)) *(MG.((OFG)".i)) )" by A24,A27,A23,FUNCT_2:5
,15;
A30: OFI.i in CB by A24,FUNCT_2:5;
then
A31: MF.(OFI.i) is one-to-one by A5,MSUALG_3:1;
A32: (OGI.(OFI.i)) in CA by A30,FUNCT_2:5;
then
A33: MG.(OGI.(OFI.i)) is one-to-one by A6,MSUALG_3:1;
( MF.(OF".i) *(MG.((OGI*OFI).i)) )" = ((MF.(OF".i)) * (MG.(OGI.(OFI
.i))))" by A24,FUNCT_2:15
.= (MG.(OGI.(OFI.i)))" * (MF.(OFI.i))" by A33,A31,FUNCT_1:44
.= (MG"".(OGI.(OFI.i))) * (MF.(OF".i))" by A11,A6,A32,MSUALG_3:def 4
.= ((MG""*OGI).(OFI.i)) * (MF.(OF".i))" by A24,FUNCT_2:5,15
.= ((MG""*OGI)*OFI).i * (MF.(OFI.i))" by A24,FUNCT_2:15
.= ((MG""*OGI)*OFI).i * (MF"".(OFI.i)) by A5,A7,A30,MSUALG_3:def 4
.= ((MG""*OGI)*OFI).i * (MF""*OFI).i by A24,FUNCT_2:15;
hence thesis by A20,A24,A21,A29,A25,PBOOLE:def 19;
end;
then
the MorphMap of (F*G)" = ((the MorphMap of GI)*the ObjectMap of FI)**
the MorphMap of FI by A3,A4,A18
.= the MorphMap of (GI*FI) by FUNCTOR0:def 36;
hence thesis;
end;
the ObjectMap of (F*G)" = (the ObjectMap of (F*G))" by A13,FUNCTOR0:def 38
.= ((the ObjectMap of F)*(the ObjectMap of G))" by FUNCTOR0:def 36
.= (the ObjectMap of G)"*(the ObjectMap of F)" by A8,A12,FUNCT_1:44
.= (the ObjectMap of GI)*(the ObjectMap of F)" by A2,A3,FUNCTOR0:def 38
.= (the ObjectMap of GI)*(the ObjectMap of FI) by A1,A4,FUNCTOR0:def 38
.= the ObjectMap of (GI*FI) by FUNCTOR0:def 36;
hence thesis by A16;
end;