Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek
- Received July 31, 2001
- MML identifier: YELLOW20
- [
Mizar article,
MML identifier index
]
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;
begin :: Reverse functors
reserve x,y for set;
theorem :: YELLOW20:1
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;
theorem :: YELLOW20:2
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;
theorem :: YELLOW20:3
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;
theorem :: YELLOW20:4
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";
theorem :: YELLOW20:5
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";
theorem :: YELLOW20:6
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";
theorem :: YELLOW20:7
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";
theorem :: YELLOW20:8
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";
theorem :: YELLOW20:9
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";
begin :: Intersection of categories
definition
let A, B be AltCatStr;
pred A, B have_the_same_composition means
:: YELLOW20:def 1
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 :: YELLOW20:10
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;
theorem :: YELLOW20:11
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;
theorem :: YELLOW20:12
for A, B being para-functional semi-functional category holds
A, B have_the_same_composition;
definition
let f, g be Function;
func Intersect(f, g) -> Function means
:: YELLOW20:def 2
dom it = (dom f) /\ (dom g) &
for x being set st x in (dom f) /\ (dom g) holds it.x = (f.x) /\ (g.x);
commutativity;
end;
theorem :: YELLOW20:13
for I being set, A,B being ManySortedSet of I
holds Intersect(A, B) = A /\ B;
theorem :: YELLOW20:14
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;
theorem :: YELLOW20:15
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;
theorem :: YELLOW20:16
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;
theorem :: YELLOW20:17
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;
theorem :: YELLOW20:18
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|};
theorem :: YELLOW20:19
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|};
definition
let A, B be AltCatStr such that
A, B have_the_same_composition;
func Intersect(A, B) -> strict AltCatStr means
:: YELLOW20:def 3
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);
end;
theorem :: YELLOW20:20
for A, B being AltCatStr st A, B have_the_same_composition
holds Intersect(A, B) = Intersect(B, A);
theorem :: YELLOW20:21
for A, B being AltCatStr st A, B have_the_same_composition
holds Intersect(A, B) is SubCatStr of A;
theorem :: YELLOW20:22
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^>;
theorem :: YELLOW20:23
for A, B being transitive AltCatStr st A, B have_the_same_composition
holds Intersect(A, B) is transitive;
theorem :: YELLOW20:24
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^>;
theorem :: YELLOW20:25
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^>;
theorem :: YELLOW20:26
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;
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
for a being object of A() holds a is object of B1() iff P[a] and
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
for a being object of A() holds a is object of B2() iff P[a] and
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];
theorem :: YELLOW20:27
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^>;
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
ex a being object of A() st P[a];
scheme FullSubcategoryUniq
{ A() -> category,
B1, B2() -> full non empty subcategory of A(),
P[set]}:
the AltCatStr of B1() = the AltCatStr of B2()
provided
for a being object of A() holds a is object of B1() iff P[a] and
for a being object of A() holds a is object of B2() iff P[a];
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;
end;
theorem :: YELLOW20:28
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;
definition
let A be category;
let C be non empty subcategory of A;
cluster incl C -> id-preserving comp-preserving;
end;
definition
let A be category;
let C be non empty subcategory of A;
cluster incl C -> Covariant;
end;
definition
let A be category;
let C be non empty subcategory of A;
redefine func incl C -> strict covariant Functor of C,A;
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;
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;
end;
theorem :: YELLOW20:29
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;
theorem :: YELLOW20:30
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;
theorem :: YELLOW20:31
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;
theorem :: YELLOW20:32
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;
theorem :: YELLOW20:33
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;
theorem :: YELLOW20:34
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;
theorem :: YELLOW20:35
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;
theorem :: YELLOW20:36
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;
theorem :: YELLOW20:37
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;
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
:: YELLOW20:def 4
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
:: YELLOW20:def 5
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 :: YELLOW20:38
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 :: YELLOW20:39
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 :: YELLOW20:40
for A,B being category, F being covariant Functor of A,B
st A, B are_isomorphic_under F
holds F is bijective;
theorem :: YELLOW20:41
for A,B being category, F being contravariant Functor of A,B
st A, B are_anti-isomorphic_under F
holds F is bijective;
theorem :: YELLOW20:42
for A,B being category, F being covariant Functor of A,B
st F is bijective
holds A, B are_isomorphic_under F;
theorem :: YELLOW20:43
for A,B being category, F being contravariant Functor of A,B
st F is bijective
holds A, B are_anti-isomorphic_under F;
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
F() is bijective and
for a being object of A1() holds
a is object of B1() iff F().a is object of B2() and
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^>;
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
F() is bijective and
for a being object of A1() holds
a is object of B1() iff F().a is object of B2() and
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^>;
theorem :: YELLOW20:44
for A being category, B being non empty subcategory of A
holds B,B are_isomorphic_under id A;
theorem :: YELLOW20:45
for f, g being Function st f c= g holds ~f c= ~g;
theorem :: YELLOW20:46
for f, g being Function st dom f is Relation & ~f c= ~g holds f c= g;
theorem :: YELLOW20:47
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;
theorem :: YELLOW20:48
for A being transitive non empty AltCatStr
for B being transitive non empty SubCatStr of A
holds B opp is SubCatStr of A opp;
theorem :: YELLOW20:49
for A being category, B being non empty subcategory of A
holds B opp is subcategory of A opp;
theorem :: YELLOW20:50
for A being category, B being non empty subcategory of A
holds B,B opp are_anti-isomorphic_under dualizing-func(A, A opp);
theorem :: YELLOW20:51
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";
theorem :: YELLOW20:52
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";
theorem :: YELLOW20:53
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;
theorem :: YELLOW20:54
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;
theorem :: YELLOW20:55
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;
theorem :: YELLOW20:56
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;
Back to top