Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | crhmsubc.c | |- C = ( U i^i CRing ) |
|
| crhmsubc.j | |- J = ( r e. C , s e. C |-> ( r RingHom s ) ) |
||
| Assertion | crhmsubc | |- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | crhmsubc.c | |- C = ( U i^i CRing ) |
|
| 2 | crhmsubc.j | |- J = ( r e. C , s e. C |-> ( r RingHom s ) ) |
|
| 3 | crngring | |- ( r e. CRing -> r e. Ring ) |
|
| 4 | 3 | rgen | |- A. r e. CRing r e. Ring |
| 5 | 4 1 2 | srhmsubc | |- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) ) |