:: ISOCAT_1 semantic presentation

theorem Th1: :: ISOCAT_1:1

for b₁, b₂ being Function st b₁ is one-to-one & b₂ is one-to-one holds
[:b₁,b₂:] is one-to-one

proof end;

theorem Th2: :: ISOCAT_1:2

for b₁, b₂ being Category holds
( rng (pr1 b₁,b₂) = the Morphisms of b₁ & rng (pr2 b₂,b₁) = the Morphisms of b₁ )

proof end;

theorem Th3: :: ISOCAT_1:3

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁
for b₄ being Morphism of b₂ st b₄ is invertible holds
b₃ . b₄ is invertible

proof end;

theorem Th4: :: ISOCAT_1:4

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Functor of b₂,b₁ holds
( b₃ * (id b₁) = b₃ & (id b₁) * b₄ = b₄ ) by FUNCT_2:23;

theorem Th5: :: ISOCAT_1:5

canceled;

theorem Th6: :: ISOCAT_1:6

canceled;

theorem Th7: :: ISOCAT_1:7

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st b₃ is_transformable_to b₄ holds
for b₅ being transformation of b₃,b₄
for b₆ being Object of b₁ holds b₅ . b₆ in Hom (b₃ . b₆),(b₄ . b₆)

proof end;

theorem Th8: :: ISOCAT_1:8

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₂,b₃ st b₄ is_transformable_to b₅ & b₆ is_transformable_to b₇ holds
b₆ * b₄ is_transformable_to b₇ * b₅

proof end;

theorem Th9: :: ISOCAT_1:9

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st b₃ is_transformable_to b₄ holds
for b₅ being transformation of b₃,b₄ st b₅ is invertible holds
for b₆ being Object of b₁ holds b₃ . b₆,b₄ . b₆ are_isomorphic

proof end;

definition

let c₁, c₂ be Category;
redefine mode Functor of c₁,c₂ -> M6(the Morphisms of a₁,the Morphisms of a₂) means :: ISOCAT_1:def 1
( ( for b₁ being Object of a₁ ex b₂ being Object of a₂ st a₃ . (id b₁) = id b₂ ) & ( for b₁ being Morphism of a₁ holds
( a₃ . (id (dom b₁)) = id (dom (a₃ . b₁)) & a₃ . (id (cod b₁)) = id (cod (a₃ . b₁)) ) ) & ( for b₁, b₂ being Morphism of a₁ st dom b₂ = cod b₁ holds
a₃ . (b₂ * b₁) = (a₃ . b₂) * (a₃ . b₁) ) );
compatibility by CAT_1:96, CAT_1:97, CAT_1:98, CAT_1:99;

end;

:: deftheorem Def1 defines Functor ISOCAT_1:def 1 :

definition

let c₁ be Category;
redefine func id as id c₁ -> Functor of a₁,a₁;
coherence ;
let c₂, c₃ be Category;
let c₄ be Functor of c₁,c₂;
let c₅ be Functor of c₂,c₃;
redefine func * as c₅ * c₄ -> Functor of a₁,a₃;
coherence

proof end;

end;

theorem Th10: :: ISOCAT_1:10

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁ st b₃ is isomorphic holds
for b₄ being Morphism of b₁ ex b₅ being Morphism of b₂ st b₃ . b₅ = b₄

proof end;

theorem Th11: :: ISOCAT_1:11

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁ st b₃ is isomorphic holds
for b₄ being Object of b₁ ex b₅ being Object of b₂ st b₃ . b₅ = b₄

proof end;

theorem Th12: :: ISOCAT_1:12

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ st b₃ is one-to-one holds
Obj b₃ is one-to-one

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
assume E11: c₃ is isomorphic ;
func c₃ " -> Functor of a₂,a₁ equals :Def2: :: ISOCAT_1:def 2
a₃ " ;
coherence

proof end;

end;

:: deftheorem Def2 defines " ISOCAT_1:def 2 :

notation

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
synonym c₃ is_an_isomorphism for isomorphic c₃c₃ is_an_isomorphism is_an_isomorphism ;

end;

definition

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
redefine attr a₃ is isomorphic means :Def3: :: ISOCAT_1:def 3
( a₃ is one-to-one & rng a₃ = the Morphisms of a₂ );
compatibility

