- Grothendieck Completion
- > {-# OPTIONS -XNoMonomorphismRestriction -XExistentialQuantification #-}
- > import Data.Monoid
- > import Data.Set
- One of the experiences of learning mathematics is climbing the ladder
- of numbers from natural numbers to complex numbers:
- N < Z < Q < R < C
- Here I'll review how Z may be constructed from N by a general algebraic
- method and then see what that same method yields when applied to more
- arbitrary data types.
- We define natural numbers as Peano numerals.
- > data N = Zero | Succ N deriving (Eq, Show)
- A mathematician would say that we have made a free monoid on one
- generator (the Succ constructor).
- Addition is a simple matter of combining all the generators.
- > addN Zero n = n
- > addN (Succ m) n = Succ (addN m n)
- This makes N into a monoid.
- > instance Monoid N where
- > mempty = Zero
- > mappend = addN
- As a matter of syntactic convenience, we'll use an infix operator for
- the monoid operation and use a shorthand for the unit.
- > e = mempty
- > (>>>) = mappend
- The left-to-right bias of >>> is intended. Later we will be working with
- non-commutative monoids.
- The e is shorthand for Einheit, meaning unit, and is a common abbreviation
- in the literature. If you don't like it, tough! Blame Germany for producing
- so many influential algebraists and settling countless conventional one-letter
- abbreviations like K for fields (K for Körper).
- We'd like for N to be an instance of Num so we can use fromInteger. We don't
- care about the rest, so we leave them undefined.
- > instance Num N where
- > fromInteger n = iterate Succ Zero !! fromInteger n
- >
- > (+) = undefined
- > (*) = undefined
- > abs = undefined
- > signum = undefined
- Most of us are used to thinking of the integers Z as natural numbers with a
- sign prefixed. To construct Z from N, your first instinct is probably to define
- data Sign = Minus | Plus
- data Z = Z Sign N
- Indeed, that is one possible way to go. The only hitch is that you have to
- ensure that Z Plus Zero and Z Minus Zero are considered equal. The easiest
- way to achieve that is to use some consistent normalization:
- normalizeZ (Z Minus Zero) = Z Plus Zero
- normalizeZ n = n
- All functions that construct new integers must then call normalizeZ.
- However, there is also an alternative construction of Z from N. The idea is
- this: Rather than view the sign (plus or minus) as a prefix, we can view it
- as an infix between two numbers. That is, we know that every integer can be
- expressed as the difference of two naturals, so we should be able to represent
- integers as pairs of naturals (m, n), corresponding to the integer m - n.
- The mathematician Grothendieck invented a more general version of this
- construction to define the K_0 groups of K theory, and therefore it generally
- bears his name. You see variations on "Grothendieck construction", "Grothendieck
- completion" and "K-completion" thrown around. Here I'll refer to it as the
- Grothendieck completion as best describes its purpose of completing (in the
- sense of filling or perfecting) a monoid by adjoining formal inverses.
- > data Z = Z N N deriving Show
- With the sign-based representation, the only redundantly represented number
- was zero, expressible as either plus or minus zero. With this pair-based
- representation, there are far more redundancies. For example, 2 - 3 and
- 1 - 2 both represent the same number. More generally,
- m - n = m' - n'
- if and only if
- m + n' = m' + n
- As an aside, note how this looks like the rule for comparing fractions
- if you replace + and - by * and /. The only difference is that we allow
- our "denominators" to be zero.
- > instance Eq Z where
- > (Z m n) == (Z m' n') = (m >>> n') == (m' >>> n)
- Addition is now defined by simply adding entrywise, much like how fractions
- are multiplied by multiplying numerators and denominators separately.
- > addZ (Z m n) (Z m' n') = Z (m >>> m') (n >>> n')
- If no for other reason, this simple implementation of integer addition should
- make us appreciate this pair-based construction.
- Addition for sign-based integers is less symmetric and messier. It corresponds
- to addition in the pair-based representation, where Plus n and Minus n are
- interpreted as (n, Zero) and (Zero, n), followed by a normalization step that
- shifts all the Succ occurrences to one side or the other, depending on which is
- larger.
- > instance Monoid Z where
- > mempty = Z Zero Zero
- > mappend = addZ
- Everything should far should have been pretty simple. I hope you're convinced
- that this pair-based representation indeed produces a structure isomorphic to
- integers. However, let's review what we did in more general terms in an attempt
- to identify the assumptions that made it work out so well.
- We started with N, a free monoid on one generator. Because it only has a single
- generator, N is automatically commutative. While the monoidal operation (addition)
- is not generally invertible, N's freeness as a monoid does have a related
- property: If a >> b = a >> c then a = b. This makes N a cancelative monoid.
- Let's say we want to extend or complete N to make its operation invertible.
- That is, we want to make N a group. A group is just a monoid with a way of
- computing inverses for every element.
- > class Monoid g => Group g where
- > inverse :: g -> g
- For a Group instance to represent an actual group, the defining property
- of inverses must hold:
- x >>> inverse x = e
- inverse x >>> x = e
- This is easily implemented for our integer type Z. It's just a matter of
- swapping the entries in a pair.
- > instance Group Z where
- > inverse (Z m n) = (Z n m)
- As an aside, it's curious to see that the involution property of inverses
- follows from the fact that swapping pair entries twice does nothing!
- The group completion of N is a new algebraic object K N with a map
- inject :: N -> K N
- It is injective and therefore paired with a projection:
- project :: K N -> Maybe K
- Projection is the left inverse of injection:
- project . inject = Just
- Whatever else its properties, a basic requirement is that the injective image
- of N inside of K N should behave identically to N on its own. That is, if
- we zoom in on the part of K N that is the injective image of N then the
- dynamics should be indistinguishable from N's own dynamics. This is another
- way of saying that the injection is a monoid homomorphism:
- inject (x >>> y) = inject x >>> inject y
- The >>> on the left side is in N and the one on the right side is in K N.
- Let's return to the cancelation property and consider a general monoid M.
- We saw earlier that in the case of N, a cancelative monoid, we successfully
- got Z, a group, as the completion. What would happen if M were not cancelative?
- One case would be the natural numbers, this time with multiplication instead of
- addition. We can cancel most of the time but not when the multiplier is zero.
- Certainly 0 * 1 = 0 * 3 does not imply 1 = 3. In attempting to complete this M to
- K M the requirement that 'inject' is a homomorphism means that n * 0 = 0 for all n
- must also hold true in K M as well. But since every element, including 0, must have
- an inverse, we can take the equality like 0 * n = 0 and multiply both sides by the
- inverse of 0 to get n = 0. That is, the image of M inside K M is 0, so 'inject'
- certainly cannot be injective!
- Thus we see that a monoid must be cancelative to have a group completion.
- The other special fact about N is that it is a free monoid, and in particular it
- is a free monoid on one generator ("one-dimensional") and therefore commutative.
- What about free monoids on more generators, which would be non-commutative?
- For any type X we can consider the free monoid F X with a generator for every element
- in X. An element of F X is a word (possibly empty) drawn from the alphabet X and
- the monoid operation is concatenation. The free monoid construction is a functor,
- meaning every map X -> Y can be lifted to a map F X -> F Y on the free monoids.
- This F is of course none other than the type constructor for lists! The monoid operation
- is list concatenation and the identity element is the empty list. The lifting is our
- familiar friend map :: (a -> b) -> ([a] -> [b]).
- We have said multiple times that N is a free monoid on one generator. With this
- identification of the free monoid construction F with the type constructor for lists,
- this is simply a way of saying that N is isomorphic to [()] since () is the canonical
- type inhabited by a single value, also denoted ().
- What happens when we transfer our pairing construction to arbitrary free monoids?
- It's a straightforward matter of taking our code from Z and replacing every occurrence
- of N with an abstract type parameter:
- > data K m = K m m deriving Show
- >
- > instance Monoid m => Monoid (K m) where
- > mempty = K e e
- > mappend (K x y) (K x' y') = K (x >>> x') (y >>> y')
- >
- > instance Monoid m => Group (K m) where
- > inverse (K x y) = (K y x)
- >
- > instance (Monoid m, Eq m) => Eq (K m) where
- > (K x y) == (K x' y') = (x >>> y') == (x' >>> y)
- Injection and projection is now a simple matter:
- > inject x = (K x e)
- >
- > project (K x e) = Just x
- > project _ = Nothing
- It's easy to see that project . inject = Just. What about the homomorphism property?
- Can you prove that?
- We defined an instance of Group for K m but is it actually a group? So far we've only
- verified that directly for the type N, or equivalently [()]. Let's tackle the next
- simplest case, where the value type has two elements. We might as well pick the standard
- type Bool.
- *Main> let x = inject [True]
- *Main> x
- K [True] []
- *Main> inverse x
- K [] True
- *Main> x >>> inverse x
- K [True] [True]
- *Main> x >>> inverse x == e
- True
- Cool! But so far we have only used lists of one kind of value. Let's try more.
- *Main> let x = inject [True, False]
- *Main> x
- K [True,False] []
- *Main> inverse x
- K [] [True,False]
- *Main> x >>> inverse x == e
- True
- It seems to work alright. Let's try some experiments with an infinite value type. We'll
- use the integers.
- *Main> let a = inject [1]
- *Main> let b = inject [2]
- *Main> let c = inject [3]
- *Main> a >>> (b >>> inverse b)
- K [1,2] [2]
- *Main> a >>> (b >>> inverse b) >>> c
- K [1,2,3] [2]
- We would expect (b >>> inverse b) to be not only equal to e in the sense of the (==)
- equality function we defined but to be interchangeable with all e in all contexts,
- *Main> a >>> e >>> c
- K [1,3] []
- *Main> a >>> (b >>> inverse b) >>> c == a >>> e >>> c
- False
- Damn! That's definitely not right!
- The problem stems from the lack of commutativity, so it seem that the commutativity of N
- that may have seemed incidental to our success in constructing Z is not so incidental
- after all.
- To verify that the construction indeed works for commutative monoids other than N, let's
- explore some related examples. It turned out that lists (free mononoids) did not work due
- to the non-commutativity of list concatenation. What are the closest thing to lists
- while having a commutative kind of concatenation? Sets of course! The Set type constructor
- in fact corresponds to the free commutative monoid construction. Given a type X that acts
- as a generating set, Set X is the freest possible commutative monoid with X as generators.
- Let's replay the failing example with sets instead of lists.
- *Main> let a = inject (singleton 1)
- *Main> let b = inject (singleton 2)
- *Main> let c = inject (singleton 3)
- *Main> a >>> (b >>> inverse b) >>> c == a >>> e >>> c
- True
- Yay! It worked!
- If K N were the integers then what is K (Set X)? Because of the commutativity, the different
- generators don't really interact, so you'd expect it to be a product of integers, one copy
- for each value in X. That is, K (Set X) is isomorphic to the function type X -> Z.