## Stream: maths

### Topic: Category exercice

#### orlando (Mar 19 2020 at 14:37):

Hello, it is not a question but a I suggest a little exercise to learn a little category theory, if somebody want to play :upside_down:

import category_theory.functor_category
open category_theory
open category_theory.category
universes v₁ v₂ u₁ u₂

variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
include 𝒞 𝒟

variables (X Y U V: C)
variables (f : X ⟶ Y) (g : V ⟶ U)(h : Y ⟶ V)
variables (F G  : C ⥤ D)
variables (α : F ⟶ G)

/- The diagram coming from g and α
F(f)        F(h)       F(g)
F X ---> F Y  --->  F V   ----> F U
|        |           |          |
|α(X)    |α(Y)       | α (v)    |  α (U)
v        v           v          v
G X ---> G Y ---->    G(V) ---- G(U)
G(f)       G(h)         G(g)
commutes.
-/
example : F.map f ≫  α.app Y ≫ G.map h ≫  G.map g   =  F.map f ≫ F.map h ≫ α.app V  ≫ G.map g := begin simp, end  --- :)


#### Kevin Buzzard (Mar 19 2020 at 14:44):

Does simp work for you?

no !!!

#### Kevin Buzzard (Mar 19 2020 at 14:47):

Did you see the intro file for category theory? Maybe a bunch of rewrites does it

#### orlando (Mar 19 2020 at 14:48):

I need to do some step !

example : F.map f ≫  α.app Y ≫ G.map h ≫  G.map g   =  F.map f ≫ F.map h ≫ α.app V  ≫ G.map g :=  begin
rw ← G.map_comp h g,
rw ← α.naturality (h ≫ g),
simp,
end


#### Reid Barton (Mar 19 2020 at 14:49):

We don't have these naturality squares as simp lemmas because it's not clear in which direction you want to rewrite.

#### orlando (Mar 19 2020 at 14:50):

Kevin, Yes i read the intro (it's good text !!!) , and i make this exercice to manipulate i little !

#### Reid Barton (Mar 19 2020 at 14:50):

It might be better to just pick a direction (arbitrarily?) as the simp-direction though

#### Kevin Buzzard (Mar 19 2020 at 14:50):

but any schoolkid could prove this by rewriting

#### Kevin Buzzard (Mar 19 2020 at 14:51):

so where's the tactic?

#### Reid Barton (Mar 19 2020 at 14:51):

rewrite_search?

#### Kevin Buzzard (Mar 19 2020 at 14:52):

unknown identifier? :-(

#### Reid Barton (Mar 19 2020 at 14:52):

I don't know, I've thought about having some robust tactic for this kind of equational reasoning in category theory, like a ring for categories, but it hasn't been a pressing concern

same !

#### Kevin Buzzard (Mar 19 2020 at 14:52):

@orlando the tactic which should solve this goal is still being written

#### Kevin Buzzard (Mar 19 2020 at 14:53):

I don't know to what extent it exists yet

#### Kevin Buzzard (Mar 19 2020 at 14:53):

myaybe it half-exists?

#### Kevin Buzzard (Mar 19 2020 at 14:57):

example : F.map f ≫  α.app Y ≫ G.map h ≫  G.map g   =  F.map f ≫ F.map h ≫ α.app V  ≫ G.map g :=
begin
congr' 1,
rw ←assoc,
rw ←assoc,
congr' 1,
rw ←nat_trans.naturality,
end


#### Kevin Buzzard (Mar 19 2020 at 14:57):

example : F.map f ≫  α.app Y ≫ G.map h ≫  G.map g   =  F.map f ≫ F.map h ≫ α.app V  ≫ G.map g :=
begin
apply congr_arg,
rw ←assoc,
rw ←assoc,
apply congr_fun,
rw ←nat_trans.naturality,
end


#### orlando (Mar 19 2020 at 14:59):

oh nice : congr' 1,

#### Kevin Buzzard (Mar 19 2020 at 15:09):

here is the sorry I'm working on, I'm also trying to learn category theory

#### Kevin Buzzard (Mar 19 2020 at 15:54):

@orlando when I get to a computer again I'll write your tactic :-)

#### Kevin Buzzard (Mar 19 2020 at 16:51):

the proof was rfl by the way :-)

#### orlando (Mar 19 2020 at 16:53):

@Kevin Buzzard : I try to read your file : i have a determinist timeout with " tidy " i don't know tidy, what is it ?

#### Kevin Buzzard (Mar 19 2020 at 16:53):

@Scott Morrison wrote it, I don't understand it -- for me it is just like all the other tactics which sometimes solve a goal and sometimes don't.

#### Kevin Buzzard (Mar 19 2020 at 16:54):

I only just learnt what rewrite_search did today after Reid's comment above.

#### Scott Morrison (Mar 19 2020 at 16:55):

tidy, more or less, attempts to solve goals by "decomposing into pieces" and then using simp lemma. When it does work, you can ask it to report what it did by writing tidy?

#### Scott Morrison (Mar 19 2020 at 16:55):

Often it is a some sequence of intros, ext, dsimp, and simp, but sometimes manages some more exotic steps.

#### Scott Morrison (Mar 19 2020 at 16:55):

It essentially contains a list of tactics to try, and it keeps trying tactics from that list until nothing makes further progress.

#### Scott Morrison (Mar 19 2020 at 16:56):

In particular, it has potentially unbounded run time. And sometimes it does very dumb things.

#### Scott Morrison (Mar 19 2020 at 16:56):

(But once you get the hang of when it does work, it works great.)

#### Scott Morrison (Mar 19 2020 at 16:57):

Kevin Buzzard said:

I only just learnt what rewrite_search did today after Reid's comment above.

Note that rewrite_search doesn't exist in mathlib... We started attempting to PR it, but got bogged down.

#### Scott Morrison (Mar 19 2020 at 16:57):

It is awesome. :-)

