:: FUNCTOR3 semantic presentation
begin
registration
cluster non empty transitive strict associative with_units for AltCatStr ;
existence
ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict )
proof
set A = the non empty transitive strict associative with_units AltCatStr ;
take the non empty transitive strict associative with_units AltCatStr ; ::_thesis: ( the non empty transitive strict associative with_units AltCatStr is transitive & the non empty transitive strict associative with_units AltCatStr is associative & the non empty transitive strict associative with_units AltCatStr is with_units & the non empty transitive strict associative with_units AltCatStr is strict )
thus ( the non empty transitive strict associative with_units AltCatStr is transitive & the non empty transitive strict associative with_units AltCatStr is associative & the non empty transitive strict associative with_units AltCatStr is with_units & the non empty transitive strict associative with_units AltCatStr is strict ) ; ::_thesis: verum
end;
end;
registration
let A be non empty transitive AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict Covariant Contravariant comp-preserving comp-reversing for FunctorStr over A,B;
existence
ex b1 being FunctorStr over A,B st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible )
proof
set o = the object of B;
take A --> (idm the object of B) ; ::_thesis: ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible )
thus ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible ) ; ::_thesis: verum
end;
end;
registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict Covariant Contravariant id-preserving comp-preserving comp-reversing for FunctorStr over A,B;
existence
ex b1 being FunctorStr over A,B st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible & b1 is id-preserving )
proof
set o = the object of B;
take A --> (idm the object of B) ; ::_thesis: ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible & A --> (idm the object of B) is id-preserving )
thus ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible & A --> (idm the object of B) is id-preserving ) ; ::_thesis: verum
end;
end;
registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict id-preserving covariant contravariant for Functor of A,B;
existence
ex b1 being Functor of A,B st
( b1 is strict & b1 is feasible & b1 is covariant & b1 is contravariant )
proof
set o = the object of B;
set I = A --> (idm the object of B);
reconsider I = A --> (idm the object of B) as Functor of A,B by FUNCTOR0:def_25;
take I ; ::_thesis: ( I is strict & I is feasible & I is covariant & I is contravariant )
thus ( I is strict & I is feasible ) ; ::_thesis: ( I is covariant & I is contravariant )
thus I is covariant ; ::_thesis: I is contravariant
thus I is contravariant ; ::_thesis: verum
end;
end;
theorem :: FUNCTOR3:1
for C being category
for o1, o2, o3, o4 being object of C
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
proof
let C be category; ::_thesis: for o1, o2, o3, o4 being object of C
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
let o1, o2, o3, o4 be object of C; ::_thesis: for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
let a be Morphism of o1,o2; ::_thesis: for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
let b be Morphism of o2,o3; ::_thesis: for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
let c be Morphism of o1,o4; ::_thesis: for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
let d be Morphism of o4,o3; ::_thesis: ( b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} implies c * (a ") = (d ") * b )
assume that
A1: b * a = d * c and
A2: a * (a ") = idm o2 and
A3: (d ") * d = idm o4 and
A4: <^o1,o2^> <> {} and
A5: <^o2,o1^> <> {} and
A6: <^o2,o3^> <> {} and
A7: <^o3,o4^> <> {} and
A8: <^o4,o3^> <> {} ; ::_thesis: c * (a ") = (d ") * b
A9: <^o2,o4^> <> {} by A6, A7, ALTCAT_1:def_2;
<^o1,o3^> <> {} by A4, A6, ALTCAT_1:def_2;
then A10: <^o1,o4^> <> {} by A7, ALTCAT_1:def_2;
b = b * (idm o2) by A6, ALTCAT_1:def_17
.= (b * a) * (a ") by A2, A4, A5, A6, ALTCAT_1:21 ;
hence (d ") * b = (d ") * (d * (c * (a "))) by A1, A5, A8, A10, ALTCAT_1:21
.= ((d ") * d) * (c * (a ")) by A7, A8, A9, ALTCAT_1:21
.= c * (a ") by A3, A9, ALTCAT_1:20 ;
::_thesis: verum
end;
theorem :: FUNCTOR3:2
for A being non empty transitive AltCatStr
for B, C being non empty with_units AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
proof
let A be non empty transitive AltCatStr ; ::_thesis: for B, C being non empty with_units AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
let B, C be non empty with_units AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
let F be feasible Covariant FunctorStr over A,B; ::_thesis: for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
let G be FunctorStr over B,C; ::_thesis: for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
let o, o1 be object of A; ::_thesis: Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
( dom the MorphMap of G = [: the carrier of B, the carrier of B:] & rng the ObjectMap of F c= [: the carrier of B, the carrier of B:] ) by PARTFUN1:def_2;
then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:27
.= [: the carrier of A, the carrier of A:] by FUNCT_2:def_1 ;
then A1: [o,o1] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87;
then A2: ( the MorphMap of G * the ObjectMap of F) . [o,o1] = the MorphMap of G . ( the ObjectMap of F . (o,o1)) by FUNCT_1:12
.= Morph-Map (G,(F . o),(F . o1)) by FUNCTOR0:22 ;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [o,o1] in dom the MorphMap of F by ZFMISC_1:87;
then [o,o1] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A1, XBOOLE_0:def_4;
then A3: [o,o1] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def_19;
thus Morph-Map ((G * F),o,o1) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1) by FUNCTOR0:def_36
.= (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) by A3, A2, PBOOLE:def_19 ; ::_thesis: verum
end;
theorem :: FUNCTOR3:3
for A being non empty transitive AltCatStr
for B, C being non empty with_units AltCatStr
for F being feasible Contravariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
proof
let A be non empty transitive AltCatStr ; ::_thesis: for B, C being non empty with_units AltCatStr
for F being feasible Contravariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
let B, C be non empty with_units AltCatStr ; ::_thesis: for F being feasible Contravariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
let F be feasible Contravariant FunctorStr over A,B; ::_thesis: for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
let G be FunctorStr over B,C; ::_thesis: for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
let o, o1 be object of A; ::_thesis: Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
( dom the MorphMap of G = [: the carrier of B, the carrier of B:] & rng the ObjectMap of F c= [: the carrier of B, the carrier of B:] ) by PARTFUN1:def_2;
then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:27
.= [: the carrier of A, the carrier of A:] by FUNCT_2:def_1 ;
then A1: [o,o1] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87;
then A2: ( the MorphMap of G * the ObjectMap of F) . [o,o1] = the MorphMap of G . ( the ObjectMap of F . (o,o1)) by FUNCT_1:12
.= Morph-Map (G,(F . o1),(F . o)) by FUNCTOR0:23 ;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [o,o1] in dom the MorphMap of F by ZFMISC_1:87;
then [o,o1] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A1, XBOOLE_0:def_4;
then A3: [o,o1] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def_19;
thus Morph-Map ((G * F),o,o1) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1) by FUNCTOR0:def_36
.= (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) by A3, A2, PBOOLE:def_19 ; ::_thesis: verum
end;
Lm1: for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
proof
let I1 be set ; ::_thesis: for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let I2 be non empty set ; ::_thesis: for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let f be Function of I1,I2; ::_thesis: for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let A be ManySortedSet of I1; ::_thesis: for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let B be ManySortedSet of I2; ::_thesis: for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let M be ManySortedFunction of A,B * f; ::_thesis: ((id B) * f) ** M = M
A1: now__::_thesis:_for_i_being_set_st_i_in_I1_holds_
(_(B_*_f)_._i_=_B_._(f_._i)_&_((id_B)_*_f)_._i_=_id_((B_*_f)_._i)_)
let i be set ; ::_thesis: ( i in I1 implies ( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) ) )
assume A2: i in I1 ; ::_thesis: ( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) )
hence A3: (B * f) . i = B . (f . i) by FUNCT_2:15; ::_thesis: ((id B) * f) . i = id ((B * f) . i)
( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A2, FUNCT_2:5, FUNCT_2:15;
hence ((id B) * f) . i = id ((B * f) . i) by A3, MSUALG_3:def_1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_set_st_i_in_I1_holds_
(((id_B)_*_f)_**_M)_._i_=_M_._i
A4: (id B) * f is ManySortedFunction of B * f,B * f
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I1 or ((id B) * f) . i is M2( bool [:((B * f) . i),((B * f) . i):]) )
assume i in I1 ; ::_thesis: ((id B) * f) . i is M2( bool [:((B * f) . i),((B * f) . i):])
then ((id B) * f) . i = id ((B * f) . i) by A1;
hence ((id B) * f) . i is M2( bool [:((B * f) . i),((B * f) . i):]) ; ::_thesis: verum
end;
let i be set ; ::_thesis: ( i in I1 implies (((id B) * f) ** M) . i = M . i )
assume A5: i in I1 ; ::_thesis: (((id B) * f) ** M) . i = M . i
then A6: M . i is Function of (A . i),((B * f) . i) by PBOOLE:def_15;
( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A5, FUNCT_2:5, FUNCT_2:15;
then A7: ((id B) * f) . i = id (B . (f . i)) by MSUALG_3:def_1;
(B * f) . i = B . (f . i) by A1, A5;
hence (((id B) * f) ** M) . i = (id ((B * f) . i)) * (M . i) by A5, A4, A7, MSUALG_3:2
.= M . i by A6, FUNCT_2:17 ;
::_thesis: verum
end;
hence ((id B) * f) ** M = M by PBOOLE:3; ::_thesis: verum
end;
theorem :: FUNCTOR3:4
for A being non empty transitive AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
proof
let A be non empty transitive AltCatStr ; ::_thesis: for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let B be non empty with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let F be feasible FunctorStr over A,B; ::_thesis: (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
A1: the ObjectMap of ((id B) * F) = the ObjectMap of (id B) * the ObjectMap of F by FUNCTOR0:def_36
.= (id [: the carrier of B, the carrier of B:]) * the ObjectMap of F by FUNCTOR0:def_29
.= the ObjectMap of F by FUNCT_2:17 ;
A2: the MorphMap of F is ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by FUNCTOR0:def_4;
the MorphMap of ((id B) * F) = ( the MorphMap of (id B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def_36
.= ((id the Arrows of B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def_29
.= the MorphMap of F by A2, Lm1 ;
hence (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A1; ::_thesis: verum
end;
theorem :: FUNCTOR3:5
for A being non empty transitive with_units AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
proof
let A be non empty transitive with_units AltCatStr ; ::_thesis: for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let B be non empty with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let F be feasible FunctorStr over A,B; ::_thesis: F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
A1: the ObjectMap of (F * (id A)) = the ObjectMap of F * the ObjectMap of (id A) by FUNCTOR0:def_36
.= the ObjectMap of F * (id [: the carrier of A, the carrier of A:]) by FUNCTOR0:def_29
.= the ObjectMap of F by FUNCT_2:17 ;
A2: the MorphMap of F is ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by FUNCTOR0:def_4;
the MorphMap of (F * (id A)) = ( the MorphMap of F * the ObjectMap of (id A)) ** the MorphMap of (id A) by FUNCTOR0:def_36
.= ( the MorphMap of F * (id [: the carrier of A, the carrier of A:])) ** the MorphMap of (id A) by FUNCTOR0:def_29
.= the MorphMap of F ** the MorphMap of (id A) by FUNCTOR0:2
.= the MorphMap of F ** (id the Arrows of A) by FUNCTOR0:def_29
.= the MorphMap of F by A2, MSUALG_3:3 ;
hence F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A1; ::_thesis: verum
end;
theorem Th6: :: FUNCTOR3:6
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
proof
let A be non empty AltCatStr ; ::_thesis: for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let B, C be non empty reflexive AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let F be feasible Covariant FunctorStr over A,B; ::_thesis: for G being feasible Covariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let G be feasible Covariant FunctorStr over B,C; ::_thesis: for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (G * F) . m = G . (F . m) )
set I = the carrier of A;
reconsider s = the MorphMap of F . (o1,o2) as Function ;
reconsider r = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o1,o2) as Function ;
reconsider t = ( the MorphMap of G * the ObjectMap of F) . (o1,o2) as Function ;
A1: dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) = (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def_19
.= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] ;
A2: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1;
A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
assume A4: <^o1,o2^> <> {} ; ::_thesis: (G * F) . m = G . (F . m)
then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def_18;
then A6: dom (Morph-Map (F,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1;
A7: <^(G . (F . o1)),(G . (F . o2))^> <> {} by A5, FUNCTOR0:def_18;
( (G * F) . o1 = G . (F . o1) & (G * F) . o2 = G . (F . o2) ) by FUNCTOR0:33;
hence (G * F) . m = (Morph-Map ((G * F),o1,o2)) . m by A4, A7, FUNCTOR0:def_15
.= r . m by FUNCTOR0:def_36
.= (t * s) . m by A1, A3, PBOOLE:def_19
.= t . ((Morph-Map (F,o1,o2)) . m) by A4, A6, FUNCT_1:13
.= t . (F . m) by A4, A5, FUNCTOR0:def_15
.= ( the MorphMap of G . ( the ObjectMap of F . (o1,o2))) . (F . m) by A2, A3, FUNCT_1:13
.= (Morph-Map (G,(F . o1),(F . o2))) . (F . m) by FUNCTOR0:22
.= G . (F . m) by A5, A7, FUNCTOR0:def_15 ;
::_thesis: verum
end;
theorem Th7: :: FUNCTOR3:7
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for M being feasible Contravariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
proof
let A be non empty AltCatStr ; ::_thesis: for B, C being non empty reflexive AltCatStr
for M being feasible Contravariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
let B, C be non empty reflexive AltCatStr ; ::_thesis: for M being feasible Contravariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
let M be feasible Contravariant FunctorStr over A,B; ::_thesis: for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
let N be feasible Contravariant FunctorStr over B,C; ::_thesis: for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (N * M) . m = N . (M . m) )
set I = the carrier of A;
reconsider s = the MorphMap of M . (o1,o2) as Function ;
reconsider r = (( the MorphMap of N * the ObjectMap of M) ** the MorphMap of M) . (o1,o2) as Function ;
reconsider t = ( the MorphMap of N * the ObjectMap of M) . (o1,o2) as Function ;
A1: dom (( the MorphMap of N * the ObjectMap of M) ** the MorphMap of M) = (dom ( the MorphMap of N * the ObjectMap of M)) /\ (dom the MorphMap of M) by PBOOLE:def_19
.= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of M) by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] ;
A2: dom the ObjectMap of M = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1;
A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
assume A4: <^o1,o2^> <> {} ; ::_thesis: (N * M) . m = N . (M . m)
then A5: <^(M . o2),(M . o1)^> <> {} by FUNCTOR0:def_19;
then A6: dom (Morph-Map (M,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1;
A7: <^(N . (M . o1)),(N . (M . o2))^> <> {} by A5, FUNCTOR0:def_19;
( (N * M) . o1 = N . (M . o1) & (N * M) . o2 = N . (M . o2) ) by FUNCTOR0:33;
hence (N * M) . m = (Morph-Map ((N * M),o1,o2)) . m by A4, A7, FUNCTOR0:def_15
.= r . m by FUNCTOR0:def_36
.= (t * s) . m by A1, A3, PBOOLE:def_19
.= t . ((Morph-Map (M,o1,o2)) . m) by A4, A6, FUNCT_1:13
.= t . (M . m) by A4, A5, FUNCTOR0:def_16
.= ( the MorphMap of N . ( the ObjectMap of M . (o1,o2))) . (M . m) by A2, A3, FUNCT_1:13
.= (Morph-Map (N,(M . o2),(M . o1))) . (M . m) by FUNCTOR0:23
.= N . (M . m) by A5, A7, FUNCTOR0:def_16 ;
::_thesis: verum
end;
theorem Th8: :: FUNCTOR3:8
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
proof
let A be non empty AltCatStr ; ::_thesis: for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
let B, C be non empty reflexive AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
let F be feasible Covariant FunctorStr over A,B; ::_thesis: for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
let N be feasible Contravariant FunctorStr over B,C; ::_thesis: for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (N * F) . m = N . (F . m) )
set I = the carrier of A;
reconsider s = the MorphMap of F . (o1,o2) as Function ;
reconsider r = (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) . (o1,o2) as Function ;
reconsider t = ( the MorphMap of N * the ObjectMap of F) . (o1,o2) as Function ;
A1: dom (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) = (dom ( the MorphMap of N * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def_19
.= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] ;
A2: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1;
A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
assume A4: <^o1,o2^> <> {} ; ::_thesis: (N * F) . m = N . (F . m)
then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def_18;
then A6: dom (Morph-Map (F,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1;
A7: <^(N . (F . o2)),(N . (F . o1))^> <> {} by A5, FUNCTOR0:def_19;
( (N * F) . o1 = N . (F . o1) & (N * F) . o2 = N . (F . o2) ) by FUNCTOR0:33;
hence (N * F) . m = (Morph-Map ((N * F),o1,o2)) . m by A4, A7, FUNCTOR0:def_16
.= r . m by FUNCTOR0:def_36
.= (t * s) . m by A1, A3, PBOOLE:def_19
.= t . ((Morph-Map (F,o1,o2)) . m) by A4, A6, FUNCT_1:13
.= t . (F . m) by A4, A5, FUNCTOR0:def_15
.= ( the MorphMap of N . ( the ObjectMap of F . (o1,o2))) . (F . m) by A2, A3, FUNCT_1:13
.= (Morph-Map (N,(F . o1),(F . o2))) . (F . m) by FUNCTOR0:22
.= N . (F . m) by A5, A7, FUNCTOR0:def_16 ;
::_thesis: verum
end;
theorem Th9: :: FUNCTOR3:9
for A being non empty AltCatStr
for C, B being non empty reflexive AltCatStr
for G being feasible Covariant FunctorStr over B,C
for M being feasible Contravariant FunctorStr over A,B
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
proof
let A be non empty AltCatStr ; ::_thesis: for C, B being non empty reflexive AltCatStr
for G being feasible Covariant FunctorStr over B,C
for M being feasible Contravariant FunctorStr over A,B
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
let C, B be non empty reflexive AltCatStr ; ::_thesis: for G being feasible Covariant FunctorStr over B,C
for M being feasible Contravariant FunctorStr over A,B
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
let G be feasible Covariant FunctorStr over B,C; ::_thesis: for M being feasible Contravariant FunctorStr over A,B
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
let M be feasible Contravariant FunctorStr over A,B; ::_thesis: for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (G * M) . m = G . (M . m) )
set I = the carrier of A;
reconsider s = the MorphMap of M . (o1,o2) as Function ;
reconsider r = (( the MorphMap of G * the ObjectMap of M) ** the MorphMap of M) . (o1,o2) as Function ;
reconsider t = ( the MorphMap of G * the ObjectMap of M) . (o1,o2) as Function ;
A1: dom (( the MorphMap of G * the ObjectMap of M) ** the MorphMap of M) = (dom ( the MorphMap of G * the ObjectMap of M)) /\ (dom the MorphMap of M) by PBOOLE:def_19
.= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of M) by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2
.= [: the carrier of A, the carrier of A:] ;
A2: dom the ObjectMap of M = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1;
A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
assume A4: <^o1,o2^> <> {} ; ::_thesis: (G * M) . m = G . (M . m)
then A5: <^(M . o2),(M . o1)^> <> {} by FUNCTOR0:def_19;
then A6: dom (Morph-Map (M,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1;
A7: <^(G . (M . o2)),(G . (M . o1))^> <> {} by A5, FUNCTOR0:def_18;
( (G * M) . o1 = G . (M . o1) & (G * M) . o2 = G . (M . o2) ) by FUNCTOR0:33;
hence (G * M) . m = (Morph-Map ((G * M),o1,o2)) . m by A4, A7, FUNCTOR0:def_16
.= r . m by FUNCTOR0:def_36
.= (t * s) . m by A1, A3, PBOOLE:def_19
.= t . ((Morph-Map (M,o1,o2)) . m) by A4, A6, FUNCT_1:13
.= t . (M . m) by A4, A5, FUNCTOR0:def_16
.= ( the MorphMap of G . ( the ObjectMap of M . (o1,o2))) . (M . m) by A2, A3, FUNCT_1:13
.= (Morph-Map (G,(M . o2),(M . o1))) . (M . m) by FUNCTOR0:23
.= G . (M . m) by A5, A7, FUNCTOR0:def_15 ;
::_thesis: verum
end;
registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Covariant comp-preserving FunctorStr over A,B;
let G be feasible Covariant comp-preserving FunctorStr over B,C;
clusterG * F -> comp-preserving ;
coherence
G * F is comp-preserving
proof
let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1)
A3: ( <^(F . o1),(F . o2)^> <> {} & <^(F . o2),(F . o3)^> <> {} ) by A1, A2, FUNCTOR0:def_18;
let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . b1) * ((G * F) . f)
let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . g) * ((G * F) . f)
A4: ( (G * F) . o1 = G . (F . o1) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33;
A5: (G * F) . o2 = G . (F . o2) by FUNCTOR0:33;
then reconsider GFg = (G * F) . g as Morphism of (G . (F . o2)),(G . (F . o3)) by FUNCTOR0:33;
<^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2;
hence (G * F) . (g * f) = G . (F . (g * f)) by Th6
.= G . ((F . g) * (F . f)) by A1, A2, FUNCTOR0:def_23
.= (G . (F . g)) * (G . (F . f)) by A3, FUNCTOR0:def_23
.= GFg * (G . (F . f)) by A2, Th6
.= ((G * F) . g) * ((G * F) . f) by A1, A5, A4, Th6 ;
::_thesis: verum
end;
end;
registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Contravariant comp-reversing FunctorStr over A,B;
let G be feasible Contravariant comp-reversing FunctorStr over B,C;
clusterG * F -> comp-preserving ;
coherence
G * F is comp-preserving
proof
let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1)
A3: ( <^(F . o2),(F . o1)^> <> {} & <^(F . o3),(F . o2)^> <> {} ) by A1, A2, FUNCTOR0:def_19;
let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . b1) * ((G * F) . f)
let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . g) * ((G * F) . f)
A4: ( (G * F) . o1 = G . (F . o1) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33;
A5: (G * F) . o2 = G . (F . o2) by FUNCTOR0:33;
then reconsider GFg = (G * F) . g as Morphism of (G . (F . o2)),(G . (F . o3)) by FUNCTOR0:33;
<^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2;
hence (G * F) . (g * f) = G . (F . (g * f)) by Th7
.= G . ((F . f) * (F . g)) by A1, A2, FUNCTOR0:def_24
.= (G . (F . g)) * (G . (F . f)) by A3, FUNCTOR0:def_24
.= GFg * (G . (F . f)) by A2, Th7
.= ((G * F) . g) * ((G * F) . f) by A1, A5, A4, Th7 ;
::_thesis: verum
end;
end;
registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Covariant comp-preserving FunctorStr over A,B;
let G be feasible Contravariant comp-reversing FunctorStr over B,C;
clusterG * F -> comp-reversing ;
coherence
G * F is comp-reversing
proof
let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_24 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2)
A3: ( <^(F . o1),(F . o2)^> <> {} & <^(F . o2),(F . o3)^> <> {} ) by A1, A2, FUNCTOR0:def_18;
let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . f) * ((G * F) . b1)
let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . f) * ((G * F) . g)
A4: ( (G * F) . o2 = G . (F . o2) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33;
A5: (G * F) . o1 = G . (F . o1) by FUNCTOR0:33;
then reconsider GFf = (G * F) . f as Morphism of (G . (F . o2)),(G . (F . o1)) by FUNCTOR0:33;
<^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2;
hence (G * F) . (g * f) = G . (F . (g * f)) by Th8
.= G . ((F . g) * (F . f)) by A1, A2, FUNCTOR0:def_23
.= (G . (F . f)) * (G . (F . g)) by A3, FUNCTOR0:def_24
.= GFf * (G . (F . g)) by A1, Th8
.= ((G * F) . f) * ((G * F) . g) by A2, A5, A4, Th8 ;
::_thesis: verum
end;
end;
registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Contravariant comp-reversing FunctorStr over A,B;
let G be feasible Covariant comp-preserving FunctorStr over B,C;
clusterG * F -> comp-reversing ;
coherence
G * F is comp-reversing
proof
let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_24 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2)
A3: ( <^(F . o2),(F . o1)^> <> {} & <^(F . o3),(F . o2)^> <> {} ) by A1, A2, FUNCTOR0:def_19;
let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . f) * ((G * F) . b1)
let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . f) * ((G * F) . g)
A4: ( (G * F) . o2 = G . (F . o2) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33;
A5: (G * F) . o1 = G . (F . o1) by FUNCTOR0:33;
then reconsider GFf = (G * F) . f as Morphism of (G . (F . o2)),(G . (F . o1)) by FUNCTOR0:33;
<^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2;
hence (G * F) . (g * f) = G . (F . (g * f)) by Th9
.= G . ((F . f) * (F . g)) by A1, A2, FUNCTOR0:def_24
.= (G . (F . f)) * (G . (F . g)) by A3, FUNCTOR0:def_23
.= GFf * (G . (F . g)) by A1, Th9
.= ((G * F) . f) * ((G * F) . g) by A2, A5, A4, Th9 ;
::_thesis: verum
end;
end;
definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be covariant Functor of A,B;
let G be covariant Functor of B,C;
:: original: *
redefine funcG * F -> strict covariant Functor of A,C;
coherence
G * F is strict covariant Functor of A,C by FUNCTOR0:def_25;
end;
definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be contravariant Functor of A,B;
let G be contravariant Functor of B,C;
:: original: *
redefine funcG * F -> strict covariant Functor of A,C;
coherence
G * F is strict covariant Functor of A,C by FUNCTOR0:def_25;
end;
definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be covariant Functor of A,B;
let G be contravariant Functor of B,C;
:: original: *
redefine funcG * F -> strict contravariant Functor of A,C;
coherence
G * F is strict contravariant Functor of A,C by FUNCTOR0:def_25;
end;
definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be contravariant Functor of A,B;
let G be covariant Functor of B,C;
:: original: *
redefine funcG * F -> strict contravariant Functor of A,C;
coherence
G * F is strict contravariant Functor of A,C by FUNCTOR0:def_25;
end;
theorem Th10: :: FUNCTOR3:10
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
proof
let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
let G1, G2 be covariant Functor of B,C; ::_thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1 * F1 is_transformable_to G2 * F2 )
assume A1: for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ; :: according to FUNCTOR2:def_1 ::_thesis: ( not G1 is_transformable_to G2 or G1 * F1 is_transformable_to G2 * F2 )
assume A2: for a being object of B holds <^(G1 . a),(G2 . a)^> <> {} ; :: according to FUNCTOR2:def_1 ::_thesis: G1 * F1 is_transformable_to G2 * F2
let a be object of A; :: according to FUNCTOR2:def_1 ::_thesis: not <^((G1 * F1) . a),((G2 * F2) . a)^> = {}
<^(F1 . a),(F2 . a)^> <> {} by A1;
then A3: <^(G1 . (F1 . a)),(G1 . (F2 . a))^> <> {} by FUNCTOR0:def_18;
A4: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by FUNCTOR0:33;
<^(G1 . (F2 . a)),(G2 . (F2 . a))^> <> {} by A2;
hence not <^((G1 * F1) . a),((G2 * F2) . a)^> = {} by A4, A3, ALTCAT_1:def_2; ::_thesis: verum
end;
begin
definition
let A, B, C be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
let t be transformation of F1,F2;
let G be covariant Functor of B,C;
assume B1: F1 is_transformable_to F2 ;
funcG * t -> transformation of G * F1,G * F2 means :Def1: :: FUNCTOR3:def 1
for o being object of A holds it . o = G . (t ! o);
existence
ex b1 being transformation of G * F1,G * F2 st
for o being object of A holds b1 . o = G . (t ! o)
proof
defpred S1[ set , set ] means ex o being object of A st
( $1 = o & $2 = G . (t ! o) );
set I = the carrier of A;
A1: for i being set st i in the carrier of A holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in the carrier of A implies ex j being set st S1[i,j] )
assume i in the carrier of A ; ::_thesis: ex j being set st S1[i,j]
then reconsider o = i as object of A ;
take G . (t ! o) ; ::_thesis: S1[i,G . (t ! o)]
thus S1[i,G . (t ! o)] ; ::_thesis: verum
end;
consider IT being ManySortedSet of the carrier of A such that
A2: for o being set st o in the carrier of A holds
S1[o,IT . o] from PBOOLE:sch_3(A1);
IT is transformation of G * F1,G * F2
proof
thus G * F1 is_transformable_to G * F2 by B1, Th10; :: according to FUNCTOR2:def_2 ::_thesis: for b1 being M2( the carrier of A) holds IT . b1 is M2(<^((G * F1) . b1),((G * F2) . b1)^>)
let o be object of A; ::_thesis: IT . o is M2(<^((G * F1) . o),((G * F2) . o)^>)
( S1[o,IT . o] & G . (F1 . o) = (G * F1) . o ) by A2, FUNCTOR0:33;
hence IT . o is M2(<^((G * F1) . o),((G * F2) . o)^>) by FUNCTOR0:33; ::_thesis: verum
end;
then reconsider IT = IT as transformation of G * F1,G * F2 ;
take IT ; ::_thesis: for o being object of A holds IT . o = G . (t ! o)
let o be object of A; ::_thesis: IT . o = G . (t ! o)
S1[o,IT . o] by A2;
hence IT . o = G . (t ! o) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being transformation of G * F1,G * F2 st ( for o being object of A holds b1 . o = G . (t ! o) ) & ( for o being object of A holds b2 . o = G . (t ! o) ) holds
b1 = b2
proof
let X, Y be transformation of G * F1,G * F2; ::_thesis: ( ( for o being object of A holds X . o = G . (t ! o) ) & ( for o being object of A holds Y . o = G . (t ! o) ) implies X = Y )
assume that
A3: for o being object of A holds X . o = G . (t ! o) and
A4: for o being object of A holds Y . o = G . (t ! o) ; ::_thesis: X = Y
A5: G * F1 is_transformable_to G * F2 by B1, Th10;
now__::_thesis:_for_o_being_object_of_A_holds_X_!_o_=_Y_!_o
let o be object of A; ::_thesis: X ! o = Y ! o
thus X ! o = X . o by A5, FUNCTOR2:def_4
.= G . (t ! o) by A3
.= Y . o by A4
.= Y ! o by A5, FUNCTOR2:def_4 ; ::_thesis: verum
end;
hence X = Y by B1, Th10, FUNCTOR2:3; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines * FUNCTOR3:def_1_:_
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for t being transformation of F1,F2
for G being covariant Functor of B,C st F1 is_transformable_to F2 holds
for b8 being transformation of G * F1,G * F2 holds
( b8 = G * t iff for o being object of A holds b8 . o = G . (t ! o) );
theorem Th11: :: FUNCTOR3:11
for C, B, A being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for o being object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
proof
let C, B, A be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for o being object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for o being object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let G1 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2
for o being object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let p be transformation of F1,F2; ::_thesis: for o being object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let o be object of A; ::_thesis: ( F1 is_transformable_to F2 implies (G1 * p) ! o = G1 . (p ! o) )
assume A1: F1 is_transformable_to F2 ; ::_thesis: (G1 * p) ! o = G1 . (p ! o)
then G1 * F1 is_transformable_to G1 * F2 by Th10;
hence (G1 * p) ! o = (G1 * p) . o by FUNCTOR2:def_4
.= G1 . (p ! o) by A1, Def1 ;
::_thesis: verum
end;
definition
let A, B, C be non empty transitive with_units AltCatStr ;
let G1, G2 be covariant Functor of B,C;
let F be covariant Functor of A,B;
let s be transformation of G1,G2;
assume B1: G1 is_transformable_to G2 ;
funcs * F -> transformation of G1 * F,G2 * F means :Def2: :: FUNCTOR3:def 2
for o being object of A holds it . o = s ! (F . o);
existence
ex b1 being transformation of G1 * F,G2 * F st
for o being object of A holds b1 . o = s ! (F . o)
proof
defpred S1[ set , set ] means ex o being object of A st
( $1 = o & $2 = s ! (F . o) );
set I = the carrier of A;
A1: for i being set st i in the carrier of A holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in the carrier of A implies ex j being set st S1[i,j] )
assume i in the carrier of A ; ::_thesis: ex j being set st S1[i,j]
then reconsider o = i as object of A ;
take s ! (F . o) ; ::_thesis: S1[i,s ! (F . o)]
thus S1[i,s ! (F . o)] ; ::_thesis: verum
end;
consider IT being ManySortedSet of the carrier of A such that
A2: for o being set st o in the carrier of A holds
S1[o,IT . o] from PBOOLE:sch_3(A1);
IT is transformation of G1 * F,G2 * F
proof
thus G1 * F is_transformable_to G2 * F by B1, Th10; :: according to FUNCTOR2:def_2 ::_thesis: for b1 being M2( the carrier of A) holds IT . b1 is M2(<^((G1 * F) . b1),((G2 * F) . b1)^>)
let o be object of A; ::_thesis: IT . o is M2(<^((G1 * F) . o),((G2 * F) . o)^>)
( S1[o,IT . o] & G1 . (F . o) = (G1 * F) . o ) by A2, FUNCTOR0:33;
hence IT . o is M2(<^((G1 * F) . o),((G2 * F) . o)^>) by FUNCTOR0:33; ::_thesis: verum
end;
then reconsider IT = IT as transformation of G1 * F,G2 * F ;
take IT ; ::_thesis: for o being object of A holds IT . o = s ! (F . o)
let o be object of A; ::_thesis: IT . o = s ! (F . o)
S1[o,IT . o] by A2;
hence IT . o = s ! (F . o) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being transformation of G1 * F,G2 * F st ( for o being object of A holds b1 . o = s ! (F . o) ) & ( for o being object of A holds b2 . o = s ! (F . o) ) holds
b1 = b2
proof
let X, Y be transformation of G1 * F,G2 * F; ::_thesis: ( ( for o being object of A holds X . o = s ! (F . o) ) & ( for o being object of A holds Y . o = s ! (F . o) ) implies X = Y )
assume that
A3: for o being object of A holds X . o = s ! (F . o) and
A4: for o being object of A holds Y . o = s ! (F . o) ; ::_thesis: X = Y
A5: G1 * F is_transformable_to G2 * F by B1, Th10;
now__::_thesis:_for_o_being_object_of_A_holds_X_!_o_=_Y_!_o
let o be object of A; ::_thesis: X ! o = Y ! o
thus X ! o = X . o by A5, FUNCTOR2:def_4
.= s ! (F . o) by A3
.= Y . o by A4
.= Y ! o by A5, FUNCTOR2:def_4 ; ::_thesis: verum
end;
hence X = Y by B1, Th10, FUNCTOR2:3; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines * FUNCTOR3:def_2_:_
for A, B, C being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for F being covariant Functor of A,B
for s being transformation of G1,G2 st G1 is_transformable_to G2 holds
for b8 being transformation of G1 * F,G2 * F holds
( b8 = s * F iff for o being object of A holds b8 . o = s ! (F . o) );
theorem Th12: :: FUNCTOR3:12
for B, C, A being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2
for o being object of A st G1 is_transformable_to G2 holds
(q * F1) ! o = q ! (F1 . o)
proof
let B, C, A be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2
for o being object of A st G1 is_transformable_to G2 holds
(q * F1) ! o = q ! (F1 . o)
let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2
for o being object of A st G1 is_transformable_to G2 holds
(q * F1) ! o = q ! (F1 . o)
let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2
for o being object of A st G1 is_transformable_to G2 holds
(q * F1) ! o = q ! (F1 . o)
let q be transformation of G1,G2; ::_thesis: for o being object of A st G1 is_transformable_to G2 holds
(q * F1) ! o = q ! (F1 . o)
let o be object of A; ::_thesis: ( G1 is_transformable_to G2 implies (q * F1) ! o = q ! (F1 . o) )
assume A1: G1 is_transformable_to G2 ; ::_thesis: (q * F1) ! o = q ! (F1 . o)
then G1 * F1 is_transformable_to G2 * F1 by Th10;
hence (q * F1) ! o = (q * F1) . o by FUNCTOR2:def_4
.= q ! (F1 . o) by A1, Def2 ;
::_thesis: verum
end;
theorem Th13: :: FUNCTOR3:13
for C, A, B being non empty transitive with_units AltCatStr
for F1, F2, F3 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
proof
let C, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2, F3 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let F1, F2, F3 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let G1 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let p be transformation of F1,F2; ::_thesis: for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let p1 be transformation of F2,F3; ::_thesis: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 implies G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) )
assume that
A1: F1 is_transformable_to F2 and
A2: F2 is_transformable_to F3 ; ::_thesis: G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
A3: ( G1 * F1 is_transformable_to G1 * F2 & G1 * F2 is_transformable_to G1 * F3 ) by A1, A2, Th10;
A4: now__::_thesis:_for_a_being_object_of_A_holds_(G1_*_(p1_`*`_p))_!_a_=_((G1_*_p1)_`*`_(G1_*_p))_!_a
let a be object of A; ::_thesis: (G1 * (p1 `*` p)) ! a = ((G1 * p1) `*` (G1 * p)) ! a
A5: ( G1 . (F2 . a) = (G1 * F2) . a & G1 . (F3 . a) = (G1 * F3) . a ) by FUNCTOR0:33;
A6: G1 . (F1 . a) = (G1 * F1) . a by FUNCTOR0:33;
then reconsider G1ta = (G1 * p) ! a as Morphism of (G1 . (F1 . a)),(G1 . (F2 . a)) by FUNCTOR0:33;
A7: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A1, A2, FUNCTOR2:def_1;
thus (G1 * (p1 `*` p)) ! a = G1 . ((p1 `*` p) ! a) by A1, A2, Th11, FUNCTOR2:2
.= G1 . ((p1 ! a) * (p ! a)) by A1, A2, FUNCTOR2:def_5
.= (G1 . (p1 ! a)) * (G1 . (p ! a)) by A7, FUNCTOR0:def_23
.= (G1 . (p1 ! a)) * G1ta by A1, Th11
.= ((G1 * p1) ! a) * ((G1 * p) ! a) by A2, A6, A5, Th11
.= ((G1 * p1) `*` (G1 * p)) ! a by A3, FUNCTOR2:def_5 ; ::_thesis: verum
end;
F1 is_transformable_to F3 by A1, A2, FUNCTOR2:2;
hence G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) by A4, Th10, FUNCTOR2:3; ::_thesis: verum
end;
theorem Th14: :: FUNCTOR3:14
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
proof
let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let F1 be covariant Functor of A,B; ::_thesis: for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let G1, G2, G3 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let q be transformation of G1,G2; ::_thesis: for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let q1 be transformation of G2,G3; ::_thesis: ( G1 is_transformable_to G2 & G2 is_transformable_to G3 implies (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) )
assume that
A1: G1 is_transformable_to G2 and
A2: G2 is_transformable_to G3 ; ::_thesis: (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
A3: ( G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G3 * F1 ) by A1, A2, Th10;
A4: now__::_thesis:_for_a_being_object_of_A_holds_((q1_`*`_q)_*_F1)_!_a_=_((q1_*_F1)_`*`_(q_*_F1))_!_a
let a be object of A; ::_thesis: ((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! a
A5: ( G1 . (F1 . a) = (G1 * F1) . a & G3 . (F1 . a) = (G3 * F1) . a ) by FUNCTOR0:33;
A6: G2 . (F1 . a) = (G2 * F1) . a by FUNCTOR0:33;
then reconsider s1F1a = (q1 * F1) ! a as Morphism of (G2 . (F1 . a)),(G3 . (F1 . a)) by FUNCTOR0:33;
thus ((q1 `*` q) * F1) ! a = (q1 `*` q) ! (F1 . a) by A1, A2, Th12, FUNCTOR2:2
.= (q1 ! (F1 . a)) * (q ! (F1 . a)) by A1, A2, FUNCTOR2:def_5
.= s1F1a * (q ! (F1 . a)) by A2, Th12
.= ((q1 * F1) ! a) * ((q * F1) ! a) by A1, A6, A5, Th12
.= ((q1 * F1) `*` (q * F1)) ! a by A3, FUNCTOR2:def_5 ; ::_thesis: verum
end;
G1 is_transformable_to G3 by A1, A2, FUNCTOR2:2;
hence (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) by A4, Th10, FUNCTOR2:3; ::_thesis: verum
end;
theorem Th15: :: FUNCTOR3:15
for A, B, C, D being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
proof
let A, B, C, D be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let F1 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let G1 be covariant Functor of B,C; ::_thesis: for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let H1, H2 be covariant Functor of C,D; ::_thesis: for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let r be transformation of H1,H2; ::_thesis: ( H1 is_transformable_to H2 implies (r * G1) * F1 = r * (G1 * F1) )
A1: (H2 * G1) * F1 = H2 * (G1 * F1) by FUNCTOR0:32;
then reconsider m = r * (G1 * F1) as transformation of (H1 * G1) * F1,(H2 * G1) * F1 by FUNCTOR0:32;
assume A2: H1 is_transformable_to H2 ; ::_thesis: (r * G1) * F1 = r * (G1 * F1)
A3: now__::_thesis:_for_a_being_object_of_A_holds_((r_*_G1)_*_F1)_!_a_=_m_!_a
let a be object of A; ::_thesis: ((r * G1) * F1) ! a = m ! a
thus ((r * G1) * F1) ! a = (r * G1) ! (F1 . a) by A2, Th10, Th12
.= r ! (G1 . (F1 . a)) by A2, Th12
.= r ! ((G1 * F1) . a) by FUNCTOR0:33
.= (r * (G1 * F1)) ! a by A2, Th12
.= m ! a by A1, FUNCTOR0:32 ; ::_thesis: verum
end;
H1 * G1 is_transformable_to H2 * G1 by A2, Th10;
hence (r * G1) * F1 = r * (G1 * F1) by A3, Th10, FUNCTOR2:3; ::_thesis: verum
end;
theorem Th16: :: FUNCTOR3:16
for A, D, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)
proof
let A, D, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)
let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)
let G1, G2 be covariant Functor of B,C; ::_thesis: for H1 being covariant Functor of C,D
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)
let H1 be covariant Functor of C,D; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)
let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies (H1 * q) * F1 = H1 * (q * F1) )
A1: (H1 * G2) * F1 = H1 * (G2 * F1) by FUNCTOR0:32;
then reconsider m = H1 * (q * F1) as transformation of (H1 * G1) * F1,(H1 * G2) * F1 by FUNCTOR0:32;
assume A2: G1 is_transformable_to G2 ; ::_thesis: (H1 * q) * F1 = H1 * (q * F1)
A3: now__::_thesis:_for_a_being_object_of_A_holds_((H1_*_q)_*_F1)_!_a_=_m_!_a
let a be object of A; ::_thesis: ((H1 * q) * F1) ! a = m ! a
A4: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33;
thus ((H1 * q) * F1) ! a = (H1 * q) ! (F1 . a) by A2, Th10, Th12
.= H1 . (q ! (F1 . a)) by A2, Th11
.= H1 . ((q * F1) ! a) by A2, A4, Th12
.= (H1 * (q * F1)) ! a by A2, Th10, Th11
.= m ! a by A1, FUNCTOR0:32 ; ::_thesis: verum
end;
H1 * G1 is_transformable_to H1 * G2 by A2, Th10;
hence (H1 * q) * F1 = H1 * (q * F1) by A3, Th10, FUNCTOR2:3; ::_thesis: verum
end;
theorem Th17: :: FUNCTOR3:17
for C, D, A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(H1 * G1) * p = H1 * (G1 * p)
proof
let C, D, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(H1 * G1) * p = H1 * (G1 * p)
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(H1 * G1) * p = H1 * (G1 * p)
let G1 be covariant Functor of B,C; ::_thesis: for H1 being covariant Functor of C,D
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(H1 * G1) * p = H1 * (G1 * p)
let H1 be covariant Functor of C,D; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(H1 * G1) * p = H1 * (G1 * p)
let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies (H1 * G1) * p = H1 * (G1 * p) )
A1: (H1 * G1) * F2 = H1 * (G1 * F2) by FUNCTOR0:32;
then reconsider m = H1 * (G1 * p) as transformation of (H1 * G1) * F1,(H1 * G1) * F2 by FUNCTOR0:32;
assume A2: F1 is_transformable_to F2 ; ::_thesis: (H1 * G1) * p = H1 * (G1 * p)
now__::_thesis:_for_a_being_object_of_A_holds_((H1_*_G1)_*_p)_!_a_=_m_!_a
let a be object of A; ::_thesis: ((H1 * G1) * p) ! a = m ! a
A3: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33;
A4: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1;
thus ((H1 * G1) * p) ! a = (H1 * G1) . (p ! a) by A2, Th11
.= H1 . (G1 . (p ! a)) by A4, Th6
.= H1 . ((G1 * p) ! a) by A2, A3, Th11
.= (H1 * (G1 * p)) ! a by A2, Th10, Th11
.= m ! a by A1, FUNCTOR0:32 ; ::_thesis: verum
end;
hence (H1 * G1) * p = H1 * (G1 * p) by A2, Th10, FUNCTOR2:3; ::_thesis: verum
end;
theorem Th18: :: FUNCTOR3:18
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)
proof
let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)
let F1 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)
let G1 be covariant Functor of B,C; ::_thesis: (idt G1) * F1 = idt (G1 * F1)
now__::_thesis:_for_a_being_object_of_A_holds_((idt_G1)_*_F1)_!_a_=_(idt_(G1_*_F1))_!_a
let a be object of A; ::_thesis: ((idt G1) * F1) ! a = (idt (G1 * F1)) ! a
thus ((idt G1) * F1) ! a = (idt G1) ! (F1 . a) by Th12
.= idm (G1 . (F1 . a)) by FUNCTOR2:4
.= idm ((G1 * F1) . a) by FUNCTOR0:33
.= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; ::_thesis: verum
end;
hence (idt G1) * F1 = idt (G1 * F1) by FUNCTOR2:3; ::_thesis: verum
end;
theorem Th19: :: FUNCTOR3:19
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1)
proof
let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1)
let F1 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1)
let G1 be covariant Functor of B,C; ::_thesis: G1 * (idt F1) = idt (G1 * F1)
now__::_thesis:_for_a_being_object_of_A_holds_(G1_*_(idt_F1))_!_a_=_(idt_(G1_*_F1))_!_a
let a be object of A; ::_thesis: (G1 * (idt F1)) ! a = (idt (G1 * F1)) ! a
thus (G1 * (idt F1)) ! a = G1 . ((idt F1) ! a) by Th11
.= G1 . (idm (F1 . a)) by FUNCTOR2:4
.= idm (G1 . (F1 . a)) by FUNCTOR2:1
.= idm ((G1 * F1) . a) by FUNCTOR0:33
.= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; ::_thesis: verum
end;
hence G1 * (idt F1) = idt (G1 * F1) by FUNCTOR2:3; ::_thesis: verum
end;
theorem Th20: :: FUNCTOR3:20
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p
let F1, F2 be covariant Functor of A,B; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p
let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies (id B) * p = p )
assume A1: F1 is_transformable_to F2 ; ::_thesis: (id B) * p = p
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_A_holds_
((id_B)_*_p)_._i_=_p_._i
let i be set ; ::_thesis: ( i in the carrier of A implies ((id B) * p) . i = p . i )
assume i in the carrier of A ; ::_thesis: ((id B) * p) . i = p . i
then reconsider a = i as object of A ;
A2: <^(F1 . a),(F2 . a)^> <> {} by A1, FUNCTOR2:def_1;
thus ((id B) * p) . i = (id B) . (p ! a) by A1, Def1
.= p ! a by A2, FUNCTOR0:31
.= p . i by A1, FUNCTOR2:def_4 ; ::_thesis: verum
end;
hence (id B) * p = p by PBOOLE:3; ::_thesis: verum
end;
theorem Th21: :: FUNCTOR3:21
for C, B being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * (id B) = q
proof
let C, B be non empty transitive with_units AltCatStr ; ::_thesis: for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * (id B) = q
let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * (id B) = q
let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies q * (id B) = q )
assume A1: G1 is_transformable_to G2 ; ::_thesis: q * (id B) = q
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_B_holds_
(q_*_(id_B))_._i_=_q_._i
let i be set ; ::_thesis: ( i in the carrier of B implies (q * (id B)) . i = q . i )
assume i in the carrier of B ; ::_thesis: (q * (id B)) . i = q . i
then reconsider a = i as object of B ;
thus (q * (id B)) . i = q ! ((id B) . a) by A1, Def2
.= q ! a by FUNCTOR0:29
.= q . i by A1, FUNCTOR2:def_4 ; ::_thesis: verum
end;
hence q * (id B) = q by PBOOLE:3; ::_thesis: verum
end;
begin
definition
let A, B, C be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
let G1, G2 be covariant Functor of B,C;
let t be transformation of F1,F2;
let s be transformation of G1,G2;
funcs (#) t -> transformation of G1 * F1,G2 * F2 equals :: FUNCTOR3:def 3
(s * F2) `*` (G1 * t);
coherence
(s * F2) `*` (G1 * t) is transformation of G1 * F1,G2 * F2 ;
end;
:: deftheorem defines (#) FUNCTOR3:def_3_:_
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for t being transformation of F1,F2
for s being transformation of G1,G2 holds s (#) t = (s * F2) `*` (G1 * t);
theorem Th22: :: FUNCTOR3:22
for C, A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
proof
let C, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let G1, G2 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let p be transformation of F1,F2; ::_thesis: for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let q be natural_transformation of G1,G2; ::_thesis: ( F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 implies q (#) p = (G2 * p) `*` (q * F1) )
assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; ::_thesis: q (#) p = (G2 * p) `*` (q * F1)
A3: G1 * F1 is_transformable_to G1 * F2 by A1, Th10;
A4: G2 * F1 is_transformable_to G2 * F2 by A1, Th10;
A5: G1 is_transformable_to G2 by A2, FUNCTOR2:def_6;
then A6: G1 * F1 is_transformable_to G2 * F1 by Th10;
A7: G1 * F2 is_transformable_to G2 * F2 by A5, Th10;
now__::_thesis:_for_a_being_object_of_A_holds_((q_*_F2)_`*`_(G1_*_p))_!_a_=_((G2_*_p)_`*`_(q_*_F1))_!_a
let a be object of A; ::_thesis: ((q * F2) `*` (G1 * p)) ! a = ((G2 * p) `*` (q * F1)) ! a
A8: G1 . (F1 . a) = (G1 * F1) . a by FUNCTOR0:33;
A9: G2 . (F2 . a) = (G2 * F2) . a by FUNCTOR0:33;
then reconsider sF2a = q ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) by FUNCTOR0:33;
reconsider G2ta = (G2 * p) ! a as Morphism of (G2 . (F1 . a)),(G2 . (F2 . a)) by A9, FUNCTOR0:33;
A10: G1 . (F2 . a) = (G1 * F2) . a by FUNCTOR0:33;
A11: <^(F1 . a),(F2 . a)^> <> {} by A1, FUNCTOR2:def_1;
A12: G2 . (F1 . a) = (G2 * F1) . a by FUNCTOR0:33;
thus ((q * F2) `*` (G1 * p)) ! a = ((q * F2) ! a) * ((G1 * p) ! a) by A7, A3, FUNCTOR2:def_5
.= sF2a * ((G1 * p) ! a) by A5, Th12
.= (q ! (F2 . a)) * (G1 . (p ! a)) by A1, A8, A10, A9, Th11
.= (G2 . (p ! a)) * (q ! (F1 . a)) by A2, A11, FUNCTOR2:def_7
.= G2ta * (q ! (F1 . a)) by A1, Th11
.= ((G2 * p) ! a) * ((q * F1) ! a) by A5, A8, A12, A9, Th12
.= ((G2 * p) `*` (q * F1)) ! a by A6, A4, FUNCTOR2:def_5 ; ::_thesis: verum
end;
hence q (#) p = (G2 * p) `*` (q * F1) by A1, A5, Th10, FUNCTOR2:3; ::_thesis: verum
end;
theorem :: FUNCTOR3:23
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(idt (id B)) (#) p = p
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(idt (id B)) (#) p = p
let F1, F2 be covariant Functor of A,B; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(idt (id B)) (#) p = p
let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies (idt (id B)) (#) p = p )
assume A1: F1 is_transformable_to F2 ; ::_thesis: (idt (id B)) (#) p = p
then A2: (id B) * F1 is_transformable_to (id B) * F2 by Th10;
thus (idt (id B)) (#) p = (idt ((id B) * F2)) `*` ((id B) * p) by Th18
.= (id B) * p by A2, FUNCTOR2:5
.= p by A1, Th20 ; ::_thesis: verum
end;
theorem :: FUNCTOR3:24
for C, B being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q
proof
let C, B be non empty transitive with_units AltCatStr ; ::_thesis: for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q
let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q
let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies q (#) (idt (id B)) = q )
assume A1: G1 is_transformable_to G2 ; ::_thesis: q (#) (idt (id B)) = q
then A2: G1 * (id B) is_transformable_to G2 * (id B) by Th10;
thus q (#) (idt (id B)) = (q * (id B)) `*` (idt (G1 * (id B))) by Th19
.= q * (id B) by A2, FUNCTOR2:5
.= q by A1, Th21 ; ::_thesis: verum
end;
theorem :: FUNCTOR3:25
for C, A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
proof
let C, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
let G1 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies G1 * p = (idt G1) (#) p )
assume F1 is_transformable_to F2 ; ::_thesis: G1 * p = (idt G1) (#) p
then G1 * F1 is_transformable_to G1 * F2 by Th10;
hence G1 * p = (idt (G1 * F2)) `*` (G1 * p) by FUNCTOR2:5
.= (idt G1) (#) p by Th18 ;
::_thesis: verum
end;
theorem :: FUNCTOR3:26
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * F1 = q (#) (idt F1)
proof
let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * F1 = q (#) (idt F1)
let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * F1 = q (#) (idt F1)
let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * F1 = q (#) (idt F1)
let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies q * F1 = q (#) (idt F1) )
assume G1 is_transformable_to G2 ; ::_thesis: q * F1 = q (#) (idt F1)
then G1 * F1 is_transformable_to G2 * F1 by Th10;
hence q * F1 = (q * F1) `*` (idt (G1 * F1)) by FUNCTOR2:5
.= q (#) (idt F1) by Th19 ;
::_thesis: verum
end;
theorem :: FUNCTOR3:27
for A, B, C, D being category
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
proof
let A, B, C, D be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let G1, G2 be covariant Functor of B,C; ::_thesis: for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let H1, H2 be covariant Functor of C,D; ::_thesis: for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let t be transformation of F1,F2; ::_thesis: for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let s be transformation of G1,G2; ::_thesis: for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let u be transformation of H1,H2; ::_thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 implies (u (#) s) (#) t = u (#) (s (#) t) )
assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_transformable_to G2 and
A3: H1 is_transformable_to H2 ; ::_thesis: (u (#) s) (#) t = u (#) (s (#) t)
A4: ( G1 * F2 is_transformable_to G2 * F2 & G1 * F1 is_transformable_to G1 * F2 ) by A1, A2, Th10;
A5: ( (H1 * s) * F2 = H1 * (s * F2) & (H1 * G1) * t = H1 * (G1 * t) ) by A1, A2, Th16, Th17;
A6: ( (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by FUNCTOR0:32;
A7: ( (H1 * G1) * F1 is_transformable_to (H1 * G1) * F2 & (u * G2) * F2 = u * (G2 * F2) ) by A1, A3, Th10, Th15;
A8: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) ) by FUNCTOR0:32;
A9: H1 * G1 is_transformable_to H1 * G2 by A2, Th10;
then A10: (H1 * G1) * F2 is_transformable_to (H1 * G2) * F2 by Th10;
A11: H1 * G2 is_transformable_to H2 * G2 by A3, Th10;
then A12: (H1 * G2) * F2 is_transformable_to (H2 * G2) * F2 by Th10;
thus (u (#) s) (#) t = (((u * G2) * F2) `*` ((H1 * s) * F2)) `*` ((H1 * G1) * t) by A11, A9, Th14
.= (u * (G2 * F2)) `*` ((H1 * (s * F2)) `*` (H1 * (G1 * t))) by A12, A10, A7, A5, A8, A6, FUNCTOR2:6
.= u (#) (s (#) t) by A4, Th13 ; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_A,_B,_C_being_category
for_F1,_F2_being_covariant_Functor_of_A,B
for_G1,_G2_being_covariant_Functor_of_B,C
for_s_being_natural_transformation_of_G1,G2
for_t_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&_G1_is_naturally_transformable_to_G2_holds_
(_G1_*_F1_is_naturally_transformable_to_G2_*_F2_&_s_(#)_t_is_natural_transformation_of_G1_*_F1,G2_*_F2_)
let A, B, C be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let G1, G2 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let s be natural_transformation of G1,G2; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )
set k = s (#) t;
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: ( G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )
then A2: F1 is_transformable_to F2 by FUNCTOR2:def_6;
assume A3: G1 is_naturally_transformable_to G2 ; ::_thesis: ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )
then A4: G1 is_transformable_to G2 by FUNCTOR2:def_6;
A5: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_((s_(#)_t)_!_b)_*_((G1_*_F1)_._f)_=_((G2_*_F2)_._f)_*_((s_(#)_t)_!_a)
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a) )
assume A6: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)
A7: <^((G1 * F1) . a),((G1 * F1) . b)^> <> {} by A6, FUNCTOR0:def_18;
A8: (G2 * F2) . a = G2 . (F2 . a) by FUNCTOR0:33;
then reconsider sF2a = s ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) by FUNCTOR0:33;
A9: (G2 * F2) . b = G2 . (F2 . b) by FUNCTOR0:33;
then reconsider sF2b = s ! (F2 . b) as Morphism of ((G1 * F2) . b),((G2 * F2) . b) by FUNCTOR0:33;
<^(G1 . (F2 . b)),(G2 . (F2 . b))^> <> {} by A4, FUNCTOR2:def_1;
then A10: <^((G1 * F2) . b),((G2 * F2) . b)^> <> {} by A9, FUNCTOR0:33;
let f be Morphism of a,b; ::_thesis: ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)
A11: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33;
then reconsider G1tbF1f = G1 . ((t ! b) * (F1 . f)) as Morphism of ((G1 * F1) . a),((G1 * F2) . b) by FUNCTOR0:33;
reconsider G1ta = G1 . (t ! a) as Morphism of ((G1 * F1) . a),((G1 * F2) . a) by A11, FUNCTOR0:33;
A12: <^(G1 . (F1 . a)),(G2 . (F1 . a))^> <> {} by A4, FUNCTOR2:def_1;
A13: (G1 * F1) . b = G1 . (F1 . b) by FUNCTOR0:33;
then reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),((G1 * F2) . b) by FUNCTOR0:33;
A14: <^(F1 . b),(F2 . b)^> <> {} by A2, FUNCTOR2:def_1;
then <^(G1 . (F1 . b)),(G1 . (F2 . b))^> <> {} by FUNCTOR0:def_18;
then A15: <^((G1 * F1) . b),((G1 * F2) . b)^> <> {} by A13, FUNCTOR0:33;
A16: <^(F1 . a),(F1 . b)^> <> {} by A6, FUNCTOR0:def_18;
then A17: <^(F1 . a),(F2 . b)^> <> {} by A14, ALTCAT_1:def_2;
reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by A13, FUNCTOR0:33;
A18: s ! (F2 . a) = (s * F2) . a by A4, Def2;
A19: G1 . ((t ! b) * (F1 . f)) = (G1 . (t ! b)) * (G1 . (F1 . f)) by A14, A16, FUNCTOR0:def_23
.= G1tb * G1F1f by A11, A13, FUNCTOR0:33 ;
reconsider G2F2f = G2 . (F2 . f) as Morphism of ((G2 * F2) . a),((G2 * F2) . b) by A8, FUNCTOR0:33;
A20: s ! (F2 . b) = (s * F2) . b by A4, Def2;
A21: G1 * F2 is_transformable_to G2 * F2 by A4, Th10;
A22: <^(F2 . a),(F2 . b)^> <> {} by A6, FUNCTOR0:def_18;
then A23: <^(G2 . (F2 . a)),(G2 . (F2 . b))^> <> {} by FUNCTOR0:def_18;
A24: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1;
then A25: <^(G2 . (F1 . a)),(G2 . (F2 . a))^> <> {} by FUNCTOR0:def_18;
A26: G1 * F1 is_transformable_to G1 * F2 by A2, Th10;
hence ((s (#) t) ! b) * ((G1 * F1) . f) = (((s * F2) ! b) * ((G1 * t) ! b)) * ((G1 * F1) . f) by A21, FUNCTOR2:def_5
.= (sF2b * ((G1 * t) ! b)) * ((G1 * F1) . f) by A21, A20, FUNCTOR2:def_4
.= (sF2b * G1tb) * ((G1 * F1) . f) by A2, Th11
.= (sF2b * G1tb) * G1F1f by A6, Th6
.= sF2b * G1tbF1f by A7, A15, A10, A19, ALTCAT_1:21
.= (s ! (F2 . b)) * (G1 . ((t ! b) * (F1 . f))) by A11, A9, FUNCTOR0:33
.= (G2 . ((t ! b) * (F1 . f))) * (s ! (F1 . a)) by A3, A17, FUNCTOR2:def_7
.= (G2 . ((F2 . f) * (t ! a))) * (s ! (F1 . a)) by A1, A6, FUNCTOR2:def_7
.= ((G2 . (F2 . f)) * (G2 . (t ! a))) * (s ! (F1 . a)) by A22, A24, FUNCTOR0:def_23
.= (G2 . (F2 . f)) * ((G2 . (t ! a)) * (s ! (F1 . a))) by A12, A25, A23, ALTCAT_1:21
.= (G2 . (F2 . f)) * ((s ! (F2 . a)) * (G1 . (t ! a))) by A3, A24, FUNCTOR2:def_7
.= G2F2f * (sF2a * G1ta) by A11, A8, A9, FUNCTOR0:33
.= ((G2 * F2) . f) * (sF2a * G1ta) by A6, Th6
.= ((G2 * F2) . f) * (((s * F2) ! a) * G1ta) by A21, A18, FUNCTOR2:def_4
.= ((G2 * F2) . f) * (((s * F2) ! a) * ((G1 * t) ! a)) by A2, Th11
.= ((G2 * F2) . f) * ((s (#) t) ! a) by A21, A26, FUNCTOR2:def_5 ;
::_thesis: verum
end;
thus G1 * F1 is_naturally_transformable_to G2 * F2 ::_thesis: s (#) t is natural_transformation of G1 * F1,G2 * F2
proof
thus G1 * F1 is_transformable_to G2 * F2 by A2, A4, Th10; :: according to FUNCTOR2:def_6 ::_thesis: ex b1 being transformation of G1 * F1,G2 * F2 st
for b2, b3 being M2( the carrier of A) holds
( <^b2,b3^> = {} or for b4 being M2(<^b2,b3^>) holds (b1 ! b3) * ((G1 * F1) . b4) = ((G2 * F2) . b4) * (b1 ! b2) )
take s (#) t ; ::_thesis: for b1, b2 being M2( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) )
thus for b1, b2 being M2( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) ) by A5; ::_thesis: verum
end;
hence s (#) t is natural_transformation of G1 * F1,G2 * F2 by A5, FUNCTOR2:def_7; ::_thesis: verum
end;
theorem Th28: :: FUNCTOR3:28
for C, A, B being category
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
proof
let C, A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let G1 be covariant Functor of B,C; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies G1 * t is natural_transformation of G1 * F1,G1 * F2 )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: G1 * t is natural_transformation of G1 * F1,G1 * F2
then A2: F1 is_transformable_to F2 by FUNCTOR2:def_6;
thus G1 * F1 is_naturally_transformable_to G1 * F2 by A1, Lm2; :: according to FUNCTOR2:def_7 ::_thesis: for b1, b2 being M2( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((G1 * t) ! b2) * ((G1 * F1) . b3) = ((G1 * F2) . b3) * ((G1 * t) ! b1) )
let a, b be object of A; ::_thesis: ( <^a,b^> = {} or for b1 being M2(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a) )
assume A3: <^a,b^> <> {} ; ::_thesis: for b1 being M2(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a)
A4: ( (G1 * F1) . b = G1 . (F1 . b) & <^(F1 . a),(F1 . b)^> <> {} ) by A3, FUNCTOR0:33, FUNCTOR0:def_18;
A5: <^(F1 . b),(F2 . b)^> <> {} by A2, FUNCTOR2:def_1;
A6: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1;
reconsider G1ta = G1 . (t ! a) as Morphism of (G1 . (F1 . a)),((G1 * F2) . a) by FUNCTOR0:33;
reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),(G1 . (F2 . b)) by FUNCTOR0:33;
let f be Morphism of a,b; ::_thesis: ((G1 * t) ! b) * ((G1 * F1) . f) = ((G1 * F2) . f) * ((G1 * t) ! a)
A7: (G1 * F2) . a = G1 . (F2 . a) by FUNCTOR0:33;
A8: <^(F2 . a),(F2 . b)^> <> {} by A3, FUNCTOR0:def_18;
A9: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33;
then reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by FUNCTOR0:33;
A10: (G1 * F2) . b = G1 . (F2 . b) by FUNCTOR0:33;
hence ((G1 * t) ! b) * ((G1 * F1) . f) = G1tb * ((G1 * F1) . f) by A2, Th11
.= G1tb * G1F1f by A3, Th6
.= G1 . ((t ! b) * (F1 . f)) by A9, A4, A5, FUNCTOR0:def_23
.= G1 . ((F2 . f) * (t ! a)) by A1, A3, FUNCTOR2:def_7
.= (G1 . (F2 . f)) * (G1 . (t ! a)) by A6, A8, FUNCTOR0:def_23
.= ((G1 * F2) . f) * G1ta by A3, A7, A10, Th6
.= ((G1 * F2) . f) * ((G1 * t) ! a) by A2, A9, Th11 ;
::_thesis: verum
end;
theorem Th29: :: FUNCTOR3:29
for A, B, C being category
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
proof
let A, B, C be category; ::_thesis: for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
let G1, G2 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
let s be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies s * F1 is natural_transformation of G1 * F1,G2 * F1 )
assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: s * F1 is natural_transformation of G1 * F1,G2 * F1
thus G1 * F1 is_naturally_transformable_to G2 * F1 by A1, Lm2; :: according to FUNCTOR2:def_7 ::_thesis: for b1, b2 being M2( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s * F1) ! b2) * ((G1 * F1) . b3) = ((G2 * F1) . b3) * ((s * F1) ! b1) )
let a, b be object of A; ::_thesis: ( <^a,b^> = {} or for b1 being M2(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b1) = ((G2 * F1) . b1) * ((s * F1) ! a) )
assume A2: <^a,b^> <> {} ; ::_thesis: for b1 being M2(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b1) = ((G2 * F1) . b1) * ((s * F1) ! a)
A3: <^(F1 . a),(F1 . b)^> <> {} by A2, FUNCTOR0:def_18;
reconsider sF1a = s ! (F1 . a) as Morphism of (G1 . (F1 . a)),((G2 * F1) . a) by FUNCTOR0:33;
let f be Morphism of a,b; ::_thesis: ((s * F1) ! b) * ((G1 * F1) . f) = ((G2 * F1) . f) * ((s * F1) ! a)
A4: (G2 * F1) . a = G2 . (F1 . a) by FUNCTOR0:33;
A5: (G2 * F1) . b = G2 . (F1 . b) by FUNCTOR0:33;
then reconsider sF1b = s ! (F1 . b) as Morphism of ((G1 * F1) . b),((G2 * F1) . b) by FUNCTOR0:33;
A6: ( (G1 * F1) . b = G1 . (F1 . b) & (G2 * F1) . b = G2 . (F1 . b) ) by FUNCTOR0:33;
A7: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33;
then reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by FUNCTOR0:33;
A8: G1 is_transformable_to G2 by A1, FUNCTOR2:def_6;
hence ((s * F1) ! b) * ((G1 * F1) . f) = sF1b * ((G1 * F1) . f) by Th12
.= sF1b * G1F1f by A2, Th6
.= (G2 . (F1 . f)) * (s ! (F1 . a)) by A1, A7, A6, A3, FUNCTOR2:def_7
.= ((G2 * F1) . f) * sF1a by A2, A4, A5, Th6
.= ((G2 * F1) . f) * ((s * F1) ! a) by A8, A7, Th12 ;
::_thesis: verum
end;
theorem :: FUNCTOR3:30
for A, B, C being category
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for t being natural_transformation of F1,F2
for s being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) by Lm2;
theorem :: FUNCTOR3:31
for A, B, C being category
for F1, F2, F3 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
proof
let A, B, C be category; ::_thesis: for F1, F2, F3 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let F1, F2, F3 be covariant Functor of A,B; ::_thesis: for G1, G2, G3 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let G1, G2, G3 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let s be natural_transformation of G1,G2; ::_thesis: for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let s1 be natural_transformation of G2,G3; ::_thesis: for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let t be transformation of F1,F2; ::_thesis: for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let t1 be transformation of F2,F3; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_naturally_transformable_to F3 and
A3: G1 is_naturally_transformable_to G2 and
A4: G2 is_naturally_transformable_to G3 ; ::_thesis: (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
A5: F1 is_transformable_to F2 by A1, FUNCTOR2:def_6;
then A6: s (#) t = (G2 * t) `*` (s * F1) by A3, Th22;
A7: G2 * F1 is_transformable_to G2 * F2 by A5, Th10;
A8: G3 * F1 is_transformable_to G3 * F2 by A5, Th10;
G1 * F1 is_naturally_transformable_to G2 * F2 by A1, A3, Lm2;
then A9: G1 * F1 is_transformable_to G2 * F2 by FUNCTOR2:def_6;
A10: G1 is_transformable_to G2 by A3, FUNCTOR2:def_6;
then A11: G1 * F1 is_transformable_to G2 * F1 by Th10;
A12: F2 is_transformable_to F3 by A2, FUNCTOR2:def_6;
then A13: s1 (#) t1 = (G3 * t1) `*` (s1 * F2) by A4, Th22;
A14: G3 * F2 is_transformable_to G3 * F3 by A12, Th10;
A15: G2 is_transformable_to G3 by A4, FUNCTOR2:def_6;
then A16: G2 * F1 is_transformable_to G3 * F1 by Th10;
G1 is_transformable_to G3 by A10, A15, FUNCTOR2:2;
then A17: G1 * F1 is_transformable_to G3 * F1 by Th10;
A18: G2 * F2 is_transformable_to G3 * F2 by A15, Th10;
F1 is_transformable_to F3 by A5, A12, FUNCTOR2:2;
hence (s1 `*` s) (#) (t1 `*` t) = (G3 * (t1 `*` t)) `*` ((s1 `*` s) * F1) by A3, A4, Th22, FUNCTOR2:8
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by A5, A12, Th13
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by A3, A4, FUNCTOR2:def_8
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 * F1) `*` (s * F1)) by A10, A15, Th14
.= (G3 * t1) `*` ((G3 * t) `*` ((s1 * F1) `*` (s * F1))) by A14, A8, A17, FUNCTOR2:6
.= (G3 * t1) `*` (((G3 * t) `*` (s1 * F1)) `*` (s * F1)) by A8, A11, A16, FUNCTOR2:6
.= (G3 * t1) `*` ((s1 (#) t) `*` (s * F1)) by A4, A5, Th22
.= (G3 * t1) `*` ((s1 * F2) `*` ((G2 * t) `*` (s * F1))) by A11, A18, A7, FUNCTOR2:6
.= (s1 (#) t1) `*` (s (#) t) by A14, A18, A9, A13, A6, FUNCTOR2:6 ;
::_thesis: verum
end;
begin
theorem Th32: :: FUNCTOR3:32
for B, A being category
for F1, F2 being covariant Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
proof
let B, A be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
let F1, F2 be covariant Functor of A,B; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) implies ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) ) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1 and
A3: for a being object of A holds t ! a is iso ; ::_thesis: ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
defpred S1[ set , set ] means ex a being object of A st
( a = $1 & $2 = (t ! a) " );
set I = the carrier of A;
A4: for i being set st i in the carrier of A holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in the carrier of A implies ex j being set st S1[i,j] )
assume i in the carrier of A ; ::_thesis: ex j being set st S1[i,j]
then reconsider o = i as object of A ;
take (t ! o) " ; ::_thesis: S1[i,(t ! o) " ]
thus S1[i,(t ! o) " ] ; ::_thesis: verum
end;
consider f being ManySortedSet of the carrier of A such that
A5: for i being set st i in the carrier of A holds
S1[i,f . i] from PBOOLE:sch_3(A4);
f is transformation of F2,F1
proof
thus F2 is_transformable_to F1 by A2; :: according to FUNCTOR2:def_2 ::_thesis: for b1 being M2( the carrier of A) holds f . b1 is M2(<^(F2 . b1),(F1 . b1)^>)
let a be object of A; ::_thesis: f . a is M2(<^(F2 . a),(F1 . a)^>)
ex b being object of A st
( b = a & f . a = (t ! b) " ) by A5;
hence f . a is M2(<^(F2 . a),(F1 . a)^>) ; ::_thesis: verum
end;
then reconsider f = f as transformation of F2,F1 ;
A6: F1 is_transformable_to F2 by A1, FUNCTOR2:def_6;
A7: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_g_being_Morphism_of_a,b_holds_(f_!_b)_*_(F2_._g)_=_(F1_._g)_*_(f_!_a)
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a) )
assume A8: <^a,b^> <> {} ; ::_thesis: for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a)
A9: <^(F1 . a),(F1 . b)^> <> {} by A8, FUNCTOR0:def_18;
let g be Morphism of a,b; ::_thesis: (f ! b) * (F2 . g) = (F1 . g) * (f ! a)
A10: ex bb being object of A st
( bb = b & f . b = (t ! bb) " ) by A5;
A11: t ! b is iso by A3;
A12: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def_1;
A13: <^(F1 . a),(F2 . a)^> <> {} by A6, FUNCTOR2:def_1;
A14: ex aa being object of A st
( aa = a & f . a = (t ! aa) " ) by A5;
then reconsider fa = f . a as Morphism of (F2 . a),(F1 . a) ;
A15: t ! a is iso by A3;
A16: <^(F1 . b),(F2 . b)^> <> {} by A6, FUNCTOR2:def_1;
A17: <^(F2 . b),(F1 . b)^> <> {} by A2, FUNCTOR2:def_1;
A18: <^(F2 . a),(F2 . b)^> <> {} by A8, FUNCTOR0:def_18;
then A19: <^(F2 . a),(F1 . b)^> <> {} by A17, ALTCAT_1:def_2;
hence (f ! b) * (F2 . g) = ((f ! b) * (F2 . g)) * (idm (F2 . a)) by ALTCAT_1:def_17
.= ((f ! b) * (F2 . g)) * ((t ! a) * fa) by A14, A15, ALTCAT_3:def_5
.= ((f ! b) * (F2 . g)) * ((t ! a) * (f ! a)) by A2, FUNCTOR2:def_4
.= (((f ! b) * (F2 . g)) * (t ! a)) * (f ! a) by A13, A12, A19, ALTCAT_1:21
.= ((f ! b) * ((F2 . g) * (t ! a))) * (f ! a) by A13, A17, A18, ALTCAT_1:21
.= ((f ! b) * ((t ! b) * (F1 . g))) * (f ! a) by A1, A8, FUNCTOR2:def_7
.= (((f ! b) * (t ! b)) * (F1 . g)) * (f ! a) by A17, A16, A9, ALTCAT_1:21
.= ((((t ! b) ") * (t ! b)) * (F1 . g)) * (f ! a) by A2, A10, FUNCTOR2:def_4
.= ((idm (F1 . b)) * (F1 . g)) * (f ! a) by A11, ALTCAT_3:def_5
.= (F1 . g) * (f ! a) by A9, ALTCAT_1:20 ;
::_thesis: verum
end;
hence F2 is_naturally_transformable_to F1 by A2, FUNCTOR2:def_6; ::_thesis: ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso )
F2 is_naturally_transformable_to F1 by A2, A7, FUNCTOR2:def_6;
then reconsider f = f as natural_transformation of F2,F1 by A7, FUNCTOR2:def_7;
take f ; ::_thesis: for a being object of A holds
( f . a = (t ! a) " & f ! a is iso )
let a be object of A; ::_thesis: ( f . a = (t ! a) " & f ! a is iso )
consider b being object of A such that
A20: b = a and
A21: f . a = (t ! b) " by A5;
thus f . a = (t ! a) " by A20, A21; ::_thesis: f ! a is iso
A22: <^(F1 . a),(F2 . a)^> <> {} by A6, FUNCTOR2:def_1;
A23: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def_1;
f ! a = (t ! b) " by A2, A21, FUNCTOR2:def_4;
hence f ! a is iso by A3, A20, A22, A23, ALTCAT_4:3; ::_thesis: verum
end;
definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
predF1,F2 are_naturally_equivalent means :Def4: :: FUNCTOR3:def 4
( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso );
reflexivity
for F1 being covariant Functor of A,B holds
( F1 is_naturally_transformable_to F1 & F1 is_transformable_to F1 & ex t being natural_transformation of F1,F1 st
for a being object of A holds t ! a is iso )
proof
let F be covariant Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F & F is_transformable_to F & ex t being natural_transformation of F,F st
for a being object of A holds t ! a is iso )
thus ( F is_naturally_transformable_to F & F is_transformable_to F ) ; ::_thesis: ex t being natural_transformation of F,F st
for a being object of A holds t ! a is iso
take idt F ; ::_thesis: for a being object of A holds (idt F) ! a is iso
let a be object of A; ::_thesis: (idt F) ! a is iso
(idt F) ! a = idm (F . a) by FUNCTOR2:4;
hence (idt F) ! a is iso ; ::_thesis: verum
end;
symmetry
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso holds
( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso )
proof
let F1, F2 be covariant Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso implies ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso ) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1 ; ::_thesis: ( for t being natural_transformation of F1,F2 holds
not for a being object of A holds t ! a is iso or ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso ) )
given t being natural_transformation of F1,F2 such that A3: for a being object of A holds t ! a is iso ; ::_thesis: ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso )
consider f being natural_transformation of F2,F1 such that
A4: for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) by A1, A2, A3, Th32;
thus F2 is_naturally_transformable_to F1 by A1, A2, A3, Th32; ::_thesis: ( F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso )
thus F1 is_transformable_to F2 by A1, FUNCTOR2:def_6; ::_thesis: ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso
take f ; ::_thesis: for a being object of A holds f ! a is iso
thus for a being object of A holds f ! a is iso by A4; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines are_naturally_equivalent FUNCTOR3:def_4_:_
for A, B being category
for F1, F2 being covariant Functor of A,B holds
( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso ) );
definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
assume A1: F1,F2 are_naturally_equivalent ;
mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :Def5: :: FUNCTOR3:def 5
for a being object of A holds it ! a is iso ;
existence
ex b1 being natural_transformation of F1,F2 st
for a being object of A holds b1 ! a is iso by A1, Def4;
end;
:: deftheorem Def5 defines natural_equivalence FUNCTOR3:def_5_:_
for A, B being category
for F1, F2 being covariant Functor of A,B st F1,F2 are_naturally_equivalent holds
for b5 being natural_transformation of F1,F2 holds
( b5 is natural_equivalence of F1,F2 iff for a being object of A holds b5 ! a is iso );
theorem Th33: :: FUNCTOR3:33
for A, B being category
for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
F1,F3 are_naturally_equivalent
proof
let A, B be category; ::_thesis: for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
F1,F3 are_naturally_equivalent
let F1, F2, F3 be covariant Functor of A,B; ::_thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies F1,F3 are_naturally_equivalent )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1 ; :: according to FUNCTOR3:def_4 ::_thesis: ( for t being natural_transformation of F1,F2 holds
not for a being object of A holds t ! a is iso or not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )
given t being natural_transformation of F1,F2 such that A3: for a being object of A holds t ! a is iso ; ::_thesis: ( not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )
assume that
A4: F2 is_naturally_transformable_to F3 and
A5: F3 is_transformable_to F2 ; :: according to FUNCTOR3:def_4 ::_thesis: ( for t being natural_transformation of F2,F3 holds
not for a being object of A holds t ! a is iso or F1,F3 are_naturally_equivalent )
given t1 being natural_transformation of F2,F3 such that A6: for a being object of A holds t1 ! a is iso ; ::_thesis: F1,F3 are_naturally_equivalent
thus ( F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 ) by A1, A2, A4, A5, FUNCTOR2:2, FUNCTOR2:8; :: according to FUNCTOR3:def_4 ::_thesis: ex t being natural_transformation of F1,F3 st
for a being object of A holds t ! a is iso
take t1 `*` t ; ::_thesis: for a being object of A holds (t1 `*` t) ! a is iso
let a be object of A; ::_thesis: (t1 `*` t) ! a is iso
A7: t1 ! a is iso by A6;
F3 is_transformable_to F1 by A2, A5, FUNCTOR2:2;
then A8: <^(F3 . a),(F1 . a)^> <> {} by FUNCTOR2:def_1;
A9: t ! a is iso by A3;
A10: F2 is_transformable_to F3 by A4, FUNCTOR2:def_6;
then A11: <^(F2 . a),(F3 . a)^> <> {} by FUNCTOR2:def_1;
A12: F1 is_transformable_to F2 by A1, FUNCTOR2:def_6;
then A13: <^(F1 . a),(F2 . a)^> <> {} by FUNCTOR2:def_1;
(t1 `*` t) ! a = (t1 `*` t) ! a by A1, A4, FUNCTOR2:def_8
.= (t1 ! a) * (t ! a) by A12, A10, FUNCTOR2:def_5 ;
hence (t1 `*` t) ! a is iso by A13, A11, A8, A7, A9, ALTCAT_3:7; ::_thesis: verum
end;
theorem Th34: :: FUNCTOR3:34
for A, B being category
for F1, F2, F3 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3
proof
let A, B be category; ::_thesis: for F1, F2, F3 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3
let F1, F2, F3 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3
let e be natural_equivalence of F1,F2; ::_thesis: for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3
let e1 be natural_equivalence of F2,F3; ::_thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies e1 `*` e is natural_equivalence of F1,F3 )
assume that
A1: F1,F2 are_naturally_equivalent and
A2: F2,F3 are_naturally_equivalent ; ::_thesis: e1 `*` e is natural_equivalence of F1,F3
thus A3: F1,F3 are_naturally_equivalent by A1, A2, Th33; :: according to FUNCTOR3:def_5 ::_thesis: for a being object of A holds (e1 `*` e) ! a is iso
let a be object of A; ::_thesis: (e1 `*` e) ! a is iso
A4: F1 is_transformable_to F2 by A1, Def4;
then A5: <^(F1 . a),(F2 . a)^> <> {} by FUNCTOR2:def_1;
F3 is_transformable_to F1 by A3, Def4;
then A6: <^(F3 . a),(F1 . a)^> <> {} by FUNCTOR2:def_1;
A7: F2 is_transformable_to F3 by A2, Def4;
then A8: <^(F2 . a),(F3 . a)^> <> {} by FUNCTOR2:def_1;
( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A1, A2, Def4;
then A9: (e1 `*` e) ! a = (e1 `*` e) ! a by FUNCTOR2:def_8
.= (e1 ! a) * (e ! a) by A4, A7, FUNCTOR2:def_5 ;
( e1 ! a is iso & e ! a is iso ) by A1, A2, Def5;
hence (e1 `*` e) ! a is iso by A9, A5, A8, A6, ALTCAT_3:7; ::_thesis: verum
end;
theorem Th35: :: FUNCTOR3:35
for C, A, B being category
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
proof
let C, A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
let G1 be covariant Functor of B,C; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) )
assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
then A2: F2 is_transformable_to F1 by Def4;
A3: F1 is_naturally_transformable_to F2 by A1, Def4;
then reconsider k = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;
A4: F1 is_transformable_to F2 by A1, Def4;
A5: now__::_thesis:_for_a_being_object_of_A_holds_k_!_a_is_iso
let a be object of A; ::_thesis: k ! a is iso
A6: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33;
A7: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def_1;
( k ! a = G1 . (e ! a) & <^(F1 . a),(F2 . a)^> <> {} ) by A4, Th11, FUNCTOR2:def_1;
hence k ! a is iso by A1, A6, A7, Def5, ALTCAT_4:20; ::_thesis: verum
end;
G1 * F1,G1 * F2 are_naturally_equivalent
proof
thus G1 * F1 is_naturally_transformable_to G1 * F2 by A3, Lm2; :: according to FUNCTOR3:def_4 ::_thesis: ( G1 * F2 is_transformable_to G1 * F1 & ex t being natural_transformation of G1 * F1,G1 * F2 st
for a being object of A holds t ! a is iso )
thus G1 * F2 is_transformable_to G1 * F1 by A2, Th10; ::_thesis: ex t being natural_transformation of G1 * F1,G1 * F2 st
for a being object of A holds t ! a is iso
take k ; ::_thesis: for a being object of A holds k ! a is iso
let a be object of A; ::_thesis: k ! a is iso
thus k ! a is iso by A5; ::_thesis: verum
end;
hence ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A5, Def5; ::_thesis: verum
end;
theorem Th36: :: FUNCTOR3:36
for A, B, C being category
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
proof
let A, B, C be category; ::_thesis: for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
let G1, G2 be covariant Functor of B,C; ::_thesis: for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
let f be natural_equivalence of G1,G2; ::_thesis: ( G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) )
assume A1: G1,G2 are_naturally_equivalent ; ::_thesis: ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
then A2: G1 is_naturally_transformable_to G2 by Def4;
then reconsider k = f * F1 as natural_transformation of G1 * F1,G2 * F1 by Th29;
A3: now__::_thesis:_for_a_being_object_of_A_holds_k_!_a_is_iso
let a be object of A; ::_thesis: k ! a is iso
G1 is_transformable_to G2 by A1, Def4;
then A4: k ! a = f ! (F1 . a) by Th12;
( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33;
hence k ! a is iso by A1, A4, Def5; ::_thesis: verum
end;
G1 * F1,G2 * F1 are_naturally_equivalent
proof
thus G1 * F1 is_naturally_transformable_to G2 * F1 by A2, Lm2; :: according to FUNCTOR3:def_4 ::_thesis: ( G2 * F1 is_transformable_to G1 * F1 & ex t being natural_transformation of G1 * F1,G2 * F1 st
for a being object of A holds t ! a is iso )
G2 is_transformable_to G1 by A1, Def4;
hence G2 * F1 is_transformable_to G1 * F1 by Th10; ::_thesis: ex t being natural_transformation of G1 * F1,G2 * F1 st
for a being object of A holds t ! a is iso
take k ; ::_thesis: for a being object of A holds k ! a is iso
let a be object of A; ::_thesis: k ! a is iso
thus k ! a is iso by A3; ::_thesis: verum
end;
hence ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) by A3, Def5; ::_thesis: verum
end;
theorem :: FUNCTOR3:37
for A, B, C being category
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
proof
let A, B, C be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let G1, G2 be covariant Functor of B,C; ::_thesis: for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let e be natural_equivalence of F1,F2; ::_thesis: for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let f be natural_equivalence of G1,G2; ::_thesis: ( F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) )
assume that
A1: F1,F2 are_naturally_equivalent and
A2: G1,G2 are_naturally_equivalent ; ::_thesis: ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
A3: G1 * F1,G1 * F2 are_naturally_equivalent by A1, Th35;
then A4: G1 * F1 is_naturally_transformable_to G1 * F2 by Def4;
G1 is_naturally_transformable_to G2 by A2, Def4;
then reconsider sF2 = f * F2 as natural_transformation of G1 * F2,G2 * F2 by Th29;
F1 is_naturally_transformable_to F2 by A1, Def4;
then reconsider G1t = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;
A5: G1 * F2,G2 * F2 are_naturally_equivalent by A2, Th36;
then A6: G1 * F2 is_naturally_transformable_to G2 * F2 by Def4;
( f * F2 is natural_equivalence of G1 * F2,G2 * F2 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A1, A2, Th35, Th36;
then sF2 `*` G1t is natural_equivalence of G1 * F1,G2 * F2 by A5, A3, Th34;
hence ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) by A5, A3, A6, A4, Th33, FUNCTOR2:def_8; ::_thesis: verum
end;
definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
let e be natural_equivalence of F1,F2;
assume B1: F1,F2 are_naturally_equivalent ;
funce " -> natural_equivalence of F2,F1 means :Def6: :: FUNCTOR3:def 6
for a being object of A holds it . a = (e ! a) " ;
existence
ex b1 being natural_equivalence of F2,F1 st
for a being object of A holds b1 . a = (e ! a) "
proof
A1: for a being object of A holds e ! a is iso by B1, Def5;
( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 ) by B1, Def4;
then consider f being natural_transformation of F2,F1 such that
A2: for a being object of A holds
( f . a = (e ! a) " & f ! a is iso ) by A1, Th32;
f is natural_equivalence of F2,F1
proof
thus F2,F1 are_naturally_equivalent by B1; :: according to FUNCTOR3:def_5 ::_thesis: for a being object of A holds f ! a is iso
let a be object of A; ::_thesis: f ! a is iso
thus f ! a is iso by A2; ::_thesis: verum
end;
then reconsider f = f as natural_equivalence of F2,F1 ;
take f ; ::_thesis: for a being object of A holds f . a = (e ! a) "
let a be object of A; ::_thesis: f . a = (e ! a) "
thus f . a = (e ! a) " by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being natural_equivalence of F2,F1 st ( for a being object of A holds b1 . a = (e ! a) " ) & ( for a being object of A holds b2 . a = (e ! a) " ) holds
b1 = b2
proof
let P, R be natural_equivalence of F2,F1; ::_thesis: ( ( for a being object of A holds P . a = (e ! a) " ) & ( for a being object of A holds R . a = (e ! a) " ) implies P = R )
assume that
A3: for a being object of A holds P . a = (e ! a) " and
A4: for a being object of A holds R . a = (e ! a) " ; ::_thesis: P = R
A5: F2 is_transformable_to F1 by B1, Def4;
now__::_thesis:_for_a_being_object_of_A_holds_P_!_a_=_R_!_a
let a be object of A; ::_thesis: P ! a = R ! a
thus P ! a = P . a by A5, FUNCTOR2:def_4
.= (e ! a) " by A3
.= R . a by A4
.= R ! a by A5, FUNCTOR2:def_4 ; ::_thesis: verum
end;
hence P = R by A5, FUNCTOR2:3; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines " FUNCTOR3:def_6_:_
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
for b6 being natural_equivalence of F2,F1 holds
( b6 = e " iff for a being object of A holds b6 . a = (e ! a) " );
theorem Th38: :: FUNCTOR3:38
for B, A being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for o being object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
proof
let B, A be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for o being object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2
for o being object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let e be natural_equivalence of F1,F2; ::_thesis: for o being object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let o be object of A; ::_thesis: ( F1,F2 are_naturally_equivalent implies (e ") ! o = (e ! o) " )
assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: (e ") ! o = (e ! o) "
then F2 is_transformable_to F1 by Def4;
hence (e ") ! o = (e ") . o by FUNCTOR2:def_4
.= (e ! o) " by A1, Def6 ;
::_thesis: verum
end;
theorem Th39: :: FUNCTOR3:39
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
e `*` (e ") = idt F2
proof
let A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
e `*` (e ") = idt F2
let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
e `*` (e ") = idt F2
let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies e `*` (e ") = idt F2 )
assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: e `*` (e ") = idt F2
then A2: ( F1 is_transformable_to F2 & F2 is_transformable_to F1 ) by Def4;
A3: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A1, Def4;
now__::_thesis:_for_a_being_object_of_A_holds_(e_`*`_(e_"))_!_a_=_(idt_F2)_!_a
let a be object of A; ::_thesis: (e `*` (e ")) ! a = (idt F2) ! a
A4: e ! a is iso by A1, Def5;
thus (e `*` (e ")) ! a = (e `*` (e ")) ! a by A3, FUNCTOR2:def_8
.= (e ! a) * ((e ") ! a) by A2, FUNCTOR2:def_5
.= (e ! a) * ((e ! a) ") by A1, Th38
.= idm (F2 . a) by A4, ALTCAT_3:def_5
.= (idt F2) ! a by FUNCTOR2:4 ; ::_thesis: verum
end;
hence e `*` (e ") = idt F2 by FUNCTOR2:3; ::_thesis: verum
end;
theorem :: FUNCTOR3:40
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") `*` e = idt F1
proof
let A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") `*` e = idt F1
let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") `*` e = idt F1
let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies (e ") `*` e = idt F1 )
assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: (e ") `*` e = idt F1
then A2: ( F1 is_transformable_to F2 & F2 is_transformable_to F1 ) by Def4;
A3: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A1, Def4;
now__::_thesis:_for_a_being_object_of_A_holds_((e_")_`*`_e)_!_a_=_(idt_F1)_!_a
let a be object of A; ::_thesis: ((e ") `*` e) ! a = (idt F1) ! a
A4: e ! a is iso by A1, Def5;
thus ((e ") `*` e) ! a = ((e ") `*` e) ! a by A3, FUNCTOR2:def_8
.= ((e ") ! a) * (e ! a) by A2, FUNCTOR2:def_5
.= ((e ! a) ") * (e ! a) by A1, Th38
.= idm (F1 . a) by A4, ALTCAT_3:def_5
.= (idt F1) ! a by FUNCTOR2:4 ; ::_thesis: verum
end;
hence (e ") `*` e = idt F1 by FUNCTOR2:3; ::_thesis: verum
end;
definition
let A, B be category;
let F be covariant Functor of A,B;
:: original: idt
redefine func idt F -> natural_equivalence of F,F;
coherence
idt F is natural_equivalence of F,F
proof
set e = the natural_equivalence of F,F;
the natural_equivalence of F,F `*` ( the natural_equivalence of F,F ") = idt F by Th39;
hence idt F is natural_equivalence of F,F by Th34; ::_thesis: verum
end;
end;
theorem :: FUNCTOR3:41
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") " = e
proof
let A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") " = e
let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") " = e
let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies (e ") " = e )
assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: (e ") " = e
then A2: F1 is_transformable_to F2 by Def4;
now__::_thesis:_for_a_being_object_of_A_holds_((e_")_")_!_a_=_e_!_a
let a be object of A; ::_thesis: ((e ") ") ! a = e ! a
A3: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1;
F2 is_transformable_to F1 by A1, Def4;
then A4: <^(F2 . a),(F1 . a)^> <> {} by FUNCTOR2:def_1;
e ! a is iso by A1, Def5;
then A5: ( e ! a is retraction & e ! a is coretraction ) by ALTCAT_3:5;
thus ((e ") ") ! a = ((e ") ! a) " by A1, Th38
.= ((e ! a) ") " by A1, Th38
.= e ! a by A3, A4, A5, ALTCAT_3:3 ; ::_thesis: verum
end;
hence (e ") " = e by A2, FUNCTOR2:3; ::_thesis: verum
end;
theorem :: FUNCTOR3:42
for A, B being category
for F1, F3, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3
for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")
proof
let A, B be category; ::_thesis: for F1, F3, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3
for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")
let F1, F3, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3
for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")
let e be natural_equivalence of F1,F2; ::_thesis: for e1 being natural_equivalence of F2,F3
for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")
let e1 be natural_equivalence of F2,F3; ::_thesis: for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")
let k be natural_equivalence of F1,F3; ::_thesis: ( k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies k " = (e ") `*` (e1 ") )
assume that
A1: k = e1 `*` e and
A2: F1,F2 are_naturally_equivalent and
A3: F2,F3 are_naturally_equivalent ; ::_thesis: k " = (e ") `*` (e1 ")
A4: ( F3 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A2, A3, Def4;
A5: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A2, A3, Def4;
A6: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A2, A3, Def4;
A7: ( F3 is_transformable_to F2 & F2 is_transformable_to F1 ) by A2, A3, Def4;
then A8: F3 is_transformable_to F1 by FUNCTOR2:2;
now__::_thesis:_for_a_being_object_of_A_holds_(k_")_!_a_=_((e_")_`*`_(e1_"))_!_a
let a be object of A; ::_thesis: (k ") ! a = ((e ") `*` (e1 ")) ! a
A9: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A5, FUNCTOR2:def_1;
A10: <^(F3 . a),(F1 . a)^> <> {} by A8, FUNCTOR2:def_1;
A11: ( e ! a is iso & e1 ! a is iso ) by A2, A3, Def5;
thus (k ") ! a = ((e1 `*` e) ! a) " by A1, A2, A3, Th33, Th38
.= ((e1 `*` e) ! a) " by A6, FUNCTOR2:def_8
.= ((e1 ! a) * (e ! a)) " by A5, FUNCTOR2:def_5
.= ((e ! a) ") * ((e1 ! a) ") by A11, A9, A10, ALTCAT_3:7
.= ((e ! a) ") * ((e1 ") ! a) by A3, Th38
.= ((e ") ! a) * ((e1 ") ! a) by A2, Th38
.= ((e ") `*` (e1 ")) ! a by A7, FUNCTOR2:def_5
.= ((e ") `*` (e1 ")) ! a by A4, FUNCTOR2:def_8 ; ::_thesis: verum
end;
hence k " = (e ") `*` (e1 ") by A7, FUNCTOR2:2, FUNCTOR2:3; ::_thesis: verum
end;
theorem :: FUNCTOR3:43
for A, B being category
for F1 being covariant Functor of A,B holds (idt F1) " = idt F1
proof
let A, B be category; ::_thesis: for F1 being covariant Functor of A,B holds (idt F1) " = idt F1
let F1 be covariant Functor of A,B; ::_thesis: (idt F1) " = idt F1
now__::_thesis:_for_a_being_object_of_A_holds_((idt_F1)_")_!_a_=_(idt_F1)_!_a
let a be object of A; ::_thesis: ((idt F1) ") ! a = (idt F1) ! a
thus ((idt F1) ") ! a = ((idt F1) ! a) " by Th38
.= (idm (F1 . a)) " by FUNCTOR2:4
.= idm (F1 . a) by ALTCAT_3:4
.= (idt F1) ! a by FUNCTOR2:4 ; ::_thesis: verum
end;
hence (idt F1) " = idt F1 by FUNCTOR2:3; ::_thesis: verum
end;