Category exercice

Stream: maths

[orlando]

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]

Does simp work for you?

[orlando]

no !!!

[Kevin Buzzard]

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

[orlando]

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]

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

[orlando]

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

[Reid Barton]

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

[Kevin Buzzard]

but any schoolkid could prove this by rewriting

[Kevin Buzzard]

so where's the tactic?

[Reid Barton]

rewrite_search?

[Kevin Buzzard]

unknown identifier? :-(

[Reid Barton]

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

[orlando]

same !

[Kevin Buzzard]

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

[Kevin Buzzard]

I don't know to what extent it exists yet

[Kevin Buzzard]

myaybe it half-exists?

[Kevin Buzzard]

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]

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]

oh nice : congr' 1,

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

the proof was rfl by the way :-)

[orlando]

@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]

@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]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

It is awesome. :-)

[orlando]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

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]

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]

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]

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]

That nice !!! Why hte meta programming fails

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

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]

Like mul_left_comm but for natural transformations

[Johan Commelin]

Doesn't comp_right_app already exist by the reassoc machinery?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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