#### orlando (Mar 19 2020 at 16:58):

And the notion of : Module.of ? I thinck it's a tool to "categorify " ?

#### Johan Commelin (Mar 19 2020 at 17:06):

It's a tool to "bundle" the underlying type of a module together with the module structure.

#### Johan Commelin (Mar 19 2020 at 17:06):

As a side effect, it becomes an object of the category of modules.

#### Kevin Buzzard (Mar 19 2020 at 17:08):

@orlando you already know that the usual way to do rings in Lean is variables (R : Type) [comm_ring R]. But there is also a category of rings, where you just put R : Ring. These are two different ways of storing the same data in the computer, and this of thing moves from one to the other.

#### Kevin Buzzard (Mar 19 2020 at 17:10):

It is an implementation issue which is not interesting to mathematicians but becomes important if you want to do this stuff seriously.

#### Kevin Buzzard (Mar 19 2020 at 18:48):

There is something wrong with my tactic :-(

import category_theory.functor_category
open category_theory
open category_theory.category
universes v₁ v₂ u₁ u₂

variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
include 𝒞 𝒟

variables (X Y U V: C)
variables (f : X ⟶ Y) (g : V ⟶ U)(h : Y ⟶ V)
variables (F G  : C ⥤ D)
variables (α : F ⟶ G)

/- The diagram coming from g and α
F(f)        F(h)       F(g)
F X ---> F Y  --->  F V   ----> F U
|        |           |          |
|α(X)    |α(Y)       | α (v)    |  α (U)
v        v           v          v
G X ---> G Y ---->    G(V) ---- G(U)
G(f)       G(h)         G(g)
commutes.
-/

meta def poor_mans_rewrite_search : tactic unit := do
[iterate 5
{ repeat {rw assoc},
try {rw nat_trans.naturality},
try {simp},
repeat {rw ←assoc},
try {rw nat_trans.naturality},
try {simp}
}]
example :
F.map f ≫  α.app Y ≫ G.map h ≫  G.map g =
F.map f ≫ F.map h ≫ α.app V  ≫ G.map g :=
begin
poor_mans_rewrite_search, -- fails
end


#### Kevin Buzzard (Mar 19 2020 at 18:49):

this

example :
F.map f ≫  α.app Y ≫ G.map h ≫  G.map g =
F.map f ≫ F.map h ≫ α.app V  ≫ G.map g :=
begin
iterate 5
{ repeat {rw assoc},
try {rw nat_trans.naturality},
try {simp},
repeat {rw ←assoc},
try {rw nat_trans.naturality},
try {simp}
}
end


works fine (and the same tactic should solve other goals of this nature)

#### Kevin Buzzard (Mar 19 2020 at 18:51):

It solves this:

  α.app X ≫  G.map f ≫ G.map h ≫  G.map g =
F.map f ≫ F.map h ≫ F.map g  ≫ α.app U :=


#### Kevin Buzzard (Mar 19 2020 at 18:52):

and even this:

  α.app X ≫  G.map f ≫ 𝟙 (G.obj Y) ≫ G.map h ≫  G.map g =
F.map f ≫ F.map h ≫ F.map g  ≫ α.app U :=


#### orlando (Mar 19 2020 at 19:00):

That nice !!! Why hte meta programming fails

#### Kevin Buzzard (Mar 19 2020 at 19:00):

yeah but it would be good to make it into a tactic and I can't work out how :-/

#### Kevin Buzzard (Mar 19 2020 at 19:03):

Thanks to Chris Hughes who pointed out that it's the include that is causing the problem. You have to move the meta def before the include.

#### Kevin Buzzard (Mar 19 2020 at 19:03):

import category_theory.functor_category
open category_theory
open category_theory.category
universes v₁ v₂ u₁ u₂

meta def poor_mans_rewrite_search : tactic unit := do
[iterate 5
{ repeat {rw assoc},
try {rw nat_trans.naturality},
try {simp},
repeat {rw ←assoc},
try {rw nat_trans.naturality},
try {simp}
}]

variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
include 𝒞 𝒟

variables (X Y U V: C)
variables (f : X ⟶ Y) (g : V ⟶ U)(h : Y ⟶ V)
variables (F G  : C ⥤ D)
variables (α : F ⟶ G)

/- The diagram coming from g and α
F(f)        F(h)       F(g)
F X ---> F Y  --->  F V   ----> F U
|        |           |          |
|α(X)    |α(Y)       | α (v)    |  α (U)
v        v           v          v
G X ---> G Y ---->    G(V) ---- G(U)
G(f)       G(h)         G(g)
commutes.
-/

example :
α.app X ≫  G.map f ≫ 𝟙 (G.obj Y) ≫ G.map h ≫  G.map g =
F.map f ≫ F.map h ≫ F.map g  ≫ α.app U :=
begin
poor_mans_rewrite_search -- works :-)
end


#### Kevin Buzzard (Mar 19 2020 at 19:04):

He also suggested a better tactic, which I'll write next

#### Mario Carneiro (Mar 19 2020 at 19:17):

you could also omit inside a section if you don't want to move it

#### Scott Morrison (Mar 19 2020 at 19:26):

You should also try the conv_lhs { slice 3 4, ... } idiom for dealing with associativity. This slice tactic could do with some work, but it mostly works. It rearranges brackets for you and zooms in to the "3rd through 4th" morphisms in a chain.

#### Kevin Buzzard (Mar 19 2020 at 19:28):

Here's Chris' suggestion:

def comp_right_app {W : D} {j : G.obj V ⟶ W} :
F.map h ≫ (α.app V) ≫ j =
α.app Y ≫ (G.map h) ≫ j :=
begin
rw ←assoc,
rw nat_trans.naturality,
apply assoc
end

omit 𝒞 𝒟

meta def poor_mans_rewrite_search : tactic unit := do
[{ repeat {rw assoc},
try {simp},
repeat {rw comp_right_app},
repeat {rw nat_trans.naturality},
}]

include 𝒞 𝒟

example :
α.app X ≫  G.map f ≫ 𝟙 (G.obj Y) ≫ G.map h ≫  G.map g =
F.map f ≫ F.map h ≫ F.map g  ≫ α.app U :=
begin
poor_mans_rewrite_search
end


#### Kevin Buzzard (Mar 19 2020 at 19:28):

Like mul_left_comm but for natural transformations

#### Johan Commelin (Mar 19 2020 at 19:52):

Doesn't comp_right_app already exist by the reassoc machinery?

#### Kevin Buzzard (Mar 19 2020 at 20:02):

Maybe, I don't know anything about any machinery. I was just trying to make a simple tactic which solved goals like this.

#### Scott Morrison (Mar 20 2020 at 17:36):

It turns out comp_right_app didn't exist, but should have and does now, see #2200. by simp` now suffices.

#### Kevin Buzzard (Mar 20 2020 at 17:44):

Oh nice! @orlando you found a hole in the library!

Last updated: May 19 2021 at 00:40 UTC