MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sect Unicode version

Definition df-sect 13666
Description: Function returning the section relation in a category. Given arrows  f : X --> Y and  g : Y --> X, we say  fSect g, that is,  f is a section of  g, if  g  o.  f  =  1 `  X. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
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 ) ) } ) )
Distinct variable group:    f, c, g, h, x, y

Detailed syntax breakdown of Definition df-sect
StepHypRef Expression
1 csect 13663 . 2  class Sect
2 vc . . 3  set  c
3 ccat 13582 . . 3  class  Cat
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1631 . . . . 5  class  c
7 cbs 13164 . . . . 5  class  Base
86, 7cfv 5271 . . . 4  class  ( Base `  c )
9 vf . . . . . . . . . 10  set  f
109cv 1631 . . . . . . . . 9  class  f
114cv 1631 . . . . . . . . . 10  class  x
125cv 1631 . . . . . . . . . 10  class  y
13 vh . . . . . . . . . . 11  set  h
1413cv 1631 . . . . . . . . . 10  class  h
1511, 12, 14co 5874 . . . . . . . . 9  class  ( x h y )
1610, 15wcel 1696 . . . . . . . 8  wff  f  e.  ( x h y )
17 vg . . . . . . . . . 10  set  g
1817cv 1631 . . . . . . . . 9  class  g
1912, 11, 14co 5874 . . . . . . . . 9  class  ( y h x )
2018, 19wcel 1696 . . . . . . . 8  wff  g  e.  ( y h x )
2116, 20wa 358 . . . . . . 7  wff  ( f  e.  ( x h y )  /\  g  e.  ( y h x ) )
2211, 12cop 3656 . . . . . . . . . 10  class  <. x ,  y >.
23 cco 13236 . . . . . . . . . . 11  class comp
246, 23cfv 5271 . . . . . . . . . 10  class  (comp `  c )
2522, 11, 24co 5874 . . . . . . . . 9  class  ( <.
x ,  y >.
(comp `  c )
x )
2618, 10, 25co 5874 . . . . . . . 8  class  ( g ( <. x ,  y
>. (comp `  c )
x ) f )
27 ccid 13583 . . . . . . . . . 10  class  Id
286, 27cfv 5271 . . . . . . . . 9  class  ( Id
`  c )
2911, 28cfv 5271 . . . . . . . 8  class  ( ( Id `  c ) `
 x )
3026, 29wceq 1632 . . . . . . 7  wff  ( g ( <. x ,  y
>. (comp `  c )
x ) f )  =  ( ( Id
`  c ) `  x )
3121, 30wa 358 . . . . . 6  wff  ( ( f  e.  ( x h y )  /\  g  e.  ( y
h x ) )  /\  ( g (
<. x ,  y >.
(comp `  c )
x ) f )  =  ( ( Id
`  c ) `  x ) )
32 chom 13235 . . . . . . 7  class  Hom
336, 32cfv 5271 . . . . . 6  class  (  Hom  `  c )
3431, 13, 33wsbc 3004 . . . . 5  wff  [. (  Hom  `  c )  /  h ]. ( ( f  e.  ( x h y )  /\  g  e.  ( y h x ) )  /\  (
g ( <. x ,  y >. (comp `  c ) x ) f )  =  ( ( Id `  c
) `  x )
)
3534, 9, 17copab 4092 . . . 4  class  { <. 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 ) ) }
364, 5, 8, 8, 35cmpt2 5876 . . 3  class  ( 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 ) ) } )
372, 3, 36cmpt 4093 . 2  class  ( 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 ) ) } ) )
381, 37wceq 1632 1  wff 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 ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  sectffval  13669
  Copyright terms: Public domain W3C validator