:: ALTCAT_2 semantic presentation

theorem :: ALTCAT_2:1

for X1, X2, a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]

proof end;

registration

let I be set ;
cluster [0] I -> Function-yielding ;
coherence

proof end;

end;

theorem :: ALTCAT_2:2

for f, g being Function holds ~ (g * f) = g * (~ f)

proof end;

theorem :: ALTCAT_2:3

for f, g, h being Function holds ~ (f * [:g,h:]) = (~ f) * [:h,g:]

proof end;

registration

let f be Function-yielding Function;
cluster ~ f -> Function-yielding ;
coherence

proof end;

end;

theorem :: ALTCAT_2:4

for I being set
for A, B, C being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C

proof end;

definition

let I be set ;
let A be ManySortedSet of [:I,I:];
:: original: ~
redefine func ~ A -> ManySortedSet of [:I,I:];
coherence

proof end;

end;

theorem :: ALTCAT_2:5

for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f

proof end;

definition

let I be set ;
let A, B be ManySortedSet of [:I,I:];
let F be ManySortedFunction of A,B;
:: original: ~
redefine func ~ F -> ManySortedFunction of ~ A, ~ B;
coherence

proof end;

end;

theorem :: ALTCAT_2:6

for I1, I2 being non empty set
for M being ManySortedSet of [:I1,I2:]
for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . o2,o1 = M . o1,o2

proof end;

definition

let I1 be set ;
let f, g be ManySortedFunction of I1;
:: original: **
redefine func g ** f -> ManySortedFunction of I1;
coherence

proof end;

end;

definition

let f, g be Function;
pred f cc= g means :Def1: :: ALTCAT_2:def 1
( dom f c= dom g & ( for i being set st i in dom f holds
f . i c= g . i ) );
reflexivity ;

end;

:: deftheorem Def1 defines cc= ALTCAT_2:def 1 :

definition

let I, J be set ;
let A be ManySortedSet of I;
let B be ManySortedSet of J;
:: original: cc=
redefine pred A cc= B means :Def2: :: ALTCAT_2:def 2
( I c= J & ( for i being set st i in I holds
A . i c= B . i ) );
compatibility

proof end;

end;

:: deftheorem Def2 defines cc= ALTCAT_2:def 2 :

theorem :: ALTCAT_2:7

canceled;

theorem Th8: :: ALTCAT_2:8

for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B

proof end;

theorem Th9: :: ALTCAT_2:9

for I, J, K being set
for A being ManySortedSet of I
for B being ManySortedSet of J
for C being ManySortedSet of K st A cc= B & B cc= C holds
A cc= C

proof end;

theorem :: ALTCAT_2:10

for I being set
for A, B being ManySortedSet of I holds
( A cc= B iff A c= B )

proof end;

scheme :: ALTCAT_2:sch 1
OnSingletons{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set ] } :

{ [o,F₂(o)] where o is Element of F₁() : P₁[o] } is Function

proof end;

scheme :: ALTCAT_2:sch 2
DomOnSingletons{ F₁() -> non empty set , F₂() -> Function, F₃( set ) -> set , P₁[ set ] } :

dom F₂() = { o where o is Element of F₁() : P₁[o] }

provided

A1: F₂() = { [o,F₃(o)] where o is Element of F₁() : P₁[o] }

proof end;

scheme :: ALTCAT_2:sch 3
ValOnSingletons{ F₁() -> non empty set , F₂() -> Function, F₃() -> Element of F₁(), F₄( set ) -> set , P₁[ set ] } :

F₂() . F₃() = F₄(F₃())

provided

A1: F₂() = { [o,F₄(o)] where o is Element of F₁() : P₁[o] } and
A2: P₁[F₃()]

proof end;

theorem Th11: :: ALTCAT_2:11

for C being Category
for i, j, k being Object of C holds [:(Hom j,k),(Hom i,j):] c= dom the Comp of C

proof end;

theorem Th12: :: ALTCAT_2:12

for C being Category
for i, j, k being Object of C holds the Comp of C .: [:(Hom j,k),(Hom i,j):] c= Hom i,k

proof end;

definition

let C be CatStr ;
func the_hom_sets_of C -> ManySortedSet of [:the Objects of C,the Objects of C:] means :Def3: :: ALTCAT_2:def 3
for i, j being Object of C holds it . i,j = Hom i,j;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def 3 :

theorem Th13: :: ALTCAT_2:13

for C being Category
for i being Object of C holds id i in (the_hom_sets_of C) . i,i

