:: ALTCAT_1 semantic presentation

registration

let c₁ be functional set ;
cluster -> functional Element of bool a₁;
coherence

proof end;

end;

registration

let c₁ be Function-yielding Function;
let c₂ be set ;
cluster a₁ | a₂ -> Function-yielding ;
correctness by MSUHOM_1:3;

end;

registration

let c₁ be Function;
cluster {a₁} -> functional ;
coherence

proof end;

end;

theorem Th1: :: ALTCAT_1:1

canceled;

theorem Th2: :: ALTCAT_1:2

for b₁ being set holds id b₁ in Funcs b₁,b₁

proof end;

theorem Th3: :: ALTCAT_1:3

Funcs {} ,{} = {(id {} )}

proof end;

theorem Th4: :: ALTCAT_1:4

for b₁, b₂, b₃ being set
for b₄, b₅ being Function st b₄ in Funcs b₁,b₂ & b₅ in Funcs b₂,b₃ holds
b₅ * b₄ in Funcs b₁,b₃

proof end;

theorem Th5: :: ALTCAT_1:5

for b₁, b₂, b₃ being set st Funcs b₁,b₂ <> {} & Funcs b₂,b₃ <> {} holds
Funcs b₁,b₃ <> {}

proof end;

theorem Th6: :: ALTCAT_1:6

canceled;

theorem Th7: :: ALTCAT_1:7

for b₁, b₂ being set
for b₃ being ManySortedSet of [:b₂,b₁:]
for b₄ being Subset of b₁
for b₅ being Subset of b₂
for b₆, b₇ being set st b₆ in b₄ & b₇ in b₅ holds
b₃ . b₇,b₆ = (b₃ | [:b₅,b₄:]) . b₇,b₆

proof end;

scheme :: ALTCAT_1:sch 1
s1{ F₁() -> set , F₂() -> set , F₃( set , set ) -> set } :

ex b₁ being ManySortedSet of [:F₁(),F₂():] st
for b₂, b₃ being set st b₂ in F₁() & b₃ in F₂() holds
b₁ . b₂,b₃ = F₃(b₂,b₃)

proof end;

scheme :: ALTCAT_1:sch 2
s2{ F₁() -> non empty set , F₂() -> non empty set , F₃( set , set ) -> set } :

ex b₁ being ManySortedSet of [:F₁(),F₂():] st
for b₂ being Element of F₁()
for b₃ being Element of F₂() holds b₁ . b₂,b₃ = F₃(b₂,b₃)

proof end;

scheme :: ALTCAT_1:sch 3
s3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set , set ) -> set } :

ex b₁ being ManySortedSet of [:F₁(),F₂(),F₃():] st
for b₂, b₃, b₄ being set st b₂ in F₁() & b₃ in F₂() & b₄ in F₃() holds
b₁ . b₂,b₃,b₄ = F₄(b₂,b₃,b₄)

proof end;

scheme :: ALTCAT_1:sch 4
s4{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set , set , set ) -> set } :

ex b₁ being ManySortedSet of [:F₁(),F₂(),F₃():] st
for b₂ being Element of F₁()
for b₃ being Element of F₂()
for b₄ being Element of F₃() holds b₁ . b₂,b₃,b₄ = F₄(b₂,b₃,b₄)

proof end;

theorem Th8: :: ALTCAT_1:8

for b₁, b₂ being set
for b₃, b₄ being ManySortedSet of [:b₁,b₂:] st ( for b₅, b₆ being set st b₅ in b₁ & b₆ in b₂ holds
b₃ . b₅,b₆ = b₄ . b₅,b₆ ) holds
b₄ = b₃

proof end;

theorem Th9: :: ALTCAT_1:9

for b₁, b₂ being non empty set
for b₃, b₄ being ManySortedSet of [:b₁,b₂:] st ( for b₅ being Element of b₁
for b₆ being Element of b₂ holds b₃ . b₅,b₆ = b₄ . b₅,b₆ ) holds
b₄ = b₃

proof end;

theorem Th10: :: ALTCAT_1:10

