Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Miscellaneous Facts about Functors

**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