proof end;

definition

let C be Category;
func the_comps_of C -> BinComp of (the_hom_sets_of C) means :Def4: :: ALTCAT_2:def 4
for i, j, k being Object of C holds it . i,j,k = the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines the_comps_of ALTCAT_2:def 4 :

theorem Th14: :: ALTCAT_2:14

for C being Category
for i, j, k being Object of C st Hom i,j <> {} & Hom j,k <> {} holds
for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . i,j,k) . g,f = g * f

proof end;

theorem Th15: :: ALTCAT_2:15

for C being Category holds the_comps_of C is associative

proof end;

theorem Th16: :: ALTCAT_2:16

for C being Category holds
( the_comps_of C is with_left_units & the_comps_of C is with_right_units )

proof end;

definition

let C be Category;
func Alter C -> non empty strict AltCatStr equals :: ALTCAT_2:def 5
AltCatStr(# the Objects of C,(the_hom_sets_of C),(the_comps_of C) #);
correctness ;

end;

:: deftheorem defines Alter ALTCAT_2:def 5 :

theorem Th17: :: ALTCAT_2:17

for C being Category holds Alter C is associative

proof end;

theorem Th18: :: ALTCAT_2:18

for C being Category holds Alter C is with_units

proof end;

theorem Th19: :: ALTCAT_2:19

for C being Category holds Alter C is transitive

proof end;

registration

let C be Category;
cluster Alter C -> non empty transitive strict associative with_units ;
coherence by Th17, Th18, Th19;

end;

registration

cluster non empty strict AltGraph ;
existence

proof end;

end;

definition

let C be AltGraph ;
attr C is reflexive means :Def6: :: ALTCAT_2:def 6
for x being set st x in the carrier of C holds
the Arrows of C . x,x <> {} ;

end;

:: deftheorem Def6 defines reflexive ALTCAT_2:def 6 :

definition

let C be non empty AltGraph ;
redefine attr C is reflexive means :: ALTCAT_2:def 7
for o being object of C holds <^o,o^> <> {} ;
compatibility

proof end;

end;

:: deftheorem defines reflexive ALTCAT_2:def 7 :

definition

let C be non empty transitive AltCatStr ;
redefine attr C is associative means :Def8: :: ALTCAT_2:def 8
for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f);
compatibility

proof end;

end;

:: deftheorem Def8 defines associative ALTCAT_2:def 8 :

definition

let C be non empty AltCatStr ;
redefine attr C is with_units means :: ALTCAT_2:def 9
for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) );
compatibility

proof end;

end;

:: deftheorem defines with_units ALTCAT_2:def 9 :

registration

cluster non empty with_units -> non empty reflexive AltCatStr ;
coherence

proof end;

end;

registration

cluster non empty reflexive AltGraph ;
existence

proof end;

end;

registration

cluster non empty reflexive AltCatStr ;
existence

proof end;

end;

Lm1: for E1, E2 being strict AltCatStr st the carrier of E1 is empty & the carrier of E2 is empty holds
E1 = E2

proof end;

definition

func the_empty_category -> strict AltCatStr means :Def10: :: ALTCAT_2:def 10
the carrier of it is empty;
existence

proof end;

uniqueness by Lm1;

end;

:: deftheorem Def10 defines the_empty_category ALTCAT_2:def 10 :

registration

cluster the_empty_category -> empty strict ;
coherence

proof end;

end;

registration

cluster empty strict AltCatStr ;
existence

proof end;

end;

theorem :: ALTCAT_2:20

for E being empty strict AltCatStr holds E = the_empty_category

proof end;

definition

let C be AltCatStr ;
mode SubCatStr of C -> AltCatStr means :Def11: :: ALTCAT_2:def 11
( the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C );
existence ;

end;

:: deftheorem Def11 defines SubCatStr ALTCAT_2:def 11 :

theorem Th21: :: ALTCAT_2:21

for C being AltCatStr holds C is SubCatStr of C

proof end;

theorem :: ALTCAT_2:22

for C1, C2, C3 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C3 holds
C1 is SubCatStr of C3

proof end;

theorem Th23: :: ALTCAT_2:23

for C1, C2 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C1 holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)

proof end;

registration

let C be AltCatStr ;
cluster strict SubCatStr of C;
existence

proof end;

end;

definition