for b₁ being set
for b₂, b₃ being ManySortedSet of [:b₁,b₁,b₁:] st ( for b₄, b₅, b₆ being set st b₄ in b₁ & b₅ in b₁ & b₆ in b₁ holds
b₂ . b₄,b₅,b₆ = b₃ . b₄,b₅,b₆ ) holds
b₃ = b₂

proof end;

theorem Th11: :: ALTCAT_1:11

for b₁, b₂, b₃ being set holds b₁,b₂ :-> b₃ = [b₁,b₂] .--> b₃

proof end;

theorem Th12: :: ALTCAT_1:12

for b₁, b₂, b₃ being set holds (b₁,b₂ :-> b₃) . b₁,b₂ = b₃

proof end;

definition

attr a₁ is strict;
struct AltGraph -> 1-sorted ;
aggr AltGraph(# carrier, Arrows #) -> AltGraph ;
sel Arrows c₁ -> ManySortedSet of [:the carrier of a₁,the carrier of a₁:];

end;

definition

let c₁ be AltGraph ;
mode object of a₁ is Element of a₁;

end;

definition

let c₁ be AltGraph ;
let c₂, c₃ be object of c₁;
canceled;
func <^c₂,c₃^> -> set equals :: ALTCAT_1:def 2
the Arrows of a₁ . a₂,a₃;
correctness ;

end;

:: deftheorem Def1 ALTCAT_1:def 1 :

:: deftheorem Def2 defines <^ ALTCAT_1:def 2 :

definition

let c₁ be AltGraph ;
let c₂, c₃ be object of c₁;
mode Morphism of a₂,a₃ is Element of <^a₂,a₃^>;

end;

definition

let c₁ be AltGraph ;
canceled;
attr a₁ is transitive means :Def4: :: ALTCAT_1:def 4
for b₁, b₂, b₃ being object of a₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
<^b₁,b₃^> <> {} ;

end;

:: deftheorem Def3 ALTCAT_1:def 3 :

:: deftheorem Def4 defines transitive ALTCAT_1:def 4 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of [:c₁,c₁:];
func {|c₂|} -> ManySortedSet of [:a₁,a₁,a₁:] means :Def5: :: ALTCAT_1:def 5
for b₁, b₂, b₃ being set st b₁ in a₁ & b₂ in a₁ & b₃ in a₁ holds
a₃ . b₁,b₂,b₃ = a₂ . b₁,b₃;
existence

proof end;

uniqueness

proof end;

let c₃ be ManySortedSet of [:c₁,c₁:];
func {|c₂,c₃|} -> ManySortedSet of [:a₁,a₁,a₁:] means :Def6: :: ALTCAT_1:def 6
for b₁, b₂, b₃ being set st b₁ in a₁ & b₂ in a₁ & b₃ in a₁ holds
a₄ . b₁,b₂,b₃ = [:(a₃ . b₂,b₃),(a₂ . b₁,b₂):];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines {| ALTCAT_1:def 5 :

:: deftheorem Def6 defines {| ALTCAT_1:def 6 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of [:c₁,c₁:];
mode BinComp of a₂ is ManySortedFunction of {|a₂,a₂|},{|a₂|};

end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of [:c₁,c₁:];
let c₃ be BinComp of c₂;
let c₄, c₅, c₆ be Element of c₁;
redefine func . as c₃ . c₄,c₅,c₆ -> Function of [:(a₂ . a₅,a₆),(a₂ . a₄,a₅):],a₂ . a₄,a₆;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of [:c₁,c₁:];
let c₃ be BinComp of c₂;
attr a₃ is associative means :Def7: :: ALTCAT_1:def 7
for b₁, b₂, b₃, b₄ being Element of a₁
for b₅, b₆, b₇ being set st b₅ in a₂ . b₁,b₂ & b₆ in a₂ . b₂,b₃ & b₇ in a₂ . b₃,b₄ holds
(a₃ . b₁,b₃,b₄) . b₇,((a₃ . b₁,b₂,b₃) . b₆,b₅) = (a₃ . b₁,b₂,b₄) . ((a₃ . b₂,b₃,b₄) . b₇,b₆),b₅;
attr a₃ is with_right_units means :Def8: :: ALTCAT_1:def 8
for b₁ being Element of a₁ ex b₂ being set st
( b₂ in a₂ . b₁,b₁ & ( for b₃ being Element of a₁
for b₄ being set st b₄ in a₂ . b₁,b₃ holds
(a₃ . b₁,b₁,b₃) . b₄,b₂ = b₄ ) );
attr a₃ is with_left_units means :Def9: :: ALTCAT_1:def 9
for b₁ being Element of a₁ ex b₂ being set st
( b₂ in a₂ . b₁,b₁ & ( for b₃ being Element of a₁
for b₄ being set st b₄ in a₂ . b₃,b₁ holds
(a₃ . b₃,b₁,b₁) . b₂,b₄ = b₄ ) );

end;

:: deftheorem Def7 defines associative ALTCAT_1:def 7 :

:: deftheorem Def8 defines with_right_units ALTCAT_1:def 8 :

:: deftheorem Def9 defines with_left_units ALTCAT_1:def 9 :

definition

attr a₁ is strict;
struct AltCatStr -> AltGraph ;
aggr AltCatStr(# carrier, Arrows, Comp #) -> AltCatStr ;
sel Comp c₁ -> BinComp of the Arrows of a₁;

end;

registration

cluster non empty strict AltCatStr ;
existence

proof end;

end;

definition

let c₁ be non empty AltCatStr ;
let c₂, c₃, c₄ be object of c₁;
assume E16: ( <^c₂,c₃^> <> {} & <^c₃,c₄^> <> {} ) ;
let c₅ be Morphism of c₂,c₃;
let c₆ be Morphism of c₃,c₄;
func c₆ * c₅ -> Morphism of a₂,a₄ equals :Def10: :: ALTCAT_1:def 10
(the Comp of a₁ . a₂,a₃,a₄) . a₆,a₅;
coherence

proof end;

correctness ;

end;

:: deftheorem Def10 defines * ALTCAT_1:def 10 :

definition

let c₁ be Function;
attr a₁ is compositional means :Def11: :: ALTCAT_1:def 11
for b₁ being set st b₁ in dom a₁ holds
ex b₂, b₃ being Function st
( b₁ = [b₃,b₂] & a₁ . b₁ = b₃ * b₂ );

end;

:: deftheorem Def11 defines compositional ALTCAT_1:def 11 :

registration

let c₁, c₂ be functional set ;
cluster compositional ManySortedSet of [:a₁,a₂:];
existence

proof end;

end;

theorem Th13: :: ALTCAT_1:13

for b₁, b₂ being functional set
for b₃ being compositional ManySortedSet of [:b₁,b₂:]
for b₄, b₅ being Function st b₄ in b₁ & b₅ in b₂ holds
b₃ . b₄,b₅ = b₄ * b₅

proof end;

definition

let c₁, c₂ be functional set ;
func FuncComp c₁,c₂ -> compositional ManySortedFunction of [:a₂,a₁:] means :Def12: :: ALTCAT_1:def 12
verum;
uniqueness

proof end;

correctness ;

end;

:: deftheorem Def12 defines FuncComp ALTCAT_1:def 12 :

theorem Th14: :: ALTCAT_1:14

for b₁, b₂, b₃ being set holds rng (FuncComp (Funcs b₁,b₂),(Funcs b₂,b₃)) c= Funcs b₁,b₃

proof end;

theorem Th15: :: ALTCAT_1:15

for b₁ being set holds FuncComp {(id b₁)},{(id b₁)} = (id b₁),(id b₁) :-> (id b₁)

proof end;

theorem Th16: :: ALTCAT_1:16

for b₁, b₂ being functional set
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds FuncComp b₃,b₄ = (FuncComp b₁,b₂) | [:b₄,b₃:]

proof end;

definition

let c₁ be non empty AltCatStr ;
attr a₁ is quasi-functional means :Def13: :: ALTCAT_1:def 13
for b₁, b₂ being object of a₁ holds <^b₁,b₂^> c= Funcs b₁,b₂;
attr a₁ is semi-functional means :Def14: :: ALTCAT_1:def 14
for b₁, b₂, b₃ being object of a₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} & <^b₁,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃
for b₆, b₇ being Function st b₄ = b₆ & b₅ = b₇ holds
b₅ * b₄ = b₇ * b₆;
attr a₁ is pseudo-functional means :Def15: :: ALTCAT_1:def 15
for b₁, b₂, b₃ being object of a₁ holds the Comp of a₁ . b₁,b₂,b₃ = (FuncComp (Funcs b₁,b₂),(Funcs b₂,b₃)) | [:<^b₂,b₃^>,<^b₁,b₂^>:];

end;

:: deftheorem Def13 defines quasi-functional ALTCAT_1:def 13 :

:: deftheorem Def14 defines semi-functional ALTCAT_1:def 14 :

:: deftheorem Def15 defines pseudo-functional ALTCAT_1:def 15 :

registration

let c₁ be non empty set ;
let c₂ be ManySortedSet of [:c₁,c₁:];
let c₃ be BinComp of c₂;
cluster AltCatStr(# a₁,a₂,a₃ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty strict pseudo-functional AltCatStr ;
existence

proof end;

end;

theorem Th17: :: ALTCAT_1:17

for b₁ being non empty AltCatStr
for b₂, b₃, b₄ being object of b₁ holds the Comp of b₁ . b₂,b₃,b₄ is Function of [:<^b₃,b₄^>,<^b₂,b₃^>:],<^b₂,b₄^> ;

theorem Th18: :: ALTCAT_1:18

for b₁ being non empty pseudo-functional AltCatStr
for b₂, b₃, b₄ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} & <^b₂,b₄^> <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄
for b₇, b₈ being Function st b₅ = b₇ & b₆ = b₈ holds
b₆ * b₅ = b₈ * b₇

proof end;

definition

let c₁ be non empty set ;
func EnsCat c₁ -> non empty strict pseudo-functional AltCatStr means :Def16: :: ALTCAT_1:def 16
( the carrier of a₂ = a₁ & ( for b₁, b₂ being object of a₂ holds <^b₁,b₂^> = Funcs b₁,b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines EnsCat ALTCAT_1:def 16 :

definition

let c₁ be non empty AltCatStr ;
attr a₁ is associative means :Def17: :: ALTCAT_1:def 17
the Comp of a₁ is associative;
attr a₁ is with_units means :Def18: :: ALTCAT_1:def 18
( the Comp of a₁ is with_left_units & the Comp of a₁ is with_right_units );

end;

:: deftheorem Def17 defines associative ALTCAT_1:def 17 :

:: deftheorem Def18 defines with_units ALTCAT_1:def 18 :

Lemma30: for b₁ being non empty set holds
( EnsCat b₁ is transitive & EnsCat b₁ is associative & EnsCat b₁ is with_units )

proof end;

registration

cluster non empty transitive strict associative with_units AltCatStr ;
existence

proof end;

end;

theorem Th19: :: ALTCAT_1:19

canceled;

theorem Th20: :: ALTCAT_1:20

for b₁ being non empty transitive AltCatStr
for b₂, b₃, b₄ being object of b₁ holds
( dom (the Comp of b₁ . b₂,b₃,b₄) = [:<^b₃,b₄^>,<^b₂,b₃^>:] & rng (the Comp of b₁ . b₂,b₃,b₄) c= <^b₂,b₄^> )

proof end;

theorem Th21: :: ALTCAT_1:21

for b₁ being non empty with_units AltCatStr
for b₂ being object of b₁ holds <^b₂,b₂^> <> {}

proof end;

registration

let c₁ be non empty set ;
cluster EnsCat a₁ -> non empty transitive strict pseudo-functional associative with_units ;
coherence by Lemma30;

end;

registration

cluster non empty transitive quasi-functional semi-functional -> non empty pseudo-functional AltCatStr ;
coherence

proof end;

cluster non empty transitive pseudo-functional with_units -> non empty quasi-functional semi-functional AltCatStr ;
coherence

proof end;

end;

definition

mode category is non empty transitive associative with_units AltCatStr ;

end;

definition

let c₁ be non empty with_units AltCatStr ;
let c₂ be object of c₁;
func idm c₂ -> Morphism of a₂,a₂ means :Def19: :: ALTCAT_1:def 19
for b₁ being object of a₁ st <^a₂,b₁^> <> {} holds
for b₂ being Morphism of a₂,b₁ holds b₂ * a₃ = b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines idm ALTCAT_1:def 19 :

theorem Th22: :: ALTCAT_1:22

canceled;

theorem Th23: :: ALTCAT_1:23

for b₁ being non empty with_units AltCatStr
for b₂ being object of b₁ holds idm b₂ in <^b₂,b₂^>

proof end;

theorem Th24: :: ALTCAT_1:24

for b₁ being non empty with_units AltCatStr
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds (idm b₃) * b₄ = b₄

proof end;

theorem Th25: :: ALTCAT_1:25

for b₁ being non empty transitive associative AltCatStr
for b₂, b₃, b₄, b₅ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} & <^b₄,b₅^> <> {} holds
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₃,b₄
for b₈ being Morphism of b₄,b₅ holds b₈ * (b₇ * b₆) = (b₈ * b₇) * b₆

proof end;

definition

let c₁ be AltCatStr ;
attr a₁ is quasi-discrete means :Def20: :: ALTCAT_1:def 20
for b₁, b₂ being object of a₁ st <^b₁,b₂^> <> {} holds
b₁ = b₂;
attr a₁ is pseudo-discrete means :Def21: :: ALTCAT_1:def 21
for b₁ being object of a₁ holds <^b₁,b₁^> is trivial;

end;

:: deftheorem Def20 defines quasi-discrete ALTCAT_1:def 20 :

:: deftheorem Def21 defines pseudo-discrete ALTCAT_1:def 21 :

theorem Th26: :: ALTCAT_1:26

for b₁ being non empty with_units AltCatStr holds
( b₁ is pseudo-discrete iff for b₂ being object of b₁ holds <^b₂,b₂^> = {(idm b₂)} )

proof end;

registration

cluster non empty trivial -> quasi-discrete AltCatStr ;
coherence

proof end;

end;

theorem Th27: :: ALTCAT_1:27

( EnsCat 1 is pseudo-discrete & EnsCat 1 is trivial )

proof end;

registration

cluster trivial strict quasi-discrete pseudo-discrete AltCatStr ;
existence by Th27;

end;

registration

cluster trivial strict quasi-discrete pseudo-discrete AltCatStr ;
existence

proof end;

end;

definition

mode discrete_category is quasi-discrete pseudo-discrete category;

end;

definition

let c₁ be non empty set ;
func DiscrCat c₁ -> non empty strict quasi-discrete AltCatStr means :Def22: :: ALTCAT_1:def 22
( the carrier of a₂ = a₁ & ( for b₁ being object of a₂ holds <^b₁,b₁^> = {(id b₁)} ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def22 defines DiscrCat ALTCAT_1:def 22 :

registration

cluster quasi-discrete -> transitive AltCatStr ;
coherence

proof end;

end;

theorem Th28: :: ALTCAT_1:28

for b₁ being non empty set
for b₂, b₃, b₄ being object of (DiscrCat b₁) st ( b₂ <> b₃ or b₃ <> b₄ ) holds
the Comp of (DiscrCat b₁) . b₂,b₃,b₄ = {}

proof end;

theorem Th29: :: ALTCAT_1:29

for b₁ being non empty set
for b₂ being object of (DiscrCat b₁) holds the Comp of (DiscrCat b₁) . b₂,b₂,b₂ = (id b₂),(id b₂) :-> (id b₂)

proof end;

registration

let c₁ be non empty set ;
cluster DiscrCat a₁ -> non empty transitive strict quasi-functional semi-functional pseudo-functional associative with_units quasi-discrete pseudo-discrete ;
coherence

proof end;

end;