# Zulip Chat Archive

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