Zulip Chat Archive

Stream: maths

Topic: automation in category theory


view this post on Zulip Kevin Buzzard (Dec 07 2019 at 13:41):

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]

view this post on Zulip Johan Commelin (Dec 07 2019 at 13:58):

The second version is what the library code usually looks like

view this post on Zulip Johan Commelin (Dec 07 2019 at 13:59):

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.

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:00):

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

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:02):

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?

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:03):

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

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:04):

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.

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:06):

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.

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 14:12):

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.

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 14:14):

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...

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 15:34):

/-- 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.

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 15:35):

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

view this post on Zulip Scott Morrison (Dec 07 2019 at 23:25):

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.


Last updated: May 11 2021 at 16:22 UTC