.. _structures:

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 :math:`G` and :math:`H` be groups. A group homomorphism :math:`f:G\to H` is a function :math:`f` from :math:`G` to :math:`H` satisfying :math:`f(ab)=f(a)f(b)` for all :math:`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 :math:`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:

.. code-block::

   /-- `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 :math:`\mathrm{Hom}(G,H)` of all group homomorphisms from ``G`` to ``H``; the way to talk about a group homomorphism :math:`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 :ref:`definitionally equal <defeq>` 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

.. code-block::

   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

.. code-block::
   
   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 :ref:`dot notation <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 :ref:`coercions <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.

.. code-block::
   
   /-- `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.