automation in category theory

Stream: maths

[Kevin Buzzard]

Hey, I was just comparing notes with @Calle Sönne because we were both trying to prove that equalizer(f,g)=equalizer(g,f). His proof looks like this:

lemma comm_of_equalizer : equalizer f g ≅ equalizer g f :=
begin
  refine_struct { hom := equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
  inv := equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)), },
  rw [←limit.w (parallel_pair f g) walking_parallel_pair_hom.right, parallel_pair_map_right],
  rw [←limit.w (parallel_pair g f) walking_parallel_pair_hom.right, parallel_pair_map_right],
end

but I've just realised that this proof has non-terminal simps in! The definition of category_theory.iso is

structure iso {C : Type u} [category.{v} C] (X Y : C) :=
(hom : X ⟶ Y)
(inv : Y ⟶ X)
(hom_inv_id' : hom ≫ inv = 𝟙 X . obviously)
(inv_hom_id' : inv ≫ hom = 𝟙 Y . obviously)

and those autoparams fire in both cases, and I believe they apply simp in both cases (and several other things). In neither case does obviously close the goal though, so we have non-terminal simps here. I rewrote as

def equalizer.symm.hom : equalizer g f ⟶ equalizer f g :=
equalizer.lift _ _ (equalizer.ι g f) (equalizer.condition g f).symm

def equalizer.symm : equalizer f g ≅ equalizer g f :=
{ hom := equalizer.symm.hom g f,
  inv := equalizer.symm.hom f g,
  hom_inv_id' := begin
    suffices : limits.equalizer.ι f g ≫ g = limits.limit.π (limits.parallel_pair f g) limits.walking_parallel_pair.one,
      obviously,
    rw [←limit.w (parallel_pair f g) walking_parallel_pair_hom.right, parallel_pair_map_right]
  end,
  inv_hom_id' := begin
    suffices : limits.equalizer.ι g f ≫ f = limits.limit.π (limits.parallel_pair g f) limits.walking_parallel_pair.one,
      obviously,
    rw [←limit.w (parallel_pair g f) walking_parallel_pair_hom.right, parallel_pair_map_right],
  end}

and I think this avoids them. I would never have noticed the non-terminal simps if I'd been reviewing this code. [NB one needs local attribute [tidy] tactic.case_bash for this proof to work]

[Johan Commelin]

The second version is what the library code usually looks like

[Johan Commelin]

One red flag is that the first piece of code is a lemma where it should be a def. Once that is fixed, the fact that the data is defined with begin ... end is another reddish flag.

[Johan Commelin]

Once you start fixing that, by writing down the constructor directly. You converge towards the latter codeblock automatically

[Johan Commelin]

One thing you'll notice is that almost every def in the category lib is followed by some simp-lemmas. (Although there are now attributes that take some of this job out of your hands.) Is there a natural simp-lemma that should follow your definitions?

[Johan Commelin]

I guess you can tag @[simps] before def equalizer.symm to get some useful simp lemmas.

[Johan Commelin]

Also, we should think about whether the stuff following suffices : this_stuff_is_what_I_mean can be simplified further with a suitable simp-lemma.

[Johan Commelin]

I think you can write a simp-lemma for that fact that simplifies the RHS to the LHS. Once that is done, you can compress your definition to just the hom and inv parts.

[Kevin Buzzard]

Calle asked whether this should be in mathlib and I didn't really know. What I'm learning now is that there's a lot more to getting category theory into mathlib than meets the eye.

I am constantly running into issues in my future plans which will need category theory so I've got to learn it really. Here is a question which stumped me. At some point in the equalizer proof one needs the following fact: if K : limits.fork f g is the limit cone for the equaliser diagram (two maps f and g from A to B, say) then K is an object X and then the data of maps from X to A and B and some theorems (all packaged up as one natural transformation). I wanted to show that if you took the map from X to A and then made a new cone, it was equal to the original cone:

def equalizer.fork : fork f g := limit.cone _

theorem fork_of_equalizer_eq_fork :
  fork.of_ι (equalizer.ι f g) (equalizer.condition f g) = equalizer.fork f g :=
begin
  sorry
end

Then I realised I was missing some sort of cone.ext. And then I realised that this might be a problematic lemma because it's some equality of dependent types in there somewhere. So I decided not to go down that route.

[Kevin Buzzard]

In my application I only needed that a specific map coming from both natural transformations was the same so I could work around it. But it occurred to me that in general one should probably never be attempting to prove that objects are equal, limits are equal, cones are equal...

[Kevin Buzzard]

/-- The braiding isomorphism which swaps a binary product. -/
@[simps] def prod.braiding (P Q : C) : P ⨯ Q ≅ Q ⨯ P :=
{ hom := prod.lift prod.snd prod.fst,
  inv := prod.lift prod.snd prod.fst }

Here automation finishes everything (and again local attribute [tidy] tactic.case_bash). This is from category_theory.limits.shapes.binary_products. The reason it doesn't finish the equalizer question is that Lean doesn't know that if you have a cone for an equalizer diagram X -> -> Y then you can reconstruct it from the map to X.

[Kevin Buzzard]

I see, so Johan is saying that perhaps the missing steps should be simp lemmas.

[Scott Morrison]

Sorry that I've been completely absent for a while, but I think getting some eyes on https://github.com/leanprover-community/mathlib/pull/1622 would be a good idea. Making these changes would, I think, make all this sort of stuff easier.