:: by Artur Korni{\l}owicz

::

:: Received August 19, 2012

:: Copyright (c) 2012-2019 Association of Mizar Users

registration
end;

definition

let C be AltGraph ;

end;
attr C is functional means :Def1: :: ALTCAT_5:def 1

for a, b being Object of C holds <^a,b^> is functional ;

for a, b being Object of C holds <^a,b^> is functional ;

:: deftheorem Def1 defines functional ALTCAT_5:def 1 :

for C being AltGraph holds

( C is functional iff for a, b being Object of C holds <^a,b^> is functional );

for C being AltGraph holds

( C is functional iff for a, b being Object of C holds <^a,b^> is functional );

registration
end;

registration

let C be functional AltCatStr ;

coherence

AltGraph(# the carrier of C, the Arrows of C #) is functional

end;
coherence

AltGraph(# the carrier of C, the Arrows of C #) is functional

proof end;

registration
end;

registration
end;

registration
end;

reconsider a = 0 , b = 1 as Element of 2 by CARD_1:50, TARSKI:def 2;

set C = EnsCat {{}};

Lm1: the carrier of (EnsCat {{}}) = {0}

by ALTCAT_1:def 14;

reconsider o = {} as Object of (EnsCat {{}}) by Lm1, TARSKI:def 1;

Lm2: Funcs ({},{}) = {{}}

by FUNCT_5:57;

Lm3: now :: thesis: for o1, o being Object of (EnsCat {{}}) holds

( {} is Morphism of o1,o & {} in <^o1,o^> )

( {} is Morphism of o1,o & {} in <^o1,o^> )

let o1, o be Object of (EnsCat {{}}); :: thesis: ( {} is Morphism of o1,o & {} in <^o1,o^> )

A1: ( o1 = {} & o = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence ( {} is Morphism of o1,o & {} in <^o1,o^> ) by A1, Lm1, Lm2; :: thesis: verum

end;
A1: ( o1 = {} & o = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence ( {} is Morphism of o1,o & {} in <^o1,o^> ) by A1, Lm1, Lm2; :: thesis: verum

Lm4: now :: thesis: for o1, o being Object of (EnsCat {{}})

for m1 being Morphism of o1,o holds m1 = {}

for m1 being Morphism of o1,o holds m1 = {}

let o1, o be Object of (EnsCat {{}}); :: thesis: for m1 being Morphism of o1,o holds m1 = {}

let m1 be Morphism of o1,o; :: thesis: m1 = {}

A1: ( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence m1 = {} by A1, Lm2, TARSKI:def 1; :: thesis: verum

end;
let m1 be Morphism of o1,o; :: thesis: m1 = {}

A1: ( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence m1 = {} by A1, Lm2, TARSKI:def 1; :: thesis: verum

Lm5: now :: thesis: for o1, o being Object of (EnsCat {{}}) holds o1 = o

let o1, o be Object of (EnsCat {{}}); :: thesis: o1 = o

( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

hence o1 = o ; :: thesis: verum

end;
( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

hence o1 = o ; :: thesis: verum

Lm6: now :: thesis: for o1, o being Object of (EnsCat {{}})

for m1, m being Morphism of o1,o holds m1 = m

for m1, m being Morphism of o1,o holds m1 = m

let o1, o be Object of (EnsCat {{}}); :: thesis: for m1, m being Morphism of o1,o holds m1 = m

let m1, m be Morphism of o1,o; :: thesis: m1 = m

thus m1 = {} by Lm4

.= m by Lm4 ; :: thesis: verum

end;
let m1, m be Morphism of o1,o; :: thesis: m1 = m

thus m1 = {} by Lm4

.= m by Lm4 ; :: thesis: verum

definition
end;

definition

let C be non empty AltCatStr ;

let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & b_{1} . i is Morphism of o,o1 )

end;
let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

mode MorphismsFamily of o,f -> ManySortedSet of I means :Def2: :: ALTCAT_5:def 2

for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & it . i is Morphism of o,o1 );

existence for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & it . i is Morphism of o,o1 );

ex b

for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & b

proof end;

:: deftheorem Def2 defines MorphismsFamily ALTCAT_5:def 2 :

for C being non empty AltCatStr

for o being Object of C

for I being set

for f being ObjectsFamily of I,C

for b_{5} being ManySortedSet of I holds

( b_{5} is MorphismsFamily of o,f iff for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & b_{5} . i is Morphism of o,o1 ) );

for C being non empty AltCatStr

for o being Object of C

for I being set

for f being ObjectsFamily of I,C

for b

( b

ex o1 being Object of C st

( o1 = f . i & b

definition

let C be non empty AltCatStr ;

let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

for b_{1} being ManySortedSet of I holds

( b_{1} is MorphismsFamily of o,f iff for i being Element of I holds b_{1} . i is Morphism of o,(f . i) )

end;
let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

redefine mode MorphismsFamily of o,f means :Def3: :: ALTCAT_5:def 3

for i being Element of I holds it . i is Morphism of o,(f . i);

compatibility for i being Element of I holds it . i is Morphism of o,(f . i);

for b

( b

proof end;

:: deftheorem Def3 defines MorphismsFamily ALTCAT_5:def 3 :

for C being non empty AltCatStr

for o being Object of C

for I being non empty set

for f being ObjectsFamily of I,C

for b_{5} being ManySortedSet of I holds

( b_{5} is MorphismsFamily of o,f iff for i being Element of I holds b_{5} . i is Morphism of o,(f . i) );

for C being non empty AltCatStr

for o being Object of C

for I being non empty set

for f being ObjectsFamily of I,C

for b

( b

definition

let C be non empty AltCatStr ;

let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

let M be MorphismsFamily of o,f;

let i be Element of I;

:: original: .

redefine func M . i -> Morphism of o,(f . i);

coherence

M . i is Morphism of o,(f . i) by Def3;

end;
let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

let M be MorphismsFamily of o,f;

let i be Element of I;

:: original: .

redefine func M . i -> Morphism of o,(f . i);

coherence

M . i is Morphism of o,(f . i) by Def3;

registration

let C be non empty functional AltCatStr ;

let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

coherence

for b_{1} being MorphismsFamily of o,f holds b_{1} is Function-yielding

end;
let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

coherence

for b

proof end;

theorem Th1: :: ALTCAT_5:1

for C being non empty AltCatStr

for o being Object of C

for f being ObjectsFamily of {},C holds {} is MorphismsFamily of o,f

for o being Object of C

for f being ObjectsFamily of {},C holds {} is MorphismsFamily of o,f

proof end;

definition

let C be non empty AltCatStr ;

let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

end;
let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

:: deftheorem defines feasible ALTCAT_5:def 4 :

for C being non empty AltCatStr

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is feasible iff for i being set st i in I holds

ex o being Object of C st

( o = A . i & P . i in <^B,o^> ) );

for C being non empty AltCatStr

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is feasible iff for i being set st i in I holds

ex o being Object of C st

( o = A . i & P . i in <^B,o^> ) );

definition

let C be non empty AltCatStr ;

let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

( P is feasible iff for i being Element of I holds P . i in <^B,(A . i)^> )

end;
let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

redefine attr P is feasible means :Def5: :: ALTCAT_5:def 5

for i being Element of I holds P . i in <^B,(A . i)^>;

compatibility for i being Element of I holds P . i in <^B,(A . i)^>;

( P is feasible iff for i being Element of I holds P . i in <^B,(A . i)^> )

proof end;

:: deftheorem Def5 defines feasible ALTCAT_5:def 5 :

for C being non empty AltCatStr

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is feasible iff for i being Element of I holds P . i in <^B,(A . i)^> );

for C being non empty AltCatStr

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is feasible iff for i being Element of I holds P . i in <^B,(A . i)^> );

definition

let C be category;

let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

end;
let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

attr P is projection-morphisms means :: ALTCAT_5:def 6

for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,B st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f1 ) ) holds

f = f1 ) );

