12.1.1 List of Omitted Proofs

Не так благотворна истина, как зловредна ее видимость.

Даниил Данковский

Truth does not do as much good in the world as the appearance of truth does evil.

Daniil Dankovsky

There’s a very large number of omitted proofs throughout these notes. Here we list them in decreasing order of importance, noting also whether they rely on material that has yet to be developed, marked by a sign. This list is under construction.

Proofs that need to be added at some point:

  1. Chapter 5: Tensor Products of Pointed Sets, .
  2. Chapter 5: Tensor Products of Pointed Sets, .
  3. Horizontal composition of natural transformations is associative: Chapter 9: Preorders, Item 2 of Proposition 9.9.5.1.3.
  4. Fully faithful functors are essentially injective: Chapter 9: Preorders, Item 4 of Proposition 9.6.3.1.2.

Proofs that would be very nice to be added at some point:

  1. Properties of pseudomonic functors: Chapter 9: Preorders, Proposition 9.7.4.1.2.
  2. Characterisation of fully faithful functors: Chapter 9: Preorders, Item 1 of Proposition 9.6.3.1.2.
  3. The quadruple adjunction between categories and sets: Chapter 9: Preorders, Proposition 9.3.1.1.1.
  4. $F_{*}$ faithful iff $F$ faithful: Chapter 9: Preorders, Item 2 of Proposition 9.6.1.1.2.
  5. Properties of groupoid completions: Chapter 9: Preorders, Proposition 9.4.3.1.3.
  6. Properties of cores: Chapter 9: Preorders, Proposition 9.4.4.1.4.
  7. $\mathrm{Rel}$ is isomorphic to the category of free algebras of the powerset monad: Chapter 6: Relations, Proposition 6.3.14.1.1.
  8. Non/existence of left Kan extensions in $\textbf{Rel}$:
    1. Chapter 7: Constructions With Relations, Item 1 of Proposition 7.2.1.1.1.
    2. Chapter 7: Constructions With Relations, Item 2 of Proposition 7.2.1.1.1.
  9. Non/existence of left Kan lifts in $\textbf{Rel}$:
    1. Chapter 7: Constructions With Relations, Item 1 of Proposition 7.2.2.1.1.
    2. Chapter 7: Constructions With Relations, Item 2 of Proposition 7.2.2.1.1.

Proofs that would be nice to be added at some point:

  1. Quotient by an equivalence relation is a coequaliser: Chapter 2: Constructions With Sets, Example 2.2.5.1.4.
  2. Quotient by an equivalence relation is a coequaliser, repetition: , .
  3. Properties of posetal categories: Chapter 9: Preorders, Proposition 9.2.7.1.2.
  4. Injective on objects functors are precisely the isocofibrations in $\mathsf{Cats}_{\mathsf{2}}$: Chapter 9: Preorders, Item 1 of Proposition 9.8.1.1.2.
  5. Characterisations of monomorphisms of categories: Chapter 9: Preorders, Item 1 of Proposition 9.7.2.1.2.
  6. Epimorphisms of categories are surjective on objects: Chapter 9: Preorders, Item 2 of Proposition 9.7.3.1.2.
  7. Properties of pseudoepic functors: Chapter 9: Preorders, Proposition 9.7.5.1.2.

Proofs that would be nice but not essential to be added at some point:

  1. Proof that $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\text{Ø},\times ,\text{pt}\webright )$ is a symmetric bimonoidal category: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.1.3.1.3.
  2. Proof that $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\text{Ø},\times ,\text{pt}\webright )$ is a symmetric bimonoidal category: Chapter 3: Monoidal Structures on the Category of Sets, Proposition 3.3.5.1.1.
  3. Proof that $\webleft (\mathsf{Sets},\times _{X},X\webright )$ is a symmetric monoidal category: Chapter 2: Constructions With Sets, Item 10 of Proposition 2.1.4.1.5.
  4. Proof that $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\text{Ø}\webright )$ is a symmetric monoidal category: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.2.3.1.3.
  5. Proof that $\webleft (\mathsf{Sets},\mathbin {\textstyle \coprod _{X}},X\webright )$ is a symmetric monoidal category: Chapter 2: Constructions With Sets, Item 7 of Proposition 2.2.4.1.6.

