Zulip Chat Archive

Stream: maths

Topic: Category exercice


view this post on Zulip 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  --- :)

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:44):

Does simp work for you?

view this post on Zulip orlando (Mar 19 2020 at 14:45):

no !!!

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:47):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 !

view this post on Zulip Reid Barton (Mar 19 2020 at 14:50):

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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:50):

but any schoolkid could prove this by rewriting

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:51):

so where's the tactic?

view this post on Zulip Reid Barton (Mar 19 2020 at 14:51):

rewrite_search?

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:52):

unknown identifier? :-(

view this post on Zulip 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

view this post on Zulip orlando (Mar 19 2020 at 14:52):

same !

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:52):

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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:53):

I don't know to what extent it exists yet

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 14:53):

myaybe it half-exists?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip orlando (Mar 19 2020 at 14:59):

oh nice : congr' 1,

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 15:09):

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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 15:54):

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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 16:51):

the proof was rfl by the way :-)

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 16:54):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 19 2020 at 16:56):

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

view this post on Zulip Scott Morrison (Mar 19 2020 at 16:56):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 19 2020 at 16:57):

It is awesome. :-)

view this post on Zulip orlando (Mar 19 2020 at 16:58):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 19 2020 at 17:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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 :=

view this post on Zulip 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 :=

view this post on Zulip orlando (Mar 19 2020 at 19:00):

That nice !!! Why hte meta programming fails

view this post on Zulip 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 :-/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 19:04):

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

view this post on Zulip Mario Carneiro (Mar 19 2020 at 19:17):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 19:28):

Like mul_left_comm but for natural transformations

view this post on Zulip Johan Commelin (Mar 19 2020 at 19:52):

Doesn't comp_right_app already exist by the reassoc machinery?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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