let C be non empty AltCatStr ;
let o be object of C;
func ObCat o -> strict SubCatStr of C means :Def12: :: ALTCAT_2:def 12
( the carrier of it = {o} & the Arrows of it = o,o :-> <^o,o^> & the Comp of it = [o,o,o] .--> (the Comp of C . o,o,o) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines ObCat ALTCAT_2:def 12 :

theorem Th24: :: ALTCAT_2:24

for C being non empty AltCatStr
for o being object of C
for o' being object of (ObCat o) holds o' = o

proof end;

registration

let C be non empty AltCatStr ;
let o be object of C;
cluster ObCat o -> non empty transitive strict ;
coherence

proof end;

end;

registration

let C be non empty AltCatStr ;
cluster non empty transitive strict SubCatStr of C;
existence

proof end;

end;

theorem Th25: :: ALTCAT_2:25

for C being non empty transitive AltCatStr
for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds
D1 is SubCatStr of D2

proof end;

definition

let C be AltCatStr ;
let D be SubCatStr of C;
attr D is full means :Def13: :: ALTCAT_2:def 13
the Arrows of D = the Arrows of C || the carrier of D;

end;

:: deftheorem Def13 defines full ALTCAT_2:def 13 :

definition

let C be non empty with_units AltCatStr ;
let D be SubCatStr of C;
attr D is id-inheriting means :Def14: :: ALTCAT_2:def 14
for o being object of D
for o' being object of C st o = o' holds
idm o' in <^o,o^> if not D is empty
otherwise verum;
consistency ;

end;

:: deftheorem Def14 defines id-inheriting ALTCAT_2:def 14 :

registration

let C be AltCatStr ;
cluster strict full SubCatStr of C;
existence

proof end;

end;

registration

let C be non empty AltCatStr ;
cluster non empty strict full SubCatStr of C;
existence

proof end;

end;

registration

let C be category;
let o be object of C;
cluster ObCat o -> non empty transitive strict full id-inheriting ;
coherence

proof end;

end;

registration

let C be category;
cluster non empty strict full id-inheriting SubCatStr of C;
existence

proof end;

end;

theorem Th26: :: ALTCAT_2:26

for C being non empty transitive AltCatStr
for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds
AltCatStr(# the carrier of D,the Arrows of D,the Comp of D #) = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #)

proof end;

theorem Th27: :: ALTCAT_2:27

for C being non empty transitive AltCatStr
for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds
AltCatStr(# the carrier of D1,the Arrows of D1,the Comp of D1 #) = AltCatStr(# the carrier of D2,the Arrows of D2,the Comp of D2 #)

proof end;

theorem :: ALTCAT_2:28

for C being non empty transitive AltCatStr
for D being full SubCatStr of C st the carrier of D = the carrier of C holds
AltCatStr(# the carrier of D,the Arrows of D,the Comp of D #) = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #)

proof end;

theorem Th29: :: ALTCAT_2:29

for C being non empty AltCatStr
for D being non empty full SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>

proof end;

theorem Th30: :: ALTCAT_2:30

for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o being object of D holds o is object of C

proof end;

registration

let C be non empty transitive AltCatStr ;
cluster non empty full -> transitive SubCatStr of C;
coherence

proof end;

end;

theorem :: ALTCAT_2:31

for C being non empty transitive AltCatStr
for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds
AltCatStr(# the carrier of D1,the Arrows of D1,the Comp of D1 #) = AltCatStr(# the carrier of D2,the Arrows of D2,the Comp of D2 #)

proof end;

theorem Th32: :: ALTCAT_2:32

for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>

proof end;

theorem Th33: :: ALTCAT_2:33

for C being non empty transitive AltCatStr
for D being non empty transitive SubCatStr of C
for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds
for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff

proof end;

registration

let C be non empty transitive associative AltCatStr ;
cluster non empty transitive -> non empty associative SubCatStr of C;
coherence

proof end;

end;

theorem Th34: :: ALTCAT_2:34

for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2

proof end;

registration

let C be non empty transitive with_units AltCatStr ;
cluster non empty transitive id-inheriting -> non empty with_units reflexive SubCatStr of C;
coherence

proof end;

end;

registration

let C be category;
cluster non empty transitive associative with_units reflexive id-inheriting SubCatStr of C;
existence

proof end;

end;

definition

let C be category;
mode subcategory of C is transitive id-inheriting SubCatStr of C;

end;

theorem :: ALTCAT_2:35

for C being category
for D being non empty subcategory of C
for o being object of D
for o' being object of C st o = o' holds
idm o = idm o'

proof end;