:: Products in Categories without Uniqueness of { \bf cod } and { \bf dom }
:: by Artur Korni{\l}owicz
::
:: Received August 19, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


registration
cluster empty Relation-like -> {} -defined for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is {} -defined
proof end;
end;

definition
let C be AltGraph ;
attr C is functional means :Def1: :: ALTCAT_5:def 1
 for a, b being Object of C holds <^a,b^> is functional ;
end;

:: 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 );

registration
let E be non empty set ;
cluster EnsCat E -> functional ;
coherence
EnsCat E is functional
proof end;
end;

registration
cluster non empty V62() strict V71() with_units functional for AltCatStr ;
existence
ex b1 being category st
( b1 is functional & b1 is strict )
proof end;
end;

registration
let C be functional AltCatStr ;
cluster AltGraph(# the carrier of C, the Arrows of C #) -> functional ;
coherence
AltGraph(# the carrier of C, the Arrows of C #) is functional
proof end;
end;

registration
cluster strict functional for AltGraph ;
existence
ex b1 being AltGraph st
( b1 is functional & b1 is strict )
proof end;
end;

registration
cluster non empty V62() strict V71() with_units functional for AltCatStr ;
existence
ex b1 being category st
( b1 is functional & b1 is strict )
proof end;
end;

registration
let C be functional AltGraph ;
let a, b be Object of C;
cluster <^a,b^> -> functional ;
coherence
<^a,b^> is functional by Def1;
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^> )
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;

Lm4: now :: thesis: for o1, o being Object of (EnsCat {{}})
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;

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;

Lm6: now :: thesis: for o1, o being Object of (EnsCat {{}})
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;

definition
let C be non empty AltCatStr ;
let I be set ;
mode ObjectsFamily of I,C is Function of I,C;
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;
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
ex b1 being ManySortedSet of I st
for i being object st i in I holds
ex o1 being Object of C st
( o1 = f . i & b1 . i is Morphism of o,o1 )
proof end;
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 b5 being ManySortedSet of I holds
( b5 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 & b5 . i is Morphism of o,o1 ) );

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;
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 b1 being ManySortedSet of I holds
( b1 is MorphismsFamily of o,f iff for i being Element of I holds b1 . i is Morphism of o,(f . i) )
proof end;
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 b5 being ManySortedSet of I holds
( b5 is MorphismsFamily of o,f iff for i being Element of I holds b5 . i is Morphism of o,(f . i) );

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;

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;
cluster -> Function-yielding for MorphismsFamily of o,f;
coherence
for b1 being MorphismsFamily of o,f holds b1 is Function-yielding
proof end;
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
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;
attr P is feasible means :: ALTCAT_5:def 4
 for i being set st i in I holds
ex o being Object of C st
( o = A . i & P . i in <^B,o^> );
end;

:: 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^> ) );

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;
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
( P is feasible iff for i being Element of I holds P . i in <^B,(A . i)^> )
proof end;
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)^> );

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;
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 ) );
end;

:: 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 ) ) );

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;
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
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;
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 ) ) );

registration
let C be category;
let A be ObjectsFamily of {},C;
let B be Object of C;
cluster -> feasible for MorphismsFamily of B,A;
coherence
for b1 being MorphismsFamily of B,A holds b1 is feasible ;
end;

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 )
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
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 )
proof end;

definition
let C be category;
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 );
end;

:: 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 ) );

registration
cluster EnsCat {{}} -> with_products ;
coherence
EnsCat {{}} is with_products
proof end;
end;

registration
cluster non empty V62() V71() with_units with_products for AltCatStr ;
existence
ex b1 being category st b1 is with_products
proof end;
end;

definition
let C be category;
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 );
end;

:: 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 ) );

registration
let C be with_products category;
let I be set ;
let A be ObjectsFamily of I,C;
cluster A -CatProduct-like for Element of the carrier of C;
existence
ex b1 being Object of C st b1 is A -CatProduct-like
proof end;
end;

registration
let C be category;
let A be ObjectsFamily of {},C;
cluster A -CatProduct-like -> terminal for Element of the carrier of C;
coherence
for b1 being Object of C st b1 is A -CatProduct-like holds
b1 is terminal
proof end;
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
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
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 ;
func EnsCatProductObj A -> Object of (EnsCat E) equals :Def10: :: ALTCAT_5:def 10
 product A;
coherence
product A is Object of (EnsCat E) by A1, ALTCAT_1:def 14;
end;

:: 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;

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 ;
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
ex b1 being MorphismsFamily of EnsCatProductObj A,A st
for i being set st i in I holds
b1 . i = proj (A,i)
proof end;
uniqueness
for b1, b2 being MorphismsFamily of EnsCatProductObj A,A st ( for i being set st i in I holds
b1 . i = proj (A,i) ) & ( for i being set st i in I holds
b2 . i = proj (A,i) ) holds
b1 = b2
proof end;
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 b4 being MorphismsFamily of EnsCatProductObj A,A holds
( b4 = EnsCatProduct A iff for i being set st i in I holds
b4 . i = proj (A,i) );

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 --> {}
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 )
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
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
proof end;