Stream: maths

Topic: automation in category theory

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]

Johan Commelin (Dec 07 2019 at 13:58):

The second version is what the library code usually looks like

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.

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

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?

Johan Commelin (Dec 07 2019 at 14:03):

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

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.

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.

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.

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

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.

Kevin Buzzard (Dec 07 2019 at 15:35):

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

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