This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-sect

Description: Function returning the section relation in a category. Given arrows f : X --> Y and g : Y --> X , we say f Sect g , that is, f is a section of g , if g o. f = 1X . If there there is an arrow g with f Sect g , the arrow f is called a section, see definition 7.19 of Adamek p. 106. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-sect 
|- Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csect 
 |-  Sect
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  c
6 5 4 cfv 
 |-  ( Base ` c )
7 vy 
 |-  y
8 vf 
 |-  f
9 vg 
 |-  g
10 chom 
 |-  Hom
11 5 10 cfv 
 |-  ( Hom ` c )
12 vh 
 |-  h
13 8 cv 
 |-  f
14 3 cv 
 |-  x
15 12 cv 
 |-  h
16 7 cv 
 |-  y
17 14 16 15 co 
 |-  ( x h y )
18 13 17 wcel 
 |-  f e. ( x h y )
19 9 cv 
 |-  g
20 16 14 15 co 
 |-  ( y h x )
21 19 20 wcel 
 |-  g e. ( y h x )
22 18 21 wa 
 |-  ( f e. ( x h y ) /\ g e. ( y h x ) )
23 14 16 cop 
 |-  <. x , y >.
24 cco 
 |-  comp
25 5 24 cfv 
 |-  ( comp ` c )
26 23 14 25 co 
 |-  ( <. x , y >. ( comp ` c ) x )
27 19 13 26 co 
 |-  ( g ( <. x , y >. ( comp ` c ) x ) f )
28 ccid 
 |-  Id
29 5 28 cfv 
 |-  ( Id ` c )
30 14 29 cfv 
 |-  ( ( Id ` c ) ` x )
31 27 30 wceq 
 |-  ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x )
32 22 31 wa 
 |-  ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) )
33 32 12 11 wsbc 
 |-  [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) )
34 33 8 9 copab 
 |-  { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) }
35 3 7 6 6 34 cmpo 
 |-  ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } )
36 1 2 35 cmpt 
 |-  ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )
37 0 36 wceq 
 |-  Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )