CatDat/database/data/special-morphism-rules.yaml at main · ScriptRaccoon/CatDat · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
- property: groupoid
  kind: isomorphisms
  description: every morphism
  proof: The category is a groupoid.

- property: gaunt
  kind: isomorphisms
  description: only the identities
  proof: The category is gaunt.

- property: thin
  kind: monomorphisms
  description: every morphism
  proof: It is a thin category.

- property: thin
  kind: epimorphisms
  description: every morphism
  proof: It is a thin category.

- property: left cancellative
  kind: monomorphisms
  description: every morphism
  proof: The category is left cancellative.

- property: right cancellative
  kind: epimorphisms
  description: every morphism
  proof: The category is right cancellative.

- property: left cancellative
  kind: regular epimorphisms
  description: same as isomorphisms
  proof: The category is left cancellative, and a regular epimorphism which is a monomorphism must be an isomorphism.

- property: right cancellative
  kind: regular monomorphisms
  description: same as isomorphisms
  proof: The category is right cancellative, and a regular monomorphism which is an epimorphism must be an isomorphism.

- property: one-sorted finitary algebraic
  kind: isomorphisms
  description: bijective morphisms
  proof: 'This holds in every one-sorted finitary algebraic category: the inverse of a bijective morphism is again a morphism.'

- property: one-sorted finitary algebraic
  kind: monomorphisms
  description: injective morphisms
  proof: 'This holds in every one-sorted finitary algebraic category: the forgetful functor to sets is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'

- property: one-sorted finitary algebraic
  kind: regular epimorphisms
  description: surjective morphisms
  proof: 'This holds in every one-sorted finitary algebraic category: the construction of coequalizers shows that every regular epimorphism is surjective. Conversely, the fundamental theorem on homomorphisms states that every surjective homomorphism $A \to B$ is the coequalizer of the two projections $A \times_B A \rightrightarrows A$.'

- property: mono-regular
  kind: regular monomorphisms
  description: same as monomorphisms
  proof: The category is mono-regular.

- property: epi-regular
  kind: regular epimorphisms
  description: same as epimorphisms
  proof: The category is epi-regular.

- property: subobject-trivial
  kind: monomorphisms
  description: same as isomorphisms
  proof: The category is subobject-trivial.

- property: quotient-trivial
  kind: epimorphisms
  description: same as isomorphisms
  proof: The category is quotient-trivial.

- property: regular-subobject-trivial
  kind: regular monomorphisms
  description: same as isomorphisms
  proof: The category is regular-subobject-trivial.

- property: regular-quotient-trivial
  kind: regular epimorphisms
  description: same as isomorphisms
  proof: The category is regular-quotient-trivial.