proof end;

end;

:: deftheorem Def3 defines is_an_isomorphism ISOCAT_1:def 3 :

theorem Th13: :: ISOCAT_1:13

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ st b₃ is_an_isomorphism holds
b₃ " is_an_isomorphism

proof end;

theorem Th14: :: ISOCAT_1:14

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ st b₃ is_an_isomorphism holds
(Obj b₃) " = Obj (b₃ " )

proof end;

theorem Th15: :: ISOCAT_1:15

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ st b₃ is_an_isomorphism holds
(b₃ " ) " = b₃

proof end;

theorem Th16: :: ISOCAT_1:16

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁ st b₃ is_an_isomorphism holds
( b₃ * (b₃ " ) = id b₁ & (b₃ " ) * b₃ = id b₂ )

proof end;

theorem Th17: :: ISOCAT_1:17

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₂,b₃ st b₄ is_an_isomorphism & b₅ is_an_isomorphism holds
b₅ * b₄ is_an_isomorphism

proof end;

definition

let c₁, c₂ be Category;
pred c₁,c₂ are_isomorphic means :: ISOCAT_1:def 4
ex b₁ being Functor of a₁,a₂ st b₁ is_an_isomorphism ;
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def4 defines are_isomorphic ISOCAT_1:def 4 :

notation

let c₁, c₂ be Category;
synonym c₁ ~= c₂ for c₁,c₂ are_isomorphic ;

end;

theorem Th18: :: ISOCAT_1:18

canceled;

theorem Th19: :: ISOCAT_1:19

canceled;

theorem Th20: :: ISOCAT_1:20

for b₁, b₂, b₃ being Category st b₁ ~= b₂ & b₂ ~= b₃ holds
b₁ ~= b₃

proof end;

theorem Th21: :: ISOCAT_1:21

for b₁ being Category
for b₂, b₃ being set holds [:(1Cat b₂,b₃),b₁:] ~= b₁

proof end;

theorem Th22: :: ISOCAT_1:22

for b₁, b₂ being Category holds [:b₁,b₂:] ~= [:b₂,b₁:]

proof end;

theorem Th23: :: ISOCAT_1:23

for b₁, b₂, b₃ being Category holds [:[:b₁,b₂:],b₃:] ~= [:b₁,[:b₂,b₃:]:]

proof end;

theorem Th24: :: ISOCAT_1:24

for b₁, b₂, b₃, b₄ being Category st b₁ ~= b₂ & b₃ ~= b₄ holds
[:b₁,b₃:] ~= [:b₂,b₄:]

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₁,c₂;
assume E16: c₄ is_transformable_to c₅ ;
let c₆ be transformation of c₄,c₅;
let c₇ be Functor of c₂,c₃;
func c₇ * c₆ -> transformation of a₇ * a₄,a₇ * a₅ equals :Def5: :: ISOCAT_1:def 5
a₇ * a₆;
coherence

proof end;

correctness ;

end;

:: deftheorem Def5 defines * ISOCAT_1:def 5 :

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₂,c₃;
assume E17: c₄ is_transformable_to c₅ ;
let c₆ be Functor of c₁,c₂;
let c₇ be transformation of c₄,c₅;
func c₇ * c₆ -> transformation of a₄ * a₆,a₅ * a₆ equals :Def6: :: ISOCAT_1:def 6
a₇ * (Obj a₆);
coherence

proof end;

correctness ;

end;

:: deftheorem Def6 defines * ISOCAT_1:def 6 :

theorem Th25: :: ISOCAT_1:25

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂ st b₄ is_transformable_to b₅ holds
for b₆ being Functor of b₃,b₁
for b₇ being transformation of b₄,b₅
for b₈ being Object of b₃ holds (b₇ * b₆) . b₈ = b₇ . (b₆ . b₈)

proof end;

theorem Th26: :: ISOCAT_1:26

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂ st b₄ is_transformable_to b₅ holds
for b₆ being transformation of b₄,b₅
for b₇ being Functor of b₂,b₃
for b₈ being Object of b₁ holds (b₇ * b₆) . b₈ = b₇ . (b₆ . b₈)

proof end;

theorem Th27: :: ISOCAT_1:27

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₂,b₃ st b₄ is_naturally_transformable_to b₅ & b₆ is_naturally_transformable_to b₇ holds
b₆ * b₄ is_naturally_transformable_to b₇ * b₅

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₁,c₂;
assume E21: c₄ is_naturally_transformable_to c₅ ;
let c₆ be natural_transformation of c₄,c₅;
let c₇ be Functor of c₂,c₃;
func c₇ * c₆ -> natural_transformation of a₇ * a₄,a₇ * a₅ equals :Def7: :: ISOCAT_1:def 7
a₇ * a₆;
coherence

proof end;

correctness ;

end;

:: deftheorem Def7 defines * ISOCAT_1:def 7 :

theorem Th28: :: ISOCAT_1:28

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂ st b₄ is_naturally_transformable_to b₅ holds
for b₆ being natural_transformation of b₄,b₅
for b₇ being Functor of b₂,b₃
for b₈ being Object of b₁ holds (b₇ * b₆) . b₈ = b₇ . (b₆ . b₈)

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₂,c₃;
assume E23: c₄ is_naturally_transformable_to c₅ ;
let c₆ be Functor of c₁,c₂;
let c₇ be natural_transformation of c₄,c₅;
func c₇ * c₆ -> natural_transformation of a₄ * a₆,a₅ * a₆ equals :Def8: :: ISOCAT_1:def 8
a₇ * a₆;
coherence

proof end;

correctness ;

end;

:: deftheorem Def8 defines * ISOCAT_1:def 8 :

theorem Th29: :: ISOCAT_1:29

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂ st b₄ is_naturally_transformable_to b₅ holds
for b₆ being Functor of b₃,b₁
for b₇ being natural_transformation of b₄,b₅
for b₈ being Object of b₃ holds (b₇ * b₆) . b₈ = b₇ . (b₆ . b₈)

proof end;

theorem Th30: :: ISOCAT_1:30

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₂,b₁ st b₃ is_naturally_transformable_to b₄ holds
for b₅ being Object of b₂ holds Hom (b₃ . b₅),(b₄ . b₅) <> {}

proof end;

theorem Th31: :: ISOCAT_1:31

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₂,b₁ st b₃ is_naturally_transformable_to b₄ holds
for b₅, b₆ being natural_transformation of b₃,b₄ st ( for b₇ being Object of b₂ holds b₅ . b₇ = b₆ . b₇ ) holds
b₅ = b₆

proof end;

theorem Th32: :: ISOCAT_1:32

for b₁, b₂, b₃ being Category
for b₄, b₅, b₆ being Functor of b₂,b₃
for b₇ being Functor of b₃,b₁
for b₈ being natural_transformation of b₄,b₅
for b₉ being natural_transformation of b₅,b₆ st b₄ is_naturally_transformable_to b₅ & b₅ is_naturally_transformable_to b₆ holds
b₇ * (b₉ `*` b₈) = (b₇ * b₉) `*` (b₇ * b₈)

proof end;

theorem Th33: :: ISOCAT_1:33

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅, b₆, b₇ being Functor of b₂,b₃
for b₈ being natural_transformation of b₅,b₆
for b₉ being natural_transformation of b₆,b₇ st b₅ is_naturally_transformable_to b₆ & b₆ is_naturally_transformable_to b₇ holds
(b₉ `*` b₈) * b₄ = (b₉ * b₄) `*` (b₈ * b₄)

proof end;

theorem Th34: :: ISOCAT_1:34

for b₁, b₂, b₃, b₄ being Category
for b₅ being Functor of b₁,b₂
for b₆ being Functor of b₂,b₃
for b₇, b₈ being Functor of b₃,b₄
for b₉ being natural_transformation of b₇,b₈ st b₇ is_naturally_transformable_to b₈ holds
(b₉ * b₆) * b₅ = b₉ * (b₆ * b₅)

proof end;

theorem Th35: :: ISOCAT_1:35

for b₁, b₂, b₃, b₄ being Category
for b₅ being Functor of b₁,b₃
for b₆, b₇ being Functor of b₃,b₄
for b₈ being Functor of b₄,b₂
for b₉ being natural_transformation of b₆,b₇ st b₆ is_naturally_transformable_to b₇ holds
(b₈ * b₉) * b₅ = b₈ * (b₉ * b₅)

proof end;

theorem Th36: :: ISOCAT_1:36

for b₁, b₂, b₃, b₄ being Category
for b₅, b₆ being Functor of b₃,b₄
for b₇ being Functor of b₄,b₁
for b₈ being Functor of b₁,b₂
for b₉ being natural_transformation of b₅,b₆ st b₅ is_naturally_transformable_to b₆ holds
(b₈ * b₇) * b₉ = b₈ * (b₇ * b₉)

proof end;

theorem Th37: :: ISOCAT_1:37

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₂,b₃ holds (id b₅) * b₄ = id (b₅ * b₄)

proof end;

theorem Th38: :: ISOCAT_1:38

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₂,b₃ holds b₅ * (id b₄) = id (b₅ * b₄)

proof end;

theorem Th39: :: ISOCAT_1:39

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₂,b₁
for b₅ being natural_transformation of b₃,b₄ st b₃ is_naturally_transformable_to b₄ holds
b₅ * (id b₂) = b₅

proof end;

theorem Th40: :: ISOCAT_1:40

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being natural_transformation of b₃,b₄ st b₃ is_naturally_transformable_to b₄ holds
(id b₂) * b₅ = b₅

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₁,c₂;
let c₆, c₇ be Functor of c₂,c₃;
let c₈ be natural_transformation of c₄,c₅;
let c₉ be natural_transformation of c₆,c₇;
func c₉ (#) c₈ -> natural_transformation of a₆ * a₄,a₇ * a₅ equals :: ISOCAT_1:def 9
(a₉ * a₅) `*` (a₆ * a₈);
correctness ;

end;

:: deftheorem Def9 defines (#) ISOCAT_1:def 9 :

theorem Th41: :: ISOCAT_1:41

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₂,b₃
for b₈ being natural_transformation of b₄,b₅
for b₉ being natural_transformation of b₆,b₇ st b₄ is_naturally_transformable_to b₅ & b₆ is_naturally_transformable_to b₇ holds
b₉ (#) b₈ = (b₇ * b₈) `*` (b₉ * b₄)

proof end;

theorem Th42: :: ISOCAT_1:42

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being natural_transformation of b₃,b₄ st b₃ is_naturally_transformable_to b₄ holds
(id (id b₂)) (#) b₅ = b₅

proof end;

theorem Th43: :: ISOCAT_1:43

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₂,b₁
for b₅ being natural_transformation of b₃,b₄ st b₃ is_naturally_transformable_to b₄ holds
b₅ (#) (id (id b₂)) = b₅

proof end;

theorem Th44: :: ISOCAT_1:44

for b₁, b₂, b₃, b₄ being Category
for b₅, b₆ being Functor of b₁,b₂
for b₇, b₈ being Functor of b₂,b₃
for b₉, b₁₀ being Functor of b₃,b₄
for b₁₁ being natural_transformation of b₅,b₆
for b₁₂ being natural_transformation of b₇,b₈
for b₁₃ being natural_transformation of b₉,b₁₀ st b₅ is_naturally_transformable_to b₆ & b₇ is_naturally_transformable_to b₈ & b₉ is_naturally_transformable_to b₁₀ holds
b₁₃ (#) (b₁₂ (#) b₁₁) = (b₁₃ (#) b₁₂) (#) b₁₁

proof end;

theorem Th45: :: ISOCAT_1:45

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅, b₆ being Functor of b₂,b₃
for b₇ being natural_transformation of b₅,b₆ st b₅ is_naturally_transformable_to b₆ holds
b₇ * b₄ = b₇ (#) (id b₄)

proof end;

theorem Th46: :: ISOCAT_1:46

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₂,b₃
for b₆ being Functor of b₃,b₁
for b₇ being natural_transformation of b₄,b₅ st b₄ is_naturally_transformable_to b₅ holds
b₆ * b₇ = (id b₆) (#) b₇

proof end;

theorem Th47: :: ISOCAT_1:47

for b₁, b₂, b₃ being Category
for b₄, b₅, b₆ being Functor of b₁,b₂
for b₇, b₈, b₉ being Functor of b₂,b₃
for b₁₀ being natural_transformation of b₄,b₅
for b₁₁ being natural_transformation of b₅,b₆
for b₁₂ being natural_transformation of b₇,b₈
for b₁₃ being natural_transformation of b₈,b₉ st b₄ is_naturally_transformable_to b₅ & b₅ is_naturally_transformable_to b₆ & b₇ is_naturally_transformable_to b₈ & b₈ is_naturally_transformable_to b₉ holds
(b₁₃ `*` b₁₂) (#) (b₁₁ `*` b₁₀) = (b₁₃ (#) b₁₁) `*` (b₁₂ (#) b₁₀)

proof end;

theorem Th48: :: ISOCAT_1:48

for b₁, b₂, b₃, b₄ being Category
for b₅ being Functor of b₁,b₂
for b₆ being Functor of b₃,b₄
for b₇, b₈ being Functor of b₂,b₃ st b₇ ~= b₈ holds
( b₆ * b₇ ~= b₆ * b₈ & b₇ * b₅ ~= b₈ * b₅ )

proof end;

theorem Th49: :: ISOCAT_1:49

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Functor of b₂,b₁
for b₅ being Functor of b₁,b₁ st b₅ ~= id b₁ holds
( b₃ * b₅ ~= b₃ & b₅ * b₄ ~= b₄ )

proof end;

definition

let c₁, c₂ be Category;
pred c₁ is_equivalent_with c₂ means :Def10: :: ISOCAT_1:def 10
ex b₁ being Functor of a₁,a₂ex b₂ being Functor of a₂,a₁ st
( b₂ * b₁ ~= id a₁ & b₁ * b₂ ~= id a₂ );
reflexivity

proof end;

symmetry ;

end;

:: deftheorem Def10 defines is_equivalent_with ISOCAT_1:def 10 :

notation

let c₁, c₂ be Category;
synonym c₁,c₂ are_equivalent for c₁ is_equivalent_with c₂;

end;

theorem Th50: :: ISOCAT_1:50

for b₁, b₂ being Category st b₁ ~= b₂ holds
b₁ is_equivalent_with b₂

proof end;

theorem Th51: :: ISOCAT_1:51

canceled;

theorem Th52: :: ISOCAT_1:52

canceled;

theorem Th53: :: ISOCAT_1:53

for b₁, b₂, b₃ being Category st b₁,b₂ are_equivalent & b₂,b₃ are_equivalent holds
b₁,b₃ are_equivalent

proof end;

definition

let c₁, c₂ be Category;
assume E41: c₁,c₂ are_equivalent ;
mode Equivalence of c₁,c₂ -> Functor of a₁,a₂ means :Def11: :: ISOCAT_1:def 11
ex b₁ being Functor of a₂,a₁ st
( b₁ * a₃ ~= id a₁ & a₃ * b₁ ~= id a₂ );
existence by E41, Def10;

end;

:: deftheorem Def11 defines Equivalence ISOCAT_1:def 11 :

theorem Th54: :: ISOCAT_1:54

for b₁ being Category holds id b₁ is Equivalence of b₁,b₁

proof end;

theorem Th55: :: ISOCAT_1:55

for b₁, b₂, b₃ being Category st b₁,b₂ are_equivalent & b₂,b₃ are_equivalent holds
for b₄ being Equivalence of b₁,b₂
for b₅ being Equivalence of b₂,b₃ holds b₅ * b₄ is Equivalence of b₁,b₃

proof end;

theorem Th56: :: ISOCAT_1:56

for b₁, b₂ being Category st b₁,b₂ are_equivalent holds
for b₃ being Equivalence of b₁,b₂ ex b₄ being Equivalence of b₂,b₁ st
( b₄ * b₃ ~= id b₁ & b₃ * b₄ ~= id b₂ )

proof end;

theorem Th57: :: ISOCAT_1:57

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Functor of b₂,b₁ st b₄ * b₃ ~= id b₁ holds
b₃ is faithful

proof end;

theorem Th58: :: ISOCAT_1:58

for b₁, b₂ being Category st b₁,b₂ are_equivalent holds
for b₃ being Equivalence of b₁,b₂ holds
( b₃ is full & b₃ is faithful & ( for b₄ being Object of b₂ ex b₅ being Object of b₁ st b₄,b₃ . b₅ are_isomorphic ) )

proof end;