Structures

A lot of the time in this course we are concerned with proving theorems. However sometimes it’s interesting to make a new definition, and then prove theorems about the definition. In section 3 we made things like groups, subgroups, and group homomorphisms from first principles, even though mathlib has them already. We made them using structures and classes.

Let’s start by going through the example of group homomorphisms in some detail. The Lean code is in sheet 4 of section 3. A group homomorphism is a structure, so it will serve as an example of how structures work.

The mathematics

Let \(G\) and \(H\) be groups. A group homomorphism \(f:G\to H\) is a function \(f\) from \(G\) to \(H\) satisfying \(f(ab)=f(a)f(b)\) for all \(a,b\in G\). So, pedantically speaking, a group homomorphism is a pair consisting of a function and a proof.

The Lean

In Lean the way to say “let \(G\) be a group” is variable (G : Type) [group G]. We’ll talk more about this later when we get onto classes (group G is a class) but let’s not worry about this now. Here is the definition of a group homomorphism from G to H in sheet 4 of section 3:

/-- `my_group_hom G H` is the type of group homomorphisms from `G` to `H`. -/
@[ext] structure my_group_hom (G H : Type) [group G] [group H] :=
(to_fun : G → H)
(map_mul' (a b : G) : to_fun (a * b) = to_fun a * to_fun b)

The first line, starting with /--, is the docstring for the definition, i.e., an explanation of the definition in human language. This means that whenever you see my_group_hom in some Lean code, hovering over my_group_hom will display a pop-up with this explanation.

The next line (@[ext] structure...) announces that we’re going to make a new structure called my_group_hom which takes as input two groups G and H. The result of this command will be a new type my_group_hom G H, the type of group homomorphisms from G to H. Remember that a type is just a collection of stuff, like a set; here we are making the collection \(\mathrm{Hom}(G,H)\) of all group homomorphisms from G to H; the way to talk about a group homomorphism \(f:G\to H\) will be f : my_group_hom G H (although in the file in section 3 I actually make notation f : G →** H for this; I would have used f : G →* H but that notation is already taken by Lean’s actual group homomorphisms).

The @[ext] tag on the structure means that it’s tagged with the @[ext] attribute. Group homomorphisms, like most things in maths, are extensional objects: two group homomorphisms are equal iff they take the same value on every input. Tagging the structure with this @[ext] attribute automatically generates some lemmas my_group_hom.ext and my_group_hom.ext_iff expressing this idea. Extensionality for group homomorphisms is provable in Lean whether or not you tag the structure; the advantage of tagging the structure is simply that the system generates the lemmas automatically.

The remaining two lines in the definition are the fields of the structure; they are a list of the data which we have to give to Lean to make a group homomorphism. The data is unsurprising: we want a function (called to_fun) which defines a map from G to H, and then we want an axiom map_mul' which says that for all a b : G, to_fun (a * b) = to_fun(a) * to_fun(b) (and note the usual functional programming trick of leaving off the brackets). Why did we put a prime on map_mul? We’ll come back to this later; the point is that we want map_mul to be something definitionally equal but syntactically more beautiful.

So that’s it for the definition. A group homomorphism is then two pieces of data; the function, and the axiom that it preserves multiplication. We have made a new type my_group_hom G H. The next thing we need to know is its constructor and eliminators; in less computer-sciency terms, we need to know how to make a term of this type, and also how to get at the data (the function and the proof), given a term of this type.

Lean has a standard way of making any inductive type with one constructor; the pointy bracket constructor. If φ : G → H and h : ∀ a b : G, φ (a * b) = φ a * φ b then we can make the group homomorphism associated to this data simply as ⟨φ, h⟩ : my_group_hom G H. But there are classier ways to make a term of a structure. If you write

def f : my_group_hom G H :=
_

in VS Code, and put your cursor near the _, then a light bulb will pop up. Clicking on the light bulb and selecting “generate a skeleton for the structure under construction” will give you

def f : my_group_hom G H :=
{ to_fun := _,
  map_mul' := _ }

and you can now fill in the underscores with the function and the proof.

So there are two ways of constructing terms of type my_group_hom G H; what is a way of eliminating them, that is, accessing the function and the proof from the group homomorphism? The way structures work is that the full names of the fields become new functions which are added to Lean. When the structure is created, Lean generates a function my_group_hom.to_fun, which takes as input f : my_group_hom G H and outputs the function G → H. It also generates a function my_group_hom.map_mul' which takes as input f : my_group_hom G H and spits out a proof that my_group_hom.to_fun f preserves multiplication.

Because my_group_hom.to_fun takes as input a term f of type my_group_hom..., this means that Lean’s dot notation applies, giving us a shorthand; instead of writing my_group_hom.to_fun f we can write f.to_fun. Similarly, we can write f.map_mul' : ∀ (a b : G), f.to_fun (a * b) = f.to_fun a * f.to_fun b.

But dot notation does not solve the actual problem which we face here. Lean pedantically distinguishes between the function G → H and the group homomorphism f : my_group_hom G H; a group homomorphism is a pair consisting of a function and a proof. That’s all very funny of course, but in practice mathematicians don’t want that pedantry; given a group homomorphism f : my_group_hom G H they want to talk about f g for g : G, and not is_group_hom.to_fun f g or even f.to_fun g. We finish by explaining how to make this work.

Lean has things called coercions. This is a way that given a term x of one type, you can “pretend” that it has a different type. What is actually happening is that a function which is essentially invisible to mathematicians is being called; the function is usually omitted completely by mathematicians, and is typically denoted by some kind of up arrow in Lean. One of the coercion capabilities that Lean has is that you can set up a coercion which takes a term of some type (like f : my_group_hom G H) and coerces it to be a function with notation ⇑f : G → H. Furthermore, you do not even need to type that ⇑ up-arrow (which you do with \u= by the way); once the coercion is defined, you can just write f g and Lean will make sense of this.

We finish by looking at all the Lean code used to define group homomorphisms, and explain what it all means.

/-- `my_group_hom G H` is the type of group homomorphisms from `G` to `H`. -/
@[ext] structure my_group_hom (G H : Type) [group G] [group H] :=
(to_fun : G → H)
(map_mul' (a b : G) : to_fun (a * b) = to_fun a * to_fun b)

namespace my_group_hom

-- throughout this sheet, `G` and `H` will be groups.
variables {G H : Type} [group G] [group H]

-- We use notation `G →** H` for the type of group homs from `G` to `H`.
notation G ` →** ` H := my_group_hom G H

-- A group hom is a function, and so we set up a "coercion"
-- so that a group hom can be regarded as a function (even
-- though it's actually a pair consisting of a function and an axiom)
instance : has_coe_to_fun (G →** H) (λ _, G → H) :=
{ coe := my_group_hom.to_fun }

-- Notice that we can now write `f (a * b)` even though `f` isn't actually a
-- function, it's a pair consisting of a function `f.to_fun` and an axiom `f.map_mul'`.
-- The below lemma is how we want to use it as mathematicians though.
lemma map_mul (f : G →** H) (a b : G) :
  f (a * b) = f a * f b :=
begin
  -- the point is that f.map_mul and f.map_mul' are *definitionally equal*
  -- but *syntactically different*, and the primed version looks uglier.
  -- The point of this lemma is that `f.map_mul` looks nicer.
  exact f.map_mul' a b
end

end my_group_hom -- close namespace

After the structure my_group_hom G H is defined, we move into the my_group_hom namespace. This means that any definitions we make here (for example definition foo := ... will actually be called my_group_hom.foo.

The first thing we do is to set up notation G →** H for my_group_hom G H. I would have used G →* H but that’s already used for Lean’s “official” group homomorphisms.

The next thing is to set up the coercion from G →** H to G → H. The coercion is the function my_group_hom.to_fun which takes a group homomorphism to its underlying function.

And now we magically have the ability to write things like f a instead of f.to_fun a! So we can define map_mul (without the ') to say f (a * b) = f a * f b, which is the expression we want to be using. Because this definition is made in the my_group_hom namespace, it means that if f : G →** H then f.map_mul is the proof of ∀ a b, f (a * b) = f a * f b. Note that f.map_mul and f.map_mul' are definitionally equal, however they are syntactically different, and the unprimed version is the cleaner one.