for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,B st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f1 ) ) holds

f = f1 ) );

:: deftheorem defines projection-morphisms ALTCAT_5:def 6 :

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is projection-morphisms iff for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,B st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f1 ) ) holds

f = f1 ) ) );

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is projection-morphisms iff for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,B st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of B,si st

( si = A . i & Pi = P . i & F . i = Pi * f1 ) ) holds

f = f1 ) ) );

definition

let C be category;

let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

compatibility

( P is projection-morphisms iff for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being Element of I holds F . i = (P . i) * f ) & ( for f1 being Morphism of X,B st ( for i being Element of I holds F . i = (P . i) * f1 ) holds

f = f1 ) ) );

end;
let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of B,A;

redefine attr P is projection-morphisms means :: ALTCAT_5:def 7

for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being Element of I holds F . i = (P . i) * f ) & ( for f1 being Morphism of X,B st ( for i being Element of I holds F . i = (P . i) * f1 ) holds

f = f1 ) );

correctness for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being Element of I holds F . i = (P . i) * f ) & ( for f1 being Morphism of X,B st ( for i being Element of I holds F . i = (P . i) * f1 ) holds

f = f1 ) );

compatibility

( P is projection-morphisms iff for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being Element of I holds F . i = (P . i) * f ) & ( for f1 being Morphism of X,B st ( for i being Element of I holds F . i = (P . i) * f1 ) holds

f = f1 ) ) );