Proofs that have been (temporarily) omitted because they are “clear”, “straightforward”, or “tedious”:

  1. Properties of products of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 3 of Proposition 2.1.3.1.3.
    2. Left Unitality: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    3. Right Unitality: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    4. Commutativity: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.1.3.1.3.
    5. Left Distributivity Over Coproducts: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    6. Right Distributivity Over Coproducts: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    7. Left Annihilation With the Empty Set: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    8. Right Annihilation With the Empty Set: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    9. Symmetric Monoidality: Chapter 2: Constructions With Sets, Item 13 of Proposition 2.1.3.1.3.
    10. Symmetric Bionoidality: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.1.3.1.3.
  2. Properties of coproducts of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.3.1.3.
    2. Left unitality: Chapter 2: Constructions With Sets, of Proposition 2.2.3.1.3.
    3. Right unitality: Chapter 2: Constructions With Sets, of Proposition 2.2.3.1.3.
    4. Commutativity: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.3.1.3.
  3. Properties of pushouts of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.4.1.6.
    2. Unitality: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.4.1.6.
    3. Commutativity: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.2.4.1.6.
    4. Pushout of sets over the empty set recovers the coproduct of sets: Chapter 2: Constructions With Sets, Item 6 of Proposition 2.2.4.1.6.
  4. Properties of coequalisers of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.2.5.1.5.
    2. Unitality: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.5.1.5.
    3. Commutativity: Chapter 2: Constructions With Sets, Item 3 of Proposition 2.2.5.1.5.
    4. Interaction with composition: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.5.1.5.
  5. Properties of set differences:
    1. Chapter 2: Constructions With Sets, Item 4 of Proposition 2.3.10.1.2.
    2. Chapter 2: Constructions With Sets, Item 11 of Proposition 2.3.10.1.2.
    3. Chapter 2: Constructions With Sets, Item 15 of Proposition 2.3.10.1.2.
  6. Complements and characteristic functions: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.3.11.1.2.
  7. Properties of symmetric differences:
    1. Chapter 2: Constructions With Sets, Item 1 of Proposition 2.3.12.1.2.
    2. Chapter 2: Constructions With Sets, Item 1 of Proposition 2.3.12.1.2.
    3. Chapter 2: Constructions With Sets, Item 16 of Proposition 2.3.12.1.2.
    4. Chapter 2: Constructions With Sets, Item 18 of Proposition 2.3.12.1.2.
    5. Chapter 2: Constructions With Sets, Item 19 of Proposition 2.3.12.1.2.
  8. The Yoneda lemma for sets: Chapter 2: Constructions With Sets, Proposition 2.5.5.1.1.
  9. Co/completeness of powersets: Chapter 2: Constructions With Sets, of .
  10. Properties of direct images:
    1. Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.1.1.4.
    2. Interaction with coproducts: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.1.1.4.
    3. Interaction with products: Chapter 2: Constructions With Sets, Item 16 of Proposition 2.6.1.1.4.
  11. Properties of inverse images:
    1. Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.2.1.3.
    2. Interaction with coproducts: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.2.1.3.
    3. Interaction with products; Chapter 2: Constructions With Sets, Item 16 of Proposition 2.6.2.1.3.
  12. Properties of direct images with compact support:
    1. Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.3.1.6.
    2. Lax preservation of colimits: Chapter 2: Constructions With Sets, Item 10 of Proposition 2.6.3.1.6.
    3. Interaction with coproducts: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.6.3.1.6.
    4. Interaction with products: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.3.1.6.
  13. Left distributor of $\times $ over $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.1.1.1.
  14. Right distributor of $\times $ over $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.2.1.1.
  15. Left annihilator of $\times $ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.3.1.1.
  16. Right annihilator of $\times $ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.4.1.1.
  17. Properties of wedge products of pointed sets:
    1. Associativity: Chapter 4: Pointed Sets, Item 2 of Proposition 4.3.3.1.2.
    2. Unitality: Chapter 4: Pointed Sets, Item 3 of Proposition 4.3.3.1.2.
    3. Commutativity: Chapter 4: Pointed Sets, Item 4 of Proposition 4.3.3.1.2.
    4. Symmetric monoidality: Chapter 4: Pointed Sets, Item 5 of Proposition 4.3.3.1.2.
  18. Properties of pushouts of pointed sets:
    1. Interaction with coproducts: Chapter 4: Pointed Sets, Item 5 of Proposition 4.3.4.1.2.
    2. Symmetric monoidality: Chapter 4: Pointed Sets, Item 6 of Proposition 4.3.4.1.2.
  19. Properties of free pointed sets:
    1. Functoriality: Chapter 4: Pointed Sets, Item 1 of Proposition 4.4.1.1.2.
  20. $\mathrm{Rel}$ with $\times $ is closed symmetric monoidal: Chapter 6: Relations, Proposition 6.2.3.8.1.
  21. Properties of graphs:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.1.1.2.
    2. Interaction With Inverses: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.3.1.1.2.
  22. Properties of inverses of functions (as relations):
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.2.1.2.
    2. Interaction With Inverses of Relations: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.3.2.1.2.
  23. Binary unions of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.5.1.2.
  24. Unions of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.6.1.2.
  25. Binary Intersections of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.7.1.2.
  26. Intersections of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.8.1.2.
  27. Properties of inverses of relations: all items of Chapter 7: Constructions With Relations, Proposition 7.3.11.1.3.
  28. Properties of composition of relations: some items of Chapter 7: Constructions With Relations, Proposition 7.3.12.1.3.
  29. Properties of collages of relations: all items of Chapter 7: Constructions With Relations, Proposition 7.3.13.1.2.
  30. Properties of direct images of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.1.1.3.
    2. Oplax Preservation of Limits: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.4.1.1.3.
  31. Properties of strong inverse images of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.2.1.3.
    2. Lax Preservation of Colimits: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.4.2.1.3.
  32. Properties of weak inverse images of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.3.1.3.
    2. Oplax Preservation of Limits: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.4.3.1.3.
  33. Properties of direct images with compact support of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.4.1.3.
    2. Lax Preservation of Colimits: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.4.4.1.3.
  34. Functoriality of Powersets II: Chapter 7: Constructions With Relations, Proposition 7.4.6.1.3.
  35. Proof that the reflexive closure of a relation satisfies the appropriate universal property: Chapter 8: Conditions on Relations, Construction 8.1.2.1.2.
  36. Properties of Symmetric Relations, Chapter 8: Conditions on Relations, Proposition 8.2.1.1.4.
  37. Proof that the symmetric closure of a relation satisfies the appropriate universal property: Chapter 8: Conditions on Relations, Construction 8.2.2.1.2.
  38. Properties of the symmetric closure of a relation:
    1. Chapter 8: Conditions on Relations, Item 2 of Proposition 8.2.2.1.3.
    2. Chapter 8: Conditions on Relations, Item 4 of Proposition 8.2.2.1.3.
  39. Properties of transitive relations, Chapter 8: Conditions on Relations, Proposition 8.3.1.1.4.
  40. Proof that the transitive closure of a relation satisfies the appropriate universal property: Chapter 8: Conditions on Relations, Construction 8.3.2.1.2.
  41. Properties of the transitive closure of a relation:
    1. Chapter 8: Conditions on Relations, Item 2 of Proposition 8.3.2.1.3.
  42. Chapter 8: Conditions on Relations, of .
  43. Properties of Quotient Sets, Chapter 8: Conditions on Relations, Proposition 8.5.2.1.3:
    1. Chapter 8: Conditions on Relations, Item 1 of Proposition 8.5.2.1.3.
    2. Chapter 8: Conditions on Relations, Item 2 of Proposition 8.5.2.1.3.
    3. Chapter 8: Conditions on Relations, Item 3 of Proposition 8.5.2.1.3.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: