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