proof end;

:: deftheorem defines projection-morphisms ALTCAT_5:def 7 :

for C being category

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is projection-morphisms iff for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being Element of I holds F . i = (P . i) * f ) & ( for f1 being Morphism of X,B st ( for i being Element of I holds F . i = (P . i) * f1 ) holds

f = f1 ) ) );

for C being category

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of B,A holds

( P is projection-morphisms iff for X being Object of C

for F being MorphismsFamily of X,A st F is feasible holds

ex f being Morphism of X,B st

( f in <^X,B^> & ( for i being Element of I holds F . i = (P . i) * f ) & ( for f1 being Morphism of X,B st ( for i being Element of I holds F . i = (P . i) * f1 ) holds

f = f1 ) ) );

registration

let C be category;

let A be ObjectsFamily of {},C;

let B be Object of C;

coherence

for b_{1} being MorphismsFamily of B,A holds b_{1} is feasible
;

end;
let A be ObjectsFamily of {},C;

let B be Object of C;

coherence

for b

theorem Th2: :: ALTCAT_5:2

for C being category

for A being ObjectsFamily of {},C

for B being Object of C st B is terminal holds

ex P being MorphismsFamily of B,A st

( P is empty & P is projection-morphisms )

for A being ObjectsFamily of {},C

for B being Object of C st B is terminal holds

ex P being MorphismsFamily of B,A st

( P is empty & P is projection-morphisms )

proof end;

theorem Th3: :: ALTCAT_5:3

for I being set

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of o,A

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of o,A

proof end;

theorem Th4: :: ALTCAT_5:4

for I being set

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}})

for P being MorphismsFamily of o,A st P = I --> {} holds

( P is feasible & P is projection-morphisms )

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}})

for P being MorphismsFamily of o,A st P = I --> {} holds

( P is feasible & P is projection-morphisms )

proof end;

definition

let C be category;

end;
attr C is with_products means :Def8: :: ALTCAT_5:def 8

for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms );

for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms );

:: deftheorem Def8 defines with_products ALTCAT_5:def 8 :

for C being category holds

( C is with_products iff for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms ) );

for C being category holds

( C is with_products iff for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms ) );

registration
end;

definition

let C be category;

let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

end;
let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

