:: ALTCAT_3 semantic presentation
:: deftheorem E1 defines is_left_inverse_of ALTCAT_3:def 1 :
:: deftheorem E2 defines retraction ALTCAT_3:def 2 :
:: deftheorem E3 defines coretraction ALTCAT_3:def 3 :
theorem E4: :: ALTCAT_3:1
definition
let c
1 be
category;
let c
2, c
3 be
object of c
1;
assume E5:
(
<^c2,c3^> <> {} &
<^c3,c2^> <> {} )
;
let c
4 be
Morphism of c
2,c
3;
assume E6:
( c
4 is
retraction & c
4 is
coretraction )
;
func a
4 " -> Morphism of a
3,a
2 means :
E5:
:: ALTCAT_3:def 4
( a
5 is_left_inverse_of a
4 & a
5 is_right_inverse_of a
4 );
existence
ex b1 being Morphism of c3,c2 st
( b1 is_left_inverse_of c4 & b1 is_right_inverse_of c4 )
proof
consider c
5 being
Morphism of c
3,c
2 such that
E7:
c
5 is_right_inverse_of c
4
by E6, E2;
consider c
6 being
Morphism of c
3,c
2 such that
E8:
c
6 is_left_inverse_of c
4
by E6, E3;
E9: c
5 =
(idm c2) * c
5
by E5, ALTCAT_1:24
.=
(c6 * c4) * c
5
by E8, E1
.=
c
6 * (c4 * c5)
by E5, ALTCAT_1:25
.=
c
6 * (idm c3)
by E7, E1
.=
c
6
by E5, ALTCAT_1:def 19
;
take
c
5
;
thus
( c
5 is_left_inverse_of c
4 & c
5 is_right_inverse_of c
4 )
by E7, E8, E9;
end;
uniqueness
for b1, b2 being Morphism of c3,c2 holds
( ( b1 is_left_inverse_of c4 & b1 is_right_inverse_of c4 & b2 is_left_inverse_of c4 & b2 is_right_inverse_of c4 ) implies ( b1 = b2 ) )
end;
:: deftheorem E5 defines " ALTCAT_3:def 4 :
theorem E6: :: ALTCAT_3:2
theorem E7: :: ALTCAT_3:3
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
assume E8:
(
<^c2,c3^> <> {} &
<^c3,c2^> <> {} )
;
let c
4 be
Morphism of c
2,c
3;
assume
( c
4 is
retraction & c
4 is
coretraction )
;
then E9:
( c
4 " is_left_inverse_of c
4 & c
4 " is_right_inverse_of c
4 )
by E8, E5;
then
( c
4 " is
retraction & c
4 " is
coretraction )
by E2, E3;
then E10:
(c4 " ) " is_right_inverse_of c
4 "
by E8, E5;
thus (c4 " ) " =
(idm c3) * ((c4 " ) " )
by E8, ALTCAT_1:24
.=
(c4 * (c4 " )) * ((c4 " ) " )
by E9, E1
.=
c
4 * ((c4 " ) * ((c4 " ) " ))
by E8, ALTCAT_1:25
.=
c
4 * (idm c2)
by E10, E1
.=
c
4
by E8, ALTCAT_1:def 19
;
end;
theorem E8: :: ALTCAT_3:4
:: deftheorem E9 defines iso ALTCAT_3:def 5 :
theorem E10: :: ALTCAT_3:5
theorem E11: :: ALTCAT_3:6
theorem E12: :: ALTCAT_3:7
proof
let c
1 be
category;
let c
2, c
3, c
4 be
object of c
1;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
assume E13:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} &
<^c4,c2^> <> {} )
;
then E14:
(
<^c3,c2^> <> {} &
<^c4,c3^> <> {} &
<^c2,c4^> <> {} )
by ALTCAT_1:def 4;
assume
( c
5 is
iso & c
6 is
iso )
;
then E15:
( c
5 is
retraction & c
5 is
coretraction & c
6 is
retraction & c
6 is
coretraction )
by E13, E14, E11;
consider c
7 being
Morphism of c
3,c
2 such that
E16:
c
7 = c
5 "
;
consider c
8 being
Morphism of c
4,c
3 such that
E17:
c
8 = c
6 "
;
E18:
(c7 * c8) * (c6 * c5) =
c
7 * (c8 * (c6 * c5))
by E14, ALTCAT_1:25
.=
c
7 * ((c8 * c6) * c5)
by E13, E14, ALTCAT_1:25
.=
c
7 * ((idm c3) * c5)
by E13, E14, E15, E17, E6
.=
c
7 * c
5
by E13, ALTCAT_1:24
.=
idm c
2
by E13, E14, E15, E16, E6
;
then E19:
c
7 * c
8 is_left_inverse_of c
6 * c
5
by E1;
then E20:
c
6 * c
5 is
coretraction
by E3;
E21:
(c6 * c5) * (c7 * c8) =
c
6 * (c5 * (c7 * c8))
by E13, ALTCAT_1:25
.=
c
6 * ((c5 * c7) * c8)
by E13, E14, ALTCAT_1:25
.=
c
6 * ((idm c3) * c8)
by E13, E14, E15, E16, E6
.=
c
6 * c
8
by E14, ALTCAT_1:24
.=
idm c
4
by E13, E14, E15, E17, E6
;
then E22:
c
7 * c
8 is_right_inverse_of c
6 * c
5
by E1;
then
c
6 * c
5 is
retraction
by E2;
then
c
7 * c
8 = (c6 * c5) "
by E13, E14, E19, E20, E22, E5;
hence
( c
6 * c
5 is
iso &
(c6 * c5) " = (c5 " ) * (c6 " ) )
by E16, E17, E18, E21, E9;
end;
definition
let c
1 be
category;
let c
2, c
3 be
object of c
1;
pred a
2,a
3 are_iso means :
E13:
:: ALTCAT_3:def 6
(
<^a2,a3^> <> {} &
<^a3,a2^> <> {} & ex b
1 being
Morphism of a
2,a
3 st b
1 is
iso );
reflexivity
for b1 being object of c1 holds
( <^b1,b1^> <> {} & <^b1,b1^> <> {} & ex b2 being Morphism of b1,b1 st b2 is iso )
symmetry
for b1, b2 being object of c1 holds
( ( ) implies ( not <^b1,b2^> <> {} or not <^b2,b1^> <> {} or for b3 being Morphism of b1,b2 holds
not b3 is iso or ( <^b2,b1^> <> {} & <^b1,b2^> <> {} & ex b3 being Morphism of b2,b1 st b3 is iso ) ) )
proof
let c
4, c
5 be
object of c
1;
assume that
E13:
(
<^c4,c5^> <> {} &
<^c5,c4^> <> {} )
and
E14:
ex b
1 being
Morphism of c
4,c
5 st b
1 is
iso
;
consider c
6 being
Morphism of c
4,c
5 such that
E15:
c
6 is
iso
by E14;
E16:
( c
6 is
retraction & c
6 is
coretraction )
by E15, E10;
thus
(
<^c5,c4^> <> {} &
<^c4,c5^> <> {} )
by E13;
take c
7 = c
6 " ;
E17: c
7 * (c7 " ) =
(c6 " ) * c
6
by E13, E16, E7
.=
idm c
4
by E13, E16, E6
;
(c7 " ) * c
7 =
c
6 * (c6 " )
by E13, E16, E7
.=
idm c
5
by E13, E16, E6
;
hence
c
7 is
iso
by E17, E9;
end;
end;
:: deftheorem E13 defines are_iso ALTCAT_3:def 6 :
theorem :: ALTCAT_3:8
proof
let c
1 be
category;
let c
2, c
3, c
4 be
object of c
1;
assume that
E14:
c
2,c
3 are_iso
and
E15:
c
3,c
4 are_iso
;
E16:
(
<^c2,c3^> <> {} &
<^c3,c2^> <> {} &
<^c3,c4^> <> {} &
<^c4,c3^> <> {} )
by E14, E15, E13;
hence E17:
(
<^c2,c4^> <> {} &
<^c4,c2^> <> {} )
by ALTCAT_1:def 4;
:: uses ALTCAT_3:def 6
consider c
5 being
Morphism of c
2,c
3 such that
E18:
c
5 is
iso
by E14, E13;
consider c
6 being
Morphism of c
3,c
4 such that
E19:
c
6 is
iso
by E15, E13;
take
c
6 * c
5
;
thus
c
6 * c
5 is
iso
by E16, E17, E18, E19, E12;
end;
:: deftheorem E14 defines mono ALTCAT_3:def 7 :
:: deftheorem E15 defines epi ALTCAT_3:def 8 :
theorem E16: :: ALTCAT_3:9
proof
let c
1 be non
empty transitive associative AltCatStr ;
let c
2, c
3, c
4 be
object of c
1;
assume E17:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} )
;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
assume E18:
( c
5 is
mono & c
6 is
mono )
;
let c
7 be
object of c
1;
:: uses ALTCAT_3:def 7
assume E19:
<^c7,c2^> <> {}
;
let c
8, c
9 be
Morphism of c
7,c
2;
assume E20:
(c6 * c5) * c
8 = (c6 * c5) * c
9
;
E21:
(c6 * c5) * c
8 = c
6 * (c5 * c8)
by E17, E19, ALTCAT_1:25;
E22:
(c6 * c5) * c
9 = c
6 * (c5 * c9)
by E17, E19, ALTCAT_1:25;
<^c7,c3^> <> {}
by E17, E19, ALTCAT_1:def 4;
then
c
5 * c
8 = c
5 * c
9
by E18, E20, E21, E22, E14;
hence
c
8 = c
9
by E18, E19, E14;
end;
theorem E17: :: ALTCAT_3:10
proof
let c
1 be non
empty transitive associative AltCatStr ;
let c
2, c
3, c
4 be
object of c
1;
assume E18:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} )
;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
assume E19:
( c
5 is
epi & c
6 is
epi )
;
let c
7 be
object of c
1;
:: uses ALTCAT_3:def 8
assume E20:
<^c4,c7^> <> {}
;
let c
8, c
9 be
Morphism of c
4,c
7;
assume E21:
c
8 * (c6 * c5) = c
9 * (c6 * c5)
;
E22:
c
8 * (c6 * c5) = (c8 * c6) * c
5
by E18, E20, ALTCAT_1:25;
E23:
c
9 * (c6 * c5) = (c9 * c6) * c
5
by E18, E20, ALTCAT_1:25;
<^c3,c7^> <> {}
by E18, E20, ALTCAT_1:def 4;
then
c
8 * c
6 = c
9 * c
6
by E19, E21, E22, E23, E15;
hence
c
8 = c
9
by E19, E20, E15;
end;
theorem :: ALTCAT_3:11
proof
let c
1 be non
empty transitive associative AltCatStr ;
let c
2, c
3, c
4 be
object of c
1;
assume E18:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} )
;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
assume E19:
c
6 * c
5 is
mono
;
let c
7 be
object of c
1;
:: uses ALTCAT_3:def 7
assume E20:
<^c7,c2^> <> {}
;
let c
8, c
9 be
Morphism of c
7,c
2;
assume E21:
c
5 * c
8 = c
5 * c
9
;
E22:
(c6 * c5) * c
8 = c
6 * (c5 * c8)
by E18, E20, ALTCAT_1:25;
(c6 * c5) * c
9 = c
6 * (c5 * c9)
by E18, E20, ALTCAT_1:25;
hence
c
8 = c
9
by E19, E20, E21, E22, E14;
end;
theorem :: ALTCAT_3:12
proof
let c
1 be non
empty transitive associative AltCatStr ;
let c
2, c
3, c
4 be
object of c
1;
assume E18:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} )
;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
assume E19:
c
6 * c
5 is
epi
;
let c
7 be
object of c
1;
:: uses ALTCAT_3:def 8
assume E20:
<^c4,c7^> <> {}
;
let c
8, c
9 be
Morphism of c
4,c
7;
assume E21:
c
8 * c
6 = c
9 * c
6
;
E22:
(c8 * c6) * c
5 = c
8 * (c6 * c5)
by E18, E20, ALTCAT_1:25;
(c9 * c6) * c
5 = c
9 * (c6 * c5)
by E18, E20, ALTCAT_1:25;
hence
c
8 = c
9
by E19, E20, E21, E22, E15;
end;
theorem :: ALTCAT_3:13
proof
let c
1 be non
empty set ;
let c
2, c
3 be
object of
(EnsCat c1);
assume E19:
<^c2,c3^> <> {}
;
let c
4 be
Morphism of c
2,c
3;
let c
5 be
Function of c
2,c
3;
assume E20:
c
5 = c
4
;
per cases
not ( not c
3 <> {} & not c
3 = {} )
;
suppose
c
3 <> {}
;
then E21:
dom c
5 = c
2
by FUNCT_2:def 1;
thus
( c
4 is
mono implies c
5 is
one-to-one )
proof
assume E22:
c
4 is
mono
;
assume
not c
5 is
one-to-one
;
then consider c
6, c
7 being
set such that
E23:
( c
6 in dom c
5 & c
7 in dom c
5 )
and
E24:
c
5 . c
6 = c
5 . c
7
and
E25:
c
6 <> c
7
by FUNCT_1:def 8;
set c
8 = c
2;
E26:
<^c2,c2^> <> {}
by ALTCAT_1:23;
set c
9 = c
2 --> c
6;
E27:
dom (c2 --> c6) = c
2
by FUNCOP_1:19;
E28:
for b
1 being
set holds
( b
1 in c
2 implies
(c2 --> c6) . b
1 = c
6 )
by FUNCOP_1:13;
set c
10 = c
2 --> c
7;
E29:
dom (c2 --> c7) = c
2
by FUNCOP_1:19;
E30:
for b
1 being
set holds
( b
1 in c
2 implies
(c2 --> c7) . b
1 = c
7 )
by FUNCOP_1:13;
consider c
11 being
Element of c
2;
(c2 --> c6) . c
11 = c
6
by E21, E23, E28;
then E31:
(c2 --> c6) . c
11 <> (c2 --> c7) . c
11
by E21, E23, E25, E30;
E32:
rng (c2 --> c6) c= c
2
then
c
2 --> c
6 in Funcs c
2,c
2
by E27, FUNCT_2:def 2;
then reconsider c
12 = c
2 --> c
6 as
Morphism of c
2,c
2 by ALTCAT_1:def 16;
E33:
rng (c2 --> c7) c= c
2
then
c
2 --> c
7 in Funcs c
2,c
2
by E29, FUNCT_2:def 2;
then reconsider c
13 = c
2 --> c
7 as
Morphism of c
2,c
2 by ALTCAT_1:def 16;
E34:
dom ((c2 --> c6) * c5) = c
2
by E21, E27, E32, RELAT_1:46;
E35:
dom ((c2 --> c7) * c5) = c
2
by E21, E29, E33, RELAT_1:46;
now
let c
14 be
set ;
assume E36:
c
14 in c
2
;
hence ((c2 --> c6) * c5) . c
14 =
c
5 . ((c2 --> c6) . c14)
by E34, FUNCT_1:22
.=
c
5 . c
7
by E24, E28, E36
.=
c
5 . ((c2 --> c7) . c14)
by E30, E36
.=
((c2 --> c7) * c5) . c
14
by E35, E36, FUNCT_1:22
;
end;
then
(c2 --> c6) * c
5 = (c2 --> c7) * c
5
by E34, E35, FUNCT_1:9;
then c
4 * c
12 =
(c2 --> c7) * c
5
by E19, E20, E26, ALTCAT_1:18
.=
c
4 * c
13
by E19, E20, E26, ALTCAT_1:18
;
hence
not verum
by E22, E26, E31, E14;
end;
thus
( c
5 is
one-to-one implies c
4 is
mono )
proof
assume E22:
c
5 is
one-to-one
;
let c
6 be
object of
(EnsCat c1);
:: uses ALTCAT_3:def 7
assume E23:
<^c6,c2^> <> {}
;
let c
7, c
8 be
Morphism of c
6,c
2;
assume E24:
c
4 * c
7 = c
4 * c
8
;
E25:
<^c6,c2^> = Funcs c
6,c
2
by ALTCAT_1:def 16;
then consider c
9 being
Function such that
E26:
( c
9 = c
7 &
dom c
9 = c
6 &
rng c
9 c= c
2 )
by E23, FUNCT_2:def 2;
consider c
10 being
Function such that
E27:
( c
10 = c
8 &
dom c
10 = c
6 &
rng c
10 c= c
2 )
by E23, E25, FUNCT_2:def 2;
E28:
<^c6,c3^> <> {}
by E19, E23, ALTCAT_1:def 4;
then E29: c
9 * c
5 =
c
4 * c
8
by E19, E20, E23, E24, E26, ALTCAT_1:18
.=
c
10 * c
5
by E19, E20, E23, E27, E28, ALTCAT_1:18
;
now
let c
11 be
set ;
assume E30:
c
11 in c
6
;
then E31:
( c
9 . c
11 in rng c
9 & c
10 . c
11 in rng c
10 )
by E26, E27, FUNCT_1:def 5;
c
5 . (c9 . c11) = (c9 * c5) . c
11
by E26, E30, FUNCT_1:23;
then
c
5 . (c9 . c11) = c
5 . (c10 . c11)
by E27, E29, E30, FUNCT_1:23;
hence
c
9 . c
11 = c
10 . c
11
by E21, E22, E26, E27, E31, FUNCT_1:def 8;
end;
hence
c
7 = c
8
by E26, E27, FUNCT_1:9;
end;
end;
suppose E21:
c
3 = {}
;
E22:
now
per cases
not ( not c
2 = {} & not c
2 <> {} )
;
end;
thus
( c
4 is
mono implies c
5 is
one-to-one )
thus
( c
5 is
one-to-one implies c
4 is
mono )
proof
assume
c
5 is
one-to-one
;
let c
6 be
object of
(EnsCat c1);
:: uses ALTCAT_3:def 7
assume E23:
<^c6,c2^> <> {}
;
let c
7, c
8 be
Morphism of c
6,c
2;
assume
c
4 * c
7 = c
4 * c
8
;
E24:
<^c6,c2^> = Funcs c
6,c
2
by ALTCAT_1:def 16;
then consider c
9 being
Function such that
E25:
( c
9 = c
7 &
dom c
9 = c
6 &
rng c
9 c= c
2 )
by E23, FUNCT_2:def 2;
consider c
10 being
Function such that
E26:
( c
10 = c
8 &
dom c
10 = c
6 &
rng c
10 c= c
2 )
by E23, E24, FUNCT_2:def 2;
E27:
<^c2,c3^> = Funcs c
2,c
3
by ALTCAT_1:def 16;
consider c
11 being
Element of
Funcs c
2,c
3;
consider c
12 being
Function such that
E28:
( c
12 = c
11 &
dom c
12 = c
2 &
rng c
12 c= c
3 )
by E19, E27, FUNCT_2:def 2;
rng c
12 = {}
by E21, E28, XBOOLE_1:3;
then
dom c
12 = {}
by RELAT_1:65;
then E29:
rng c
9 = {}
by E25, E28, XBOOLE_1:3;
then E30:
dom c
9 = {}
by RELAT_1:65;
c
9 =
{}
by E29, RELAT_1:64
.=
c
10
by E25, E26, E30, RELAT_1:64
;
hence
c
7 = c
8
by E25, E26;
end;
end;
end;
end;
theorem :: ALTCAT_3:14
proof
let c
1 be non
empty with_non-empty_elements set ;
let c
2, c
3 be
object of
(EnsCat c1);
assume E19:
<^c2,c3^> <> {}
;
let c
4 be
Morphism of c
2,c
3;
let c
5 be
Function of c
2,c
3;
assume E20:
c
5 = c
4
;
per cases
not ( ex b
1 being
set st
( b
1 in c
1 & not b
1 is
trivial ) & for b
1 being
set holds
not ( b
1 in c
1 & not b
1 is
trivial ) )
;
suppose E21:
for b
1 being
set holds
( b
1 in c
1 implies b
1 is
trivial )
;
thus
( c
4 is
epi implies c
5 is
onto )
proof
assume
c
4 is
epi
;
now
per cases
not ( not c
3 = {} & not c
3 <> {} )
;
suppose E22:
c
3 = {}
;
end;
suppose E22:
c
3 <> {}
;
end;
end;
hence
c
5 is
onto
;
end;
thus
( c
5 is
onto implies c
4 is
epi )
proof
assume E22:
c
5 is
onto
;
let c
6 be
object of
(EnsCat c1);
:: uses ALTCAT_3:def 8
assume E23:
<^c3,c6^> <> {}
;
let c
7, c
8 be
Morphism of c
3,c
6;
assume E24:
c
7 * c
4 = c
8 * c
4
;
E25:
<^c3,c6^> = Funcs c
3,c
6
by ALTCAT_1:def 16;
then consider c
9 being
Function such that
E26:
( c
9 = c
7 &
dom c
9 = c
3 &
rng c
9 c= c
6 )
by E23, FUNCT_2:def 2;
consider c
10 being
Function such that
E27:
( c
10 = c
8 &
dom c
10 = c
3 &
rng c
10 c= c
6 )
by E23, E25, FUNCT_2:def 2;
E28:
<^c2,c6^> <> {}
by E19, E23, ALTCAT_1:def 4;
then E29: c
5 * c
9 =
c
8 * c
4
by E19, E20, E23, E24, E26, ALTCAT_1:18
.=
c
5 * c
10
by E19, E20, E23, E27, E28, ALTCAT_1:18
;
hence
c
7 = c
8
by E26, E27;
end;
end;
suppose E21:
ex b
1 being
set st
( b
1 in c
1 & not b
1 is
trivial )
;
now
per cases
not ( not c
3 <> {} & not c
3 = {} )
;