[Haskell-beginners] Category question

[Manfred Lotz]

On Mon, 28 May 2012 10:04:33 -0400
Brent Yorgey <byorgey at seas.upenn.edu> wrote:

> On Mon, May 28, 2012 at 02:08:14PM +0200, Manfred Lotz wrote:
> > On Mon, 28 May 2012 13:34:01 +0200
> > Alessandro Pezzoni <alessandro_pezzoni at lavabit.com> wrote:
> > 
> > > On Mon, May 28, 2012 at 11:54:11AM +0200, Manfred Lotz wrote:
> > > > In the definition of a (mathematical) category it is said (among
> > > > other things), that for any object A there exists an identity
> > > > morphism:
> > > >
> > > > idA: A -> A and if f: A -> B for two objects A, B then
> > > >
> > > >    idB . f = f and f . idA = f
> > > >
> > > > must hold.
> > > >
> > > > My question: Because I cannot think of any counterexample for
> > > > the last statement I would like to know if I just could omit
> > > > this from the definition and formulate this as a small theorem.
> > > >
> > > > Or does there exist a counterexample where all conditions of a
> > > > category hold but there exist two objects A, and B where we have
> > > > idB . f <> f and/or f .idA <> f?
> > > 
> > > When you ask that
> > >   idB . f = f    and    f . idA = f
> > > you are basically defining a left and a right identity,
> > > respectively.
> > > 
> > > If I get your question correctly, you are asking if you can drop
> > > the axiom (requirement) of existence of an identity morphism for
> > > every object and deduce it from the other axioms, i.e. that the
> > > composition of morphisms is always well defined and that it is
> > > associative.
> > > 
> > 
> > No, I do not want to drop the requirement of existence of an
> > identity morphism. I only want to drop the axion that idB .f = f
> > and f . idA = f do hold because IMHO this follows readily from the
> > definition of what an identity morphism is all about.
> 
> "Follows readily from the definition of what an identity morphism is
> all about" -- and what exactly is that defintion?
> 

For me id: A -> A could be defined by: A morphism id: A -> A is
called identity morphism iff for all x of A we have  id(x) = x.

IMHO, from this the following follows readily.


> In fact, the definition is precisely that
> 
>   idB . f = f and f . idA = f
> 
> This is not an "extra" requirement on identity morphisms.  It is
> simply the definition.
> 

I agree that I could define id by these two statements.

My point is that in the books about category theory those two statements
are stated as axioms, and id is (in many books) just self understood or
defined as I have defined it above.

If in a book about category the author would say that for each object A
there must exist a morphism id: A -> A (called identity morphism) which
is defined by idB . f = f and f . idA = f then this would be clearer
(and better, IMHO).

-- 
Manfred










-- 
Manfred