attr B is A -CatProduct-like means :: ALTCAT_5:def 9

ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms );

ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms );

:: deftheorem defines -CatProduct-like ALTCAT_5:def 9 :

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C holds

( B is A -CatProduct-like iff ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms ) );

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C holds

( B is A -CatProduct-like iff ex P being MorphismsFamily of B,A st

( P is feasible & P is projection-morphisms ) );

registration

let C be with_products category;

let I be set ;

let A be ObjectsFamily of I,C;

existence

ex b_{1} being Object of C st b_{1} is A -CatProduct-like

end;
let I be set ;

let A be ObjectsFamily of I,C;

existence

ex b

proof end;

registration

let C be category;

let A be ObjectsFamily of {},C;

coherence

for b_{1} being Object of C st b_{1} is A -CatProduct-like holds

b_{1} is terminal

end;
let A be ObjectsFamily of {},C;

coherence

for b

b

proof end;

theorem :: ALTCAT_5:5

for C being category

for A being ObjectsFamily of {},C

for B being Object of C st B is terminal holds

B is A -CatProduct-like

for A being ObjectsFamily of {},C

for B being Object of C st B is terminal holds

B is A -CatProduct-like

proof end;

theorem :: ALTCAT_5:6

for I being set

for C being category

for A being ObjectsFamily of I,C

for C1, C2 being Object of C st C1 is A -CatProduct-like & C2 is A -CatProduct-like holds

C1,C2 are_iso

for C being category

for A being ObjectsFamily of I,C

for C1, C2 being Object of C st C1 is A -CatProduct-like & C2 is A -CatProduct-like holds

C1,C2 are_iso

proof end;

definition

let I be set ;

let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: product A in E ;

coherence

product A is Object of (EnsCat E) by A1, ALTCAT_1:def 14;

end;
let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: product A in E ;

coherence

product A is Object of (EnsCat E) by A1, ALTCAT_1:def 14;

:: deftheorem Def10 defines EnsCatProductObj ALTCAT_5:def 10 :

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

EnsCatProductObj A = product A;

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

EnsCatProductObj A = product A;

definition

let I be set ;

let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: product A in E ;

ex b_{1} being MorphismsFamily of EnsCatProductObj A,A st

for i being set st i in I holds

b_{1} . i = proj (A,i)

for b_{1}, b_{2} being MorphismsFamily of EnsCatProductObj A,A st ( for i being set st i in I holds

b_{1} . i = proj (A,i) ) & ( for i being set st i in I holds

b_{2} . i = proj (A,i) ) holds

b_{1} = b_{2}

end;
let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: product A in E ;

func EnsCatProduct A -> MorphismsFamily of EnsCatProductObj A,A means :Def11: :: ALTCAT_5:def 11

for i being set st i in I holds

it . i = proj (A,i);

existence for i being set st i in I holds

it . i = proj (A,i);

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines EnsCatProduct ALTCAT_5:def 11 :

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

for b_{4} being MorphismsFamily of EnsCatProductObj A,A holds

( b_{4} = EnsCatProduct A iff for i being set st i in I holds

b_{4} . i = proj (A,i) );

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

for b

( b

b

theorem Th7: :: ALTCAT_5:7

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E & product A = {} holds

EnsCatProduct A = I --> {}

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E & product A = {} holds

EnsCatProduct A = I --> {}

proof end;

theorem Th8: :: ALTCAT_5:8

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )

proof end;

theorem :: ALTCAT_5:9

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

EnsCatProductObj A is A -CatProduct-like

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st product A in E holds

EnsCatProductObj A is A -CatProduct-like

proof end;

theorem :: ALTCAT_5:10

for E being non empty set st ( for I being set

for A being ObjectsFamily of I,(EnsCat E) holds product A in E ) holds

EnsCat E is with_products

for A being ObjectsFamily of I,(EnsCat E) holds product A in E ) holds

EnsCat E is with_products

proof end;