Copyright (c) 2001 Association of Mizar Users
environ
vocabulary RELAT_2, ALTCAT_1, MSUALG_6, FUNCTOR0, SGRAPH1, FUNCT_1, RELAT_1,
BOOLE, CAT_1, ENS_1, PARTFUN1, YELLOW18, CANTOR_1, PBOOLE, ALTCAT_2,
PRALG_1, FUNCT_3, MCART_1, MSUALG_3, WELLORD1, OPPCAT_1, YELLOW20;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, MCART_1, BINOP_1, MULTOP_1, STRUCT_0, FUNCT_4, PARTFUN1, PBOOLE,
MSUALG_1, PRALG_1, MSUALG_3, FUNCT_3, ALTCAT_1, ALTCAT_2, FUNCTOR0,
FUNCTOR3, YELLOW18;
constructors AMI_1, FUNCTOR3, YELLOW18;
clusters SUBSET_1, RELSET_1, RELAT_1, PRALG_1, STRUCT_0, MSUALG_1, ALTCAT_2,
FUNCTOR0, FUNCTOR2, ALTCAT_4, YELLOW18, FUNCT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_1, PARTFUN1, PBOOLE, MSUALG_1, MSUALG_3, ALTCAT_1,
ALTCAT_2, FUNCTOR0, FUNCT_2, XBOOLE_0;
theorems ZFMISC_1, RELAT_1, FUNCT_1, PBOOLE, MCART_1, STRUCT_0, GRFUNC_1,
FUNCT_2, BINOP_1, FUNCT_3, FUNCT_4, ALTCAT_1, ALTCAT_2, FUNCTOR3,
ALTCAT_4, FUNCTOR0, FUNCTOR1, FUNCTOR2, RELSET_1, PARTFUN1, MULTOP_1,
MSUALG_1, MSUALG_3, YELLOW18, XBOOLE_0, XBOOLE_1;
schemes FUNCT_1, YELLOW18;
begin :: Reverse functors
reserve x,y for set;
theorem Th1:
for A,B being transitive with_units (non empty AltCatStr)
for F being feasible reflexive FunctorStr over A,B
st F is coreflexive bijective
for a being object of A, b being object of B
holds F.a = b iff F".b = a
proof let A,B be transitive with_units (non empty AltCatStr);
let F be feasible reflexive FunctorStr over A,B such that
A1: F is coreflexive bijective;
let a be object of A, b be object of B;
F" * F = id A by A1,FUNCTOR1:22;
then a = (F" * F).a by FUNCTOR0:30;
hence F.a = b implies F".b = a by FUNCTOR0:34;
reconsider G = F" as feasible reflexive FunctorStr over B,A
by A1,FUNCTOR0:36,37;
F * G = id B by A1,FUNCTOR1:21;
then b = (F * G).b by FUNCTOR0:30;
hence thesis by FUNCTOR0:34;
end;
theorem Th2:
for A,B being transitive with_units (non empty AltCatStr)
for F being Covariant feasible FunctorStr over A,B
for G being Covariant feasible FunctorStr over B,A
st F is bijective & G = F"
for a1,a2 being object of A st <^a1,a2^> <> {}
for f being Morphism of a1,a2, g being Morphism of F.a1, F.a2
holds F.f = g iff G.g = f
proof let A,B be transitive with_units (non empty AltCatStr);
let F be Covariant feasible FunctorStr over A,B;
let G be Covariant feasible FunctorStr over B,A such that
A1: F is bijective & G = F";
let a1,a2 be object of A such that
A2: <^a1,a2^> <> {};
let f be Morphism of a1,a2, g be Morphism of F.a1, F.a2;
F" * F = id A by A1,FUNCTOR1:22;
then f = (G * F).f by A1,A2,FUNCTOR0:32;
hence F.f = g implies G.g = f by A2,FUNCTOR3:6;
A3: <^F.a1,F.a2^> <> {} by A2,FUNCTOR0:def 19;
F is surjective by A1,FUNCTOR0:def 36;
then F is onto by FUNCTOR0:def 35;
then F is reflexive coreflexive by FUNCTOR0:45;
then A4: G.(F.a1) = a1 & G.(F.a2) = a2 by A1,Th1;
F * G = id B by A1,FUNCTOR1:21;
then g = (F * G).g by A3,FUNCTOR0:32;
hence thesis by A3,A4,FUNCTOR3:6;
end;
theorem Th3:
for A,B being transitive with_units (non empty AltCatStr)
for F being Contravariant feasible FunctorStr over A,B
for G being Contravariant feasible FunctorStr over B,A
st F is bijective & G = F"
for a1,a2 being object of A st <^a1,a2^> <> {}
for f being Morphism of a1,a2, g being Morphism of F.a2, F.a1
holds F.f = g iff G.g = f
proof let A,B be transitive with_units (non empty AltCatStr);
let F be Contravariant feasible FunctorStr over A,B;
let G be Contravariant feasible FunctorStr over B,A such that
A1: F is bijective & G = F";
let a1,a2 be object of A such that
A2: <^a1,a2^> <> {};
let f be Morphism of a1,a2, g be Morphism of F.a2, F.a1;
F" * F = id A by A1,FUNCTOR1:22;
then f = (G * F).f by A1,A2,FUNCTOR0:32;
hence F.f = g implies G.g = f by A2,FUNCTOR3:7;
A3: <^F.a2,F.a1^> <> {} by A2,FUNCTOR0:def 20;
F is surjective by A1,FUNCTOR0:def 36;
then F is onto by FUNCTOR0:def 35;
then F is reflexive coreflexive by FUNCTOR0:46;
then A4: G.(F.a1) = a1 & G.(F.a2) = a2 by A1,Th1;
F * G = id B by A1,FUNCTOR1:21;
then g = (F * G).g by A3,FUNCTOR0:32;
hence thesis by A3,A4,FUNCTOR3:7;
end;
theorem Th4:
for A,B being category, F being Functor of A,B st F is bijective
for G being Functor of B,A st F*G = id B
holds the FunctorStr of G = F"
proof let A,B be category, F be Functor of A,B; assume
A1: F is bijective;
then reconsider FF = F" as feasible FunctorStr over B,A by FUNCTOR0:36;
let G be Functor of B,A such that
A2: F * G = id B;
F"*F = id A by A1,FUNCTOR1:22;
then (id A)*G = FF * id B by A2,FUNCTOR0:33 .= F" by FUNCTOR3:5;
hence the FunctorStr of G = F" by FUNCTOR3:4;
end;
theorem Th5:
for A,B being category, F being Functor of A,B st F is bijective
for G being Functor of B,A st G*F = id A
holds the FunctorStr of G = F"
proof let A,B be category, F be Functor of A,B; assume
A1: F is bijective;
then reconsider FF = F" as feasible FunctorStr over B,A by FUNCTOR0:36;
let G be Functor of B,A such that
A2: G * F = id A;
F*FF = id B by A1,FUNCTOR1:21;
then (id A)*FF = G * id B by A2,FUNCTOR0:33
.= the FunctorStr of G by FUNCTOR3:5;
hence the FunctorStr of G = F" by FUNCTOR3:4;
end;
theorem
for A,B being category, F being covariant Functor of A,B st F is bijective
for G being covariant Functor of B,A st
(for b being object of B holds F.(G.b) = b) &
(for a,b being object of B st <^a,b^> <> {}
for f being Morphism of a,b holds F.(G.f) = f)
holds the FunctorStr of G = F"
proof let A,B be category, F be covariant Functor of A,B such that
A1: F is bijective;
let G be covariant Functor of B,A such that
A2: for b being object of B holds F.(G.b) = b and
A3: for a,b being object of B st <^a,b^> <> {}
for f being Morphism of a,b holds F.(G.f) = f;
A4: now let b be object of B;
thus (F*G).b = F.(G.b) by FUNCTOR0:34 .= b by A2
.= (id B).b by FUNCTOR0:30;
end;
now let a,b be object of B such that
A5: <^a,b^> <> {};
let f be Morphism of a,b;
thus (F*G).f = F.(G.f) by A5,FUNCTOR3:6 .= f by A3,A5
.= (id B).f by A5,FUNCTOR0:32;
end;
then F*G = id B by A4,YELLOW18:1;
hence thesis by A1,Th4;
end;
theorem
for A,B being category, F being contravariant Functor of A,B st F is
bijective
for G being contravariant Functor of B,A st
(for b being object of B holds F.(G.b) = b) &
(for a,b being object of B st <^a,b^> <> {}
for f being Morphism of a,b holds F.(G.f) = f)
holds the FunctorStr of G = F"
proof let A,B be category, F be contravariant Functor of A,B such that
A1: F is bijective;
let G be contravariant Functor of B,A such that
A2: for b being object of B holds F.(G.b) = b and
A3: for a,b being object of B st <^a,b^> <> {}
for f being Morphism of a,b holds F.(G.f) = f;
A4: now let b be object of B;
thus (F*G).b = F.(G.b) by FUNCTOR0:34 .= b by A2
.= (id B).b by FUNCTOR0:30;
end;
now let a,b be object of B such that
A5: <^a,b^> <> {};
let f be Morphism of a,b;
thus (F*G).f = F.(G.f) by A5,FUNCTOR3:7 .= f by A3,A5
.= (id B).f by A5,FUNCTOR0:32;
end;
then F*G = id B by A4,YELLOW18:1;
hence thesis by A1,Th4;
end;
theorem
for A,B being category, F being covariant Functor of A,B st F is bijective
for G being covariant Functor of B,A st
(for a being object of A holds G.(F.a) = a) &
(for a,b being object of A st <^a,b^> <> {}
for f being Morphism of a,b holds G.(F.f) = f)
holds the FunctorStr of G = F"
proof let A,B be category, F be covariant Functor of A,B such that
A1: F is bijective;
let G be covariant Functor of B,A such that
A2: for b being object of A holds G.(F.b) = b and
A3: for a,b being object of A st <^a,b^> <> {}
for f being Morphism of a,b holds G.(F.f) = f;
A4: now let b be object of A;
thus (G*F).b = G.(F.b) by FUNCTOR0:34 .= b by A2
.= (id A).b by FUNCTOR0:30;
end;
now let a,b be object of A such that
A5: <^a,b^> <> {};
let f be Morphism of a,b;
thus (G*F).f = G.(F.f) by A5,FUNCTOR3:6 .= f by A3,A5
.= (id A).f by A5,FUNCTOR0:32;
end;
then G*F = id A by A4,YELLOW18:1;
hence thesis by A1,Th5;
end;
theorem
for A,B being category, F being contravariant Functor of A,B st F is
bijective
for G being contravariant Functor of B,A st
(for a being object of A holds G.(F.a) = a) &
(for a,b being object of A st <^a,b^> <> {}
for f being Morphism of a,b holds G.(F.f) = f)
holds the FunctorStr of G = F"
proof let A,B be category, F be contravariant Functor of A,B such that
A1: F is bijective;
let G be contravariant Functor of B,A such that
A2: for b being object of A holds G.(F.b) = b and
A3: for a,b being object of A st <^a,b^> <> {}
for f being Morphism of a,b holds G.(F.f) = f;
A4: now let b be object of A;
thus (G*F).b = G.(F.b) by FUNCTOR0:34 .= b by A2
.= (id A).b by FUNCTOR0:30;
end;
now let a,b be object of A such that
A5: <^a,b^> <> {};
let f be Morphism of a,b;
thus (G*F).f = G.(F.f) by A5,FUNCTOR3:7 .= f by A3,A5
.= (id A).f by A5,FUNCTOR0:32;
end;
then G*F = id A by A4,YELLOW18:1;
hence thesis by A1,Th5;
end;
begin :: Intersection of categories
definition
let A, B be AltCatStr;
pred A, B have_the_same_composition means:
Def1:
for a1, a2, a3 being set holds
(the Comp of A).[a1,a2,a3] tolerates (the Comp of B).[a1,a2,a3];
symmetry;
end;
theorem Th10:
for A, B being AltCatStr holds
A,B have_the_same_composition
iff
for a1,a2,a3,x being set st
x in dom ((the Comp of A).[a1,a2,a3]) &
x in dom ((the Comp of B).[a1,a2,a3])
holds ((the Comp of A).[a1,a2,a3]).x = ((the Comp of B).[a1,a2,a3]).x
proof let A, B be AltCatStr;
hereby assume
A1: A,B have_the_same_composition;
let a1,a2,a3,x be set such that
A2: x in dom ((the Comp of A).[a1,a2,a3]) and
A3: x in dom ((the Comp of B).[a1,a2,a3]);
x in dom ((the Comp of A).[a1,a2,a3]) /\
dom ((the Comp of B).[a1,a2,a3]) &
(the Comp of A).[a1,a2,a3] tolerates (the Comp of B).[a1,a2,a3]
by A1,A2,A3,Def1,XBOOLE_0:def 3;
hence ((the Comp of A).[a1,a2,a3]).x = ((the Comp of B).[a1,a2,a3]).x
by PARTFUN1:def 6;
end;
assume
A4: for a1,a2,a3,x being set st
x in dom ((the Comp of A).[a1,a2,a3]) &
x in dom ((the Comp of B).[a1,a2,a3])
holds ((the Comp of A).[a1,a2,a3]).x = ((the Comp of B).[a1,a2,a3]).x;
let a1,a2,a3,x be set; assume
x in dom ((the Comp of A).[a1,a2,a3]) /\
dom ((the Comp of B).[a1,a2,a3]);
then x in dom ((the Comp of A).[a1,a2,a3]) &
x in dom ((the Comp of B).[a1,a2,a3]) by XBOOLE_0:def 3;
hence thesis by A4;
end;
theorem Th11:
for A, B being transitive non empty AltCatStr holds
A,B have_the_same_composition
iff
for a1,a2,a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {}
for b1,b2,b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} &
b1 = a1 & b2 = a2 & b3 = a3
for f1 being Morphism of a1,a2, g1 being Morphism of b1,b2 st g1 = f1
for f2 being Morphism of a2,a3, g2 being Morphism of b2,b3 st g2 = f2
holds f2 * f1 = g2 * g1
proof let A,B be transitive non empty AltCatStr;
hereby assume
A1: A,B have_the_same_composition;
let a1,a2,a3 be object of A such that
A2: <^a1,a2^> <> {} & <^a2,a3^> <> {};
let b1,b2,b3 be object of B such that
A3: <^b1,b2^> <> {} & <^b2,b3^> <> {} and
A4: b1 = a1 & b2 = a2 & b3 = a3;
let f1 be Morphism of a1,a2, g1 be Morphism of b1,b2 such that
A5: g1 = f1;
let f2 be Morphism of a2,a3, g2 be Morphism of b2,b3 such that
A6: g2 = f2;
A7: (the Comp of A).(a1,a2,a3) = (the Comp of A).[a1,a2,a3] &
(the Comp of B).(b1,b2,b3) = (the Comp of B).[b1,b2,b3]
by MULTOP_1:def 1;
(the Comp of A).(a1,a2,a3) is
Function of [:<^a2,a3^>,<^a1,a2^>:], <^a1,a3^> & <^a1,a3^> <> {} &
(the Comp of B).(b1,b2,b3) is
Function of [:<^b2,b3^>,<^b1,b2^>:], <^b1,b3^> & <^b1,b3^> <> {}
by A2,A3,ALTCAT_1:17,def 4;
then dom ((the Comp of A).(a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] &
dom ((the Comp of B).(b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:]
by FUNCT_2:def 1;
then A8: [f2,f1] in dom ((the Comp of A).(a1,a2,a3)) &
[g2,g1] in dom ((the Comp of B).(b1,b2,b3)) by A2,A3,ZFMISC_1:def 2;
thus f2 * f1 = (the Comp of A).(a1,a2,a3).(f2,f1) by A2,ALTCAT_1:def 10
.= (the Comp of A).[a1,a2,a3].[f2,f1] by A7,BINOP_1:def 1
.= (the Comp of B).[b1,b2,b3].[g2,g1] by A1,A4,A5,A6,A7,A8,Th10
.= (the Comp of B).(b1,b2,b3).(g2,g1) by A7,BINOP_1:def 1
.= g2 * g1 by A3,ALTCAT_1:def 10;
end;
assume
A9: for a1,a2,a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {}
for b1,b2,b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} &
b1 = a1 & b2 = a2 & b3 = a3
for f1 being Morphism of a1,a2, g1 being Morphism of b1,b2 st g1 = f1
for f2 being Morphism of a2,a3, g2 being Morphism of b2,b3 st g2 = f2
holds f2 * f1 = g2 * g1;
let a1,a2,a3,x be set; assume
x in dom ((the Comp of A).[a1,a2,a3]) /\
dom ((the Comp of B).[a1,a2,a3]);
then A10: x in dom ((the Comp of A).[a1,a2,a3]) &
x in dom ((the Comp of B).[a1,a2,a3]) by XBOOLE_0:def 3;
then [a1,a2,a3] in dom the Comp of A & [a1,a2,a3] in dom the Comp of B
by FUNCT_1:def 4,RELAT_1:60;
then [a1,a2,a3] in [:the carrier of A, the carrier of A, the carrier of A
:] &
[a1,a2,a3] in [:the carrier of B, the carrier of B, the carrier of B:]
by PBOOLE:def 3;
then A11: a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier
of A &
a1 in the carrier of B & a2 in the carrier of B & a3 in the carrier of B
by MCART_1:73;
then reconsider a1,a2,a3 as object of A;
reconsider b1 = a1, b2 = a2, b3 = a3 as object of B by A11;
A12: (the Comp of A).(a1,a2,a3) = (the Comp of A).[a1,a2,a3] &
(the Comp of B).(b1,b2,b3) = (the Comp of B).[b1,b2,b3]
by MULTOP_1:def 1;
A13: (the Comp of A).(a1,a2,a3) is
Function of [:<^a2,a3^>,<^a1,a2^>:], <^a1,a3^> &
(the Comp of B).(b1,b2,b3) is
Function of [:<^b2,b3^>,<^b1,b2^>:], <^b1,b3^> by ALTCAT_1:17;
then ([:<^a2,a3^>,<^a1,a2^>:] <> {} implies <^a1,a3^> <> {}) &
([:<^b2,b3^>,<^b1,b2^>:] <> {} implies <^b1,b3^> <> {})
by A10,A12,FUNCT_2:def 1,RELAT_1:60;
then A14: dom ((the Comp of A).(a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] &
dom ((the Comp of B).(b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:]
by A13,FUNCT_2:def 1;
then consider f2,f1 being set such that
A15: f2 in <^a2,a3^> & f1 in <^a1,a2^> & x = [f2,f1] by A10,A12,ZFMISC_1:def 2;
reconsider f2 as Morphism of a2,a3 by A15;
reconsider f1 as Morphism of a1,a2 by A15;
A16: f1 in <^b1,b2^> & f2 in <^b2,b3^> by A10,A12,A14,A15,ZFMISC_1:106;
then reconsider g1 = f1 as Morphism of b1,b2 ;
reconsider g2 = f2 as Morphism of b2,b3 by A16;
((the Comp of A).[a1,a2,a3]).x
= (the Comp of A).(a1,a2,a3).(f2,f1) by A12,A15,BINOP_1:def 1
.= f2 * f1 by A15,ALTCAT_1:def 10
.= g2 * g1 by A9,A15,A16
.= (the Comp of B).(b1,b2,b3).(g2,g1) by A16,ALTCAT_1:def 10;
hence thesis by A12,A15,BINOP_1:def 1;
end;
theorem
for A, B being para-functional semi-functional category holds
A, B have_the_same_composition
proof let A, B be para-functional semi-functional category;
now let a1,a2,a3 be object of A such that
A1: <^a1,a2^> <> {} & <^a2,a3^> <> {};
let b1,b2,b3 be object of B such that
A2: <^b1,b2^> <> {} & <^b2,b3^> <> {} and
b1 = a1 & b2 = a2 & b3 = a3;
let f1 be Morphism of a1,a2, g1 be Morphism of b1,b2 such that
A3: g1 = f1;
let f2 be Morphism of a2,a3, g2 be Morphism of b2,b3 such that
A4: g2 = f2;
reconsider f = f1 as Function of the_carrier_of a1, the_carrier_of a2
by A1,YELLOW18:35;
reconsider g = f2 as Function of the_carrier_of a2, the_carrier_of a3
by A1,YELLOW18:35;
A5: <^a1,a3^> <> {} & <^b1,b3^> <> {} by A1,A2,ALTCAT_1:def 4;
hence f2 * f1 = g * f by A1,ALTCAT_1:def 14
.= g2 * g1 by A2,A3,A4,A5,ALTCAT_1:def 14;
end;
hence thesis by Th11;
end;
definition
let f, g be Function;
func Intersect(f, g) -> Function means:
Def2:
dom it = (dom f) /\ (dom g) &
for x being set st x in (dom f) /\ (dom g) holds it.x = (f.x) /\ (g.x);
existence
proof deffunc F(set) = (f.$1) /\ (g.$1);
thus ex h being Function st
dom h = (dom f) /\ (dom g) &
for x being set st x in (dom f) /\ (dom g) holds h.x = F(x)
from Lambda;
end;
uniqueness
proof let f1,f2 be Function such that
A1: dom f1 = (dom f) /\ (dom g) and
A2: for x being set st x in (dom f) /\ (dom g) holds f1.x = (f.x) /\ (g.x) and
A3: dom f2 = (dom f) /\ (dom g) and
A4: for x being set st x in (dom f) /\ (dom g) holds f2.x = (f.x) /\ (g.x);
now let x be set; assume x in (dom f) /\ (dom g);
then f1.x = (f.x) /\ (g.x) & f2.x = (f.x) /\ (g.x) by A2,A4;
hence f1.x = f2.x;
end;
hence thesis by A1,A3,FUNCT_1:9;
end;
commutativity;
end;
theorem
for I being set, A,B being ManySortedSet of I
holds Intersect(A, B) = A /\ B
proof let I be set, A,B be ManySortedSet of I;
A1: dom A = I & dom B = I by PBOOLE:def 3;
then dom Intersect(A,B) = I /\ I by Def2;
then reconsider AB = Intersect(A,B) as ManySortedSet of I by PBOOLE:def 3;
I /\ I = I;
then for i being set st i in I holds AB.i = A.i /\ B.i by A1,Def2;
hence thesis by PBOOLE:def 8;
end;
theorem Th14:
for I,J being set
for A being ManySortedSet of I, B being ManySortedSet of J
holds Intersect(A, B) is ManySortedSet of I /\ J
proof let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J;
dom A = I & dom B = J by PBOOLE:def 3;
hence dom Intersect(A,B) = I /\ J by Def2;
end;
theorem Th15:
for I,J being set
for A being ManySortedSet of I, B being Function
for C being ManySortedSet of J st C = Intersect(A, B)
holds C cc= A
proof let I,J be set, A be ManySortedSet of I, B be Function;
let C be ManySortedSet of J such that
A1: C = Intersect(A, B);
A2: dom A = I & dom C = J by PBOOLE:def 3;
then A3: J = I /\ dom B by A1,Def2;
hence J c= I by XBOOLE_1:17;
let i be set; assume i in J;
then C.i = A.i /\ B.i by A1,A2,A3,Def2;
hence thesis by XBOOLE_1:17;
end;
theorem Th16:
for A1,A2, B1,B2 being set
for f being Function of A1,A2, g being Function of B1,B2
st f tolerates g
holds f /\ g is Function of A1 /\ B1, A2 /\ B2
proof let A1,A2, B1,B2 be set;
let f be Function of A1,A2, g be Function of B1,B2 such that
A1: f tolerates g;
(A1 = {} or A1 <> {}) & (A2 = {} or A2 <> {});
then A2: f = {} & (A1 = {} or A2 = {}) or
dom f = A1 & A1 <> {} & A2 <> {} by FUNCT_2:def 1,RELSET_1:26;
(B1 = {} or B1 <> {}) & (B2 = {} or B2 <> {});
then A3: g = {} & (B1 = {} or B2 = {}) or
dom g = B1 & B1 <> {} & B2 <> {} by FUNCT_2:def 1,RELSET_1:26;
A4: dom f c= A1 & rng f c= A2 & dom g c= B1 & rng g c= B2 by RELSET_1:12;
then A5: dom (f/\g) c= dom f /\ dom g & rng (f/\g) c= rng f /\ rng g &
dom f /\ dom g c= A1/\B1 & rng f /\ rng g c= A2/\B2
by RELAT_1:14,27,XBOOLE_1:27;
then A6: dom (f/\g) c= A1/\B1 & rng (f/\g) c= A2/\B2 by XBOOLE_1:1;
then A7: f /\ g is PartFunc of A1 /\ B1, A2 /\ B2 by GRFUNC_1:27,RELSET_1:11;
A8: now assume
A9: dom f = A1 & A1 <> {} & dom g = B1 & B1 <> {};
consider a being Element of A1 /\ B1;
hereby assume A1 /\ B1 <> {};
then f.a = g.a & a in A1 & a in B1 by A1,A9,PARTFUN1:def 6,XBOOLE_0:def
3;
then f.a in rng f & f.a in rng g by A9,FUNCT_1:def 5;
hence A2 /\ B2 <> {} by A4,XBOOLE_0:def 3;
end;
thus dom (f /\ g) = A1 /\ B1
proof thus dom (f /\ g) c= A1 /\ B1 by A5,XBOOLE_1:1;
let a be set; assume a in A1 /\ B1;
then f.a = g.a & a in A1 & a in B1
by A1,A9,PARTFUN1:def 6,XBOOLE_0:def 3;
then [a,f.a] in f & [a,f.a] in g by A9,FUNCT_1:def 4;
then [a,f.a] in f /\ g by XBOOLE_0:def 3;
hence thesis by RELAT_1:def 4;
end;
end;
now per cases;
case A2 /\ B2 <> {};
hence dom (f /\ g) = A1 /\ B1 by A2,A3,A8,RELAT_1:60;
case A1 /\ B1 = {};
hence dom (f /\ g) = A1 /\ B1 by A7,RELAT_1:60,RELSET_1:26;
case
A2 /\ B2 = {} & A1 /\ B1 <> {};
hence f /\ g = {} by A2,A3,A8;
end;
hence thesis by A6,FUNCT_2:def 1,GRFUNC_1:27,RELSET_1:11;
end;
theorem Th17:
for I1,I2 being set
for A1,B1 being ManySortedSet of I1
for A2,B2 being ManySortedSet of I2
for A,B being ManySortedSet of I1 /\ I2
st A = Intersect(A1, A2) & B = Intersect(B1, B2)
for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2
st for x being set st x in dom F & x in dom G holds F.x tolerates G.x
holds Intersect(F, G) is ManySortedFunction of A, B
proof let I1,I2 be set;
let A1,B1 be ManySortedSet of I1;
let A2,B2 be ManySortedSet of I2;
let A,B be ManySortedSet of I1 /\ I2 such that
A1: A = Intersect(A1, A2) & B = Intersect(B1, B2);
let F be ManySortedFunction of A1,B1;
let G be ManySortedFunction of A2,B2 such that
A2: for x being set st x in dom F & x in dom G holds F.x tolerates G.x;
reconsider H = Intersect(F, G) as ManySortedSet of I1 /\ I2 by Th14;
A3: dom F = I1 & dom G = I2 & dom A1 = I1 & dom A2 = I2 & dom A = I1 /\ I2 &
dom B1 = I1 & dom B2 = I2 & dom B = I1 /\ I2 by PBOOLE:def 3;
H is ManySortedFunction of A, B
proof let i be set; assume i in I1 /\ I2;
then A4: i in I1 & i in I2 & A.i = (A1.i)/\(A2.i) &
B.i = (B1.i)/\(B2.i) & H.i = (F.i)/\(G.i)
by A1,A3,Def2,XBOOLE_0:def 3;
then F.i is Function of A1.i, B1.i & G.i is Function of A2.i, B2.i &
F.i tolerates G.i by A2,A3,MSUALG_1:def 2;
hence H.i is Function of A.i, B.i by A4,Th16;
end;
hence thesis;
end;
theorem Th18:
for I,J being set
for F being ManySortedSet of [:I,I:]
for G being ManySortedSet of [:J,J:]
ex H being ManySortedSet of [:I/\J,I/\J:]
st H = Intersect(F, G) & Intersect({|F|}, {|G|}) = {|H|}
proof let I,J be set; let F be ManySortedSet of [:I,I:];
let G be ManySortedSet of [:J,J:];
A1: [:I/\J,I/\J:] = [:I,I:]/\[:J,J:] by ZFMISC_1:123;
then reconsider H = Intersect(F, G) as ManySortedSet of [:I/\J,I/\J:] by
Th14;
take H; thus H = Intersect(F, G);
A2: dom F = [:I,I:] & dom G = [:J,J:] & dom H = [:I/\J,I/\J:] &
dom {|F|} = [:I,I,I:] & dom {|G|} = [:J,J,J:] & dom {|H|} = [:I/\J,I/\J,I/\
J:]
by PBOOLE:def 3;
[:I,I,I:] = [:[:I,I:],I:] & [:J,J,J:] = [:[:J,J:],J:]
by ZFMISC_1:def 3;
then A3: [:I,I,I:]/\[:J,J,J:] = [:[:I/\J,I/\J:],I/\J:] by A1,ZFMISC_1:123
.= [:I/\J,I/\J,I/\J:] by ZFMISC_1:def 3;
now let x be set; assume x in [:I,I,I:]/\[:J,J,J:];
then A4: x in [:I,I,I:] & x in [:J,J,J:] by XBOOLE_0:def 3;
then consider a,b,c being set such that
A5: a in I & b in I & c in I & x = [a,b,c] by MCART_1:72;
A6: a in J & b in J & c in J by A4,A5,MCART_1:73;
then A7: a in I/\J & b in I/\J & c in I/\J by A5,XBOOLE_0:def 3;
then A8: [a,c] in [:I/\J,I/\J:] by ZFMISC_1:106;
A9: {|F|}.(a,b,c) = F.(a,c) & {|G|}.(a,b,c) = G.(a,c) &
{|H|}.(a,b,c) = H.(a,c) by A5,A6,A7,ALTCAT_1:def 5;
hence {|H|}.x = H.(a,c) by A5,MULTOP_1:def 1
.= H.[a,c] by BINOP_1:def 1
.= (F.[a,c])/\(G.[a,c]) by A1,A2,A8,Def2
.= (F.(a,c))/\(G.[a,c]) by BINOP_1:def 1
.= (F.(a,c))/\(G.(a,c)) by BINOP_1:def 1
.= ({|F|}.x)/\(G.(a,c)) by A5,A9,MULTOP_1:def 1
.= {|F|}.x /\ {|G|}.x by A5,A9,MULTOP_1:def 1;
end;
hence thesis by A2,A3,Def2;
end;
theorem Th19:
for I,J being set
for F1,F2 being ManySortedSet of [:I,I:]
for G1,G2 being ManySortedSet of [:J,J:]
ex H1,H2 being ManySortedSet of [:I/\J,I/\J:]
st H1 = Intersect(F1, G1) & H2 = Intersect(F2, G2) &
Intersect({|F1,F2|}, {|G1,G2|}) = {|H1, H2|}
proof let I,J be set; let F1,F2 be ManySortedSet of [:I,I:];
let G1,G2 be ManySortedSet of [:J,J:];
A1: [:I/\J,I/\J:] = [:I,I:]/\[:J,J:] by ZFMISC_1:123;
then reconsider H1 = Intersect(F1, G1), H2 = Intersect(F2, G2)
as ManySortedSet of [:I/\J,I/\J:] by Th14;
take H1, H2; thus H1 = Intersect(F1, G1) & H2 = Intersect(F2, G2);
A2: dom F1 = [:I,I:] & dom G1 = [:J,J:] & dom H1 = [:I/\J,I/\J:] &
dom F2 = [:I,I:] & dom G2 = [:J,J:] & dom H2 = [:I/\J,I/\J:] &
dom {|F1, F2|} = [:I,I,I:] & dom {|G1, G2|} = [:J,J,J:] &
dom {|H1, H2|} = [:I/\J,I/\J,I/\J:]
by PBOOLE:def 3;
[:I,I,I:] = [:[:I,I:],I:] & [:J,J,J:] = [:[:J,J:],J:]
by ZFMISC_1:def 3;
then A3: [:I,I,I:]/\[:J,J,J:] = [:[:I/\J,I/\J:],I/\J:] by A1,ZFMISC_1:123
.= [:I/\J,I/\J,I/\J:] by ZFMISC_1:def 3;
now let x be set; assume x in [:I,I,I:]/\[:J,J,J:];
then A4: x in [:I,I,I:] & x in [:J,J,J:] by XBOOLE_0:def 3;
then consider a,b,c being set such that
A5: a in I & b in I & c in I & x = [a,b,c] by MCART_1:72;
A6: a in J & b in J & c in J by A4,A5,MCART_1:73;
then A7: a in I/\J & b in I/\J & c in I/\J by A5,XBOOLE_0:def 3;
then A8: [a,b] in [:I/\J,I/\J:] & [b,c] in [:I/\J,I/\J:] by ZFMISC_1:106;
A9: H1.(a,b) = H1.[a,b] & H2.(b,c) = H2.[b,c] by BINOP_1:def 1;
A10: F1.(a,b) = F1.[a,b] & F2.(b,c) = F2.[b,c] by BINOP_1:def 1;
A11: G1.(a,b) = G1.[a,b] & G2.(b,c) = G2.[b,c] by BINOP_1:def 1;
A12: {|F1, F2|}.(a,b,c) = [:F2.(b,c),F1.(a,b):] &
{|G1, G2|}.(a,b,c) = [:G2.(b,c),G1.(a,b):] &
{|H1, H2|}.(a,b,c) = [:H2.(b,c),H1.(a,b):] by A5,A6,A7,ALTCAT_1:def 6;
hence {|H1, H2|}.x = [:H2.(b,c),H1.(a,b):] by A5,MULTOP_1:def 1
.= [:(F2.[b,c])/\(G2.[b,c]), H1.(a,b):] by A1,A2,A8,A9,Def2
.= [:(F2.[b,c])/\(G2.[b,c]), (F1.[a,b])/\(G1.[a,b]):]
by A1,A2,A8,A9,Def2
.= [:F2.[b,c],F1.[a,b]:]/\[:G2.[b,c],G1.[a,b]:] by ZFMISC_1:123
.= ({|F1,F2|}.x)/\[:G2.[b,c],G1.[a,b]:] by A5,A10,A12,MULTOP_1:def 1
.= {|F1,F2|}.x /\ {|G1,G2|}.x by A5,A11,A12,MULTOP_1:def 1;
end;
hence thesis by A2,A3,Def2;
end;
definition
let A, B be AltCatStr such that
A1: A, B have_the_same_composition;
func Intersect(A, B) -> strict AltCatStr means:
Def3:
the carrier of it = (the carrier of A) /\ (the carrier of B) &
the Arrows of it = Intersect(the Arrows of A, the Arrows of B) &
the Comp of it = Intersect(the Comp of A, the Comp of B);
existence
proof
set Cr = (the carrier of A) /\ (the carrier of B);
A2: [:Cr, Cr:] = [:the carrier of A, the carrier of A:] /\
[:the carrier of B, the carrier of B:] by ZFMISC_1:123;
consider Ar being ManySortedSet of [:Cr,Cr:] such that
A3: Ar = Intersect(the Arrows of A, the Arrows of B) and
A4: Intersect({|the Arrows of A|}, {|the Arrows of B|}) = {|Ar|} by Th18;
consider Ar1,Ar2 being ManySortedSet of [:Cr,Cr:] such that
A5: Ar1 = Intersect(the Arrows of A, the Arrows of B) &
Ar2 = Intersect(the Arrows of A, the Arrows of B) and
A6: Intersect({|the Arrows of A, the Arrows of A|},
{|the Arrows of B, the Arrows of B|}) = {|Ar1,Ar2|} by Th19;
[:the carrier of A, the carrier of A, the carrier of A:] =
[:[:the carrier of A, the carrier of A:], the carrier of A:] &
[:the carrier of B, the carrier of B, the carrier of B:] =
[:[:the carrier of B, the carrier of B:], the carrier of B:]
by ZFMISC_1:def 3;
then A7: [:the carrier of A, the carrier of A, the carrier of A:] /\
[:the carrier of B, the carrier of B, the carrier of B:]
= [:[:Cr, Cr:], Cr:] by A2,ZFMISC_1:123
.= [:Cr, Cr, Cr:] by ZFMISC_1:def 3;
A8: dom the Comp of A =
[:the carrier of A, the carrier of A, the carrier of A:] &
dom the Comp of B =
[:the carrier of B, the carrier of B, the carrier of B:]
by PBOOLE:def 3;
now let x be set; assume x in dom the Comp of A;
then consider a1,a2,a3 being set such that
a1 in the carrier of A & a2 in the carrier of A &
a3 in the carrier of A and
A9: x = [a1,a2,a3] by A8,MCART_1:72;
assume x in dom the Comp of B;
thus (the Comp of A).x tolerates (the Comp of B).x by A1,A9,Def1;
end;
then reconsider Cm = Intersect(the Comp of A, the Comp of B) as
ManySortedFunction of {|Ar,Ar|}, {|Ar|} by A3,A4,A5,A6,A7,Th17;
take AltCatStr(#Cr,Ar,Cm#);
thus thesis by A3;
end;
uniqueness;
end;
theorem
for A, B being AltCatStr st A, B have_the_same_composition
holds Intersect(A, B) = Intersect(B, A)
proof let A,B be AltCatStr; set AB = Intersect(A,B);
assume
A1: A, B have_the_same_composition;
then the carrier of AB = (the carrier of A) /\ (the carrier of B) &
the Arrows of AB = Intersect(the Arrows of A, the Arrows of B) &
the Comp of AB = Intersect(the Comp of A, the Comp of B) by Def3;
hence thesis by A1,Def3;
end;
theorem Th21:
for A, B being AltCatStr st A, B have_the_same_composition
holds Intersect(A, B) is SubCatStr of A
proof let A,B be AltCatStr; set AB = Intersect(A,B);
assume A, B have_the_same_composition;
then the carrier of AB = (the carrier of A) /\ (the carrier of B) &
the Arrows of AB = Intersect(the Arrows of A, the Arrows of B) &
the Comp of AB = Intersect(the Comp of A, the Comp of B) by Def3;
hence the carrier of AB c= the carrier of A &
the Arrows of AB cc= the Arrows of A &
the Comp of AB cc= the Comp of A by Th15,XBOOLE_1:17;
end;
theorem Th22:
for A, B being AltCatStr st A, B have_the_same_composition
for a1,a2 being object of A, b1,b2 being object of B
for o1, o2 being object of Intersect(A, B)
st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2
holds <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
proof let A, B be AltCatStr such that
A1: A, B have_the_same_composition;
let a1,a2 be object of A, b1,b2 be object of B;
let o1, o2 be object of Intersect(A, B) such that
A2: o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2;
A3: the carrier of Intersect(A, B) = (the carrier of A)/\(the carrier of B) &
the Arrows of Intersect(A,B) = Intersect(the Arrows of A, the Arrows of B)
by A1,Def3;
then A4: [:the carrier of Intersect(A, B), the carrier of Intersect(A, B):] =
[:the carrier of A, the carrier of A:] /\
[:the carrier of B, the carrier of B:] by ZFMISC_1:123;
A5: dom the Arrows of A = [:the carrier of A, the carrier of A:] &
dom the Arrows of B = [:the carrier of B, the carrier of B:] &
dom the Arrows of Intersect(A,B) =
[:the carrier of Intersect(A, B), the carrier of Intersect(A, B):]
by PBOOLE:def 3;
A6: now assume the carrier of A <> {} & the carrier of B <> {};
then [a1,a2] in [:the carrier of A, the carrier of A:] &
[b1,b2] in [:the carrier of B, the carrier of B:] by ZFMISC_1:def 2;
hence [o1,o2] in
[:the carrier of Intersect(A, B), the carrier of Intersect(A, B):]
by A2,A4,XBOOLE_0:def 3;
end;
A7: now assume the carrier of A = {} or the carrier of B = {};
then [:the carrier of A, the carrier of A:] = {} or
[:the carrier of B, the carrier of B:] = {} by ZFMISC_1:113;
then [:the carrier of Intersect(A, B), the carrier of Intersect(A, B):]
= {} &
((the Arrows of A).[a1,a2] = {} or (the Arrows of B).[b1,b2] = {})
by A4,A5,FUNCT_1:def 4;
hence (the Arrows of A).[a1,a2] /\ (the Arrows of B).[b1,b2] = {} &
(the Arrows of Intersect(A,B)).[o1,o2] = {} by A5,FUNCT_1:def 4;
end;
thus <^o1,o2^> = (the Arrows of Intersect(A, B)).(o1,o2) by ALTCAT_1:def 2
.= (the Arrows of Intersect(A, B)).[o1,o2] by BINOP_1:def 1
.= (the Arrows of A).[a1,a2] /\ (the Arrows of B).[b1,b2]
by A2,A3,A4,A5,A6,A7,Def2
.= (the Arrows of A).(a1,a2) /\ (the Arrows of B).[b1,b2] by BINOP_1:def 1
.= <^a1,a2^> /\ (the Arrows of B).[b1,b2] by ALTCAT_1:def 2
.= <^a1,a2^> /\ (the Arrows of B).(b1,b2) by BINOP_1:def 1
.= <^a1,a2^> /\ <^b1,b2^> by ALTCAT_1:def 2;
end;
theorem Th23:
for A, B being transitive AltCatStr st A, B have_the_same_composition
holds Intersect(A, B) is transitive
proof let A,B be transitive AltCatStr; set AB = Intersect(A,B);
assume
A1: A, B have_the_same_composition;
then A2: the carrier of AB = (the carrier of A) /\ (the carrier of B) &
the Arrows of AB = Intersect(the Arrows of A, the Arrows of B) &
the Comp of AB = Intersect(the Comp of A, the Comp of B) by Def3;
let o1,o2,o3 be object of AB such that
A3: <^o1,o2^> <> {} & <^o2,o3^> <> {};
A4: dom the Arrows of AB = [:the carrier of AB, the carrier of AB:]
by PBOOLE:def 3;
<^o1,o2^> = (the Arrows of AB).(o1,o2) &
<^o2,o3^> = (the Arrows of AB).(o2,o3) by ALTCAT_1:def 2;
then <^o1,o2^> = (the Arrows of AB).[o1,o2] &
<^o2,o3^> = (the Arrows of AB).[o2,o3] by BINOP_1:def 1;
then [o1,o2] in dom the Arrows of AB & [o2,o3] in dom the Arrows of AB
by A3,FUNCT_1:def 4;
then o1 in the carrier of AB & o2 in the carrier of AB & o3 in the carrier
of AB
by A4,ZFMISC_1:106;
then A5: o1 in the carrier of A & o2 in the carrier of A & o3 in the carrier of
A &
o1 in the carrier of B & o2 in the carrier of B & o3 in the carrier of B
by A2,XBOOLE_0:def 3;
then reconsider A, B as non empty transitive AltCatStr by STRUCT_0:def 1;
reconsider a1=o1, a2=o2, a3=o3 as object of A by A5;
reconsider b1=o1, b2=o2, b3=o3 as object of B by A5;
A6: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> & <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> &
<^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> by A1,Th22;
then <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^b1,b2^> <> {} & <^b2,b3^> <> {}
by A3;
then A7: <^a1,a3^> <> {} & <^b1,b3^> <> {} by ALTCAT_1:def 4;
consider f being Morphism of o1,o2, g being Morphism of o2,o3;
A8: f in <^a1,a2^> & f in <^b1,b2^> & g in <^a2,a3^> & g in <^b2,b3^>
by A3,A6,XBOOLE_0:def 3;
then reconsider f1 = f as Morphism of a1,a2 ;
reconsider f2 = f as Morphism of b1,b2 by A8;
reconsider g1 = g as Morphism of a2,a3 by A8;
reconsider g2 = g as Morphism of b2,b3 by A8;
g1 * f1 = g2 * f2 by A1,A8,Th11;
hence <^o1,o3^> <> {} by A6,A7,XBOOLE_0:def 3;
end;
theorem Th24:
for A, B being AltCatStr
st A, B have_the_same_composition
for a1,a2 being object of A, b1,b2 being object of B
for o1,o2 being object of Intersect(A, B)
st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 &
<^a1,a2^> <> {} & <^b1,b2^> <> {}
for f being Morphism of a1,a2, g being Morphism of b1,b2 st f = g
holds f in <^o1,o2^>
proof let A, B be AltCatStr such that
A1: A, B have_the_same_composition;
let a1,a2 be object of A, b1,b2 be object of B;
let o1,o2 be object of Intersect(A, B);
assume o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2;
then <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1,Th22;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th25:
for A, B being with_units (non empty AltCatStr)
st A, B have_the_same_composition
for a being object of A, b being object of B
for o being object of Intersect(A, B)
st o = a & o = b & idm a = idm b
holds idm a in <^o,o^> by Th24;
theorem
for A, B being category
st A, B have_the_same_composition &
Intersect(A,B) is non empty &
for a being object of A, b being object of B st a = b holds idm a = idm b
holds Intersect(A, B) is subcategory of A
proof let A,B be category such that
A1: A, B have_the_same_composition and
A2: Intersect(A,B) is non empty and
A3: for a being object of A, b being object of B st a = b holds idm a = idm b;
reconsider AB = Intersect(A,B) as transitive non empty SubCatStr of A
by A1,A2,Th21,Th23;
A4: the carrier of AB = (the carrier of A) /\ (the carrier of B) by A1,Def3;
now let o be object of AB, a be object of A; assume
A5: o = a;
o in the carrier of B by A4,XBOOLE_0:def 3;
then reconsider b = o as object of B;
idm a = idm b by A3,A5;
hence idm a in <^o,o^> by A1,A5,Th25;
end;
hence thesis by ALTCAT_2:def 14;
end;
begin :: Subcategories
scheme SubcategoryUniq
{ A() -> category,
B1, B2() -> non empty subcategory of A(),
P[set], Q[set,set,set]}:
the AltCatStr of B1() = the AltCatStr of B2()
provided
A1: for a being object of A() holds a is object of B1() iff P[a] and
A2: for a,b being object of A(), a',b' being object of B1()
st a' = a & b' = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a',b'^> iff Q[a,b,f] and
A3: for a being object of A() holds a is object of B2() iff P[a] and
A4: for a,b being object of A(), a',b' being object of B2()
st a' = a & b' = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a',b'^> iff Q[a,b,f]
proof
A5: the carrier of B1() c= the carrier of A() &
the carrier of B2() c= the carrier of A() by ALTCAT_2:def 11;
A6: the carrier of B1() = the carrier of B2()
proof
hereby let x be set; assume
A7: x in the carrier of B1();
then reconsider a = x as object of B1();
reconsider a as object of A() by A5,A7;
P[a] by A1;
then a is object of B2() by A3;
hence x in the carrier of B2();
end;
let x be set; assume
A8: x in the carrier of B2();
then reconsider a = x as object of B2();
reconsider a as object of A() by A5,A8;
P[a] by A3;
then a is object of B1() by A1;
hence x in the carrier of B1();
end;
now let a,b be Element of B1();
reconsider x1 = a, y1 = b as object of B1();
reconsider x2 = x1, y2 = y1 as object of B2() by A6;
x1 in the carrier of B1() & y1 in the carrier of B1();
then reconsider a' = a, b' = b as object of A() by A5;
A9: <^x1,y1^> c= <^a',b'^> & <^x2,y2^> c= <^a',b'^> by ALTCAT_2:32;
A10: <^x1,y1^> c= <^x2,y2^>
proof let f be set; assume
A11: f in <^x1,y1^>;
then reconsider f as Morphism of a',b' by A9;
Q[a',b',f] by A2,A9,A11;
hence thesis by A4,A9,A11;
end;
A12: <^x2,y2^> c= <^x1,y1^>
proof let f be set; assume
A13: f in <^x2,y2^>;
then reconsider f as Morphism of a',b' by A9;
Q[a',b',f] by A4,A9,A13;
hence thesis by A2,A9,A13;
end;
thus (the Arrows of B1()).(a,b)
= <^x1,y1^> by ALTCAT_1:def 2
.= <^x2,y2^> by A10,A12,XBOOLE_0:def 10
.= (the Arrows of B2()).(a,b) by ALTCAT_1:def 2;
end;
then the Arrows of B1() = the Arrows of B2() by A6,ALTCAT_1:9;
hence thesis by A6,ALTCAT_2:27;
end;
theorem Th27:
for A being non empty AltCatStr, B being non empty SubCatStr of A holds
B is full iff
for a1,a2 being object of A, b1,b2 being object of B st b1 = a1 & b2 = a2
holds <^b1,b2^> = <^a1,a2^>
proof let A be non empty AltCatStr, B be non empty SubCatStr of A;
thus B is full implies
for a1,a2 being object of A, b1,b2 being object of B st b1 = a1 & b2 = a2
holds <^b1,b2^> = <^a1,a2^> by ALTCAT_2:29;
assume
A1: for a1,a2 being object of A, b1,b2 being object of B st b1 = a1 & b2 = a2
holds <^b1,b2^> = <^a1,a2^>;
A2: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
then [:the carrier of B, the carrier of B:] c=
[:the carrier of A, the carrier of A:] by ZFMISC_1:119;
then A3: [:the carrier of A, the carrier of A:] /\
[:the carrier of B, the carrier of B:]
= [:the carrier of B, the carrier of B:] by XBOOLE_1:28;
A4: dom the Arrows of A = [:the carrier of A, the carrier of A:] &
dom the Arrows of B = [:the carrier of B, the carrier of B:]
by PBOOLE:def 3;
now let x be set; assume x in dom the Arrows of B;
then consider b1,b2 being set such that
A5: b1 in the carrier of B & b2 in the carrier of B & x = [b1,b2]
by A4,ZFMISC_1:def 2;
reconsider b1, b2 as object of B by A5;
reconsider a1 = b1, a2 = b2 as object of A by A2,A5;
thus (the Arrows of B).x = (the Arrows of B).(b1,b2) by A5,BINOP_1:def 1
.= <^b1,b2^> by ALTCAT_1:def 2 .= <^a1,a2^> by A1
.= (the Arrows of A).(a1,a2) by ALTCAT_1:def 2
.= (the Arrows of A).x by A5,BINOP_1:def 1;
end;
hence the Arrows of B = (the Arrows of A)|
[:the carrier of B, the carrier of B:] by A3,A4,FUNCT_1:68;
end;
scheme FullSubcategoryEx
{ A() -> category, P[set]}:
ex B being strict full non empty subcategory of A() st
for a being object of A() holds a is object of B iff P[a]
provided
A1: ex a being object of A() st P[a]
proof defpred p[set] means P[$1];
defpred Q[set,set,set] means not contradiction;
A2: ex a being object of A() st p[a] by A1;
A3: for a,b,c being object of A()
st p[a] & p[b] & p[c] & <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
st Q[a,b,f] & Q[b,c,g]
holds Q[a,c,g*f];
A4: for a being object of A() st p[a] holds Q[a,a, idm a];
consider B being strict non empty subcategory of A() such that
A5: for a being object of A() holds a is object of B iff p[a] and
A6: for a,b being object of A(), a',b' being object of B
st a' = a & b' = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a',b'^> iff Q[a,b,f]
from SubcategoryEx(A2,A3,A4);
now let a1,a2 be object of A(), b1,b2 be object of B; assume
A7: b1 = a1 & b2 = a2;
then A8: <^b1,b2^> c= <^a1,a2^> by ALTCAT_2:32;
<^a1,a2^> c= <^b1,b2^>
proof let f be set; assume f in <^a1,a2^>;
hence thesis by A6,A7;
end;
hence <^b1,b2^> = <^a1,a2^> by A8,XBOOLE_0:def 10;
end;
then B is full by Th27;
hence thesis by A5;
end;
scheme FullSubcategoryUniq
{ A() -> category,
B1, B2() -> full non empty subcategory of A(),
P[set]}:
the AltCatStr of B1() = the AltCatStr of B2()
provided
A1: for a being object of A() holds a is object of B1() iff P[a] and
A2: for a being object of A() holds a is object of B2() iff P[a]
proof defpred p[set] means P[$1];
A3: for a being object of A() holds a is object of B1() iff p[a] by A1;
A4: for a being object of A() holds a is object of B2() iff p[a] by A2;
defpred Q[set,set,set] means not contradiction;
A5: now let a,b be object of A(), a',b' be object of B1();
assume a' = a & b' = b; then <^a',b'^> = <^a,b^> by Th27;
hence <^a,b^> <> {} implies
for f being Morphism of a,b holds f in <^a',b'^> iff Q[a,b,f];
end;
A6: now let a,b be object of A(), a',b' be object of B2();
assume a' = a & b' = b; then <^a',b'^> = <^a,b^> by Th27;
hence <^a,b^> <> {} implies
for f being Morphism of a,b holds f in <^a',b'^> iff Q[a,b,f];
end;
thus thesis from SubcategoryUniq(A3,A5,A4,A6);
end;
begin :: Inclusion functors and functor restrictions
definition
let f be Function-yielding Function;
let x,y be set;
cluster f.(x,y) -> Relation-like Function-like;
coherence
proof f.(x,y) = f.[x,y] by BINOP_1:def 1;
hence thesis;
end;
end;
theorem Th28:
for A being category, C being non empty subcategory of A
for a,b being object of C st <^a,b^> <> {}
for f being Morphism of a,b holds (incl C).f = f
proof let A be category, C be non empty subcategory of A;
A1: the MorphMap of incl C = id the Arrows of C by FUNCTOR0:def 29;
let a,b be object of C such that
A2: <^a,b^> <> {};
let f be Morphism of a,b;
A3: [a,b] in [:the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
<^a,b^> c= <^(incl C).a, (incl C).b^> by FUNCTOR0:29;
then <^(incl C).a, (incl C).b^> <> {} by A2,XBOOLE_1:3;
hence (incl C).f = Morph-Map(incl C, a, b).f by A2,FUNCTOR0:def 16
.= ((id the Arrows of C).(a,b)).f by A1,FUNCTOR0:def 15
.= ((id the Arrows of C).[a,b]).f by BINOP_1:def 1
.= (id ((the Arrows of C).[a,b])).f by A3,MSUALG_3:def 1
.= (id ((the Arrows of C).(a,b))).f by BINOP_1:def 1
.= (id <^a,b^>).f by ALTCAT_1:def 2
.= f by A2,FUNCT_1:35;
end;
definition
let A be category;
let C be non empty subcategory of A;
cluster incl C -> id-preserving comp-preserving;
coherence
proof
thus incl C is id-preserving
proof let a be object of C;
A2: (incl C).a = a by FUNCTOR0:28;
thus Morph-Map(incl C, a, a).idm a = (incl C).idm a by FUNCTOR0:def 16
.= idm a by Th28
.= idm ((incl C).a) by A2,ALTCAT_2:35;
end;
let o1,o2,o3 be object of C such that
A3: <^o1,o2^> <> {} & <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
<^o1,o3^> <> {} by A3,ALTCAT_1:def 4;
then (incl C).o1 = o1 & (incl C).o2 = o2 & (incl C).o3 = o3 &
(incl C).g = g & (incl C).f = f & (incl C).(g*f) = g*f
by A3,Th28,FUNCTOR0:28;
hence (incl C).(g*f) = ((incl C).g)*((incl C).f) by A3,ALTCAT_2:33;
end;
end;
definition
let A be category;
let C be non empty subcategory of A;
cluster incl C -> Covariant;
coherence;
end;
definition
let A be category;
let C be non empty subcategory of A;
redefine func incl C -> strict covariant Functor of C,A;
coherence by FUNCTOR0:def 26,def 27;
end;
definition
let A,B be category;
let C be non empty subcategory of A;
let F be covariant Functor of A,B;
redefine func F|C -> strict covariant Functor of C,B;
coherence
proof F|C = F*incl C by FUNCTOR0:def 38;
hence thesis;
end;
end;
definition
let A,B be category;
let C be non empty subcategory of A;
let F be contravariant Functor of A,B;
redefine func F|C -> strict contravariant Functor of C,B;
coherence
proof F|C = F*incl C by FUNCTOR0:def 38;
hence thesis;
end;
end;
theorem Th29:
for A,B being category, C being non empty subcategory of A
for F being FunctorStr over A,B
for a being object of A, c being object of C st c = a
holds (F|C).c = F.a
proof let A,B be category, C be non empty subcategory of A;
let F be FunctorStr over A,B;
A1: F|C = F*incl C by FUNCTOR0:def 38;
let b be object of A;
let a be object of C;
assume a = b;
then (incl C).a = b by FUNCTOR0:28;
hence (F|C).a = F.b by A1,FUNCTOR0:34;
end;
theorem Th30:
for A,B being category, C being non empty subcategory of A
for F being covariant Functor of A,B
for a,b being object of A, c,d being object of C
st c = a & d = b & <^c,d^> <> {}
for f being Morphism of a,b for g being Morphism of c,d st g = f
holds (F|C).g = F.f
proof let A,B be category, C be non empty subcategory of A;
let F be covariant Functor of A,B;
A1: F|C = F*incl C by FUNCTOR0:def 38;
let a,b be object of A;
let c,d be object of C;
assume
A2: c = a & d = b & <^c,d^> <> {};
then A3: (incl C).c = a & (incl C).d = b by FUNCTOR0:28;
let f be Morphism of a,b; let g be Morphism of c,d;
assume g = f;
then (incl C).g = f by A2,Th28;
hence (F|C).g = F.f by A1,A2,A3,FUNCTOR3:6;
end;
theorem Th31:
for A,B being category, C being non empty subcategory of A
for F being contravariant Functor of A,B
for a,b being object of A, c,d being object of C
st c = a & d = b & <^c,d^> <> {}
for f being Morphism of a,b for g being Morphism of c,d st g = f
holds (F|C).g = F.f
proof let A,B be category, C be non empty subcategory of A;
let F be contravariant Functor of A,B;
A1: F|C = F*incl C by FUNCTOR0:def 38;
let a,b be object of A;
let c,d be object of C;
assume
A2: c = a & d = b & <^c,d^> <> {};
then A3: (incl C).c = a & (incl C).d = b by FUNCTOR0:28;
let f be Morphism of a,b; let g be Morphism of c,d;
assume g = f;
then (incl C).g = f by A2,Th28;
hence (F|C).g = F.f by A1,A2,A3,FUNCTOR3:8;
end;
theorem Th32:
for A,B being non empty AltGraph
for F being BimapStr over A,B st F is Covariant one-to-one
for a,b being object of A
st F.a = F.b holds a = b
proof let A,B be non empty AltGraph;
let F be BimapStr over A,B;
given f being Function of the carrier of A, the carrier of B such that
A1: the ObjectMap of F = [:f,f:];
assume the ObjectMap of F is one-to-one;
then A2: f is one-to-one by A1,FUNCTOR0:8;
let a,b be object of A such that
A3: F.a = F.b;
(the ObjectMap of F).(a,a) = (the ObjectMap of F).[a,a] &
(the ObjectMap of F).(b,b) = (the ObjectMap of F).[b,b]
by BINOP_1:def 1;
then A4: (the ObjectMap of F).(a,a) = [f.a, f.a] &
(the ObjectMap of F).(b,b) = [f.b, f.b] by A1,FUNCT_3:96;
[f.a,f.a]`1 = f.a & [f.b,f.b]`1 = f.b by MCART_1:7;
then F.a = f.a & F.b = f.b by A4,FUNCTOR0:def 6;
hence thesis by A2,A3,FUNCT_2:25;
end;
theorem Th33:
for A,B being non empty reflexive AltGraph
for F being feasible Covariant FunctorStr over A,B st F is faithful
for a,b being object of A st <^a,b^> <> {}
for f,g being Morphism of a,b
st F.f = F.g holds f = g
proof let A,B be non empty reflexive AltGraph;
let F be feasible Covariant FunctorStr over A,B such that
A1: for i being set, f being Function
st i in dom the MorphMap of F & (the MorphMap of F).i = f
holds f is one-to-one;
let a,b be object of A such that
A2: <^a,b^> <> {};
let f,g be Morphism of a,b;
A3: <^F.a, F.b^> <> {} by A2,FUNCTOR0:def 19;
then A4: F.f = Morph-Map(F,a,b).f & F.g = Morph-Map(F,a,b).g by A2,FUNCTOR0:def
16;
A5: dom the MorphMap of F = [:the carrier of A, the carrier of A:] &
[a,b] in [:the carrier of A, the carrier of A:]
by PBOOLE:def 3,ZFMISC_1:def 2;
Morph-Map(F,a,b) = (the MorphMap of F).(a,b) by FUNCTOR0:def 15
.= (the MorphMap of F).[a,b] by BINOP_1:def 1;
then Morph-Map(F,a,b) is one-to-one & f in <^a,b^> & g in <^a,b^> by A1,A2,
A5;
hence thesis by A3,A4,FUNCT_2:25;
end;
theorem Th34:
for A,B being non empty AltGraph
for F being Covariant FunctorStr over A,B st F is surjective
for a,b being object of B st <^a,b^> <> {}
for f being Morphism of a,b
ex c,d being object of A, g being Morphism of c,d st
a = F.c & b = F.d & <^c,d^> <> {} & f = F.g
proof let A,B be non empty AltGraph;
let F be Covariant FunctorStr over A,B;
given f being ManySortedFunction of
the Arrows of A, (the Arrows of B)*the ObjectMap of F such that
A1: f = the MorphMap of F & f is "onto";
assume
A2: rng the ObjectMap of F = [:the carrier of B, the carrier of B:];
A3: dom the ObjectMap of F = [:the carrier of A, the carrier of A:]
by FUNCT_2:def 1;
let a,b be object of B such that
A4: <^a,b^> <> {};
let f be Morphism of a,b;
[a,b] in rng the ObjectMap of F by A2,ZFMISC_1:def 2;
then consider x such that
A5: x in [:the carrier of A, the carrier of A:] &
[a,b] = (the ObjectMap of F).x by A3,FUNCT_1:def 5;
consider c,d being set such that
A6: c in the carrier of A & d in the carrier of A & [c,d] = x
by A5,ZFMISC_1:def 2;
reconsider c, d as object of A by A6;
take c, d;
the ObjectMap of F is Covariant by FUNCTOR0:def 13;
then consider g being Function of the carrier of A, the carrier of B such
that
A7: the ObjectMap of F = [:g,g:] by FUNCTOR0:def 2;
(the ObjectMap of F).(c,c) = (the ObjectMap of F).[c,c] &
(the ObjectMap of F).(d,d) = (the ObjectMap of F).[d,d]
by BINOP_1:def 1;
then (the ObjectMap of F).(c,c) = [g.c, g.c] &
(the ObjectMap of F).(d,d) = [g.d, g.d] by A7,FUNCT_3:96;
then F.c = [g.c,g.c]`1 & F.d = [g.d,g.d]`1 by FUNCTOR0:def 6;
then F.c = g.c & F.d = g.d by MCART_1:7;
then A8: (the ObjectMap of F).[c,d] = [F.c,F.d] by A7,FUNCT_3:96;
then A9: a = F.c & b = F.d by A5,A6,ZFMISC_1:33;
Morph-Map(F,c,d) = (the MorphMap of F).(c,d) by FUNCTOR0:def 15
.= (the MorphMap of F).[c,d] by BINOP_1:def 1;
then rng Morph-Map(F,c,d) = ((the Arrows of B)*the ObjectMap of F).[c,d]
by A1,A5,A6,MSUALG_3:def 3
.= (the Arrows of B).((the ObjectMap of F).[c,d]) by A5,A6,FUNCT_2:21
.= (the Arrows of B).(a,b) by A5,A6,BINOP_1:def 1
.= <^a,b^> by ALTCAT_1:def 2;
then consider g being set such that
A10:g in dom Morph-Map(F,c,d) & f = Morph-Map(F,c,d).g by A4,FUNCT_1:def 5;
reconsider g as Morphism of c,d by A10;
take g; thus a = F.c & b = F.d & <^c,d^> <> {} by A5,A6,A8,A10,ZFMISC_1:33;
thus f = F.g by A4,A9,A10,FUNCTOR0:def 16;
end;
theorem Th35:
for A,B being non empty AltGraph
for F being BimapStr over A,B st F is Contravariant one-to-one
for a,b being object of A
st F.a = F.b holds a = b
proof let A,B be non empty AltGraph;
let F be BimapStr over A,B;
given f being Function of the carrier of A, the carrier of B such that
A1: the ObjectMap of F = ~[:f,f:];
assume the ObjectMap of F is one-to-one;
then [:f,f:] is one-to-one by A1,FUNCTOR0:10;
then A2: f is one-to-one by FUNCTOR0:8;
let a,b be object of A such that
A3: F.a = F.b;
A4: dom the ObjectMap of F = [:the carrier of A, the carrier of A:] &
[a,a] in [:the carrier of A, the carrier of A:] &
[b,b] in [:the carrier of A, the carrier of A:]
by FUNCT_2:def 1,ZFMISC_1:def 2;
(the ObjectMap of F).(a,a) = (the ObjectMap of F).[a,a] &
(the ObjectMap of F).(b,b) = (the ObjectMap of F).[b,b]
by BINOP_1:def 1;
then (the ObjectMap of F).(a,a) = [:f,f:].[a,a] &
(the ObjectMap of F).(b,b) = [:f,f:].[b,b] by A1,A4,FUNCT_4:44;
then A5: (the ObjectMap of F).(a,a) = [f.a, f.a] &
(the ObjectMap of F).(b,b) = [f.b, f.b] by FUNCT_3:96;
[f.a,f.a]`1 = f.a & [f.b,f.b]`1 = f.b by MCART_1:7;
then F.a = f.a & F.b = f.b by A5,FUNCTOR0:def 6;
hence thesis by A2,A3,FUNCT_2:25;
end;
theorem Th36:
for A,B being non empty reflexive AltGraph
for F being feasible Contravariant FunctorStr over A,B st F is faithful
for a,b being object of A st <^a,b^> <> {}
for f,g being Morphism of a,b
st F.f = F.g holds f = g
proof let A,B be non empty reflexive AltGraph;
let F be feasible Contravariant FunctorStr over A,B such that
A1: for i being set, f being Function
st i in dom the MorphMap of F & (the MorphMap of F).i = f
holds f is one-to-one;
let a,b be object of A such that
A2: <^a,b^> <> {};
let f,g be Morphism of a,b;
A3: <^F.b, F.a^> <> {} by A2,FUNCTOR0:def 20;
then A4: F.f = Morph-Map(F,a,b).f & F.g = Morph-Map(F,a,b).g by A2,FUNCTOR0:def
17;
A5: dom the MorphMap of F = [:the carrier of A, the carrier of A:] &
[a,b] in [:the carrier of A, the carrier of A:]
by PBOOLE:def 3,ZFMISC_1:def 2;
Morph-Map(F,a,b) = (the MorphMap of F).(a,b) by FUNCTOR0:def 15
.= (the MorphMap of F).[a,b] by BINOP_1:def 1;
then Morph-Map(F,a,b) is one-to-one & f in <^a,b^> & g in <^a,b^> by A1,A2,
A5;
hence thesis by A3,A4,FUNCT_2:25;
end;
theorem Th37:
for A,B being non empty AltGraph
for F being Contravariant FunctorStr over A,B st F is surjective
for a,b being object of B st <^a,b^> <> {}
for f being Morphism of a,b
ex c,d being object of A, g being Morphism of c,d st
b = F.c & a = F.d & <^c,d^> <> {} & f = F.g
proof let A,B be non empty AltGraph;
let F be Contravariant FunctorStr over A,B;
given f being ManySortedFunction of
the Arrows of A, (the Arrows of B)*the ObjectMap of F such that
A1: f = the MorphMap of F & f is "onto";
assume
A2: rng the ObjectMap of F = [:the carrier of B, the carrier of B:];
A3: dom the ObjectMap of F = [:the carrier of A, the carrier of A:]
by FUNCT_2:def 1;
let a,b be object of B such that
A4: <^a,b^> <> {};
let f be Morphism of a,b;
[a,b] in rng the ObjectMap of F by A2,ZFMISC_1:def 2;
then consider x such that
A5: x in [:the carrier of A, the carrier of A:] &
[a,b] = (the ObjectMap of F).x by A3,FUNCT_1:def 5;
consider d,c being set such that
A6: d in the carrier of A & c in the carrier of A & [d,c] = x
by A5,ZFMISC_1:def 2;
reconsider c, d as object of A by A6;
take d,c;
the ObjectMap of F is Contravariant by FUNCTOR0:def 14;
then consider g being Function of the carrier of A, the carrier of B such
that
A7: the ObjectMap of F = ~[:g,g:] by FUNCTOR0:def 3;
A8: dom the ObjectMap of F = [:the carrier of A, the carrier of A:] &
[c,c] in [:the carrier of A, the carrier of A:] &
[d,c] in [:the carrier of A, the carrier of A:] &
[d,d] in [:the carrier of A, the carrier of A:]
by FUNCT_2:def 1,ZFMISC_1:def 2;
(the ObjectMap of F).(c,c) = (the ObjectMap of F).[c,c] &
(the ObjectMap of F).(d,d) = (the ObjectMap of F).[d,d]
by BINOP_1:def 1;
then (the ObjectMap of F).(c,c) = [:g,g:].[c,c] &
(the ObjectMap of F).(d,d) = [:g,g:].[d,d] by A7,A8,FUNCT_4:44;
then (the ObjectMap of F).(c,c) = [g.c, g.c] &
(the ObjectMap of F).(d,d) = [g.d, g.d] by FUNCT_3:96;
then F.c = [g.c,g.c]`1 & F.d = [g.d,g.d]`1 by FUNCTOR0:def 6;
then A9:F.c = g.c & F.d = g.d by MCART_1:7;
A10: (the ObjectMap of F).[d,c] = [:g,g:].[c,d] by A7,A8,FUNCT_4:44
.= [F.c,F.d] by A9,FUNCT_3:96;
then A11:a = F.c & b = F.d by A5,A6,ZFMISC_1:33;
Morph-Map(F,d,c) = (the MorphMap of F).(d,c) by FUNCTOR0:def 15
.= (the MorphMap of F).[d,c] by BINOP_1:def 1;
then rng Morph-Map(F,d,c) = ((the Arrows of B)*the ObjectMap of F).[d,c]
by A1,A5,A6,MSUALG_3:def 3
.= (the Arrows of B).((the ObjectMap of F).[d,c]) by A5,A6,FUNCT_2:21
.= (the Arrows of B).(a,b) by A5,A6,BINOP_1:def 1
.= <^a,b^> by ALTCAT_1:def 2;
then consider g being set such that
A12:g in dom Morph-Map(F,d,c) & f = Morph-Map(F,d,c).g by A4,FUNCT_1:def 5;
reconsider g as Morphism of d,c by A12;
take g; thus b = F.d & a = F.c & <^d,c^> <> {} by A5,A6,A10,A12,ZFMISC_1:33
;
thus f = F.g by A4,A11,A12,FUNCTOR0:def 17;
end;
begin :: Isomorphisms under arbitrary functor
definition
let A,B be category;
let F be FunctorStr over A,B;
let A', B' be category;
pred A',B' are_isomorphic_under F means
A' is subcategory of A & B' is subcategory of B &
ex G being covariant Functor of A',B' st G is bijective &
(for a' being object of A', a being object of A st a' = a holds G.a' = F.a) &
(for b',c' being object of A', b,c being object of A
st <^b',c'^> <> {} & b' = b & c' = c
for f' being Morphism of b',c', f being Morphism of b,c
st f' = f holds G.f' = Morph-Map(F,b,c).f);
pred A',B' are_anti-isomorphic_under F means
A' is subcategory of A & B' is subcategory of B &
ex G being contravariant Functor of A',B' st G is bijective &
(for a' being object of A', a being object of A st a' = a holds G.a' = F.a) &
(for b',c' being object of A', b,c being object of A
st <^b',c'^> <> {} & b' = b & c' = c
for f' being Morphism of b',c', f being Morphism of b,c
st f' = f holds G.f' = Morph-Map(F,b,c).f);
end;
theorem
for A,B, A1, B1 being category, F being FunctorStr over A,B
st A1, B1 are_isomorphic_under F
holds A1, B1 are_isomorphic
proof let A,B,A',B' be category, F be FunctorStr over A,B such that
A' is subcategory of A & B' is subcategory of B;
given G being covariant Functor of A',B' such that
A1: G is bijective and
(for a' being object of A', a being object of A
st a' = a holds G.a' = F.a) &
(for b',c' being object of A', b,c being object of A
st <^b',c'^> <> {} & b' = b & c' = c
for f' being Morphism of b',c', f being Morphism of b,c
st f' = f holds G.f' = Morph-Map(F,b,c).f);
take G; thus thesis by A1;
end;
theorem
for A,B, A1, B1 being category, F being FunctorStr over A,B
st A1, B1 are_anti-isomorphic_under F
holds A1, B1 are_anti-isomorphic
proof let A,B,A',B' be category, F be FunctorStr over A,B such that
A' is subcategory of A & B' is subcategory of B;
given G being contravariant Functor of A',B' such that
A1: G is bijective and
(for a' being object of A', a being object of A
st a' = a holds G.a' = F.a) &
(for b',c' being object of A', b,c being object of A
st <^b',c'^> <> {} & b' = b & c' = c
for f' being Morphism of b',c', f being Morphism of b,c
st f' = f holds G.f' = Morph-Map(F,b,c).f);
take G; thus thesis by A1;
end;
theorem
for A,B being category, F being covariant Functor of A,B
st A, B are_isomorphic_under F
holds F is bijective
proof let A,B be category, F be covariant Functor of A,B such that
A is subcategory of A & B is subcategory of B;
given G being covariant Functor of A,B such that
A1: G is bijective and
A2: for a' being object of A, a being object of A
st a' = a holds G.a' = F.a and
A3: for b',c' being object of A, b,c being object of A
st <^b',c'^> <> {} & b' = b & c' = c
for f' being Morphism of b',c', f being Morphism of b,c
st f' = f holds G.f' = Morph-Map(F,b,c).f;
A4: for a being object of A holds F.a = G.a by A2;
now let a,b be object of A such that
A5: <^a,b^> <> {};
let f be Morphism of a,b;
<^F.a, F.b^> <> {} by A5,FUNCTOR0:def 19;
hence F.f = Morph-Map(F,a,b).f by A5,FUNCTOR0:def 16 .= G.f by A3,A5;
end;
then A6: the FunctorStr of F = the FunctorStr of G by A4,YELLOW18:1;
G is injective surjective by A1,FUNCTOR0:def 36;
then G is one-to-one faithful full onto by FUNCTOR0:def 34,def 35;
hence the ObjectMap of F is one-to-one &
the MorphMap of F is "1-1" &
(ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto") &
the ObjectMap of F is onto
by A6,FUNCTOR0:def 7,def 8,def 31,def 33;
end;
theorem
for A,B being category, F being contravariant Functor of A,B
st A, B are_anti-isomorphic_under F
holds F is bijective
proof let A,B be category, F be contravariant Functor of A,B such that
A is subcategory of A & B is subcategory of B;
given G being contravariant Functor of A,B such that
A1: G is bijective and
A2: for a' being object of A, a being object of A
st a' = a holds G.a' = F.a and
A3: for b',c' being object of A, b,c being object of A
st <^b',c'^> <> {} & b' = b & c' = c
for f' being Morphism of b',c', f being Morphism of b,c
st f' = f holds G.f' = Morph-Map(F,b,c).f;
A4: for a being object of A holds F.a = G.a by A2;
now let a,b be object of A such that
A5: <^a,b^> <> {};
let f be Morphism of a,b;
<^F.b, F.a^> <> {} by A5,FUNCTOR0:def 20;
hence F.f = Morph-Map(F,a,b).f by A5,FUNCTOR0:def 17 .= G.f by A3,A5;
end;
then A6: the FunctorStr of F = the FunctorStr of G by A4,YELLOW18:2;
G is injective surjective by A1,FUNCTOR0:def 36;
then G is one-to-one faithful full onto by FUNCTOR0:def 34,def 35;
hence the ObjectMap of F is one-to-one &
the MorphMap of F is "1-1" &
(ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto") &
the ObjectMap of F is onto
by A6,FUNCTOR0:def 7,def 8,def 31,def 33;
end;
theorem
for A,B being category, F being covariant Functor of A,B
st F is bijective
holds A, B are_isomorphic_under F
proof let A,B be category, F be covariant Functor of A,B such that
A1: F is bijective;
A is SubCatStr of A & B is SubCatStr of B &
the carrier of A = the carrier of A & the carrier of B = the carrier of B &
the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B
by ALTCAT_2:21;
hence A is subcategory of A & B is subcategory of B by ALTCAT_4:35;
take F; thus F is bijective &
for a' being object of A, a being object of A
st a' = a holds F.a' = F.a by A1;
let b',c' be object of A, b,c be object of A; assume
A2: <^b',c'^> <> {} & b' = b & c' = c;
then <^F.b,F.c^> <> {} by FUNCTOR0:def 19;
hence thesis by A2,FUNCTOR0:def 16;
end;
theorem
for A,B being category, F being contravariant Functor of A,B
st F is bijective
holds A, B are_anti-isomorphic_under F
proof let A,B be category, F be contravariant Functor of A,B such that
A1: F is bijective;
A is SubCatStr of A & B is SubCatStr of B &
the carrier of A = the carrier of A & the carrier of B = the carrier of B &
the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B
by ALTCAT_2:21;
hence A is subcategory of A & B is subcategory of B by ALTCAT_4:35;
take F; thus F is bijective &
for a' being object of A, a being object of A
st a' = a holds F.a' = F.a by A1;
let b',c' be object of A, b,c be object of A; assume
A2: <^b',c'^> <> {} & b' = b & c' = c;
then <^F.c,F.b^> <> {} by FUNCTOR0:def 20;
hence thesis by A2,FUNCTOR0:def 17;
end;
scheme CoBijectRestriction
{A1, A2() -> non empty category,
F() -> covariant Functor of A1(), A2(),
B1() -> non empty subcategory of A1(),
B2() -> non empty subcategory of A2()}:
B1(), B2() are_isomorphic_under F()
provided
A1: F() is bijective and
A2: for a being object of A1() holds
a is object of B1() iff F().a is object of B2() and
A3: for a,b being object of A1() st <^a,b^> <> {}
for a1,b1 being object of B1() st a1 = a & b1 = b
for a2,b2 being object of B2() st a2 = F().a & b2 = F().b
for f being Morphism of a,b holds
f in <^a1,b1^> iff F().f in <^a2,b2^>
proof
thus B1() is subcategory of A1() & B2() is subcategory of A2();
A4: the carrier of B1() c= the carrier of A1() by ALTCAT_2:def 11;
deffunc O(object of B1()) = (F()|B1()).$1;
deffunc F(object of B1(),object of B1(),Morphism of $1,$2) =
(F()|B1()).$3;
A5: now let a be object of B1();
a in the carrier of B1();
then reconsider b = a as object of A1() by A4;
(F()|B1()).a = F().b by Th29;
hence O(a) is object of B2() by A2;
end;
A6: now let a,b be object of B1() such that
A7: <^a,b^> <> {};
a in the carrier of B1() & b in the carrier of B1();
then reconsider c = a, d = b as object of A1() by A4;
reconsider a' = (F()|B1()).a, b' = (F()|B1()).b as object of B2() by A5;
let f be Morphism of a,b;
A8: <^a,b^> c= <^c,d^> & f in <^a,b^> by A7,ALTCAT_2:32;
then reconsider g = f as Morphism of c,d ;
(F()|B1()).a = F().c & (F()|B1()).b = F().d &
(F()|B1()).f = F().g by A7,Th29,Th30;
then (F()|B1()).f in <^a',b'^> by A3,A8;
hence F(a,b,f) in (the Arrows of B2()).(O(a), O(b)) by ALTCAT_1:def 2;
end;
A9: now let a,b,c be object of B1() such that
A10: <^a,b^> <> {} & <^b,c^> <> {};
a in the carrier of B1() & b in the carrier of B1() &
c in the carrier of B1();
then reconsider a1 = a, b1 = b, c1 = c as object of A1()
by A4;
let f be Morphism of a,b, g be Morphism of b,c;
let a',b',c' be object of B2() such that
A11: a' = O(a) & b' = O(b) & c' = O(c);
let f' be Morphism of a',b', g' be Morphism of b',c' such that
A12: f' = F(a,b,f) & g' = F(b,c,g);
A13: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A10,ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
A14: <^b,c^> c= <^b1,c1^> & g in <^b,c^> by A10,ALTCAT_2:32;
then reconsider g1 = g as Morphism of b1,c1 ;
A15: <^a,c^> <> {} by A10,ALTCAT_1:def 4;
A16: g*f = g1*f1 by A10,ALTCAT_2:33;
A17: a' = F().a1 & b' = F().b1 & c' = F().c1 by A11,Th29;
A18: (F()|B1()).(g*f) = F().(g1*f1) & f' = F().f1 & g' = F().g1
by A10,A12,A15,A16,Th30; then
A19: f' in <^a',b'^> & g' in <^b',c'^> by A3,A13,A14,A17;
thus F(a,c,g*f) = (F().g1)*(F().f1) by A13,A14,A18,FUNCTOR0:def 24
.= g'*f' by A17,A18,A19,ALTCAT_2:33;
end;
A20: now let a be object of B1(), a' be object of B2() such that
A21: a' = O(a);
a in the carrier of B1();
then reconsider a1 = a as object of A1() by A4;
idm a in <^a,a^> & idm a = idm a1 by ALTCAT_2:35;
hence F(a,a,idm a) = F().idm a1 by Th30
.= idm (F().a1) by FUNCTOR2:2
.= idm ((F()|B1()).a) by Th29
.= idm a' by A21,ALTCAT_2:35;
end;
consider G being covariant strict Functor of B1(),B2() such that
A22: for a being object of B1() holds G.a = O(a) and
A23: for a,b being object of B1() st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = F(a,b,f)
from CovariantFunctorLambda(A5,A6,A9,A20);
take G;
A24: F() is injective surjective by A1,FUNCTOR0:def 36;
then
A25: F() is one-to-one faithful surjective by FUNCTOR0:def 34;
A26: now let a,b be object of B1();
a in the carrier of B1() & b in the carrier of B1();
then reconsider a1 = a, b1 = b as object of A1() by A4;
assume O(a) = O(b);
then F().a1 = (F()|B1()).b by Th29 .= F().b1 by Th29;
hence a = b by A25,Th32;
end;
A27: now let a,b be object of B1() such that
A28: <^a,b^> <> {};
a in the carrier of B1() & b in the carrier of B1();
then reconsider a1 = a, b1 = b as object of A1() by A4;
let f,g be Morphism of a,b;
A29: <^a,b^> c= <^a1,b1^> & f in <^a,b^> & g in <^a,b^>
by A28,ALTCAT_2:32;
then reconsider f1 = f, g1 = g as Morphism of a1,b1 ;
assume F(a,b,f) = F(a,b,g);
then F().f1 = (F()|B1()).g by A28,Th30 .= F().g1 by A28,Th30;
hence f = g by A25,A29,Th33;
end;
A30: for a,b being object of B2() st <^a,b^> <> {}
for f being Morphism of a,b
ex c,d being object of B1(), g being Morphism of c,d
st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof let a,b be object of B2() such that
A31: <^a,b^> <> {};
a in the carrier of B2() & b in the carrier of B2() &
the carrier of B2() c= the carrier of A2() by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as object of A2();
let f be Morphism of a,b;
A32: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A31,ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
consider c1, d1 being object of A1(), g1 being Morphism of c1,d1
such that
A33: a1 = F().c1 & b1 = F().d1 & <^c1,d1^> <> {} & f1 = F().g1
by A24,A32,Th34;
reconsider c = c1, d = d1 as object of B1() by A2,A33;
A34: g1 in <^c,d^> by A3,A31,A33;
then reconsider g = g1 as Morphism of c,d ;
take c,d,g;
thus thesis by A33,A34,Th29,Th30;
end;
thus G is bijective from CoBijectiveSch(A22,A23,A26,A27,A30);
hereby let a be object of B1(), a1 be object of A1() such that
A35: a = a1;
thus G.a = (F()|B1()).a by A22 .= F().a1 by A35,Th29;
end;
let b,c be object of B1(), b1,c1 be object of A1() such that
A36: <^b,c^> <> {} & b1 = b & c1 = c;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A37: f = f1;
A38: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A36,ALTCAT_2:32;
then A39: <^F().b1, F().c1^> <> {} by FUNCTOR0:def 19;
thus G.f = (F()|B1()).f by A23,A36 .= F().f1 by A36,A37,Th30
.= Morph-Map(F(),b1,c1).f1 by A38,A39,FUNCTOR0:def 16;
end;
scheme ContraBijectRestriction
{A1, A2() -> non empty category,
F() -> contravariant Functor of A1(), A2(),
B1() -> non empty subcategory of A1(),
B2() -> non empty subcategory of A2()}:
B1(), B2() are_anti-isomorphic_under F()
provided
A1: F() is bijective and
A2: for a being object of A1() holds
a is object of B1() iff F().a is object of B2() and
A3: for a,b being object of A1() st <^a,b^> <> {}
for a1,b1 being object of B1() st a1 = a & b1 = b
for a2,b2 being object of B2() st a2 = F().a & b2 = F().b
for f being Morphism of a,b holds
f in <^a1,b1^> iff F().f in <^b2,a2^>
proof
thus B1() is subcategory of A1() & B2() is subcategory of A2();
A4: the carrier of B1() c= the carrier of A1() by ALTCAT_2:def 11;
deffunc O(object of B1()) = (F()|B1()).$1;
deffunc F(object of B1(),object of B1(),Morphism of $1,$2) =
(F()|B1()).$3;
A5: now let a be object of B1();
a in the carrier of B1();
then reconsider b = a as object of A1() by A4;
(F()|B1()).a = F().b by Th29;
hence O(a) is object of B2() by A2;
end;
A6: now let a,b be object of B1() such that
A7: <^a,b^> <> {};
a in the carrier of B1() & b in the carrier of B1();
then reconsider c = a, d = b as object of A1() by A4;
reconsider a' = (F()|B1()).a, b' = (F()|B1()).b as object of B2() by A5;
let f be Morphism of a,b;
A8: <^a,b^> c= <^c,d^> & f in <^a,b^> by A7,ALTCAT_2:32;
then reconsider g = f as Morphism of c,d ;
(F()|B1()).a = F().c & (F()|B1()).b = F().d &
(F()|B1()).f = F().g by A7,Th29,Th31;
then (F()|B1()).f in <^b',a'^> by A3,A8;
hence F(a,b,f) in (the Arrows of B2()).(O(b), O(a)) by ALTCAT_1:def 2;
end;
A9: now let a,b,c be object of B1() such that
A10: <^a,b^> <> {} & <^b,c^> <> {};
a in the carrier of B1() & b in the carrier of B1() &
c in the carrier of B1();
then reconsider a1 = a, b1 = b, c1 = c as object of A1() by A4;
let f be Morphism of a,b, g be Morphism of b,c;
let a',b',c' be object of B2() such that
A11: a' = O(a) & b' = O(b) & c' = O(c);
let f' be Morphism of b',a', g' be Morphism of c',b' such that
A12: f' = F(a,b,f) & g' = F(b,c,g);
A13: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A10,ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
A14: <^b,c^> c= <^b1,c1^> & g in <^b,c^> by A10,ALTCAT_2:32;
then reconsider g1 = g as Morphism of b1,c1 ;
A15: <^a,c^> <> {} by A10,ALTCAT_1:def 4;
A16: g*f = g1*f1 by A10,ALTCAT_2:33;
A17: a' = F().a1 & b' = F().b1 & c' = F().c1 by A11,Th29;
A18: (F()|B1()).(g*f) = F().(g1*f1) & f' = F().f1 & g' = F().g1
by A10,A12,A15,A16,Th31;
then
A19: f' in <^b',a'^> & g' in <^c',b'^> by A3,A13,A14,A17;
thus F(a,c,g*f) = (F().f1)*(F().g1) by A13,A14,A18,FUNCTOR0:def 25
.= f'*g' by A17,A18,A19,ALTCAT_2:33;
end;
A20: now let a be object of B1(), a' be object of B2() such that
A21: a' = O(a);
a in the carrier of B1();
then reconsider a1 = a as object of A1() by A4;
idm a in <^a,a^> & idm a = idm a1 by ALTCAT_2:35;
hence F(a,a,idm a) = F().idm a1 by Th31
.= idm (F().a1) by ALTCAT_4:13
.= idm ((F()|B1()).a) by Th29
.= idm a' by A21,ALTCAT_2:35;
end;
consider G being contravariant strict Functor of B1(),B2() such that
A22: for a being object of B1() holds G.a = O(a) and
A23: for a,b being object of B1() st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = F(a,b,f)
from ContravariantFunctorLambda(A5,A6,A9,A20);
take G;
A24: F() is injective surjective by A1,FUNCTOR0:def 36;
then A25: F() is one-to-one faithful surjective by FUNCTOR0:def 34;
A26: now let a,b be object of B1();
a in the carrier of B1() & b in the carrier of B1();
then reconsider a1 = a, b1 = b as object of A1() by A4;
assume O(a) = O(b);
then F().a1 = (F()|B1()).b by Th29 .= F().b1 by Th29;
hence a = b by A25,Th35;
end;
A27: now let a,b be object of B1() such that
A28: <^a,b^> <> {};
a in the carrier of B1() & b in the carrier of B1();
then reconsider a1 = a, b1 = b as object of A1() by A4;
let f,g be Morphism of a,b;
A29: <^a,b^> c= <^a1,b1^> & f in <^a,b^> & g in <^a,b^>
by A28,ALTCAT_2:32;
then reconsider f1 = f, g1 = g as Morphism of a1,b1 ;
assume F(a,b,f) = F(a,b,g);
then F().f1 = (F()|B1()).g by A28,Th31 .= F().g1 by A28,Th31;
hence f = g by A25,A29,Th36;
end;
A30: for a,b being object of B2() st <^a,b^> <> {}
for f being Morphism of a,b
ex c,d being object of B1(), g being Morphism of c,d
st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof let a,b be object of B2() such that
A31: <^a,b^> <> {};
a in the carrier of B2() & b in the carrier of B2() &
the carrier of B2() c= the carrier of A2() by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as object of A2();
let f be Morphism of a,b;
A32: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A31,ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
consider c1, d1 being object of A1(), g1 being Morphism of c1,d1
such that
A33: b1 = F().c1 & a1 = F().d1 & <^c1,d1^> <> {} & f1 = F().g1
by A24,A32,Th37;
reconsider c = c1, d = d1 as object of B1() by A2,A33;
A34: g1 in <^c,d^> by A3,A31,A33;
then reconsider g = g1 as Morphism of c,d ;
take c,d,g;
thus thesis by A33,A34,Th29,Th31;
end;
thus G is bijective from ContraBijectiveSch(A22,A23,A26,A27,A30);
hereby let a be object of B1(), a1 be object of A1() such that
A35: a = a1;
thus G.a = (F()|B1()).a by A22 .= F().a1 by A35,Th29;
end;
let b,c be object of B1(), b1,c1 be object of A1();
assume
A36: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A37: f = f1;
A38: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A36,ALTCAT_2:32;
then A39: <^F().c1, F().b1^> <> {} by FUNCTOR0:def 20;
thus G.f = (F()|B1()).f by A23,A36 .= F().f1 by A36,A37,Th31
.= Morph-Map(F(),b1,c1).f1 by A38,A39,FUNCTOR0:def 17;
end;
theorem
for A being category, B being non empty subcategory of A
holds B,B are_isomorphic_under id A
proof let A be category, B be non empty subcategory of A;
set F = id A;
thus B is subcategory of A & B is subcategory of A;
take G = id B; thus G is bijective;
hereby let a be object of B, a1 be object of A;
assume a = a1;
hence G.a = a1 by FUNCTOR0:30 .= F.a1 by FUNCTOR0:30;
end;
let b,c be object of B, b1,c1 be object of A such that
A1: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A2: f = f1;
A3: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A1,ALTCAT_2:32;
A4: F.b1 = b1 & F.c1 = c1 by FUNCTOR0:30;
thus G.f = f by A1,FUNCTOR0:32 .= F.f1 by A2,A3,FUNCTOR0:32
.= Morph-Map(F,b1,c1).f1 by A3,A4,FUNCTOR0:def 16;
end;
theorem Th45:
for f, g being Function st f c= g holds ~f c= ~g
proof let f, g be Function such that
A1: f c= g;
let x,y; assume
A2: [x,y] in ~f;
then x in dom ~f by RELAT_1:def 4;
then consider z2,z1 being set such that
A3: x = [z1,z2] & [z2,z1] in dom f by FUNCT_4:def 2;
y = (~f).x by A2,FUNCT_1:8 .= f.[z2,z1] by A3,FUNCT_4:def 2;
then [[z2,z1],y] in f by A3,FUNCT_1:8;
then [z2,z1] in dom g & y = g.[z2,z1] by A1,FUNCT_1:8;
then x in dom ~g & y = (~g).x by A3,FUNCT_4:def 2;
hence thesis by FUNCT_1:8;
end;
theorem
for f, g being Function st dom f is Relation & ~f c= ~g holds f c= g
proof let f, g be Function; assume dom f is Relation;
then reconsider R = dom f as Relation;
R c= [:dom R, rng R:] by RELAT_1:21;
then A1: ~~f = f & ~~g c= g by FUNCT_4:52,53;
assume ~f c= ~g;
then f c= ~~g by A1,Th45;
hence thesis by A1,XBOOLE_1:1;
end;
theorem Th47:
for I, J being set
for A being ManySortedSet of [:I,I:], B being ManySortedSet of [:J,J:]
st A cc= B holds ~A cc= ~B
proof let I, J be set;
let A be ManySortedSet of [:I,I:], B be ManySortedSet of [:J,J:] such that
A1: [:I,I:] c= [:J,J:] and
A2: for x st x in [:I,I:] holds A.x c= B.x;
thus [:I,I:] c= [:J,J:] by A1;
let x; assume
x in [:I,I:];
then consider x1,x2 being set such that
A3: x1 in I & x2 in I & x = [x1,x2] by ZFMISC_1:def 2;
A4: [x2,x1] in [:I,I:] by A3,ZFMISC_1:def 2;
dom A = [:I,I:] & dom B = [:J,J:] by PBOOLE:def 3;
then (~A).x = A.[x2,x1] & (~B).x = B.[x2,x1] by A1,A3,A4,FUNCT_4:def 2;
hence thesis by A2,A4;
end;
theorem Th48:
for A being transitive non empty AltCatStr
for B being transitive non empty SubCatStr of A
holds B opp is SubCatStr of A opp
proof let A be transitive non empty AltCatStr;
let B be transitive non empty SubCatStr of A;
A1: the carrier of B c= the carrier of A &
the Arrows of B cc= the Arrows of A &
the Comp of B cc= the Comp of A by ALTCAT_2:def 11;
A2: A, A opp are_opposite & B, B opp are_opposite by YELLOW18:def 4;
then A3: the carrier of A opp = the carrier of A &
the carrier of B opp = the carrier of B by YELLOW18:def 3;
hence
the carrier of B opp c= the carrier of A opp by ALTCAT_2:def 11;
the Arrows of A opp = ~the Arrows of A &
the Arrows of B opp = ~the Arrows of B by A2,YELLOW18:def 3;
hence the Arrows of B opp cc= the Arrows of A opp by A1,Th47;
thus [:the carrier of B opp, the carrier of B opp, the carrier of B opp:]
c= [:the carrier of A opp, the carrier of A opp, the carrier of A opp:]
by A1,A3,MCART_1:77;
let x; assume
x in [:the carrier of B opp, the carrier of B opp, the carrier of B opp:]
;
then consider x1,x2,x3 being set such that
A4: x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier of B &
x = [x1,x2,x3] by A3,MCART_1:72;
reconsider a = x1, b = x2, c = x3 as object of B by A4;
reconsider a1 = a, b1 = b, c1 = c as object of A by A1,A4;
reconsider a' = a, b' = b, c' = c as object of B opp
by A3;
reconsider a1' = a1, b1' = b1, c1' = c1 as object of A opp
by A3;
A5: (the Comp of B opp).(a',b',c') = ~((the Comp of B).(c,b,a))
by A2,YELLOW18:def 3;
A6: (the Comp of A opp).(a1',b1',c1') = ~((the Comp of A).(c1,b1,a1))
by A2,YELLOW18:def 3;
A7: [x3,x2,x1] in [:the carrier of B, the carrier of B, the carrier of B:]
by A4,MCART_1:73;
A8: (the Comp of B opp).(a',b',c') = (the Comp of B opp).x &
(the Comp of A opp).(a1',b1',c1') = (the Comp of A opp).x
by A4,MULTOP_1:def 1;
(the Comp of B).(c,b,a) = (the Comp of B).[c,b,a] &
(the Comp of A).(c1,b1,a1) = (the Comp of A).[c1,b1,a1]
by MULTOP_1:def 1;
then (the Comp of B).(c,b,a) c= (the Comp of A).(c1,b1,a1)
by A1,A7,ALTCAT_2:def 2;
hence (the Comp of B opp).x c= (the Comp of A opp).x by A5,A6,A8,Th45;
end;
theorem Th49:
for A being category, B being non empty subcategory of A
holds B opp is subcategory of A opp
proof let A be category, B be non empty subcategory of A;
reconsider BB = B opp as transitive non empty SubCatStr of A opp by Th48;
A1: BB, B are_opposite & A opp, A are_opposite by YELLOW18:def 4;
then A2: the carrier of BB = the carrier of B &
the carrier of A opp = the carrier of A by YELLOW18:def 3;
BB is id-inheriting
proof per cases; case BB is non empty;
let o be object of BB, o' be object of A opp;
reconsider a = o as object of B by A2;
reconsider a' = o' as object of A by A2;
assume o = o';
then idm a' in <^a,a^> by ALTCAT_2:def 14;
then idm o' in <^a,a^> by A1,YELLOW18:10;
hence idm o' in <^o,o^> by A1,YELLOW18:7;
case BB is empty; thus thesis;
end;
hence thesis;
end;
theorem
for A being category, B being non empty subcategory of A
holds B,B opp are_anti-isomorphic_under dualizing-func(A, A opp)
proof let A be category, B be non empty subcategory of A;
set F = dualizing-func(A, A opp);
A1: A, A opp are_opposite & B, B opp are_opposite by YELLOW18:def 4;
thus B is subcategory of A & B opp is subcategory of A opp by Th49;
take G = dualizing-func(B, B opp); thus G is bijective;
hereby let a be object of B, a1 be object of A;
assume a = a1;
hence G.a = a1 by A1,YELLOW18:def 5 .= F.a1 by A1,YELLOW18:def 5;
end;
let b,c be object of B, b1,c1 be object of A such that
A2: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A3: f = f1;
A4: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A2,ALTCAT_2:32;
then A5: <^F.c1,F.b1^> <> {} by FUNCTOR0:def 20;
thus G.f = f by A1,A2,YELLOW18:def 5 .= F.f1 by A1,A3,A4,YELLOW18:def 5
.= Morph-Map(F,b1,c1).f1 by A4,A5,FUNCTOR0:def 17;
end;
theorem
for A1,A2 being category, F being covariant Functor of A1,A2
st F is bijective
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
st B1,B2 are_isomorphic_under F
holds B2,B1 are_isomorphic_under F"
proof let A1,A2 be category, F be covariant Functor of A1,A2 such that
A1: F is bijective;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2 such that
B1 is subcategory of A1 & B2 is subcategory of A2;
given G being covariant Functor of B1,B2 such that
A2: G is bijective and
A3: for a being object of B1, a1 being object of A1 st a = a1 holds G.a = F.a1
and
A4: for b,c being object of B1, b1,c1 being object of A1
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds G.f = Morph-Map(F,b1,c1).f1;
thus B2 is subcategory of A2 & B1 is subcategory of A1;
consider H being Functor of B2,B1 such that
A5: H = G" & H is bijective covariant by A2,FUNCTOR0:49;
reconsider H as covariant Functor of B2,B1 by A5;
ex H being Functor of A2,A1 st H = F" & H is bijective covariant
by A1,FUNCTOR0:49;
then reconsider F' = F" as covariant Functor of A2,A1;
take H; thus H is bijective by A5;
A6: the carrier of B1 c= the carrier of A1 &
the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;
F is surjective & G is surjective by A1,A2,FUNCTOR0:def 36;
then F is onto & G is onto by FUNCTOR0:def 35;
then A7: F is coreflexive & G is coreflexive by FUNCTOR0:47;
thus
A8: now let a be object of B2, a1 be object of A2;
H.a in the carrier of B1;
then reconsider Ha = H.a as object of A1 by A6;
assume
A9: a = a1;
G.(H.a) = F.Ha by A3;
then F.Ha = a by A2,A5,A7,Th1;
hence H.a = F".a1 by A1,A7,A9,Th1;
end;
let b,c be object of B2, b1,c1 be object of A2 such that
A10: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A11: f = f1;
A12: H.b = F".b1 & H.c = F".c1 & <^H.b, H.c^> <> {}
by A8,A10,FUNCTOR0:def 19;
then A13: <^H.b, H.c^> c= <^F".b1, F".c1^> & H.f in <^H.b, H.c^> by ALTCAT_2:32
;
then reconsider Hf = H.f as Morphism of F".b1, F".c1 ;
A14: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A10,ALTCAT_2:32;
then A15: F.(F".b1) = b1 & F.(F".c1) = c1 & f in <^b1,c1^> by A1,A7,Th1;
A16: G.(H.b) = b & G.(H.c) = c by A2,A5,A7,Th1;
G.(H.f) = Morph-Map(F,F".b1, F".c1).Hf by A4,A12
.= F.Hf by A13,A15,FUNCTOR0:def 16;
then F.Hf = f by A2,A5,A12,A16,Th2;
hence H.f = F'.f1 by A1,A11,A13,A15,Th2
.= Morph-Map(F",b1,c1).f1 by A13,A14,FUNCTOR0:def 16;
end;
theorem
for A1,A2 being category, F being contravariant Functor of A1,A2
st F is bijective
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
st B1,B2 are_anti-isomorphic_under F
holds B2,B1 are_anti-isomorphic_under F"
proof let A1,A2 be category, F be contravariant Functor of A1,A2 such that
A1: F is bijective;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2 such that
B1 is subcategory of A1 & B2 is subcategory of A2;
given G being contravariant Functor of B1,B2 such that
A2: G is bijective and
A3: for a being object of B1, a1 being object of A1 st a = a1 holds G.a = F.a1
and
A4: for b,c being object of B1, b1,c1 being object of A1
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds G.f = Morph-Map(F,b1,c1).f1;
thus B2 is subcategory of A2 & B1 is subcategory of A1;
consider H being Functor of B2,B1 such that
A5: H = G" & H is bijective contravariant by A2,FUNCTOR0:50;
reconsider H as contravariant Functor of B2,B1 by A5;
ex H being Functor of A2,A1 st H = F" & H is bijective contravariant
by A1,FUNCTOR0:50;
then reconsider F' = F" as contravariant Functor of A2,A1;
take H; thus H is bijective by A5;
A6: the carrier of B1 c= the carrier of A1 &
the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;
F is surjective & G is surjective by A1,A2,FUNCTOR0:def 36;
then F is onto & G is onto by FUNCTOR0:def 35;
then A7: F is coreflexive & G is coreflexive by FUNCTOR0:48;
thus
A8: now let a be object of B2, a1 be object of A2;
H.a in the carrier of B1;
then reconsider Ha = H.a as object of A1 by A6;
assume
A9: a = a1;
G.(H.a) = F.Ha by A3;
then F.Ha = a by A2,A5,A7,Th1;
hence H.a = F".a1 by A1,A7,A9,Th1;
end;
let b,c be object of B2, b1,c1 be object of A2 such that
A10: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A11: f = f1;
A12: H.b = F".b1 & H.c = F".c1 & <^H.c, H.b^> <> {}
by A8,A10,FUNCTOR0:def 20;
then A13: <^H.c, H.b^> c= <^F".c1, F".b1^> & H.f in <^H.c, H.b^> by ALTCAT_2:32
;
then reconsider Hf = H.f as Morphism of F".c1, F".b1 ;
A14: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A10,ALTCAT_2:32;
then A15: F.(F".b1) = b1 & F.(F".c1) = c1 & f in <^b1,c1^> by A1,A7,Th1;
A16: G.(H.b) = b & G.(H.c) = c by A2,A5,A7,Th1;
G.(H.f) = Morph-Map(F,F".c1, F".b1).Hf by A4,A12
.= F.Hf by A13,A15,FUNCTOR0:def 17;
then F.Hf = f by A2,A5,A12,A16,Th3;
hence H.f = F'.f1 by A1,A11,A13,A15,Th3
.= Morph-Map(F",b1,c1).f1 by A13,A14,FUNCTOR0:def 17;
end;
theorem
for A1,A2,A3 being category
for F being covariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3
st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G
holds B1,B3 are_isomorphic_under G*F
proof let A1,A2,A3 be category;
let F be covariant Functor of A1,A2;
let G be covariant Functor of A2,A3;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2;
let B3 be non empty subcategory of A3;
assume B1 is subcategory of A1 & B2 is subcategory of A2;
given F1 being covariant Functor of B1,B2 such that
A1: F1 is bijective and
A2: for a being object of B1, a1 being object of A1 st a = a1 holds F1.a = F.a1
and
A3: for b,c being object of B1, b1,c1 being object of A1
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds F1.f = Morph-Map(F,b1,c1).f1;
assume B2 is subcategory of A2 & B3 is subcategory of A3;
given G1 being covariant Functor of B2,B3 such that
A4: G1 is bijective and
A5: for a being object of B2, a1 being object of A2 st a = a1 holds G1.a = G.a1
and
A6: for b,c being object of B2, b1,c1 being object of A2
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds G1.f = Morph-Map(G,b1,c1).f1;
thus B1 is subcategory of A1 & B3 is subcategory of A3;
take G1*F1; thus G1*F1 is bijective by A1,A4,FUNCTOR1:13;
hereby let a be object of B1, b be object of A1;
assume a = b;
then F1.a = F.b by A2;
then G1.(F1.a) = G.(F.b) by A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:34 .= (G*F).b by FUNCTOR0:34;
end;
let b,c be object of B1, b1,c1 be object of A1 such that
A7: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A8: <^F1.b, F1.c^> <> {} & F1.b = F.b1 & F1.c = F.c1 by A2,A7,FUNCTOR0:def 19;
then A9: f in <^b,c^> & <^b,c^> c= <^b1,c1^> &
F1.f in <^F1.b, F1.c^> & <^F1.b, F1.c^> c= <^F.b1, F.c1^>
by A7,ALTCAT_2:32;
then A10: <^(G*F).b1, (G*F).c1^> <> {} & (G*F).b1 = G.(F.b1) & (G*F).c1 = G.(F.
c1)
by FUNCTOR0:34,def 19;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7
.= F.f1 by A9,FUNCTOR0:def 16;
then G1.(F1.f) = Morph-Map(G,F.b1,F.c1).(F.f1) by A6,A8;
hence (G1*F1).f = Morph-Map(G,F.b1,F.c1).(F.f1) by A7,FUNCTOR3:6
.= G.(F.f1) by A9,A10,FUNCTOR0:def 16
.= (G*F).f1 by A9,FUNCTOR3:6
.= Morph-Map(G*F,b1,c1).f1 by A9,A10,FUNCTOR0:def 16;
end;
theorem
for A1,A2,A3 being category
for F being contravariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3
st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G
holds B1,B3 are_anti-isomorphic_under G*F
proof let A1,A2,A3 be category;
let F be contravariant Functor of A1,A2;
let G be covariant Functor of A2,A3;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2;
let B3 be non empty subcategory of A3;
assume B1 is subcategory of A1 & B2 is subcategory of A2;
given F1 being contravariant Functor of B1,B2 such that
A1: F1 is bijective and
A2: for a being object of B1, a1 being object of A1 st a = a1 holds F1.a = F.a1
and
A3: for b,c being object of B1, b1,c1 being object of A1
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds F1.f = Morph-Map(F,b1,c1).f1;
assume B2 is subcategory of A2 & B3 is subcategory of A3;
given G1 being covariant Functor of B2,B3 such that
A4: G1 is bijective and
A5: for a being object of B2, a1 being object of A2 st a = a1 holds G1.a = G.a1
and
A6: for b,c being object of B2, b1,c1 being object of A2
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds G1.f = Morph-Map(G,b1,c1).f1;
thus B1 is subcategory of A1 & B3 is subcategory of A3;
take G1*F1; thus G1*F1 is bijective by A1,A4,FUNCTOR1:13;
hereby let a be object of B1, b be object of A1;
assume a = b;
then F1.a = F.b by A2;
then G1.(F1.a) = G.(F.b) by A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:34 .= (G*F).b by FUNCTOR0:34;
end;
let b,c be object of B1, b1,c1 be object of A1 such that
A7: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A8: <^F1.c, F1.b^> <> {} & F1.b = F.b1 & F1.c = F.c1 by A2,A7,FUNCTOR0:def 20;
then A9: f in <^b,c^> & <^b,c^> c= <^b1,c1^> &
F1.f in <^F1.c, F1.b^> & <^F1.c, F1.b^> c= <^F.c1, F.b1^>
by A7,ALTCAT_2:32;
then A10: <^(G*F).c1, (G*F).b1^> <> {} & (G*F).b1 = G.(F.b1) & (G*F).c1 = G.(F.
c1)
by FUNCTOR0:34,def 20;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7
.= F.f1 by A9,FUNCTOR0:def 17;
then G1.(F1.f) = Morph-Map(G,F.c1,F.b1).(F.f1) by A6,A8;
hence (G1*F1).f = Morph-Map(G,F.c1,F.b1).(F.f1) by A7,FUNCTOR3:9
.= G.(F.f1) by A9,A10,FUNCTOR0:def 16
.= (G*F).f1 by A9,FUNCTOR3:9
.= Morph-Map(G*F,b1,c1).f1 by A9,A10,FUNCTOR0:def 17;
end;
theorem
for A1,A2,A3 being category
for F being covariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3
st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G
holds B1,B3 are_anti-isomorphic_under G*F
proof let A1,A2,A3 be category;
let F be covariant Functor of A1,A2;
let G be contravariant Functor of A2,A3;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2;
let B3 be non empty subcategory of A3;
assume B1 is subcategory of A1 & B2 is subcategory of A2;
given F1 being covariant Functor of B1,B2 such that
A1: F1 is bijective and
A2: for a being object of B1, a1 being object of A1 st a = a1 holds F1.a = F.a1
and
A3: for b,c being object of B1, b1,c1 being object of A1
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds F1.f = Morph-Map(F,b1,c1).f1;
assume B2 is subcategory of A2 & B3 is subcategory of A3;
given G1 being contravariant Functor of B2,B3 such that
A4: G1 is bijective and
A5: for a being object of B2, a1 being object of A2 st a = a1 holds G1.a = G.a1
and
A6: for b,c being object of B2, b1,c1 being object of A2
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds G1.f = Morph-Map(G,b1,c1).f1;
thus B1 is subcategory of A1 & B3 is subcategory of A3;
take G1*F1; thus G1*F1 is bijective by A1,A4,FUNCTOR1:13;
hereby let a be object of B1, b be object of A1;
assume a = b;
then F1.a = F.b by A2;
then G1.(F1.a) = G.(F.b) by A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:34 .= (G*F).b by FUNCTOR0:34;
end;
let b,c be object of B1, b1,c1 be object of A1 such that
A7: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A8: <^F1.b, F1.c^> <> {} & F1.b = F.b1 & F1.c = F.c1 by A2,A7,FUNCTOR0:def 19;
then A9: f in <^b,c^> & <^b,c^> c= <^b1,c1^> &
F1.f in <^F1.b, F1.c^> & <^F1.b, F1.c^> c= <^F.b1, F.c1^>
by A7,ALTCAT_2:32;
then A10: <^(G*F).c1, (G*F).b1^> <> {} & (G*F).b1 = G.(F.b1) & (G*F).c1 = G.(F.
c1)
by FUNCTOR0:34,def 20;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7
.= F.f1 by A9,FUNCTOR0:def 16;
then G1.(F1.f) = Morph-Map(G,F.b1,F.c1).(F.f1) by A6,A8;
hence (G1*F1).f = Morph-Map(G,F.b1,F.c1).(F.f1) by A7,FUNCTOR3:8
.= G.(F.f1) by A9,A10,FUNCTOR0:def 17
.= (G*F).f1 by A9,FUNCTOR3:8
.= Morph-Map(G*F,b1,c1).f1 by A9,A10,FUNCTOR0:def 17;
end;
theorem
for A1,A2,A3 being category
for F being contravariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3
st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G
holds B1,B3 are_isomorphic_under G*F
proof let A1,A2,A3 be category;
let F be contravariant Functor of A1,A2;
let G be contravariant Functor of A2,A3;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2;
let B3 be non empty subcategory of A3;
assume B1 is subcategory of A1 & B2 is subcategory of A2;
given F1 being contravariant Functor of B1,B2 such that
A1: F1 is bijective and
A2: for a being object of B1, a1 being object of A1 st a = a1 holds F1.a = F.a1
and
A3: for b,c being object of B1, b1,c1 being object of A1
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds F1.f = Morph-Map(F,b1,c1).f1;
assume B2 is subcategory of A2 & B3 is subcategory of A3;
given G1 being contravariant Functor of B2,B3 such that
A4: G1 is bijective and
A5: for a being object of B2, a1 being object of A2 st a = a1 holds G1.a = G.a1
and
A6: for b,c being object of B2, b1,c1 being object of A2
st <^b,c^> <> {} & b = b1 & c = c1
for f being Morphism of b,c, f1 being Morphism of b1,c1
st f = f1 holds G1.f = Morph-Map(G,b1,c1).f1;
thus B1 is subcategory of A1 & B3 is subcategory of A3;
take G1*F1; thus G1*F1 is bijective by A1,A4,FUNCTOR1:13;
hereby let a be object of B1, b be object of A1;
assume a = b;
then F1.a = F.b by A2;
then G1.(F1.a) = G.(F.b) by A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:34 .= (G*F).b by FUNCTOR0:34;
end;
let b,c be object of B1, b1,c1 be object of A1 such that
A7: <^b,c^> <> {} & b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A8: <^F1.c, F1.b^> <> {} & F1.b = F.b1 & F1.c = F.c1 by A2,A7,FUNCTOR0:def 20;
then A9: f in <^b,c^> & <^b,c^> c= <^b1,c1^> &
F1.f in <^F1.c, F1.b^> & <^F1.c, F1.b^> c= <^F.c1, F.b1^>
by A7,ALTCAT_2:32;
then A10: <^(G*F).b1, (G*F).c1^> <> {} & (G*F).b1 = G.(F.b1) & (G*F).c1 = G.(F.
c1)
by FUNCTOR0:34,def 19;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7
.= F.f1 by A9,FUNCTOR0:def 17;
then G1.(F1.f) = Morph-Map(G,F.c1,F.b1).(F.f1) by A6,A8;
hence (G1*F1).f = Morph-Map(G,F.c1,F.b1).(F.f1) by A7,FUNCTOR3:7
.= G.(F.f1) by A9,A10,FUNCTOR0:def 17
.= (G*F).f1 by A9,FUNCTOR3:7
.= Morph-Map(G*F,b1,c1).f1 by A9,A10,FUNCTOR0:def 16;
end;