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 talking about the structure Equiv X Y, with notation X ≃ Y.

Equiv – two inverse bijections

Let X and Y be types. Here’s how mathlib defines a type X ≃ Y whose elements are bijections from X to Y.

/-- `X ≃ Y` is the type of functions from `X` to `Y` with a two-sided inverse. -/
structure Equiv (X Y : Type) where
  toFun : X → Y
  invFun : Y → X
  left_inv : LeftInverse invFun toFun
  right_inv : RightInverse invFun toFun

infixl:25 " ≃ " => Equiv

What’s going on here? The actual name of the type is Equiv X Y, and we set up a (left-associative, binding power 25) notation X ≃ Y for it (as a rule of thumb, if it’s a funny maths character then it’s notation, and if it’s spelt out in normal letters it’s the official name). The line starting with /-- is the docstring for the definition; this ensures that when you hover over Equiv you can see its definition. Note that every definition you write should have a docstring!

The structure we’re defining here has four fields: two functions and two proofs. To make a term of this type, you have to supply four things:

  1. a map from X to Y

  2. a map from Y to X

  3. a proof that if you do the map from X to Y and then the map from Y to X you get back to where you started;

  4. same as (3) but start at Y then go to X then back to Y.

In other words, you need to supply two maps and then a proof that one is the two-sided inverse of the other.

If you have read something about inductive types – X ≃ Y is an inductive type, with one constructor (called Equiv.mk internally) which takes as inputs the four things above, and then outputs a term of type X ≃ Y.

Let’s let X and Y both be the integers, and let’s let the map from X to Y send n to n+37. Then the inverse map sends n to n-37, and the ring tactic will be able to prove that (n+37)-37=n, so we should be able to make a term of type ℤ ≃ ℤ using this data. Let’s call it e. By the way, I started writing this definition by typing def e : ℤ ≃ ℤ := _ and then clicking on the blue lightbulb and selecting the option which mentioned structures.

def e : ℤ ≃ ℤ where
  toFun n := n + 37
  invFun m := m - 37
  left_inv := by
    intro n
    -- some messy goal with a bunch of ``fun`` in
    dsimp only -- tidy up
    -- ⊢ n + 37 - 37 = n
    ring
  right_inv := by
    intro m
    ring -- don't actually need to tidy up

You can think of e as a 4-tuple: two functions, and two proofs. How do you get this information from the term e? You can use functions like Equiv.toFun etc, which were created under the hood when Equiv was defined. Here are some examples of how to use the “parts” of e. Note that because the type of e is Equiv [something], e.toFun is short for Equiv.toFun e. This is Lean’s dot notation in action.

#check Equiv.toFun e -- ℤ → ℤ
#check e.toFun -- ℤ → ℤ

example : e.toFun 1 = 38 := by
  simp only [e] -- replace ``e`` with its definition
  -- ⊢ 1 + 37 = 38
  norm_num

example (x : ℤ) : e.invFun x = x - 37 := by
  rfl

example : ∀ x : ℤ, e.invFun (e.toFun x) = x :=
  e.left_inv

The final thing I’ll explain is the coercion associated to the bijection. We sometimes want to think of e as a function from ℤ to ℤ, and forget the fact that it’s really an Equiv. We could do this by talking about e.toFun all the time, but Lean will just let you use e as a function:

example : e 1 = 38 := by
  dsimp [e]
  -- ⊢ 1 + 37 = 38
  norm_num

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; it sends a bijection to the associated function! There’s a coercion defined from Equiv X Y to X → Y and this coercion is applied automatically when e receives the “input” 1.