:: Miscellaneous Facts about Functors
:: by Grzegorz Bancerek
::
:: Received July 31, 2001
:: Copyright (c) 2001-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 RELAT_2, ALTCAT_1, XBOOLE_0, MSUALG_6, FUNCTOR0, FUNCT_2,
FUNCT_1, RELAT_1, CAT_1, ENS_1, PARTFUN1, ZFMISC_1, STRUCT_0, YELLOW18,
SETFAM_1, PBOOLE, ALTCAT_2, TARSKI, SUBSET_1, REALSET1, FUNCOP_1,
FUNCT_3, MCART_1, MSUALG_3, WELLORD1, ARYTM_0, YELLOW20, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, MCART_1, BINOP_1, REALSET1, MULTOP_1, PBOOLE, STRUCT_0, FUNCT_4,
PARTFUN1, FUNCOP_1, MSUALG_3, FUNCT_3, ALTCAT_1, ALTCAT_2, FUNCTOR0,
FUNCTOR3, YELLOW18;
constructors REALSET1, MSUALG_3, FUNCTOR3, YELLOW18, RELSET_1, XTUPLE_0;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, STRUCT_0,
ALTCAT_2, FUNCTOR0, FUNCTOR2, ALTCAT_4, YELLOW18, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_1, PARTFUN1, PBOOLE, MSUALG_3, ALTCAT_1, ALTCAT_2,
FUNCTOR0, FUNCT_2, XBOOLE_0;
equalities ALTCAT_1, FUNCTOR0, XBOOLE_0, BINOP_1, REALSET1;
expansions TARSKI, PARTFUN1, MSUALG_3, ALTCAT_2, FUNCTOR0, XBOOLE_0;
theorems ZFMISC_1, RELAT_1, FUNCT_1, PBOOLE, MCART_1, FUNCT_2, FUNCT_3,
FUNCT_4, ALTCAT_1, ALTCAT_2, FUNCTOR3, ALTCAT_4, FUNCTOR0, FUNCTOR1,
FUNCTOR2, PARTFUN1, MULTOP_1, MSUALG_3, YELLOW18, XBOOLE_0, XBOOLE_1,
XTUPLE_0;
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;
reconsider G = F" as feasible reflexive FunctorStr over B,A by A1,FUNCTOR0:35
,36;
let a be Object of A, b be Object of B;
F" * F = id A by A1,FUNCTOR1:19;
then a = (F" * F).a by FUNCTOR0:29;
hence F.a = b implies F".b = a by FUNCTOR0:33;
F * G = id B by A1,FUNCTOR1:18;
then b = (F * G).b by FUNCTOR0:29;
hence thesis by FUNCTOR0:33;
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 and
A2: G = F";
let a1,a2 be Object of A such that
A3: <^a1,a2^> <> {};
A4: <^F.a1,F.a2^> <> {} by A3,FUNCTOR0:def 18;
F is surjective by A1;
then F is onto;
then F is reflexive coreflexive by FUNCTOR0:44;
then
A5: G.(F.a1) = a1 & G.(F.a2) = a2 by A1,A2,Th1;
let f be Morphism of a1,a2, g be Morphism of F.a1, F.a2;
F" * F = id A by A1,FUNCTOR1:19;
then f = (G * F).f by A2,A3,FUNCTOR0:31;
hence F.f = g implies G.g = f by A3,FUNCTOR3:6;
F * G = id B by A1,A2,FUNCTOR1:18;
then g = (F * G).g by A4,FUNCTOR0:31;
hence thesis by A4,A5,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 and
A2: G = F";
let a1,a2 be Object of A such that
A3: <^a1,a2^> <> {};
A4: <^F.a2,F.a1^> <> {} by A3,FUNCTOR0:def 19;
F is surjective by A1;
then F is onto;
then F is reflexive coreflexive by FUNCTOR0:45;
then
A5: G.(F.a1) = a1 & G.(F.a2) = a2 by A1,A2,Th1;
let f be Morphism of a1,a2, g be Morphism of F.a2, F.a1;
F" * F = id A by A1,FUNCTOR1:19;
then f = (G * F).f by A2,A3,FUNCTOR0:31;
hence F.f = g implies G.g = f by A3,FUNCTOR3:7;
F * G = id B by A1,A2,FUNCTOR1:18;
then g = (F * G).g by A4,FUNCTOR0:31;
hence thesis by A4,A5,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:35;
A2: F"*F = id A by A1,FUNCTOR1:19;
let G be Functor of B,A;
assume F * G = id B;
then (id A)*G = FF * id B by A2,FUNCTOR0:32
.= F" by FUNCTOR3:5;
hence thesis 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:35;
A2: F*FF = id B by A1,FUNCTOR1:18;
let G be Functor of B,A;
assume G * F = id A;
then (id A)*FF = G * id B by A2,FUNCTOR0:32
.= the FunctorStr of G by FUNCTOR3:5;
hence thesis 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 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:31;
end;
now
let b be Object of B;
thus (F*G).b = F.(G.b) by FUNCTOR0:33
.= b by A2
.= (id B).b by FUNCTOR0:29;
end;
hence thesis by A1,A4,Th4,YELLOW18:1;
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 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:31;
end;
now
let b be Object of B;
thus (F*G).b = F.(G.b) by FUNCTOR0:33
.= b by A2
.= (id B).b by FUNCTOR0:29;
end;
hence thesis by A1,A4,Th4,YELLOW18:1;
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 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:31;
end;
now
let b be Object of A;
thus (G*F).b = G.(F.b) by FUNCTOR0:33
.= b by A2
.= (id A).b by FUNCTOR0:29;
end;
hence thesis by A1,A4,Th5,YELLOW18:1;
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 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:31;
end;
now
let b be Object of A;
thus (G*F).b = G.(F.b) by FUNCTOR0:33
.= b by A2
.= (id A).b by FUNCTOR0:29;
end;
hence thesis by A1,A4,Th5,YELLOW18:1;
end;
begin :: Intersection of categories
definition
let A, B be AltCatStr;
pred A, B have_the_same_composition means
for a1, a2, a3 being object
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 object
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 object;
assume x in dom ((the Comp of A).[a1,a2,a3]) & x in dom ((the Comp of B).
[a1,a2,a3] );
then
A2: x in dom ((the Comp of A).[a1,a2,a3]) /\ dom ((the Comp of B).[a1,a2,
a3] ) by XBOOLE_0:def 4;
(the Comp of A).[a1,a2,a3] tolerates (the Comp of B).[a1,a2,a3] by A1;
hence
((the Comp of A).[a1,a2,a3]).x = ((the Comp of B).[a1,a2,a3]).x by A2;
end;
assume
A3: for a1,a2,a3,x being object
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 object;
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 4;
hence thesis by A3;
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;
<^b1,b3^> <> {} by A3,ALTCAT_1:def 2;
then dom ((the Comp of B).(b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by
FUNCT_2:def 1;
then
A7: [g2,g1] in dom ((the Comp of B).(b1,b2,b3)) by A3,ZFMISC_1:def 2;
<^a1,a3^> <> {} by A2,ALTCAT_1:def 2;
then dom ((the Comp of A).(a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by
FUNCT_2:def 1;
then
A8: [f2,f1] in dom ((the Comp of A).(a1,a2,a3)) by A2,ZFMISC_1:def 2;
A9: (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;
thus f2 * f1 = (the Comp of A).(a1,a2,a3).(f2,f1) by A2,ALTCAT_1:def 8
.= (the Comp of B).(b1,b2,b3).(g2,g1) by A1,A4,A5,A6,A9,A8,A7,Th10
.= g2 * g1 by A3,ALTCAT_1:def 8;
end;
assume
A10: 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 object;
assume
A11: x in dom ((the Comp of A).[a1,a2,a3]) /\ dom ((the Comp of B).[a1,
a2,a3]);
then
A12: x in dom ((the Comp of A).[a1,a2,a3]) by XBOOLE_0:def 4;
then [a1,a2,a3] in dom the Comp of A by FUNCT_1:def 2,RELAT_1:38;
then
A13: [a1,a2,a3] in [:the carrier of A, the carrier of A, the carrier of A :];
A14: x in dom ((the Comp of B).[a1,a2,a3]) by A11,XBOOLE_0:def 4;
then [a1,a2,a3] in dom the Comp of B by FUNCT_1:def 2,RELAT_1:38;
then
A15: [a1,a2,a3] in [:the carrier of B, the carrier of B, the carrier of B:];
reconsider a1,a2,a3 as Object of A by A13,MCART_1:69;
reconsider b1 = a1, b2 = a2, b3 = a3 as Object of B by A15,MCART_1:69;
A16: (the Comp of A).(a1,a2,a3) = (the Comp of A).[a1,a2,a3] by MULTOP_1:def 1;
then [:<^a2,a3^>,<^a1,a2^>:] <> {} implies <^a1,a3^> <> {} by A11,
XBOOLE_0:def 4;
then dom ((the Comp of A).(a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by
FUNCT_2:def 1;
then consider f2,f1 being object such that
A17: f2 in <^a2,a3^> and
A18: f1 in <^a1,a2^> and
A19: x = [f2,f1] by A12,A16,ZFMISC_1:def 2;
reconsider f1 as Morphism of a1,a2 by A18;
reconsider f2 as Morphism of a2,a3 by A17;
A20: (the Comp of B).(b1,b2,b3) = (the Comp of B).[b1,b2,b3] by MULTOP_1:def 1;
then [:<^b2,b3^>,<^b1,b2^>:] <> {} implies <^b1,b3^> <> {} by A11,
XBOOLE_0:def 4;
then
A21: dom ((the Comp of B).(b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by
FUNCT_2:def 1;
then
A22: f1 in <^b1,b2^> & f2 in <^b2,b3^> by A14,A20,A19,ZFMISC_1:87;
reconsider g2 = f2 as Morphism of b2,b3 by A14,A20,A21,A19,ZFMISC_1:87;
reconsider g1 = f1 as Morphism of b1,b2 by A14,A20,A21,A19,ZFMISC_1:87;
((the Comp of A).[a1,a2,a3]).x = (the Comp of A).(a1,a2,a3).(f2,f1) by A19,
MULTOP_1:def 1
.= f2 * f1 by A17,A18,ALTCAT_1:def 8
.= g2 * g1 by A10,A17,A18,A22
.= (the Comp of B).(b1,b2,b3).(g2,g1) by A22,ALTCAT_1:def 8;
hence thesis by A19,MULTOP_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^> <> {} and
A2: <^a2,a3^> <> {};
let b1,b2,b3 be Object of B such that
A3: <^b1,b2^> <> {} & <^b2,b3^> <> {} and
b1 = a1 and
b2 = a2 and
b3 = a3;
let f1 be Morphism of a1,a2, g1 be Morphism of b1,b2 such that
A4: g1 = f1;
reconsider f = f1 as Function of the_carrier_of a1, the_carrier_of a2 by A1
,YELLOW18:34;
let f2 be Morphism of a2,a3, g2 be Morphism of b2,b3 such that
A5: g2 = f2;
A6: <^b1,b3^> <> {} by A3,ALTCAT_1:def 2;
reconsider g = f2 as Function of the_carrier_of a2, the_carrier_of a3 by A2
,YELLOW18:34;
<^a1,a3^> <> {} by A1,A2,ALTCAT_1:def 2;
hence f2 * f1 = g * f by A1,A2,ALTCAT_1:def 12
.= g2 * g1 by A3,A4,A5,A6,ALTCAT_1:def 12;
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 object st x in (dom f) /\ (dom g) holds it.x = (f.x) /\ (g.x);
existence
proof
deffunc F(object) = (f.$1) /\ (g.$1);
thus ex h being Function st dom h = (dom f) /\ (dom g) &
for x being object
st x in (dom f) /\ (dom g) holds h.x = F(x) from FUNCT_1:sch 3;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = (dom f) /\ (dom g) and
A2: for x being object 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 object
st x in (dom f) /\ (dom g) holds f2.x = (f.x) /\ ( g.x);
now
let x be object;
assume
A5: x in (dom f) /\ (dom g);
then f1.x = (f.x) /\ (g.x) by A2;
hence f1.x = f2.x by A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
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 PARTFUN1:def 2;
then dom Intersect(A,B) = I /\ I by Def2;
then reconsider AB = Intersect(A,B) as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
I /\ I = I;
then for i being object st i in I holds AB.i = A.i /\ B.i by A1,Def2;
hence thesis by PBOOLE:def 5;
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 PARTFUN1:def 2;
then dom Intersect(A,B) = I /\ J by Def2;
hence thesis by PARTFUN1:def 2,RELAT_1:def 18;
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 by PARTFUN1:def 2;
dom C = J by PARTFUN1:def 2;
then
A3: J = I /\ dom B by A1,A2,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 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;
A3: dom B1 = I1 & dom B2 = I2 by PARTFUN1:def 2;
reconsider H = Intersect(F, G) as ManySortedSet of I1 /\ I2 by Th14;
A4: dom F = I1 & dom G = I2 by PARTFUN1:def 2;
A5: dom A1 = I1 & dom A2 = I2 by PARTFUN1:def 2;
H is ManySortedFunction of A, B
proof
let i be object;
assume
A6: i in I1 /\ I2;
then
A7: H.i = (F.i)/\(G.i) by A4,Def2;
A8: i in I2 by A6,XBOOLE_0:def 4;
then
A9: G.i is Function of A2.i, B2.i by PBOOLE:def 15;
A10: A.i = (A1.i)/\(A2.i) & B.i = (B1.i)/\(B2.i) by A1,A5,A3,A6,Def2;
A11: i in I1 by A6,XBOOLE_0:def 4;
then F.i is Function of A1.i, B1.i by PBOOLE:def 15;
hence thesis by A2,A4,A11,A8,A10,A7,A9,FUNCT_2:120;
end;
hence thesis;
end;
theorem Th17:
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:100;
then reconsider H = Intersect(F, G) as ManySortedSet of [:I/\J,I/\J:] by Th14
;
[:I,I,I:] = [:[:I,I:],I:] & [:J,J,J:] = [:[:J,J:],J:] by ZFMISC_1:def 3;
then
A2: [:I,I,I:]/\[:J,J,J:] = [:[:I/\J,I/\J:],I/\J:] by A1,ZFMISC_1:100
.= [:I/\J,I/\J,I/\J:] by ZFMISC_1:def 3;
A3: dom F = [:I,I:] & dom G = [:J,J:] by PARTFUN1:def 2;
A4: now
let x be object;
assume
A5: x in [:I,I,I:]/\[:J,J,J:];
then
A6: x in [:J,J,J:] by XBOOLE_0:def 4;
x in [:I,I,I:] by A5,XBOOLE_0:def 4;
then consider a,b,c being object such that
A7: a in I and
A8: b in I and
A9: c in I and
A10: x = [a,b,c] by MCART_1:68;
A11: c in J by A6,A10,MCART_1:69;
then
A12: c in I/\J by A9,XBOOLE_0:def 4;
A13: a in J by A6,A10,MCART_1:69;
then
A14: a in I/\J by A7,XBOOLE_0:def 4;
then
A15: [a,c] in [:I/\J,I/\J:] by A12,ZFMISC_1:87;
A16: b in J by A6,A10,MCART_1:69;
then
A17: {|G|}.(a,b,c) = G.(a,c) by A13,A11,ALTCAT_1:def 3;
A18: {|F|}.(a,b,c) = F.(a,c) by A7,A8,A9,ALTCAT_1:def 3;
b in I/\J by A8,A16,XBOOLE_0:def 4;
then {|H|}.(a,b,c) = H.(a,c) by A14,A12,ALTCAT_1:def 3;
hence {|H|}.x = H.[a,c] by A10,MULTOP_1:def 1
.= (F.(a,c))/\(G.[a,c]) by A1,A3,A15,Def2
.= ({|F|}.x)/\(G.(a,c)) by A10,A18,MULTOP_1:def 1
.= {|F|}.x /\ {|G|}.x by A10,A17,MULTOP_1:def 1;
end;
take H;
thus H = Intersect(F, G);
A19: dom {|H|} = [:I/\J,I/\J,I/\ J:] by PARTFUN1:def 2;
dom {|F|} = [:I,I,I:] & dom {|G|} = [:J,J,J:] by PARTFUN1:def 2;
hence thesis by A19,A2,A4,Def2;
end;
theorem Th18:
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: dom F2 = [:I,I:] & dom G2 = [:J,J:] by PARTFUN1:def 2;
A2: [:I/\J,I/\J:] = [:I,I:]/\[:J,J:] by ZFMISC_1:100;
then reconsider
H1 = Intersect(F1, G1), H2 = Intersect(F2, G2) as ManySortedSet
of [:I/\J,I/\J:] by Th14;
[: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 A2,ZFMISC_1:100
.= [:I/\J,I/\J,I/\J:] by ZFMISC_1:def 3;
A4: dom F1 = [:I,I:] & dom G1 = [:J,J:] by PARTFUN1:def 2;
A5: now
let x be object;
assume
A6: x in [:I,I,I:]/\[:J,J,J:];
then
A7: x in [:J,J,J:] by XBOOLE_0:def 4;
x in [:I,I,I:] by A6,XBOOLE_0:def 4;
then consider a,b,c being object such that
A8: a in I and
A9: b in I and
A10: c in I and
A11: x = [a,b,c] by MCART_1:68;
A12: b in J by A7,A11,MCART_1:69;
then
A13: b in I/\J by A9,XBOOLE_0:def 4;
A14: c in J by A7,A11,MCART_1:69;
then
A15: c in I/\J by A10,XBOOLE_0:def 4;
then
A16: [b,c] in [:I/\J,I/\J:] by A13,ZFMISC_1:87;
A17: a in J by A7,A11,MCART_1:69;
then
A18: a in I/\J by A8,XBOOLE_0:def 4;
then
A19: [a,b] in [:I/\J,I/\J:] by A13,ZFMISC_1:87;
A20: {|F1, F2|}.(a,b,c) = [:F2.(b,c),F1.(a,b):] by A8,A9,A10,ALTCAT_1:def 4;
A21: {|G1, G2|}.(a,b,c) = [:G2.(b,c),G1.(a,b):] by A17,A12,A14,ALTCAT_1:def 4;
{|H1, H2|}.(a,b,c) = [:H2.(b,c),H1.(a,b):] by A18,A13,A15,ALTCAT_1:def 4;
hence {|H1, H2|}.x = [:H2.(b,c),H1.(a,b):] by A11,MULTOP_1:def 1
.= [:(F2.[b,c])/\(G2.[b,c]), H1.(a,b):] by A2,A1,A16,Def2
.= [:(F2.[b,c])/\(G2.[b,c]), (F1.[a,b])/\(G1.[a,b]):] by A2,A4,A19,Def2
.= [:F2.[b,c],F1.[a,b]:]/\[:G2.[b,c],G1.[a,b]:] by ZFMISC_1:100
.= ({|F1,F2|}.x)/\[:G2.[b,c],G1.[a,b]:] by A11,A20,MULTOP_1:def 1
.= {|F1,F2|}.x /\ {|G1,G2|}.x by A11,A21,MULTOP_1:def 1;
end;
take H1, H2;
thus H1 = Intersect(F1, G1) & H2 = Intersect(F2, G2);
A22: dom {|H1, H2|} = [:I/\J,I/\J,I/\J:] by PARTFUN1:def 2;
dom {|F1, F2|} = [:I,I,I:] & dom {|G1, G2|} = [:J,J,J:] by PARTFUN1:def 2;
hence thesis by A22,A3,A5,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
A2: now
let x be set;
assume
A3: x in dom the Comp of A;
assume x in dom the Comp of B;
ex a1,a2,a3 being object
st a1 in the carrier of A & a2 in the carrier
of A & a3 in the carrier of A & x = [a1,a2,a3] by A3,MCART_1:68;
hence (the Comp of A).x tolerates (the Comp of B).x by A1;
end;
set Cr = (the carrier of A) /\ (the carrier of B);
A4: [: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;
[:Cr, Cr:] = [:the carrier of A, the carrier of A:] /\ [:the carrier
of B, the carrier of B:] & [:the carrier of A, the carrier of A, the carrier of
A:] = [:[:the carrier of A, the carrier of A:], the carrier of A:] by
ZFMISC_1:100,def 3;
then
A5: [: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
A4,ZFMISC_1:100
.= [:Cr, Cr, Cr:] by ZFMISC_1:def 3;
consider Ar being ManySortedSet of [:Cr,Cr:] such that
A6: Ar = Intersect(the Arrows of A, the Arrows of B) and
A7: Intersect({|the Arrows of A|}, {|the Arrows of B|}) = {|Ar|} by Th17;
ex Ar1,Ar2 being ManySortedSet of [:Cr,Cr:] st Ar1 = Intersect(the
Arrows of A, the Arrows of B) & Ar2 = Intersect(the Arrows of A, the Arrows of
B) & Intersect({|the Arrows of A, the Arrows of A|}, {|the Arrows of B, the
Arrows of B|}) = {|Ar1,Ar2|} by Th18;
then reconsider Cm = Intersect(the Comp of A, the Comp of B) as
ManySortedFunction of {|Ar,Ar|}, {|Ar|} by A6,A7,A5,A2,Th16;
take AltCatStr(#Cr,Ar,Cm#);
thus thesis by A6;
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
A2: the Comp of AB = Intersect(the Comp of A, the Comp of B) by Def3;
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) by A1,Def3;
hence thesis by A1,A2,Def3;
end;
theorem Th20:
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
A1: A, B have_the_same_composition;
then
A2: the Comp of AB = Intersect(the Comp of A, the Comp of B) by Def3;
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) by A1,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 A2,Th15,XBOOLE_1:17;
end;
theorem Th21:
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;
the carrier of Intersect(A, B) = (the carrier of A)/\(the carrier of B)
by A1,Def3;
then
A2: [: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:100;
let a1,a2 be Object of A, b1,b2 be Object of B;
let o1, o2 be Object of Intersect(A, B) such that
A3: o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2;
A4: 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 A3,A2,XBOOLE_0:def 4;
end;
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:] by PARTFUN1:def 2;
A6: now
assume the carrier of A = {} or the carrier of B = {};
then
A7: [:the carrier of A, the carrier of A:] = {} or [:the carrier of B,
the carrier of B:] = {} by ZFMISC_1:90;
then (the Arrows of A).[a1,a2] = {} or (the Arrows of B).[b1,b2] = {};
hence (the Arrows of A).[a1,a2] /\ (the Arrows of B).[b1,b2] = {} & (the
Arrows of Intersect(A,B)).[o1,o2] = {} by A2,A7;
end;
the Arrows of Intersect(A,B) = Intersect(the Arrows of A, the Arrows of
B) by A1,Def3;
hence thesis by A3,A2,A5,A4,A6,Def2;
end;
theorem Th22:
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) by Def3;
let o1,o2,o3 be Object of AB such that
A3: <^o1,o2^> <> {} and
A4: <^o2,o3^> <> {};
dom the Arrows of AB = [:the carrier of AB, the carrier of AB:] & [o1,o2
] in dom the Arrows of AB by A3,FUNCT_1:def 2,PARTFUN1:def 2;
then
A5: o1 in the carrier of AB by ZFMISC_1:87;
then reconsider A, B as non empty transitive AltCatStr by A2,XBOOLE_0:def 4;
reconsider b1=o1, b2=o2, b3=o3 as Object of B by A2,A5,XBOOLE_0:def 4;
reconsider a1=o1, a2=o2, a3=o3 as Object of A by A2,A5,XBOOLE_0:def 4;
set f = the Morphism of o1,o2,g = the Morphism of o2,o3;
A6: <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> by A1,Th21;
then
A7: g in <^a2,a3^> & g in <^b2,b3^> by A4,XBOOLE_0:def 4;
A8: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1,Th21;
then reconsider f1 = f as Morphism of a1,a2 by A3,XBOOLE_0:def 4;
reconsider g2 = g as Morphism of b2,b3 by A4,A6,XBOOLE_0:def 4;
reconsider g1 = g as Morphism of a2,a3 by A4,A6,XBOOLE_0:def 4;
reconsider f2 = f as Morphism of b1,b2 by A3,A8,XBOOLE_0:def 4;
f in <^a1,a2^> & f in <^b1,b2^> by A3,A8,XBOOLE_0:def 4;
then
A9: g1 * f1 = g2 * f2 by A1,A7,Th11;
A10: <^b2,b3^> <> {} by A4,A6;
A11: <^a2,a3^> <> {} by A4,A6;
<^b1,b2^> <> {} by A3,A8;
then
A12: <^b1,b3^> <> {} by A10,ALTCAT_1:def 2;
<^a1,a2^> <> {} by A3,A8;
then
A13: <^a1,a3^> <> {} by A11,ALTCAT_1:def 2;
<^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> by A1,Th21;
hence thesis by A13,A12,A9,XBOOLE_0:def 4;
end;
theorem Th23:
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,Th21;
hence thesis by XBOOLE_0:def 4;
end;
theorem
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 Th23;
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,Th20,Th22;
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;
reconsider b = o as Object of B by A4,XBOOLE_0:def 4;
assume
A5: o = a;
then idm a = idm b by A3;
hence idm a in <^o,o^> by A1,A5,Th23;
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(), a9,b9 being Object of B1() st a9 = a &
b9 = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> 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(), a9,b9 being Object of B2() st a9 = a &
b9 = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a
,b,f]
proof
A5: the carrier of B1() c= the carrier of A() by ALTCAT_2:def 11;
A6: the carrier of B2() c= the carrier of A() by ALTCAT_2:def 11;
A7: the carrier of B1() = the carrier of B2()
proof
hereby
let x be object;
assume
x in the carrier of B1();
then reconsider a = x as Object of B1();
reconsider a as Object of A() by A5;
P[a] by A1;
then a is Object of B2() by A3;
hence x in the carrier of B2();
end;
let x be object;
assume
x in the carrier of B2();
then reconsider a = x as Object of B2();
reconsider a as Object of A() by A6;
P[a] by A3;
then a is Object of B1() by A1;
hence thesis;
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 A7;
reconsider a9 = a, b9 = b as Object of A() by A5;
A8: <^x2,y2^> c= <^a9,b9^> by ALTCAT_2:31;
A9: <^x2,y2^> c= <^x1,y1^>
proof
let f be object;
assume
A10: f in <^x2,y2^>;
then reconsider f as Morphism of a9,b9 by A8;
Q[a9,b9,f] by A4,A8,A10;
hence thesis by A2,A8,A10;
end;
A11: <^x1,y1^> c= <^a9,b9^> by ALTCAT_2:31;
<^x1,y1^> c= <^x2,y2^>
proof
let f be object;
assume
A12: f in <^x1,y1^>;
then reconsider f as Morphism of a9,b9 by A11;
Q[a9,b9,f] by A2,A11,A12;
hence thesis by A4,A11,A12;
end;
hence (the Arrows of B1()).(a,b) = (the Arrows of B2()).(a,b) by A9;
end;
hence thesis by A7,ALTCAT_1:7,ALTCAT_2:26;
end;
theorem Th26:
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:28;
A1: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
A2: dom the Arrows of B = [:the carrier of B, the carrier of B:] by
PARTFUN1:def 2;
assume
A3: for a1,a2 being Object of A, b1,b2 being Object of B st b1 = a1 & b2
= a2 holds <^b1,b2^> = <^a1,a2^>;
A4: now
let x be object;
assume x in dom the Arrows of B;
then consider b1,b2 being object such that
A5: b1 in the carrier of B & b2 in the carrier of B and
A6: x = [b1,b2] by ZFMISC_1:def 2;
reconsider b1, b2 as Object of B by A5;
reconsider a1 = b1, a2 = b2 as Object of A by A1;
thus (the Arrows of B).x = <^b1,b2^> by A6
.= <^a1,a2^> by A3
.= (the Arrows of A).x by A6;
end;
A7: dom the Arrows of A = [:the carrier of A, the carrier of A:] by
PARTFUN1:def 2;
[: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 A1,XBOOLE_1:28
,ZFMISC_1:96;
hence the Arrows of B = (the Arrows of A)||the carrier of B by A7,A2,A4,
FUNCT_1:46;
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 Q[set,set,set] means not contradiction;
A2: 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];
A3: for a being Object of A() st P[a] holds Q[a,a, idm a];
A4: ex a being Object of A() st P[a] by A1;
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(), a9,b9 being Object of B st a9 = a & b9
= b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,
f] from YELLOW18:sch 7(A4,A2,A3);
now
let a1,a2 be Object of A(), b1,b2 be Object of B;
assume
A7: b1 = a1 & b2 = a2;
A8: <^a1,a2^> c= <^b1,b2^>
by A6,A7;
<^b1,b2^> c= <^a1,a2^> by A7,ALTCAT_2:31;
hence <^b1,b2^> = <^a1,a2^> by A8;
end;
then B is full by Th26;
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
A3: 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;
A4: now
let a,b be Object of A(), a9,b9 be Object of B1();
assume a9 = a & b9 = b;
then <^a9,b9^> = <^a,b^> by Th26;
hence <^a,b^> <> {} implies for f being Morphism of a,b holds f in <^a9,b9
^> iff Q[a,b,f];
end;
A5: now
let a,b be Object of A(), a9,b9 be Object of B2();
assume a9 = a & b9 = b;
then <^a9,b9^> = <^a,b^> by Th26;
hence <^a,b^> <> {} implies for f being Morphism of a,b holds f in <^a9,b9
^> iff Q[a,b,f];
end;
A6: for a being Object of A() holds a is Object of B1() iff P[a] by A1;
thus thesis from SubcategoryUniq(A6,A4,A3,A5);
end;
begin :: Inclusion functors and functor restrictions
registration
let f be Function-yielding Function;
let x,y be set;
cluster f.(x,y) -> Relation-like Function-like;
coherence;
end;
theorem Th27:
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;
let a,b be Object of C such that
A1: <^a,b^> <> {};
let f be Morphism of a,b;
A2: the MorphMap of incl C = id the Arrows of C & [a,b] in [:the carrier of
C, the carrier of C:] by FUNCTOR0:def 28,ZFMISC_1:def 2;
<^(incl C).a, (incl C).b^> <> {} by A1,FUNCTOR0:28,XBOOLE_1:3;
hence (incl C).f = Morph-Map(incl C, a, b).f by A1,FUNCTOR0:def 15
.= (id ((the Arrows of C).(a,b))).f by A2,MSUALG_3:def 1
.= f;
end;
registration
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;
A1: (incl C).a = a by FUNCTOR0:27;
thus Morph-Map(incl C, a, a).idm a = (incl C).idm a by FUNCTOR0:def 15
.= idm a by Th27
.= idm ((incl C).a) by A1,ALTCAT_2:34;
end;
let o1,o2,o3 be Object of C such that
A2: <^o1,o2^> <> {} & <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
<^o1,o3^> <> {} by A2,ALTCAT_1:def 2;
then
A3: (incl C).o3 = o3 & (incl C).(g*f) = g*f by Th27,FUNCTOR0:27;
A4: (incl C).o1 = o1 & (incl C).o2 = o2 by FUNCTOR0:27;
(incl C).g = g & (incl C).f = f by A2,Th27;
hence thesis by A2,A4,A3,ALTCAT_2:32;
end;
end;
registration
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; :: redefines incl (FUNCTOR0, definition)
coherence by FUNCTOR0:def 25;
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; :: redefines | (FUNCTOR0, definition)
coherence
proof
F|C = F*incl C;
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; :: redefines | (FUNCTOR0, definition)
coherence
proof
F|C = F*incl C;
hence thesis;
end;
end;
theorem Th28:
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;
let b be Object of A;
let a be Object of C;
assume a = b;
then (incl C).a = b by FUNCTOR0:27;
hence thesis by FUNCTOR0:33;
end;
theorem Th29:
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;
let a,b be Object of A;
let c,d be Object of C;
assume that
A1: c = a & d = b and
A2: <^c,d^> <> {};
let f be Morphism of a,b;
let g be Morphism of c,d;
assume g = f;
then
A3: (incl C).g = f by A2,Th27;
(incl C).c = a & (incl C).d = b by A1,FUNCTOR0:27;
hence thesis by A2,A3,FUNCTOR3:6;
end;
theorem Th30:
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;
let a,b be Object of A;
let c,d be Object of C;
assume that
A1: c = a & d = b and
A2: <^c,d^> <> {};
let f be Morphism of a,b;
let g be Morphism of c,d;
assume g = f;
then
A3: (incl C).g = f by A2,Th27;
(incl C).c = a & (incl C).d = b by A1,FUNCTOR0:27;
hence thesis by A2,A3,FUNCTOR3:8;
end;
theorem Th31:
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:7;
let a,b be Object of A such that
A3: F.a = F.b;
A4: [f.a,f.a]`1 = f.a & [f.b,f.b]`1 = f.b;
(the ObjectMap of F).(a,a) = [f.a, f.a] & (the ObjectMap of F).(b,b) = [
f.b, f.b] by A1,FUNCT_3:75;
hence thesis by A2,A3,A4,FUNCT_2:19;
end;
theorem Th32:
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;
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 PARTFUN1:def 2,ZFMISC_1:def 2;
then
A3: Morph-Map(F,a,b) is one-to-one by A1;
A4: <^F.a, F.b^> <> {} by A2,FUNCTOR0:def 18;
then F.f = Morph-Map(F,a,b).f & F.g = Morph-Map(F,a,b).g by A2,
FUNCTOR0:def 15;
hence thesis by A2,A4,A3,FUNCT_2:19;
end;
theorem Th33:
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:];
let a,b be Object of B such that
A3: <^a,b^> <> {};
the ObjectMap of F is Covariant by FUNCTOR0:def 12;
then consider
g being Function of the carrier of A, the carrier of B such that
A4: the ObjectMap of F = [:g,g:];
let f be Morphism of a,b;
dom the ObjectMap of F = [:the carrier of A, the carrier of A:] & [a,b]
in rng the ObjectMap of F by A2,FUNCT_2:def 1,ZFMISC_1:def 2;
then consider x being object such that
A5: x in [:the carrier of A, the carrier of A:] and
A6: [a,b] = (the ObjectMap of F).x by FUNCT_1:def 3;
consider c,d being object such that
A7: c in the carrier of A & d in the carrier of A and
A8: [c,d] = x by A5,ZFMISC_1:def 2;
reconsider c, d as Object of A by A7;
(the ObjectMap of F).(d,d) = [g.d, g.d] by A4,FUNCT_3:75;
then
A9: F.d = g.d;
(the ObjectMap of F).(c,c) = [g.c, g.c] by A4,FUNCT_3:75;
then F.c = g.c;
then
A10: (the ObjectMap of F).(c,d) = [F.c,F.d] by A4,A9,FUNCT_3:75;
rng Morph-Map(F,c,d) = ((the Arrows of B)*the ObjectMap of F).[c,d] by A1,A5
,A8
.= <^a,b^> by A5,A6,A8,FUNCT_2:15;
then consider g being object such that
A11: g in dom Morph-Map(F,c,d) and
A12: f = Morph-Map(F,c,d).g by A3,FUNCT_1:def 3;
take c, d;
reconsider g as Morphism of c,d by A11;
take g;
thus a = F.c & b = F.d & <^c,d^> <> {} by A6,A8,A10,A11,XTUPLE_0:1;
thus thesis by A3,A6,A8,A10,A11,A12,FUNCTOR0:def 15;
end;
theorem Th34:
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:9;
then
A2: f is one-to-one by FUNCTOR0:7;
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:] by
FUNCT_2:def 1;
[b,b] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then (the ObjectMap of F).(b,b) = [:f,f:].(b,b) by A1,A4,FUNCT_4:43;
then
A5: (the ObjectMap of F).(b,b) = [f.b, f.b] by FUNCT_3:75;
[a,a] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then (the ObjectMap of F).(a,a) = [:f,f:].(a,a) by A1,A4,FUNCT_4:43;
then
A6: (the ObjectMap of F).(a,a) = [f.a, f.a] by FUNCT_3:75;
[f.a,f.a]`1 = f.a & [f.b,f.b]`1 = f.b;
hence thesis by A2,A3,A6,A5,FUNCT_2:19;
end;
theorem Th35:
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;
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 PARTFUN1:def 2,ZFMISC_1:def 2;
then
A3: Morph-Map(F,a,b) is one-to-one by A1;
A4: <^F.b, F.a^> <> {} by A2,FUNCTOR0:def 19;
then F.f = Morph-Map(F,a,b).f & F.g = Morph-Map(F,a,b).g by A2,
FUNCTOR0:def 16;
hence thesis by A2,A4,A3,FUNCT_2:19;
end;
theorem Th36:
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:];
let a,b be Object of B such that
A3: <^a,b^> <> {};
let f be Morphism of a,b;
dom the ObjectMap of F = [:the carrier of A, the carrier of A:] & [a,b]
in rng the ObjectMap of F by A2,FUNCT_2:def 1,ZFMISC_1:def 2;
then consider x being object such that
A4: x in [:the carrier of A, the carrier of A:] and
A5: [a,b] = (the ObjectMap of F).x by FUNCT_1:def 3;
A6: dom the ObjectMap of F = [:the carrier of A, the carrier of A:] by
FUNCT_2:def 1;
the ObjectMap of F is Contravariant 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:];
consider d,c being object such that
A8: d in the carrier of A & c in the carrier of A and
A9: [d,c] = x by A4,ZFMISC_1:def 2;
reconsider c, d as Object of A by A8;
[c,c] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then (the ObjectMap of F).(c,c) = [:g,g:].(c,c) by A7,A6,FUNCT_4:43;
then (the ObjectMap of F).(c,c) = [g.c, g.c] by FUNCT_3:75;
then
A10: F.c = g.c;
[d,d] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then (the ObjectMap of F).(d,d) = [:g,g:].(d,d) by A7,A6,FUNCT_4:43;
then (the ObjectMap of F).(d,d) = [g.d, g.d] by FUNCT_3:75;
then
A11: F.d = g.d;
[d,c] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then
A12: (the ObjectMap of F).(d,c) = [:g,g:].(c,d) by A7,A6,FUNCT_4:43
.= [F.c,F.d] by A10,A11,FUNCT_3:75;
rng Morph-Map(F,d,c) = ((the Arrows of B)*the ObjectMap of F).[d,c] by A1,A4
,A9
.= <^a,b^> by A4,A5,A9,FUNCT_2:15;
then consider g being object such that
A13: g in dom Morph-Map(F,d,c) and
A14: f = Morph-Map(F,d,c).g by A3,FUNCT_1:def 3;
take d,c;
reconsider g as Morphism of d,c by A13;
take g;
thus b = F.d & a = F.c & <^d,c^> <> {} by A5,A9,A12,A13,XTUPLE_0:1;
thus thesis by A3,A5,A9,A12,A13,A14,FUNCTOR0:def 16;
end;
begin :: Isomorphisms under arbitrary functor
definition
let A,B be category;
let F be FunctorStr over A,B;
let A9, B9 be category;
pred A9,B9 are_isomorphic_under F means
A9 is subcategory of A & B9 is
subcategory of B & ex G being covariant Functor of A9,B9 st G is bijective & (
for a9 being Object of A9, a being Object of A st a9 = a holds G.a9 = F.a) &
for b9,c9 being Object of A9, b,c being Object of A st <^b9,c9^> <> {} & b9 = b
& c9 = c for f9 being Morphism of b9,c9, f being Morphism of b,c st f9 = f
holds G.f9 = Morph-Map(F,b,c).f;
pred A9,B9 are_anti-isomorphic_under F means
A9 is subcategory of A & B9 is
subcategory of B & ex G being contravariant Functor of A9,B9 st G is bijective
& (for a9 being Object of A9, a being Object of A st a9 = a holds G.a9 = F.a) &
for b9,c9 being Object of A9, b,c being Object of A st <^b9,c9^> <> {} & b9 = b
& c9 = c for f9 being Morphism of b9,c9, f being Morphism of b,c st f9 = f
holds G.f9 = 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;
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;
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 and
B is subcategory of B;
given G being covariant Functor of A,B such that
A1: G is bijective and
A2: for a9 being Object of A, a being Object of A st a9 = a holds G.a9 =
F.a and
A3: for b9,c9 being Object of A, b,c being Object of A st <^b9,c9^> <>
{} & b9 = b & c9 = c for f9 being Morphism of b9,c9, f being Morphism of b,c st
f9 = f holds G.f9 = Morph-Map(F,b,c).f;
G is injective surjective by A1;
then
A4: G is one-to-one faithful full onto;
A5: now
let a,b be Object of A such that
A6: <^a,b^> <> {};
let f be Morphism of a,b;
<^F.a, F.b^> <> {} by A6,FUNCTOR0:def 18;
hence F.f = Morph-Map(F,a,b).f by A6,FUNCTOR0:def 15
.= G.f by A3,A6;
end;
for a being Object of A holds F.a = G.a by A2;
then the FunctorStr of F = the FunctorStr of G by A5,YELLOW18:1;
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
A4;
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 and
B is subcategory of B;
given G being contravariant Functor of A,B such that
A1: G is bijective and
A2: for a9 being Object of A, a being Object of A st a9 = a holds G.a9 =
F.a and
A3: for b9,c9 being Object of A, b,c being Object of A st <^b9,c9^> <>
{} & b9 = b & c9 = c for f9 being Morphism of b9,c9, f being Morphism of b,c st
f9 = f holds G.f9 = Morph-Map(F,b,c).f;
G is injective surjective by A1;
then
A4: G is one-to-one faithful full onto;
A5: now
let a,b be Object of A such that
A6: <^a,b^> <> {};
let f be Morphism of a,b;
<^F.b, F.a^> <> {} by A6,FUNCTOR0:def 19;
hence F.f = Morph-Map(F,a,b).f by A6,FUNCTOR0:def 16
.= G.f by A3,A6;
end;
for a being Object of A holds F.a = G.a by A2;
then the FunctorStr of F = the FunctorStr of G by A5,YELLOW18:2;
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
A4;
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;
the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B;
hence A is subcategory of A & B is subcategory of B by ALTCAT_2:20
,ALTCAT_4:35;
take F;
thus F is bijective & for a9 being Object of A, a being Object of A st a9 =
a holds F.a9 = F.a by A1;
let b9,c9 be Object of A, b,c be Object of A;
assume
A2: <^b9,c9^> <> {} & b9 = b & c9 = c;
then <^F.b,F.c^> <> {} by FUNCTOR0:def 18;
hence thesis by A2,FUNCTOR0:def 15;
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;
the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B;
hence A is subcategory of A & B is subcategory of B by ALTCAT_2:20
,ALTCAT_4:35;
take F;
thus F is bijective & for a9 being Object of A, a being Object of A st a9 =
a holds F.a9 = F.a by A1;
let b9,c9 be Object of A, b,c be Object of A;
assume
A2: <^b9,c9^> <> {} & b9 = b & c9 = c;
then <^F.c,F.b^> <> {} by FUNCTOR0:def 19;
hence thesis by A2,FUNCTOR0:def 16;
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:29
.= F.a1 by FUNCTOR0:29;
end;
let b,c be Object of B, b1,c1 be Object of A such that
A1: <^b,c^> <> {} and
A2: 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 A1,A2,ALTCAT_2:31;
A5: F.b1 = b1 & F.c1 = c1 by FUNCTOR0:29;
thus G.f = f by A1,FUNCTOR0:31
.= F.f1 by A3,A4,FUNCTOR0:31
.= Morph-Map(F,b1,c1).f1 by A4,A5,FUNCTOR0:def 15;
end;
theorem Th44:
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 be object;
assume
A2: [x,y] in ~f;
then x in dom ~f by XTUPLE_0:def 12;
then consider z2,z1 being object such that
A3: x = [z1,z2] and
A4: [z2,z1] in dom f by FUNCT_4:def 2;
y = (~f).(z1,z2) by A2,A3,FUNCT_1:1
.= f.(z2,z1) by A4,FUNCT_4:def 2;
then
A5: [[z2,z1],y] in f by A4,FUNCT_1:1;
then
A6: [z2,z1] in dom g by A1,FUNCT_1:1;
y = g.(z2,z1) by A1,A5,FUNCT_1:1;
then
A7: y = (~g).(z1,z2) by A6,FUNCT_4:def 2;
x in dom ~g by A3,A6,FUNCT_4:def 2;
hence thesis by A3,A7,FUNCT_1:1;
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:7;
then
A1: ~~f = f by FUNCT_4:52;
assume ~f c= ~g;
then ~~g c= g & f c= ~~g by A1,Th44,FUNCT_4:51;
hence thesis;
end;
theorem Th46:
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 object such that
A3: x1 in I & x2 in I and
A4: x = [x1,x2] by ZFMISC_1:def 2;
A5: [x2,x1] in [:I,I:] by A3,ZFMISC_1:def 2;
dom A = [:I,I:] by PARTFUN1:def 2;
then
A6: ~A.(x1,x2) = A.(x2,x1) by A5,FUNCT_4:def 2;
dom B = [:J,J:] by PARTFUN1:def 2;
then ~B.(x1,x2) = B.(x2,x1) by A1,A5,FUNCT_4:def 2;
hence thesis by A2,A4,A5,A6;
end;
theorem Th47:
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: B, B opp are_opposite by YELLOW18:def 4;
then
A2: the carrier of B opp = the carrier of B by YELLOW18:def 3;
A3: the Arrows of B opp = ~the Arrows of B by A1,YELLOW18:def 3;
A4: A, A opp are_opposite by YELLOW18:def 4;
then
A5: the carrier of A opp = the carrier of A by YELLOW18:def 3;
hence the carrier of B opp c= the carrier of A opp by A2,ALTCAT_2:def 11;
the Arrows of B cc= the Arrows of A & the Arrows of A opp = ~the Arrows
of A by A4,ALTCAT_2:def 11,YELLOW18:def 3;
hence the Arrows of B opp cc= the Arrows of A opp by A3,Th46;
A6: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
hence
[: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 A5,A2
,MCART_1:73;
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 object such that
A7: x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier
of B and
A8: x = [x1,x2,x3] by A2,MCART_1:68;
reconsider a = x1, b = x2, c = x3 as Object of B by A7;
reconsider a1 = a, b1 = b, c1 = c as Object of A by A6;
reconsider a19 = a1, b19 = b1, c19 = c1 as Object of A opp by A4,
YELLOW18:def 3;
A9: the Comp of B cc= the Comp of A & (the Comp of B).(c,b,a) = (the Comp
of B). [c,b,a] by ALTCAT_2:def 11,MULTOP_1:def 1;
A10: (the Comp of A).(c1,b1,a1) = (the Comp of A).[c1,b1,a1] by MULTOP_1:def 1;
[x3,x2,x1] in [:the carrier of B, the carrier of B, the carrier of B:]
by A7,MCART_1:69;
then
A11: (the Comp of B).(c,b,a) c= (the Comp of A).(c1,b1,a1) by A9,A10;
reconsider a9 = a, b9 = b, c9 = c as Object of B opp by A1,YELLOW18:def 3;
A12: (the Comp of B opp).(a9,b9,c9) = (the Comp of B opp).x & (the Comp of A
opp) .(a19,b19,c19) = (the Comp of A opp).x by A8,MULTOP_1:def 1;
A13: (the Comp of A opp).(a19,b19,c19) = ~((the Comp of A).(c1,b1,a1)) by A4,
YELLOW18:def 3;
(the Comp of B opp).(a9,b9,c9) = ~((the Comp of B).(c,b,a)) by A1,
YELLOW18:def 3;
hence thesis by A13,A12,A11,Th44;
end;
theorem Th48:
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 Th47;
A1: A opp, A are_opposite by YELLOW18:def 4;
A2: BB, B are_opposite by YELLOW18:def 4;
BB is id-inheriting
proof
per cases;
case BB is non empty;
let o be Object of BB, o9 be Object of A opp;
reconsider a9 = o9 as Object of A by A1,YELLOW18:def 3;
reconsider a = o as Object of B by A2,YELLOW18:def 3;
assume o = o9;
then idm a9 in <^a,a^> by ALTCAT_2:def 14;
then idm o9 in <^a,a^> by A1,YELLOW18:10;
hence thesis by A2,YELLOW18:7;
end;
case BB is empty;
end;
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: B, B opp are_opposite by YELLOW18:def 4;
thus B is subcategory of A & B opp is subcategory of A opp by Th48;
take G = dualizing-func(B, B opp);
thus G is bijective;
A2: A, A opp are_opposite by YELLOW18:def 4;
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 A2,YELLOW18:def 5;
end;
let b,c be Object of B, b1,c1 be Object of A such that
A3: <^b,c^> <> {} and
A4: b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A5: f = f1;
A6: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A3,A4,ALTCAT_2:31;
then
A7: <^F.c1,F.b1^> <> {} by FUNCTOR0:def 19;
thus G.f = f by A1,A3,YELLOW18:def 5
.= F.f1 by A2,A5,A6,YELLOW18:def 5
.= Morph-Map(F,b1,c1).f1 by A6,A7,FUNCTOR0:def 16;
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;
F is surjective by A1;
then F is onto;
then
A2: F is coreflexive by FUNCTOR0:46;
ex H being Functor of A2,A1 st H = F" & H is bijective covariant by A1,
FUNCTOR0:48;
then reconsider F9 = F" as covariant Functor of A2,A1;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2 such that
B1 is subcategory of A1 and
B2 is subcategory of A2;
given G being covariant Functor of B1,B2 such that
A3: G is bijective and
A4: for a being Object of B1, a1 being Object of A1 st a = a1 holds G.a
= F.a1 and
A5: 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;
G is surjective by A3;
then G is onto;
then
A6: G is coreflexive by FUNCTOR0:46;
thus B2 is subcategory of A2 & B1 is subcategory of A1;
consider H being Functor of B2,B1 such that
A7: H = G" and
A8: H is bijective covariant by A3,FUNCTOR0:48;
reconsider H as covariant Functor of B2,B1 by A8;
take H;
thus H is bijective by A8;
A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;
thus
A10: now
let a be Object of B2, a1 be Object of A2;
reconsider Ha = H.a as Object of A1 by A9;
G.(H.a) = F.Ha by A4;
then
A11: F.Ha = a by A3,A7,A6,Th1;
assume a = a1;
hence H.a = F".a1 by A1,A2,A11,Th1;
end;
let b,c be Object of B2, b1,c1 be Object of A2 such that
A12: <^b,c^> <> {} and
A13: b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A14: f = f1;
A15: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A12,A13,ALTCAT_2:31;
A16: G.(H.b) = b & G.(H.c) = c by A3,A7,A6,Th1;
A17: <^H.b, H.c^> <> {} by A12,FUNCTOR0:def 18;
then
A18: H.f in <^H.b, H.c^>;
A19: F.(F".b1) = b1 & F.(F".c1) = c1 by A1,A2,Th1;
A20: H.b = F".b1 & H.c = F".c1 by A10,A13;
then
A21: <^H.b, H.c^> c= <^F".b1, F".c1^> by ALTCAT_2:31;
then reconsider Hf = H.f as Morphism of F".b1, F".c1 by A18;
G.(H.f) = Morph-Map(F,F".b1, F".c1).Hf by A5,A20,A17
.= F.Hf by A21,A18,A15,A19,FUNCTOR0:def 15;
then F.Hf = f by A3,A7,A17,A16,Th2;
hence H.f = F9.f1 by A1,A14,A21,A18,A19,Th2
.= Morph-Map(F",b1,c1).f1 by A21,A18,A15,FUNCTOR0:def 15;
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;
F is surjective by A1;
then F is onto;
then
A2: F is coreflexive by FUNCTOR0:47;
ex H being Functor of A2,A1 st H = F" & H is bijective contravariant by A1,
FUNCTOR0:49;
then reconsider F9 = F" as contravariant Functor of A2,A1;
let B1 be non empty subcategory of A1;
let B2 be non empty subcategory of A2 such that
B1 is subcategory of A1 and
B2 is subcategory of A2;
given G being contravariant Functor of B1,B2 such that
A3: G is bijective and
A4: for a being Object of B1, a1 being Object of A1 st a = a1 holds G.a
= F.a1 and
A5: 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;
G is surjective by A3;
then G is onto;
then
A6: G is coreflexive by FUNCTOR0:47;
thus B2 is subcategory of A2 & B1 is subcategory of A1;
consider H being Functor of B2,B1 such that
A7: H = G" and
A8: H is bijective contravariant by A3,FUNCTOR0:49;
reconsider H as contravariant Functor of B2,B1 by A8;
take H;
thus H is bijective by A8;
A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;
thus
A10: now
let a be Object of B2, a1 be Object of A2;
reconsider Ha = H.a as Object of A1 by A9;
G.(H.a) = F.Ha by A4;
then
A11: F.Ha = a by A3,A7,A6,Th1;
assume a = a1;
hence H.a = F".a1 by A1,A2,A11,Th1;
end;
let b,c be Object of B2, b1,c1 be Object of A2 such that
A12: <^b,c^> <> {} and
A13: b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A14: f = f1;
A15: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A12,A13,ALTCAT_2:31;
A16: G.(H.b) = b & G.(H.c) = c by A3,A7,A6,Th1;
A17: <^H.c, H.b^> <> {} by A12,FUNCTOR0:def 19;
then
A18: H.f in <^H.c, H.b^>;
A19: F.(F".b1) = b1 & F.(F".c1) = c1 by A1,A2,Th1;
A20: H.b = F".b1 & H.c = F".c1 by A10,A13;
then
A21: <^H.c, H.b^> c= <^F".c1, F".b1^> by ALTCAT_2:31;
then reconsider Hf = H.f as Morphism of F".c1, F".b1 by A18;
G.(H.f) = Morph-Map(F,F".c1, F".b1).Hf by A5,A20,A17
.= F.Hf by A21,A18,A15,A19,FUNCTOR0:def 16;
then F.Hf = f by A3,A7,A17,A16,Th3;
hence H.f = F9.f1 by A1,A14,A21,A18,A19,Th3
.= Morph-Map(F",b1,c1).f1 by A21,A18,A15,FUNCTOR0:def 16;
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 that
B1 is subcategory of A1 and
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 that
B2 is subcategory of A2 and
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:12;
hereby
let a be Object of B1, b be Object of A1;
assume a = b;
then G1.(F1.a) = G.(F.b) by A2,A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:33
.= (G*F).b by FUNCTOR0:33;
end;
let b,c be Object of B1, b1,c1 be Object of A1 such that
A7: <^b,c^> <> {} and
A8: b = b1 & c = c1;
A9: (G*F).b1 = G.(F.b1) & (G*F).c1 = G.( F. c1) by FUNCTOR0:33;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A10: f in <^b,c^> & <^b,c^> c= <^b1,c1^> by A7,A8,ALTCAT_2:31;
then
A11: <^(G*F).b1, (G*F).c1^> <> {} by FUNCTOR0:def 18;
A12: <^F1.b, F1.c^> <> {} by A7,FUNCTOR0:def 18;
then
A13: F1.f in <^F1.b, F1.c^>;
A14: F1.b = F.b1 & F1.c = F.c1 by A2,A8;
then
A15: <^F1.b, F1.c^> c= <^F.b1, F.c1^> by ALTCAT_2:31;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7,A8
.= F.f1 by A10,A13,A15,FUNCTOR0:def 15;
then G1.(F1.f) = Morph-Map(G,F.b1,F.c1).(F.f1) by A6,A12,A14;
hence (G1*F1).f = Morph-Map(G,F.b1,F.c1).(F.f1) by A7,FUNCTOR3:6
.= G.(F.f1) by A13,A15,A11,A9,FUNCTOR0:def 15
.= (G*F).f1 by A10,FUNCTOR3:6
.= Morph-Map(G*F,b1,c1).f1 by A10,A11,FUNCTOR0:def 15;
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 that
B1 is subcategory of A1 and
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 that
B2 is subcategory of A2 and
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:12;
hereby
let a be Object of B1, b be Object of A1;
assume a = b;
then G1.(F1.a) = G.(F.b) by A2,A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:33
.= (G*F).b by FUNCTOR0:33;
end;
let b,c be Object of B1, b1,c1 be Object of A1 such that
A7: <^b,c^> <> {} and
A8: b = b1 & c = c1;
A9: (G*F).b1 = G.(F.b1) & (G*F).c1 = G.( F. c1) by FUNCTOR0:33;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A10: f in <^b,c^> & <^b,c^> c= <^b1,c1^> by A7,A8,ALTCAT_2:31;
then
A11: <^(G*F).c1, (G*F).b1^> <> {} by FUNCTOR0:def 19;
A12: <^F1.c, F1.b^> <> {} by A7,FUNCTOR0:def 19;
then
A13: F1.f in <^F1.c, F1.b^>;
A14: F1.b = F.b1 & F1.c = F.c1 by A2,A8;
then
A15: <^F1.c, F1.b^> c= <^F.c1, F.b1^> by ALTCAT_2:31;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7,A8
.= F.f1 by A10,A13,A15,FUNCTOR0:def 16;
then G1.(F1.f) = Morph-Map(G,F.c1,F.b1).(F.f1) by A6,A12,A14;
hence (G1*F1).f = Morph-Map(G,F.c1,F.b1).(F.f1) by A7,FUNCTOR3:9
.= G.(F.f1) by A13,A15,A11,A9,FUNCTOR0:def 15
.= (G*F).f1 by A10,FUNCTOR3:9
.= Morph-Map(G*F,b1,c1).f1 by A10,A11,FUNCTOR0:def 16;
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 that
B1 is subcategory of A1 and
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 that
B2 is subcategory of A2 and
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:12;
hereby
let a be Object of B1, b be Object of A1;
assume a = b;
then G1.(F1.a) = G.(F.b) by A2,A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:33
.= (G*F).b by FUNCTOR0:33;
end;
let b,c be Object of B1, b1,c1 be Object of A1 such that
A7: <^b,c^> <> {} and
A8: b = b1 & c = c1;
A9: (G*F).b1 = G.(F.b1) & (G*F).c1 = G.( F. c1) by FUNCTOR0:33;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A10: f in <^b,c^> & <^b,c^> c= <^b1,c1^> by A7,A8,ALTCAT_2:31;
then
A11: <^(G*F).c1, (G*F).b1^> <> {} by FUNCTOR0:def 19;
A12: <^F1.b, F1.c^> <> {} by A7,FUNCTOR0:def 18;
then
A13: F1.f in <^F1.b, F1.c^>;
A14: F1.b = F.b1 & F1.c = F.c1 by A2,A8;
then
A15: <^F1.b, F1.c^> c= <^F.b1, F.c1^> by ALTCAT_2:31;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7,A8
.= F.f1 by A10,A13,A15,FUNCTOR0:def 15;
then G1.(F1.f) = Morph-Map(G,F.b1,F.c1).(F.f1) by A6,A12,A14;
hence (G1*F1).f = Morph-Map(G,F.b1,F.c1).(F.f1) by A7,FUNCTOR3:8
.= G.(F.f1) by A13,A15,A11,A9,FUNCTOR0:def 16
.= (G*F).f1 by A10,FUNCTOR3:8
.= Morph-Map(G*F,b1,c1).f1 by A10,A11,FUNCTOR0:def 16;
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 that
B1 is subcategory of A1 and
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 that
B2 is subcategory of A2 and
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:12;
hereby
let a be Object of B1, b be Object of A1;
assume a = b;
then G1.(F1.a) = G.(F.b) by A2,A5;
hence (G1*F1).a = G.(F.b) by FUNCTOR0:33
.= (G*F).b by FUNCTOR0:33;
end;
let b,c be Object of B1, b1,c1 be Object of A1 such that
A7: <^b,c^> <> {} and
A8: b = b1 & c = c1;
A9: (G*F).b1 = G.(F.b1) & (G*F).c1 = G.( F. c1) by FUNCTOR0:33;
let f be Morphism of b,c, f1 be Morphism of b1,c1;
A10: f in <^b,c^> & <^b,c^> c= <^b1,c1^> by A7,A8,ALTCAT_2:31;
then
A11: <^(G*F).b1, (G*F).c1^> <> {} by FUNCTOR0:def 18;
A12: <^F1.c, F1.b^> <> {} by A7,FUNCTOR0:def 19;
then
A13: F1.f in <^F1.c, F1.b^>;
A14: F1.b = F.b1 & F1.c = F.c1 by A2,A8;
then
A15: <^F1.c, F1.b^> c= <^F.c1, F.b1^> by ALTCAT_2:31;
assume f = f1;
then F1.f = Morph-Map(F,b1,c1).f1 by A3,A7,A8
.= F.f1 by A10,A13,A15,FUNCTOR0:def 16;
then G1.(F1.f) = Morph-Map(G,F.c1,F.b1).(F.f1) by A6,A12,A14;
hence (G1*F1).f = Morph-Map(G,F.c1,F.b1).(F.f1) by A7,FUNCTOR3:7
.= G.(F.f1) by A13,A15,A11,A9,FUNCTOR0:def 16
.= (G*F).f1 by A10,FUNCTOR3:7
.= Morph-Map(G*F,b1,c1).f1 by A10,A11,FUNCTOR0:def 15;
end;
theorem
for A1, A2 be non empty category, F be covariant Functor of A1, A2,
B1 be non empty subcategory of A1, B2 be non empty subcategory of A2 st
F is bijective &
(for a being Object of A1 holds a is Object of B1 iff F.a is Object of B2) &
(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^>)
holds B1, B2 are_isomorphic_under F
proof
let A1, A2 be non empty category, F be covariant Functor of A1, A2,
B1 be non empty subcategory of A1, B2 be non empty subcategory of A2;
assume that
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^>;
thus B1, B2 are_isomorphic_under F
proof
deffunc F(Object of B1,Object of B1,Morphism of $1,$2) = (F|B1).$3;
deffunc O(Object of B1) = (F|B1).$1;
A4: F is injective surjective by A1;
A5: 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
A6: the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;
let a,b be Object of B2 such that
A7: <^a,b^> <> {};
reconsider a1 = a, b1 = b as Object of A2 by A6;
let f be Morphism of a,b;
A8: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A7,ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1;
consider c1, d1 being Object of A1, g1 being Morphism of c1,d1 such that
A9: a1 = F.c1 & b1 = F.d1 and
A10: <^c1,d1^> <> {} and
A11: f1 = F.g1 by A4,A8,Th33;
reconsider c = c1, d = d1 as Object of B1 by A2,A9;
reconsider g = g1 as Morphism of c,d by A3,A7,A9,A10,A11;
take c,d,g;
g1 in <^c,d^> by A3,A7,A9,A10,A11;
hence thesis by A9,A11,Th28,Th29;
end;
A12: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;
A13: now
let a be Object of B1;
reconsider b = a as Object of A1 by A12;
(F|B1).a = F.b by Th28;
hence O(a) is Object of B2 by A2;
end;
A14: now
let a,b be Object of B1 such that
A15: <^a,b^> <> {};
let f be Morphism of a,b;
reconsider c = a, d = b as Object of A1 by A12;
A16: <^a,b^> c= <^c,d^> & f in <^a,b^> by A15,ALTCAT_2:31;
then reconsider g = f as Morphism of c,d;
reconsider a9 = (F|B1).a, b9 = (F|B1).b as Object of B2 by A13;
A17: (F|B1).a = F.c & (F|B1).b = F.d by Th28;
(F|B1).f = F.g by A15,Th29;
then (F|B1).f in <^a9,b9^> by A3,A16,A17;
hence F(a,b,f) in (the Arrows of B2).(O(a), O(b));
end;
thus B1 is subcategory of A1 & B2 is subcategory of A2;
A18: F is one-to-one faithful surjective by A4;
A19: now
let a,b be Object of B1 such that
A20: <^a,b^> <> {};
reconsider a1 = a, b1 = b as Object of A1 by A12;
let f,g be Morphism of a,b;
A21: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A20,ALTCAT_2:31;
reconsider f1 = f, g1 = g as Morphism of a1,b1 by A21;
assume F(a,b,f) = F(a,b,g);
then F.f1 = (F|B1).g by A20,Th29
.= F.g1 by A20,Th29;
hence f = g by A18,A21,Th32;
end;
A22: now
let a,b,c be Object of B1 such that
A23: <^a,b^> <> {} and
A24: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;
let a9,b9,c9 be Object of B2 such that
A25: a9 = O(a) and
A26: b9 = O(b) and
A27: c9 = O(c);
let f9 be Morphism of a9,b9, g9 be Morphism of b9,c9 such that
A28: f9 = F(a,b,f) and
A29: g9 = F(b,c,g);
A30: b9 = F.b1 by A26,Th28;
A31: <^b,c^> c= <^b1,c1^> & g in <^b,c^> by A24,ALTCAT_2:31;
then reconsider g1 = g as Morphism of b1,c1;
A32: c9 = F.c1 by A27,Th28;
A33: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A23,ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1;
A34: a9 = F.a1 by A25,Th28;
A35: g9 = F.g1 by A24,A29,Th29;
then
A36: g9 in <^b9,c9^> by A3,A31,A30,A32;
A37: f9 = F.f1 by A23,A28,Th29;
then
A38: f9 in <^a9,b9^> by A3,A33,A34,A30;
<^a,c^> <> {} & g*f = g1*f1 by A23,A24,ALTCAT_1:def 2,ALTCAT_2:32;
then (F|B1).(g*f) = F.(g1*f1) by Th29;
hence F(a,c,g*f) = (F.g1)*(F.f1) by A33,A31,FUNCTOR0:def 23
.= g9*f9 by A34,A30,A32,A37,A35,A38,A36,ALTCAT_2:32;
end;
A39: now
let a be Object of B1, a9 be Object of B2 such that
A40: a9 = O(a);
reconsider a1 = a as Object of A1 by A12;
thus F(a,a,idm a) = F.idm a1 by Th29,ALTCAT_2:34
.= idm (F.a1) by FUNCTOR2:1
.= idm a9 by A40,Th28,ALTCAT_2:34;
end;
consider G being covariant strict Functor of B1,B2 such that
A41: for a being Object of B1 holds G.a = O(a) and
A42: 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 YELLOW18:sch 8(A13,A14,A22,A39);
take G;
A43: now
let a,b be Object of B1;
reconsider a1 = a, b1 = b as Object of A1 by A12;
assume O(a) = O(b);
then F.a1 = (F|B1).b by Th28
.= F.b1 by Th28;
hence a = b by A18,Th31;
end;
thus G is bijective from YELLOW18:sch 10(A41,A42,A43,A19,A5);
hereby
let a be Object of B1, a1 be Object of A1 such that
A44: a = a1;
thus G.a = (F|B1).a by A41
.= F.a1 by A44,Th28;
end;
let b,c be Object of B1, b1,c1 be Object of A1 such that
A45: <^b,c^> <> {} and
A46: b1 = b & c1 = c;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A47: f = f1;
A48: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A45,A46,ALTCAT_2:31;
then
A49: <^F.b1, F.c1^> <> {} by FUNCTOR0:def 18;
thus G.f = (F|B1).f by A42,A45
.= F.f1 by A45,A46,A47,Th29
.= Morph-Map(F,b1,c1).f1 by A48,A49,FUNCTOR0:def 15;
end;
end;
theorem
for A1, A2 be non empty category, F be contravariant Functor of A1,A2,
B1 be non empty subcategory of A1, B2 be non empty subcategory of A2 st
F is bijective &
(for a being Object of A1 holds a is Object of B1 iff
F.a is Object of B2) &
(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^>)
holds B1, B2 are_anti-isomorphic_under F
proof let A1, A2 be non empty category, F be contravariant Functor of A1,A2,
B1 be non empty subcategory of A1, B2 be non empty subcategory of A2;
assume that
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^>;
thus B1, B2 are_anti-isomorphic_under F
proof
deffunc F(Object of B1,Object of B1,Morphism of $1,$2) = (F|B1).$3;
deffunc O(Object of B1) = (F|B1).$1;
A4: F is injective surjective by A1;
A5: 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
A6: the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;
let a,b be Object of B2 such that
A7: <^a,b^> <> {};
reconsider a1 = a, b1 = b as Object of A2 by A6;
let f be Morphism of a,b;
A8: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A7,ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1;
consider c1, d1 being Object of A1, g1 being Morphism of c1,d1 such that
A9: b1 = F.c1 & a1 = F.d1 and
A10: <^c1,d1^> <> {} and
A11: f1 = F.g1 by A4,A8,Th36;
reconsider c = c1, d = d1 as Object of B1 by A2,A9;
reconsider g = g1 as Morphism of c,d by A3,A7,A9,A10,A11;
take c,d,g;
g1 in <^c,d^> by A3,A7,A9,A10,A11;
hence thesis by A9,A11,Th28,Th30;
end;
A12: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;
A13: now
let a be Object of B1;
reconsider b = a as Object of A1 by A12;
(F|B1).a = F.b by Th28;
hence O(a) is Object of B2 by A2;
end;
A14: now
let a,b be Object of B1 such that
A15: <^a,b^> <> {};
let f be Morphism of a,b;
reconsider c = a, d = b as Object of A1 by A12;
A16: <^a,b^> c= <^c,d^> & f in <^a,b^> by A15,ALTCAT_2:31;
then reconsider g = f as Morphism of c,d;
reconsider a9 = (F|B1).a, b9 = (F|B1).b as Object of B2 by A13;
A17: (F|B1).a = F.c & (F|B1).b = F.d by Th28;
(F|B1).f = F.g by A15,Th30;
then (F|B1).f in <^b9,a9^> by A3,A16,A17;
hence F(a,b,f) in (the Arrows of B2).(O(b), O(a));
end;
thus B1 is subcategory of A1 & B2 is subcategory of A2;
A18: F is one-to-one faithful surjective by A4;
A19: now
let a,b be Object of B1 such that
A20: <^a,b^> <> {};
reconsider a1 = a, b1 = b as Object of A1 by A12;
let f,g be Morphism of a,b;
A21: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A20,ALTCAT_2:31;
reconsider f1 = f, g1 = g as Morphism of a1,b1 by A21;
assume F(a,b,f) = F(a,b,g);
then F.f1 = (F|B1).g by A20,Th30
.= F.g1 by A20,Th30;
hence f = g by A18,A21,Th35;
end;
A22: now
let a,b,c be Object of B1 such that
A23: <^a,b^> <> {} and
A24: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;
let a9,b9,c9 be Object of B2 such that
A25: a9 = O(a) and
A26: b9 = O(b) and
A27: c9 = O(c);
let f9 be Morphism of b9,a9, g9 be Morphism of c9,b9 such that
A28: f9 = F(a,b,f) and
A29: g9 = F(b,c,g);
A30: b9 = F.b1 by A26,Th28;
A31: <^b,c^> c= <^b1,c1^> & g in <^b,c^> by A24,ALTCAT_2:31;
then reconsider g1 = g as Morphism of b1,c1;
A32: c9 = F.c1 by A27,Th28;
A33: <^a,b^> c= <^a1,b1^> & f in <^a,b^> by A23,ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1;
A34: a9 = F.a1 by A25,Th28;
A35: g9 = F.g1 by A24,A29,Th30;
then
A36: g9 in <^c9,b9^> by A3,A31,A30,A32;
A37: f9 = F.f1 by A23,A28,Th30;
then
A38: f9 in <^b9,a9^> by A3,A33,A34,A30;
<^a,c^> <> {} & g*f = g1*f1 by A23,A24,ALTCAT_1:def 2,ALTCAT_2:32;
then (F|B1).(g*f) = F.(g1*f1) by Th30;
hence F(a,c,g*f) = (F.f1)*(F.g1) by A33,A31,FUNCTOR0:def 24
.= f9*g9 by A34,A30,A32,A37,A35,A38,A36,ALTCAT_2:32;
end;
A39: now
let a be Object of B1, a9 be Object of B2 such that
A40: a9 = O(a);
reconsider a1 = a as Object of A1 by A12;
thus F(a,a,idm a) = F.idm a1 by Th30,ALTCAT_2:34
.= idm (F.a1) by ALTCAT_4:13
.= idm a9 by A40,Th28,ALTCAT_2:34;
end;
consider G being contravariant strict Functor of B1,B2 such that
A41: for a being Object of B1 holds G.a = O(a) and
A42: 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 YELLOW18:sch 9(A13,A14,A22,A39);
take G;
A43: now
let a,b be Object of B1;
reconsider a1 = a, b1 = b as Object of A1 by A12;
assume O(a) = O(b);
then F.a1 = (F|B1).b by Th28
.= F.b1 by Th28;
hence a = b by A18,Th34;
end;
thus G is bijective from YELLOW18:sch 12(A41,A42,A43,A19,A5);
hereby
let a be Object of B1, a1 be Object of A1 such that
A44: a = a1;
thus G.a = (F|B1).a by A41
.= F.a1 by A44,Th28;
end;
let b,c be Object of B1, b1,c1 be Object of A1;
assume that
A45: <^b,c^> <> {} and
A46: b = b1 & c = c1;
let f be Morphism of b,c, f1 be Morphism of b1,c1 such that
A47: f = f1;
A48: <^b,c^> c= <^b1,c1^> & f in <^b,c^> by A45,A46,ALTCAT_2:31;
then
A49: <^F.c1, F.b1^> <> {} by FUNCTOR0:def 19;
thus G.f = (F|B1).f by A42,A45
.= F.f1 by A45,A46,A47,Th30
.= Morph-Map(F,b1,c1).f1 by A48,A49,FUNCTOR0:def 16;
end;
end;