Email Gateway (Aug 19 2022 at 11:46): Email Gateway (Aug 19 2022 at 11:46):From: Josh Tilles <merelyapseudonym@gmail.com>
BRIEFLY:
I'm going through a few books related to Category Theory and I'm interested
in doing many of the exercises in Isabelle/Isar. Are there any libraries
out there that have already laid the groundwork for "arrow-oriented" proofs?
EXPLANATION/DETAIL:
If it helps to make my scope clearer, let me list the books that I'm using:
- Conceptual
Mathematics<http://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/conceptual-mathematics-first-introduction-categories-2nd-edition>
by
Bill Lawvere and Stephen Schanuel
- Algebra: Chapter
0<http://www.math.fsu.edu/~aluffi/mainhtmls/pubs.html#Chapter0> by
Paolo Aluffi
- Arrows, Structures, and Functors: The Categorical
Imperative<http://books.google.com/books/about/Arrows_structures_and_functors.html?id=2txQAAAAMAAJ>
by
Michael Arbib and Ernest Manes
- Topoi: the Categorial Analysis of
Logic<http://ebooks.library.cornell.edu/cgi/t/text/text-idx?c=math;idno=gold010>
by
Robert Goldblatt
I'm aware of the two Category Theory AFP entries (Greg
O'Keefe's<http://afp.sourceforge.net/entries/Category.shtml>
and Alexander Katovsky's<http://afp.sourceforge.net/entries/Category2.shtml>),
but although I'm not _familiar_ with their details, they appear to go
deeper into Category Theory than I need right now. At the very least, it's
not yet clear to me what parts of their theories are "general-purpose".
In the hopes of ensuring that my goals are clear, let me also provide some
representative exercises that I'd like to solve using Isabelle/Isar.
- Prove that for every function $f : A -> B$ with $A$ non-empty, there
exists a 'choice function' $g : B -> A$ such that $f . g . f = f$. In
axiomatic set theory this is an acceptable form of the 'axiom of choice'
Arbib & Manes, Exercise 1.1.2
- A finite set $A$ has an even number of elements iff (i.e. if and only
if) there is an involution on $A$ with no fixed points; $A$ has an odd
number of elements iff there is an involution on $A$ with just one fixed
point.
Lawvere & Schanuel, Exercise III.3
- Prove that final [i.e., terminal] objects are unique up to isomorphism.
Aluffi, Exercise I.5.3
- The disjoint union is a coproduct in the the category of sets.
Aluffi, Proposition I.5.6
- Any map $p$ which is an equalizer of some pair of maps is itself a
monomorphism
Lawvere & Schanuel, Exercise 27.6
- Prove that a category with initial and terminal objects has 'zero
maps' if and only if an initial object is isomorphic to a terminal object.
Lawvere & Schanuel, Exercise 26.2
- [Prove that] every group is the group of isomorphisms of a groupoid.
In particular, every group is the group of automorphisms of some object in
some category.
Aluffi, Exercise II.1.1
It's not that I have no idea how to approach these; I'd just like to know
if I'm "reinventing the wheel".
Cheers,
--Josh Tilles
Email Gateway (Aug 19 2022 at 11:46):From: Tobias Nipkow <nipkow@in.tum.de>
There are two Category Theory entries in the AFP.
Tobias
Last updated: Apr 27 2024 at 01:05 UTC