:: 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 b₁ being Relation st b₁ is empty holds
b₁ 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 b₁ being category st
( b₁ is functional & b₁ 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 b₁ being AltGraph st
( b₁ is functional & b₁ is strict )

proof end;

end;

registration

cluster non empty V62() strict V71() with_units functional for AltCatStr ;

existence
ex b₁ being category st
( b₁ is functional & b₁ 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 b₁ 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₁ . 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 b₅ being ManySortedSet of I holds
( b₅ 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₅ . 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 b₁ being ManySortedSet of I holds
( b₁ is MorphismsFamily of o,f iff for i being Element of I holds b₁ . 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 b₅ being ManySortedSet of I holds
( b₅ is MorphismsFamily of o,f iff for i being Element of I holds b₅ . 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 b₁ being MorphismsFamily of o,f holds b₁ 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 b₁ being MorphismsFamily of B,A holds b₁ 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 b₁ being category st b₁ 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 b₁ being Object of C st b₁ 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 b₁ being Object of C st b₁ is A -CatProduct-like holds
b₁ 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 b₁ being MorphismsFamily of EnsCatProductObj A,A st
for i being set st i in I holds
b₁ . i = proj (A,i)

proof end;

uniqueness
for b₁, b₂ being MorphismsFamily of EnsCatProductObj A,A st ( for i being set st i in I holds
b₁ . i = proj (A,i) ) & ( for i being set st i in I holds
b₂ . i = proj (A,i) ) holds
b₁ = b₂

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 b₄ being MorphismsFamily of EnsCatProductObj A,A holds
( b₄ = EnsCatProduct A iff for i being set st i in I holds
b₄ . 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;