YAP (was Re: Proposal: Remove Show and Eq superclasses of Num)

[Tyson Whitehead]

On November 3, 2011 12:11:19 Paterson, Ross wrote:
> Tyson Whitehead writes:
> > I see an integral domain is just a commutative ring with no zero divisors
> > (and every euclidean domain is also an integral domain)
> >
> > http://en.wikipedia.org/wiki/Integral_domain
> >
> > If I'm understanding you then this is sufficient structure to tell us
> > that an associate and unit decomposition exists, even if we can't
> > compute it.
> >
> > I spent sometime last night trying to figure out what about this
> > structure guarantees such a decomposition.  I didn't have much luck
> > though.  Any hints?
>
> Units are invertible elements, and two elements are associates if they're
> factors of each other.  So association is an equivalence relation; in
> particular the associates of 1 are the units, and the only associate of
> 0 is itself.
>
> Now choose a member from each association equivalence class to be the
> canonical associate for all the members of that class, choosing 1 as
> the canonical associate for the unit class.  Because there are no zero
> divisors, that uniquely determines the canonical unit for each element.

To see if I've got this correct.

1 - All invertable elements are associates of 1

 - for all x and x' inverses, x * 1 = x, x' * 1 = x', and x * x' = 1, so
 - 1, x, and x' are associates (x * x'^2 = x' and x^2 * x' = x)

2 - The only associate of 0 is 0

 - an associate of 0 would require 0 to be a factor, so
 - the lack of zero divisors means only 0 itself statisfies this requirement

3 Fixing cannonical associates uniquely determines the cannonical units

 - for all x /= 0 we have a cannonical associate x# /= 0, this means
 - x and x# are factors of each other so there are unique a and b such that
 - x = x# * a and x# = x * b, which in turn gives
 - x = x# * a = x * b * a, which means
 - b * a = 1, which means a and b are units (invertable), so
 - x = x# * a satisfies the decomposition (and x# determines a)

It would, therefore, seem to me that the key observation this encoding is
expressing is that two elements being being factors of each other implies they
are nessesarily related by an invertable multiple.

I guess then that the set of associates is also completely characterized as
any of its elements multiplied by all unit (invertable) elements.

Thanks very much for the clarification.

Cheers!  -Tyson